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