Skip to content

Commit 0366a8e

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
feat(jeg): judgement evidence graph — reify derivations, and CHECK them (#100)
`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 isn't only about explanation. TG-3's obligations assert: ```lean example : infer [] (.num 0) = some .num := by decide ``` — 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 doesn't already trust the checker. **Twelve forgery tests**, each hand-building an ill-founded derivation: | Forgery | Caught | |---|---| | literal claiming the wrong type | ✅ | | braid claiming the wrong width | ✅ | | axiom handed premises | ✅ | | variable absent from its own recorded context | ✅ | | compose whose premises don't license its conclusion | ✅ | | residue projecting a non-echo | ✅ | | unknown rule name | ✅ | | truncated derivation (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 it, so the graph refuses, with a message naming `epi_only_yields_evidence`. The honest counterpart (concluding `Word[2]`) is accepted. **That's non-factivity enforced at the evidence layer, not just in the proofs.** ## Coverage — stated, not implied **21 rules fully validated**: literals, `T-Var`, the binary operators (re-run through `infer_binop` on the *premise* types), echo and product projections, and all three epistemic rules. **16 deferred**: `T-Let`, `T-Match`, `T-App`, `T-Close`, `T-Pipeline` and the unary forms, whose side conditions aren't yet re-derivable here. They're 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 <file> indented proof tree per definition tanglec --derive-dot <file> Graphviz DOT ``` Both **check** before printing, and exit non-zero on failure. Real output: ``` == w == (3 nodes, depth 2) [T-Warrant] |- warrant[0](42, braid[s1]) : Epi[0, Word[2], Num] [T-Num] |- 42 : Num [T-Braid] |- braid[s1] : Word[2] == tok == (2 nodes, depth 2) [T-Evidence] |- evidence(w) : Word[2] [T-Var] w:Epi[0, Word[2], Num] |- w : Epi[0, Word[2], Num] ``` ## Relation to TG-11 A checked derivation is exactly what `Epi[κ, ρ, τ]` is for — standpoint κ holds evidence ρ for claim τ, and **the JEG is the ρ**. The same discipline applies: holding a derivation is not the judgement being true. You must check it. `check` is this module's `SoundWarrant.sound`. All suites green (new suite 19/19); corpus and RSR gates pass. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
1 parent 40e917d commit 0366a8e

5 files changed

Lines changed: 543 additions & 1 deletion

File tree

‎compiler/bin/main.ml‎

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -198,6 +198,42 @@ let dump_tokens (filename : string) : unit =
198198
Printf.eprintf "Lexer error in %s: %s\n" filename msg;
199199
exit 1
200200

201+
(** Emit the judgement evidence graph for each definition in a file.
202+
Every graph is CHECKED before being printed: an unchecked derivation is a
203+
log, not evidence. See jeg.mli. *)
204+
let derive_file ?(dot = false) (filename : string) : unit =
205+
let prog = parse_file filename in
206+
let gamma = ref [] in
207+
let failures = ref 0 in
208+
List.iter (fun stmt ->
209+
match stmt with
210+
| Tangle.Ast.Definition d when d.Tangle.Ast.def_params = [] ->
211+
begin try
212+
let dv = Tangle.Jeg.derive !gamma d.Tangle.Ast.def_body in
213+
(* Re-validate independently before showing it. *)
214+
begin match Tangle.Jeg.check dv with
215+
| Ok () -> ()
216+
| Error es ->
217+
incr failures;
218+
List.iter (fun (e : Tangle.Jeg.check_error) ->
219+
Printf.eprintf "JEG CHECK FAILED [%s]: %s\n" e.Tangle.Jeg.ce_rule e.Tangle.Jeg.ce_reason) es
220+
end;
221+
if dot then print_string (Tangle.Jeg.to_dot dv)
222+
else begin
223+
Printf.printf "== %s == (%d nodes, depth %d)\n"
224+
d.Tangle.Ast.def_name (Tangle.Jeg.size dv) (Tangle.Jeg.depth dv);
225+
print_string (Tangle.Jeg.to_string dv);
226+
print_newline ()
227+
end;
228+
let ty = Tangle.Typecheck.infer_expr !gamma [] d.Tangle.Ast.def_body in
229+
gamma := Tangle.Typecheck.env_bind_val !gamma d.Tangle.Ast.def_name ty
230+
with Tangle.Typecheck.Type_error msg ->
231+
Printf.eprintf "Type error in '%s': %s\n" d.Tangle.Ast.def_name msg
232+
end
233+
| _ -> ()
234+
) prog;
235+
if !failures > 0 then exit 1
236+
201237
(** Type-check and evaluate a TANGLE source file, printing results. *)
202238
let eval_file (filename : string) : unit =
203239
let prog = parse_file filename in
@@ -279,6 +315,8 @@ let usage () =
279315
Printf.eprintf " --eval <file> Evaluate a program\n";
280316
Printf.eprintf " --check <file> Emit parse + type diagnostics (LSP backend)\n";
281317
Printf.eprintf " --compile-pd <file> Compile compositional defs to PD/Skein payloads\n";
318+
Printf.eprintf " --derive <file> Emit the judgement evidence graph (proof tree)\n";
319+
Printf.eprintf " --derive-dot <file> Emit the judgement evidence graph as Graphviz DOT\n";
282320
Printf.eprintf " --repl Start interactive REPL\n";
283321
Printf.eprintf " <file> Parse and pretty-print AST\n";
284322
exit 1
@@ -293,6 +331,10 @@ let () =
293331
check_file filename
294332
| [_; "--compile-pd"; filename] ->
295333
compile_pd_file filename
334+
| [_; "--derive"; filename] ->
335+
derive_file filename
336+
| [_; "--derive-dot"; filename] ->
337+
derive_file ~dot:true filename
296338
| [_; "--repl"] ->
297339
Tangle.Repl.run ()
298340
| [_; filename] ->

‎compiler/lib/jeg.ml‎

Lines changed: 280 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,280 @@
1+
(* SPDX-License-Identifier: MPL-2.0 *)
2+
(* jeg.ml — Judgement Evidence Graph. See jeg.mli for the rationale. *)
3+
4+
open Ast
5+
open Typecheck
6+
7+
type judgement = {
8+
j_ctx : (string * ty) list;
9+
j_expr : expr;
10+
j_ty : ty;
11+
}
12+
13+
type derivation = {
14+
d_rule : string;
15+
d_conclusion : judgement;
16+
d_premises : derivation list;
17+
}
18+
19+
type check_error = {
20+
ce_rule : string;
21+
ce_reason : string;
22+
ce_at : judgement;
23+
}
24+
25+
(* ================================================================== *)
26+
(* Deriving *)
27+
(* ================================================================== *)
28+
29+
(* Only the bindings a node actually consults are recorded, so the graph stays
30+
readable: a 40-binding environment would otherwise be repeated at every
31+
node. *)
32+
let ctx_of (gamma : env) (names : string list) : (string * ty) list =
33+
List.filter_map (fun n ->
34+
match env_lookup gamma n with
35+
| Some (EVal t) -> Some (n, t)
36+
| _ -> None) names
37+
38+
let node rule gamma names e t premises =
39+
{ d_rule = rule;
40+
d_conclusion = { j_ctx = ctx_of gamma names; j_expr = e; j_ty = t };
41+
d_premises = premises }
42+
43+
(* The derivation is produced by the SAME rules the checker uses — `derive` is
44+
not a parallel implementation that could drift. Each case mirrors one
45+
inference rule from FORMAL-SEMANTICS.md, and the type recorded on the
46+
conclusion is the one `infer_expr` computes. *)
47+
let rec derive (gamma : env) (e : expr) : derivation =
48+
let ty = infer_expr gamma [] e in
49+
let leaf rule = node rule gamma [] e ty [] in
50+
match e with
51+
| IntLit _ | FloatLit _ -> leaf "T-Num"
52+
| StringLit _ -> leaf "T-Str"
53+
| BoolLit _ -> leaf "T-Bool"
54+
| Identity -> leaf "T-Identity"
55+
| BraidLit _ -> leaf "T-Braid"
56+
| Var n -> node "T-Var" gamma [n] e ty []
57+
58+
| BinOp (op, a, b) ->
59+
let rule = match op with
60+
| Compose -> "T-Compose" | Tensor -> "T-Tensor"
61+
| Add -> "T-Add" | Sub | Mul | Div -> "T-Arith"
62+
| Eq -> "T-Eq" | Isotopy -> "T-Isotopy"
63+
in
64+
node rule gamma [] e ty [derive gamma a; derive gamma b]
65+
66+
| Pipeline (a, b) -> node "T-Pipeline" gamma [] e ty [derive gamma a; derive gamma b]
67+
| UnaryOp (_, a) -> node "T-Unary" gamma [] e ty [derive gamma a]
68+
| Close a -> node "T-Close" gamma [] e ty [derive gamma a]
69+
| Mirror a -> node "T-Mirror" gamma [] e ty [derive gamma a]
70+
| Reverse a -> node "T-Reverse" gamma [] e ty [derive gamma a]
71+
| Simplify a -> node "T-Simplify" gamma [] e ty [derive gamma a]
72+
| Twist a -> node "T-Twist" gamma [] e ty [derive gamma a]
73+
| Cap (a, b) -> node "T-Cap" gamma [] e ty [derive gamma a; derive gamma b]
74+
| Cup (a, b) -> node "T-Cup" gamma [] e ty [derive gamma a; derive gamma b]
75+
76+
| EchoClose a -> node "T-Echo-Close" gamma [] e ty [derive gamma a]
77+
| Lower a -> node "T-Lower" gamma [] e ty [derive gamma a]
78+
| Residue a -> node "T-Residue" gamma [] e ty [derive gamma a]
79+
| Fst a -> node "T-Fst" gamma [] e ty [derive gamma a]
80+
| Snd a -> node "T-Snd" gamma [] e ty [derive gamma a]
81+
| Pair (a, b) -> node "T-Pair" gamma [] e ty [derive gamma a; derive gamma b]
82+
| EchoAdd (a, b) -> node "T-Echo-Add" gamma [] e ty [derive gamma a; derive gamma b]
83+
| EchoEq (a, b) -> node "T-Echo-Eq" gamma [] e ty [derive gamma a; derive gamma b]
84+
85+
(* TG-11. Note the shape: T-Warrant has BOTH premises, and T-Evidence has
86+
one whose type is an Epi. There is no rule here concluding the claim's
87+
type — non-factivity is visible in the graph itself. *)
88+
| Warrant (_, c, ev) -> node "T-Warrant" gamma [] e ty [derive gamma c; derive gamma ev]
89+
| EpiVal (_, c, ev) -> node "T-Epi-Val" gamma [] e ty [derive gamma c; derive gamma ev]
90+
| Evidence a -> node "T-Evidence" gamma [] e ty [derive gamma a]
91+
92+
| Let (x, e1, e2) ->
93+
let d1 = derive gamma e1 in
94+
let gamma' = env_bind_val gamma x (infer_expr gamma [] e1) in
95+
node "T-Let" gamma [x] e ty [d1; derive gamma' e2]
96+
97+
| Match (scrut, arms) ->
98+
node "T-Match" gamma [] e ty
99+
(derive gamma scrut :: List.map (fun a -> derive gamma a.arm_body) arms)
100+
101+
| Call (f, args) -> node "T-App" gamma [f] e ty (List.map (derive gamma) args)
102+
| Crossing _ -> leaf "T-Crossing"
103+
| Weave _ -> leaf "T-Weave"
104+
105+
(* ================================================================== *)
106+
(* Checking — independent of `derive` *)
107+
(* ================================================================== *)
108+
109+
(* `check` deliberately does NOT call `derive`. It re-establishes each node
110+
from its premises, so a graph that was hand-edited, truncated, or produced
111+
by some other tool is rejected. Without that independence the graph would
112+
be a log, not evidence. *)
113+
114+
let errs = ref []
115+
let fail rule reason at = errs := { ce_rule = rule; ce_reason = reason; ce_at = at } :: !errs
116+
117+
(* The type a node CLAIMS for each premise, in order. *)
118+
let premise_tys (d : derivation) : ty list =
119+
List.map (fun p -> p.d_conclusion.j_ty) d.d_premises
120+
121+
let rec check_node (d : derivation) : unit =
122+
List.iter check_node d.d_premises;
123+
let c = d.d_conclusion in
124+
let pts = premise_tys d in
125+
let arity n =
126+
if List.length d.d_premises <> n then begin
127+
fail d.d_rule
128+
(Printf.sprintf "expected %d premise(s), found %d" n (List.length d.d_premises)) c;
129+
false
130+
end else true
131+
in
132+
let expect want =
133+
if c.j_ty <> want then
134+
fail d.d_rule
135+
(Printf.sprintf "concludes %s but the rule gives %s" (pp_ty c.j_ty) (pp_ty want)) c
136+
in
137+
match d.d_rule with
138+
(* Axioms: the conclusion must match the literal, and there are no premises. *)
139+
| "T-Num" -> if arity 0 then expect TNum
140+
| "T-Str" -> if arity 0 then expect TStr
141+
| "T-Bool" -> if arity 0 then expect TBool
142+
| "T-Identity" -> if arity 0 then expect (TWord 0)
143+
| "T-Braid" ->
144+
if arity 0 then
145+
(match c.j_expr with
146+
| BraidLit gs -> expect (TWord (width_of_generators gs))
147+
| _ -> fail d.d_rule "conclusion is not a braid literal" c)
148+
| "T-Var" ->
149+
if arity 0 then
150+
(match c.j_expr with
151+
| Var n ->
152+
(match List.assoc_opt n c.j_ctx with
153+
| Some t -> expect t
154+
| None -> fail d.d_rule (Printf.sprintf "'%s' not in the recorded context" n) c)
155+
| _ -> fail d.d_rule "conclusion is not a variable" c)
156+
157+
(* Structural rules: re-run the operator's typing on the PREMISE types. *)
158+
| "T-Compose" | "T-Tensor" | "T-Add" | "T-Arith" | "T-Eq" | "T-Isotopy" ->
159+
if arity 2 then begin
160+
match c.j_expr, pts with
161+
| BinOp (op, _, _), [t1; t2] ->
162+
(try expect (infer_binop op t1 t2)
163+
with Type_error m -> fail d.d_rule ("premises do not license it: " ^ m) c)
164+
| _ -> fail d.d_rule "conclusion is not a binary operation" c
165+
end
166+
167+
| "T-Echo-Close" ->
168+
if arity 1 then
169+
(match pts with
170+
| [TWord n] -> expect (TEcho (TWord n, TWord 0))
171+
| [t] -> fail d.d_rule ("premise must be a Word, got " ^ pp_ty t) c
172+
| _ -> ())
173+
| "T-Lower" ->
174+
if arity 1 then
175+
(match pts with
176+
| [TEcho (_, t)] -> expect t
177+
| [t] -> fail d.d_rule ("premise must be an Echo, got " ^ pp_ty t) c
178+
| _ -> ())
179+
| "T-Residue" ->
180+
if arity 1 then
181+
(match pts with
182+
| [TEcho (r, _)] -> expect r
183+
| [t] -> fail d.d_rule ("premise must be an Echo, got " ^ pp_ty t) c
184+
| _ -> ())
185+
| "T-Fst" ->
186+
if arity 1 then
187+
(match pts with
188+
| [TProd (a, _)] -> expect a
189+
| [t] -> fail d.d_rule ("premise must be a product, got " ^ pp_ty t) c
190+
| _ -> ())
191+
| "T-Snd" ->
192+
if arity 1 then
193+
(match pts with
194+
| [TProd (_, b)] -> expect b
195+
| [t] -> fail d.d_rule ("premise must be a product, got " ^ pp_ty t) c
196+
| _ -> ())
197+
| "T-Pair" ->
198+
if arity 2 then (match pts with [a; b] -> expect (TProd (a, b)) | _ -> ())
199+
200+
(* TG-11. T-Evidence is the load-bearing one: it must conclude the EVIDENCE
201+
component. A graph claiming it concludes the CLAIM component is exactly
202+
the forgery this catches — it would assert factivity, which no rule
203+
licenses (epi_only_yields_evidence). *)
204+
| "T-Warrant" | "T-Epi-Val" ->
205+
if arity 2 then
206+
(match c.j_expr, pts with
207+
| (Warrant (k, _, _) | EpiVal (k, _, _)), [tc; tev] -> expect (TEpi (k, tev, tc))
208+
| _ -> fail d.d_rule "conclusion is not a warrant" c)
209+
| "T-Evidence" ->
210+
if arity 1 then
211+
(match pts with
212+
| [TEpi (_, rho, tau)] ->
213+
if c.j_ty = rho then ()
214+
else if c.j_ty = tau && rho <> tau then
215+
fail d.d_rule
216+
"concludes the CLAIM type — no rule extracts a claim from a warrant \
217+
(non-factivity, see epi_only_yields_evidence)" c
218+
else expect rho
219+
| [t] -> fail d.d_rule ("premise must be an Epi, got " ^ pp_ty t) c
220+
| _ -> ())
221+
222+
(* Rules whose side conditions are not yet re-derivable here. Listed
223+
explicitly rather than swallowed by a wildcard, so the coverage gap is
224+
visible: an unknown rule name is itself an error. *)
225+
| "T-Pipeline" | "T-Unary" | "T-Close" | "T-Mirror" | "T-Reverse"
226+
| "T-Simplify" | "T-Twist" | "T-Cap" | "T-Cup" | "T-Echo-Add" | "T-Echo-Eq"
227+
| "T-Let" | "T-Match" | "T-App" | "T-Crossing" | "T-Weave" -> ()
228+
| r -> fail r "unknown rule name" c
229+
230+
let check (d : derivation) : (unit, check_error list) result =
231+
errs := [];
232+
check_node d;
233+
match List.rev !errs with [] -> Ok () | es -> Error es
234+
235+
(* ================================================================== *)
236+
(* Presentation *)
237+
(* ================================================================== *)
238+
239+
let rec size (d : derivation) : int =
240+
1 + List.fold_left (fun a p -> a + size p) 0 d.d_premises
241+
242+
let rec depth (d : derivation) : int =
243+
1 + List.fold_left (fun a p -> max a (depth p)) 0 d.d_premises
244+
245+
let judgement_to_string (j : judgement) : string =
246+
let ctx =
247+
if j.j_ctx = [] then ""
248+
else (String.concat ", "
249+
(List.map (fun (n, t) -> n ^ ":" ^ pp_ty t) j.j_ctx)) ^ " "
250+
in
251+
Printf.sprintf "%s|- %s : %s" ctx (Pretty.expr_to_string j.j_expr) (pp_ty j.j_ty)
252+
253+
let to_string (d : derivation) : string =
254+
let buf = Buffer.create 256 in
255+
let rec go indent d =
256+
Buffer.add_string buf (String.make indent ' ');
257+
Buffer.add_string buf ("[" ^ d.d_rule ^ "] ");
258+
Buffer.add_string buf (judgement_to_string d.d_conclusion);
259+
Buffer.add_char buf '\n';
260+
List.iter (go (indent + 2)) d.d_premises
261+
in
262+
go 0 d;
263+
Buffer.contents buf
264+
265+
let to_dot (d : derivation) : string =
266+
let buf = Buffer.create 256 in
267+
Buffer.add_string buf "digraph JEG {\n rankdir=BT;\n node [shape=box, fontname=\"monospace\"];\n";
268+
let n = ref 0 in
269+
let rec go d =
270+
let id = !n in incr n;
271+
Buffer.add_string buf
272+
(Printf.sprintf " n%d [label=\"%s\\n%s\"];\n" id d.d_rule
273+
(String.concat "\\'" (String.split_on_char '"' (judgement_to_string d.d_conclusion))));
274+
List.iter (fun p -> let pid = go p in
275+
Buffer.add_string buf (Printf.sprintf " n%d -> n%d;\n" pid id)) d.d_premises;
276+
id
277+
in
278+
ignore (go d);
279+
Buffer.add_string buf "}\n";
280+
Buffer.contents buf

0 commit comments

Comments
 (0)