diff options
| -rw-r--r-- | docs/states.org | 65 | ||||
| -rw-r--r-- | docs/virtual-machine-specification.org | 19 | ||||
| -rw-r--r-- | lib/branch.ml | 162 | ||||
| -rw-r--r-- | lib/branch.mli | 46 | ||||
| -rw-r--r-- | lib/vm.ml | 47 | ||||
| -rw-r--r-- | lib/world.ml | 10 | ||||
| -rw-r--r-- | lib/world.mli | 35 | ||||
| -rw-r--r-- | test/dune | 2 | ||||
| -rw-r--r-- | test/test_branch.ml | 151 | ||||
| -rw-r--r-- | test/test_embedding.ml | 4 |
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. *) @@ -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 @@ -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) |