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

1 files changed, 46 insertions, 0 deletions

diff --git a/lib/branch.mli b/lib/branch.mli
new file mode 100644
index 0000000..a60d91e
--- /dev/null
+++ b/lib/branch.mli
@@ -0,0 +1,46 @@
+(** The branch world: the reference stateful host.
+
+    This is the RNT-shaped world of decisions 3, 5, 7 and 8, in
+    miniature: states are whole content-addressed trees, a state
+    value is its digest, reads are state-scoped, [Insert] is a
+    transition relation between states, and the single effect is
+    compare-and-swap on a branch tip. The store is append-only;
+    everything else is pure value manipulation.
+
+    The digest is a canonical-serialization hash (a placeholder for
+    RNT's SHA256 content addressing; same shape, weaker hash). *)
+
+type t
+
+val create : schemas:(string * (Label.t * World.primitive) list) list -> t
+(** A world with the given catalog, an empty root state, and one
+    branch, ["main"], whose tip is the root. The catalog is fixed at
+    creation; DDL-as-transition comes with the full catalog work. *)
+
+val find : t -> ?at:Term.t -> string -> World.def option
+(** State-scoped read. [at:] is the state digest (as a string
+    term); omitted, the read sees the ["main"] tip, which is the
+    REPL elaboration rule of decision 7. *)
+
+val transition : t -> string -> Pattern.t Label.Map.t -> World.transition_result option
+(** [Insert relation: "R" tuple: {...} before: S after: S']: checks
+    the tuple against the relation's schema (integrity at the
+    transition, decision 3), stores the successor state, and
+    returns its digest for the VM to unify with [after:]. Stuck
+    until [relation:], [tuple:] and [before:] are ground. *)
+
+val tip : t -> string -> Term.t option
+(** The branch's current state digest. *)
+
+val commit :
+  t -> branch:string -> expect:Term.t -> next:Term.t -> (unit, [ `Conflict ]) result
+(** The single effect (decisions 3 and 8): install [next] as the
+    tip iff the tip still equals [expect]. Everything above this
+    primitive is DCL's business. *)
+
+val linear : World.expr -> (unit, string) result
+(** The linearity discipline of decision 6, checked before running:
+    no state variable is consumed twice (two [before:] uses) or
+    produced twice (two [after:] uses) across the expression's
+    transition applications. Forks are DCL's to express, not a
+    query's. *)