diff options
Diffstat (limited to 'docs')
| -rw-r--r-- | docs/states.org | 65 | ||||
| -rw-r--r-- | docs/virtual-machine-specification.org | 19 |
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 |