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

2 files changed, 77 insertions, 7 deletions

diff --git a/docs/states.org b/docs/states.org
new file mode 100644
index 0000000..7849918
--- /dev/null
+++ b/docs/states.org
@@ -0,0 +1,65 @@
+#+TITLE: States and Transitions
+
+* About
+
+This document describes =lib/branch=, the reference stateful world,
+and the engine support it stands on: state scoped reads and
+transition relations. It is the database half of Sol, decisions 3,
+5, 6, 7 and 8 running in miniature. RNT implements the same =WORLD=
+contract against its kernel; this module is the working model of
+that shape.
+
+* The world contract grew
+
+A world now answers three things: which relation lives under a name,
+at which state, and which names are transition relations. The
+standalone world ignores states (it is its own single, eternal
+state) and has no transitions, exactly as decision 5 prescribes. The
+pure fragment did not move.
+
+* States
+
+A state is the whole tree: every relation's stored tuples, content
+addressed. The state value is its digest, computed from a canonical
+serialization, so equal states are equal values. The store is append
+only. The digest here is a placeholder hash with the same shape as
+RNT's SHA256 content addressing.
+
+* Reads
+
+A stored relation is read at a state: =[Person name: N at: S]=. The
+=at:= label is reserved, stripped before unification, and must be
+ground before the read runs; an unbound state defers the goal like
+any other waiting constraint. A read without =at:= sees the =main=
+tip, which is the elaboration rule of decision 7 for bare queries.
+
+* Transitions
+
+=Insert= is a relation between states:
+
+#+BEGIN_SRC sol
+[Insert relation: "Person" tuple: {name: "Ana" age: 12} before: S1 after: S2]
+#+END_SRC
+
+It holds when the successor of =S1= by admitting that tuple is =S2=.
+The tuple must match the relation's schema exactly and satisfy its
+domains, or there is no such transition: integrity is part of the
+relation, not a hook bolted on. Solving computes successor states
+and binds them; nothing moves. The relation name is a string for
+now, a provisional notation until relation references in term
+position get their own decision.
+
+Sequencing is the chain: =before: S1 after: S2= in one application,
+=before: S2= in the next. Conjunction stays commutative; the order
+comes from the dataflow. The linearity check of decision 6 rejects
+forks before running: no state variable is consumed twice or
+produced twice inside one expression.
+
+* Commit
+
+The single effect. =commit= installs a new tip iff the tip still
+equals the expected state: compare and swap, nothing else. A stale
+expectation conflicts and the caller decides what to do, because
+conflict policy is DCL's business, not the kernel's (decision 8).
+The tests drive the whole story: solve a chain, observe the tip
+unmoved, commit once, watch the stale second commit conflict.
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