branch world: state scoped reads, insert transitions, tip commit

1 files changed, 12 insertions, 7 deletions

diff --git a/docs/virtual-machine-specification.org b/docs/virtual-machine-specification.org
index f84bc84..f244f10 100644
--- a/docs/virtual-machine-specification.org
+++ b/docs/virtual-machine-specification.org
@@ -105,13 +105,18 @@ checks and solving them with the same engine.
 
 * Interaction with stored relations
 
-The engine never owns storage. A world answers =find=; the standalone
-world is an immutable map built by loading; RNT's world is the
-kernel catalog, where tuples are content addressed and a branch tip
-names the state being read. State scoped reads (decision 7) enter
-here: the host resolves =at:= to a snapshot and serves =find= from
-it. Transitions and commit stay outside the engine, in DCL and the
-kernel's single compare and swap (decisions 3, 5, 8).
+The engine never owns storage. A world answers =find=, now state
+scoped: the reserved =at:= label names the state a stored relation
+is read from, stripped before unification and demanded ground before
+the read runs. A world also answers =transition=: transition
+relations like =Insert= are the world's, never the engine's; the VM
+unifies the successor state with =after:= and defers ungrounded
+chains. The standalone world ignores states and has no transitions
+(decision 5). =lib/branch= is the reference stateful world:
+content-addressed states, append-only store, tip per branch, commit
+as compare and swap, and the linearity check of decision 6 over
+transition chains. RNT implements the same contract against its
+kernel. See =docs/states.org=.
 
 * Error and proof obligation reporting