This repository was archived by the owner on Sep 12, 2026. It is now read-only.
Fixing stuff - #13
Merged
Merged
Conversation
A dropped constraint is the compiler's quietest failure: the happy path passes, nothing is diagnosed, and the only symptom is a proof of something weaker than the source says. Positive tests cannot catch it, so attack the absence of a constraint from three sides. - Perturbation (soundness/cases.rs), the shape of ../leanVM's own test_soundness_suite: one valid trial per program plus a table of single-cell pokes at the public input or a witness stream, each of which must make the run fail. Six cases covering the arithmetic relations, both assert forms, the division back-solve, the exponent range check, match_range dispatch, an if/else join, a mul_range loop with a runtime bound, pack64x2's K-range assertion, and the digest-as-verification idiom. - Equivalence (soundness/pairs.rs): two spellings zkDSL.md documents as interchangeable must accept exactly the same trials. This is the layer that finds dropped stores. A dropped store is invisible alone, since the program still runs and its honest witness still passes; it is obvious against a spelling that kept it, and the more permissive side is the buggy one. Each pair carries the promise it tests, to be quoted in the bug report. - Unconstrained reads (Execution::unconstrained_reads, asserted in cpu::prove): a cell an instruction read that nothing ever wrote. zkDSL.md says don't; this is what says whether the emitted code did. Read off the count and written vectors after the run rather than recorded in Mem::get, which is in the opcode loop, so it costs the prover nothing. Scoped to the program's own cells, below where the fill's frames begin: fill rows read cells nobody writes as a matter of course and are soundness-neutral for it. A hard assert rather than a debug_assert, since release is the only profile the VM runs in. The invariant holds today for every program in the repo, including the recursion guest: aggregate_one_signer and aggregate_two_to_one prove clean under it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`take_inline_ret_cell` handed back `RetBind::Stack(base, 1)`'s raw frame cell while its `RetBind::Gaddr` sibling arm materialized. If the `@inline` body had filled that cell with a deferred copy or constant, `stack_store` emitted nothing, so no instruction ever wrote it and every expression-position consumer read a cell outside the constraint system: `expr`'s call arm (an `assert` operand), `expr_into`'s call arm (any store RHS), and `lower_match_range`'s inline-arm join, whose `copy` also reads its source raw. An unwritten cell is not zero, it is free. Memory is a committed array and the memory bus only forces accesses to one address to agree, never that the address was written, so the prover fixes it at commit time and the honest runner back-solves it to whatever the statement demands. Before this commit `assert pick(v[0]) != v[1]` with `v[0] == v[1]` proved and verified, and the same program published three different values for `pick(v[0])` under one witness. The `let` spelling of the same source rejected all of it, which is the asymmetry: `ret_binding` hands over a `Binding::Stack` whose reads go through `word_src`, and an expression use has to agree with it. Fix is that one call, in both consumers. No instance existed in the shipped guest, whose `@inline` StackBuf returns are all two cells, so nothing previously provable changes. Regression test: soundness::pairs::inline_stackbuf_return_in_expression_position. Both of the new infrastructure's relevant layers catch it, which is why the pair is the whole test: the equivalence check sees the two spellings disagree on an equal-valued witness, and the unconstrained-read check sees the raw cell on every trial including the accepting ones. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`stack_store` deferred a copy-or-constant RHS as an `Alias` unconditionally and
emitted nothing, while the two consumers that name a stack run by its physical
cells did not follow the alias: the `BLAKE2s` output arm and `hint_witness`'s
destination. So the physical cell and the alias source were joined by no
constraint, and a `StackBuf` store was never the write-once equality assertion
that zkDSL.md §Memory promises and §BLAKE2s recommends by name ("If `out` was
already written, the statement *asserts* the digest equals it ... which is
exactly what a signature verifier wants"). It did not. Pinning a hint with
`s[k] = <checked value>` dropped the check, a pre-written `StackBuf` digest was
written where nothing read it, and two stores of different values to one cell
produced no conflict at all.
The alias is sound only while nothing else gives the cell a value, so track
that and stop the two from colliding, in both orders:
- `emit` records the stack cells an instruction writes (`Deref`'s local cell
included, since the interpreter fills whichever side of its equality is
unset), and `stack_store` emits instead of aliasing when `dst` is one of
them. That is the store-after-write order.
- `materialize_run` gives a raw destination run real values in its own cells
before a consumer names them, and marks the run written. That is the
write-after-store order. Called from the `BLAKE2s` output arm,
`hint_witness`, and `hint_f192_limbs`, which is the third consumer of the
same shape and had the same defect.
zkDSL.md said both things in different places; it now states the precondition
where it describes the alias, so the two halves agree.
Nothing in the shipped guest collided, so the emitted bytecode is unchanged
there: the whole workspace passes, including aggregate_two_to_one and the
adversarial aggregate_statement_binds / aggregate_hints_bind.
Regression tests: soundness::pairs::stack_store_pins_a_hint_like_a_heap_store
and ::prewritten_blake2s_out_asserts_the_digest, both verified red before this
commit. The first publishes the PIN rather than the hint on purpose: publishing
the hint hides a dropped pin, because the publication then forwards through the
very alias that dropped it and both spellings agree by accident.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Two defects with one root, both in the deferred-alias path. A second store into a cell whose value was itself deferred just replaced the first alias, so the two values never met: `s[0] = a; s[0] = b` emitted a single `SET` of `b` and asserted nothing, where the same pair of stores into a HeapBuf cell is the write-once equality assertion zkDSL.md §Memory promises. The previous commit's message listed this case while describing the bug, but its fix only covered a store into a PHYSICALLY written cell; a store into a deferred one stayed silent. This is that case. `scoped` then inherited it. A branch storing into a cell that carried a pre-branch alias took the replace path, so the branch's value lived only in the branch-local alias; `scoped` materialized it at the join and immediately restored the pre-branch alias over it, leaving the write orphaned and every post-join read forwarding to the pre-branch source. The published value was the pre-branch one whichever arm ran. The rule that fixes both: a store into a cell that already has a value, deferred or physical, is the assertion, so materialize what the cell already stood for and then emit. Assembly is untouched, since assembling a BLAKE2s operand or a list literal stores each cell once. `scoped` needs no change of its own: the in-branch store now asserts against the pre-branch value on both arms symmetrically, which is what makes restoring the pre-branch alias correct rather than lossy, since the assertion is exactly what says the two agree. Also sort `branch_outputs` before emitting its copies. It was iterating a HashMap, so two builds of one source could emit them in different orders and produce different bytecode. The bytecode digest leads the Fiat--Shamir transcript, so that is a verifier that disagrees with itself across processes. Guest unaffected: bytecode byte-identical (DBG_PROF_DUMP diff clean) and the recursion benchmark unchanged at 321,127 instructions / 796,006 cycles. Regression tests: soundness::pairs::two_stack_stores_to_one_cell_assert_equality and ::store_inside_a_branch_asserts_against_the_pre_branch_value, both verified red before this commit. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`lower_dispatched_call`'s join emits one `DEREF` per bound name without ever comparing that count to any callee's declared arity, while the non-fused path enforces exactly that (`call_into`). So one source was rejected by one lowering of `match_range` and silently miscompiled by the other. A name past a callee's arity reads a callee-frame offset nothing on the taken path writes, and because the shared frame is sized to the LARGEST callee the offset exists inside the allocation: the surplus name binds a prover-chosen word. Memory is a committed array and the memory bus only forces accesses to one address to agree, never that the address was written. Broader than mixed-arity arms, which is how it was first described: a SINGLE over-bound callee fuses with no diagnostic too, and that is the shape all three guest sites use, so the guest was correct only because its author counted right, with nothing checking. The check has to look the callee up in the queue as well as in `defs`, which is the reason a `defs`-only version of it passes on everything: `specialize` registers a `Const` specialization in the queue under a mangled name and never puts it in `defs`, and a dispatched `match_range` names specializations exclusively. `return_shapes_of` covers both. Regression tests: soundness::cases::dispatched_call_rejects_a_mixed_arity_arm and ::dispatched_call_rejects_an_over_bound_callee. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
zkDSL.md §Global constants reserves a top-level constant's name: "do not reuse it as a parameter or local name". A SCALAR constant enforced that by construction, since the parser substitutes its value textually and the shadowing binding becomes a literal, which fails loudly. A constant ARRAY is carried to lowering instead, where `const_array_elem` resolves `NAME[i]` against `const_arrays` without consulting the scope and `expr` folds constants before its index arm could see the local. So the collision was silent, and the local's compile-time-indexed reads were folded to baked literals. That is the catastrophic direction for a hint. A `hint_witness` into a shadowed buffer had its range check evaluated against the constant: `Q = [8, 32]` with a local `Q = StackBuf(2)` compiled `assert log(Q[0]) < 8` into the 3-cycle gadget applied to the literal `g^3`, which passes, while the actual witness `g^40` was never bounded and its cells never read. Checked at the three places a name is bound: `rebind` for locals and assignments, the inline-callee parameter binds, and the function-entry parameter binds. Rejecting is right rather than letting the local win, since picking a winner silently changes the meaning of existing sources and the doc already says the name is not available. The guest defines many constant arrays (the LIG_* tables) and collides with none of them. Regression tests: soundness::cases::a_local_may_not_shadow_a_constant_array and ::a_parameter_may_not_shadow_a_constant_array. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…rifiers A proof announces table heights, a memory size and a rate. Each was capped on its own, but what the PCS has to be configured for is the stacked size 2^mu they IMPLY, and the caps do not bound it: maxing all of them gives mu = 41, and the memory cap alone gives 35 while the bytecode cap alone gives 33. So the documented instance caps describe shapes the WHIR ladder has no config for at all, and nothing checked it: the missing config surfaced as a panic inside the opening. `pcs::MAX_MU` is the single knob, and everything else derives from it. `cpu::read_public` checks `MIN_MU..=MAX_MU` before any reduction runs against the layout, and `rec_aggregation::MU_MAX` IS `pcs::MAX_MU`, so the recursion guest's compiled opening arms follow the knob through its existing placeholder (`LIG_N_LOG_SIZES`) with nothing to keep in step by hand. Verified by moving it: at 29 the guest recompiles to 364,481 instructions from 321,127, the four extra arms, and the whole suite passes. `python-verifier` is standalone and dependency-free, so it cannot read the Rust constant and keeps a literal. `whir_query_table.rs` already dumped its two ends without comparing them; it now asserts them against the Rust constants and its failure message names the edit. MAX_MU = 28 is a policy cap, not the ladder's ceiling, which is higher and rate-dependent (36 at log_inv_rate 1, 32 at 4). A test keeps the window inside what the ladder supports at every rate, which is what lets a plain range check stand in for re-deriving it. Note that 28 leaves one bit over the non-recursive XMSS path, which commits 2^26.195 at 900 signatures and scales linearly with the signature count: doubling that workload needs the knob raised, and raising it costs ~4 guest opening arms of ~12k instructions per size. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`from_parts` recomputed the two deferred claims before anything else, so deserializing ran a pass over the whole stacked bytecode plus a walk of the BLAKE2s circuit on points a peer chose. Anything decidable without that has to be decided first: `recompute` already checked the point dimensions, and `check_signer_set` now runs ahead of it, so a malformed signer set costs a sort check instead of the two evaluations. `verify` still checks it too, since `aggregate` builds the object directly rather than through `from_parts`. Also reject trailing bytes. `bincode`'s free functions allow them, so every padding of an aggregate's encoding decoded to the same aggregate, and anything downstream that dedupes or indexes on the serialized bytes could be shown one aggregate as many. `wire()` keeps the same fixed-width integer encoding and rejects the trailing bytes; the encoding was checked to be byte-identical to what the free function produces, since a wire-format change would have to move every encoder and decoder with it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
It was zero everywhere and had never run. The only two sources of `fold_grinding_bits` were `vec![0usize; n_levels]` in the fallback config and the literal `0` in the production derivation, and two assertions pinned it there, so four implementations of the mechanism (the prover, the native verifier, the recursive verifier, and the guest's zkDSL) had never executed a single time in any test. Untested code that claims a security capability is worse than absent code, because it reads as coverage. It is also not the lever it looks like. The eta search keeps the proximity-gap term at or above the 128-bit target on its own across every feasible size (measured: min pg_bits is 128..137 over the whole ladder at every rate), so grinding the fold challenges had nothing to close. Where the ladder does stop, it stops because no eta satisfies the Johnson terms simultaneously, at committed sizes well past anything reachable here: every leaf has to be guest-verifiable, so MU_MAX = 28 caps the whole topology while fold grinding would only have bought roughly 32 to 37. Removal is transcript-neutral by construction, since every grind sat behind `if bits > 0` and the bits were always 0. Confirmed: bytecode 321,127 instructions and 796,006 cycles for the recursion benchmark, 2^26.195 committed for the XMSS one, all byte-identical to before, and the adversarial aggregate_statement_binds / aggregate_hints_bind / aggregate_three_levels pass. Query-phase grinding is untouched: it is a live, load-bearing 17 bits. Side effect worth noting: `pow_bits_ok`'s `debug_assert!(bits < 64)` precondition now has one caller instead of two, and the survivor is a compile-time constant. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`lean_vm::cpu::read_public` rejects a bytecode that is not a power of two or longer than 2^MAX_LOG_BYTECODE; `python-verifier` checked neither. The power-of-two half was reachable only through `Framework.log_bytecode`, a property, so it fired wherever that was first read rather than up front, and nothing bounded the length at all. Checked in `build_layout`, with the memory-size, table-height and BLAKE2s-floor caps it belongs to. `0 <= log_bytecode` also rejects a bytecode shorter than one bus row, which used to yield a negative log and carry on. The 2^32 ceiling is not exercisable in a test: reaching it needs 2^36 K-words of stacked bytecode. Same on the Rust side. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Protocol 1 step 4 described a final level that checks `Enc(f_final)[x_q] == c_q` for each query directly. All three verifiers instead turn each consistency check into a weighted claim about `f_final`, which Lemma `lem:colweight` already says it is, batch those with the residual claim under a fresh lambda drawn after the columns and their opened rows are bound, and discharge the batch with the level's remaining sumcheck rounds, closing on one evaluation of the transmitted table. That is one evaluation of `f_final` where the written version is `n_q` encodings of it. Same claims, so the case analysis is unchanged; it now ends by putting `f_final` in violation of one of the `n_q + 1` batched claims rather than failing a check outright. The extra batching challenge the implementations draw was missing from `thm:rbr`, so add its term: `n_q / |E|`, with no union over a list, since `f_final` is a single transmitted table rather than one of the codewords near an oracle. At the query counts in use that term is far below the 128-bit target, so the security level does not move; the point is that the theorem now accounts for every challenge the protocol draws. The RBR invariant gains the matching step, since the transcript no longer ends at the final query message. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`johnson_algebraic_bits_for` took the level's OWN query count as the degree of
its batching polynomial. The claims that batch carries are the ones the
PREVIOUS level's query phase raised: `thm:rbr` has `J_i = n_{i-1} + 2`, one per
query plus the residual and the OOD claim. Query counts fall with depth (at
rate 1/2, log_n 28: 228, 56, 38, 28, 23, 19, 16), so the level's own count is
the smaller one, and substituting it understates the degree and overstates the
bound, by about 2 bits at L1.
Thread the previous level's count through instead: the eta search takes it as a
parameter, and `validate()` and the production-profile test read it off the
level list.
Inert either way today, which is the reason to fix it rather than leave it: the
degree is `max(RING_SWITCH_SOUNDNESS_DEGREE, prev_queries + ood_samples, 2)`,
and the ring-switch map's degree is about 2^31, some 23 bits above any query
count, so it takes the max at every level. A wrong term with no effect is the
kind that survives a refactor; if that degree is ever tightened, or a level
skips ring switching, the bound now degrades correctly.
Derivation unchanged, and checked rather than assumed:
`whir_query_table_matches_rust` compares the derived query counts against the
pinned table at every rate and size in the window, and still passes.
L0 is passed 0 and still does not model `J_0`, which is the outer protocol's
claim pool rather than a query count. Recorded in the comment; accounting for
it would mean teaching `whir_config` about `lean_vm`'s pool.
Co-Authored-By: Claude Opus 5 (1M context) <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 subscribe to this conversation on GitHub.
Already have an account?
Sign in.
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.
No description provided.