fix: non-vacuous range-check specs + verdict-engine hypothesis audit - #11
Conversation
The trust root of every proof is its Spec, and nothing checked the Spec — the
range-check specs were quietly weak:
- `range_check_8bit_sound` concluded `∃ k : Fin 256, (k.val : ZMod p) = x`, which
is vacuously true whenever `p ≤ 256` (every field element is then the cast of a
byte). `hp : p > 256` was declared as a `variable` the theorem never referenced,
so Lean dropped it from the signature entirely — the theorem proved something
strictly weaker than "x is a byte" and never required the bound.
- `HalvaRangeCheck.Spec` took `hp : P > 10` but never used it, so it was decorative
around the same vacuous existential.
Restate both as the honest, non-vacuous bound `ZMod.val x < 256` (resp. `< 10`),
which cannot be proved without the prime bound:
- Move `hp` into an explicit, load-bearing hypothesis used by the proof via
`ZMod.val_natCast_of_lt` (N < bound < p ⟹ `ZMod.val` of the cast is exactly N).
`#check @range_check_8bit_sound` now shows `p > 256` in the signature.
- HalvaRangeCheck keeps the 10-way field case split to establish membership in
{0..9}, then converts to `ZMod.val advice < 10` using `hp`.
- Add a machine-checked non-vacuity witness to each file
(`¬ ((256 : ZMod 257).val < 256)`, `¬ ((10 : ZMod 11).val < 10)`).
Begin the dual-sided verdict engine (a refuter over the Spec) with its
deterministic core, C1 (hypothesis liveness), in `lean/ZkGadgets/Audit.lean`:
- `#audit_uses <thm>` errors if an explicit hypothesis is never used by the proof
term (catches the decorative-hypothesis class).
- `#audit_requires <thm> "needle"` errors unless `needle` is in the signature
(pins a load-bearing bound so dropping it turns the build red).
Both have an in-file self-test and are wired as live CI gates next to
`range_check_8bit_sound` ("p > 256") and `RangeCheck.soundness` ("P > 10"); they
pass now and fire on the pre-fix specs. Finite-model non-vacuity probes (C2),
antecedent satisfiability (C3), and an adversarial LLM refuter (C4) remain, noted
in the Audit.lean module header.
Both proofs stay kernel-checked (lake build green; #print axioms shows only
propext/Classical.choice/Quot.sound). README restructured (hero, badges,
sections) with the gadget table updated to the honest claims.
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: c389d0b260
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| docker run --rm scribe:dev scribe --help | ||
| ```sh | ||
| cargo run -p halva-bridge -- examples/halva-range-check/extracted.lean \ | ||
| --spec-file examples/halva-range-check/spec.lean \ |
There was a problem hiding this comment.
When users follow this documented command, halva-bridge reads examples/halva-range-check/spec.lean; checked that file and its Spec still concludes the old ∃ k : Fin 10, ... form at lines 9-11, with hp unused. That regenerates or optionally proves the vacuous range-check theorem this change is trying to retire, and even writes it over lean/ZkGadgets/HalvaRangeCheck.lean, so the example spec should be updated to the new ZMod.val ... < 10 claim before this path is advertised.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Fixed in e10a215. examples/halva-range-check/spec.lean now states the honest ZMod.val (advice) < 10 claim (matching lean/ZkGadgets/HalvaRangeCheck.lean), so the documented bridge command no longer regenerates the vacuous spec. Verified: re-running the command emits the non-vacuous Spec and the scaffold compiles.
Codex review: the README documents `halva-bridge … --spec-file examples/halva-range-check/spec.lean`, but that input spec still concluded the old `∃ k : Fin 10, …` form with `hp` unused — so following the documented path would regenerate (and could overwrite) the vacuous theorem this PR retires. Update the example spec to the honest `ZMod.val (advice) < 10` claim, matching lean/ZkGadgets/HalvaRangeCheck.lean. Verified: re-running the documented bridge command now emits the non-vacuous Spec, and the scaffold compiles.
1 participant
The bug
The trust root of every proof is its
Spec, and nothing checked theSpec. The range-check specs were quietly weak:range_check_8bit_soundconcluded∃ k : Fin 256, (k.val : ZMod p) = x, which is vacuously true wheneverp ≤ 256(every field element is then the cast of some byte).hp : p > 256was declared as avariablethe theorem never referenced, so Lean dropped it from the signature entirely — the theorem proved something strictly weaker than "x is a byte" and never required the bound.HalvaRangeCheck.Spectookhp : P > 10but never used it — decorative, around the same vacuous existential.The fix
Restate both as the honest, non-vacuous bound
ZMod.val x < 256(resp.< 10), which cannot be proved without the prime bound:hpmoved into an explicit hypothesis, used by the proof viaZMod.val_natCast_of_lt(N < bound < p ⟹ ZMod.val (↑N) = N).{0..9}, then converts toZMod.val advice < 10usinghp.¬ ((256 : ZMod 257).val < 256),¬ ((10 : ZMod 11).val < 10).Verdict engine (C1)
Begins the dual-sided verdict engine — a refuter over the
Specthat complements the single-sided proof loop. This lands its deterministic core, C1 (hypothesis liveness), inlean/ZkGadgets/Audit.lean:#audit_uses <thm>— errors if an explicit hypothesis is never used by the proof term (catches the decorative-hypothesis class).#audit_requires <thm> "needle"— errors unlessneedleis in the signature (pins a load-bearing bound so dropping it turns the build red).Both have an in-file self-test and are wired as live CI gates next to
range_check_8bit_sound("p > 256") andRangeCheck.soundness("P > 10"). They pass now and fire on the pre-fix specs.Remaining phases — finite-model non-vacuity probes (C2), antecedent satisfiability (C3), adversarial LLM refuter (C4), and a
scribe auditverdict subcommand — are noted in theAudit.leanmodule header.Verification
#check @range_check_8bit_soundnow showsp > 256in the signature (reproduced the original drop before fixing).#print axiomson both theorems: onlypropext,Classical.choice,Quot.sound— nosorryAx.lake buildgreen; the audit guards demonstrably fire on a regression.Also restructures the README (hero, badges, sections) and updates the gadget table to the honest claims.