[MuhDur]

Closes #1182.

--verdict checks a template at opaque constants k~p, and the kernel needs each one to have a model. The models were picked one at a time: le got λx y. False{}, so a law ~step: … -> {le(x, y) == True{}} had none, the def went out of scope (bend f.bend -o f.bendtt says no model for step_le~step), and --verdict reported a mismatch without running the kernel. A law over a template type, {x == y : A} at A = Unit, had none either.

model_at now yields its models best first, inside #1218's bounded search; the first is the one it returned before, after the same work, so every model model() picks is unchanged (#1338's Unit and datatype checks included). When a constant has none, refit backtracks over the root's constants so far, up to 8 models each, in model_by's rounds of doubling depth on one MODEL_FUEL, so the backtracking is bounded too; def_emit emits the models it chose. Only in that search, a live λ of a datatype whose constructors have no fields, with no model under a variable, gets a match. The kernel still checks every model and the constants stay opaque in the body. Contradictory laws have no models that hold together, so they stay out of scope instead of handing the kernel a closed def of type Empty.

Checks:

• New tests: tests/proof/template_law_models gives SOME PROOFS FAIL under --verdict on main and ALL PROOFS CHECK here; tests/proof/template_laws_contradict is accepted by bend2 and stays out of scope (no model for bad~ir).
• Kernel alone, with the emitted roots' bodies edited to {==}: rejected (expected: le x0 x1, observed: True; expected: x0, observed: x1), so the convenient models don't leak into the proofs.
• On all 1588 tests/**/*.bend, --verdict output and the -o BendTT text are byte-identical to main; only the two new tests are added.
• tsc gives the same 12 errors as main. gates/repo.ts passes 50 / 50; safe.ts goes from 21,935 to 22,836 ttok (cap 24,000).
• On the hub package bend-mathlib, algebra and order (transitivity/associativity chains over a ~le / ~op with their laws as ~ proofs) now pass --verdict; bool, equal, list, maybe, nat, perm and string emit identical BendTT. sort brings its ~le_total roots into scope but still fails on defs out of scope for another reason (a kind that depends on a run-time value).
• Not run: the cluster gates, gates/safe.ts and gates/test.ts included.

Not covered: a ~ law whose only model is a real proof (the injectivity ~F in the original report) still has none.

🤖 Generated with Claude Code

https://claude.ai/code/session_01LLZJANUtM1mTd4jg5kXqJf

[MuhDur]

Rebased onto main after #1218: the candidate models and the backtracking now run inside its bounded search (one MODEL_FUEL, its doubling depth), and model()'s answers stay exactly main's. On all 1554 tests, --verdict and the -o BendTT text are byte-identical to main.

[MuhDur]

Rebased onto main 53fc961 (after #1338/#1220/#1224). #1338's Unit-provenance check is kept inside the unchanged first answer; it does not cover the {x == y : A} at A = Unit case, so the match model stays (only inside refit). On all 1588 tests, --verdict and the -o BendTT text are byte-identical to main apart from the two new tests.

[MuhDur]

This conflicts again after #1353/#1354 (both touch safe.ts/def_emit). Since that code is moving daily, I'll hold off on rebasing until someone has a look; happy to rebase on request, it's a short job. The root cause is on #1182 and the two added tests (tests/proof/template_law_models.bend, template_laws_contradict.bend) pin the intended behaviour.

[Lorenzobattistela]

Thanks @MuhDur I'm reviewing rn and ended up rebasing, i'll report back shortly

[Lorenzobattistela]

Thanks @MuhDur, the diagnosis is right: safe.ts picks one model per ~ constant at a time, and that is why v_n
never reached the kernel. But this PR doesn't fix #1182, so we're closing it.

Why it doesn't fix #1182: I rebased it onto current main and ran leo-guinan's three repros (
higher_evidence_base, law_higher_evidence_probe, dependent_empty_result_probe). All three still fail
--verdict with no model for use~F, both on this branch and on main. Their ~F is an injectivity proof ({S{a}
== S{b}} -> {a == b}). The model search builds models from constructors and constants only, so it can't
produce one, and searching harder doesn't help. Backtracking only helps when a root has several ~ constants
that each have a model but the first ones picked don't fit together. That's your v_n and bend-mathlib's
algebra and order, not the issue as reported.

Why we'd rather not take it as a partial fix:

• It adds about 900 ttok to safe.ts. Fixing the problems below brings that to about 1,400, which leaves 336
under the 24k cap.
• The search blows up when unrelated ~ constants sit between a law and the constant it reads: about 7 to 10 s
per root, then a false out of scope. Backjumping fixes this, but it adds more code.
• It interacts badly with #1358, where roots share ~ constants. Either a refit changes a constant an earlier
root already depends on, or, if kept constants are never refit, later roots lose proofs that pass today
(bend-mathlib's sort.bend ~le_total roots).
• Whatever it gains is fewer false rejects. It doesn't change what gets certified.

A direction that could fix #1182: use checked defs as models. If the book has a closed, kernel-checked def of
the same type as the ~ constant (inj in the repro), use it as the model. That covers the reported case
directly, and it's a lookup rather than a search.

Note: the head of this branch (a357864) is my rebase, which has a --verdict crash (vs.flatMap(at) passes the
index as a constant). That's on me, not you, and closing makes it moot.