Route kernel-decidable Lean verify cases through decide +kernel - #812
Merged
Conversation
Sampled `verify` cases all emitted `native_decide`, which puts `Lean.ofReduceBool` into every case's axiom closure — the proof rests on native evaluation rather than on the kernel. Concrete SHA-256 examples carried that trust axiom even though the exported crypto model is total and kernel-reducible. Classify each case instead. A case emits `decide +kernel` only when the emitter can positively establish that its whole closure reduces in the kernel, and `native_decide` whenever anything is unknown: - Kernel-opaque emissions are read off the text this export actually produced (`partial def`, `unsafe`, `opaque`, `sorry`, a fuel wrapper's `panic!` arm, any mutual group), not re-derived from the source shape. - Any Float reachable through the closure disqualifies a case: Lean has no `DecidableEq Float`, and the prelude's shim is an `@[implemented_by]` `opaque` constant. Recursive user types carry the same shim. - Builtins are allowed from an explicit table pinned against Lean 4.32; a new `Builtin` variant is a compile error there, not a silent reclassification. - A case needs the VM ground-truth literal on its expected side. Lean's `panic!` returns `default` silently under kernel reduction where native evaluation prints the `PANIC at …` line `aver proof --check` charges as a failure, so a literal expected side keeps that gate meaningful. - Oversized terms keep `native_decide`: kernel reduction has no heartbeat limit, so the emitted term text carries a 1 KiB data budget calibrated against the measured SHA-256 curve. Only proof mode classifies; the standard emit is byte-identical. On `tests/fixtures/stdlib_bytes_app.av` the SHA-256 and byte-range cases now build green under `decide +kernel` (1.3-7.4 s each, entry module 0.3 s to 6.3 s) with axiom closures inside Lean's core three, while the hex cases stay native because they route through the `partial def` hex parser. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The literal expected side was carrying the whole anti-vacuity argument,
and it does not hold on its own. Lean's `panic!` returns `default`, and
under kernel reduction it does so with no diagnostic, so a model that
panics still satisfies the equation whenever `default` equals the value
the VM recorded — `false` for any `Bool` case, which is half of them.
The reviewer's counterexample reaches that in two steps, neither of
which a single-builtin audit catches:
s = match Vector.get(Vector.fromList(["x"]), 0 - 1)
Option.None -> "B"
Option.Some(_) -> ""
Char.toCode(s) == 65
`Vector.get` lowers to `arr[Int.toNat i]?`, and `Int.toNat` maps every
negative index to `0`, so the model takes the `Some` arm the runtime
never took, lands on `Char.toCode ""`, and defaults that panic to `0`.
`0 == 65` is `false` — the literal the VM recorded. It built green and
silent under `decide +kernel`; on `native_decide` the same case prints
`PANIC at Char.toCode` and `aver proof --check` fails the run.
So classify the faithfulness of each builtin's lowering next to its
kernel-reducibility, in a second exhaustive table a new `Builtin`
variant cannot skip. Declined: `Char.toCode` (reaches `panic!` on the
empty string), `Vector.get` and `Vector.set` (narrow a negative index
the runtime rejects — and `Array.set!` panics outright on an empty
vector). Kept, with the reason recorded: `List.take` / `List.drop`
narrow through the same `Int.toNat` but the runtime clamps identically,
`String.slice` and `String.charAt` guard theirs, and SHA-256's
`Array.get!` / `set!` indices are fixed by the definition rather than by
any argument. Across the example and proof corpora 37 sampled cases move
back to `native_decide`, all in `examples/games/wumpus.av` (Vector.get)
and `examples/data/json.av` (Char.toCode).
Two more fixes in the same area:
- The term budget measured only the left-hand side, so a three-token
call returning kilobytes of literal data passed it. The kernel reduces
the equation, so budget the equation.
- The named-type walk keyed its field scan on the bare type name, which
unions two dependency modules' same-named records: a `Metrics.Reading`
of one Int inherited the Float of a `Sensors.Reading` and lost kernel
coverage. Follow the stamped `TypeId` instead, with the source name
only as the fallback for references the symbol table never bound.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Sampled
verifycases all emittednative_decide, so every case's axiom closure carriedLean.ofReduceBool— including concrete SHA-256 examples, whose exported model is total and kernel-reducible.Each case is now classified individually.
decide +kernelis emitted only when the emitter can positively establish that the case's whole closure reduces in the kernel; anything unknown stays onnative_decide.What declines a case:
partial def,unsafe,opaque,sorry, a fuel wrapper'spanic!arm, any mutual group)DecidableEq Float; the prelude shim is an@[implemented_by]opaqueconstant), and recursive user types, which carry the same shimBuiltinvariant is a compile error rather than a silent reclassificationpanic!returnsdefaultsilently under kernel reduction where native evaluation prints thePANIC at …lineaver proof --checkcharges as a failurelake buildslowOnly proof mode classifies; the standard emit is byte-identical.
Evidence on
tests/fixtures/stdlib_bytes_app.av: the SHA-256, byte-range and digest-length cases emitdecide +kerneland build green (1.3–7.4 s per case; entry module 0.3 s → 6.3 s, whole project 5.4 s → 7.8 s), with#print axiomsreporting onlypropext/Quot.sound. The hex cases stay onnative_decidebecause they route through thepartial defhex parser. Both verdicts live in one file, so a classifier that collapses either way fails the new regression.Tests: two additions in
tests/proof_spec/lean_kernel.rs(crypto routing + axiom-closure audit via reallake, and a Float pin on the newtests/fixtures/kernel_decide_split.av). Fullproof_specsuite green locally with real lake — 233 passed, 0 failed, 171 s. Thelarge_domain_lawgolden moves onetripleSumcase to the new tactic.🤖 Generated with Claude Code