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

1 files changed, 65 insertions, 0 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.