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

10 files changed, 523 insertions, 18 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
 
diff --git a/lib/branch.ml b/lib/branch.ml
new file mode 100644
index 0000000..a1382c6
--- /dev/null
+++ b/lib/branch.ml
@@ -0,0 +1,162 @@
+module String_map = Map.Make (String)
+
+type state = Term.t Label.Map.t list String_map.t
+(* relation name -> stored tuples, the whole tree of one state *)
+
+type t = {
+  schemas : (Label.t * World.primitive) list String_map.t;
+  states : (string, state) Hashtbl.t;  (* digest -> state; append-only *)
+  mutable tips : (string * string) list;  (* branch -> digest; the one mutable place *)
+}
+
+let forced_label name =
+  match Label.of_string name with Ok l -> l | Error _ -> assert false
+
+let relation_l = forced_label "relation"
+let tuple_l = forced_label "tuple"
+let before_l = forced_label "before"
+let after_l = forced_label "after"
+
+(* Canonical serialization: relations in name order (the map gives
+   it), tuples in term order, printed in canonical notation. Equal
+   states digest equally because terms are canonical by
+   construction. *)
+let digest_of_state (state : state) =
+  let buffer = Buffer.create 256 in
+  String_map.iter
+    (fun name tuples ->
+      Buffer.add_string buffer name;
+      let terms =
+        List.map (fun tuple -> Term.record (Label.Map.bindings tuple)) tuples
+        |> List.filter_map Result.to_option
+        |> List.sort Term.compare
+      in
+      List.iter
+        (fun term -> Buffer.add_string buffer (Format.asprintf "|%a" Term.pp term))
+        terms;
+      Buffer.add_char buffer '\n')
+    state;
+  Digest.to_hex (Digest.string (Buffer.contents buffer))
+
+let store world state =
+  let digest = digest_of_state state in
+  if not (Hashtbl.mem world.states digest) then
+    Hashtbl.add world.states digest state;
+  digest
+
+let create ~schemas =
+  let catalog =
+    List.fold_left
+      (fun acc (name, schema) -> String_map.add name schema acc)
+      String_map.empty schemas
+  in
+  let root : state =
+    String_map.map (fun _ -> []) catalog
+  in
+  let world = { schemas = catalog; states = Hashtbl.create 16; tips = [] } in
+  let root_digest = store world root in
+  world.tips <- [ ("main", root_digest) ];
+  world
+
+let state_at world = function
+  | Some (Term.String digest) -> Hashtbl.find_opt world.states digest
+  | Some _ -> None
+  | None -> (
+      match List.assoc_opt "main" world.tips with
+      | Some digest -> Hashtbl.find_opt world.states digest
+      | None -> None)
+
+let find world ?at name =
+  match (String_map.find_opt name world.schemas, state_at world at) with
+  | Some schema, Some state ->
+      let facts = Option.value ~default:[] (String_map.find_opt name state) in
+      let schema = List.map (fun (l, p) -> (l, World.Primitive p)) schema in
+      Some (World.Table { schema; facts })
+  | _ -> None
+
+(* [Insert]: the transition relation between states (decision 3).
+   Ground relation name, ground tuple, ground predecessor state;
+   the tuple must match the schema exactly and satisfy its
+   primitive domains, or there is no such transition. *)
+let insert world bindings =
+  let ground label =
+    Option.bind (Label.Map.find_opt label bindings) Pattern.to_term
+  in
+  match (ground relation_l, ground tuple_l, ground before_l) with
+  | Some (Term.String relation), Some (Term.Record tuple), Some (Term.String before)
+    -> (
+      match
+        (String_map.find_opt relation world.schemas, Hashtbl.find_opt world.states before)
+      with
+      | Some schema, Some state ->
+          let conforms =
+            List.length schema = Label.Map.cardinal tuple
+            && List.for_all
+                 (fun (label, domain) ->
+                   match Label.Map.find_opt label tuple with
+                   | Some value -> World.member_of_primitive value domain
+                   | None -> false)
+                 schema
+          in
+          if not conforms then World.T_fail
+          else
+            let facts = Option.value ~default:[] (String_map.find_opt relation state) in
+            let successor = String_map.add relation (facts @ [ tuple ]) state in
+            World.T_state (Term.string (store world successor))
+      | _ -> World.T_fail)
+  | Some _, Some _, Some _ -> World.T_fail
+  | _ ->
+      (* Something essential is not ground yet: wait for the chain. *)
+      World.T_stuck
+
+let transition world name bindings =
+  match name with "Insert" -> Some (insert world bindings) | _ -> None
+
+let tip world branch =
+  Option.map Term.string (List.assoc_opt branch world.tips)
+
+(* The single effect: compare-and-swap on the tip (decision 8). *)
+let commit world ~branch ~expect ~next =
+  match (expect, next, List.assoc_opt branch world.tips) with
+  | Term.String expected, Term.String next_digest, Some current
+    when String.equal current expected && Hashtbl.mem world.states next_digest ->
+      world.tips <-
+        (branch, next_digest) :: List.remove_assoc branch world.tips;
+      Ok ()
+  | _ -> Error `Conflict
+
+(* Linearity (decision 6): within one expression, a state variable
+   is consumed at most once as [before:] and produced at most once
+   as [after:]. Sequencing comes from the chain, and the chain must
+   be a chain. *)
+let linear expr =
+  let rec applications = function
+    | World.Apply (name, bindings) -> [ (name, bindings) ]
+    | World.And (a, b) | World.Or (a, b) | World.Not (a, b) | World.Forall (a, b)
+      ->
+        applications a @ applications b
+  in
+  let uses label =
+    applications expr
+    |> List.filter (fun (name, _) -> String.equal name "Insert")
+    |> List.filter_map (fun (_, bindings) ->
+           match Label.Map.find_opt label bindings with
+           | Some (Pattern.Var v) -> Some v
+           | _ -> None)
+  in
+  let duplicate vars =
+    let sorted = List.sort String.compare vars in
+    let rec scan = function
+      | a :: b :: _ when String.equal a b -> Some a
+      | _ :: rest -> scan rest
+      | [] -> None
+    in
+    scan sorted
+  in
+  match (duplicate (uses before_l), duplicate (uses after_l)) with
+  | Some v, _ ->
+      Error
+        (Printf.sprintf
+           "state %s consumed twice: a fork inside one expression is not a chain" v)
+  | _, Some v -> Error (Printf.sprintf "state %s produced twice" v)
+  | None, None -> Ok ()
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. *)
diff --git a/lib/vm.ml b/lib/vm.ml
index 4a11c4d..67efc56 100644
--- a/lib/vm.ml
+++ b/lib/vm.ml
@@ -23,6 +23,12 @@ type solution = {
 module Make (W : World.WORLD) = struct
   exception Stuck of string list
 
+  let forced_label name =
+    match Label.of_string name with Ok l -> l | Error _ -> assert false
+
+  let at_label = forced_label "at"
+  let after_label = forced_label "after"
+
   (* A goal is a proposition to establish or a denial to refute.
      Conjunction flattens; [u :not d] contributes the universe
      positively and the denial negatively. *)
@@ -547,7 +553,22 @@ module Make (W : World.WORLD) = struct
               else if List.mem `Unknown statuses then
                 Wait { residuatable = false }
               else Run [ (subst, []) ])
