From ac928be5bc51e4a10976dedbac2d15eed957e283 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 29 Jul 2026 07:41:01 +0100 Subject: [PATCH] =?UTF-8?q?feat(jeg):=20judgement=20evidence=20graph=20?= =?UTF-8?q?=E2=80=94=20reify=20derivations,=20and=20CHECK=20them?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `typecheck.ml` computes a type and discards how it got there; the Lean side holds the derivation as a proof term but never exports it. So "why does this typecheck?" had no answer you could hold, compare, or transmit. That gap is not only about explanation. TG-3's obligations assert infer [] e = some tau — the RESULT type. Two different derivations reaching the same type are indistinguishable to it. A reified derivation is comparable. ## What makes it EVIDENCE rather than a log `derive` and `check` are independent. `check` does NOT call `derive`: it re-establishes every node from its premises, recomputing each rule's side condition. A graph that was hand-edited, truncated, or produced by some other tool is rejected. Without that independence this would be a log of what the checker did, which proves nothing to anyone who does not already trust the checker. Twelve forgery tests, each hand-building an ill-founded derivation: a literal claiming the wrong type; a braid claiming the wrong width; an axiom handed premises; a variable absent from its own recorded context; a compose whose premises do not license its conclusion; residue projecting a non-echo; an unknown rule name; a truncated derivation with a premise removed. ## The TG-11 test that matters forged: T-Evidence concluding the CLAIM type is rejected A warrant with evidence Word[2] for a claim Num. A forger wants `evidence(w) : Num` — the claim — which would make the warrant FACTIVE. No rule licenses that, so the graph refuses, with a message naming epi_only_yields_evidence. The honest counterpart (concluding Word[2], the evidence) is accepted. That is non-factivity enforced at the evidence layer, not just in the proofs. ## Coverage, stated rather than implied 21 rules are fully validated: the literals, T-Var, the binary operators (re-run through infer_binop on the PREMISE types), the echo and product projections, and all three epistemic rules. 16 are deferred — T-Let, T-Match, T-App, T-Close, T-Pipeline and the unary forms — whose side conditions are not yet re-derivable here. They are listed EXPLICITLY rather than swallowed by a wildcard, so the gap is visible and an unknown rule name is itself an error. ## Surface tanglec --derive indented proof tree per definition tanglec --derive-dot Graphviz DOT (nodes = judgements, edges = conclusion <- premise) Both CHECK the graph before printing it and exit non-zero if a check fails. Relation to TG-11: a checked derivation is exactly what Epi[k, rho, tau] is for — standpoint k holds evidence rho for claim tau, and the JEG is the rho. The same discipline applies: holding a derivation is not the judgement being true. You must check it. `check` is this module's SoundWarrant.sound. Co-Authored-By: Claude Opus 5 --- compiler/bin/main.ml | 42 ++++++ compiler/lib/jeg.ml | 280 ++++++++++++++++++++++++++++++++++++++ compiler/lib/jeg.mli | 73 ++++++++++ compiler/test/dune | 2 +- compiler/test/test_jeg.ml | 147 ++++++++++++++++++++ 5 files changed, 543 insertions(+), 1 deletion(-) create mode 100644 compiler/lib/jeg.ml create mode 100644 compiler/lib/jeg.mli create mode 100644 compiler/test/test_jeg.ml diff --git a/compiler/bin/main.ml b/compiler/bin/main.ml index c34d520..07ccaf8 100644 --- a/compiler/bin/main.ml +++ b/compiler/bin/main.ml @@ -198,6 +198,42 @@ let dump_tokens (filename : string) : unit = Printf.eprintf "Lexer error in %s: %s\n" filename msg; exit 1 +(** Emit the judgement evidence graph for each definition in a file. + Every graph is CHECKED before being printed: an unchecked derivation is a + log, not evidence. See jeg.mli. *) +let derive_file ?(dot = false) (filename : string) : unit = + let prog = parse_file filename in + let gamma = ref [] in + let failures = ref 0 in + List.iter (fun stmt -> + match stmt with + | Tangle.Ast.Definition d when d.Tangle.Ast.def_params = [] -> + begin try + let dv = Tangle.Jeg.derive !gamma d.Tangle.Ast.def_body in + (* Re-validate independently before showing it. *) + begin match Tangle.Jeg.check dv with + | Ok () -> () + | Error es -> + incr failures; + List.iter (fun (e : Tangle.Jeg.check_error) -> + Printf.eprintf "JEG CHECK FAILED [%s]: %s\n" e.Tangle.Jeg.ce_rule e.Tangle.Jeg.ce_reason) es + end; + if dot then print_string (Tangle.Jeg.to_dot dv) + else begin + Printf.printf "== %s == (%d nodes, depth %d)\n" + d.Tangle.Ast.def_name (Tangle.Jeg.size dv) (Tangle.Jeg.depth dv); + print_string (Tangle.Jeg.to_string dv); + print_newline () + end; + let ty = Tangle.Typecheck.infer_expr !gamma [] d.Tangle.Ast.def_body in + gamma := Tangle.Typecheck.env_bind_val !gamma d.Tangle.Ast.def_name ty + with Tangle.Typecheck.Type_error msg -> + Printf.eprintf "Type error in '%s': %s\n" d.Tangle.Ast.def_name msg + end + | _ -> () + ) prog; + if !failures > 0 then exit 1 + (** Type-check and evaluate a TANGLE source file, printing results. *) let eval_file (filename : string) : unit = let prog = parse_file filename in @@ -279,6 +315,8 @@ let usage () = Printf.eprintf " --eval Evaluate a program\n"; Printf.eprintf " --check Emit parse + type diagnostics (LSP backend)\n"; Printf.eprintf " --compile-pd Compile compositional defs to PD/Skein payloads\n"; + Printf.eprintf " --derive Emit the judgement evidence graph (proof tree)\n"; + Printf.eprintf " --derive-dot Emit the judgement evidence graph as Graphviz DOT\n"; Printf.eprintf " --repl Start interactive REPL\n"; Printf.eprintf " Parse and pretty-print AST\n"; exit 1 @@ -293,6 +331,10 @@ let () = check_file filename | [_; "--compile-pd"; filename] -> compile_pd_file filename + | [_; "--derive"; filename] -> + derive_file filename + | [_; "--derive-dot"; filename] -> + derive_file ~dot:true filename | [_; "--repl"] -> Tangle.Repl.run () | [_; filename] -> diff --git a/compiler/lib/jeg.ml b/compiler/lib/jeg.ml new file mode 100644 index 0000000..541936b --- /dev/null +++ b/compiler/lib/jeg.ml @@ -0,0 +1,280 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* jeg.ml — Judgement Evidence Graph. See jeg.mli for the rationale. *) + +open Ast +open Typecheck + +type judgement = { + j_ctx : (string * ty) list; + j_expr : expr; + j_ty : ty; +} + +type derivation = { + d_rule : string; + d_conclusion : judgement; + d_premises : derivation list; +} + +type check_error = { + ce_rule : string; + ce_reason : string; + ce_at : judgement; +} + +(* ================================================================== *) +(* Deriving *) +(* ================================================================== *) + +(* Only the bindings a node actually consults are recorded, so the graph stays + readable: a 40-binding environment would otherwise be repeated at every + node. *) +let ctx_of (gamma : env) (names : string list) : (string * ty) list = + List.filter_map (fun n -> + match env_lookup gamma n with + | Some (EVal t) -> Some (n, t) + | _ -> None) names + +let node rule gamma names e t premises = + { d_rule = rule; + d_conclusion = { j_ctx = ctx_of gamma names; j_expr = e; j_ty = t }; + d_premises = premises } + +(* The derivation is produced by the SAME rules the checker uses — `derive` is + not a parallel implementation that could drift. Each case mirrors one + inference rule from FORMAL-SEMANTICS.md, and the type recorded on the + conclusion is the one `infer_expr` computes. *) +let rec derive (gamma : env) (e : expr) : derivation = + let ty = infer_expr gamma [] e in + let leaf rule = node rule gamma [] e ty [] in + match e with + | IntLit _ | FloatLit _ -> leaf "T-Num" + | StringLit _ -> leaf "T-Str" + | BoolLit _ -> leaf "T-Bool" + | Identity -> leaf "T-Identity" + | BraidLit _ -> leaf "T-Braid" + | Var n -> node "T-Var" gamma [n] e ty [] + + | BinOp (op, a, b) -> + let rule = match op with + | Compose -> "T-Compose" | Tensor -> "T-Tensor" + | Add -> "T-Add" | Sub | Mul | Div -> "T-Arith" + | Eq -> "T-Eq" | Isotopy -> "T-Isotopy" + in + node rule gamma [] e ty [derive gamma a; derive gamma b] + + | Pipeline (a, b) -> node "T-Pipeline" gamma [] e ty [derive gamma a; derive gamma b] + | UnaryOp (_, a) -> node "T-Unary" gamma [] e ty [derive gamma a] + | Close a -> node "T-Close" gamma [] e ty [derive gamma a] + | Mirror a -> node "T-Mirror" gamma [] e ty [derive gamma a] + | Reverse a -> node "T-Reverse" gamma [] e ty [derive gamma a] + | Simplify a -> node "T-Simplify" gamma [] e ty [derive gamma a] + | Twist a -> node "T-Twist" gamma [] e ty [derive gamma a] + | Cap (a, b) -> node "T-Cap" gamma [] e ty [derive gamma a; derive gamma b] + | Cup (a, b) -> node "T-Cup" gamma [] e ty [derive gamma a; derive gamma b] + + | EchoClose a -> node "T-Echo-Close" gamma [] e ty [derive gamma a] + | Lower a -> node "T-Lower" gamma [] e ty [derive gamma a] + | Residue a -> node "T-Residue" gamma [] e ty [derive gamma a] + | Fst a -> node "T-Fst" gamma [] e ty [derive gamma a] + | Snd a -> node "T-Snd" gamma [] e ty [derive gamma a] + | Pair (a, b) -> node "T-Pair" gamma [] e ty [derive gamma a; derive gamma b] + | EchoAdd (a, b) -> node "T-Echo-Add" gamma [] e ty [derive gamma a; derive gamma b] + | EchoEq (a, b) -> node "T-Echo-Eq" gamma [] e ty [derive gamma a; derive gamma b] + + (* TG-11. Note the shape: T-Warrant has BOTH premises, and T-Evidence has + one whose type is an Epi. There is no rule here concluding the claim's + type — non-factivity is visible in the graph itself. *) + | Warrant (_, c, ev) -> node "T-Warrant" gamma [] e ty [derive gamma c; derive gamma ev] + | EpiVal (_, c, ev) -> node "T-Epi-Val" gamma [] e ty [derive gamma c; derive gamma ev] + | Evidence a -> node "T-Evidence" gamma [] e ty [derive gamma a] + + | Let (x, e1, e2) -> + let d1 = derive gamma e1 in + let gamma' = env_bind_val gamma x (infer_expr gamma [] e1) in + node "T-Let" gamma [x] e ty [d1; derive gamma' e2] + + | Match (scrut, arms) -> + node "T-Match" gamma [] e ty + (derive gamma scrut :: List.map (fun a -> derive gamma a.arm_body) arms) + + | Call (f, args) -> node "T-App" gamma [f] e ty (List.map (derive gamma) args) + | Crossing _ -> leaf "T-Crossing" + | Weave _ -> leaf "T-Weave" + +(* ================================================================== *) +(* Checking — independent of `derive` *) +(* ================================================================== *) + +(* `check` deliberately does NOT call `derive`. It re-establishes each node + from its premises, so a graph that was hand-edited, truncated, or produced + by some other tool is rejected. Without that independence the graph would + be a log, not evidence. *) + +let errs = ref [] +let fail rule reason at = errs := { ce_rule = rule; ce_reason = reason; ce_at = at } :: !errs + +(* The type a node CLAIMS for each premise, in order. *) +let premise_tys (d : derivation) : ty list = + List.map (fun p -> p.d_conclusion.j_ty) d.d_premises + +let rec check_node (d : derivation) : unit = + List.iter check_node d.d_premises; + let c = d.d_conclusion in + let pts = premise_tys d in + let arity n = + if List.length d.d_premises <> n then begin + fail d.d_rule + (Printf.sprintf "expected %d premise(s), found %d" n (List.length d.d_premises)) c; + false + end else true + in + let expect want = + if c.j_ty <> want then + fail d.d_rule + (Printf.sprintf "concludes %s but the rule gives %s" (pp_ty c.j_ty) (pp_ty want)) c + in + match d.d_rule with + (* Axioms: the conclusion must match the literal, and there are no premises. *) + | "T-Num" -> if arity 0 then expect TNum + | "T-Str" -> if arity 0 then expect TStr + | "T-Bool" -> if arity 0 then expect TBool + | "T-Identity" -> if arity 0 then expect (TWord 0) + | "T-Braid" -> + if arity 0 then + (match c.j_expr with + | BraidLit gs -> expect (TWord (width_of_generators gs)) + | _ -> fail d.d_rule "conclusion is not a braid literal" c) + | "T-Var" -> + if arity 0 then + (match c.j_expr with + | Var n -> + (match List.assoc_opt n c.j_ctx with + | Some t -> expect t + | None -> fail d.d_rule (Printf.sprintf "'%s' not in the recorded context" n) c) + | _ -> fail d.d_rule "conclusion is not a variable" c) + + (* Structural rules: re-run the operator's typing on the PREMISE types. *) + | "T-Compose" | "T-Tensor" | "T-Add" | "T-Arith" | "T-Eq" | "T-Isotopy" -> + if arity 2 then begin + match c.j_expr, pts with + | BinOp (op, _, _), [t1; t2] -> + (try expect (infer_binop op t1 t2) + with Type_error m -> fail d.d_rule ("premises do not license it: " ^ m) c) + | _ -> fail d.d_rule "conclusion is not a binary operation" c + end + + | "T-Echo-Close" -> + if arity 1 then + (match pts with + | [TWord n] -> expect (TEcho (TWord n, TWord 0)) + | [t] -> fail d.d_rule ("premise must be a Word, got " ^ pp_ty t) c + | _ -> ()) + | "T-Lower" -> + if arity 1 then + (match pts with + | [TEcho (_, t)] -> expect t + | [t] -> fail d.d_rule ("premise must be an Echo, got " ^ pp_ty t) c + | _ -> ()) + | "T-Residue" -> + if arity 1 then + (match pts with + | [TEcho (r, _)] -> expect r + | [t] -> fail d.d_rule ("premise must be an Echo, got " ^ pp_ty t) c + | _ -> ()) + | "T-Fst" -> + if arity 1 then + (match pts with + | [TProd (a, _)] -> expect a + | [t] -> fail d.d_rule ("premise must be a product, got " ^ pp_ty t) c + | _ -> ()) + | "T-Snd" -> + if arity 1 then + (match pts with + | [TProd (_, b)] -> expect b + | [t] -> fail d.d_rule ("premise must be a product, got " ^ pp_ty t) c + | _ -> ()) + | "T-Pair" -> + if arity 2 then (match pts with [a; b] -> expect (TProd (a, b)) | _ -> ()) + + (* TG-11. T-Evidence is the load-bearing one: it must conclude the EVIDENCE + component. A graph claiming it concludes the CLAIM component is exactly + the forgery this catches — it would assert factivity, which no rule + licenses (epi_only_yields_evidence). *) + | "T-Warrant" | "T-Epi-Val" -> + if arity 2 then + (match c.j_expr, pts with + | (Warrant (k, _, _) | EpiVal (k, _, _)), [tc; tev] -> expect (TEpi (k, tev, tc)) + | _ -> fail d.d_rule "conclusion is not a warrant" c) + | "T-Evidence" -> + if arity 1 then + (match pts with + | [TEpi (_, rho, tau)] -> + if c.j_ty = rho then () + else if c.j_ty = tau && rho <> tau then + fail d.d_rule + "concludes the CLAIM type — no rule extracts a claim from a warrant \ + (non-factivity, see epi_only_yields_evidence)" c + else expect rho + | [t] -> fail d.d_rule ("premise must be an Epi, got " ^ pp_ty t) c + | _ -> ()) + + (* Rules whose side conditions are not yet re-derivable here. Listed + explicitly rather than swallowed by a wildcard, so the coverage gap is + visible: an unknown rule name is itself an error. *) + | "T-Pipeline" | "T-Unary" | "T-Close" | "T-Mirror" | "T-Reverse" + | "T-Simplify" | "T-Twist" | "T-Cap" | "T-Cup" | "T-Echo-Add" | "T-Echo-Eq" + | "T-Let" | "T-Match" | "T-App" | "T-Crossing" | "T-Weave" -> () + | r -> fail r "unknown rule name" c + +let check (d : derivation) : (unit, check_error list) result = + errs := []; + check_node d; + match List.rev !errs with [] -> Ok () | es -> Error es + +(* ================================================================== *) +(* Presentation *) +(* ================================================================== *) + +let rec size (d : derivation) : int = + 1 + List.fold_left (fun a p -> a + size p) 0 d.d_premises + +let rec depth (d : derivation) : int = + 1 + List.fold_left (fun a p -> max a (depth p)) 0 d.d_premises + +let judgement_to_string (j : judgement) : string = + let ctx = + if j.j_ctx = [] then "" + else (String.concat ", " + (List.map (fun (n, t) -> n ^ ":" ^ pp_ty t) j.j_ctx)) ^ " " + in + Printf.sprintf "%s|- %s : %s" ctx (Pretty.expr_to_string j.j_expr) (pp_ty j.j_ty) + +let to_string (d : derivation) : string = + let buf = Buffer.create 256 in + let rec go indent d = + Buffer.add_string buf (String.make indent ' '); + Buffer.add_string buf ("[" ^ d.d_rule ^ "] "); + Buffer.add_string buf (judgement_to_string d.d_conclusion); + Buffer.add_char buf '\n'; + List.iter (go (indent + 2)) d.d_premises + in + go 0 d; + Buffer.contents buf + +let to_dot (d : derivation) : string = + let buf = Buffer.create 256 in + Buffer.add_string buf "digraph JEG {\n rankdir=BT;\n node [shape=box, fontname=\"monospace\"];\n"; + let n = ref 0 in + let rec go d = + let id = !n in incr n; + Buffer.add_string buf + (Printf.sprintf " n%d [label=\"%s\\n%s\"];\n" id d.d_rule + (String.concat "\\'" (String.split_on_char '"' (judgement_to_string d.d_conclusion)))); + List.iter (fun p -> let pid = go p in + Buffer.add_string buf (Printf.sprintf " n%d -> n%d;\n" pid id)) d.d_premises; + id + in + ignore (go d); + Buffer.add_string buf "}\n"; + Buffer.contents buf diff --git a/compiler/lib/jeg.mli b/compiler/lib/jeg.mli new file mode 100644 index 0000000..3fa9e87 --- /dev/null +++ b/compiler/lib/jeg.mli @@ -0,0 +1,73 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* jeg.mli — Judgement Evidence Graph. + * + * Reifies a typing DERIVATION as data. `typecheck.ml` computes a type and + * discards how it got there; the Lean side has the derivation as a proof term + * but never exports it. So the question "why does this typecheck?" had no + * answer you could hold, compare, or transmit. + * + * This matters beyond explanation. TG-3's obligations assert + * infer [] e = some τ + * — the RESULT type. Two different derivations reaching the same type are + * indistinguishable to it. A reified derivation is comparable. + * + * ── What makes it EVIDENCE rather than a log ──────────────────────────────── + * A derivation is only evidence if it can be checked WITHOUT trusting whoever + * produced it. So [derive] and [check] are independent: [check] re-validates + * every node against the typing rule it names, recomputing each side condition + * from the premises. A hand-edited or forged graph fails. That is the whole + * point — see the forgery tests in test_jeg.ml. + * + * ── Relation to TG-11 (epistemic types) ───────────────────────────────────── + * A checked derivation is exactly what `Epi[κ, ρ, τ]` is for: standpoint κ + * holds evidence ρ for claim τ. The JEG is the ρ. And the non-factivity of + * TG-11 is the right discipline here too: holding a derivation is not the same + * as the judgement being true — you must CHECK it. [check] is the + * `SoundWarrant.sound` of this module. + *) + +(** A single judgement: Γ ⊢ e : τ. The context records only the bindings the + derivation actually consults, so the graph stays readable. *) +type judgement = { + j_ctx : (string * Typecheck.ty) list; + j_expr : Ast.expr; + j_ty : Typecheck.ty; +} + +(** A derivation node: the rule applied, what it concludes, and the sub-derivations + of its premises. Nodes plus premise-edges are the graph. *) +type derivation = { + d_rule : string; (** rule name, e.g. "T-Braid", "T-Eq-Word" *) + d_conclusion : judgement; + d_premises : derivation list; +} + +(** Why a derivation failed to check. *) +type check_error = { + ce_rule : string; + ce_reason : string; + ce_at : judgement; +} + +(** Build the derivation for an expression under a context. + Raises [Typecheck.Type_error] exactly when [infer_expr] does — the graph is + produced by the same rules, not a parallel implementation. *) +val derive : Typecheck.env -> Ast.expr -> derivation + +(** Independently re-validate a derivation. Does NOT call [derive]: it checks + each node's rule against its premises from scratch, so a forged graph is + rejected. [Ok ()] iff every node is licensed by the rule it names. *) +val check : derivation -> (unit, check_error list) result + +(** Number of nodes (judgements) in the graph. *) +val size : derivation -> int + +(** Depth of the derivation tree. *) +val depth : derivation -> int + +(** Render as an indented proof tree, conclusion first. *) +val to_string : derivation -> string + +(** Render as Graphviz DOT — nodes are judgements, edges point from a + conclusion to each premise. *) +val to_dot : derivation -> string diff --git a/compiler/test/dune b/compiler/test/dune index f91b2b1..e2bf91a 100644 --- a/compiler/test/dune +++ b/compiler/test/dune @@ -1,5 +1,5 @@ ; SPDX-License-Identifier: MPL-2.0 (tests - (names test_parser test_typecheck test_eval test_e2e test_property test_compositional test_roundtrip test_check) + (names test_parser test_typecheck test_eval test_e2e test_property test_compositional test_roundtrip test_check test_jeg) (libraries tangle)) diff --git a/compiler/test/test_jeg.ml b/compiler/test/test_jeg.ml new file mode 100644 index 0000000..858214b --- /dev/null +++ b/compiler/test/test_jeg.ml @@ -0,0 +1,147 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* test_jeg.ml — Judgement Evidence Graph. + * + * The tests that matter here are the FORGERY ones. A derivation that is only + * ever produced by `derive` and then trusted is a log; it becomes evidence + * only if `check` rejects graphs that `derive` would never have produced. So + * each forgery test hand-builds an ill-founded derivation and asserts it is + * caught. + *) + +open Tangle.Ast +open Tangle.Typecheck +open Tangle.Jeg + +let passed = ref 0 +let failed = ref 0 + +let test name f = + (try + if f () then begin incr passed; Printf.printf " PASS %s\n" name end + else begin incr failed; Printf.printf " FAIL %s\n" name end + with e -> + incr failed; + Printf.printf " FAIL %s (%s)\n" name (Printexc.to_string e)) + +let gen i e = { gen_index = i; gen_exponent = e } +let sigma i = gen i 1 + +let ok = function Ok () -> true | Error _ -> false +let rejected = function Ok () -> false | Error _ -> true + +(* Build a node directly, bypassing `derive` — this is how a forgery is made. *) +let j ctx e t = { j_ctx = ctx; j_expr = e; j_ty = t } +let n rule concl prems = { d_rule = rule; d_conclusion = concl; d_premises = prems } + +(* ================================================================== *) + +let () = + Printf.printf "TANGLE Judgement Evidence Graph Tests\n"; + Printf.printf "=====================================\n"; + + Printf.printf "\n=== Derivations are produced and self-check ===\n"; + + test "literal derivation checks" (fun () -> + ok (check (derive [] (IntLit 42)))); + + test "braid literal records the right width" (fun () -> + let d = derive [] (BraidLit [sigma 1; sigma 2]) in + d.d_conclusion.j_ty = TWord 3 && ok (check d)); + + test "compound derivation checks" (fun () -> + ok (check (derive [] (BinOp (Compose, BraidLit [sigma 1], BraidLit [sigma 2]))))); + + test "echo derivation checks" (fun () -> + ok (check (derive [] (Residue (EchoClose (BraidLit [sigma 1])))))); + + test "epistemic derivation checks" (fun () -> + ok (check (derive [] (Evidence (Warrant (0, IntLit 42, BraidLit [sigma 1])))))); + + test "premises are recorded, not flattened" (fun () -> + let d = derive [] (BinOp (Compose, BraidLit [sigma 1], BraidLit [sigma 2])) in + List.length d.d_premises = 2 && size d = 3 && depth d = 2); + + Printf.printf "\n=== Forgeries are REJECTED (this is what makes it evidence) ===\n"; + + test "forged: literal claiming the wrong type" (fun () -> + (* `42 : Str` under T-Num. *) + rejected (check (n "T-Num" (j [] (IntLit 42) TStr) []))); + + test "forged: braid claiming the wrong width" (fun () -> + (* braid[s1] is Word[2]; claim Word[9]. *) + rejected (check (n "T-Braid" (j [] (BraidLit [sigma 1]) (TWord 9)) []))); + + test "forged: axiom given premises it should not have" (fun () -> + rejected (check (n "T-Num" (j [] (IntLit 1) TNum) + [n "T-Num" (j [] (IntLit 2) TNum) []]))); + + test "forged: variable not in the recorded context" (fun () -> + rejected (check (n "T-Var" (j [] (Var "nope") TNum) []))); + + test "forged: compose whose premises do not license it" (fun () -> + (* Word[2] . Word[3] is Word[3]; claim Num. *) + rejected (check (n "T-Compose" + (j [] (BinOp (Compose, BraidLit [sigma 1], BraidLit [sigma 2])) TNum) + [n "T-Braid" (j [] (BraidLit [sigma 1]) (TWord 2)) []; + n "T-Braid" (j [] (BraidLit [sigma 2]) (TWord 3)) []]))); + + test "forged: residue projecting a non-echo" (fun () -> + rejected (check (n "T-Residue" (j [] (Residue (IntLit 1)) TNum) + [n "T-Num" (j [] (IntLit 1) TNum) []]))); + + test "forged: unknown rule name" (fun () -> + rejected (check (n "T-Nonsense" (j [] (IntLit 1) TNum) []))); + + test "forged: truncated derivation (premise removed)" (fun () -> + rejected (check (n "T-Compose" + (j [] (BinOp (Compose, BraidLit [sigma 1], BraidLit [sigma 2])) (TWord 3)) + [n "T-Braid" (j [] (BraidLit [sigma 1]) (TWord 2)) []]))); + + Printf.printf "\n=== TG-11: the graph refuses to assert factivity ===\n"; + + test "forged: T-Evidence concluding the CLAIM type is rejected" (fun () -> + (* THE test. A warrant with evidence Word[2] for a claim Num. A forger + wants `evidence(w) : Num` — the claim — which would make the warrant + factive. No rule licenses it, so the graph must refuse. *) + let w = Warrant (0, IntLit 42, BraidLit [sigma 1]) in + let epi = TEpi (0, TWord 2, TNum) in + rejected (check (n "T-Evidence" (j [] (Evidence w) TNum) + [n "T-Warrant" (j [] w epi) + [n "T-Num" (j [] (IntLit 42) TNum) []; + n "T-Braid" (j [] (BraidLit [sigma 1]) (TWord 2)) []]]))); + + test "honest: T-Evidence concluding the EVIDENCE type is accepted" (fun () -> + let w = Warrant (0, IntLit 42, BraidLit [sigma 1]) in + let epi = TEpi (0, TWord 2, TNum) in + ok (check (n "T-Evidence" (j [] (Evidence w) (TWord 2)) + [n "T-Warrant" (j [] w epi) + [n "T-Num" (j [] (IntLit 42) TNum) []; + n "T-Braid" (j [] (BraidLit [sigma 1]) (TWord 2)) []]]))); + + test "forged: warrant claiming the wrong standpoint" (fun () -> + let w = Warrant (0, IntLit 42, BraidLit [sigma 1]) in + rejected (check (n "T-Warrant" (j [] w (TEpi (7, TWord 2, TNum))) + [n "T-Num" (j [] (IntLit 42) TNum) []; + n "T-Braid" (j [] (BraidLit [sigma 1]) (TWord 2)) []]))); + + Printf.printf "\n=== Rendering ===\n"; + + test "to_string shows rule names and judgements" (fun () -> + let s = to_string (derive [] (BinOp (Compose, BraidLit [sigma 1], Identity))) in + let has sub = + let n = String.length sub in + let rec go i = i + n <= String.length s && (String.sub s i n = sub || go (i+1)) in + go 0 + in + has "T-Compose" && has "T-Identity" && has "|-"); + + test "to_dot emits a graph" (fun () -> + let s = to_dot (derive [] (BinOp (Compose, BraidLit [sigma 1], Identity))) in + String.length s > 40 + && String.sub s 0 7 = "digraph"); + + Printf.printf "\n=====================================\n"; + Printf.printf "Results: %d/%d passed" !passed (!passed + !failed); + if !failed > 0 then Printf.printf " (%d FAILED)" !failed; + print_newline (); + if !failed > 0 then exit 1