Repository navigation
Conversation
…λ-match on it, so the kernel checks that the values cover it (bendlang#1186) root_cols enumerated a specialized parameter of a finite type (Quant, or a datatype whose constructors have no fields) and safe.ts sent one instance per value, so --verdict trusted that the enumeration covers the def. At an empty type there were no instances: the def never went to the kernel, and --verdict still printed ALL PROOFS CHECK. root_cols now returns its enumeration as a tree, and root_emit sends a root with branches as one def: a λ-match on each finite parameter whose arms are the instances' bodies (or name the instance, for a datatype, a def with no body or an @unsafe one), at a type that is a λ-match on it too. The kernel checks that the match covers every value, and at an empty type that there are none: λ{(,): λ{}}. Instances still go out where a caller uses them. Closes bendlang#1186 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…mit is written like the rest of the file Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… a case two others cover Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…-match arms instead of inlining their bodies The instances were never the problem: what main lacked was a check that they cover the root. Naming them keeps main's defs byte-identical, drops the second copy of a recursive body, and the special case for a datatype, a def with no body or an @unsafe one. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… the values it holds, and shares one λ-match helper, mats, with adt_emit and group_emit
…goes out after them, reports a failing instance's own reason, and --verdict fails a def that reaches no kernel def Each arm of the covering def's type is now the def's type, a λ on its ~ parameters, applied to that instance's arguments, so the kernel checks the substitution instead of trusting tele_fill on both sides. Where the def's type needs its ~ parameters closed (a template call), the arm is the instance's own type, as before. The instances go out before that type is built, so one whose type is out of scope no longer takes the others with it, and a root reports its first failing instance's reason rather than "names <instance>". A match node keeps its kernel labels and whether it is a datatype's, and QS spells Quant's labels once. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…, which the kernel checks, in one walk over the telescope
The covering def's arms were checked against a λ-match type built from
the same tree as its body, so a root_emit bug that named one instance
under two labels passed: the kernel checked coverage and each instance
against the def's type at its own arguments, never that the arm under a
label holds that label's instance. Each match is now annotated
∀y:A -> Σz:A -> {z == y : A} and each arm returns its value, so the
kernel ties the label to the instance it names.
The cover is a def at <()> that checks the instances in erased lets,
with G, the def's type as a λ on its ~ parameters, bound once instead of
copied into every arm; an arm names its instance unannotated where G
needs its parameters closed. root_of and root_emit are one walk that
emits each instance at its leaf, so the Root tree is gone. safe.ts is
23,278 ttok (main 22,386).
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…cannot go out is undone, and the unit type and value are UT and UV A root kept only its first failing name's reason, where main printed one line per failing instance; it now prints each distinct one, and its cover's only when alone (that reason names an instance). Building G registers the names its type mentions, so a Scope_Error there is undone as item_ref undoes a failed emission. The test says no gate runs --verdict to failure. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…aves nothing behind, and fin says whether it has a finite parameter
…tors, so calls and literals (flip(b) == False, Nat.add(1n, 1n) == 3n, 1 == 2 : U32) refute like written constructors; the kernel still checks each refutation
What 4ecba08 changes: before looking for a constructor mismatch in an equation column, both sides are first evaluated to constructors ( Probes (
Soundness checks:
Gates on 4ecba08 (macOS):
Not run: Linux, CUDA, the hub corpus. |
|
Pulled4ecba085 without rewriting it and published four permanent call/literal regressions in e4d52cd. On Linux, the resulting eleven-law fixture prints ALL PROOFS CHECK with the source-matched Lean4.34.0 native kernel; emitted JS and native C both print3n. The original constant-Unit-motive certificate is rejected (exit1, expectedEmpty), and the inhabited but unmodelled probe equation remains out of scope (exit1, no model for stuck~h). Repo gate passes54/54 using the persisted tokenizer cache. The description now separates this Linux evidence from your disclosed unsupervised normalization contribution and your reported macOS/cluster results. No cluster/GPU or human-review claim from me. |
Fixes #1544. Parent #1225 is merged; main dbb3157 is integrated normally. Current head is e4d52cd, preserving peer normalization commit 4ecba08 and adding its permanent regressions. This remains the empty-equation follow-up, not a second claim to resolve #1186.
A specialized equation with incompatible closed constructor shapes contributes a kernel-checked empty-domain proof to the root cover. A discriminator maps the left endpoint to Unit and the incompatible endpoint to Empty; equality rewriting transports the Unit inhabitant, and Empty elimination closes the Unit-valued coverage branch. Nested dependent fields retain their prefix matches. Model failure is never evidence of emptiness; failed attempts restore exporter state.
Equation-only refutations trigger coverage even without a finite datatype parameter. The merged parent's Open_Error-only type fallback, per-column cache, transactional exporter log and selector encoding are preserved. Two private variable/application AST constructors replace repeated node literals to fit the permanent safe.ts cap; the actual parent finite-cover export is byte-identical after this cutover. No protected checker, kernel, gate, cap or workflow edits; no unrelated comment trimming.
Both equation endpoints are evaluated to constructors before mismatch detection, including nested fields and U32 literal Word bits. That normalization and the shared EFQ simplifications are the peer contribution in 4ecba085, explicitly disclosed by its author as unsupervised AI work without human review. Linux qualification and the four added regression cases below are separate from the peer's reported macOS/cluster runs.
Verification on Linux x86_64, Bun 1.3.13 and the actual source-built Lean 4.34.0 kernel:
BEND_NO_TELEMETRY=1 bun bend2/main.ts tests/proof/empty_equation_cover.bend --verdict: ALL PROOFS CHECK. Eleven laws retain the seven original cases and addflip(b) == False,Bool.and(a,b) == True,Nat.add(1n,1n) == 3n, and1 == 2 : U32.3n.probe(n) == Falseequation whose evidence is used stays out of scope (no model for stuck~h), not an absurd branch.bun gates/repo.tspasses54/54 with the persisted cl100k tokenizer cache; the first post-restart combined command timed out after printing its kernel verdict and is not claimed as a gate pass.The maintainer-reported #1544 failure and the peer's pre-normalization failures are the before evidence, not rerun merely to confirm them. Positive, wrong-motive and nonempty-unmodelled controls were exercised locally. The fixture participates in the existing proof corpus; no separate Lean job is proposed. No cluster, GPU, macOS or hosted-current-head pass is claimed as our execution. AI-assisted, no subagents.