Review follow-ups for #876: the CI gap, three stale soundness comments, and three test gaps

.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 <name>` 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

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;

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::<FieldElement>::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::<FieldElement>::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})"
+            );
+        }
+    }
+}

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"] }

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];
         }
     }
 

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);
+    }
+}

prover/src/tables/hint.rs

@@ -356,12 +356,12 @@ pub fn bus_interactions() -> Vec<BusInteraction> {
 /// 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;
 

prover/src/test_utils.rs

@@ -897,9 +897,10 @@ pub fn create_halt_air(proof_options: &ProofOptions) -> ConcreteVmAir<EmptyConst
     )
 }
 
-/// Create HINT AIR: a receiver for the `hint` ecall (Ecall receive, x12 register
-/// read, four output MEMW writes, output byte range-checks) with a single boolean
-/// constraint on the multiplicity column `mu`.
+/// Create HINT AIR: a receiver for the `hint` ecall (Ecall receive, the x10/x11/x12
+/// register reads, the three ALU `LT` operand range-checks, four output MEMW writes,
+/// output byte range-checks) with a single boolean constraint on the multiplicity
+/// column `mu`.
 pub fn create_hint_air(proof_options: &ProofOptions) -> ConcreteVmAir<HintConstraints> {
     build_air(
         hint_cols::NUM_COLUMNS,

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());