diff --git a/.github/workflows/pr_main.yaml b/.github/workflows/pr_main.yaml index 62c3cd19d..2d7c1723b 100644 --- a/.github/workflows/pr_main.yaml +++ b/.github/workflows/pr_main.yaml @@ -117,6 +117,15 @@ jobs: run: | cargo test --release -p executor --test flamegraph + # The unit tests under `executor/src/tests/` are a *lib* target (`pub mod tests;` + # in lib.rs), which none of the `--test ` steps above select — and the + # `test_ckzg` step below filters by name, so it doesn't run them either. Without + # this step they never run in CI. It shares the lib test binary with that step, + # so it costs a test run, not an extra compile. + - name: Run executor lib unit tests + run: | + cargo test --release -p executor --lib + - name: Run ignored executor tests run: | cargo test --release -p executor test_ckzg -- --ignored diff --git a/Cargo.lock b/Cargo.lock index bcee4a74b..2868f3e1b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -585,6 +585,7 @@ version = "0.1.0" dependencies = [ "ecsm", "k256", + "lambda-vm-syscalls", "rustc-demangle", "serde", "serde_json", diff --git a/crypto/ethrex-crypto/src/lib.rs b/crypto/ethrex-crypto/src/lib.rs index 702416ea6..ec36b0831 100644 --- a/crypto/ethrex-crypto/src/lib.rs +++ b/crypto/ethrex-crypto/src/lib.rs @@ -196,9 +196,12 @@ where let mut y: FieldElement = Option::from(FieldElement::from_bytes(&y_be.into()))?; let y2: FieldElement = y.square(); // Verify the untrusted root: y² must equal x³+7. Negate `y2`, not `rhs`: - // `Neg` is `negate(1)` and only accepts magnitude 1, which `square()` always - // returns, whereas `rhs` is a sum and carries magnitude 2 — negating it would - // silently compute the wrong value in release, where the debug assert is gone. + // `Neg` is `negate(1)`, whose debug assert requires magnitude <= 1. `square()` + // always returns magnitude 1, whereas `rhs` is a sum carrying magnitude 2, so + // negating it would trip that assert and panic in debug builds. (The value would + // still come out right — `negate(m)` computes `2*(m+1)*P_limb - self`, which for a + // magnitude-2 operand stays non-negative — so this is a build-configuration + // hazard, not a wrong answer.) // (`ct_eq` is unusable here for the same reason as in `field_inv`.) if !bool::from((rhs + y2.negate(1)).normalizes_to_zero()) { return None; diff --git a/crypto/ethrex-crypto/src/tests/hint_tests.rs b/crypto/ethrex-crypto/src/tests/hint_tests.rs index a7e992577..ace59f208 100644 --- a/crypto/ethrex-crypto/src/tests/hint_tests.rs +++ b/crypto/ethrex-crypto/src/tests/hint_tests.rs @@ -5,10 +5,12 @@ //! inverse / square root, then verifies it in-circuit. These tests inject the //! oracle directly — an *honest* oracle (matching the executor's `compute_hint`) //! and a *lying* one — and assert the software fallback makes the result identical -//! either way. That is the property C1 turns on: a bad hint can only make the guest -//! do more work, never change its accept/reject outcome. On the guest this code is -//! `cfg(target_arch = "riscv64")`; the `test` gate on `*_with_oracle` is what lets -//! CI compile and exercise it on the host. +//! either way. That is the property the whole hint design rests on: because the +//! prover chooses the hinted bytes and the ecall adds no correctness constraint, a +//! bad hint must only be able to make the guest do more work, never change its +//! accept/reject outcome. On the guest this code is `cfg(target_arch = "riscv64")`; +//! the `test` gate on `*_with_oracle` is what lets CI compile and exercise it on +//! the host. use crate::*; @@ -75,6 +77,26 @@ fn scalar_inv_lying_hint_falls_back_to_software() { } } +#[test] +fn scalar_inv_canonical_but_wrong_hint_falls_back_to_software() { + // The `[0; 32]` / `[0xFF; 32]` lies above both die in `Scalar::from_repr` — they + // never reach the verify predicate. These two are perfectly canonical scalars that + // simply aren't the inverse, so they exercise the rejecting branch of + // `(x * inv) == 1` itself, which is the check that actually has to hold. + for k in [1u64, 2, 12345] { + let x = Scalar::from(k); + let sw = x.invert_vartime().unwrap(); + for (name, lie) in [("inv + 1", sw + Scalar::ONE), ("-inv", -sw)] { + let lie_be: [u8; 32] = lie.to_bytes().into(); + let got = scalar_inv_with_oracle(&x, |_| lie_be).expect("fallback recomputes"); + assert_eq!( + got, sw, + "a canonical-but-wrong hint ({name}) must be rejected and recomputed (k={k})" + ); + } + } +} + #[test] fn decompress_r_honest_hint_matches_software() { // x-coordinates of real points are guaranteed residues. @@ -113,6 +135,39 @@ fn decompress_r_lying_hint_falls_back_to_software() { } } +/// Sqrt oracle returning the *other* root (`−y`). Not a lie: `−y` is as valid a root +/// of `x³+7` as `y`, so the in-guest verify accepts it and the software fallback +/// never runs — fixing the sign is entirely on the parity-selection branch. +fn negated_field_sqrt(rhs_be: &[u8; 32]) -> [u8; 32] { + let honest = honest_field_sqrt(rhs_be); + let y = Option::::from(FieldElement::from_bytes(&honest.into())) + .expect("the honest root is canonical"); + (-y).normalize().to_bytes().into() +} + +#[test] +fn decompress_r_negated_sqrt_hint_recovers_the_point() { + // The hinted root's parity is the host's choice — `compute_hint` returns whichever + // root k256's `sqrt()` picks, so the caller must not depend on it. With the honest + // oracle the parity branch fires only for the `k` values whose root happens to have + // the wrong parity; forcing the negation exercises the *other* half of the branch + // for every `k`. A `Some` here comes from the hinted path, not the fallback, so a + // broken parity fix would return `-P` and fail the comparison. + for k in [1u64, 2, 5, 12345] { + let p = (ProjectivePoint::GENERATOR * Scalar::from(k)).to_affine(); + let (x, y) = affine_xy(&p).unwrap(); + let rb = x.to_bytes(); + let y_is_odd = (y.normalize().to_bytes()[31] & 1) == 1; + let got = decompress_r_with_oracle(&rb, y_is_odd, negated_field_sqrt) + .expect("the other root is still a root"); + assert_eq!( + sec1(&got), + sec1(&p), + "a negated (but valid) root must still recover the point (k={k})" + ); + } +} + #[test] fn decompress_r_non_residue_is_none_regardless_of_hint() { // Find a small x whose x³+7 has no square root: R is genuinely undecompressable @@ -187,3 +242,29 @@ fn field_inv_lying_hint_falls_back_to_software() { } } } + +#[test] +fn field_inv_canonical_but_wrong_hint_falls_back_to_software() { + // As in the scalar case: the `[0; 32]` / `[0xFF; 32]` lies die in + // `FieldElement::from_bytes`, so they never reach the verify predicate. These two + // parse cleanly and are simply not the inverse, exercising the rejecting branch of + // `x·inv − 1 == 0` — the check the fast path's soundness actually rests on. + for k in [1u64, 2, 12345] { + let x = fe_from_u64(k); + let sw = Option::::from(x.invert()) + .unwrap() + .normalize(); + for (name, lie) in [ + ("inv + 1", (sw + FieldElement::ONE).normalize()), + ("-inv", -sw), + ] { + let lie_be: [u8; 32] = lie.normalize().to_bytes().into(); + let got = field_inv_with_oracle(&x, |_| lie_be).expect("fallback recomputes"); + assert_eq!( + got.normalize().to_bytes(), + sw.to_bytes(), + "a canonical-but-wrong hint ({name}) must be rejected and recomputed (k={k})" + ); + } + } +} diff --git a/executor/Cargo.toml b/executor/Cargo.toml index 924b1de66..91ae64ae9 100644 --- a/executor/Cargo.toml +++ b/executor/Cargo.toml @@ -14,6 +14,14 @@ ecsm = { path = "../crypto/ecsm" } k256 = { version = "0.13", default-features = false, features = ["arithmetic", "expose-field"] } [dev-dependencies] +# Test-only: the guest-side syscall crate re-declares the `hint` selectors as `usize` +# and they must stay equal to the `u64` copies here (see `hint_selectors_match_the_guest`). +# Unlike `crypto/crypto`'s and `ethrex-crypto`'s copies of this dep, it is NOT +# target-gated, so it does build on the host — safe because the only guest-only items +# (the `#[global_allocator]` and the `_start`/`main` entrypoint) are already +# `cfg(target_arch = "riscv64")` in that crate, and `executor::tests` is itself +# `#[cfg(test)]`, so the non-test lib build never links it. +lambda-vm-syscalls = { path = "../syscalls" } serde = { version = "1.0", features = ["derive"] } serde_json = "1.0" tiny-keccak = { version = "2.0", features = ["keccak"] } diff --git a/executor/programs/rust/hint_multi/src/main.rs b/executor/programs/rust/hint_multi/src/main.rs index 67f2ab90f..2a03a644d 100644 --- a/executor/programs/rust/hint_multi/src/main.rs +++ b/executor/programs/rust/hint_multi/src/main.rs @@ -1,13 +1,15 @@ -//! Multi-hint P0/P2 guest for the Hint prover table: THREE `hint` ecalls -//! (field inverse of three different small values), each result read back with -//! ordinary `LOAD`s (XOR-accumulated) and the accumulator committed. +//! Multi-hint P0/P2 guest for the Hint prover table: THREE `hint` ecalls, one per +//! selector, each result read back with ordinary `LOAD`s (XOR-accumulated) and the +//! accumulator committed. //! //! Complements `hint_min` (one hint, read back via `commit`): this exercises the //! parts the ethrex consumer relies on that a single-call guest does not — -//! **multiple real HINT rows** (padded to a power of two) and **read-back of the -//! hinted output via normal `LOAD` instructions** (whose MEMW reads must chain to -//! the HINT table's writes). Buffers are 8-byte aligned so the writes land in the -//! aligned MEMW table. +//! **multiple real HINT rows** (padded to a power of two), **all three selectors** +//! (`HINT_FIELD_INV` / `HINT_SCALAR_INV` / `HINT_FIELD_SQRT`, so the AIR's +//! `selector < 3` range-check is exercised at every accepted value rather than only +//! at 0) and **read-back of the hinted output via normal `LOAD` instructions** +//! (whose MEMW reads must chain to the HINT table's writes). Buffers are 8-byte +//! aligned so the writes land in the aligned MEMW table. use lambda_vm_syscalls as syscalls; @@ -17,17 +19,23 @@ struct Aligned32([u8; 32]); pub fn main() { let mut acc = Aligned32([0u8; 32]); - for seed in [3u8, 5u8, 7u8] { + // One call per selector. 4 is a quadratic residue mod p, so the sqrt hint has a + // real root rather than the zeros `compute_hint` returns on a numeric failure. + for (hint_id, seed) in [ + (syscalls::syscalls::HINT_FIELD_INV, 3u8), + (syscalls::syscalls::HINT_SCALAR_INV, 5u8), + (syscalls::syscalls::HINT_FIELD_SQRT, 4u8), + ] { let mut x = Aligned32([0u8; 32]); x.0[31] = seed; - let mut inv = Aligned32([0u8; 32]); + let mut out = Aligned32([0u8; 32]); - syscalls::syscalls::hint(syscalls::syscalls::HINT_FIELD_INV, &mut inv.0, &x.0); + syscalls::syscalls::hint(hint_id, &mut out.0, &x.0); // Read the hinted output back via ordinary loads and fold it in, so the - // MEMW reads of `inv` must chain to the HINT table's writes. + // MEMW reads of `out` must chain to the HINT table's writes. for i in 0..32 { - acc.0[i] ^= inv.0[i]; + acc.0[i] ^= out.0[i]; } } diff --git a/executor/src/tests/hint_tests.rs b/executor/src/tests/hint_tests.rs index f32f25aea..2ed8c096c 100644 --- a/executor/src/tests/hint_tests.rs +++ b/executor/src/tests/hint_tests.rs @@ -165,3 +165,32 @@ fn hint_syscall_rejects_an_unknown_selector() { ); } } + +/// The guest's `lambda-vm-syscalls` crate re-declares the selectors as `usize`, +/// linked to the `u64` copies here only by a comment. A divergence is **silent**: +/// the ecall would trap on an unknown selector, or — worse for the selectors that +/// stay in range — hand back 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 ~2000× slower for the right result. +/// This test is the only thing that would notice. +/// +/// `is_valid_hint_selector`'s const-assert pins the AIR's range-check to this crate's +/// accepted set, but nothing ties the *guest's* copy of the selectors to it — that is +/// a third declaration, in a crate the workspace excludes, and this is what binds it. +/// +/// The syscall number itself is not asserted here: the guest's copy is +/// `#[cfg(target_arch = "riscv64")]` and private, so it does not exist in a host +/// build. It is covered indirectly — a wrong number makes every `hint` guest fail +/// to prove, which `test_prove_hint_min_rust_guest` catches loudly. +#[cfg(test)] +mod guest_constant_sync { + use super::{HINT_FIELD_INV, HINT_FIELD_SQRT, HINT_SCALAR_INV}; + use lambda_vm_syscalls::syscalls as guest; + + #[test] + fn hint_selectors_match_the_guest() { + assert_eq!(guest::HINT_FIELD_INV as u64, HINT_FIELD_INV); + assert_eq!(guest::HINT_SCALAR_INV as u64, HINT_SCALAR_INV); + assert_eq!(guest::HINT_FIELD_SQRT as u64, HINT_FIELD_SQRT); + } +} diff --git a/prover/src/tables/hint.rs b/prover/src/tables/hint.rs index 25a0565d8..cb1dab9f3 100644 --- a/prover/src/tables/hint.rs +++ b/prover/src/tables/hint.rs @@ -356,12 +356,12 @@ pub fn bus_interactions() -> Vec { /// The HINT table's single transition constraint: `mu·(1−mu) = 0`. /// /// `mu` is the multiplicity gating every one of this table's bus interactions -/// (the `Ecall` receive, the `x12` register read, the four output writes, the -/// 16 byte range-checks). It must be boolean, or a witness could put a non-`{0,1}` -/// value on the `AreBytes`/MEMW sends. The LogUp argument already fixes `mu`'s value -/// via the timestamp-unique `Ecall` tuple, but every other multiplicity-column table -/// bit-constrains its column in-circuit; HINT does the same rather than being the -/// lone exception that relies solely on bus balance. +/// (the `Ecall` receive, the three register reads, the three `LT` range-checks, the +/// four output writes, the 16 byte range-checks). It must be boolean, or a witness +/// could put a non-`{0,1}` value on the `AreBytes`/MEMW sends. This is load-bearing, +/// not a redundant restatement of a bus check: the `Ecall` bus pins only the *sum* +/// of `mu` over the rows sharing a tuple — see the module-level docs for the +/// spread-multiplicity witness it rules out. #[derive(Clone, Copy)] pub struct HintConstraints; diff --git a/prover/src/test_utils.rs b/prover/src/test_utils.rs index 8d7960980..d6a8b8608 100644 --- a/prover/src/test_utils.rs +++ b/prover/src/test_utils.rs @@ -897,9 +897,10 @@ pub fn create_halt_air(proof_options: &ProofOptions) -> ConcreteVmAir ConcreteVmAir { build_air( hint_cols::NUM_COLUMNS, diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index c120650f5..b91ab8eff 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -1212,10 +1212,11 @@ fn test_prove_ecsm_rust_guest() { /// End-to-end prove→verify for the non-constraining `Hint` ecall: the minimal Rust /// guest does one `hint` call (secp256k1 base-field inverse of 3) and commits the result. -/// This exercises exactly the HINT table's bus surface (Ecall receive + the four -/// 8-byte output MEMW writes) end-to-end through prove→verify, de-risking the bus -/// balance before scaling to real consumers. The committed output must equal the -/// value the executor's `compute_hint` produced (= 3^{-1} mod p). +/// This exercises the whole HINT table bus surface (Ecall receive, the x10/x11/x12 +/// register reads, the two ALU `LT` operand range-checks, the four 8-byte output MEMW +/// writes and the output byte range-checks) end-to-end through prove→verify, de-risking +/// the bus balance before scaling to real consumers. The committed output must equal +/// the value the executor's `compute_hint` produced (= 3^{-1} mod p). #[test] fn test_prove_hint_min_rust_guest() { let _ = env_logger::builder().is_test(true).try_init(); @@ -1242,11 +1243,13 @@ fn test_prove_hint_min_rust_guest() { assert_eq!(proof.public_output, expected.to_vec()); } -/// Multi-hint: three `hint` ecalls, each result read back with +/// Multi-hint: three `hint` ecalls, one per selector, each result read back with /// ordinary `LOAD`s. Complements `test_prove_hint_min_rust_guest` by proving the /// paths the ethrex consumer relies on that a single-call guest doesn't: **multiple -/// real HINT rows** (padded) and **read-back via normal LOAD** (MEMW reads chaining -/// to the HINT writes). Committed output = XOR of the three field inverses. +/// real HINT rows** (padded), **all three selectors** (so the AIR's `selector < 3` +/// range-check is exercised at every accepted value, not only at 0) and **read-back +/// via normal LOAD** (MEMW reads chaining to the HINT writes). Committed output = +/// XOR of the three hinted values. #[test] fn test_prove_hint_multi_rust_guest() { let _ = env_logger::builder().is_test(true).try_init(); @@ -1265,15 +1268,22 @@ fn test_prove_hint_multi_rust_guest() { "hint_multi rust guest should verify" ); - // Expected = XOR of field-inverses of 3, 5, 7 (32-byte BE), matching the guest. + // Expected = XOR of inv(3) mod p, inv(5) mod n and sqrt(4) mod p (32-byte BE), + // matching the guest's one-call-per-selector loop. + use executor::vm::instruction::execution::{ + HINT_FIELD_INV, HINT_FIELD_SQRT, HINT_SCALAR_INV, compute_hint, + }; let mut expected = [0u8; 32]; - for seed in [3u8, 5u8, 7u8] { + for (hint_id, seed) in [ + (HINT_FIELD_INV, 3u8), + (HINT_SCALAR_INV, 5u8), + (HINT_FIELD_SQRT, 4u8), + ] { let mut input = [0u8; 32]; input[31] = seed; - let inv = - executor::vm::instruction::execution::compute_hint(0 /* HINT_FIELD_INV */, &input); + let out = compute_hint(hint_id, &input); for i in 0..32 { - expected[i] ^= inv[i]; + expected[i] ^= out[i]; } } assert_eq!(proof.public_output, expected.to_vec());