Review follow-ups for #876: the CI gap, three stale soundness comments, and three test gaps - #905
Conversation
The unit tests under `executor/src/tests/` live in the lib target (`#[cfg(test)] pub mod tests;` in lib.rs), so none of the `--test <name>` steps select them, and the `test_ckzg` step filters by name and runs only ignored tests. They therefore never ran in CI — including the hint ecall's `HintUnknownSelector` / `HintAddressOverflow` / per-selector coverage, which has no other home. The new step shares the lib test binary with the `test_ckzg` step, so it costs a test run rather than an extra compile.
…ints The existing lying-hint tests all feed `[0; 32]` / `[0xFF; 32]`, which die in `Scalar::from_repr` / `FieldElement::from_bytes` and never reach the verify predicate. So the checks the fast paths' soundness actually rests on — `(x * inv) == 1` and `x·inv - 1 == 0` — had no test that exercised their rejecting branch. - `field_inv` / `scalar_inv`: hints that parse cleanly and simply are not the inverse (`inv + 1`, `-inv`), which must be rejected and recomputed. - `decompress_r`: an oracle returning the *other* root. That is not a lie — `-y` is as valid a root of x³+7 as `y` — so the verify accepts it and the fallback never runs, leaving the parity-selection branch solely responsible for the sign. With the honest oracle that branch fires only for the `k` whose root happens to have the wrong parity; forcing the negation exercises it for every `k`. Also drops a dangling "property C1" reference from the module doc and states the property directly.
The guest called `HINT_FIELD_INV` three times, so the AIR's `selector < 3` range-check was only ever exercised at 0 — an accepted-value bound that no end-to-end test pushed against. One call per selector (`HINT_FIELD_INV`, `HINT_SCALAR_INV`, `HINT_FIELD_SQRT`) covers the whole accepted range; `sqrt`'s input is 4, a quadratic residue mod p, so the hint is a real root rather than the zeros `compute_hint` returns on a numeric failure. `test_prove_hint_multi_rust_guest`'s expected value follows, now computed through `compute_hint` per selector instead of assuming three field inverses.
`is_valid_hint_selector` and its const-assert tie the AIR's range-check to the executor's accepted set, so the prover and executor can no longer disagree. The *guest* is a third declaration and is still unbound: `lambda-vm-syscalls` re-declares the same three selectors as `usize`, in a crate the workspace excludes, linked to the executor's `u64` copies by nothing but a comment. A divergence there is silent. The ecall would either trap on an unknown selector, or — worse, for a value that stays in range — return the wrong function's answer, which the guest's verify-then-fallback swallows as "the host lied" and quietly recomputes in software. Nothing fails; the guest just runs ~2000x slower for the right result. `lambda-vm-syscalls` is added as a dev-dependency for it. Unlike `crypto/crypto`'s and `ethrex-crypto`'s copies it is not target-gated, so it does build on the host — safe because that crate's guest-only items (the `#[global_allocator]` and the `_start`/`main` entrypoint) are already `cfg(target_arch = "riscv64")`, and `executor::tests` is itself `#[cfg(test)]`, so the non-test lib build never links it.
Follow-on to "Range-check the HINT output address low limb" and "Derive the HINT selector bound", which added interactions and constants but left these behind. - `hint.rs`: the `HintConstraints` doc still said the LogUp argument "already fixes `mu`'s value via the timestamp-unique `Ecall` tuple", framing `IS_BIT` as belt-and-braces. That contradicts the module doc directly above it: the `Ecall` tuple carries a per-instruction timestamp, a free column, so LogUp pins only the *sum* of `mu` over rows sharing a tuple — which a witness can satisfy by spreading `mu` with integer weights summing to 1. `IS_BIT` is load-bearing, and the doc now says so and points at that argument. Its bus list was also stale (one register read, no LT senders); it is three and three. - `prover/src/test_utils.rs`: same stale bus surface on `create_hint_air`. - `crypto/ethrex-crypto/src/lib.rs`: the comment justifying `negate(y2)` over `negate(rhs)` claimed negating `rhs` "would silently compute the wrong value in release". That is not what happens. k256's `negate(magnitude)` computes `2*(magnitude+1)*P_limb - self` under a `debug_assert!(self.magnitude <= magnitude)`; for a magnitude-2 operand the result stays non-negative, so the value is correct and it is the debug assert that fires. The reason to prefer `negate(y2)` is real, but it is a build-configuration hazard, not a wrong answer — worth stating accurately in a comment that exists to explain a non-obvious choice.
8ca5797 to
23384f9
Compare
MauroToscano
changed the title
|
Added one more commit ( The hint tests were running under a different k256 field implementation than the guest ships. k256 0.13.4 swaps So every test of the verify-then-fallback logic exercised code the guest never compiles. That matters here specifically because the two builds differ on exactly the operation these tests turn on: Incidentally this also means the code comment in The target now runs both profiles. Release because it is what ships; debug retained because its magnitude Also worth recording, as a coverage limit rather than a defect: on the host |
2 participants
Review follow-ups for #876, as commits rather than comments so they can be taken or dropped
individually. Targets
feat/hint-ecall, so merging brings them into #876 itself.Rebased and slimmed. This originally carried the
out_addrrange-check, the "BENCH ONLY" labelremoval, the
hint_minalignment comment and a selector-bound const-assert. All four have sincelanded independently on
feat/hint-ecall(5c55e4c1,1fa60ec6,2a5a6120,d3a85f49) and havebeen dropped rather than merged over. I checked both of the substantive ones rather than assuming
name-equivalence:
5c55e4c1(out_addr) is complete and equivalent — the thirdBusInteractiononADDR_OUT_0,the matching
LtOperationin the trace builder,lt_count += 2 → += 3incount_table_lengths,and
with_capacity(26) → 27. It derives the same seven-value window independently. Nothing left todo there.
d3a85f49(selector bound) is better than what this PR had and supersedes it. It introducesis_valid_hint_selectoras a single source of truth and const-asserts set equality in bothdirections; the const-assert here only checked the three constants were 0/1/2 and that the bound was
one past, which would not have caught a fourth selector added below the bound. The AIR re-exports
HINT_SELECTOR_BOUNDrather than restating it, so there is no second declaration to drift.What remains is five commits: one CI gap, three still-stale comments, and three test gaps.
The design itself holds up — I could not break the verify-then-fallback. An adversarial sweep of
5,138 end-to-end ecrecover comparisons plus ~7,000 per-seam, in both debug and release against the
vendored k256, found no hint for which
field_inv,scalar_invordecompress_rreturns anythingother than what the pure-software path returns, and the fallback cannot be skipped.
y = 0isunreachable,
to_bytes()normalises before serialising, and theasm!block cannot cache a stale*out.The CI gap —
d7380474test-executorruns only--test asm,--test rust,--test flamegraphand atest_ckzg-filtered--ignoredstep. Becauseexecutor/src/lib.rshas#[cfg(test)] pub mod tests;, everything underexecutor/src/tests/is a lib target that no CI command selects — including the hint tests thatare the only coverage anywhere for
HintUnknownSelector,HintAddressOverflow(both operands, plusthe accepted
2^32 − 32boundary) andcompute_hint's three selectors.I checked every
cargo test/nextestinvocation in the workflow. The nextest archive is scoped-p lambda-vm-prover -p stark -p crypto -p ecsm, with executor absent — so nothing anywhere runsthem.
One step in an already-required job, and no added compile time: the lib test binary is already built
by the
test_ckzgstep. The mechanism is pre-existing (ecsm_tests,keccak_tests,memory_testswere equally dark), so this is a missed opportunity rather than a regression in #876 — but it means
the operand-validation tests added by
5c55e4c1are currently unrun too.Three comments that would mislead an auditor —
23384f9cThese matter more than usual here, because in this table the doc comments are the soundness
argument. All three were checked against the current branch, and the operand work left them behind.
prover/src/tables/hint.rs— theHintConstraintsdoc says the LogUp argument "already fixesmu's value via the timestamp-uniqueEcalltuple". That is the exact opposite of the module doc~300 lines above, which correctly proves the
Ecallbus pins only the sum ofmu(the timestampis a free witness column) and that
IS_BITis therefore load-bearing.git log -Sdates the stalesentence to
ad21c37aand the correct analysis tobe9066bf— the later reversed the earlier andthe sentence was left behind.
It is the stated justification for the table's only algebraic constraint, so a future cleanup reading
it deletes
IS_BIT(mu)and reopens the+1/+1/−1spread-multiplicity hole. The same doc block alsostill lists the table's bus surface as one register read and no LT senders, which is now three reads
and three LT senders.
prover/src/test_utils.rs—create_hint_air's doc still describes "x12 register read, fouroutput MEMW writes", with no mention of the
x10/x11reads or the three LT senders.crypto/ethrex-crypto/src/lib.rs— the comment justifyingnegate(y2)overnegate(rhs)claimsthat negating
rhs"would silently compute the wrong value in release". Against vendored k256 0.13.4that is false:
negate(m)is2*(m+1)*P_limb − selfand is value-correct at any magnitude absentlimb underflow, and for a magnitude-2 operand
4*P_limb − self ≥ 0. The real consequence is trippingits debug assert. The code's choice is right; only its stated reason is wrong — which matters,
because a reader who believes
negateis value-incorrect above its declared magnitude may "fix" realcode on that basis.
Test gaps
0b93d949— pin the guest's selector constants against the executor's.d3a85f49bindsexecutor ↔ AIR. The guest is a third declaration:
lambda-vm-syscallsre-declares the sameselectors as
usize, in a workspace-excluded crate, tied to nothing but a comment. That is adifferent property and still unguarded.
The failure mode is silent, which is what makes it worth a test: a selector divergence makes the
verify-then-fallback swallow the wrong answer as "host lied", so the guest recomputes in software and
returns a correct result ~2000× slower, with nothing failing anywhere. Adds a
#[cfg(test)]-only dev-dependency onsyscalls; verified it cannot reach the non-test build(
cargo tree -p executor --edges normalhas zero occurrences) and that the guest-only hazards inthat crate —
global_allocator,entrypoint— are alreadycfg-gated.762b3540— exercise all three selectors inhint_multi. The guest calledHINT_FIELD_INVthree times, so
HINT_SCALAR_INVandHINT_FIELD_SQRTreached the prover nowhere. Now covers allthree at no extra CI cost: same guest, same single prove, expectation in
prove_elfs_testsupdatedto match. Both ELFs were rebuilt so the test runs against the new binary rather than a stale
artifact.
0c29db1b— negated-sqrt and canonical-but-wrong hints. Two gaps in the guest-side coverage.Both lie shapes previously tested (
[0;32],[0xFF;32]) die in parsing, so the verify predicate'srejecting branch was never exercised on a canonical value. And the negated-sqrt parity arm was
covered only by accident, via the parity of four hard-coded
kvalues — I confirmed the branch islive today by disabling the negation and watching
decompress_r_honest_hint_matches_softwarefail,but nothing pinned it.
A note on the tamper tests
Worth stating plainly, because it applies to the operand tests on both sides of this rebase: the
tamper-style tests for
ADDR_OUT_0,ADDR_IN_0andSEL_0are defence-in-depth, not isolationtests. I measured this by reverting the range-check and re-running — editing
ADDR_OUT_0alsounbalances the
x12register read and the four MEMW writes, so the proof is rejected with or withoutthe LT sender. The two pre-existing siblings admit as much in their own doc comments.
The structural test is the one with teeth: with the fix reverted it fails (
left: 2, right: 3). Thatfollows the precedent
test_hint_binds_out_addr_to_x12already set in that file for exactly thissituation, and it is worth preferring for the LT senders too.
Verification
On the rebased base, both hint guest ELFs rebuilt:
cargo test --release -p executor --lib36/36·
crypto/ethrex-crypto24/24 ·cargo test --release -p lambda-vm-prover hint13/13 ·make lintexit 0 (fmt-check + 4 clippy configurations, zero non-nvcc diagnostics).Not included — for the author
The PR body's numbers are stale: 41 columns not 37, and 27 bus interactions after
5c55e4c1,not 22. The Details and "In the AIR" sections also omit the
x10/x11bindings and the LTrange-checks — the checks that make the AIR's accepted set match the executor's, and so the ones an
auditor most needs to see.
The Impact table needs re-baselining.
5fd961a0was the right control when written, but twoperf PRs have landed between it and this branch —
9ccdaf28(perf(programs): build the ethrex guest with thin LTO #861, guest thin LTO, whose own commitmessage measures −2.28%/−2.37% guest cycles on the ethrex fixtures; confirmed present in the
treatment's guest manifest and absent at
5fd961a0) andd83b4d9e(perf(prover): halve GPU continuation proving time #863, GPU continuationproving). Roughly 2 points of the −44.1% belong to perf(programs): build the ethrex guest with thin LTO #861.
More importantly the fixture is not representative: this PR's own
/benchon the real block reports−10.4% prove time and +2.1% peak heap, against the body's −32% / −35%. The two reconcile —
3 hints per ecrecover × 29 ecrecovers × ~67k cycles ≈ −11% of the real block's 50.78M guest cycles —
because the 20-transfer fixture runs 9.16 ECSM per Mcycle against a real block's 2.28, so the work
this PR accelerates is ~4× denser there. The prove-time win is real and well separated (0.7%
spread); the suggestion is just to lead with the real-block number.
The +2.1% heap is not the new table: a marginal always-on AIR measures ~5 MB (from the
feat/dma memcpy #874-vs-Perf/dma tail wide memset #896 stacked pair, with epoch count held fixed). Epochs are capped in guest cycles, so
cutting cycles packed the same crypto into 11 epochs instead of 13, and peak heap moves in ~1 GiB
quanta from power-of-two table padding.
FIXED_TABLE_COUNTcoordination with feat/dma memcpy #874. Both take it 10 → 11 at byte-identical lines (86,546, 621), and Perf/dma tail wide memset #896 stacks on feat/dma memcpy #874 while Perf/ecsm affine selector #879 stacks on this branch. Whichever merges second must
resolve to 12. A length assertion exists (
prove_elfs_tests.rs:2825) but nothing asserts thetwo AIR lists agree in order — and lines 546 and 621 are separate conflict hunks, so an
independent resolution can order them differently, which surfaces only as a prove/verify failure.
~10 lines zipping the lists by name would close that permanently.
/profile_recursionwas never run on this PR (the workflow exists and is one comment). Analways-on table adds per-sub-proof cost to the recursion verifier in guest cycles and ~160–230 KB
per epoch proof; unmeasured across feat/dma memcpy #874/Feat/hint ecall #876/Perf/dma tail wide memset #896 alike.
make lintdoes not reachcrypto/ethrex-crypto(own[workspace]), and it is drifting —cargo fmt --checkthere exits 1 with 86 diff lines at the merge-base. That is what the "testchurn" in
ecrecover_tests.rs/ecsm_tests.rs/keccak_tests.rsactually is: pure reformat, no newcontent.
The rust-ELF cache key omits
crypto/ethrex-crypto/**, though it is a path dep of the ethrex guestand now carries the hint safety argument. This PR is safe (it touches keyed paths), but a future PR
touching only that crate would restore a stale
ethrex.elf. The recursion-ELF key two jobs downalready includes
crypto/**/src/**.