-    | Positive (World.Apply (name, bindings)) -> (
+    | Positive (World.Apply (name, all_bindings)) -> (
+        (* State-scoped reads (decision 7): the reserved [at:] label
+           names the state a stored relation is read from. It is
+           stripped before unification, since it is not an attribute
+           of any tuple, and must be ground before the read runs. *)
+        let at_pattern =
+          Option.map
+            (Pattern.Subst.resolve subst)
+            (Label.Map.find_opt at_label all_bindings)
+        in
+        let bindings = Label.Map.remove at_label all_bindings in
+        match at_pattern with
+        | Some p when not (Pattern.is_ground p) ->
+            Wait { residuatable = false }
+        | _ -> (
+        let at = Option.bind at_pattern Pattern.to_term in
         match Builtin.run subst name bindings with
         | Some (Builtin.Solved substs) ->
             Run (List.map (fun s -> (s, [])) substs)
@@ -556,7 +577,27 @@ module Make (W : World.WORLD) = struct
                case. Constraining is not searching. *)
             Wait { residuatable = true }
         | None -> (
-            match W.find world name with
+            (* Transitions before stored relations: a world that
+               declares [Insert] answers for it here (decision 3).
+               The successor state unifies with [after:]. *)
+            match
+              W.transition world name
+                (Label.Map.map (Pattern.Subst.resolve subst) bindings)
+            with
+            | Some (World.T_state successor) -> (
+                match Label.Map.find_opt after_label bindings with
+                | None -> Run [ (subst, []) ]
+                | Some pattern -> (
+                    match
+                      Pattern.Subst.unify subst pattern
+                        (Pattern.of_term successor)
+                    with
+                    | Some subst -> Run [ (subst, []) ]
+                    | None -> Run []))
+            | Some World.T_fail -> Run []
+            | Some World.T_stuck -> Wait { residuatable = false }
+            | None -> (
+            match W.find world ?at name with
             | Some (World.Table { facts; _ }) ->
                 Run
                   (List.filter_map
@@ -591,7 +632,7 @@ module Make (W : World.WORLD) = struct
                    checks references. An embedded host that lies
                    about its catalog surfaces here as a stuck goal
                    rather than a crash. *)
-                Wait { residuatable = false }))
+                Wait { residuatable = false }))))
 
   (* Search yields substitutions with the goals they left
      residuated. A state where every remaining goal is residuatable
diff --git a/lib/world.ml b/lib/world.ml
index a053c2c..94fa0a9 100644
--- a/lib/world.ml
+++ b/lib/world.ml
@@ -22,10 +22,15 @@ type def =
   | Table of { schema : (Label.t * domain) list; facts : Term.t Label.Map.t list }
   | Rules of rule list
 
+type transition_result = T_state of Term.t | T_fail | T_stuck
+
 module type WORLD = sig
   type t
 
-  val find : t -> string -> def option
+  val find : t -> ?at:Term.t -> string -> def option
+
+  val transition :
+    t -> string -> Pattern.t Label.Map.t -> transition_result option
 end
 
 type error =
@@ -227,7 +232,8 @@ module String_map = Map.Make (String)
 module Standalone = struct
   type t = def String_map.t
 
-  let find world name = String_map.find_opt name world
+  let find world ?at:_ name = String_map.find_opt name world
+  let transition _ _ _ = None
 
   let schema_of_node ~relation = function
     | Ast.Seq (entries, None) ->
diff --git a/lib/world.mli b/lib/world.mli
index 14f82d3..3868261 100644
--- a/lib/world.mli
+++ b/lib/world.mli
@@ -56,13 +56,34 @@ type def =
       (** Extensional: a schema and finite stored tuples. *)
   | Rules of rule list  (** Intensional: defined by admitted rules. *)
 
+val member_of_primitive : Term.t -> primitive -> bool
+(** Host-decided membership in a primitive domain, with the literal
+    inclusions of decision 12. Exposed so stateful worlds check
+    schemas with exactly the loader's judgment. *)
+
+(** What a transition relation says when consulted (decision 3:
+    transitions are relations over states, provided by the world,
+    never by the engine). *)
+type transition_result =
+  | T_state of Term.t
+      (** The successor state; the VM unifies it with [after:]. *)
+  | T_fail  (** No such transition: integrity violation and kin. *)
+  | T_stuck  (** Arguments not ground yet; the planner defers. *)
+
 (** What a host must answer for the VM to run: which relation lives
-    under a name. Builtins are the VM's own and are not consulted
-    here. *)
+    under a name, optionally at a state ([at:] reads, decision 7),
+    and which names are transition relations. Builtins are the VM's
+    own and are not consulted here. The standalone world has one
+    implicit state and no transitions (decision 5). *)
 module type WORLD = sig
   type t
 
-  val find : t -> string -> def option
+  val find : t -> ?at:Term.t -> string -> def option
+
+  val transition :
+    t -> string -> Pattern.t Label.Map.t -> transition_result option
+  (** [None] when the name is not a transition relation of this
+      world. Bindings arrive resolved. *)
 end
 
 type error
@@ -94,7 +115,13 @@ val expr_of_node : Ast.node -> (expr, error) result
 module Standalone : sig
   type t
 
-  val find : t -> string -> def option
+  val find : t -> ?at:Term.t -> string -> def option
+  (** [at:] is accepted and ignored: the standalone world is its own
+      single, eternal state. *)
+
+  val transition : t -> string -> Pattern.t Label.Map.t -> transition_result option
+  (** Always [None]: no branches, no transitions, the pure
+      fragment. *)
 
   val load : Ast.statement list -> (t * expr list * pending list, error) result
   (** Admits a program: registers relations, checks every fact
diff --git a/test/dune b/test/dune
index 6e5e6eb..f46fc0f 100644
--- a/test/dune
+++ b/test/dune
@@ -1,3 +1,3 @@
 (tests
- (names test_term test_vm test_embedding)
+ (names test_term test_vm test_embedding test_branch)
  (libraries sol zarith alcotest))
diff --git a/test/test_branch.ml b/test/test_branch.ml
new file mode 100644
index 0000000..2cfabdd
--- /dev/null
+++ b/test/test_branch.ml
@@ -0,0 +1,151 @@
+(* The branch world end to end: state-scoped reads, transition
+   chains threading states linearly, integrity at the transition,
+   and the single commit effect. *)
+
+let label s =
+  match Sol.Label.of_string s with
+  | Ok l -> l
+  | Error (`Invalid_label s) -> Alcotest.failf "invalid label: %s" s
+
+module Branch_vm = Sol.Vm.Make (Sol.Branch)
+
+let world () =
+  Sol.Branch.create
+    ~schemas:
+      [
+        ( "Person",
+          [ (label "name", Sol.World.D_string); (label "age", Sol.World.D_integer) ] );
+      ]
+
+let compile source =
+  match Sol.Front.parse_string ("Query expression: " ^ source) with
+  | Ok [ Sol.Ast.Directive ("Query", [ ("expression", node) ]) ] -> (
+      match Sol.World.expr_of_node node with
+      | Ok expr -> expr
+      | Error error ->
+          Alcotest.failf "compile error: %a" Sol.World.pp_error error)
+  | _ -> Alcotest.fail "expected one query"
+
+let solve world expr =
+  match Sol.Branch.linear expr with
+  | Error message -> Alcotest.failf "linearity: %s" message
+  | Ok () -> (
+      match Branch_vm.solve world expr with
+      | Ok solutions -> solutions
+      | Error error -> Alcotest.failf "solve error: %a" Sol.Vm.pp_error error)
+
+let tip_digest world =
+  match Sol.Branch.tip world "main" with
+  | Some (Sol.Term.String digest) -> digest
+  | _ -> Alcotest.fail "no main tip"
+
+let binding solution name =
+  match List.assoc_opt name solution.Sol.Vm.bindings with
+  | Some pattern -> pattern
+  | None -> Alcotest.failf "no binding for %s" name
+
+let test_transition_chain () =
+  let world = world () in
+  let source =
+    Printf.sprintf
+      {| [Insert relation: "Person" tuple: {name: "Marcos" age: 30} before: %S after: S1] :and
+         [Insert relation: "Person" tuple: {name: "Ana" age: 12} before: S1 after: S2] :and
+         [Person name: N age: A at: S2] |}
+      (tip_digest world)
+  in
+  let solutions = solve world (compile source) in
+  Alcotest.(check int) "two people at the final state" 2 (List.length solutions);
+  (* Read your own write mid-chain: only the first insert is
+     visible at S1. *)
+  let mid =
+    Printf.sprintf
+      {| [Insert relation: "Person" tuple: {name: "Marcos" age: 30} before: %S after: S1] :and
+         [Person name: N age: A at: S1] |}
+      (tip_digest world)
+  in
+  Alcotest.(check int) "one person at the middle state" 1
+    (List.length (solve world (compile mid)))
+
+let test_tip_unmoved_until_commit () =
+  let world = world () in
+  let before = tip_digest world in
+  let _ =
+    solve world
+      (compile
+         (Printf.sprintf
+            {| [Insert relation: "Person" tuple: {name: "Rui" age: 70} before: %S after: S1] |}
+            before))
+  in
+  Alcotest.(check string) "solving commits nothing" before (tip_digest world)
+
+let test_commit_and_conflict () =
+  let world = world () in
+  let root = tip_digest world in
+  let solutions =
+    solve world
+      (compile
+         (Printf.sprintf
+            {| [Insert relation: "Person" tuple: {name: "Rui" age: 70} before: %S after: S1] |}
+            root))
+  in
+  let next =
+    match solutions with
+    | [ solution ] -> (
+        match binding solution "S1" with
+        | Sol.Pattern.String digest -> Sol.Term.string digest
+        | _ -> Alcotest.fail "S1 did not resolve to a state")
+    | _ -> Alcotest.fail "expected one solution"
+  in
+  let expect = Sol.Term.string root in
+  (match Sol.Branch.commit world ~branch:"main" ~expect ~next with
+  | Ok () -> ()
+  | Error `Conflict -> Alcotest.fail "first commit must succeed");
+  (* A second commit from the same stale expectation conflicts:
+     the kernel arbitrates only the tip. *)
+  match Sol.Branch.commit world ~branch:"main" ~expect ~next with
+  | Error `Conflict -> ()
+  | Ok () -> Alcotest.fail "stale expectation must conflict"
+
+let test_integrity_at_transition () =
+  let world = world () in
+  let source =
+    Printf.sprintf
+      {| [Insert relation: "Person" tuple: {name: "Ghost" age: "old"} before: %S after: S1] |}
+      (tip_digest world)
+  in
+  Alcotest.(check int) "an ill-typed tuple is no transition" 0
+    (List.length (solve world (compile source)))
+
+let test_linearity_rejects_forks () =
+  let world = world () in
+  ignore world;
+  let source =
+    {| [Insert relation: "Person" tuple: {name: "A" age: 1} before: S0 after: S1] :and
+       [Insert relation: "Person" tuple: {name: "B" age: 2} before: S0 after: S2] |}
+  in
+  match Sol.Branch.linear (compile source) with
+  | Error _ -> ()
+  | Ok () -> Alcotest.fail "a fork inside one expression must be rejected"
+
+let test_reads_default_to_tip () =
+  let world = world () in
+  Alcotest.(check int) "the root tip has nobody" 0
+    (List.length (solve world (compile {| [Person name: N age: A] |})))
+
+let () =
+  Alcotest.run "sol-branch"
+    [
+      ( "states and transitions",
+        [
+          Alcotest.test_case "transition chain" `Quick test_transition_chain;
+          Alcotest.test_case "tip unmoved until commit" `Quick
+            test_tip_unmoved_until_commit;
+          Alcotest.test_case "commit and conflict" `Quick test_commit_and_conflict;
+          Alcotest.test_case "integrity at the transition" `Quick
+            test_integrity_at_transition;
+          Alcotest.test_case "linearity rejects forks" `Quick
+            test_linearity_rejects_forks;
+          Alcotest.test_case "reads default to tip" `Quick
+            test_reads_default_to_tip;
+        ] );
+    ]
diff --git a/test/test_embedding.ml b/test/test_embedding.ml
index a2eab95..bb7aee8 100644
--- a/test/test_embedding.ml
+++ b/test/test_embedding.ml
@@ -32,8 +32,10 @@ module Kernel_world = struct
           ];
       }
 
-  let find () name =
+  let find () ?at:_ name =
     match name with "Sensor" -> Some sensors | _ -> None
+
+  let transition () _ _ = None
 end
 
 module Kernel_vm = Sol.Vm.Make (Kernel_world)