feat(jeg): judgement evidence graph — reify derivations, and CHECK them

[hyperpolymath]

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:

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

[gitar-bot]

Note

Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime.
Learn more

Code Review ✅ Approved 2 resolved / 2 findings

Adds the Judgement Evidence Graph to reify and independently check type derivations, but --derive exits 0 on type errors and DOT label escaping corrupts quotes.

✅ 2 resolved

✅ Bug: --derive exits 0 on type errors despite gating claim

📄 compiler/bin/main.ml:207-221
derive_file only increments failures for JEG check errors; a definition that fails to typecheck raises Type_error, which is caught, printed to stderr, and swallowed without touching failures. So --derive/--derive-dot exit 0 even when a definition doesn't typecheck, contradicting the stated contract that the command 'exit[s] non-zero on failure'. In a CI gate this lets broken sources pass. Increment failures in the Type_error handler so type errors also force a non-zero exit.

✅ Quality: DOT label escaping corrupts quotes and ignores backslashes

📄 compiler/lib/jeg.ml:271-273
The DOT label is built by replacing each " with \' (backslash-apostrophe), which silently changes any double-quote in the rendered judgement (e.g. from a StringLit) into an apostrophe rather than escaping it, and it does not escape pre-existing backslashes. The Graphviz convention is to emit " for an embedded quote (and \ for a backslash). Escape backslashes first, then quotes, to keep labels faithful and valid.

Options

Display: compact → Showing less information.

Comment with these commands to change the behavior for this request:

Compact

gitar display:verbose

_{Was this helpful? React with 👍 / 👎 | Gitar}