diff --git a/crypto/crypto/src/field_ext.rs b/crypto/crypto/src/field_ext.rs new file mode 100644 index 000000000..b12dd9e5e --- /dev/null +++ b/crypto/crypto/src/field_ext.rs @@ -0,0 +1,233 @@ +//! Field-extension multiply-add backend: `a*b + c`. +//! +//! Software by default (host, and every non-accelerated field). On the riscv64 +//! guest the native degree-3 Goldilocks extension routes through the FEXT +//! precompile, so the in-VM STARK verifier's Fp3 multiplies run on the +//! accelerator instead of the software schoolbook. Mirrors the host/guest split +//! of [`crate::hash::platform_keccak`]. +//! +//! The trait carries software defaults, so the generic verifier can call +//! `FieldExtension::fma(..)` / `ext_mul(..)` unconditionally: on host (and any +//! non-Fp3 field) it is the plain arithmetic; on the guest the Fp3 impl +//! overrides it. The two impls live under mutually exclusive `cfg`s, so there is +//! never an overlap (no `specialization` needed — the host builds on stable). + +use math::field::element::FieldElement; +use math::field::traits::IsField; + +/// `a*b + c` over a field extension. Default is software; accelerated fields +/// override on targets where an accelerator exists. +pub trait Fp3Fma: IsField + Sized { + /// Fused multiply-add: `a * b + c`. + #[inline(always)] + fn fma( + a: &FieldElement, + b: &FieldElement, + c: &FieldElement, + ) -> FieldElement { + a * b + c + } + + /// Extension multiply: `a * b`. + #[inline(always)] + fn ext_mul(a: &FieldElement, b: &FieldElement) -> FieldElement { + a * b + } + + /// A resident accumulator for `acc += a*b*c` chains. On the accelerated + /// guest it lives in field-storage across the chain (operands loaded, the + /// accumulator never stored/reloaded mid-chain), removing the per-op + /// LOAD/STORE roundtrip of [`Fp3Fma::fma`]. On host it is a plain field + /// element. + type ProdAcc; + + /// A fresh zero accumulator. + fn prod_acc_new() -> Self::ProdAcc; + + /// `acc += a * b * c`. + fn prod_acc_add( + acc: &mut Self::ProdAcc, + a: &FieldElement, + b: &FieldElement, + c: &FieldElement, + ); + + /// Materialize the accumulator as a field element. + fn prod_acc_finish(acc: Self::ProdAcc) -> FieldElement; +} + +#[cfg(not(target_arch = "riscv64"))] +mod imp { + use super::Fp3Fma; + use math::field::element::FieldElement; + use math::field::traits::IsField; + + impl Fp3Fma for E { + type ProdAcc = FieldElement; + + fn prod_acc_new() -> FieldElement { + FieldElement::zero() + } + + fn prod_acc_add( + acc: &mut FieldElement, + a: &FieldElement, + b: &FieldElement, + c: &FieldElement, + ) { + *acc = &*acc + &(a * b * c); + } + + fn prod_acc_finish(acc: FieldElement) -> FieldElement { + acc + } + } +} + +#[cfg(target_arch = "riscv64")] +mod imp { + use super::Fp3Fma; + use lambda_vm_syscalls::syscalls::{fext_fma, fext_load, fext_store}; + use math::field::element::FieldElement; + use math::field::extensions_goldilocks::Degree3GoldilocksExtensionField; + use math::field::goldilocks::GoldilocksElement; + + // Verifier-scratch field-storage handles, in a reserved high range no guest + // picks for its own field-storage. FMA requires `out/a/b/c` pairwise + // distinct; `H_ZERO` is never written, so it reads as the zero element. + const BASE: u64 = 0xFFFF_0000_0000_0000; + const H_A: u64 = BASE; + const H_B: u64 = BASE + 1; + const H_C: u64 = BASE + 2; + const H_OUT: u64 = BASE + 3; + const H_ZERO: u64 = BASE + 4; + // ProdAcc scratch: `H_T` holds `a*b`; the accumulator ping-pongs between + // `H_ACC0`/`H_ACC1` so every emitted FMA has `out != c` (the executor's + // pairwise-distinct guard forbids in-place accumulation). + const H_T: u64 = BASE + 5; + const H_ACC0: u64 = BASE + 6; + const H_ACC1: u64 = BASE + 7; + + type Fp3 = Degree3GoldilocksExtensionField; + + #[inline] + fn coeffs(x: &FieldElement) -> [u64; 3] { + let v = x.value(); + [ + v[0].canonical_u64(), + v[1].canonical_u64(), + v[2].canonical_u64(), + ] + } + + #[inline] + fn from_coeffs(c: [u64; 3]) -> FieldElement { + FieldElement::from_raw([ + GoldilocksElement::from_raw(c[0]), + GoldilocksElement::from_raw(c[1]), + GoldilocksElement::from_raw(c[2]), + ]) + } + + impl Fp3Fma for Fp3 { + fn fma( + a: &FieldElement, + b: &FieldElement, + c: &FieldElement, + ) -> FieldElement { + fext_load(H_A, &coeffs(a)); + fext_load(H_B, &coeffs(b)); + fext_load(H_C, &coeffs(c)); + fext_fma(H_A, H_B, H_C, H_OUT); + from_coeffs(fext_store(H_OUT)) + } + + fn ext_mul(a: &FieldElement, b: &FieldElement) -> FieldElement { + fext_load(H_A, &coeffs(a)); + fext_load(H_B, &coeffs(b)); + fext_fma(H_A, H_B, H_ZERO, H_OUT); + from_coeffs(fext_store(H_OUT)) + } + + type ProdAcc = super::GuestAcc; + + fn prod_acc_new() -> super::GuestAcc { + // Zero the starting handle: it may hold a stale value from a + // previous chain (uninitialized-reads-as-zero doesn't apply here). + fext_load(H_ACC0, &[0, 0, 0]); + super::GuestAcc { buf: 0 } + } + + fn prod_acc_add( + acc: &mut super::GuestAcc, + a: &FieldElement, + b: &FieldElement, + c: &FieldElement, + ) { + fext_load(H_A, &coeffs(a)); + fext_load(H_B, &coeffs(b)); + fext_load(H_C, &coeffs(c)); + // tmp = a * b + fext_fma(H_A, H_B, H_ZERO, H_T); + let (cur, alt) = if acc.buf == 0 { + (H_ACC0, H_ACC1) + } else { + (H_ACC1, H_ACC0) + }; + // alt = tmp * c + cur (out=alt != c=cur, satisfies the guard) + fext_fma(H_T, H_C, cur, alt); + acc.buf ^= 1; + } + + fn prod_acc_finish(acc: super::GuestAcc) -> FieldElement { + let cur = if acc.buf == 0 { H_ACC0 } else { H_ACC1 }; + from_coeffs(fext_store(cur)) + } + } +} + +/// Guest resident-accumulator state: which of the two double-buffer handles +/// currently holds the running `acc += a*b*c` value. (`buf` stays private; only +/// this module's guest impl constructs and reads it.) +#[cfg(target_arch = "riscv64")] +pub struct GuestAcc { + buf: u8, +} + +#[cfg(test)] +mod tests { + use super::Fp3Fma; + use math::field::element::FieldElement; + use math::field::extensions_goldilocks::Degree3GoldilocksExtensionField as Fp3F; + use math::field::goldilocks::GoldilocksElement; + + type Fp3 = FieldElement; + + fn e(x: [u64; 3]) -> Fp3 { + Fp3::from_raw([ + GoldilocksElement::from(x[0]), + GoldilocksElement::from(x[1]), + GoldilocksElement::from(x[2]), + ]) + } + + /// `fma`/`ext_mul` must equal the plain field arithmetic they replace. On + /// host this exercises the software default (which also runs for every + /// non-Fp3 field); the guest FEXT impl is covered by the executor's + /// `fext_fma` tests and the recursion prove/verify E2E. + #[test] + fn fma_and_ext_mul_match_field_arithmetic() { + let cases = [ + ([1u64, 2, 3], [4u64, 5, 6], [7u64, 8, 9]), + ([0, 0, 0], [9, 9, 9], [1, 2, 3]), + ([u64::MAX - 1, 0, 5], [2, 3, 4], [0, 0, 0]), + ([10, 20, 30], [10, 20, 30], [5, 5, 5]), + ([123456789, 987654321, 555], [1, 0, 0], [0, 1, 0]), + ]; + for (a, b, c) in cases { + let (a, b, c) = (e(a), e(b), e(c)); + assert_eq!(Fp3F::fma(&a, &b, &c), &a * &b + &c); + assert_eq!(Fp3F::ext_mul(&a, &b), &a * &b); + } + } +} diff --git a/crypto/crypto/src/lib.rs b/crypto/crypto/src/lib.rs index d7a273d62..a088d1ff4 100644 --- a/crypto/crypto/src/lib.rs +++ b/crypto/crypto/src/lib.rs @@ -8,6 +8,7 @@ compile_error!("the `disk-spill` feature requires memmap2, which does not compil extern crate alloc; pub mod fiat_shamir; +pub mod field_ext; pub mod hash; pub mod merkle_tree; #[cfg(feature = "disk-spill")] diff --git a/crypto/stark/src/verifier.rs b/crypto/stark/src/verifier.rs index f78bf6e34..eabcfba78 100644 --- a/crypto/stark/src/verifier.rs +++ b/crypto/stark/src/verifier.rs @@ -16,6 +16,7 @@ use crate::{ }, }; use crypto::fiat_shamir::is_transcript::IsStarkTranscript; +use crypto::field_ext::Fp3Fma; use crypto::merkle_tree::proof::{verify_merkle_path, verify_merkle_path_from_leaf_hash}; #[cfg(not(feature = "test_fiat_shamir"))] use log::error; @@ -37,7 +38,7 @@ use std::time::Instant; /// A default STARK verifier implementing `IsStarkVerifier`. pub struct Verifier< Field: IsSubFieldOf + IsFFTField + Send + Sync, - FieldExtension: Send + Sync + IsField, + FieldExtension: Send + Sync + IsField + Fp3Fma, PI, > { phantom: PhantomData<(Field, FieldExtension, PI)>, @@ -45,7 +46,7 @@ pub struct Verifier< impl< Field: IsSubFieldOf + IsFFTField + Send + Sync, - FieldExtension: IsField + Send + Sync, + FieldExtension: IsField + Send + Sync + Fp3Fma, PI, > IsStarkVerifier for Verifier where @@ -117,7 +118,7 @@ compile_error!("the zero-copy STARK verifier requires a little-endian target"); /// downstream check — no serialization, no duplicated logic. pub trait IsStarkVerifier< Field: IsSubFieldOf + IsFFTField + Send + Sync, - FieldExtension: Send + Sync + IsField, + FieldExtension: Send + Sync + IsField + Fp3Fma, PI, > where Field::BaseType: math::field::element::NativeArchived, @@ -895,13 +896,31 @@ pub trait IsStarkVerifier< base_row_sum += base_at(col_idx) * coeff; base_row_sum_sym += base_at_sym(col_idx) * coeff; } else { + // Ext × ext products route through the FEXT accelerator on the + // guest (`fma` is `a*b + c`, identical to `+= a*b` on host). let aux_idx = col_idx - num_base; - base_row_sum += coeff * &lde_trace_aux_evaluations[aux_idx]; - base_row_sum_sym += coeff * &lde_trace_aux_evaluations_sym[aux_idx]; + base_row_sum = FieldExtension::fma( + &lde_trace_aux_evaluations[aux_idx], + coeff, + &base_row_sum, + ); + base_row_sum_sym = FieldExtension::fma( + &lde_trace_aux_evaluations_sym[aux_idx], + coeff, + &base_row_sum_sym, + ); } } - trace_term += &denoms_trace[row_idx] * &(&base_row_sum - ood_row_sum); - trace_term_sym += &denoms_trace_sym[row_idx] * &(&base_row_sum_sym - ood_row_sum); + trace_term = FieldExtension::fma( + &denoms_trace[row_idx], + &(&base_row_sum - ood_row_sum), + &trace_term, + ); + trace_term_sym = FieldExtension::fma( + &denoms_trace_sym[row_idx], + &(&base_row_sum_sym - ood_row_sum), + &trace_term_sym, + ); } let number_of_parts = query_invariant_terms.number_of_parts; diff --git a/executor/src/tests/fext_tests.rs b/executor/src/tests/fext_tests.rs index e5e68be3b..503783cba 100644 --- a/executor/src/tests/fext_tests.rs +++ b/executor/src/tests/fext_tests.rs @@ -187,3 +187,158 @@ fn fext_load_rejects_non_canonical_coefficient() { ); } } + +// Differential tests for the exact syscall sequences the in-guest STARK verifier +// emits through `crypto::field_ext::Fp3Fma` (`ext_mul` and the `prod_acc` +// resident accumulator). Those guest impls call `fext_load`/`fext_fma`/ +// `fext_store` and are `#[cfg(target_arch = "riscv64")]`, so they cannot run on +// host; here we replay the same handle choreography against the real executor +// and compare to a math-crate oracle. Keep these in sync with the sequences in +// `crypto/crypto/src/field_ext.rs`. + +// Handles mirror `field_ext.rs`; only pairwise distinctness and "H_ZERO is never +// loaded" (so it reads as the extension zero) actually matter here. +const H_A: u64 = 0; +const H_B: u64 = 1; +const H_C: u64 = 2; +const H_OUT: u64 = 3; +const H_ZERO: u64 = 4; +const H_T: u64 = 5; +const H_ACC0: u64 = 6; +const H_ACC1: u64 = 7; + +/// One `a*b*c` term of a `prod_acc` chain. +type ProdTerm = ([u64; 3], [u64; 3], [u64; 3]); + +/// Dependency-free deterministic SplitMix64, used to draw random canonical Fp3 +/// coefficients without pulling `rand` into dev-dependencies. +struct SplitMix64(u64); + +impl SplitMix64 { + fn next_u64(&mut self) -> u64 { + self.0 = self.0.wrapping_add(0x9E37_79B9_7F4A_7C15); + let mut z = self.0; + z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9); + z = (z ^ (z >> 27)).wrapping_mul(0x94D0_49BB_1331_11EB); + z ^ (z >> 31) + } + + /// Canonical (`< p`) coefficients, the only form `fext_load` accepts. + fn coeffs(&mut self) -> [u64; 3] { + [ + self.next_u64() % GOLDILOCKS_PRIME, + self.next_u64() % GOLDILOCKS_PRIME, + self.next_u64() % GOLDILOCKS_PRIME, + ] + } +} + +/// Independent reference for `sum_i a_i * b_i * c_i` over Fp3 (the value the +/// `prod_acc` chain computes). +fn reference_prod_sum(terms: &[ProdTerm]) -> [u64; 3] { + let to_fp3 = |x: [u64; 3]| { + Fp3::from_raw([ + GoldilocksElement::from(x[0]), + GoldilocksElement::from(x[1]), + GoldilocksElement::from(x[2]), + ]) + }; + let mut acc = Fp3::zero(); + for (a, b, c) in terms { + acc += to_fp3(*a) * to_fp3(*b) * to_fp3(*c); + } + let v = acc.value(); + [ + v[0].canonical_u64(), + v[1].canonical_u64(), + v[2].canonical_u64(), + ] +} + +/// Replays `Fp3Fma::prod_acc_{new,add,finish}` against the real executor and +/// returns the stored accumulator coefficients. +fn run_prod_acc_chain(terms: &[ProdTerm]) -> [u64; 3] { + let mut memory = Memory::default(); + // prod_acc_new: zero the starting buffer (it is written across chains). + run_load(&mut memory, H_ACC0, [0, 0, 0]).unwrap(); + let mut buf = 0u8; + for (a, b, c) in terms { + // prod_acc_add + run_load(&mut memory, H_A, *a).unwrap(); + run_load(&mut memory, H_B, *b).unwrap(); + run_load(&mut memory, H_C, *c).unwrap(); + run_fma(&mut memory, H_T, H_A, H_B, H_ZERO); // tmp = a * b + let (cur, alt) = if buf == 0 { + (H_ACC0, H_ACC1) + } else { + (H_ACC1, H_ACC0) + }; + run_fma(&mut memory, alt, H_T, H_C, cur); // alt = tmp * c + cur + buf ^= 1; + } + // prod_acc_finish + let cur = if buf == 0 { H_ACC0 } else { H_ACC1 }; + memory.field_load(cur) +} + +#[test] +fn fext_ext_mul_via_unwritten_zero_matches_reference() { + // Replays `Fp3Fma::ext_mul`: fma(a, b, H_ZERO) with H_ZERO never loaded, so + // the accumulator input reads as zero and the result is a*b. + let mut rng = SplitMix64(0xF00D_BEEF); + for _ in 0..100 { + let (a, b) = (rng.coeffs(), rng.coeffs()); + let mut memory = Memory::default(); + run_load(&mut memory, H_A, a).unwrap(); + run_load(&mut memory, H_B, b).unwrap(); + run_fma(&mut memory, H_OUT, H_A, H_B, H_ZERO); + assert_eq!( + memory.field_load(H_OUT), + reference_fma(a, b, [0, 0, 0]), + "a={a:?} b={b:?}" + ); + } +} + +#[test] +fn fext_prod_acc_chain_matches_reference() { + // Fixed chains covering the buffer-toggle boundaries: empty (finish reads the + // freshly zeroed H_ACC0), length 1 (ends on H_ACC1), length 2 (ends back on + // H_ACC0), length 3 (ends on H_ACC1), including a wrap-around coefficient. + let fixed: &[&[ProdTerm]] = &[ + &[], + &[([1, 2, 3], [4, 5, 6], [7, 8, 9])], + &[ + ([1, 2, 3], [4, 5, 6], [7, 8, 9]), + ([10, 0, 1], [0, 2, 0], [3, 3, 3]), + ], + &[ + ([1, 0, 0], [0, 1, 0], [0, 0, 1]), + ([2, 2, 2], [1, 1, 1], [9, 0, 9]), + ([GOLDILOCKS_PRIME - 1, 0, 0], [2, 0, 0], [1, 1, 1]), + ], + ]; + for terms in fixed { + assert_eq!( + run_prod_acc_chain(terms), + reference_prod_sum(terms), + "fixed chain len {}", + terms.len() + ); + } + + // Random chains of varying length exercise both toggle directions broadly. + let mut rng = SplitMix64(0x1234_5678); + for len in 0..=6usize { + for _ in 0..20 { + let terms: Vec<_> = (0..len) + .map(|_| (rng.coeffs(), rng.coeffs(), rng.coeffs())) + .collect(); + assert_eq!( + run_prod_acc_chain(&terms), + reference_prod_sum(&terms), + "random chain len {len}" + ); + } + } +} diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index 2e5c56a8b..c5263a811 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -67,6 +67,10 @@ use crate::tables::register; use crate::tables::trace_builder::{Traces, build_init_page_data, build_initial_image_paged}; use crate::tables::types::{GoldilocksExtension, GoldilocksField}; use crate::tables::{MaxRowsConfig, global_memory}; +use crate::test_utils::{ + create_fext_fma_air_forbidden, create_fext_load_air_forbidden, create_fext_page_air_forbidden, + create_fext_store_air_forbidden, +}; use crate::{ Error, FIXED_TABLE_COUNT, RuntimePageRange, TableCounts, VmAirs, compute_expected_commit_bus_balance, verify_l2g_commitment_binding, @@ -421,7 +425,7 @@ fn build_epoch_airs( register::compute_precomputed_commitment_with_fini(opts, register_init, reg_fini), register::NUM_PREPROCESSED_COLS_WITH_FINI, )); - VmAirs::new( + let mut airs = VmAirs::new( elf, opts, false, @@ -432,7 +436,17 @@ fn build_epoch_airs( None, None, register_preprocessed, - ) + ); + // Continuation disallows the FEXT accelerator: field-storage is not carried + // across epochs, so a value written in one epoch would read back as zero in + // the next. Force the four FEXT tables empty (μ = 0) at the AIR level so the + // *verifier* rejects any continuation proof that uses them — the prover-side + // guard in `build_traces` does not bind a malicious prover. + airs.fext_load = Box::new(create_fext_load_air_forbidden(opts)); + airs.fext_fma = Box::new(create_fext_fma_air_forbidden(opts)); + airs.fext_store = Box::new(create_fext_store_air_forbidden(opts)); + airs.fext_page = Box::new(create_fext_page_air_forbidden(opts)); + airs } /// Prove one epoch (prove half only). Commits its local-to-global table (built from diff --git a/prover/src/tables/fext_page.rs b/prover/src/tables/fext_page.rs index 862cffa92..d12f12dd0 100644 --- a/prover/src/tables/fext_page.rs +++ b/prover/src/tables/fext_page.rs @@ -289,6 +289,12 @@ impl ConstraintSet for FextPageConstraints let na1 = b.main(0, cols::NEXT_ADDR_1); let addr1_next = b.main(1, cols::ADDR_1); b.emit_base_rows(10, tr, na1 - addr1_next); + + // sel_same is a bit on EVERY row, including the last (whose definition, + // idx 6, is exempt). Without this a prover could set the addr-LT + // multiplicity to -1 on the last row and cancel an invalid `addr < next` + // lookup elsewhere, re-introducing duplicate (domain, addr) keys. + emit_is_bit(b, 11, cols::SEL_SAME, None); } fn max_degree(&self) -> usize { diff --git a/prover/src/test_utils.rs b/prover/src/test_utils.rs index 5f838cc37..50950c805 100644 --- a/prover/src/test_utils.rs +++ b/prover/src/test_utils.rs @@ -19,7 +19,7 @@ use executor::vm::instruction::decoding::Instruction; use executor::vm::logs::Log; use executor::vm::memory::U64HashMap; use math::field::element::FieldElement; -use stark::constraints::builder::{ConstraintSet, EmptyConstraints}; +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet, EmptyConstraints}; use stark::debug::validate_trace; use stark::domain::Domain; use stark::lookup::{ @@ -1007,3 +1007,90 @@ pub fn create_fext_page_air(proof_options: &ProofOptions) -> ConcreteVmAir { + pub base: C, + pub mu_col: usize, +} + +impl> ConstraintSet for ForbidEmpty { + fn eval>(&self, b: &mut B) { + self.base.eval(b); + let mu0_idx = self.base.meta().len(); + let mu = b.main(0, self.mu_col); + b.emit_base(mu0_idx, mu); + } + + fn max_degree(&self) -> usize { + self.base.max_degree() + } +} + +pub fn create_fext_load_air_forbidden( + proof_options: &ProofOptions, +) -> ConcreteVmAir> { + build_air( + fext_load_cols::NUM_COLUMNS, + fext_load_bus_interactions(), + proof_options, + 1, + ForbidEmpty { + base: FextLoadConstraints, + mu_col: fext_load_cols::MU, + }, + "FEXT_LOAD", + ) +} + +pub fn create_fext_fma_air_forbidden( + proof_options: &ProofOptions, +) -> ConcreteVmAir> { + build_air( + fext_fma_cols::NUM_COLUMNS, + fext_fma_bus_interactions(), + proof_options, + 1, + ForbidEmpty { + base: FextFmaConstraints, + mu_col: fext_fma_cols::MU, + }, + "FEXT_FMA", + ) +} + +pub fn create_fext_store_air_forbidden( + proof_options: &ProofOptions, +) -> ConcreteVmAir> { + build_air( + fext_store_cols::NUM_COLUMNS, + fext_store_bus_interactions(), + proof_options, + 1, + ForbidEmpty { + base: FextStoreConstraints, + mu_col: fext_store_cols::MU, + }, + "FEXT_STORE", + ) +} + +pub fn create_fext_page_air_forbidden( + proof_options: &ProofOptions, +) -> ConcreteVmAir> { + build_air( + fext_page_cols::NUM_COLUMNS, + fext_page_bus_interactions(), + proof_options, + 1, + ForbidEmpty { + base: FextPageConstraints, + mu_col: fext_page_cols::MU, + }, + "FEXT_PAGE", + ) +} diff --git a/prover/src/tests/fext_page_tests.rs b/prover/src/tests/fext_page_tests.rs index 726689528..fa87a6021 100644 --- a/prover/src/tests/fext_page_tests.rs +++ b/prover/src/tests/fext_page_tests.rs @@ -51,8 +51,8 @@ fn op(domain: u64, addr: u64) -> FextPageOperation { fn fext_page_constraint_and_bus_counts() { // IS_BIT(μ), domain ∈ {3,4,5}, IS_BIT(same_dom), 2 addr recompose, // μ non-increasing, sel_same def, same-domain⇒equal, domain-increase, - // 2 next-addr copies = 11. - assert_eq!(FextPageConstraints.meta().len(), 11); + // 2 next-addr copies, IS_BIT(sel_same) = 12. + assert_eq!(FextPageConstraints.meta().len(), 12); // init receiver + fini sender + addr LT + 4 IsHalfword = 7. assert_eq!(bus_interactions().len(), 7); } @@ -203,3 +203,56 @@ fn fext_page_rejects_forged_next_addr() { .set_fe(0, cols::NEXT_ADDR_0, FE::from(0x999u64)); assert_ne!(eval_transition(&trace, 0)[9], FE::zero()); } + +#[test] +fn fext_page_forbid_empty_rejects_active_row() { + // The continuation variant (ForbidEmpty) adds one `μ = 0` constraint, forcing + // the table empty so the verifier rejects any FEXT use under continuation. + use crate::test_utils::ForbidEmpty; + let forbidden = ForbidEmpty { + base: FextPageConstraints, + mu_col: cols::MU, + }; + let n = forbidden.meta().len(); + assert_eq!(n, FextPageConstraints.meta().len() + 1); // one extra: μ = 0 + + // An active row (μ = 1) violates the added μ = 0 constraint (last index). + let trace = generate_fext_page_trace(&[op(3, 0x10)]); + let main: Vec = (0..cols::NUM_COLUMNS) + .map(|c| *trace.main_table.get(0, c)) + .collect(); + let frame = Frame::::new(vec![ + TableView::new(vec![main.clone()], vec![vec![]]), + TableView::new(vec![main], vec![vec![]]), + ]); + let no_e: Vec> = vec![]; + let offset_e = FieldElement::::zero(); + let ctx = + TransitionEvaluationContext::new_prover(frame.as_row_frame(), &no_e, &no_e, &offset_e); + let mut base = vec![FE::zero(); n]; + let mut ext = vec![FieldElement::::zero(); n]; + let mut folder = ProverEvalFolder::new(&ctx, &mut base, &mut ext); + forbidden.eval(&mut folder); + assert_eq!(base[n - 1], FE::one()); // μ = 1 on the active row +} + +#[test] +fn fext_page_rejects_non_bit_sel_same() { + // sel_same is the addr-LT multiplicity; a non-bit value (e.g. -1) would let a + // prover cancel an invalid `addr < next` lookup and re-introduce duplicate + // keys. IS_BIT(sel_same) (idx 11) must reject it on any row. + let mut trace = generate_fext_page_trace(&[op(3, 0x10), op(3, 0x20)]); + trace.main_table.set_fe(0, cols::SEL_SAME, FE::from(2u64)); + assert_ne!(eval_transition(&trace, 0)[11], FE::zero()); + + // The exact attack surface is the LAST row, whose sel_same definition (idx 6) + // is exempt; IS_BIT still pins it. Force sel_same = -1 there and check idx 11. + let last = trace.num_rows() - 1; + let mut trace2 = generate_fext_page_trace(&[op(3, 0x10), op(3, 0x20)]); + trace2.main_table.set_fe(last, cols::SEL_SAME, -FE::one()); + let main: Vec = (0..cols::NUM_COLUMNS) + .map(|c| *trace2.main_table.get(last, c)) + .collect(); + let sel = main[cols::SEL_SAME]; + assert_ne!(sel * (FE::one() - sel), FE::zero()); // (-1)·2 = -2 ≠ 0 +}