1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
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 is named by a reference,
=#Person=, per decision 15: a dangling reference is simply no
transition.
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.
|
