diff --git a/Cargo.lock b/Cargo.lock index 74986dcc9..b7d023ffa 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -584,6 +584,7 @@ name = "executor" version = "0.1.0" dependencies = [ "ecsm", + "math", "rustc-demangle", "serde", "serde_json", diff --git a/bin/cli/src/main.rs b/bin/cli/src/main.rs index 1de36220b..0a8a6985e 100644 --- a/bin/cli/src/main.rs +++ b/bin/cli/src/main.rs @@ -412,7 +412,7 @@ fn cmd_execute( // below (the flamegraph path drives execution inside the executor and does // not expose per-log data). `None` means "not counted", so the accel lines // are omitted rather than printed as misleading zeros. - let mut accel_counts: Option<(u64, u64)> = None; + let mut accel_counts: Option<(u64, u64, u64, u64, u64)> = None; let cycle_count = if let Some(ref output_path) = flamegraph.path { // Shared execute+flamegraph path (executor::flamegraph) instead of @@ -480,6 +480,9 @@ fn cmd_execute( let mut cycle_count: u64 = 0; let mut keccak_calls: u64 = 0; let mut ecsm_calls: u64 = 0; + let mut fext_load_calls: u64 = 0; + let mut fext_fma_calls: u64 = 0; + let mut fext_store_calls: u64 = 0; // Reused per chunk: `(current_pc, a7)` for logs whose a7 matches an // accelerator syscall number. This is a cheap superset — a non-ECALL // instruction can hold the same value in src1 — that `accelerator_of` @@ -512,6 +515,9 @@ fn cmd_execute( match accelerator_of(executor.instructions.get(pc), a7) { Some(Accelerator::Keccak) => keccak_calls += 1, Some(Accelerator::Ecsm) => ecsm_calls += 1, + Some(Accelerator::FextLoad) => fext_load_calls += 1, + Some(Accelerator::FextFma) => fext_fma_calls += 1, + Some(Accelerator::FextStore) => fext_store_calls += 1, None => {} } } @@ -526,16 +532,27 @@ fn cmd_execute( } if cycles { - accel_counts = Some((keccak_calls, ecsm_calls)); + accel_counts = Some(( + keccak_calls, + ecsm_calls, + fext_load_calls, + fext_fma_calls, + fext_store_calls, + )); } cycle_count }; if cycles { println!("Cycles: {}", cycle_count); - if let Some((keccak_calls, ecsm_calls)) = accel_counts { + if let Some((keccak_calls, ecsm_calls, fext_load_calls, fext_fma_calls, fext_store_calls)) = + accel_counts + { println!("Keccak calls: {}", keccak_calls); println!("Ecsm calls: {}", ecsm_calls); + println!("Fext load calls: {}", fext_load_calls); + println!("Fext fma calls: {}", fext_fma_calls); + println!("Fext store calls: {}", fext_store_calls); } } diff --git a/crypto/crypto/src/field_ext.rs b/crypto/crypto/src/field_ext.rs new file mode 100644 index 000000000..5c1de788d --- /dev/null +++ b/crypto/crypto/src/field_ext.rs @@ -0,0 +1,317 @@ +//! 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; + + /// A fresh zero two-way resident accumulator for `acc += a*b` folds. `slot` + /// picks one of a fixed set of independent accumulators (the guest keeps each + /// in its own field-storage handle pair) so several folds can run at once — + /// e.g. the regular and symmetric row sums of a DEEP query. Callers must keep + /// distinct live accumulators on distinct slots and not exceed the guest's + /// slot count; host ignores `slot`. Materialize with `prod_acc_finish`. + fn mul_acc_new(slot: u8) -> Self::ProdAcc; + + /// `acc += a * b`. Like `prod_acc_add` but without the third factor: on the + /// guest it is a single FMA into the resident accumulator (no `a*b` temp), + /// matching the `fma(a, b, acc)` folds the verifier runs over trace columns. + fn mul_acc_add(acc: &mut Self::ProdAcc, a: &FieldElement, b: &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 + } + + fn mul_acc_new(_slot: u8) -> FieldElement { + FieldElement::zero() + } + + fn mul_acc_add(acc: &mut FieldElement, a: &FieldElement, b: &FieldElement) { + *acc = &*acc + &(a * b); + } + } +} + +#[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; + // Resident-accumulator handle pairs, one per slot: slot `s` owns + // `(ACC_BASE + 2s, ACC_BASE + 2s + 1)` and ping-pongs between them so every + // emitted FMA has `out != c`. `MAX_SLOTS` independent accumulators can be + // live at once (e.g. the regular and symmetric DEEP row sums). + const ACC_BASE: u64 = BASE + 6; + const MAX_SLOTS: u8 = 4; + + #[inline] + fn acc_pair(slot: u8) -> (u64, u64) { + debug_assert!(slot < MAX_SLOTS); + let lo = ACC_BASE + 2 * slot as u64; + (lo, lo + 1) + } + + 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). + let (lo, _) = acc_pair(0); + fext_load(lo, &[0, 0, 0]); + super::GuestAcc { buf: 0, slot: 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 (lo, hi) = acc_pair(acc.slot); + let (cur, alt) = if acc.buf == 0 { (lo, hi) } else { (hi, lo) }; + // 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 (lo, hi) = acc_pair(acc.slot); + let cur = if acc.buf == 0 { lo } else { hi }; + from_coeffs(fext_store(cur)) + } + + fn mul_acc_new(slot: u8) -> super::GuestAcc { + let (lo, _) = acc_pair(slot); + fext_load(lo, &[0, 0, 0]); + super::GuestAcc { buf: 0, slot } + } + + fn mul_acc_add(acc: &mut super::GuestAcc, a: &FieldElement, b: &FieldElement) { + fext_load(H_A, &coeffs(a)); + fext_load(H_B, &coeffs(b)); + let (lo, hi) = acc_pair(acc.slot); + let (cur, alt) = if acc.buf == 0 { (lo, hi) } else { (hi, lo) }; + // alt = a * b + cur (out=alt != c=cur, satisfies the guard) + fext_fma(H_A, H_B, cur, alt); + acc.buf ^= 1; + } + } +} + +/// Guest resident-accumulator state: `slot` selects the handle pair, `buf` +/// selects which of that pair currently holds the running value. (Both stay +/// private; only this module's guest impl constructs and reads them.) +#[cfg(target_arch = "riscv64")] +pub struct GuestAcc { + buf: u8, + slot: 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); + } + } + + /// The resident accumulators must fold to the same value as the plain sums + /// they replace: `prod_acc` to `Σ aᵢ·bᵢ·cᵢ`, `mul_acc` to `Σ aᵢ·bᵢ`. Two + /// `mul_acc` chains on distinct slots run interleaved (as the verifier folds + /// the regular and symmetric row sums at once) and must stay independent. + #[test] + fn resident_accumulators_match_plain_sums() { + let terms = [ + ([1u64, 2, 3], [4u64, 5, 6], [7u64, 8, 9]), + ([10, 0, 5], [2, 3, 4], [1, 1, 1]), + ([123, 456, 789], [9, 8, 7], [2, 0, 4]), + ]; + + let mut prod = Fp3F::prod_acc_new(); + let mut expected_prod = Fp3::from_raw([GoldilocksElement::from(0); 3]); + for (a, b, c) in terms { + let (a, b, c) = (e(a), e(b), e(c)); + Fp3F::prod_acc_add(&mut prod, &a, &b, &c); + expected_prod = &expected_prod + &(&a * &b * &c); + } + assert_eq!(Fp3F::prod_acc_finish(prod), expected_prod); + + let mut acc0 = Fp3F::mul_acc_new(0); + let mut acc1 = Fp3F::mul_acc_new(1); + let mut expected0 = Fp3::from_raw([GoldilocksElement::from(0); 3]); + let mut expected1 = Fp3::from_raw([GoldilocksElement::from(0); 3]); + for (a, b, c) in terms { + let (a, b, c) = (e(a), e(b), e(c)); + Fp3F::mul_acc_add(&mut acc0, &a, &b); + Fp3F::mul_acc_add(&mut acc1, &a, &c); + expected0 = &expected0 + &(&a * &b); + expected1 = &expected1 + &(&a * &c); + } + assert_eq!(Fp3F::prod_acc_finish(acc0), expected0); + assert_eq!(Fp3F::prod_acc_finish(acc1), expected1); + } +} 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/constraints/builder.rs b/crypto/stark/src/constraints/builder.rs index 5395c7228..d8a5a5c81 100644 --- a/crypto/stark/src/constraints/builder.rs +++ b/crypto/stark/src/constraints/builder.rs @@ -277,6 +277,17 @@ pub trait ConstraintSet: Send + Sync { 2 } + /// Main-trace columns this set reads on the NEXT row (via `main(1, col)`). + /// The verifier opens OOD next-row evaluations only for these columns (unioned + /// with the LogUp accumulator); an undeclared next-row read is pruned and + /// reconstructed as zero, silently corrupting this table's transition eval. + /// Statically declared so the verify/recursion path never materializes the IR; + /// a test asserts the IR's actual next-row reads are a subset of this. Default + /// empty (most tables read only the current row). + fn next_row_columns(&self) -> Vec { + Vec::new() + } + /// Idx-ordered metadata, derived by running [`Self::eval`] through a /// [`MetaBuilder`] (which records the `{kind, end_exemptions}` at each /// `emit_*`). Never overridden — the body is the source. diff --git a/crypto/stark/src/lookup.rs b/crypto/stark/src/lookup.rs index 8a89ea727..b912cd4ff 100644 --- a/crypto/stark/src/lookup.rs +++ b/crypto/stark/src/lookup.rs @@ -1004,16 +1004,19 @@ where } fn trace_ood_next_row_columns(&self) -> Vec { - // The only transition constraint that reads the next row is the circular - // LogUp accumulator, and after forward accumulation it reads only the - // accumulated column there (all committed terms and absorbed operands - // read the current row). Its full-width index is the main width plus the - // accumulated column's aux index. No interactions => no next-row reads. - if self.auxiliary_trace_build_data.interactions.is_empty() { - Vec::new() - } else { - vec![self.trace_layout.0 + self.logup.acc_column_idx] + // Columns read on the next row: the table's own constraint-set reads + // (`main(1, ·)`, statically declared) plus, when the table has LogUp + // interactions, the circular accumulator's aux column (main width + its + // aux index). The verifier opens OOD next-row evaluations only for these; + // a next-row read that is not declared here is pruned and reconstructed as + // zero, silently corrupting this table's transition evaluation. + let mut cols = self.constraint_set.next_row_columns(); + if !self.auxiliary_trace_build_data.interactions.is_empty() { + cols.push(self.trace_layout.0 + self.logup.acc_column_idx); } + cols.sort_unstable(); + cols.dedup(); + cols } fn has_trace_interaction(&self) -> bool { diff --git a/crypto/stark/src/verifier.rs b/crypto/stark/src/verifier.rs index 64ae24363..c3b83b2b8 100644 --- a/crypto/stark/src/verifier.rs +++ b/crypto/stark/src/verifier.rs @@ -18,6 +18,7 @@ use crate::{ table::Table, }; 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; @@ -39,7 +40,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)>, @@ -47,7 +48,7 @@ pub struct Verifier< impl< Field: IsSubFieldOf + IsFFTField + Send + Sync, - FieldExtension: IsField + Send + Sync, + FieldExtension: IsField + Send + Sync + Fp3Fma, PI, > IsStarkVerifier for Verifier where @@ -62,7 +63,7 @@ where /// to validate the proof-of-work nonce. pub struct Challenges where - FieldExtension: Send + Sync + IsField, + FieldExtension: Send + Sync + IsField + Fp3Fma, { /// The out-of-domain challenge. pub z: FieldElement, @@ -90,7 +91,7 @@ pub type DeepPolynomialEvaluations = (Vec>, Vec where - FieldExtension: Send + Sync + IsField, + FieldExtension: Send + Sync + IsField + Fp3Fma, { /// `ood_row_sum[row] = sum_col trace_term_coeffs[col][row] * ood(row, col)`, /// over the reconstructed full OOD grid (g·z-pruned positions are zero). @@ -122,7 +123,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, @@ -782,13 +783,21 @@ pub trait IsStarkVerifier< let mut sum = FieldElement::::zero(); if row_idx < step_size { for col_idx in 0..ood_evaluations_table_width { - sum += &trace_term_coeffs[col_idx][row_idx] * &ood_row[col_idx]; + sum = FieldExtension::fma( + &trace_term_coeffs[col_idx][row_idx], + &ood_row[col_idx], + &sum, + ); } } else { // Next-row row: off-window columns contribute coeff·0 with a // zero coeff too, so the window-only sum is exact. for &col_idx in next_row_cols { - sum += &trace_term_coeffs[col_idx][row_idx] * &ood_row[col_idx]; + sum = FieldExtension::fma( + &trace_term_coeffs[col_idx][row_idx], + &ood_row[col_idx], + &sum, + ); } } ood_row_sum.push(sum); @@ -806,7 +815,7 @@ pub trait IsStarkVerifier< } let mut h_sum_zpow = FieldElement::::zero(); for (h_i_zpower, gamma) in composition_parts_ood.iter().zip(challenges.gammas.iter()) { - h_sum_zpow += h_i_zpower * gamma; + h_sum_zpow = FieldExtension::fma(h_i_zpower, gamma, &h_sum_zpow); } Some(QueryInvariantDeepTerms { @@ -999,19 +1008,35 @@ pub trait IsStarkVerifier< let mut trace_term_sym = FieldElement::::zero(); for row_idx in 0..ood_evaluations_table_height { let ood_row_sum = &query_invariant_terms.ood_row_sum[row_idx]; + // Base columns (the cheap asymmetric F * E product) accumulate + // natively; aux columns (the Ext * Ext product) fold through a + // resident accumulator kept in field-storage on the accelerated + // guest — regular on slot 0, symmetric on slot 1 — so the running + // aux sum is never stored/reloaded per column. Splitting the two + // reorders the row sum, which is exact (field addition is + // associative/commutative). let mut base_row_sum = FieldElement::::zero(); let mut base_row_sum_sym = FieldElement::::zero(); + let mut aux_acc = FieldExtension::mul_acc_new(0); + let mut aux_acc_sym = FieldExtension::mul_acc_new(1); if row_idx < step_size { for (col_idx, coeff_col) in trace_term_coeffs.iter().enumerate() { let coeff = &coeff_col[row_idx]; if col_idx < num_base { - // F: IsSubFieldOf gives the cheap asymmetric F * E -> E product. base_row_sum += base_at(col_idx) * coeff; base_row_sum_sym += base_at_sym(col_idx) * coeff; } else { 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]; + FieldExtension::mul_acc_add( + &mut aux_acc, + coeff, + &lde_trace_aux_evaluations[aux_idx], + ); + FieldExtension::mul_acc_add( + &mut aux_acc_sym, + coeff, + &lde_trace_aux_evaluations_sym[aux_idx], + ); } } } else { @@ -1027,13 +1052,27 @@ pub trait IsStarkVerifier< base_row_sum_sym += base_at_sym(col_idx) * coeff; } else { 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]; + FieldExtension::mul_acc_add( + &mut aux_acc, + coeff, + &lde_trace_aux_evaluations[aux_idx], + ); + FieldExtension::mul_acc_add( + &mut aux_acc_sym, + coeff, + &lde_trace_aux_evaluations_sym[aux_idx], + ); } } } - 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); + let base_row_sum = &base_row_sum + &FieldExtension::prod_acc_finish(aux_acc); + let base_row_sum_sym = + &base_row_sum_sym + &FieldExtension::prod_acc_finish(aux_acc_sym); + let trace_diff = &base_row_sum - ood_row_sum; + trace_term = FieldExtension::fma(&denoms_trace[row_idx], &trace_diff, &trace_term); + let trace_diff_sym = &base_row_sum_sym - ood_row_sum; + trace_term_sym = + FieldExtension::fma(&denoms_trace_sym[row_idx], &trace_diff_sym, &trace_term_sym); } let number_of_parts = query_invariant_terms.number_of_parts; @@ -1057,11 +1096,17 @@ pub trait IsStarkVerifier< let h_i_upsilon = &lde_composition_poly_parts_evaluation[j]; let h_i_upsilon_sym = &lde_composition_poly_parts_evaluation_sym[j]; let gamma = &challenges.gammas[j]; - h_sum += h_i_upsilon * gamma; - h_sum_sym += h_i_upsilon_sym * gamma; + h_sum = FieldExtension::fma(h_i_upsilon, gamma, &h_sum); + h_sum_sym = FieldExtension::fma(h_i_upsilon_sym, gamma, &h_sum_sym); } - let h_terms = (&h_sum - &query_invariant_terms.h_sum_zpow) * denom_composition; - let h_terms_sym = (&h_sum_sym - &query_invariant_terms.h_sum_zpow) * denom_composition_sym; + let h_terms = FieldExtension::ext_mul( + &(&h_sum - &query_invariant_terms.h_sum_zpow), + &denom_composition, + ); + let h_terms_sym = FieldExtension::ext_mul( + &(&h_sum_sym - &query_invariant_terms.h_sum_zpow), + &denom_composition_sym, + ); Some((trace_term + h_terms, trace_term_sym + h_terms_sym)) } diff --git a/executor/Cargo.toml b/executor/Cargo.toml index 3f278e1c6..f7712aa12 100644 --- a/executor/Cargo.toml +++ b/executor/Cargo.toml @@ -8,6 +8,7 @@ license.workspace = true thiserror = "1.0.68" rustc-demangle = "0.1" ecsm = { path = "../crypto/ecsm" } +math = { path = "../crypto/math" } [dev-dependencies] serde = { version = "1.0", features = ["derive"] } diff --git a/executor/programs/asm/fext_bench.s b/executor/programs/asm/fext_bench.s new file mode 100644 index 000000000..78ce8d81c --- /dev/null +++ b/executor/programs/asm/fext_bench.s @@ -0,0 +1,44 @@ + .attribute 5, "rv64i2p1_m2p0_zmmul1p0" + .globl main +main: + # Load a = (1,2,3), b = (4,5,6), c = (7,8,9) into field-storage 1/2/3 once. + li a0, 1 + li a1, 1 + li a2, 2 + li a3, 3 + li a7, -20 + ecall + li a0, 2 + li a1, 4 + li a2, 5 + li a3, 6 + li a7, -20 + ecall + li a0, 3 + li a1, 7 + li a2, 8 + li a3, 9 + li a7, -20 + ecall + + # FEXT_FMA args (a=1, b=2, c=3, out=4) set once; a7 = -21. + li a0, 1 + li a1, 2 + li a2, 3 + li a3, 4 + li a7, -21 + + # Loop: N = 4096 FEXT_FMA calls. Each writes out(4) = a*b + c at a fresh + # timestamp (distinct addresses satisfy the accelerator's per-op guard). + li t0, 4096 +.Lloop: + ecall + addi t0, t0, -1 + bnez t0, .Lloop + + # Halt. + li a0, 0 + li a7, 93 + ecall +.Lfunc_end1: + .size main, .Lfunc_end1-main diff --git a/executor/programs/asm/test_fext.s b/executor/programs/asm/test_fext.s new file mode 100644 index 000000000..57d451483 --- /dev/null +++ b/executor/programs/asm/test_fext.s @@ -0,0 +1,49 @@ + .attribute 5, "rv64i2p1_m2p0_zmmul1p0" + .globl main +main: + # FEXT_LOAD a = (1, 2, 3) into field-storage address 1. + # a0 = field-storage address, a1/a2/a3 = coefficients, a7 = -20. + li a0, 1 + li a1, 1 + li a2, 2 + li a3, 3 + li a7, -20 + ecall + + # FEXT_LOAD b = (4, 5, 6) into field-storage address 2. + li a0, 2 + li a1, 4 + li a2, 5 + li a3, 6 + li a7, -20 + ecall + + # FEXT_LOAD c = (7, 8, 9) into field-storage address 3. + li a0, 3 + li a1, 7 + li a2, 8 + li a3, 9 + li a7, -20 + ecall + + # FEXT_FMA: out(addr 4) = a(addr 1) * b(addr 2) + c(addr 3). + # a0/a1/a2 = a/b/c addresses, a3 = output address, a7 = -21. + li a0, 1 + li a1, 2 + li a2, 3 + li a3, 4 + li a7, -21 + ecall + + # FEXT_STORE: read result (addr 4) back into registers a1/a2/a3. + # a0 = field-storage source address, a7 = -22. + li a0, 4 + li a7, -22 + ecall + + # Halt. + li a0, 0 + li a7, 93 + ecall +.Lfunc_end1: + .size main, .Lfunc_end1-main diff --git a/executor/src/tests/fext_tests.rs b/executor/src/tests/fext_tests.rs new file mode 100644 index 000000000..503783cba --- /dev/null +++ b/executor/src/tests/fext_tests.rs @@ -0,0 +1,344 @@ +//! Tests for the FEXT (extension-field) accelerator syscalls: FEXT_LOAD and +//! FEXT_FMA over the native degree-3 Goldilocks extension `Fp[x]/(x^3 - 2)`. + +use crate::vm::instruction::decoding::Instruction; +use crate::vm::instruction::execution::{ + ExecutionError, FEXT_FMA_SYSCALL_NUMBER, FEXT_LOAD_SYSCALL_NUMBER, FEXT_STORE_SYSCALL_NUMBER, +}; +use crate::vm::memory::Memory; +use crate::vm::registers::Registers; +use math::field::element::FieldElement; +use math::field::extensions_goldilocks::Degree3GoldilocksExtensionField; +use math::field::goldilocks::{GOLDILOCKS_PRIME, GoldilocksElement}; + +type Fp3 = FieldElement; + +/// Independent reference for `a*b + c` over Fp3, built directly from the `math` +/// crate (cross-checks the executor's own computation). +fn reference_fma(a: [u64; 3], b: [u64; 3], c: [u64; 3]) -> [u64; 3] { + let to_fp3 = |x: [u64; 3]| { + Fp3::from_raw([ + GoldilocksElement::from(x[0]), + GoldilocksElement::from(x[1]), + GoldilocksElement::from(x[2]), + ]) + }; + let r = to_fp3(a) * to_fp3(b) + to_fp3(c); + let v = r.value(); + [ + v[0].canonical_u64(), + v[1].canonical_u64(), + v[2].canonical_u64(), + ] +} + +fn run_load(memory: &mut Memory, addr: u64, coeffs: [u64; 3]) -> Result<(), ExecutionError> { + let mut pc = 0; + let mut registers = Registers::default(); + registers.write(17, FEXT_LOAD_SYSCALL_NUMBER).unwrap(); + registers.write(10, addr).unwrap(); + registers.write(11, coeffs[0]).unwrap(); + registers.write(12, coeffs[1]).unwrap(); + registers.write(13, coeffs[2]).unwrap(); + Instruction::EcallEbreak.run(&mut pc, &mut registers, memory)?; + Ok(()) +} + +fn run_fma(memory: &mut Memory, out: u64, a: u64, b: u64, c: u64) { + let mut pc = 0; + let mut registers = Registers::default(); + registers.write(17, FEXT_FMA_SYSCALL_NUMBER).unwrap(); + registers.write(10, a).unwrap(); + registers.write(11, b).unwrap(); + registers.write(12, c).unwrap(); + registers.write(13, out).unwrap(); + Instruction::EcallEbreak + .run(&mut pc, &mut registers, memory) + .unwrap(); +} + +fn run_fma_result(out: u64, a: u64, b: u64, c: u64) -> Result<(), ExecutionError> { + let mut pc = 0; + let mut memory = Memory::default(); + let mut registers = Registers::default(); + registers.write(17, FEXT_FMA_SYSCALL_NUMBER).unwrap(); + registers.write(10, a).unwrap(); + registers.write(11, b).unwrap(); + registers.write(12, c).unwrap(); + registers.write(13, out).unwrap(); + Instruction::EcallEbreak.run(&mut pc, &mut registers, &mut memory)?; + Ok(()) +} + +#[test] +fn fext_fma_rejects_overlapping_addresses() { + // The single-timestamp design requires out/a/b/c pairwise distinct. + for (out, a, b, c) in [ + (0x10, 0x10, 0x20, 0x30), // out == a + (0x40, 0x20, 0x20, 0x30), // a == b (squaring) + (0x40, 0x10, 0x20, 0x40), // out == c + (0x40, 0x10, 0x30, 0x30), // b == c + ] { + let err = run_fma_result(out, a, b, c).unwrap_err(); + assert!( + matches!(err, ExecutionError::FextOperandOverlap), + "out={out:#x} a={a:#x} b={b:#x} c={c:#x} must be rejected" + ); + } + // Pairwise-distinct addresses run fine. + run_fma_result(0x40, 0x10, 0x20, 0x30).expect("distinct addresses must run"); +} + +fn run_store(memory: &mut Memory, src_addr: u64) -> [u64; 3] { + let mut pc = 0; + let mut registers = Registers::default(); + registers.write(17, FEXT_STORE_SYSCALL_NUMBER).unwrap(); + registers.write(10, src_addr).unwrap(); + Instruction::EcallEbreak + .run(&mut pc, &mut registers, memory) + .unwrap(); + [ + registers.read(11).unwrap(), + registers.read(12).unwrap(), + registers.read(13).unwrap(), + ] +} + +#[test] +fn fext_store_reads_back_loaded_value() { + let mut memory = Memory::default(); + run_load(&mut memory, 0x100, [11, 22, 33]).unwrap(); + assert_eq!(run_store(&mut memory, 0x100), [11, 22, 33]); +} + +#[test] +fn fext_store_then_reload_roundtrips_fma() { + // LOAD a,b,c → FMA → STORE result back to registers → equals reference. + let mut memory = Memory::default(); + let (a, b, c) = ([1, 2, 3], [4, 5, 6], [7, 8, 9]); + run_load(&mut memory, 0x10, a).unwrap(); + run_load(&mut memory, 0x20, b).unwrap(); + run_load(&mut memory, 0x30, c).unwrap(); + run_fma(&mut memory, 0x40, 0x10, 0x20, 0x30); + assert_eq!(run_store(&mut memory, 0x40), reference_fma(a, b, c)); +} + +#[test] +fn fext_load_then_fma_matches_reference() { + let mut memory = Memory::default(); + let (a_addr, b_addr, c_addr, out_addr) = (0x10, 0x20, 0x30, 0x40); + + let cases = [ + ([1, 0, 0], [1, 0, 0], [0, 0, 0]), // 1 * 1 + 0 + ([0, 1, 0], [0, 1, 0], [0, 0, 0]), // w * w = w^2 + ([0, 0, 1], [0, 0, 1], [0, 0, 0]), // w^2 * w^2 = w^4 = 2w + ([1, 2, 3], [4, 5, 6], [7, 8, 9]), // generic + ([GOLDILOCKS_PRIME - 1, 0, 0], [2, 0, 0], [1, 0, 0]), // wrap-around + ]; + + for (a, b, c) in cases { + run_load(&mut memory, a_addr, a).unwrap(); + run_load(&mut memory, b_addr, b).unwrap(); + run_load(&mut memory, c_addr, c).unwrap(); + run_fma(&mut memory, out_addr, a_addr, b_addr, c_addr); + assert_eq!( + memory.field_load(out_addr), + reference_fma(a, b, c), + "a={a:?} b={b:?} c={c:?}" + ); + } +} + +#[test] +fn fext_load_stores_all_three_coefficients() { + let mut memory = Memory::default(); + run_load(&mut memory, 0x100, [11, 22, 33]).unwrap(); + assert_eq!(memory.field_load(0x100), [11, 22, 33]); +} + +#[test] +fn fext_fma_reads_uninitialized_storage_as_zero() { + // Never-loaded field-storage addresses read as the extension-field zero, so + // 0 * 0 + 0 = 0. + let mut memory = Memory::default(); + run_fma(&mut memory, 0x40, 0x10, 0x20, 0x30); + assert_eq!(memory.field_load(0x40), [0, 0, 0]); +} + +#[test] +fn fext_fma_c_only_when_a_is_zero() { + // a = 0 ⇒ out = c. + let mut memory = Memory::default(); + run_load(&mut memory, 0x20, [9, 9, 9]).unwrap(); // b (irrelevant) + run_load(&mut memory, 0x30, [4, 5, 6]).unwrap(); // c + run_fma(&mut memory, 0x40, 0x10, 0x20, 0x30); // a untouched = 0 + assert_eq!(memory.field_load(0x40), [4, 5, 6]); +} + +#[test] +fn fext_load_rejects_non_canonical_coefficient() { + let mut memory = Memory::default(); + // p itself and p+1 are non-canonical (>= p) and must be rejected. + for bad in [GOLDILOCKS_PRIME, GOLDILOCKS_PRIME + 1, u64::MAX] { + let err = run_load(&mut memory, 0x10, [1, bad, 2]).unwrap_err(); + assert!( + matches!(err, ExecutionError::FextCoefficientNotCanonical(v) if v == bad), + "coefficient {bad:#x} must be rejected" + ); + } +} + +// 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/executor/src/tests/mod.rs b/executor/src/tests/mod.rs index 456607433..8b5ad6484 100644 --- a/executor/src/tests/mod.rs +++ b/executor/src/tests/mod.rs @@ -1,4 +1,5 @@ pub mod ecsm_tests; +pub mod fext_tests; pub mod flamegraph_tests; pub mod keccak_tests; pub mod memory_tests; diff --git a/executor/src/vm/instruction/execution.rs b/executor/src/vm/instruction/execution.rs index c92c0ab88..b14cb7f27 100644 --- a/executor/src/vm/instruction/execution.rs +++ b/executor/src/vm/instruction/execution.rs @@ -4,6 +4,9 @@ use crate::vm::{ memory::{Memory, MemoryError}, registers::Registers, }; +use math::field::element::FieldElement; +use math::field::extensions_goldilocks::Degree3GoldilocksExtensionField; +use math::field::goldilocks::{GOLDILOCKS_PRIME, GoldilocksElement}; const REGULAR_PC_UPDATE: u64 = 4; @@ -16,6 +19,12 @@ pub enum SyscallNumbers { Halt = 93, // Placeholder discriminant. The actual syscall value is ECSM_SYSCALL_NUMBER. Ecsm = 94, + // Placeholder discriminant. The actual syscall value is FEXT_LOAD_SYSCALL_NUMBER. + FextLoad = 95, + // Placeholder discriminant. The actual syscall value is FEXT_FMA_SYSCALL_NUMBER. + FextFma = 96, + // Placeholder discriminant. The actual syscall value is FEXT_STORE_SYSCALL_NUMBER. + FextStore = 97, } /// Syscall number for KeccakPermute (u64::MAX - 1 = 0xFFFF_FFFF_FFFF_FFFE). @@ -31,6 +40,21 @@ const KECCAK_STATE_BYTES: u64 = 25 * 8; /// bus as `[lo32, hi32] = [2^32 - 11, 2^32 - 1]`. pub const ECSM_SYSCALL_NUMBER: u64 = u64::MAX - 10; +/// Syscall number for `FEXT_LOAD` (spec ECALL `-20`): load a degree-3 extension +/// field element from three registers into field-storage. Unsigned it is +/// `u64::MAX - 19`, placed on the `Ecall` bus as `[2^32 - 20, 2^32 - 1]`. +pub const FEXT_LOAD_SYSCALL_NUMBER: u64 = u64::MAX - 19; + +/// Syscall number for `FEXT_FMA` (spec ECALL `-21`): compute `a*b + c` over the +/// native degree-3 Goldilocks extension. Unsigned it is `u64::MAX - 20`, placed +/// on the `Ecall` bus as `[2^32 - 21, 2^32 - 1]`. +pub const FEXT_FMA_SYSCALL_NUMBER: u64 = u64::MAX - 20; + +/// Syscall number for `FEXT_STORE` (ECALL `-22`): read a degree-3 extension +/// element from field-storage and write its three coefficients to RAM (the +/// read-back companion to FEXT_LOAD). Unsigned it is `u64::MAX - 21`. +pub const FEXT_STORE_SYSCALL_NUMBER: u64 = u64::MAX - 21; + /// `2^32`. ECSM memory operands must not overflow their lower 32-bit address limb when the /// largest per-access offset is added: the 32-byte operands reach offset +31 (last byte). const LOW_LIMB: u64 = 1 << 32; @@ -45,6 +69,9 @@ impl TryFrom for SyscallNumbers { 93 => Ok(SyscallNumbers::Halt), v if v == KECCAK_SYSCALL_NUMBER => Ok(SyscallNumbers::KeccakPermute), v if v == ECSM_SYSCALL_NUMBER => Ok(SyscallNumbers::Ecsm), + v if v == FEXT_LOAD_SYSCALL_NUMBER => Ok(SyscallNumbers::FextLoad), + v if v == FEXT_FMA_SYSCALL_NUMBER => Ok(SyscallNumbers::FextFma), + v if v == FEXT_STORE_SYSCALL_NUMBER => Ok(SyscallNumbers::FextStore), _ => Err(()), } } @@ -55,6 +82,9 @@ impl TryFrom for SyscallNumbers { pub enum Accelerator { Keccak, Ecsm, + FextLoad, + FextFma, + FextStore, } impl SyscallNumbers { @@ -65,6 +95,9 @@ impl SyscallNumbers { match self { SyscallNumbers::KeccakPermute => Some(Accelerator::Keccak), SyscallNumbers::Ecsm => Some(Accelerator::Ecsm), + SyscallNumbers::FextLoad => Some(Accelerator::FextLoad), + SyscallNumbers::FextFma => Some(Accelerator::FextFma), + SyscallNumbers::FextStore => Some(Accelerator::FextStore), SyscallNumbers::Print | SyscallNumbers::Panic | SyscallNumbers::Commit @@ -98,6 +131,28 @@ fn ecsm_addr_ok(addr: u64, max_offset: u64) -> bool { (addr % LOW_LIMB) + max_offset < LOW_LIMB } +/// Computes `a*b + c` over the native degree-3 Goldilocks extension +/// `Fp[x]/(x^3 - 2)`, returning canonical coefficients. Inputs must already be +/// canonical (`< p`). Matches `Degree3GoldilocksExtensionField::mul`, so the +/// executor and the FEXT prover chip (and its trace builder) agree bit-for-bit. +pub fn fext_fma(a: [u64; 3], b: [u64; 3], c: [u64; 3]) -> [u64; 3] { + type Fp3 = FieldElement; + let to_fp3 = |x: [u64; 3]| { + Fp3::from_raw([ + GoldilocksElement::from(x[0]), + GoldilocksElement::from(x[1]), + GoldilocksElement::from(x[2]), + ]) + }; + let res = to_fp3(a) * to_fp3(b) + to_fp3(c); + let coeffs = res.value(); + [ + coeffs[0].canonical_u64(), + coeffs[1].canonical_u64(), + coeffs[2].canonical_u64(), + ] +} + impl Instruction { /// Runs the given instruction and returns its execution log pub fn run( @@ -454,6 +509,64 @@ impl Instruction { src2_val = addr_xg; dst_val = addr_k; } + SyscallNumbers::FextLoad => { + // FEXT_LOAD(-20): store a degree-3 extension element into + // field-storage. x10 = destination field-storage address; + // x11/x12/x13 = the three coefficients (native u64 form, + // each must be a canonical Goldilocks element `< p`). + let addr = registers.read(10)?; + let mut coeffs = [0u64; 3]; + for (i, slot) in coeffs.iter_mut().enumerate() { + let v = registers.read(11 + i as u32)?; + if v >= GOLDILOCKS_PRIME { + return Err(ExecutionError::FextCoefficientNotCanonical(v)); + } + *slot = v; + } + memory.field_store(addr, coeffs); + src2_val = addr; + } + SyscallNumbers::FextFma => { + // FEXT_FMA(-21): output = a*b + c over Fp[x]/(x^3-2). + // Per spec: x10/x11/x12 = addresses of a/b/c, x13 = output + // address, all in field-storage. + let a_addr = registers.read(10)?; + let b_addr = registers.read(11)?; + let c_addr = registers.read(12)?; + let out_addr = registers.read(13)?; + // The chip uses a single timestamp for all field-storage + // accesses, so the four cells must be pairwise distinct: + // otherwise the same (domain, address) is touched twice at + // one timestamp and the memory argument can't prove the + // access chain. (This forbids in-place `out == a` and + // squaring `a == b`.) + let addrs = [out_addr, a_addr, b_addr, c_addr]; + for i in 0..addrs.len() { + for j in (i + 1)..addrs.len() { + if addrs[i] == addrs[j] { + return Err(ExecutionError::FextOperandOverlap); + } + } + } + let a = memory.field_load(a_addr); + let b = memory.field_load(b_addr); + let c = memory.field_load(c_addr); + memory.field_store(out_addr, fext_fma(a, b, c)); + src2_val = a_addr; + dst_val = b_addr; + } + SyscallNumbers::FextStore => { + // FEXT_STORE(-22): read a degree-3 extension element from + // field-storage (a0 = source address) and write its three + // coefficients back to registers a1/a2/a3 (the read-back + // companion to FEXT_LOAD, which reads coeffs from a1/a2/a3). + let src_addr = registers.read(10)?; + let coeffs = memory.field_load(src_addr); + registers.write(11, coeffs[0])?; + registers.write(12, coeffs[1])?; + registers.write(13, coeffs[2])?; + src2_val = src_addr; + } SyscallNumbers::Halt => { // halt return Ok(Log { @@ -636,6 +749,10 @@ pub enum ExecutionError { EcsmOperandOverlap, #[error("ECSM scalar multiplication error: {0}")] Ecsm(#[from] ecsm::EcsmError), + #[error("FEXT_LOAD coefficient is not a canonical field element: {0:#018x}")] + FextCoefficientNotCanonical(u64), + #[error("FEXT_FMA operand/output addresses must be pairwise distinct")] + FextOperandOverlap, } // ============================================================================= diff --git a/executor/src/vm/memory.rs b/executor/src/vm/memory.rs index e1a269a01..1cf88ea0a 100644 --- a/executor/src/vm/memory.rs +++ b/executor/src/vm/memory.rs @@ -64,6 +64,12 @@ pub struct Memory { /// onto the Commit bus by `index`), so this buffer is purely the /// executor's view used by `read_return_value` and CLI display. public_output: Vec, + /// Field-storage for the FEXT accelerator: the "arithmetic black box" + /// address space (memory domains 3/4/5 in the spec), isolated from RAM + /// `cells`. Each entry holds the three canonical Goldilocks coefficients + /// of one degree-3 extension-field element at that address; coefficient + /// `k` corresponds to memory domain `3 + k`. + field_storage: U64HashMap<[u64; 3]>, } impl Memory { @@ -163,6 +169,18 @@ impl Memory { Ok(()) } + /// Load the three coefficients of the FEXT field-storage element at + /// `address`. Uninitialized cells read as zero (the extension-field zero). + pub fn field_load(&self, address: u64) -> [u64; 3] { + self.field_storage.get(&address).copied().unwrap_or([0; 3]) + } + + /// Store the three canonical coefficients of a FEXT field-storage element + /// at `address`. + pub fn field_store(&mut self, address: u64, value: [u64; 3]) { + self.field_storage.insert(address, value); + } + pub fn load_half(&self, address: u64) -> Result { if address.is_multiple_of(2) { let aligned_address = address - address % 4; diff --git a/prover/benches/vm_prover_benchmark.rs b/prover/benches/vm_prover_benchmark.rs index 73f92fa52..62c9f01ce 100644 --- a/prover/benches/vm_prover_benchmark.rs +++ b/prover/benches/vm_prover_benchmark.rs @@ -24,6 +24,8 @@ impl BenchConfig { /// Benchmark configurations const CONFIGS: &[BenchConfig] = &[ BenchConfig::new("vm_32k", "bench_32k"), // 2^15 = 32768 rows. + // 4096 FEXT_FMA calls: measures the FEXT accelerator's proving cost. + BenchConfig::new("fext_4k", "fext_bench"), ]; // ============================================================================= diff --git a/prover/src/auto_storage.rs b/prover/src/auto_storage.rs index 49707cb4c..e8b60f19a 100644 --- a/prover/src/auto_storage.rs +++ b/prover/src/auto_storage.rs @@ -11,6 +11,18 @@ use crate::tables::commit::{bus_interactions as commit_buses, cols::NUM_COLUMNS use crate::tables::cpu::{bus_interactions as cpu_buses, cols::NUM_COLUMNS as CPU_COLS}; use crate::tables::decode::{bus_interactions as decode_buses, cols::NUM_COLUMNS as DECODE_COLS}; use crate::tables::dvrm::{bus_interactions as dvrm_buses, cols::NUM_COLUMNS as DVRM_COLS}; +use crate::tables::fext_fma::{ + bus_interactions as fext_fma_buses, cols::NUM_COLUMNS as FEXT_FMA_COLS, +}; +use crate::tables::fext_load::{ + bus_interactions as fext_load_buses, cols::NUM_COLUMNS as FEXT_LOAD_COLS, +}; +use crate::tables::fext_page::{ + bus_interactions as fext_page_buses, cols::NUM_COLUMNS as FEXT_PAGE_COLS, +}; +use crate::tables::fext_store::{ + bus_interactions as fext_store_buses, cols::NUM_COLUMNS as FEXT_STORE_COLS, +}; use crate::tables::halt::{bus_interactions as halt_buses, cols::NUM_COLUMNS as HALT_COLS}; use crate::tables::load::{bus_interactions as load_buses, cols::NUM_COLUMNS as LOAD_COLS}; use crate::tables::lt::{bus_interactions as lt_buses, cols::NUM_COLUMNS as LT_COLS}; @@ -177,6 +189,31 @@ fn table_specs(lengths: &TableLengths) -> Vec { aux_cols(commit_buses().len()), 1, ), + // FEXT accelerator tables (non-preprocessed, one main tree each). + ( + lengths.fext_load_padded_rows, + FEXT_LOAD_COLS as u64, + aux_cols(fext_load_buses().len()), + 1, + ), + ( + lengths.fext_fma_padded_rows, + FEXT_FMA_COLS as u64, + aux_cols(fext_fma_buses().len()), + 1, + ), + ( + lengths.fext_store_padded_rows, + FEXT_STORE_COLS as u64, + aux_cols(fext_store_buses().len()), + 1, + ), + ( + lengths.fext_page_padded_rows, + FEXT_PAGE_COLS as u64, + aux_cols(fext_page_buses().len()), + 1, + ), // BITWISE / DECODE / PAGE / REGISTER take the preprocessed-trace commit // path: it extracts ALL columns into the LDE and builds two Merkle trees // (precomputed_tree + mult_tree), so main_cols = full NUM_COLUMNS and diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index 169cd7278..10f59fdd8 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -68,12 +68,16 @@ use crate::statement::{StatementKind, absorb_continuation_global_statement, abso use crate::tables::local_to_global::{self, CellBoundary}; use crate::tables::page::{self, PageConfig}; use crate::tables::register; +use crate::tables::trace_builder::collect_bitwise_from_lt; 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::tables::{ + MaxRowsConfig, bitwise, fext_local_to_global, global_field_memory, global_memory, lt, +}; use crate::{ Error, FIXED_TABLE_COUNT, RuntimePageRange, TableCounts, VmAirs, - compute_expected_commit_bus_balance_view, verify_l2g_commitment_binding_view, + compute_expected_commit_bus_balance_view, create_bitwise_air, create_lt_air, + verify_fext_l2g_commitment_binding_view, verify_l2g_commitment_binding_view, }; type F = GoldilocksField; @@ -244,6 +248,79 @@ fn global_memory_air( air.with_preprocessed(commitment, global_memory::NUM_PREPROCESSED_COLS) } +/// FEXT_LOCAL_TO_GLOBAL AIR on the epoch-local `Memory` bus (used inside an epoch +/// proof). The field-storage analog of [`l2g_memory_air`]: it carries the sorted-keys +/// uniqueness constraints and the `IsHalfword`/`IsB20` + addr-LT range/ordering checks +/// (this proof has the BITWISE + LT providers). `epoch_label` is the `fini_epoch` +/// constant. The global proof commits the identical trace (root-bound), so it inherits +/// these checks. +pub(crate) fn fext_l2g_memory_air( + opts: &ProofOptions, + epoch_label: u64, +) -> AirWithBuses< + F, + E, + NullBoundaryConstraintBuilder, + (), + fext_local_to_global::FextLocalToGlobalConstraints, +> { + let interactions = [ + fext_local_to_global::memory_bus_interactions(), + fext_local_to_global::range_check_interactions(epoch_label), + ] + .concat(); + AirWithBuses::new( + fext_local_to_global::cols::NUM_COLUMNS, + AuxiliaryTraceBuildData { interactions }, + opts, + 1, + fext_local_to_global::FextLocalToGlobalConstraints, + ) +} + +/// FEXT_LOCAL_TO_GLOBAL AIR on the cross-epoch `GlobalFieldMemory` bus (used in the +/// global proof). The field-storage analog of [`l2g_global_air`]: `EmptyConstraints`, +/// since the uniqueness/range/ordering checks are enforced on the epoch-local +/// `fext_l2g_memory_air` and inherited here via the equal-root commitment binding. +pub(crate) fn fext_l2g_global_air( + opts: &ProofOptions, + epoch_label: u64, +) -> AirWithBuses { + AirWithBuses::new( + fext_local_to_global::cols::NUM_COLUMNS, + AuxiliaryTraceBuildData { + interactions: fext_local_to_global::global_bus_interactions(epoch_label), + }, + opts, + 1, + EmptyConstraints, + ) +} + +/// GLOBAL_FIELD_MEMORY AIR (the cross-epoch field-storage genesis/finalization +/// anchor). Unlike RAM's dense preprocessed `global_memory_air`, this table is sparse, +/// so it carries its own sorted-keys uniqueness constraints + `IsHalfword`/addr-LT +/// lookups — hence the global proof must provide BITWISE + LT tables for it. +pub(crate) fn global_field_memory_air( + opts: &ProofOptions, +) -> AirWithBuses< + F, + E, + NullBoundaryConstraintBuilder, + (), + global_field_memory::GlobalFieldMemoryConstraints, +> { + AirWithBuses::new( + global_field_memory::cols::NUM_COLUMNS, + AuxiliaryTraceBuildData { + interactions: global_field_memory::bus_interactions(), + }, + opts, + 1, + global_field_memory::GlobalFieldMemoryConstraints, + ) +} + /// The sorted, deduped set of page bases the touched cells fall on — the SINGLE source /// of truth for which GLOBAL_MEMORY tables exist. The prover builds the committed tables /// from this list, ships the identical list in the bundle (`ContinuationProof.touched_page_bases`), @@ -408,6 +485,9 @@ struct EpochProof { /// The committed L2G table root, tied to the global proof by /// [`verify_l2g_commitment_binding_view`]. l2g_root: Commitment, + /// The committed FEXT_L2G (field-storage bookend) root, tied to the global proof + /// the same way as `l2g_root`. + fext_l2g_root: Commitment, } /// A self-contained continuation proof: the per-epoch proofs in execution order, the one @@ -527,6 +607,13 @@ impl<'a> EpochProofView<'a> { Self::Archived(e) => e.l2g_root, } } + + fn fext_l2g_root(&self) -> Commitment { + match self { + Self::Owned(e) => e.fext_l2g_root, + Self::Archived(e) => e.fext_l2g_root, + } + } } /// Borrowed view over a [`ContinuationProof`] (owned or archived-in-place), @@ -634,6 +721,7 @@ fn prove_epoch( mut traces: Traces, is_final: bool, boundary: &[CellBoundary], + field_boundary: &[fext_local_to_global::FieldCellBoundary], opts: &ProofOptions, ) -> Result { // Count this L2G table's range-check lookups into the BITWISE table so its @@ -642,6 +730,13 @@ fn prove_epoch( &mut traces.bitwise, &local_to_global::collect_bitwise_from_l2g(boundary), ); + // Same for the field bookend's own IsHalfword + IsB20 sends (init_epoch + addr + // limbs). The addr-LT and its LT-chip internal checks were already collected at + // trace-build time via `collect_lt_from_touches`. + crate::tables::bitwise::update_multiplicities( + &mut traces.bitwise, + &fext_local_to_global::collect_bitwise_from_fext_l2g(field_boundary, start.label), + ); // Continuation epochs use the L2G bookend, so PAGE is skipped: page_configs is // empty. The verifier hard-codes this (passes `&[]`); check the prover agrees so @@ -687,9 +782,15 @@ fn prove_epoch( // to the one the global proof commits (the commitment binding compares their // roots). It is appended to the proof below, not through `air_trace_pairs`. let mut l2g_trace = local_to_global::generate_local_to_global_trace(boundary); + // The field-storage bookend, appended right after L2G (same commitment-binding + // pattern). Order of the two trailing tables is [.., L2G, FEXT_L2G]. + let fext_l2g_air = fext_l2g_memory_air(opts, label); + let mut fext_l2g_trace = + fext_local_to_global::generate_fext_local_to_global_trace(field_boundary); let mut pairs = airs.air_trace_pairs(&mut traces); pairs.push((&l2g_air, &mut l2g_trace, &())); + pairs.push((&fext_l2g_air, &mut fext_l2g_trace, &())); let proof = Prover::multi_prove( pairs, &mut seed(), @@ -698,13 +799,15 @@ fn prove_epoch( ) .map_err(|e| Error::Prover(format!("{e:?}")))?; - let l2g_root = proof - .proofs - .last() - .ok_or_else(|| { - Error::ContinuationInvariant("epoch proof is missing the L2G sub-table".to_string()) - })? - .lde_trace_main_merkle_root; + // Trailing tables are [.., L2G, FEXT_L2G]: FEXT_L2G is last, L2G second-to-last. + let n = proof.proofs.len(); + if n < 2 { + return Err(Error::ContinuationInvariant( + "epoch proof is missing the L2G / FEXT_L2G sub-tables".to_string(), + )); + } + let l2g_root = proof.proofs[n - 2].lde_trace_main_merkle_root; + let fext_l2g_root = proof.proofs[n - 1].lde_trace_main_merkle_root; Ok(EpochProof { proof, @@ -713,6 +816,7 @@ fn prove_epoch( runtime_page_ranges, reg_fini, l2g_root, + fext_l2g_root, }) } @@ -754,7 +858,8 @@ fn verify_epoch( FIXED_TABLE_COUNT - 1 }; let proof = epoch.proof(); - let expected_proof_count = table_counts.total() + fixed_tables + 1; + // Two trailing bookend tables: L2G then FEXT_L2G. + let expected_proof_count = table_counts.total() + fixed_tables + 2; if expected_proof_count != proof.len() { return Ok(false); } @@ -774,8 +879,10 @@ fn verify_epoch( decode_commitment, ); let l2g_air = l2g_memory_air(opts, label); + let fext_l2g_air = fext_l2g_memory_air(opts, label); let mut refs = airs.air_refs(); refs.push(&l2g_air); + refs.push(&fext_l2g_air); let seed = || { epoch_transcript( @@ -810,9 +917,17 @@ fn verify_epoch( return Ok(false); } - // The claimed L2G root must be the one this proof actually committed (it is what - // verify_l2g_commitment_binding_view later ties to the global proof). - Ok(proof.last().map(|p| *p.lde_trace_main_merkle_root()) == Some(epoch.l2g_root())) + // The claimed L2G / FEXT_L2G roots must be the ones this proof actually committed + // (trailing tables [.., L2G, FEXT_L2G]); the commitment binding later ties both to + // the global proof. + let n = proof.len(); + if n < 2 { + return Ok(false); + } + Ok( + *proof.get(n - 2).lde_trace_main_merkle_root() == epoch.l2g_root() + && *proof.get(n - 1).lde_trace_main_merkle_root() == epoch.fext_l2g_root(), + ) } /// Build the cross-epoch global memory proof: every epoch's L2G sub-table on the @@ -822,8 +937,10 @@ fn verify_epoch( /// non-preprocessed (committed, bus-enforced genesis — see `global_memory_air` / §3.6). /// The bus balances iff every `fini` matches the next epoch's `init` and every genesis /// matches its source (the ELF for ELF/runtime pages). +#[allow(clippy::too_many_arguments)] fn prove_global( boundaries: &[Vec], + field_boundaries: &[Vec], elf_bytes: &[u8], init_page_data: &HashMap>, page_bases: &[u64], @@ -869,6 +986,55 @@ fn prove_global( .map(|config| global_memory_air(opts, config, None)) .collect(); + // --- field-storage cross-epoch aggregation (GlobalFieldMemory bus) --------- + // Each cell's final value + last-touching epoch label (epoch order, last wins). + let mut field_final: HashMap<(u64, u64), (u64, u64)> = HashMap::new(); + for (i, epoch) in field_boundaries.iter().enumerate() { + let label = local_to_global::epoch_label(i as u64); + for fb in epoch { + field_final.insert((fb.domain, fb.addr), (fb.final_val, label)); + } + } + let anchor_cells: Vec = field_final + .iter() + .map( + |(&(domain, addr), &(value, epoch))| global_field_memory::FieldCellFinal { + domain, + addr, + value, + epoch, + }, + ) + .collect(); + + let mut fext_l2g_traces: Vec> = field_boundaries + .iter() + .map(|epoch| fext_local_to_global::generate_fext_local_to_global_trace(epoch)) + .collect(); + let mut anchor_trace = global_field_memory::generate_global_field_trace(&anchor_cells); + + // Providers for the anchor's sorted-keys uniqueness. The anchor is sparse (unlike + // RAM's dense global_memory), so the global proof must provide BITWISE + LT for its + // IsHalfword + addr-LT lookups. + let anchor_lt_ops = global_field_memory::collect_lt(&anchor_cells); + let mut lt_trace = lt::generate_lt_trace(&anchor_lt_ops); + let mut bitwise_trace = bitwise::generate_bitwise_trace(); + let mut bw_ops = global_field_memory::collect_bitwise(&anchor_cells); + bw_ops.extend(collect_bitwise_from_lt(&anchor_lt_ops)); + bitwise::update_multiplicities(&mut bitwise_trace, &bw_ops); + + let fext_l2g_airs: Vec<_> = (0..field_boundaries.len()) + .map(|i| fext_l2g_global_air(opts, local_to_global::epoch_label(i as u64))) + .collect(); + let anchor_air = global_field_memory_air(opts); + let lt_air = create_lt_air(opts); + let bitwise_air = create_bitwise_air(opts).with_preprocessed( + bitwise::preprocessed_commitment(opts), + bitwise::NUM_PRECOMPUTED_COLS, + ); + + // Table order (prover and verifier MUST agree): L2G*, GM*, FEXT_L2G*, anchor, + // BITWISE, LT. let mut pairs: Vec<(AirRef, &mut TraceTable, &())> = l2g_airs .iter() .zip(l2g_traces.iter_mut()) @@ -877,6 +1043,12 @@ fn prove_global( for (air, trace) in gm_airs.iter().zip(gm_traces.iter_mut()) { pairs.push((air as AirRef, trace, &())); } + for (air, trace) in fext_l2g_airs.iter().zip(fext_l2g_traces.iter_mut()) { + pairs.push((air as AirRef, trace, &())); + } + pairs.push((&anchor_air as AirRef, &mut anchor_trace, &())); + pairs.push((&bitwise_air as AirRef, &mut bitwise_trace, &())); + pairs.push((<_air as AirRef, &mut lt_trace, &())); Prover::multi_prove( pairs, @@ -960,10 +1132,29 @@ fn verify_global( }) .collect(); + // Field-storage aggregation airs, config-free and mirroring `prove_global`'s order: + // FEXT_L2G* (one per epoch), the GLOBAL_FIELD_MEMORY anchor, then its BITWISE + LT + // providers. + let fext_l2g_airs: Vec<_> = (0..num_epochs) + .map(|i| fext_l2g_global_air(opts, local_to_global::epoch_label(i as u64))) + .collect(); + let anchor_air = global_field_memory_air(opts); + let lt_air = create_lt_air(opts); + let bitwise_air = create_bitwise_air(opts).with_preprocessed( + bitwise::preprocessed_commitment(opts), + bitwise::NUM_PRECOMPUTED_COLS, + ); + let mut refs: Vec = l2g_airs.iter().map(|a| a as AirRef).collect(); for air in &gm_airs { refs.push(air as AirRef); } + for air in &fext_l2g_airs { + refs.push(air as AirRef); + } + refs.push(&anchor_air as AirRef); + refs.push(&bitwise_air as AirRef); + refs.push(<_air as AirRef); Verifier::multi_verify_views( &refs, @@ -1020,12 +1211,20 @@ pub fn prove_continuation( let mut provenance = local_to_global::genesis_provenance(image.iter().map(|(a, v)| (a, v as u64))); + // The cross-epoch field-storage image + provenance, carried forward exactly like + // RAM's `image`/`provenance` but keyed on `(domain, addr)` with a full field-element + // value. Seeds each epoch's `FieldStorageState` so FEXT accesses read the carried + // value; genesis is empty (untouched cells read 0). + let mut field_image: HashMap<(u64, u64), u64> = HashMap::new(); + let mut field_provenance = fext_local_to_global::FieldProvenance::new(); + let mut epochs: Vec = Vec::new(); // Full per-epoch boundaries, kept prover-local for `prove_global` (L2G traces + // final-state). Deliberately NOT stored in `EpochProof`/the bundle — `CellBoundary` // holds cell values (private-input bytes for private reads); only the value-free // page-base set is shipped (see `touched_page_bases`). let mut all_boundaries: Vec> = Vec::new(); + let mut all_field_boundaries: Vec> = Vec::new(); // The previous epoch's bound final register file R_{i+1}; epoch i+1's init is // derived from it (the cross-epoch register binding). let mut prev_fini: Option> = None; @@ -1079,7 +1278,7 @@ pub fn prove_continuation( } let label = local_to_global::epoch_label(index); - let traces = Traces::from_image_and_logs( + let traces = Traces::from_image_and_logs_carried( &elf, &image, ®ister_init, @@ -1088,25 +1287,45 @@ pub fn prove_continuation( private_inputs, is_final, true, + &field_image, #[cfg(feature = "disk-spill")] stark::storage_mode::StorageMode::Ram, )?; let boundary = local_to_global::epoch_boundary(&mut provenance, label, &traces.touched_memory_cells); + let field_boundary = fext_local_to_global::field_epoch_boundary( + &mut field_provenance, + label, + &traces.touched_field_cells, + ); let start = EpochStart { register_init: ®ister_init, label, }; - let epoch = prove_epoch(&elf, elf_bytes, &start, traces, is_final, &boundary, opts)?; + let epoch = prove_epoch( + &elf, + elf_bytes, + &start, + traces, + is_final, + &boundary, + &field_boundary, + opts, + )?; prev_fini = Some(epoch.reg_fini.clone()); // Carry the image forward: this epoch's fini is the next epoch's init. for cell in &boundary { image.set(cell.address, (cell.fini.value & 0xFF) as u8); } + // Same for field-storage: this epoch's final value seeds the next epoch. + for fb in &field_boundary { + field_image.insert((fb.domain, fb.addr), fb.final_val); + } epochs.push(epoch); all_boundaries.push(boundary); + all_field_boundaries.push(field_boundary); if is_final { break; @@ -1122,6 +1341,7 @@ pub fn prove_continuation( let touched_page_bases = touched_page_bases(&all_boundaries); let global = prove_global( &all_boundaries, + &all_field_boundaries, elf_bytes, &init_page_data, &touched_page_bases, @@ -1260,6 +1480,7 @@ fn verify_continuation_view( // Derived from the ELF for epoch 0, then from each epoch's bound fini. let mut register_init = register::register_init_from_entry_point(elf.entry_point); let mut epoch_roots: Vec = Vec::with_capacity(n); + let mut epoch_fext_roots: Vec = Vec::with_capacity(n); let mut public_output: Vec = Vec::new(); for (index, epoch) in bundle.epochs().enumerate() { @@ -1282,6 +1503,7 @@ fn verify_continuation_view( } epoch_roots.push(l2g_root); + epoch_fext_roots.push(epoch.fext_l2g_root()); public_output.extend_from_slice(epoch_public_output); // Next epoch's init is this epoch's bound fini — the cross-epoch register // (and x254) binding. A mismatched fini desyncs the next epoch's AIRs. @@ -1346,6 +1568,12 @@ fn verify_continuation_view( if !verify_l2g_commitment_binding_view(&epoch_roots, global_proof) { return Ok(None); } + // Same for the FEXT_L2G tables: they follow the L2G (n) + GLOBAL_MEMORY + // (page_bases.len()) tables in the global proof. + let fext_offset = n + page_bases.len(); + if !verify_fext_l2g_commitment_binding_view(&epoch_fext_roots, global_proof, fext_offset) { + return Ok(None); + } Ok(Some((public_output, elf.entry_point))) } @@ -1400,6 +1628,30 @@ mod tests { use super::*; use crate::test_utils::asm_elf_bytes; + // FEXT accelerator ecalls under continuation: field-storage is carried across + // epochs (fext_local_to_global bookend + GlobalFieldMemory aggregation). A small + // epoch size splits `test_fext` so field-cell lifetimes cross epoch boundaries, + // exercising the carry; the whole continuation must prove and verify. + #[test] + fn fext_works_under_continuation() { + let _ = env_logger::builder().is_test(true).try_init(); + let elf_bytes = asm_elf_bytes("test_fext"); + let opts = ProofOptions::default_test_options(); + + // Force multiple epochs so a value written in one epoch is read in a later one. + let bundle = prove_continuation(&elf_bytes, &[], 4, &opts).unwrap(); + assert!( + bundle.num_epochs() > 1, + "16-cycle epochs must split test_fext into multiple epochs to exercise the carry" + ); + let output = verify_continuation(&elf_bytes, &bundle, &opts).unwrap(); + assert!( + output.is_some(), + "FEXT continuation proof must verify (the field-storage carry closes the \ + GlobalFieldMemory bus)" + ); + } + // `test_commit_split` issues two Commit syscalls, one early and one late, so a // small epoch puts the second commit in a later epoch. That epoch starts with // x254 > 0 (the carried commit index), which exercises the cross-epoch commit diff --git a/prover/src/lib.rs b/prover/src/lib.rs index ff9601bb4..893641812 100644 --- a/prover/src/lib.rs +++ b/prover/src/lib.rs @@ -53,8 +53,9 @@ use crate::tables::types::BusId; use crate::test_utils::{ E, F, VmAir, create_bitwise_air, create_branch_air, create_bytewise_air, create_commit_air, create_cpu_air, create_cpu32_air, create_decode_air, create_dvrm_air, create_ecdas_air, - create_ecsm_air, create_eq_air, create_halt_air, create_keccak_air, create_keccak_rc_air, - create_keccak_rnd_air, create_load_air, create_lt_air, create_memw_air, + create_ecsm_air, create_eq_air, create_fext_fma_air, create_fext_load_air, + create_fext_page_air, create_fext_store_air, create_halt_air, create_keccak_air, + create_keccak_rc_air, create_keccak_rnd_air, create_load_air, create_lt_air, create_memw_air, create_memw_aligned_air, create_memw_register_air, create_mul_air, create_page_air, create_register_air, create_shift_air, create_store_air, }; @@ -82,8 +83,8 @@ pub struct RuntimePageRange { /// Number of tables that always contribute exactly one sub-proof, regardless /// of `TableCounts`: bitwise, decode, halt, commit, keccak, keccak_rnd, -/// keccak_rc, register, ecsm, ecdas. -pub const FIXED_TABLE_COUNT: usize = 10; +/// keccak_rc, register, ecsm, ecdas, fext_load, fext_fma, fext_store, fext_page. +pub const FIXED_TABLE_COUNT: usize = 14; /// Number of chunks for each split table. /// The verifier needs this to reconstruct matching AIRs. @@ -503,6 +504,10 @@ pub(crate) struct VmAirs { pub keccak_rc: VmAir, pub ecsm: VmAir, pub ecdas: VmAir, + pub fext_load: VmAir, + pub fext_fma: VmAir, + pub fext_store: VmAir, + pub fext_page: VmAir, pub register: VmAir, pub pages: Vec, pub memw_registers: Vec, @@ -528,6 +533,10 @@ impl VmAirs { (self.keccak_rc.as_ref(), &mut traces.keccak_rc, &()), (self.ecsm.as_ref(), &mut traces.ecsm, &()), (self.ecdas.as_ref(), &mut traces.ecdas, &()), + (self.fext_load.as_ref(), &mut traces.fext_load, &()), + (self.fext_fma.as_ref(), &mut traces.fext_fma, &()), + (self.fext_store.as_ref(), &mut traces.fext_store, &()), + (self.fext_page.as_ref(), &mut traces.fext_page, &()), (self.register.as_ref(), &mut traces.register, &()), ]; if self.include_halt { @@ -602,6 +611,10 @@ impl VmAirs { self.keccak_rc.as_ref(), self.ecsm.as_ref(), self.ecdas.as_ref(), + self.fext_load.as_ref(), + self.fext_fma.as_ref(), + self.fext_store.as_ref(), + self.fext_page.as_ref(), self.register.as_ref(), ]; if self.include_halt { @@ -759,6 +772,10 @@ impl VmAirs { )); let ecsm: VmAir = Box::new(create_ecsm_air(proof_options)); let ecdas: VmAir = Box::new(create_ecdas_air(proof_options)); + let fext_load: VmAir = Box::new(create_fext_load_air(proof_options)); + let fext_fma: VmAir = Box::new(create_fext_fma_air(proof_options)); + let fext_store: VmAir = Box::new(create_fext_store_air(proof_options)); + let fext_page: VmAir = Box::new(create_fext_page_air(proof_options)); let register: VmAir = if let Some((commitment, num_preprocessed_cols)) = register_preprocessed { Box::new( @@ -865,6 +882,10 @@ impl VmAirs { keccak_rc, ecsm, ecdas, + fext_load, + fext_fma, + fext_store, + fext_page, register, pages, memw_registers, @@ -986,6 +1007,22 @@ pub(crate) fn verify_l2g_commitment_binding_view( .all(|(i, root)| *final_proof.get(i).lde_trace_main_merkle_root() == *root) } +/// Bind each epoch's FEXT_L2G (field-storage bookend) root to the global proof, which +/// commits the per-epoch FEXT_L2G sub-tables starting at `offset` (after the `N` L2G +/// tables and the per-page GLOBAL_MEMORY tables). Equal roots prove the cross-epoch +/// field-storage matching ran over the very same tables the epochs committed. +pub(crate) fn verify_fext_l2g_commitment_binding_view( + epoch_fext_l2g_roots: &[Commitment], + final_proof: MultiProofView<'_, F, E, ()>, + offset: usize, +) -> bool { + final_proof.len() >= offset + epoch_fext_l2g_roots.len() + && epoch_fext_l2g_roots + .iter() + .enumerate() + .all(|(i, root)| *final_proof.get(offset + i).lde_trace_main_merkle_root() == *root) +} + // ============================================================================= // Public API: Prove / Verify // ============================================================================= diff --git a/prover/src/tables/branch.rs b/prover/src/tables/branch.rs index b5bfe83b6..82e515f29 100644 --- a/prover/src/tables/branch.rs +++ b/prover/src/tables/branch.rs @@ -163,7 +163,10 @@ pub fn generate_branch_trace( *op_map.entry(op.clone()).or_insert(0) += 1; } - let unique_ops: Vec<_> = op_map.into_iter().collect(); + // Canonical row order: HashMap iteration order is per-process random, so + // sort to keep the committed trace deterministic across runs. + let mut unique_ops: Vec<_> = op_map.into_iter().collect(); + unique_ops.sort_unstable_by_key(|(op, _)| (op.pc, op.offset, op.register, op.jalr)); let num_rows = unique_ops.len().next_power_of_two().max(4); let mut trace = TraceTable::new_main( crate::tables::types::zeroed_fe_vec(num_rows * cols::NUM_COLUMNS), diff --git a/prover/src/tables/bytewise.rs b/prover/src/tables/bytewise.rs index 2808365c6..f98361570 100644 --- a/prover/src/tables/bytewise.rs +++ b/prover/src/tables/bytewise.rs @@ -104,7 +104,10 @@ pub fn generate_bytewise_trace( *op_map.entry(op.clone()).or_insert(0) += 1; } - let unique_ops: Vec<_> = op_map.into_iter().collect(); + // Canonical row order: HashMap iteration order is per-process random, so + // sort to keep the committed trace deterministic across runs. + let mut unique_ops: Vec<_> = op_map.into_iter().collect(); + unique_ops.sort_unstable_by_key(|(op, _)| (op.a, op.b, op.op)); let num_rows = unique_ops.len().next_power_of_two().max(4); let mut trace = TraceTable::new_main( crate::tables::types::zeroed_fe_vec(num_rows * cols::NUM_COLUMNS), diff --git a/prover/src/tables/cpu.rs b/prover/src/tables/cpu.rs index 781bb02b0..f9d243d0d 100644 --- a/prover/src/tables/cpu.rs +++ b/prover/src/tables/cpu.rs @@ -188,6 +188,12 @@ pub struct CpuOperation { /// Whether this ECALL is an ECSM (elliptic-curve scalar multiply) syscall pub ecall_ecsm: bool, + /// Whether this ECALL is a FEXT_LOAD syscall. + pub ecall_fext_load: bool, + /// Whether this ECALL is a FEXT_FMA syscall. + pub ecall_fext_fma: bool, + /// Whether this ECALL is a FEXT_STORE syscall. + pub ecall_fext_store: bool, } impl CpuOperation { @@ -235,6 +241,14 @@ impl CpuOperation { // in the trace builder. let ecall_ecsm = f.ecall && log.src1_val == executor::vm::instruction::execution::ECSM_SYSCALL_NUMBER; + // FEXT operand addresses (x10/x11/x12/x13) are recovered from register + // state in the trace builder, so only the classification flag is needed. + let ecall_fext_load = f.ecall + && log.src1_val == executor::vm::instruction::execution::FEXT_LOAD_SYSCALL_NUMBER; + let ecall_fext_fma = f.ecall + && log.src1_val == executor::vm::instruction::execution::FEXT_FMA_SYSCALL_NUMBER; + let ecall_fext_store = f.ecall + && log.src1_val == executor::vm::instruction::execution::FEXT_STORE_SYSCALL_NUMBER; // Word instructions are fully handled by CPU32; the main CPU row is a // delegate that only advances the PC and sends the CPU32 lookup. We still @@ -353,6 +367,9 @@ impl CpuOperation { ecall_keccak, keccak_state_addr, ecall_ecsm, + ecall_fext_load, + ecall_fext_fma, + ecall_fext_store, } } diff --git a/prover/src/tables/dvrm.rs b/prover/src/tables/dvrm.rs index 9f979742b..890478834 100644 --- a/prover/src/tables/dvrm.rs +++ b/prover/src/tables/dvrm.rs @@ -295,7 +295,10 @@ pub fn generate_dvrm_trace( } } - let unique_ops: Vec<_> = op_map.into_iter().collect(); + // Canonical row order: HashMap iteration order is per-process random, so + // sort to keep the committed trace deterministic across runs. + let mut unique_ops: Vec<_> = op_map.into_iter().collect(); + unique_ops.sort_unstable_by_key(|(op, _)| (op.n, op.d, op.signed)); let num_rows = unique_ops.len().next_power_of_two().max(4); let mut trace = TraceTable::new_main( crate::tables::types::zeroed_fe_vec(num_rows * cols::NUM_COLUMNS), diff --git a/prover/src/tables/eq.rs b/prover/src/tables/eq.rs index 0f20ca695..85ad5841d 100644 --- a/prover/src/tables/eq.rs +++ b/prover/src/tables/eq.rs @@ -125,7 +125,10 @@ pub fn generate_eq_trace( *op_map.entry(op.clone()).or_insert(0) += 1; } - let unique_ops: Vec<_> = op_map.into_iter().collect(); + // Canonical row order: HashMap iteration order is per-process random, so + // sort to keep the committed trace deterministic across runs. + let mut unique_ops: Vec<_> = op_map.into_iter().collect(); + unique_ops.sort_unstable_by_key(|(op, _)| (op.a, op.b, op.invert)); let num_rows = unique_ops.len().next_power_of_two().max(4); let mut trace = TraceTable::new_main( crate::tables::types::zeroed_fe_vec(num_rows * cols::NUM_COLUMNS), diff --git a/prover/src/tables/fext_fma.rs b/prover/src/tables/fext_fma.rs new file mode 100644 index 000000000..c8649140f --- /dev/null +++ b/prover/src/tables/fext_fma.rs @@ -0,0 +1,358 @@ +//! FEXT_FMA accelerator table: `output = a*b + c` over the native degree-3 +//! Goldilocks extension `Fp[x]/(x^3 - 2)` (spec ECALL `-21`). +//! +//! One row per invocation. The extension is `w^3 = 2`, so (matching +//! `Degree3GoldilocksExtensionField::mul`): +//! - `out0 = a0*b0 + 2*(a1*b2 + a2*b1) + c0` +//! - `out1 = a0*b1 + a1*b0 + 2*a2*b2 + c1` +//! - `out2 = a0*b2 + a1*b1 + a2*b0 + c2` +//! +//! These are the spec's general `x^3 = αx^2 + βx + γ` constraints specialized to +//! the VM's native field (`α = β = 0`, `γ = 2`), which makes them degree 2. +//! +//! ## Bus interactions +//! - **Receiver** on `Ecall`: `[ts_lo, ts_hi, FEXT_FMA_lo32, FEXT_FMA_hi32]` (mult = μ). +//! - **Sender** on `Memw` ×4: register reads of x10/x11/x12/x13 (a/b/c/out addrs). +//! - **Memory** reads ×9: coefficient `d` of each of a/b/c from cell `(3+d, addr)`. +//! - **Memory** writes ×3: output coefficient `d` to cell `(3+d, out_addr)`. +//! - **Alu** ×12: `old_ts < ts` temporal ordering per field-storage access. +//! +//! Field-storage rides the low-level `Memory` bus directly (single field-element +//! value, free domain); the per-cell init/fini tokens come from `FEXT_PAGE`. The +//! executor guarantees a/b/c/out addresses are pairwise distinct, so all accesses +//! can share one timestamp. +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; +use stark::lookup::{BusInteraction, BusValue, Multiplicity, Packing}; +use stark::trace::TraceTable; + +use executor::vm::instruction::execution::FEXT_FMA_SYSCALL_NUMBER; + +use crate::constraints::templates::emit_is_bit; + +use super::types::{ + BusId, FE, GoldilocksExtension, GoldilocksField, VmTable, alu_op, zeroed_fe_vec, +}; + +/// Column indices for the FEXT_FMA table. +pub mod cols { + pub const TIMESTAMP_0: usize = 0; + pub const TIMESTAMP_1: usize = 1; + + // Operand addresses (each DWordWL). Registers: x10=a, x11=b, x12=c, x13=out. + pub const OUT_ADDR_0: usize = 2; + pub const OUT_ADDR_1: usize = 3; + pub const A_ADDR_0: usize = 4; + pub const A_ADDR_1: usize = 5; + pub const B_ADDR_0: usize = 6; + pub const B_ADDR_1: usize = 7; + pub const C_ADDR_0: usize = 8; + pub const C_ADDR_1: usize = 9; + + // Operand coefficients (each a single BaseField element). + pub const A0: usize = 10; + pub const A1: usize = 11; + pub const A2: usize = 12; + pub const B0: usize = 13; + pub const B1: usize = 14; + pub const B2: usize = 15; + pub const C0: usize = 16; + pub const C1: usize = 17; + pub const C2: usize = 18; + + // Output coefficients. + pub const OUT0: usize = 19; + pub const OUT1: usize = 20; + pub const OUT2: usize = 21; + + /// Multiplicity bit. + pub const MU: usize = 22; + + // Old timestamps for the 9 reads, ordered (value a/b/c, coeff 0/1/2), each a + // DWordWL (2 cols): base 23..41. + pub const READ_OLD_TS: usize = 23; + // Old timestamp (DWordWL) + old value for the 3 output writes: base 41..50. + pub const WRITE_OLD: usize = 41; + + pub const NUM_COLUMNS: usize = 50; + + /// Low-limb column of the old timestamp for read `(v, d)` (v: 0=a,1=b,2=c). + pub const fn read_old_ts(v: usize, d: usize) -> usize { + READ_OLD_TS + (v * 3 + d) * 2 + } + /// Low-limb column of the old timestamp for output write of coefficient `d`. + pub const fn write_old_ts(d: usize) -> usize { + WRITE_OLD + d * 3 + } + /// Old-value column for the output write of coefficient `d`. + pub const fn write_old_val(d: usize) -> usize { + WRITE_OLD + d * 3 + 2 + } + /// Base (low) address column of operand `v` (0=a,1=b,2=c). + pub const fn operand_addr(v: usize) -> usize { + A_ADDR_0 + v * 2 + } + /// Coefficient `d` column of operand `v` (0=a,1=b,2=c). + pub const fn operand_coeff(v: usize, d: usize) -> usize { + A0 + v * 3 + d + } +} + +const FMA_SYSCALL_LO: u64 = FEXT_FMA_SYSCALL_NUMBER & 0xFFFF_FFFF; +const FMA_SYSCALL_HI: u64 = FEXT_FMA_SYSCALL_NUMBER >> 32; + +/// One FEXT_FMA invocation. +#[derive(Debug, Clone)] +pub struct FextFmaOperation { + pub timestamp: u64, + pub out_addr: u64, + pub a_addr: u64, + pub b_addr: u64, + pub c_addr: u64, + pub a: [u64; 3], + pub b: [u64; 3], + pub c: [u64; 3], + pub output: [u64; 3], + /// Last-write timestamp of each read cell, `[value a/b/c][coeff d]`. + pub read_old_ts: [[u64; 3]; 3], + /// Last-write timestamp of each output cell (coeff d). + pub write_old_ts: [u64; 3], + /// Prior value of each output cell (coeff d). + pub write_old_val: [u64; 3], +} + +/// Generates the FEXT_FMA trace. One row per operation, padded to the next power +/// of two (min 4). Padding rows are all-zero (`μ = 0`). +pub fn generate_fext_fma_trace( + ops: &[FextFmaOperation], +) -> TraceTable { + let num_rows = ops.len().next_power_of_two().max(4); + let mut trace = TraceTable::new_main( + zeroed_fe_vec(num_rows * cols::NUM_COLUMNS), + cols::NUM_COLUMNS, + 1, + ); + let table = &mut trace.main_table; + + for (row, op) in ops.iter().enumerate() { + table.set_dword_wl(row, cols::TIMESTAMP_0, op.timestamp); + table.set_dword_wl(row, cols::OUT_ADDR_0, op.out_addr); + table.set_dword_wl(row, cols::A_ADDR_0, op.a_addr); + table.set_dword_wl(row, cols::B_ADDR_0, op.b_addr); + table.set_dword_wl(row, cols::C_ADDR_0, op.c_addr); + + for (v, coeffs) in [op.a, op.b, op.c].into_iter().enumerate() { + for (d, &val) in coeffs.iter().enumerate() { + table.set_fe(row, cols::operand_coeff(v, d), FE::from(val)); + table.set_dword_wl(row, cols::read_old_ts(v, d), op.read_old_ts[v][d]); + } + } + for d in 0..3 { + table.set_fe(row, cols::OUT0 + d, FE::from(op.output[d])); + table.set_dword_wl(row, cols::write_old_ts(d), op.write_old_ts[d]); + table.set_fe(row, cols::write_old_val(d), FE::from(op.write_old_val[d])); + } + + table.set_fe(row, cols::MU, FE::one()); + } + + trace +} + +fn direct(col: usize) -> BusValue { + BusValue::Packed { + start_column: col, + packing: Packing::Direct, + } +} + +/// A MEMW register-read interaction (24-element CO24 read; `is_register = 1`, +/// `write2 = 1`). +fn memw_register_read(lo: usize, hi: usize, reg: u64) -> BusInteraction { + BusInteraction::sender( + BusId::Memw, + Multiplicity::Column(cols::MU), + vec![ + direct(lo), + direct(hi), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(1), + BusValue::constant(2 * reg), + BusValue::constant(0), + direct(lo), + direct(hi), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + direct(cols::TIMESTAMP_0), + direct(cols::TIMESTAMP_1), + BusValue::constant(1), + BusValue::constant(0), + BusValue::constant(0), + ], + ) +} + +/// `old_ts(DWordWL) < ts` on the unified ALU bus, asserting the result is 1. +fn alu_lt_ts(old_ts_lo: usize) -> BusInteraction { + BusInteraction::sender( + BusId::Alu, + Multiplicity::Column(cols::MU), + vec![ + BusValue::Packed { + start_column: old_ts_lo, + packing: Packing::DWordWL, + }, + BusValue::Packed { + start_column: cols::TIMESTAMP_0, + packing: Packing::DWordWL, + }, + BusValue::constant(alu_op::LT as u64), + BusValue::constant(1), + BusValue::constant(0), + ], + ) +} + +/// The three interactions for one field-storage access at cell `(domain, addr)`. +/// `old_val`/`new_val` are the value columns/exprs of the old and new tokens +/// (equal for a read). `old_ts_lo` is the old-timestamp low column. +fn field_access( + domain: u64, + addr_lo: usize, + addr_hi: usize, + old_ts_lo: usize, + old_val: BusValue, + new_val: BusValue, +) -> [BusInteraction; 3] { + let consume = BusInteraction::sender( + BusId::Memory, + Multiplicity::Column(cols::MU), + vec![ + BusValue::constant(domain), + direct(addr_lo), + direct(addr_hi), + direct(old_ts_lo), + direct(old_ts_lo + 1), + old_val, + ], + ); + let emit = BusInteraction::receiver( + BusId::Memory, + Multiplicity::Column(cols::MU), + vec![ + BusValue::constant(domain), + direct(addr_lo), + direct(addr_hi), + direct(cols::TIMESTAMP_0), + direct(cols::TIMESTAMP_1), + new_val, + ], + ); + [consume, emit, alu_lt_ts(old_ts_lo)] +} + +/// Bus interactions: `Ecall` receiver + 4 register reads + 9 field reads + +/// 3 field writes (3 interactions each). +pub fn bus_interactions() -> Vec { + let mut interactions = vec![ + BusInteraction::receiver( + BusId::Ecall, + Multiplicity::Column(cols::MU), + vec![ + direct(cols::TIMESTAMP_0), + direct(cols::TIMESTAMP_1), + BusValue::constant(FMA_SYSCALL_LO), + BusValue::constant(FMA_SYSCALL_HI), + ], + ), + memw_register_read(cols::A_ADDR_0, cols::A_ADDR_1, 10), + memw_register_read(cols::B_ADDR_0, cols::B_ADDR_1, 11), + memw_register_read(cols::C_ADDR_0, cols::C_ADDR_1, 12), + memw_register_read(cols::OUT_ADDR_0, cols::OUT_ADDR_1, 13), + ]; + + // 9 reads: coefficient d of operand v from cell (3+d, operand_addr(v)). + // A read leaves the value unchanged, so old_val == new_val == coeff column. + for v in 0..3 { + let addr_lo = cols::operand_addr(v); + for d in 0..3 { + let val = direct(cols::operand_coeff(v, d)); + interactions.extend(field_access( + 3 + d as u64, + addr_lo, + addr_lo + 1, + cols::read_old_ts(v, d), + val.clone(), + val, + )); + } + } + + // 3 writes: output coefficient d to cell (3+d, out_addr). + for d in 0..3 { + interactions.extend(field_access( + 3 + d as u64, + cols::OUT_ADDR_0, + cols::OUT_ADDR_1, + cols::write_old_ts(d), + direct(cols::write_old_val(d)), + direct(cols::OUT0 + d), + )); + } + + interactions +} + +/// The FEXT_FMA constraints: +/// - idx 0: `IS_BIT(μ)`; +/// - idx 1-3: the three extension-field FMA coefficient equations (degree 2). +pub struct FextFmaConstraints; + +impl ConstraintSet for FextFmaConstraints { + fn eval>(&self, b: &mut B) { + emit_is_bit(b, 0, cols::MU, None); + + let two = b.const_base(2); + let m = |b: &B, col| b.main(0, col); + + let a0 = m(b, cols::A0); + let a1 = m(b, cols::A1); + let a2 = m(b, cols::A2); + let b0 = m(b, cols::B0); + let b1 = m(b, cols::B1); + let b2 = m(b, cols::B2); + let c0 = m(b, cols::C0); + let c1 = m(b, cols::C1); + let c2 = m(b, cols::C2); + let out0 = m(b, cols::OUT0); + let out1 = m(b, cols::OUT1); + let out2 = m(b, cols::OUT2); + + // out0 = a0*b0 + 2*(a1*b2 + a2*b1) + c0 + let expr0 = out0 + - (a0.clone() * b0.clone() + + two.clone() * (a1.clone() * b2.clone() + a2.clone() * b1.clone()) + + c0); + b.emit_base(1, expr0); + + // out1 = a0*b1 + a1*b0 + 2*a2*b2 + c1 + let expr1 = out1 + - (a0.clone() * b1.clone() + + a1.clone() * b0.clone() + + two * (a2.clone() * b2.clone()) + + c1); + b.emit_base(2, expr1); + + // out2 = a0*b2 + a1*b1 + a2*b0 + c2 + let expr2 = out2 - (a0 * b2 + a1 * b1 + a2 * b0 + c2); + b.emit_base(3, expr2); + } +} diff --git a/prover/src/tables/fext_load.rs b/prover/src/tables/fext_load.rs new file mode 100644 index 000000000..d6c3f634a --- /dev/null +++ b/prover/src/tables/fext_load.rs @@ -0,0 +1,327 @@ +//! FEXT_LOAD accelerator table: load a degree-3 extension element from three +//! registers into field-storage (spec ECALL `-20`). +//! +//! Reads the destination address from x10 and the three coefficients (native +//! u64 form) from x11/x12/x13, range-checks each `< p`, and **writes** them into +//! field-storage (memory domains 3/4/5) at the destination address. The write is +//! a genuine memory write (consume old token, emit new token) — not the draft +//! spec's read-assert (`output = value`, which forces `old == value`). +//! +//! Field-storage rides the low-level `Memory` consistency bus directly (like +//! PAGE/REGISTER/HALT): a full field-element value fits in one token and the +//! domain is a free field element, so no change to the shared MEMW chip. The +//! per-cell init/fini tokens are emitted by the `FEXT_PAGE` bookend table. +//! +//! ## Bus interactions +//! - **Receiver** on `Ecall`: `[ts_lo, ts_hi, FEXT_LOAD_lo32, FEXT_LOAD_hi32]` (mult = μ). +//! - **Sender** on `Memw` ×4: register reads of x10/x11/x12/x13. +//! - **Sender** on `Alu` ×3: `coeff_i < p` range checks. +//! - **Sender/Receiver** on `Memory` ×3 each: per coefficient, consume the old +//! token `[3+i, addr, old_ts, old_val]` and emit the new token +//! `[3+i, addr, ts, coeff_lo + 2^32*coeff_hi]`. +//! - **Sender** on `Alu` ×3: `old_ts < ts` temporal ordering. +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; +use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing}; +use stark::trace::TraceTable; + +use executor::vm::instruction::execution::FEXT_LOAD_SYSCALL_NUMBER; + +use crate::constraints::templates::emit_is_bit; + +use super::types::{ + BusId, FE, GoldilocksExtension, GoldilocksField, SHIFT_32, VmTable, alu_op, zeroed_fe_vec, +}; + +/// Column indices for the FEXT_LOAD table. +pub mod cols { + // Timestamp (DWordWL). + pub const TIMESTAMP_0: usize = 0; + pub const TIMESTAMP_1: usize = 1; + + // Destination field-storage address (DWordWL), from x10. + pub const ADDR_0: usize = 2; + pub const ADDR_1: usize = 3; + + // Coefficients in native form (each a DWordWL), from x11/x12/x13. + pub const C0_0: usize = 4; + pub const C0_1: usize = 5; + pub const C1_0: usize = 6; + pub const C1_1: usize = 7; + pub const C2_0: usize = 8; + pub const C2_1: usize = 9; + + /// Multiplicity bit. + pub const MU: usize = 10; + + // Per-coefficient memory-argument witness: the timestamp (DWordWL) and value + // of the field-storage cell before this write (0/0 on first touch). + pub const OLD_TS0_0: usize = 11; + pub const OLD_TS0_1: usize = 12; + pub const OLD_VAL0: usize = 13; + pub const OLD_TS1_0: usize = 14; + pub const OLD_TS1_1: usize = 15; + pub const OLD_VAL1: usize = 16; + pub const OLD_TS2_0: usize = 17; + pub const OLD_TS2_1: usize = 18; + pub const OLD_VAL2: usize = 19; + + pub const NUM_COLUMNS: usize = 20; + + /// Low-limb column of coefficient `i` (`i` in 0..3). + pub const fn coeff(i: usize) -> usize { + C0_0 + 2 * i + } + /// Low-limb column of the old timestamp for coefficient `i`. + pub const fn old_ts(i: usize) -> usize { + OLD_TS0_0 + 3 * i + } + /// Old value column for coefficient `i`. + pub const fn old_val(i: usize) -> usize { + OLD_VAL0 + 3 * i + } +} + +const LOAD_SYSCALL_LO: u64 = FEXT_LOAD_SYSCALL_NUMBER & 0xFFFF_FFFF; +const LOAD_SYSCALL_HI: u64 = FEXT_LOAD_SYSCALL_NUMBER >> 32; + +/// Goldilocks prime `p = 2^64 - 2^32 + 1` as a `DWordWL`: low limb `1`, high +/// limb `2^32 - 1`. Carried on the ALU bus as two sub-`p` limbs (avoids the +/// `p ≡ 0` wraparound a single packed field element would suffer). +const P_LO: u64 = 1; +const P_HI: u64 = (1u64 << 32) - 1; + +/// One FEXT_LOAD invocation. +#[derive(Debug, Clone)] +pub struct FextLoadOperation { + pub timestamp: u64, + pub addr: u64, + /// The three coefficients in native form (canonical field elements `< p`). + pub coeffs: [u64; 3], + /// Timestamp of the previous write to each field-storage cell (0 on first touch). + pub old_ts: [u64; 3], + /// Value previously stored in each field-storage cell (0 on first touch). + pub old_val: [u64; 3], +} + +/// Generates the FEXT_LOAD trace (one row per op, padded to next power of two, +/// min 4). Padding rows are all-zero (`μ = 0`). +pub fn generate_fext_load_trace( + ops: &[FextLoadOperation], +) -> TraceTable { + let num_rows = ops.len().next_power_of_two().max(4); + let mut trace = TraceTable::new_main( + zeroed_fe_vec(num_rows * cols::NUM_COLUMNS), + cols::NUM_COLUMNS, + 1, + ); + let table = &mut trace.main_table; + + for (row, op) in ops.iter().enumerate() { + table.set_dword_wl(row, cols::TIMESTAMP_0, op.timestamp); + table.set_dword_wl(row, cols::ADDR_0, op.addr); + for i in 0..3 { + table.set_dword_wl(row, cols::coeff(i), op.coeffs[i]); + table.set_dword_wl(row, cols::old_ts(i), op.old_ts[i]); + table.set_fe(row, cols::old_val(i), FE::from(op.old_val[i])); + } + table.set_fe(row, cols::MU, FE::one()); + } + + trace +} + +/// A MEMW register-read interaction (24-element CO24 read; `is_register = 1`, +/// `write2 = 1`). Register file is byte-addressed ×2. +fn memw_register_read(lo: usize, hi: usize, reg: u64) -> BusInteraction { + let col = |c| BusValue::Packed { + start_column: c, + packing: Packing::Direct, + }; + BusInteraction::sender( + BusId::Memw, + Multiplicity::Column(cols::MU), + vec![ + col(lo), + col(hi), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(1), // is_register = 1 + BusValue::constant(2 * reg), + BusValue::constant(0), + col(lo), + col(hi), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + col(cols::TIMESTAMP_0), + col(cols::TIMESTAMP_1), + BusValue::constant(1), // write2 = 1 + BusValue::constant(0), + BusValue::constant(0), + ], + ) +} + +/// `lhs(DWordWL) < rhs(DWordWL)` on the unified ALU bus, asserting the result is +/// 1: `[lhs, rhs, opsel(LT), 1, 0]`. +fn alu_lt(lhs_lo: usize, rhs: [BusValue; 2]) -> BusInteraction { + let [rhs_lo, rhs_hi] = rhs; + BusInteraction::sender( + BusId::Alu, + Multiplicity::Column(cols::MU), + vec![ + BusValue::Packed { + start_column: lhs_lo, + packing: Packing::DWordWL, + }, + rhs_lo, + rhs_hi, + BusValue::constant(alu_op::LT as u64), + BusValue::constant(1), + BusValue::constant(0), + ], + ) +} + +/// The three `Memory` + `Alu` interactions for writing coefficient `i` to +/// field-storage cell `(domain 3+i, addr)`. +fn field_write(i: usize) -> [BusInteraction; 3] { + let addr = || { + [ + BusValue::Packed { + start_column: cols::ADDR_0, + packing: Packing::Direct, + }, + BusValue::Packed { + start_column: cols::ADDR_1, + packing: Packing::Direct, + }, + ] + }; + let [addr_lo, addr_hi] = addr(); + // consume the old token [3+i, addr, old_ts, old_val] + let consume = BusInteraction::sender( + BusId::Memory, + Multiplicity::Column(cols::MU), + vec![ + BusValue::constant(3 + i as u64), + addr_lo, + addr_hi, + BusValue::Packed { + start_column: cols::old_ts(i), + packing: Packing::Direct, + }, + BusValue::Packed { + start_column: cols::old_ts(i) + 1, + packing: Packing::Direct, + }, + BusValue::Packed { + start_column: cols::old_val(i), + packing: Packing::Direct, + }, + ], + ); + let [addr_lo, addr_hi] = addr(); + // emit the new token [3+i, addr, ts, coeff_lo + 2^32*coeff_hi] + let emit = BusInteraction::receiver( + BusId::Memory, + Multiplicity::Column(cols::MU), + vec![ + BusValue::constant(3 + i as u64), + addr_lo, + addr_hi, + BusValue::Packed { + start_column: cols::TIMESTAMP_0, + packing: Packing::Direct, + }, + BusValue::Packed { + start_column: cols::TIMESTAMP_1, + packing: Packing::Direct, + }, + BusValue::linear(vec![ + LinearTerm::Column { + coefficient: 1, + column: cols::coeff(i), + }, + LinearTerm::ColumnUnsigned { + coefficient: SHIFT_32, + column: cols::coeff(i) + 1, + }, + ]), + ], + ); + // old_ts < ts + let order = alu_lt( + cols::old_ts(i), + [ + BusValue::Packed { + start_column: cols::TIMESTAMP_0, + packing: Packing::Direct, + }, + BusValue::Packed { + start_column: cols::TIMESTAMP_1, + packing: Packing::Direct, + }, + ], + ); + [consume, emit, order] +} + +/// `coeff < p` on the unified ALU bus. +fn coeff_lt_p(i: usize) -> BusInteraction { + alu_lt( + cols::coeff(i), + [BusValue::constant(P_LO), BusValue::constant(P_HI)], + ) +} + +/// Bus interactions for FEXT_LOAD: `Ecall` receiver + 4 register reads + +/// 3 `< p` range checks + 3×(consume-old, emit-new, `old_ts < ts`). +pub fn bus_interactions() -> Vec { + let mut interactions = vec![ + BusInteraction::receiver( + BusId::Ecall, + Multiplicity::Column(cols::MU), + vec![ + BusValue::Packed { + start_column: cols::TIMESTAMP_0, + packing: Packing::Direct, + }, + BusValue::Packed { + start_column: cols::TIMESTAMP_1, + packing: Packing::Direct, + }, + BusValue::constant(LOAD_SYSCALL_LO), + BusValue::constant(LOAD_SYSCALL_HI), + ], + ), + memw_register_read(cols::ADDR_0, cols::ADDR_1, 10), + memw_register_read(cols::C0_0, cols::C0_1, 11), + memw_register_read(cols::C1_0, cols::C1_1, 12), + memw_register_read(cols::C2_0, cols::C2_1, 13), + ]; + for i in 0..3 { + interactions.push(coeff_lt_p(i)); + } + for i in 0..3 { + interactions.extend(field_write(i)); + } + interactions +} + +/// FEXT_LOAD constraints: idx 0 is `IS_BIT(μ)`. Coefficient canonicality and +/// memory consistency are enforced by bus interactions, not polynomial constraints. +pub struct FextLoadConstraints; + +impl ConstraintSet for FextLoadConstraints { + fn eval>(&self, b: &mut B) { + emit_is_bit(b, 0, cols::MU, None); + } +} diff --git a/prover/src/tables/fext_local_to_global.rs b/prover/src/tables/fext_local_to_global.rs new file mode 100644 index 000000000..662d10ee8 --- /dev/null +++ b/prover/src/tables/fext_local_to_global.rs @@ -0,0 +1,397 @@ +//! FEXT_LOCAL_TO_GLOBAL table: per-epoch field-storage boundary claims for +//! cross-epoch continuations (the field-storage analog of `local_to_global.rs`). +//! +//! Under continuation, field-storage (memory domains 3/4/5) is carried across +//! epochs. This table replaces FEXT_PAGE's monolithic zero-init bookend for +//! continuation epochs: for every field cell `(domain, addr)` an epoch touches it +//! +//! - **bookends the epoch-local `Memory` bus** — receives the cell's carried init +//! token `[domain, addr, ts=0, init_val]` (balancing the first FEXT access's +//! consume-old) and sends its final token `[domain, addr, final_ts, final_val]` +//! (balancing the last access's emit-new); +//! - **emits cross-epoch `GlobalFieldMemory` tokens** — receives the init token +//! `[domain, addr, init_val, init_epoch]` left by the epoch that last wrote the +//! cell and sends the fini token `[domain, addr, final_val, epoch_label]` for the +//! next epoch, matched across epochs by the GLOBAL_FIELD_MEMORY aggregation. +//! +//! Mirrors `local_to_global.rs` exactly, with three field-storage differences: +//! - the token carries the domain (3/4/5) and a full field-element value, not a byte; +//! - **uniqueness of `(domain, addr)` is explicit** (the sorted-keys argument, as in +//! FEXT_PAGE), because — unlike RAM, whose L2G leans on the MEMW genesis token — +//! the FEXT accesses emit their own consume-old tokens and nothing external pins +//! one init per cell (see `fext_page.rs`); +//! - `init_val` is a single committed column, pinned canonical by the cross-epoch +//! bus (it must match either the anchor's genesis 0 or a prior epoch's canonical +//! `final_val`), so it needs no explicit `< p` check — exactly as FEXT_PAGE's +//! `final_val` and RAM's GLOBAL_MEMORY `FINI` are pinned transitively. +//! +//! `init_epoch` is the only cross-epoch-only quantity with no bus partner, so it is +//! range-checked here (two `IsHalfword` halfwords) and ordered by +//! `IsB20[epoch_label − 1 − init_epoch]`, forcing `init_epoch < fini_epoch`. + +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; +use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing}; +use stark::trace::TraceTable; + +use super::bitwise::{BitwiseOperation, BitwiseOperationType}; +use super::fext_sorted_keys::{self, SortedKeysLayout}; +use super::local_to_global::GENESIS_EPOCH; +use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField, VmTable, zeroed_fe_vec}; + +/// Column layout for the shared `(domain, addr)` sorted-keys uniqueness argument. +const LAYOUT: SortedKeysLayout = SortedKeysLayout { + domain: cols::DOMAIN, + addr_0: cols::ADDR_0, + addr_1: cols::ADDR_1, + mu: cols::MU, + addr0_hw_lo: cols::ADDR0_HW_LO, + addr0_hw_hi: cols::ADDR0_HW_HI, + addr1_hw_lo: cols::ADDR1_HW_LO, + addr1_hw_hi: cols::ADDR1_HW_HI, + next_addr_0: cols::NEXT_ADDR_0, + next_addr_1: cols::NEXT_ADDR_1, + same_dom: cols::SAME_DOM, + sel_same: cols::SEL_SAME, +}; + +// ========================================================================= +// Column indices +// ========================================================================= + +/// Column indices for the FEXT_LOCAL_TO_GLOBAL table (one row per touched cell). +pub mod cols { + /// Memory domain of this cell (3, 4, or 5). + pub const DOMAIN: usize = 0; + /// Cell address (DWordWL). + pub const ADDR_0: usize = 1; + pub const ADDR_1: usize = 2; + /// Carried init value (pinned canonical by the GlobalFieldMemory bus). + pub const INIT_VAL: usize = 3; + /// Originating epoch as two `IsHalfword`-checked halfwords (GlobalFieldMemory-only). + pub const INIT_EPOCH_0: usize = 4; + pub const INIT_EPOCH_1: usize = 5; + /// Timestamp of the last access to this cell this epoch (DWordWL). + pub const FINAL_TS_0: usize = 6; + pub const FINAL_TS_1: usize = 7; + /// Final value at this epoch's end. + pub const FINAL_VAL: usize = 8; + /// Multiplicity bit / real-row selector. + pub const MU: usize = 9; + + // --- uniqueness (sorted-keys) argument, mirroring FEXT_PAGE ------------- + pub const ADDR0_HW_LO: usize = 10; + pub const ADDR0_HW_HI: usize = 11; + pub const ADDR1_HW_LO: usize = 12; + pub const ADDR1_HW_HI: usize = 13; + pub const NEXT_ADDR_0: usize = 14; + pub const NEXT_ADDR_1: usize = 15; + pub const SAME_DOM: usize = 16; + pub const SEL_SAME: usize = 17; + + pub const NUM_COLUMNS: usize = 18; + + /// Cross-epoch-only halfword columns, in order — every `IsHalfword`-checked + /// column that has no `Memory`-bus partner. + pub const RANGE_CHECKED_HALFWORDS: [usize; 2] = [INIT_EPOCH_0, INIT_EPOCH_1]; + /// Address-limb halfwords, `IsHalfword`-checked so the uniqueness LT is sound. + pub const ADDR_HALFWORDS: [usize; 4] = [ADDR0_HW_LO, ADDR0_HW_HI, ADDR1_HW_LO, ADDR1_HW_HI]; +} + +// ========================================================================= +// Types +// ========================================================================= + +/// The init/fini boundary claim for one touched field cell in one epoch. +/// Prover-local only (holds cell values); never serialized. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct FieldCellBoundary { + pub domain: u64, + pub addr: u64, + /// Value the cell held when this epoch first touched it. + pub init_val: u64, + /// Epoch that last wrote the cell (or `GENESIS_EPOCH`). + pub init_epoch: u64, + /// Value the cell holds at this epoch's end. + pub final_val: u64, + /// Last access timestamp for the cell this epoch. + pub final_ts: u64, +} + +/// One epoch's touched field cells, each as `(domain, addr, final_value, final_ts)` +/// — the field-storage analog of [`super::local_to_global::EpochTouches`], produced +/// by the trace builder and turned into [`FieldCellBoundary`]s by the driver. +pub type FieldTouches = Vec<(u64, u64, u64, u64)>; + +/// Per-cell field-storage provenance: `(domain, addr) → (last_writer_epoch, value)`. +/// Unset cells read back as the genesis default `(GENESIS_EPOCH, 0)`. No timestamp: +/// the cross-epoch init token is seeded at ts=0 (timestamps are epoch-local). +pub type FieldProvenance = std::collections::HashMap<(u64, u64), (u64, u64)>; + +/// One epoch's field boundaries: take each touched cell's `init` from the running +/// `provenance` (its last writer + value) and record this epoch (1-based `epoch` +/// label) as the new writer of its `final` value. Mirrors +/// [`super::local_to_global::epoch_boundary`] for field-storage cells. +pub fn field_epoch_boundary( + provenance: &mut FieldProvenance, + epoch: u64, + touched: &FieldTouches, +) -> Vec { + let mut boundaries = Vec::with_capacity(touched.len()); + for &(domain, addr, final_val, final_ts) in touched { + let (init_epoch, init_val) = provenance + .get(&(domain, addr)) + .copied() + .unwrap_or((GENESIS_EPOCH, 0)); + boundaries.push(FieldCellBoundary { + domain, + addr, + init_val, + init_epoch, + final_val, + final_ts, + }); + provenance.insert((domain, addr), (epoch, final_val)); + } + boundaries +} + +// ========================================================================= +// Trace generation +// ========================================================================= + +/// Half-words of an epoch label (genesis 0 or a small 1-based index). +fn epoch_halfwords(epoch: u64) -> [u64; 2] { + debug_assert!(epoch < (1 << 32), "epoch label exceeds 32 bits"); + [epoch & 0xFFFF, (epoch >> 16) & 0xFFFF] +} + +/// Build the FEXT_LOCAL_TO_GLOBAL trace: one row per touched cell, sorted strictly +/// ascending by `(domain, addr)` with active rows contiguous at the top, padded to +/// a power of two (min 4). Padding rows carry a valid domain (3) and `μ = 0`. +pub fn generate_fext_local_to_global_trace( + boundaries: &[FieldCellBoundary], +) -> TraceTable { + let mut boundaries = boundaries.to_vec(); + boundaries.sort_by_key(|b| (b.domain, b.addr)); + + let num_rows = boundaries.len().next_power_of_two().max(4); + let mut trace = TraceTable::new_main( + zeroed_fe_vec(num_rows * cols::NUM_COLUMNS), + cols::NUM_COLUMNS, + 1, + ); + let table = &mut trace.main_table; + + for (row, b) in boundaries.iter().enumerate() { + let init_epoch = epoch_halfwords(b.init_epoch); + table.set_fe(row, cols::DOMAIN, FE::from(b.domain)); + table.set_dword_wl(row, cols::ADDR_0, b.addr); + table.set_fe(row, cols::INIT_VAL, FE::from(b.init_val)); + table.set_fe(row, cols::INIT_EPOCH_0, FE::from(init_epoch[0])); + table.set_fe(row, cols::INIT_EPOCH_1, FE::from(init_epoch[1])); + table.set_dword_wl(row, cols::FINAL_TS_0, b.final_ts); + table.set_fe(row, cols::FINAL_VAL, FE::from(b.final_val)); + table.set_fe(row, cols::MU, FE::one()); + } + + // Shared sorted-keys columns: addr half-words, padding domain, cross-row helpers. + LAYOUT.fill_trace(table, boundaries.len(), num_rows); + + trace +} + +// ========================================================================= +// Bus interactions +// ========================================================================= + +fn direct(col: usize) -> BusValue { + BusValue::Packed { + start_column: col, + packing: Packing::Direct, + } +} + +/// A 32-bit value reconstructed from its two halfword columns: `lo + 2^16·hi`. +fn word(lo_col: usize, hi_col: usize) -> BusValue { + BusValue::linear(vec![ + LinearTerm::Column { + coefficient: 1, + column: lo_col, + }, + LinearTerm::Column { + coefficient: 1 << 16, + column: hi_col, + }, + ]) +} + +fn mu() -> Multiplicity { + Multiplicity::Column(cols::MU) +} + +/// Cross-epoch `GlobalFieldMemory` bus interactions (two per touched cell): +/// receive the init token `[domain, addr, init_val, init_epoch]` left by the +/// originating epoch, and send the fini token `[domain, addr, final_val, +/// epoch_label]` for the next epoch. Matched ACROSS epochs by the GLOBAL_FIELD_MEMORY +/// aggregation, so within one epoch's table this bus is deliberately unbalanced. +pub fn global_bus_interactions(epoch_label: u64) -> Vec { + vec![ + BusInteraction::receiver( + BusId::GlobalFieldMemory, + mu(), + vec![ + direct(cols::DOMAIN), + direct(cols::ADDR_0), + direct(cols::ADDR_1), + direct(cols::INIT_VAL), + word(cols::INIT_EPOCH_0, cols::INIT_EPOCH_1), + ], + ), + BusInteraction::sender( + BusId::GlobalFieldMemory, + mu(), + vec![ + direct(cols::DOMAIN), + direct(cols::ADDR_0), + direct(cols::ADDR_1), + direct(cols::FINAL_VAL), + BusValue::constant(epoch_label), + ], + ), + ] +} + +/// Epoch-local `Memory` bus bookend (token `[domain, addr_lo, addr_hi, ts_lo, +/// ts_hi, value]`), replacing FEXT_PAGE's init/fini for touched cells: receive the +/// carried init token at ts=0, send the final token at the last access timestamp. +pub fn memory_bus_interactions() -> Vec { + vec![ + BusInteraction::receiver( + BusId::Memory, + mu(), + vec![ + direct(cols::DOMAIN), + direct(cols::ADDR_0), + direct(cols::ADDR_1), + BusValue::constant(0), + BusValue::constant(0), + direct(cols::INIT_VAL), + ], + ), + BusInteraction::sender( + BusId::Memory, + mu(), + vec![ + direct(cols::DOMAIN), + direct(cols::ADDR_0), + direct(cols::ADDR_1), + direct(cols::FINAL_TS_0), + direct(cols::FINAL_TS_1), + direct(cols::FINAL_VAL), + ], + ), + ] +} + +/// Range-check, ordering and uniqueness bus interactions (all with the right +/// multiplicity so padding fires none): +/// - `IsHalfword` per addr-limb halfword and per `init_epoch` halfword; +/// - `IsB20[epoch_label − 1 − init_epoch]`, forcing `init_epoch < fini_epoch`; +/// - the uniqueness `addr[i] < addr[i+1]` ALU LT on same-domain transitions. +pub fn range_check_interactions(epoch_label: u64) -> Vec { + debug_assert!(epoch_label >= 1, "epoch_label must be a 1-based fini epoch"); + // Shared addr-LT + addr-limb IsHalfword, then the cross-epoch-only init_epoch + // IsHalfword + the IsB20 ordering check (init_epoch < fini_epoch). + let mut interactions = LAYOUT.bus_interactions(); + + for &column in &cols::RANGE_CHECKED_HALFWORDS { + interactions.push(BusInteraction::sender( + BusId::IsHalfword, + mu(), + vec![direct(column)], + )); + } + + interactions.push(BusInteraction::sender( + BusId::IsB20, + mu(), + vec![BusValue::linear(vec![ + LinearTerm::Constant(epoch_label as i64 - 1), + LinearTerm::Column { + coefficient: -1, + column: cols::INIT_EPOCH_0, + }, + LinearTerm::Column { + coefficient: -(1 << 16), + column: cols::INIT_EPOCH_1, + }, + ])], + )); + + interactions +} + +/// The BITWISE lookups the range checks send, so the BITWISE table's multiplicities +/// balance [`range_check_interactions`]' `IsHalfword` and `IsB20` senders. Padding +/// rows (`MU = 0`) fire nothing, so none are emitted for them. Keep in sync with +/// [`range_check_interactions`]. +pub fn collect_bitwise_from_fext_l2g( + boundaries: &[FieldCellBoundary], + epoch_label: u64, +) -> Vec { + // Shared addr-limb halfwords (4/cell), then the cross-epoch-only init_epoch + // halfwords (2/cell) + IsB20 ordering (1/cell). BITWISE is a histogram, so order + // does not matter. + let mut ops = fext_sorted_keys::collect_bitwise(boundaries.iter().map(|b| b.addr)); + for b in boundaries { + for v16 in epoch_halfwords(b.init_epoch) { + ops.push(BitwiseOperation::halfword( + BitwiseOperationType::IsHalf, + (v16 & 0xFF) as u8, + ((v16 >> 8) & 0xFF) as u8, + )); + } + // Ordering: IsB20[epoch_label - 1 - init_epoch] (init_epoch < fini_epoch). + let diff = epoch_label - 1 - b.init_epoch; + ops.push(BitwiseOperation::b20( + (diff & 0xFF) as u8, + ((diff >> 8) & 0xFF) as u8, + ((diff >> 16) & 0xF) as u8, + )); + } + ops +} + +/// The addr `<` ALU LT ops the uniqueness argument needs (same-domain consecutive +/// touched cells), which the epoch's LT table must receive. Derived from the sorted +/// touched-cell set (available at trace-build time), so it does not depend on the +/// driver-computed init_epoch. +pub fn collect_lt_from_touches(touched: &FieldTouches) -> Vec { + fext_sorted_keys::collect_lt(touched.iter().map(|&(domain, addr, _, _)| (domain, addr))) +} + +// ========================================================================= +// Constraints +// ========================================================================= + +/// FEXT_LOCAL_TO_GLOBAL constraints: `IS_BIT(μ)` (0), domain `∈ {3,4,5}` (1), +/// `IS_BIT(same_dom)` (2), addr-limb recompose (3, 4), the sorted-keys uniqueness +/// transition constraints (5..=10), and `IS_BIT(sel_same)` (11), identical in shape +/// to FEXT_PAGE. +pub struct FextLocalToGlobalConstraints; + +impl ConstraintSet for FextLocalToGlobalConstraints { + fn eval>(&self, b: &mut B) { + // The shared sorted-keys uniqueness argument (indices 0..=11); the cross-epoch + // ordering (IsB20) and value bindings ride the buses, not extra AIR constraints. + LAYOUT.emit_constraints(b); + } + + fn max_degree(&self) -> usize { + 3 + } + + fn next_row_columns(&self) -> Vec { + vec![cols::DOMAIN, cols::ADDR_0, cols::ADDR_1, cols::MU] + } +} diff --git a/prover/src/tables/fext_page.rs b/prover/src/tables/fext_page.rs new file mode 100644 index 000000000..e7cfead70 --- /dev/null +++ b/prover/src/tables/fext_page.rs @@ -0,0 +1,194 @@ +//! FEXT_PAGE table: init/finalization bookend for the field-storage memory +//! domains (3/4/5), analogous to `PAGE` (RAM, domain 0) and `REGISTER` +//! (domain 1) but for full field-element values. +//! +//! One row per field-storage cell `(domain, addr)` touched by any FEXT op. It +//! emits the cell's zero-init token and consumes its final token, closing the +//! `Memory`-bus chain the FEXT_LOAD/FEXT_FMA accesses open: +//! - **Receiver** on `Memory`: `[domain, addr, 0, 0]` — emits the zero init token +//! (balances the first access's consume-old). +//! - **Sender** on `Memory`: `[domain, addr, final_ts, final_val]` — consumes the +//! final token (balances the last access's emit-new). +//! +//! Field-storage is zero-initialized (scratch, single-proof scope), so `init` is +//! the constant 0 rather than a committed column. +//! +//! ## Soundness: domain and uniqueness +//! The domain and address feed the shared `Memory` bus, so they must be pinned: +//! - **Domain** is constrained to `{3, 4, 5}` (idx 1), otherwise a prover could +//! forge tokens in another domain's chain (e.g. domain 0 = RAM). +//! - **Uniqueness** of each active `(domain, addr)` is enforced by a sorted-keys +//! argument: rows are emitted sorted strictly ascending by `(domain, addr)`, +//! with active rows contiguous at the top. Two rows for the same cell would +//! emit two init tokens `[domain, addr, 0, 0]`, letting a prover reset a cell +//! to zero mid-execution. The strict-increase constraints (idx 5..=10, plus the +//! addr `<` ALU lookup) make the keys distinct. +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; +use stark::lookup::{BusInteraction, BusValue, Multiplicity, Packing}; +use stark::trace::TraceTable; + +use super::fext_sorted_keys::SortedKeysLayout; +use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField, VmTable, zeroed_fe_vec}; + +/// Column layout for the shared `(domain, addr)` sorted-keys uniqueness argument. +const LAYOUT: SortedKeysLayout = SortedKeysLayout { + domain: cols::DOMAIN, + addr_0: cols::ADDR_0, + addr_1: cols::ADDR_1, + mu: cols::MU, + addr0_hw_lo: cols::ADDR0_HW_LO, + addr0_hw_hi: cols::ADDR0_HW_HI, + addr1_hw_lo: cols::ADDR1_HW_LO, + addr1_hw_hi: cols::ADDR1_HW_HI, + next_addr_0: cols::NEXT_ADDR_0, + next_addr_1: cols::NEXT_ADDR_1, + same_dom: cols::SAME_DOM, + sel_same: cols::SEL_SAME, +}; + +/// Column indices for the FEXT_PAGE table. +pub mod cols { + /// Memory domain of this cell (3, 4, or 5). + pub const DOMAIN: usize = 0; + /// Cell address (DWordWL). + pub const ADDR_0: usize = 1; + pub const ADDR_1: usize = 2; + /// Timestamp of the last access to this cell (DWordWL). + pub const FINAL_TS_0: usize = 3; + pub const FINAL_TS_1: usize = 4; + /// Final value stored in this cell. + pub const FINAL_VAL: usize = 5; + /// Multiplicity bit. + pub const MU: usize = 6; + + // --- uniqueness (sorted-keys) argument --------------------------------- + /// Half-word decomposition of the two addr limbs, range-checking each to + /// `[0, 2^32)` via `IsHalfword` so the addr `<` ALU lookup is sound (the LT + /// chip assumes word-sized limbs). + pub const ADDR0_HW_LO: usize = 7; + pub const ADDR0_HW_HI: usize = 8; + pub const ADDR1_HW_LO: usize = 9; + pub const ADDR1_HW_HI: usize = 10; + /// The next row's addr limbs, copied in so the current-row-only bus can run + /// the cross-row `addr[i] < addr[i+1]` comparison. + pub const NEXT_ADDR_0: usize = 11; + pub const NEXT_ADDR_1: usize = 12; + /// 1 iff this row and the next share a domain. + pub const SAME_DOM: usize = 13; + /// `μ_next · same_dom`: gates the addr strict-increase LT (materialized + /// because multiplicities cannot be products). + pub const SEL_SAME: usize = 14; + + pub const NUM_COLUMNS: usize = 15; +} + +/// One touched field-storage cell and its final state. +#[derive(Debug, Clone)] +pub struct FextPageOperation { + pub domain: u64, + pub addr: u64, + pub final_ts: u64, + pub final_val: u64, +} + +/// Generates the FEXT_PAGE trace (one row per touched cell, padded to next power +/// of two, min 4). Rows are sorted strictly ascending by `(domain, addr)` with +/// active rows contiguous at the top; padding rows are `μ = 0` and carry a valid +/// domain (3) so the ungated domain constraint holds everywhere. +pub fn generate_fext_page_trace( + ops: &[FextPageOperation], +) -> TraceTable { + let mut ops = ops.to_vec(); + ops.sort_by_key(|o| (o.domain, o.addr)); + + let num_rows = ops.len().next_power_of_two().max(4); + let mut trace = TraceTable::new_main( + zeroed_fe_vec(num_rows * cols::NUM_COLUMNS), + cols::NUM_COLUMNS, + 1, + ); + let table = &mut trace.main_table; + + for (row, op) in ops.iter().enumerate() { + table.set_fe(row, cols::DOMAIN, FE::from(op.domain)); + table.set_dword_wl(row, cols::ADDR_0, op.addr); + table.set_dword_wl(row, cols::FINAL_TS_0, op.final_ts); + table.set_fe(row, cols::FINAL_VAL, FE::from(op.final_val)); + table.set_fe(row, cols::MU, FE::one()); + } + + // Shared sorted-keys columns: addr half-words, padding domain, cross-row helpers. + LAYOUT.fill_trace(table, ops.len(), num_rows); + + trace +} + +fn direct(col: usize) -> BusValue { + BusValue::Packed { + start_column: col, + packing: Packing::Direct, + } +} + +/// Bus interactions: emit the zero-init token and consume the final token for +/// each touched cell on the `Memory` bus, plus the shared `(domain, addr)` +/// sorted-keys uniqueness lookups (addr-LT + addr-limb `IsHalfword`). +pub fn bus_interactions() -> Vec { + let mut interactions = vec![ + // init: emit [domain, addr, ts=0, value=0] + BusInteraction::receiver( + BusId::Memory, + Multiplicity::Column(cols::MU), + vec![ + direct(cols::DOMAIN), + direct(cols::ADDR_0), + direct(cols::ADDR_1), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + ], + ), + // fini: consume [domain, addr, final_ts, final_val] + BusInteraction::sender( + BusId::Memory, + Multiplicity::Column(cols::MU), + vec![ + direct(cols::DOMAIN), + direct(cols::ADDR_0), + direct(cols::ADDR_1), + direct(cols::FINAL_TS_0), + direct(cols::FINAL_TS_1), + direct(cols::FINAL_VAL), + ], + ), + ]; + interactions.extend(LAYOUT.bus_interactions()); + interactions +} + +/// FEXT_PAGE constraints. Per-row: `IS_BIT(μ)` (0), domain `∈ {3,4,5}` (1), +/// `IS_BIT(same_dom)` (2), addr-limb recompose (3, 4). Transition (exempting the +/// last row): `μ` non-increasing (5), `sel_same` definition (6), same-domain ⇒ +/// equal domain (7), domain increases by 1 or 2 on a change (8), next-addr copies +/// (9, 10). Per-row again: `IS_BIT(sel_same)` (11), pinning the LT sender's +/// multiplicity to `{0,1}` on the last row too. +pub struct FextPageConstraints; + +impl ConstraintSet for FextPageConstraints { + fn eval>(&self, b: &mut B) { + // FEXT_PAGE's entire constraint set is the shared sorted-keys uniqueness + // argument (IS_BIT(μ), domain ∈ {3,4,5}, addr recompose, strict-ascending + // transitions, IS_BIT(sel_same)), indices 0..=11. + LAYOUT.emit_constraints(b); + } + + fn max_degree(&self) -> usize { + 3 + } + + fn next_row_columns(&self) -> Vec { + // Constraints 5-10 read the next row via `main(1, ·)`: the contiguity and + // domain-ordering checks (DOMAIN, ADDR_0, ADDR_1) and μ non-increasing (MU). + vec![cols::DOMAIN, cols::ADDR_0, cols::ADDR_1, cols::MU] + } +} diff --git a/prover/src/tables/fext_sorted_keys.rs b/prover/src/tables/fext_sorted_keys.rs new file mode 100644 index 000000000..5c4c9aa9b --- /dev/null +++ b/prover/src/tables/fext_sorted_keys.rs @@ -0,0 +1,252 @@ +//! Shared `(domain, addr)` sorted-keys uniqueness argument for the field-storage +//! tables — `FEXT_PAGE`, `FEXT_LOCAL_TO_GLOBAL`, and `GLOBAL_FIELD_MEMORY`. +//! +//! Each is a sparse table over the same key space — memory domain `∈ {3,4,5}` and a +//! 64-bit address — that emits one per-cell token on a shared bus. Two rows for the +//! same cell would emit two tokens (e.g. two zero-init tokens), letting a prover reset +//! a cell mid-run. This argument makes the keys strictly ascending so each active cell +//! appears exactly once: rows sorted by `(domain, addr)`, active rows contiguous at the +//! top, domain constrained to `{3,4,5}` and stepping by 1 or 2 on a change, and the +//! address strictly increasing within a domain via an ALU `LT` lookup (with the addr +//! limbs range-checked to `[0, 2^32)` so the lookup is sound). +//! +//! The three tables differ only in their column indices, captured by +//! [`SortedKeysLayout`]; the constraints, bus interactions, trace-fill and provider +//! collectors are identical and live here, so the soundness argument has one home. + +use stark::constraints::builder::{ConstraintBuilder, RowDomain}; +use stark::lookup::{BusInteraction, BusValue, Multiplicity, Packing}; +use stark::table::Table; + +use crate::constraints::templates::emit_is_bit; + +use super::bitwise::{BitwiseOperation, BitwiseOperationType}; +use super::lt::LtOperation; +use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField, VmTable, alu_op}; + +/// The columns the sorted-keys uniqueness argument reads and writes. All three +/// field-storage tables provide their own indices for these logical columns. +pub struct SortedKeysLayout { + /// Memory domain (3, 4, or 5). + pub domain: usize, + /// Cell address (`DWordWL`: `addr_0` = low word, `addr_1` = high word). + pub addr_0: usize, + pub addr_1: usize, + /// Real-row selector / multiplicity. + pub mu: usize, + /// Half-word decomposition of the two addr limbs (`IsHalfword`-checked). + pub addr0_hw_lo: usize, + pub addr0_hw_hi: usize, + pub addr1_hw_lo: usize, + pub addr1_hw_hi: usize, + /// The next row's addr limbs, copied in for the current-row-only addr-LT lookup. + pub next_addr_0: usize, + pub next_addr_1: usize, + /// 1 iff this row and the next share a domain. + pub same_dom: usize, + /// `μ_next · same_dom`: gates the addr strict-increase LT. + pub sel_same: usize, +} + +impl SortedKeysLayout { + /// Emit the 12 uniqueness constraints (indices 0..=11): `IS_BIT(μ)` (0), domain + /// `∈ {3,4,5}` (1), `IS_BIT(same_dom)` (2), addr-limb recompose (3, 4), then the + /// strict-ascending transition checks exempting the last row — `μ` non-increasing + /// (5), `sel_same` definition (6), same-domain ⇒ equal domain (7), domain steps by + /// 1 or 2 on a change (8), next-addr copies (9, 10) — and finally `IS_BIT(sel_same)` + /// (11), which unlike (6) applies to *every* row. + /// + /// Constraint (11) is what makes `sel_same` safe as the addr-LT sender's + /// multiplicity. On interior rows (6) already pins `sel_same = μ_next·same_dom`, a + /// product of two bits, so it is `{0,1}` there by construction — but (6) is + /// `except_last`-gated, leaving the last row's `sel_same` a free field element. + /// Since it is the LT sender's `Multiplicity::Column`, a free last-row value of `−1` + /// would let a prover cancel a forced `+1` LT claim of the same tuple (the sum-based + /// LogUp balance permits negative multiplicities), erasing the strict-increase check + /// and re-opening duplicate-cell / token-cycle forgeries. The ungated `IS_BIT` + /// forbids any non-`{0,1}` last-row multiplicity (the honest fill leaves it 0), which + /// closes that cancellation for all three field-storage tables at once. + pub fn emit_constraints>( + &self, + b: &mut B, + ) { + emit_is_bit(b, 0, self.mu, None); + + let d = b.main(0, self.domain); + let three = b.const_base(3); + let four = b.const_base(4); + let five = b.const_base(5); + b.emit_base(1, (d.clone() - three) * (d.clone() - four) * (d - five)); + + emit_is_bit(b, 2, self.same_dom, None); + + let two16 = b.const_base(1 << 16); + let a0 = b.main(0, self.addr_0); + let a0_lo = b.main(0, self.addr0_hw_lo); + let a0_hi = b.main(0, self.addr0_hw_hi); + b.emit_base(3, a0 - (a0_lo + two16.clone() * a0_hi)); + let a1 = b.main(0, self.addr_1); + let a1_lo = b.main(0, self.addr1_hw_lo); + let a1_hi = b.main(0, self.addr1_hw_hi); + b.emit_base(4, a1 - (a1_lo + two16.clone() * a1_hi)); + + let tr = RowDomain::except_last(1); + let one = b.one(); + let two = b.const_base(2); + + let mu_cur = b.main(0, self.mu); + let mu_next = b.main(1, self.mu); + let same = b.main(0, self.same_dom); + let sel = b.main(0, self.sel_same); + let d_cur = b.main(0, self.domain); + let d_next = b.main(1, self.domain); + + b.emit_base_rows(5, tr, mu_next.clone() * (one.clone() - mu_cur)); + b.emit_base_rows(6, tr, sel.clone() - mu_next.clone() * same); + b.emit_base_rows(7, tr, sel.clone() * (d_next.clone() - d_cur.clone())); + + let sel_diff = mu_next - sel; + let delta = d_next - d_cur; + b.emit_base_rows(8, tr, sel_diff * (delta.clone() - one) * (delta - two)); + + let na0 = b.main(0, self.next_addr_0); + let addr0_next = b.main(1, self.addr_0); + b.emit_base_rows(9, tr, na0 - addr0_next); + let na1 = b.main(0, self.next_addr_1); + let addr1_next = b.main(1, self.addr_1); + b.emit_base_rows(10, tr, na1 - addr1_next); + + emit_is_bit(b, 11, self.sel_same, None); + } + + /// Number of constraints [`emit_constraints`](Self::emit_constraints) emits. + pub const NUM_CONSTRAINTS: usize = 12; + + /// The uniqueness bus interactions: the `addr[i] < addr[i+1]` ALU LT on same-domain + /// active transitions (multiplicity `sel_same`), plus the four `IsHalfword` checks + /// pinning the addr limbs to `[0, 2^32)` (multiplicity `mu`). + pub fn bus_interactions(&self) -> Vec { + let is_halfword = |col: usize| { + BusInteraction::sender( + BusId::IsHalfword, + Multiplicity::Column(self.mu), + vec![direct(col)], + ) + }; + vec![ + BusInteraction::sender( + BusId::Alu, + Multiplicity::Column(self.sel_same), + vec![ + BusValue::Packed { + start_column: self.addr_0, + packing: Packing::DWordWL, + }, + BusValue::Packed { + start_column: self.next_addr_0, + packing: Packing::DWordWL, + }, + BusValue::constant(alu_op::LT as u64), + BusValue::constant(1), + BusValue::constant(0), + ], + ), + is_halfword(self.addr0_hw_lo), + is_halfword(self.addr0_hw_hi), + is_halfword(self.addr1_hw_lo), + is_halfword(self.addr1_hw_hi), + ] + } + + /// Fill the uniqueness helper columns, given the caller has already set `domain`, + /// `addr_0`/`addr_1` and `mu` on the `num_active` real rows (sorted ascending by + /// `(domain, addr)`): the addr half-words on each real row, a valid domain (3) on + /// the padding rows so the ungated domain constraint holds, and the cross-row + /// `next_addr`/`same_dom`/`sel_same` helpers (the last row's transition is exempt). + pub fn fill_trace( + &self, + table: &mut Table, + num_active: usize, + num_rows: usize, + ) { + for row in 0..num_active { + let lo = table.get(row, self.addr_0).to_raw(); + let hi = table.get(row, self.addr_1).to_raw(); + table.set_fe(row, self.addr0_hw_lo, FE::from(lo & 0xFFFF)); + table.set_fe(row, self.addr0_hw_hi, FE::from(lo >> 16)); + table.set_fe(row, self.addr1_hw_lo, FE::from(hi & 0xFFFF)); + table.set_fe(row, self.addr1_hw_hi, FE::from(hi >> 16)); + } + + for row in num_active..num_rows { + table.set_fe(row, self.domain, FE::from(3u64)); + } + + for row in 0..num_rows - 1 { + let next_addr_0 = *table.get(row + 1, self.addr_0); + let next_addr_1 = *table.get(row + 1, self.addr_1); + let cur_dom = *table.get(row, self.domain); + let next_dom = *table.get(row + 1, self.domain); + let next_active = *table.get(row + 1, self.mu) == FE::one(); + let same = cur_dom == next_dom; + + table.set_fe(row, self.next_addr_0, next_addr_0); + table.set_fe(row, self.next_addr_1, next_addr_1); + table.set_fe( + row, + self.same_dom, + if same { FE::one() } else { FE::zero() }, + ); + table.set_fe( + row, + self.sel_same, + if same && next_active { + FE::one() + } else { + FE::zero() + }, + ); + } + } +} + +fn direct(col: usize) -> BusValue { + BusValue::Packed { + start_column: col, + packing: Packing::Direct, + } +} + +/// The `addr[i] < addr[i+1]` ALU LT ops the uniqueness argument needs — one per +/// same-domain consecutive pair in the sorted `(domain, addr)` cell set — which the +/// providing LT table must receive. Data-level (no column indices), so every +/// field-storage table shares it. +pub fn collect_lt(cells: impl IntoIterator) -> Vec { + let mut cells: Vec<(u64, u64)> = cells.into_iter().collect(); + cells.sort_by_key(|&(domain, addr)| (domain, addr)); + let mut ops = Vec::new(); + for pair in cells.windows(2) { + if pair[0].0 == pair[1].0 { + ops.push(LtOperation::new(pair[0].1, pair[1].1, false)); + } + } + ops +} + +/// The four `IsHalfword` provider rows per touched cell (both addr limbs split into +/// half-words), matching the addr-limb range checks in [`SortedKeysLayout::bus_interactions`]. +pub fn collect_bitwise(addrs: impl IntoIterator) -> Vec { + let mut ops = Vec::new(); + for addr in addrs { + for word in [addr & 0xFFFF_FFFF, addr >> 32] { + for hv in [word & 0xFFFF, (word >> 16) & 0xFFFF] { + ops.push(BitwiseOperation::halfword( + BitwiseOperationType::IsHalf, + (hv & 0xFF) as u8, + ((hv >> 8) & 0xFF) as u8, + )); + } + } + } + ops +} diff --git a/prover/src/tables/fext_store.rs b/prover/src/tables/fext_store.rs new file mode 100644 index 000000000..fd347ca51 --- /dev/null +++ b/prover/src/tables/fext_store.rs @@ -0,0 +1,359 @@ +//! FEXT_STORE accelerator table: read a degree-3 extension element from +//! field-storage and write its three coefficients back to registers a1/a2/a3 +//! (ECALL `-22`). The read-back companion to FEXT_LOAD (which reads coeffs from +//! a1/a2/a3), so a guest can extract Fp3 results from the accelerator's +//! field-storage into normal registers. +//! +//! ## Bus interactions +//! - **Receiver** on `Ecall`: `[ts_lo, ts_hi, FEXT_STORE_lo32, FEXT_STORE_hi32]` (mult = μ). +//! - **Sender** on `Memw`: register read of x10 (source address). +//! - **Sender/Receiver** on `Memory` ×3 each: read coefficient `d` from cell +//! `(3+d, src_addr)` (consume old / emit new; value = `lo + 2^32*hi`). +//! - **Sender** on `Alu` ×3: `old_ts < ts` temporal ordering. +//! - **Sender** on `Memw` ×3: register writes of a1/a2/a3 = `[lo, hi]` per coeff. +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; +use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing}; +use stark::trace::TraceTable; + +use executor::vm::instruction::execution::FEXT_STORE_SYSCALL_NUMBER; + +use crate::constraints::templates::emit_is_bit; + +use super::types::{ + BusId, FE, GoldilocksExtension, GoldilocksField, SHIFT_32, VmTable, alu_op, zeroed_fe_vec, +}; + +/// Column indices for the FEXT_STORE table. +pub mod cols { + pub const TIMESTAMP_0: usize = 0; + pub const TIMESTAMP_1: usize = 1; + + /// Source field-storage address (DWordWL), from x10. + pub const SRC_ADDR_0: usize = 2; + pub const SRC_ADDR_1: usize = 3; + + // Coefficient words written to a1/a2/a3 (each register = [lo, hi] Words). + pub const C0_LO: usize = 4; + pub const C0_HI: usize = 5; + pub const C1_LO: usize = 6; + pub const C1_HI: usize = 7; + pub const C2_LO: usize = 8; + pub const C2_HI: usize = 9; + + // Last-write timestamp (DWordWL) of each read field cell. + pub const OLD_TS0_0: usize = 10; + pub const OLD_TS0_1: usize = 11; + pub const OLD_TS1_0: usize = 12; + pub const OLD_TS1_1: usize = 13; + pub const OLD_TS2_0: usize = 14; + pub const OLD_TS2_1: usize = 15; + + /// Multiplicity bit. + pub const MU: usize = 16; + + // Halfword decomposition of each of the 6 coefficient words (C0_LO..C2_HI), + // two 16-bit halves per word, used to prove each word is `< 2^32` via the + // `IsHalfword` range check (the field-storage read only pins + // `lo + 2^32*hi ≡ V (mod p)`, so without this the register write could carry + // a non-canonical word). See [`hw`]. + pub const HW_BASE: usize = 17; + + pub const NUM_COLUMNS: usize = HW_BASE + 12; + + /// Low-word column of coefficient `d`. + pub const fn coeff_lo(d: usize) -> usize { + C0_LO + 2 * d + } + /// Low-limb column of the old timestamp for the read of coefficient `d`. + pub const fn old_ts(d: usize) -> usize { + OLD_TS0_0 + 2 * d + } + /// Low half-word column for the word at column `word_col` (one of + /// `C0_LO..=C2_HI`); the high half-word is at `hw(word_col) + 1`. + pub const fn hw(word_col: usize) -> usize { + HW_BASE + 2 * (word_col - C0_LO) + } +} + +const STORE_SYSCALL_LO: u64 = FEXT_STORE_SYSCALL_NUMBER & 0xFFFF_FFFF; +const STORE_SYSCALL_HI: u64 = FEXT_STORE_SYSCALL_NUMBER >> 32; + +/// Goldilocks prime `p = 2^64 - 2^32 + 1` as a `DWordWL`: low limb `1`, high +/// limb `2^32 - 1` (carried as two sub-`p` limbs on the ALU bus, mirroring +/// `fext_load`). +const P_LO: u64 = 1; +const P_HI: u64 = (1u64 << 32) - 1; + +/// One FEXT_STORE invocation. +#[derive(Debug, Clone)] +pub struct FextStoreOperation { + pub timestamp: u64, + pub src_addr: u64, + /// The three coefficients read from field-storage. + pub coeffs: [u64; 3], + /// Last-write timestamp of each read field cell. + pub old_ts: [u64; 3], +} + +/// Generates the FEXT_STORE trace (one row per op, padded to next power of two, +/// min 4). Padding rows are all-zero (`μ = 0`). +pub fn generate_fext_store_trace( + ops: &[FextStoreOperation], +) -> TraceTable { + let num_rows = ops.len().next_power_of_two().max(4); + let mut trace = TraceTable::new_main( + zeroed_fe_vec(num_rows * cols::NUM_COLUMNS), + cols::NUM_COLUMNS, + 1, + ); + let table = &mut trace.main_table; + + for (row, op) in ops.iter().enumerate() { + table.set_dword_wl(row, cols::TIMESTAMP_0, op.timestamp); + table.set_dword_wl(row, cols::SRC_ADDR_0, op.src_addr); + for d in 0..3 { + table.set_dword_wl(row, cols::coeff_lo(d), op.coeffs[d]); + table.set_dword_wl(row, cols::old_ts(d), op.old_ts[d]); + // Split each of the coefficient's lo/hi words into two 16-bit halves. + for (k, word) in [op.coeffs[d] & 0xFFFF_FFFF, op.coeffs[d] >> 32] + .into_iter() + .enumerate() + { + let wc = cols::coeff_lo(d) + k; + table.set_fe(row, cols::hw(wc), FE::from(word & 0xFFFF)); + table.set_fe(row, cols::hw(wc) + 1, FE::from(word >> 16)); + } + } + table.set_fe(row, cols::MU, FE::one()); + } + + trace +} + +fn direct(col: usize) -> BusValue { + BusValue::Packed { + start_column: col, + packing: Packing::Direct, + } +} + +/// The coefficient value `lo + 2^32*hi` as a single field element (matches the +/// value LOAD/FMA wrote into field-storage). +fn coeff_value(d: usize) -> BusValue { + BusValue::linear(vec![ + LinearTerm::Column { + coefficient: 1, + column: cols::coeff_lo(d), + }, + LinearTerm::ColumnUnsigned { + coefficient: SHIFT_32, + column: cols::coeff_lo(d) + 1, + }, + ]) +} + +/// MEMW register **read** (24-element CO24; `old == value`, `is_register = 1`, +/// `write2 = 1`). +fn memw_register_read(lo: usize, hi: usize, reg: u64) -> BusInteraction { + BusInteraction::sender( + BusId::Memw, + Multiplicity::Column(cols::MU), + vec![ + direct(lo), + direct(hi), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(1), + BusValue::constant(2 * reg), + BusValue::constant(0), + direct(lo), + direct(hi), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + direct(cols::TIMESTAMP_0), + direct(cols::TIMESTAMP_1), + BusValue::constant(1), + BusValue::constant(0), + BusValue::constant(0), + ], + ) +} + +/// MEMW register **write** (16-element write format; `is_register = 1`, +/// `write2 = 1`): writes `[lo, hi]` of coefficient `d` to register `reg`. +fn memw_register_write(reg: u64, lo: usize, hi: usize) -> BusInteraction { + BusInteraction::sender( + BusId::Memw, + Multiplicity::Column(cols::MU), + vec![ + BusValue::constant(1), // is_register + BusValue::constant(2 * reg), + BusValue::constant(0), + direct(lo), + direct(hi), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + direct(cols::TIMESTAMP_0), + direct(cols::TIMESTAMP_1), + BusValue::constant(1), // write2 + BusValue::constant(0), + BusValue::constant(0), + ], + ) +} + +/// `IsHalfword[col]` — range-check that the column is a valid half-word +/// `[0, 2^16)` (mult = μ). +fn is_halfword(col: usize) -> BusInteraction { + BusInteraction::sender( + BusId::IsHalfword, + Multiplicity::Column(cols::MU), + vec![direct(col)], + ) +} + +/// `coeff_d(DWordWL) < p` on the ALU bus — the read-back value is canonical. +/// Sound only because the coefficient's words are pinned to `[0, 2^16)` halves +/// (the LT chip assumes word-sized limbs). +fn coeff_lt_p(d: usize) -> BusInteraction { + BusInteraction::sender( + BusId::Alu, + Multiplicity::Column(cols::MU), + vec![ + BusValue::Packed { + start_column: cols::coeff_lo(d), + packing: Packing::DWordWL, + }, + BusValue::constant(P_LO), + BusValue::constant(P_HI), + BusValue::constant(alu_op::LT as u64), + BusValue::constant(1), + BusValue::constant(0), + ], + ) +} + +/// `old_ts(DWordWL) < ts` on the ALU bus, asserting the result is 1. +fn alu_lt_ts(old_ts_lo: usize) -> BusInteraction { + BusInteraction::sender( + BusId::Alu, + Multiplicity::Column(cols::MU), + vec![ + BusValue::Packed { + start_column: old_ts_lo, + packing: Packing::DWordWL, + }, + BusValue::Packed { + start_column: cols::TIMESTAMP_0, + packing: Packing::DWordWL, + }, + BusValue::constant(alu_op::LT as u64), + BusValue::constant(1), + BusValue::constant(0), + ], + ) +} + +/// The three `Memory` interactions for reading coefficient `d` from cell +/// `(3+d, src_addr)`: consume old token, emit new token (read: value unchanged), +/// and `old_ts < ts`. +fn field_read(d: usize) -> [BusInteraction; 3] { + let domain = 3 + d as u64; + let consume = BusInteraction::sender( + BusId::Memory, + Multiplicity::Column(cols::MU), + vec![ + BusValue::constant(domain), + direct(cols::SRC_ADDR_0), + direct(cols::SRC_ADDR_1), + direct(cols::old_ts(d)), + direct(cols::old_ts(d) + 1), + coeff_value(d), + ], + ); + let emit = BusInteraction::receiver( + BusId::Memory, + Multiplicity::Column(cols::MU), + vec![ + BusValue::constant(domain), + direct(cols::SRC_ADDR_0), + direct(cols::SRC_ADDR_1), + direct(cols::TIMESTAMP_0), + direct(cols::TIMESTAMP_1), + coeff_value(d), + ], + ); + [consume, emit, alu_lt_ts(cols::old_ts(d))] +} + +/// Bus interactions: `Ecall` receiver + register read (x10) + 3×(field read +/// consume/emit + `old_ts Vec { + let mut interactions = vec![ + BusInteraction::receiver( + BusId::Ecall, + Multiplicity::Column(cols::MU), + vec![ + direct(cols::TIMESTAMP_0), + direct(cols::TIMESTAMP_1), + BusValue::constant(STORE_SYSCALL_LO), + BusValue::constant(STORE_SYSCALL_HI), + ], + ), + memw_register_read(cols::SRC_ADDR_0, cols::SRC_ADDR_1, 10), + ]; + for d in 0..3 { + interactions.extend(field_read(d)); + } + for d in 0..3 { + interactions.push(memw_register_write( + 11 + d as u64, + cols::coeff_lo(d), + cols::coeff_lo(d) + 1, + )); + } + // Canonicality of each read-back coefficient: prove both words are `< 2^16` + // halves (12 IsHalfword) and the reconstructed value is `< p` (3 ALU LT). + for d in 0..3 { + for k in 0..2 { + let wc = cols::coeff_lo(d) + k; + interactions.push(is_halfword(cols::hw(wc))); + interactions.push(is_halfword(cols::hw(wc) + 1)); + } + interactions.push(coeff_lt_p(d)); + } + interactions +} + +/// FEXT_STORE constraints: idx 0 is `IS_BIT(μ)`; idx 1..=6 recompose each of the +/// six coefficient words from its two half-word limbs (`word = lo + 2^16*hi`). +/// Combined with the `IsHalfword` range checks on those limbs, this pins every +/// word to `[0, 2^32)` so the `coeff < p` ALU check is sound and the registers +/// receive the canonical `(lo, hi)`. +pub struct FextStoreConstraints; + +impl ConstraintSet for FextStoreConstraints { + fn eval>(&self, b: &mut B) { + emit_is_bit(b, 0, cols::MU, None); + + let two16 = b.const_base(1 << 16); + for (i, word_col) in (cols::C0_LO..=cols::C2_HI).enumerate() { + let word = b.main(0, word_col); + let lo = b.main(0, cols::hw(word_col)); + let hi = b.main(0, cols::hw(word_col) + 1); + b.emit_base(1 + i, word - (lo + two16.clone() * hi)); + } + } +} diff --git a/prover/src/tables/global_field_memory.rs b/prover/src/tables/global_field_memory.rs new file mode 100644 index 000000000..7f1591efb --- /dev/null +++ b/prover/src/tables/global_field_memory.rs @@ -0,0 +1,246 @@ +//! GLOBAL_FIELD_MEMORY table for cross-epoch field-storage init/finalization. +//! +//! The field-storage (memory domains 3/4/5) analog of `global_memory.rs` +//! (`GLOBAL_MEMORY`, RAM): it closes the two loose ends of the per-cell cross-epoch +//! chain that FEXT_PAGE's continuation-mode boundary claims open on the +//! `GlobalFieldMemory` bus. For every field-storage cell `(domain, addr)` touched +//! anywhere in the run it **sends** a genesis token (value 0 — field-storage is +//! zero-initialized) and **receives** a finalization token (the cell's value after +//! the last epoch that touched it). +//! +//! ## Why sparse (not dense like `GLOBAL_MEMORY`) +//! +//! RAM's `GLOBAL_MEMORY` is dense — one preprocessed row per byte of a page — so +//! `(address)` uniqueness is automatic. Field-storage lives in a 64-bit address +//! space across three domains, which cannot be enumerated densely, so this table is +//! **sparse**: one committed row per touched cell. Uniqueness of `(domain, addr)` +//! must therefore be enforced explicitly, with the same sorted-keys argument +//! FEXT_PAGE uses (see `fext_page.rs`). Without it a prover could emit two genesis +//! tokens for one cell and let a later epoch re-read 0 — an unsound mid-run reset. +//! +//! ## Soundness sketch +//! +//! The `GlobalFieldMemory` bus balances over the whole global proof iff, per cell: +//! - exactly one genesis send `[domain, addr, 0, GENESIS]` (this table, value pinned +//! to the constant 0), consumed by the first-touching epoch's init receiver +//! (init_epoch = GENESIS); +//! - the telescoping `fini(epoch i) == init(epoch i+1)` holds (FEXT_PAGE tokens); +//! - exactly one final receive `[domain, addr, fini_val, fini_epoch]` (this table), +//! consuming the last-touching epoch's fini send. +//! +//! Completeness (a row per touched cell) is forced by the bus: an omitted genesis +//! dangles the first init receiver; an omitted final dangles the last fini sender. +//! Uniqueness (no duplicate rows) is the sorted-keys argument here. `fini_val` and +//! `fini_epoch` are plain committed columns pinned by the bus match to FEXT_PAGE's +//! fini token (whose value is already canonical), exactly as `GLOBAL_MEMORY`'s +//! `FINI`/`FINI_EPOCH` are byte-checked transitively — do not add a redundant range +//! check on them here. +//! +//! ## Bus token (`GlobalFieldMemory`) +//! +//! `[domain, addr_lo, addr_hi, value, epoch]` — carries the domain (field-storage +//! spans 3/4/5, unlike RAM's domain-0-only `GlobalMemory`) and a full field-element +//! value. No timestamp: the cross-epoch chain is ordered by epoch. + +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; +use stark::lookup::{BusInteraction, BusValue, Multiplicity, Packing}; +use stark::trace::TraceTable; + +use super::bitwise::BitwiseOperation; +use super::fext_sorted_keys::{self, SortedKeysLayout}; +use super::local_to_global::GENESIS_EPOCH; +use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField, VmTable, zeroed_fe_vec}; + +/// Column layout for the shared `(domain, addr)` sorted-keys uniqueness argument. +const LAYOUT: SortedKeysLayout = SortedKeysLayout { + domain: cols::DOMAIN, + addr_0: cols::ADDR_0, + addr_1: cols::ADDR_1, + mu: cols::MU, + addr0_hw_lo: cols::ADDR0_HW_LO, + addr0_hw_hi: cols::ADDR0_HW_HI, + addr1_hw_lo: cols::ADDR1_HW_LO, + addr1_hw_hi: cols::ADDR1_HW_HI, + next_addr_0: cols::NEXT_ADDR_0, + next_addr_1: cols::NEXT_ADDR_1, + same_dom: cols::SAME_DOM, + sel_same: cols::SEL_SAME, +}; + +// ========================================================================= +// Column indices +// ========================================================================= + +/// Column indices for the GLOBAL_FIELD_MEMORY table (one row per touched cell). +pub mod cols { + /// Memory domain of this cell (3, 4, or 5). + pub const DOMAIN: usize = 0; + /// Cell address (DWordWL). + pub const ADDR_0: usize = 1; + pub const ADDR_1: usize = 2; + /// Final value after the last touching epoch (pinned by the bus). + pub const FINI_VAL: usize = 3; + /// Last epoch that touched the cell (pinned by the bus). + pub const FINI_EPOCH: usize = 4; + /// Multiplicity bit / real-row selector. + pub const MU: usize = 5; + + // --- uniqueness (sorted-keys) argument, mirroring FEXT_PAGE ------------- + /// Half-word decomposition of the two addr limbs, range-checked to `[0, 2^32)` + /// via `IsHalfword` so the addr `<` ALU lookup is sound. + pub const ADDR0_HW_LO: usize = 6; + pub const ADDR0_HW_HI: usize = 7; + pub const ADDR1_HW_LO: usize = 8; + pub const ADDR1_HW_HI: usize = 9; + /// The next row's addr limbs, copied in for the cross-row `addr < addr` compare. + pub const NEXT_ADDR_0: usize = 10; + pub const NEXT_ADDR_1: usize = 11; + /// 1 iff this row and the next share a domain. + pub const SAME_DOM: usize = 12; + /// `μ_next · same_dom`: gates the addr strict-increase LT. + pub const SEL_SAME: usize = 13; + + pub const NUM_COLUMNS: usize = 14; +} + +// ========================================================================= +// Types +// ========================================================================= + +/// One touched field-storage cell and its final state across the whole run. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct FieldCellFinal { + pub domain: u64, + pub addr: u64, + /// Final value (canonical field element) after the last touching epoch. + pub value: u64, + /// Label of the last epoch that touched the cell. + pub epoch: u64, +} + +// ========================================================================= +// Trace generation +// ========================================================================= + +/// Build the GLOBAL_FIELD_MEMORY trace: one row per touched cell, sorted strictly +/// ascending by `(domain, addr)` with active rows contiguous at the top, padded to +/// a power of two (min 4). Padding rows carry a valid domain (3) and `μ = 0` so the +/// ungated domain constraint holds and they fire no bus interactions. +pub fn generate_global_field_trace( + cells: &[FieldCellFinal], +) -> TraceTable { + let mut cells = cells.to_vec(); + cells.sort_by_key(|c| (c.domain, c.addr)); + + let num_rows = cells.len().next_power_of_two().max(4); + let mut trace = TraceTable::new_main( + zeroed_fe_vec(num_rows * cols::NUM_COLUMNS), + cols::NUM_COLUMNS, + 1, + ); + let table = &mut trace.main_table; + + for (row, c) in cells.iter().enumerate() { + table.set_fe(row, cols::DOMAIN, FE::from(c.domain)); + table.set_dword_wl(row, cols::ADDR_0, c.addr); + table.set_fe(row, cols::FINI_VAL, FE::from(c.value)); + table.set_fe(row, cols::FINI_EPOCH, FE::from(c.epoch)); + table.set_fe(row, cols::MU, FE::one()); + } + + // Shared sorted-keys columns: addr half-words, padding domain, cross-row helpers. + LAYOUT.fill_trace(table, cells.len(), num_rows); + + trace +} + +// ========================================================================= +// Bus interactions +// ========================================================================= + +fn direct(col: usize) -> BusValue { + BusValue::Packed { + start_column: col, + packing: Packing::Direct, + } +} + +/// Bus interactions on the cross-epoch `GlobalFieldMemory` bus (token +/// `[domain, addr_lo, addr_hi, value, epoch]`), plus the shared `(domain, addr)` +/// sorted-keys uniqueness lookups (addr-LT + addr-limb `IsHalfword`). Multiplicity +/// `MU`, so padding fires nothing. +pub fn bus_interactions() -> Vec { + let mut interactions = vec![ + // GFM-GENESIS: send the genesis token [domain, addr, 0, GENESIS]. Value and + // epoch are constants — genesis field-storage is zero, ordered below every + // real epoch — so neither is a prover-chosen column. + BusInteraction::sender( + BusId::GlobalFieldMemory, + Multiplicity::Column(cols::MU), + vec![ + direct(cols::DOMAIN), + direct(cols::ADDR_0), + direct(cols::ADDR_1), + BusValue::constant(0), + BusValue::constant(GENESIS_EPOCH), + ], + ), + // GFM-FINAL: receive the finalization token [domain, addr, fini_val, + // fini_epoch]. fini_val/fini_epoch are pinned by the match to FEXT_PAGE's + // fini sender (whose value is already canonical) — no redundant check here. + BusInteraction::receiver( + BusId::GlobalFieldMemory, + Multiplicity::Column(cols::MU), + vec![ + direct(cols::DOMAIN), + direct(cols::ADDR_0), + direct(cols::ADDR_1), + direct(cols::FINI_VAL), + direct(cols::FINI_EPOCH), + ], + ), + ]; + interactions.extend(LAYOUT.bus_interactions()); + interactions +} + +/// The BITWISE `IsHalfword` rows the anchor's addr-limb range checks send (4 per +/// cell), which the global proof's BITWISE provider must count. +pub fn collect_bitwise(cells: &[FieldCellFinal]) -> Vec { + fext_sorted_keys::collect_bitwise(cells.iter().map(|c| c.addr)) +} + +/// The addr `<` ALU LT ops the anchor's uniqueness sends (same-domain consecutive +/// cells), which the global proof's LT provider must receive. +pub fn collect_lt(cells: &[FieldCellFinal]) -> Vec { + fext_sorted_keys::collect_lt(cells.iter().map(|c| (c.domain, c.addr))) +} + +// ========================================================================= +// Constraints +// ========================================================================= + +/// GLOBAL_FIELD_MEMORY constraints. Per-row: `IS_BIT(μ)` (0), domain `∈ {3,4,5}` +/// (1), `IS_BIT(same_dom)` (2), addr-limb recompose (3, 4). Transition (exempting +/// the last row): `μ` non-increasing (5), `sel_same` definition (6), same-domain ⇒ +/// equal domain (7), domain increases by 1 or 2 on a change (8), next-addr copies +/// (9, 10). Per-row again: `IS_BIT(sel_same)` (11). Mirrors FEXT_PAGE's sorted-keys +/// uniqueness argument exactly. +pub struct GlobalFieldMemoryConstraints; + +impl ConstraintSet for GlobalFieldMemoryConstraints { + fn eval>(&self, b: &mut B) { + // The sparse anchor's entire constraint set is the shared sorted-keys + // uniqueness argument (indices 0..=11); the genesis-value and finalization + // bindings ride the GlobalFieldMemory bus, not extra AIR constraints. + LAYOUT.emit_constraints(b); + } + + fn max_degree(&self) -> usize { + 3 + } + + fn next_row_columns(&self) -> Vec { + vec![cols::DOMAIN, cols::ADDR_0, cols::ADDR_1, cols::MU] + } +} diff --git a/prover/src/tables/lt.rs b/prover/src/tables/lt.rs index 86e88a9f7..9ebc33a8c 100644 --- a/prover/src/tables/lt.rs +++ b/prover/src/tables/lt.rs @@ -165,7 +165,10 @@ pub fn generate_lt_trace( *op_map.entry(op.clone()).or_insert(0) += 1; } - let unique_ops: Vec<_> = op_map.into_iter().collect(); + // Canonical row order: HashMap iteration order is per-process random, so + // sort to keep the committed trace deterministic across runs. + let mut unique_ops: Vec<_> = op_map.into_iter().collect(); + unique_ops.sort_unstable_by_key(|(op, _)| (op.lhs, op.rhs, op.signed, op.invert)); let num_rows = unique_ops.len().next_power_of_two().max(4); let mut trace = TraceTable::new_main( crate::tables::types::zeroed_fe_vec(num_rows * cols::NUM_COLUMNS), diff --git a/prover/src/tables/mod.rs b/prover/src/tables/mod.rs index 0a86e4149..0bc44e911 100644 --- a/prover/src/tables/mod.rs +++ b/prover/src/tables/mod.rs @@ -32,6 +32,13 @@ pub mod dvrm; pub mod ecdas; pub mod ecsm; pub mod eq; +pub mod fext_fma; +pub mod fext_load; +pub mod fext_local_to_global; +pub mod fext_page; +pub mod fext_sorted_keys; +pub mod fext_store; +pub mod global_field_memory; pub mod global_memory; pub mod halt; pub mod keccak; diff --git a/prover/src/tables/mul.rs b/prover/src/tables/mul.rs index 181fba514..b60b4e1b8 100644 --- a/prover/src/tables/mul.rs +++ b/prover/src/tables/mul.rs @@ -303,7 +303,10 @@ pub fn generate_mul_trace( } } - let unique_ops: Vec<_> = op_map.into_iter().collect(); + // Canonical row order: HashMap iteration order is per-process random, so + // sort to keep the committed trace deterministic across runs. + let mut unique_ops: Vec<_> = op_map.into_iter().collect(); + unique_ops.sort_unstable_by_key(|(op, _)| (op.lhs, op.lhs_signed, op.rhs, op.rhs_signed)); let num_rows = unique_ops.len().next_power_of_two().max(4); let mut trace = TraceTable::new_main( crate::tables::types::zeroed_fe_vec(num_rows * cols::NUM_COLUMNS), diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 5c6b3085e..f06e935e8 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -50,6 +50,11 @@ use super::dvrm::{self, DvrmOperation}; use super::ecdas; use super::ecsm; use super::eq; +use super::fext_fma; +use super::fext_load; +use super::fext_local_to_global; +use super::fext_page; +use super::fext_store; use super::halt; use super::keccak::{self, KeccakOperation}; use super::keccak_rc; @@ -538,6 +543,7 @@ fn collect_ops_from_cpu( cpu_ops: &[CpuOperation], memory_state: &mut MemoryState, register_state: &mut RegisterState, + field_state: &mut FieldStorageState, ) -> ( MemwBuckets, Vec, @@ -549,6 +555,9 @@ fn collect_ops_from_cpu( Vec, Vec, Vec, + Vec, + Vec, + Vec, ) { let mut memw = MemwBuckets::with_register_capacity(cpu_ops.len() * 3); let mut load_ops = Vec::with_capacity(cpu_ops.len() / 8 + 1); @@ -560,6 +569,9 @@ fn collect_ops_from_cpu( let mut cpu32_ops = Vec::new(); let mut ecsm_ops = Vec::new(); let mut ecdas_ops = Vec::new(); + let mut fext_load_ops = Vec::new(); + let mut fext_fma_ops = Vec::new(); + let mut fext_store_ops = Vec::new(); // Seed from the carried x254 (0 for a monolithic run or the first epoch) so a // continuation epoch indexes its commits globally, matching the x254 the // register binding transports across epochs. Resetting to 0 here would drift @@ -654,6 +666,24 @@ fn collect_ops_from_cpu( ecdas_ops.extend(ecdas_rows); } + // Collect FEXT_LOAD / FEXT_FMA ecall operations (register reads + the + // field-storage access chain tracked in field_state). + if op.ecall_fext_load { + let (memw_ops, load_op) = collect_fext_load_ops(op, register_state, field_state); + memw.extend_ops(memw_ops); + fext_load_ops.push(load_op); + } + if op.ecall_fext_fma { + let (memw_ops, fma_op) = collect_fext_fma_ops(op, register_state, field_state); + memw.extend_ops(memw_ops); + fext_fma_ops.push(fma_op); + } + if op.ecall_fext_store { + let (memw_ops, store_op) = collect_fext_store_ops(op, register_state, field_state); + memw.extend_ops(memw_ops); + fext_store_ops.push(store_op); + } + // --- ALU chip dispatch (no state tracking) --- // Word (`*W`) instructions are delegated to CPU32 (which itself drives // the ALU chips); the main CPU does not send the ALU bus for them, so we @@ -709,6 +739,9 @@ fn collect_ops_from_cpu( cpu32_ops, ecsm_ops, ecdas_ops, + fext_load_ops, + fext_fma_ops, + fext_store_ops, ) } @@ -948,6 +981,252 @@ fn collect_ecsm_ops( (memw_ops, ecsm_op, ecdas_ops) } +/// Field-storage state for the FEXT accelerator: per cell `(domain, address)`, +/// the current value and the timestamp of the last access (mirrors +/// `MemoryState`/`RegisterState`). Field-storage rides the low-level `Memory` +/// bus directly, so this tracks the old_ts/old_val each access consumes and, at +/// the end, the final token every touched cell needs (`into_page_ops`). +#[derive(Default)] +struct FieldStorageState { + cells: HashMap<(u64, u64), (u64, u64)>, + /// Values carried in from the previous epoch (continuation only). A cell not yet + /// touched this epoch reads back its carried value (at ts=0), instead of 0. + /// Empty for monolithic proving, so `read` returns `(0, 0)` as before. + carried: HashMap<(u64, u64), u64>, +} + +impl FieldStorageState { + /// A state seeded with the previous epoch's final field-storage values (the + /// cross-epoch carry). Untouched cells read back their carried value at ts=0. + fn with_carried(carried: HashMap<(u64, u64), u64>) -> Self { + Self { + cells: HashMap::new(), + carried, + } + } + + /// Current `(value, last_ts)` of a cell. If untouched this epoch, its carried + /// value at ts=0 (the epoch-start seed the bookend init token emits) — `(0, 0)` + /// when there is no carry (monolithic, or a genesis cell). + fn read(&self, domain: u64, addr: u64) -> (u64, u64) { + self.cells + .get(&(domain, addr)) + .copied() + .unwrap_or_else(|| (self.carried.get(&(domain, addr)).copied().unwrap_or(0), 0)) + } + + /// Record an access at `ts` that leaves `value` in the cell. + fn write(&mut self, domain: u64, addr: u64, value: u64, ts: u64) { + self.cells.insert((domain, addr), (value, ts)); + } + + /// One `FEXT_PAGE` row per touched cell, in deterministic `(domain, addr)` + /// order (monolithic bookend). + fn into_page_ops(self) -> Vec { + let mut ops: Vec<_> = self + .cells + .into_iter() + .map( + |((domain, addr), (final_val, final_ts))| fext_page::FextPageOperation { + domain, + addr, + final_ts, + final_val, + }, + ) + .collect(); + ops.sort_by_key(|o| (o.domain, o.addr)); + ops + } + + /// This epoch's touched field cells as `(domain, addr, final_val, final_ts)`, + /// in deterministic `(domain, addr)` order — the continuation carry's per-epoch + /// touch set (the driver turns it into `FextLocalToGlobal` boundaries). The + /// per-cell init value comes from the driver's field provenance, not here. + fn into_touched_field_cells(self) -> fext_local_to_global::FieldTouches { + let mut touches: fext_local_to_global::FieldTouches = self + .cells + .into_iter() + .map(|((domain, addr), (final_val, final_ts))| (domain, addr, final_val, final_ts)) + .collect(); + touches.sort_by_key(|&(domain, addr, _, _)| (domain, addr)); + touches + } +} + +/// Register reads (shared MEMW) for x10..x13 of a FEXT ecall at timestamp `t`. +fn fext_register_reads(register_state: &mut RegisterState, t: u64) -> Vec { + let mut ops = Vec::with_capacity(4); + for reg in 10..=13u8 { + let (val, old_ts) = register_state.read(reg); + let value = pack_register_value(val); + ops.push( + MemwOperation::new(true, 2 * reg as u64, value, t, 2, true) + .with_old(value, [old_ts, old_ts, 0, 0, 0, 0, 0, 0]), + ); + register_state.write(reg, val, t); + } + ops +} + +/// Collects the register reads + the FEXT_LOAD operation. Field-storage writes +/// are emitted by the chip on the `Memory` bus; here we advance `field_state` +/// and record the old_ts/old_val each write consumes. +fn collect_fext_load_ops( + op: &CpuOperation, + register_state: &mut RegisterState, + field_state: &mut FieldStorageState, +) -> (Vec, fext_load::FextLoadOperation) { + let t = op.timestamp; + let addr = register_state.read(10).0; + let coeffs = [ + register_state.read(11).0, + register_state.read(12).0, + register_state.read(13).0, + ]; + let memw_ops = fext_register_reads(register_state, t); + + let mut old_ts = [0u64; 3]; + let mut old_val = [0u64; 3]; + for i in 0..3 { + let domain = 3 + i as u64; + let (v, ts) = field_state.read(domain, addr); + old_val[i] = v; + old_ts[i] = ts; + field_state.write(domain, addr, coeffs[i], t); + } + + ( + memw_ops, + fext_load::FextLoadOperation { + timestamp: t, + addr, + coeffs, + old_ts, + old_val, + }, + ) +} + +/// Collects the register reads + the FEXT_FMA operation (9 field reads + 3 +/// writes on the `Memory` bus, tracked in `field_state`). +fn collect_fext_fma_ops( + op: &CpuOperation, + register_state: &mut RegisterState, + field_state: &mut FieldStorageState, +) -> (Vec, fext_fma::FextFmaOperation) { + let t = op.timestamp; + let a_addr = register_state.read(10).0; + let b_addr = register_state.read(11).0; + let c_addr = register_state.read(12).0; + let out_addr = register_state.read(13).0; + let memw_ops = fext_register_reads(register_state, t); + + // Read a, b, c (9 cells); a read re-emits the cell's token at t. + let in_addrs = [a_addr, b_addr, c_addr]; + let mut vals = [[0u64; 3]; 3]; + let mut read_old_ts = [[0u64; 3]; 3]; + for (v, &addr) in in_addrs.iter().enumerate() { + for d in 0..3 { + let domain = 3 + d as u64; + let (value, ts) = field_state.read(domain, addr); + vals[v][d] = value; + read_old_ts[v][d] = ts; + field_state.write(domain, addr, value, t); + } + } + + let output = executor::vm::instruction::execution::fext_fma(vals[0], vals[1], vals[2]); + + // Write output to (3+d, out_addr). + let mut write_old_ts = [0u64; 3]; + let mut write_old_val = [0u64; 3]; + for d in 0..3 { + let domain = 3 + d as u64; + let (v, ts) = field_state.read(domain, out_addr); + write_old_val[d] = v; + write_old_ts[d] = ts; + field_state.write(domain, out_addr, output[d], t); + } + + ( + memw_ops, + fext_fma::FextFmaOperation { + timestamp: t, + out_addr, + a_addr, + b_addr, + c_addr, + a: vals[0], + b: vals[1], + c: vals[2], + output, + read_old_ts, + write_old_ts, + write_old_val, + }, + ) +} + +/// Collects the register read (x10) + register writes (a1/a2/a3) + the FEXT_STORE +/// operation. Reads 3 field-storage cells (re-emitting each token at `t`) and +/// writes their coefficients back to registers. +fn collect_fext_store_ops( + op: &CpuOperation, + register_state: &mut RegisterState, + field_state: &mut FieldStorageState, +) -> (Vec, fext_store::FextStoreOperation) { + let t = op.timestamp; + let src_addr = register_state.read(10).0; + + let mut memw_ops = Vec::with_capacity(4); + // Register read x10 (source address) at t. + { + let (val, old_ts) = register_state.read(10); + let value = pack_register_value(val); + memw_ops.push( + MemwOperation::new(true, 2 * 10, value, t, 2, true) + .with_old(value, [old_ts, old_ts, 0, 0, 0, 0, 0, 0]), + ); + register_state.write(10, val, t); + } + + // Read the 3 field cells (a read re-emits the token at t). + let mut coeffs = [0u64; 3]; + let mut old_ts = [0u64; 3]; + for d in 0..3 { + let domain = 3 + d as u64; + let (value, ts) = field_state.read(domain, src_addr); + coeffs[d] = value; + old_ts[d] = ts; + field_state.write(domain, src_addr, value, t); + } + + // Write the coefficients back to registers a1/a2/a3 (x11/x12/x13). + for (d, &coeff) in coeffs.iter().enumerate() { + let reg = 11 + d as u8; + let (old_val, old_reg_ts) = register_state.read(reg); + let new_value = pack_register_value(coeff); + memw_ops.push( + MemwOperation::new(true, 2 * reg as u64, new_value, t, 2, false).with_old( + pack_register_value(old_val), + [old_reg_ts, old_reg_ts, 0, 0, 0, 0, 0, 0], + ), + ); + register_state.write(reg, coeff, t); + } + + ( + memw_ops, + fext_store::FextStoreOperation { + timestamp: t, + src_addr, + coeffs, + old_ts, + }, + ) +} + /// Collects register read/write operations (M1, M3, M5) from CpuOperation, /// pushing them into `memw_ops`. fn collect_register_ops_from_cpu( @@ -1484,6 +1763,119 @@ fn collect_lt_from_memw_aligned(memw_aligned_ops: &[MemwOperation]) -> Vec Vec { + let mut lt_ops = Vec::with_capacity(ops.len() * 6); + for op in ops { + for i in 0..3 { + lt_ops.push(LtOperation::new( + op.coeffs[i], + math::field::goldilocks::GOLDILOCKS_PRIME, + false, + )); + lt_ops.push(LtOperation::new(op.old_ts[i], op.timestamp, false)); + } + } + lt_ops +} + +/// LT provider rows for the FEXT_FMA chip's ALU lookups: `old_ts < ts` for each +/// of the 9 reads and 3 writes. +fn collect_lt_from_fext_fma(ops: &[fext_fma::FextFmaOperation]) -> Vec { + let mut lt_ops = Vec::with_capacity(ops.len() * 12); + for op in ops { + for v in 0..3 { + for d in 0..3 { + lt_ops.push(LtOperation::new(op.read_old_ts[v][d], op.timestamp, false)); + } + } + for d in 0..3 { + lt_ops.push(LtOperation::new(op.write_old_ts[d], op.timestamp, false)); + } + } + lt_ops +} + +/// LT provider rows for the FEXT_STORE chip's ALU lookups: `old_ts < ts` for each +/// of the 3 field reads. (The register read/write LT checks are handled by the +/// shared MEMW machinery.) +fn collect_lt_from_fext_store(ops: &[fext_store::FextStoreOperation]) -> Vec { + let mut lt_ops = Vec::with_capacity(ops.len() * 6); + for op in ops { + for d in 0..3 { + // coeff < p (read-back canonicality) + old_ts < ts (temporal order). + lt_ops.push(LtOperation::new( + op.coeffs[d], + math::field::goldilocks::GOLDILOCKS_PRIME, + false, + )); + lt_ops.push(LtOperation::new(op.old_ts[d], op.timestamp, false)); + } + } + lt_ops +} + +/// BITWISE `IsHalfword` provider rows for the FEXT_STORE chip: each read-back +/// coefficient's two 32-bit words are split into 16-bit halves that the chip +/// range-checks (12 per op). +fn collect_bitwise_from_fext_store( + ops: &[fext_store::FextStoreOperation], +) -> Vec { + let mut bitwise_ops = Vec::with_capacity(ops.len() * 12); + for op in ops { + for d in 0..3 { + for word in [op.coeffs[d] & 0xFFFF_FFFF, op.coeffs[d] >> 32] { + for hv in [word & 0xFFFF, (word >> 16) & 0xFFFF] { + bitwise_ops.push(BitwiseOperation::halfword( + BitwiseOperationType::IsHalf, + (hv & 0xFF) as u8, + (hv >> 8) as u8, + )); + } + } + } + } + bitwise_ops +} + +/// ALU `LT` provider rows for the FEXT_PAGE uniqueness argument: for each +/// same-domain adjacent pair (in the sorted `(domain, addr)` order the table +/// emits), the chip proves `addr[i] < addr[i+1]`. Sorting here MUST match +/// [`fext_page::generate_fext_page_trace`] so the sent and provided lookups line +/// up. +fn collect_lt_from_fext_page(ops: &[fext_page::FextPageOperation]) -> Vec { + let mut sorted = ops.to_vec(); + sorted.sort_by_key(|o| (o.domain, o.addr)); + let mut lt_ops = Vec::new(); + for pair in sorted.windows(2) { + if pair[0].domain == pair[1].domain { + lt_ops.push(LtOperation::new(pair[0].addr, pair[1].addr, false)); + } + } + lt_ops +} + +/// BITWISE `IsHalfword` provider rows for the FEXT_PAGE uniqueness argument: each +/// touched cell's 64-bit address is split into two 32-bit limbs and then 16-bit +/// halves that the chip range-checks (4 per op), pinning the addr limbs so the +/// `addr <` ALU lookup is sound. +fn collect_bitwise_from_fext_page(ops: &[fext_page::FextPageOperation]) -> Vec { + let mut bitwise_ops = Vec::with_capacity(ops.len() * 4); + for op in ops { + for word in [op.addr & 0xFFFF_FFFF, op.addr >> 32] { + for hv in [word & 0xFFFF, (word >> 16) & 0xFFFF] { + bitwise_ops.push(BitwiseOperation::halfword( + BitwiseOperationType::IsHalf, + (hv & 0xFF) as u8, + (hv >> 8) as u8, + )); + } + } + } + bitwise_ops +} + /// Checks whether a MEMW operation qualifies for the aligned fast path (MEMW_A). /// /// An operation is aligned if: @@ -1594,7 +1986,7 @@ fn reg_ts_delta_in_range(timestamp: u64, old_ts: u64) -> bool { /// Collects bitwise lookups from LT operations (MSB16 and IS_HALFWORD). /// /// Returns: Vec of bitwise lookups -fn collect_bitwise_from_lt(lt_ops: &[LtOperation]) -> Vec { +pub(crate) fn collect_bitwise_from_lt(lt_ops: &[LtOperation]) -> Vec { let mut bitwise_ops = Vec::with_capacity(lt_ops.len() * 8); for op in lt_ops { @@ -2079,7 +2471,12 @@ pub(crate) fn epoch_touched_cells( let mut memory_state = MemoryState::from_image(initial_image); let mut register_state = RegisterState::from_init(register_init); - let _ = collect_ops_from_cpu(&cpu_ops, &mut memory_state, &mut register_state); + let _ = collect_ops_from_cpu( + &cpu_ops, + &mut memory_state, + &mut register_state, + &mut FieldStorageState::default(), + ); Ok(touched_cells_from_memory_state(&memory_state)) } @@ -2723,6 +3120,18 @@ pub struct Traces { /// ECDAS double/add table (variable rows per ecall) pub ecdas: TraceTable, + /// FEXT_LOAD table (one row per FEXT_LOAD ecall) + pub fext_load: TraceTable, + + /// FEXT_FMA table (one row per FEXT_FMA ecall) + pub fext_fma: TraceTable, + + /// FEXT_STORE table (one row per FEXT_STORE ecall) + pub fext_store: TraceTable, + + /// FEXT_PAGE bookend table (one row per touched field-storage cell) + pub fext_page: TraceTable, + /// MEMW_R register-only fast-path traces (split into chunks of max_rows::MEMW_R) pub memw_registers: Vec>, /// Local-to-global boundary table for continuation epochs. Empty unless the @@ -2733,6 +3142,14 @@ pub struct Traces { /// `(address, end_value, end_timestamp)`. Populated only for continuation /// epochs that use the L2G memory bookend. pub touched_memory_cells: local_to_global::EpochTouches, + /// Per-epoch field-storage bookend for continuation epochs (the field-storage + /// analog of `local_to_global`). Empty unless the continuation driver fills it + /// with the boundary derived from `touched_field_cells`. + pub fext_local_to_global: TraceTable, + /// Touched field-storage cells observed this epoch, each as + /// `(domain, addr, final_value, final_ts)`. Populated only for continuation + /// epochs (used by the driver to build the field boundary + carry). + pub touched_field_cells: fext_local_to_global::FieldTouches, // Auxiliary ALU / memory / CPU32 dispatch chips (split into chunks of their max_rows) pub eqs: Vec>, pub bytewises: Vec>, @@ -2765,6 +3182,11 @@ struct CollectedOps { // EC scalar-multiplication accelerator chips. ecsm_ops: Vec, ecdas_ops: Vec, + // Field-extension accelerator chips. + fext_load_ops: Vec, + fext_fma_ops: Vec, + fext_store_ops: Vec, + fext_page_ops: Vec, } /// Chunk raw ops and generate one trace table per chunk. When `storage_mode` @@ -2819,6 +3241,10 @@ fn collect_all_ops( cpu32_ops: Vec, ecsm_ops: Vec, ecdas_ops: Vec, + fext_load_ops: Vec, + fext_fma_ops: Vec, + fext_store_ops: Vec, + fext_page_ops: Vec, register_state: &mut RegisterState, is_final: bool, ) -> CollectedOps { @@ -2961,6 +3387,10 @@ fn collect_all_ops( cpu32_ops, ecsm_ops, ecdas_ops, + fext_load_ops, + fext_fma_ops, + fext_store_ops, + fext_page_ops, } } @@ -2983,7 +3413,11 @@ fn build_traces( private_input: &[u8], is_final: bool, l2g_memory_bookend: bool, + touched_field_cells: fext_local_to_global::FieldTouches, ) -> Result { + // Field-storage is now carried across continuation epochs (the fext_local_to_global + // bookend + GlobalFieldMemory aggregation), so FEXT accelerator ecalls are sound + // under continuation — no interim guard here. let CollectedOps { cpu_ops, memw_ops, @@ -3004,6 +3438,10 @@ fn build_traces( cpu32_ops, ecsm_ops, ecdas_ops, + fext_load_ops, + fext_fma_ops, + fext_store_ops, + fext_page_ops, } = ops; // ===================================================================== @@ -3011,6 +3449,15 @@ fn build_traces( // ===================================================================== lt_ops.extend(collect_lt_from_memw(&memw_ops)); lt_ops.extend(collect_lt_from_memw_aligned(&memw_aligned_ops)); + lt_ops.extend(collect_lt_from_fext_load(&fext_load_ops)); + lt_ops.extend(collect_lt_from_fext_fma(&fext_fma_ops)); + lt_ops.extend(collect_lt_from_fext_store(&fext_store_ops)); + lt_ops.extend(collect_lt_from_fext_page(&fext_page_ops)); + // Continuation field bookend (fext_local_to_global): the addr-LT uniqueness ops, + // known from the sorted touched cells at build time (empty for monolithic). + lt_ops.extend(fext_local_to_global::collect_lt_from_touches( + &touched_field_cells, + )); // ===================================================================== // PHASE 4: All → Bitwise lookups @@ -3079,6 +3526,8 @@ fn build_traces( Box::new(|h| h.add_ops(&collect_bitwise_from_keccak(&keccak_ops))), Box::new(|h| h.add_ops(&collect_bitwise_from_ecsm(&ecsm_ops))), Box::new(|h| h.add_ops(&collect_bitwise_from_ecdas(&ecdas_ops))), + Box::new(|h| h.add_ops(&collect_bitwise_from_fext_store(&fext_store_ops))), + Box::new(|h| h.add_ops(&collect_bitwise_from_fext_page(&fext_page_ops))), Box::new(|h| add_padding_byte_checks(h, num_padding_rows)), ]; if let Some(image) = initial_image @@ -3365,6 +3814,11 @@ fn build_traces( // ECSM accelerator traces (empty/all-padding for programs that do not use ECSM). let gen_ecsm = || ecsm::generate_ecsm_trace(&ecsm_ops); let gen_ecdas = || ecdas::generate_ecdas_trace(&ecdas_ops); + // FEXT accelerator traces (empty/all-padding when unused). + let gen_fext_load = || fext_load::generate_fext_load_trace(&fext_load_ops); + let gen_fext_fma = || fext_fma::generate_fext_fma_trace(&fext_fma_ops); + let gen_fext_store = || fext_store::generate_fext_store_trace(&fext_store_ops); + let gen_fext_page = || fext_page::generate_fext_page_trace(&fext_page_ops); let (mut cpus_slot, mut memws_slot, mut memw_aligneds_slot, mut memw_registers_slot) = (None, None, None, None); @@ -3377,6 +3831,8 @@ fn build_traces( let (mut eqs_slot, mut bytewises_slot, mut stores_slot, mut cpu32s_slot) = (None, None, None, None); let (mut ecsm_slot, mut ecdas_slot) = (None, None); + let (mut fext_load_slot, mut fext_fma_slot, mut fext_page_slot) = (None, None, None); + let mut fext_store_slot = None; #[cfg(feature = "disk-spill")] let sequential = storage_mode == StorageMode::Disk || cfg!(not(feature = "parallel")); @@ -3418,6 +3874,10 @@ fn build_traces( spawn_into!(cpu32s_slot, gen_cpu32s); spawn_into!(ecsm_slot, gen_ecsm); spawn_into!(ecdas_slot, gen_ecdas); + spawn_into!(fext_load_slot, gen_fext_load); + spawn_into!(fext_fma_slot, gen_fext_fma); + spawn_into!(fext_store_slot, gen_fext_store); + spawn_into!(fext_page_slot, gen_fext_page); }); } else { cpus_slot = Some(gen_cpus()); @@ -3445,6 +3905,10 @@ fn build_traces( cpu32s_slot = Some(gen_cpu32s()); ecsm_slot = Some(gen_ecsm()); ecdas_slot = Some(gen_ecdas()); + fext_load_slot = Some(gen_fext_load()); + fext_fma_slot = Some(gen_fext_fma()); + fext_store_slot = Some(gen_fext_store()); + fext_page_slot = Some(gen_fext_page()); } const PHASE5_RAN: &str = "phase 5 generation ran in one of the branches above"; @@ -3479,6 +3943,10 @@ fn build_traces( let mut halt_trace = halt_slot.expect(PHASE5_RAN); let ecsm_trace = ecsm_slot.expect(PHASE5_RAN); let ecdas_trace = ecdas_slot.expect(PHASE5_RAN); + let fext_load_trace = fext_load_slot.expect(PHASE5_RAN); + let fext_fma_trace = fext_fma_slot.expect(PHASE5_RAN); + let fext_store_trace = fext_store_slot.expect(PHASE5_RAN); + let fext_page_trace = fext_page_slot.expect(PHASE5_RAN); // Fixed-size and per-page tables aren't built through `chunk_and_generate`, // so spill them here before returning. @@ -3520,6 +3988,9 @@ fn build_traces( Vec::new() }; let local_to_global = local_to_global::generate_local_to_global_trace(&[]); + // Like `local_to_global`: the driver installs the real field bookend trace after + // applying field provenance. Build an empty placeholder here. + let fext_local_to_global = fext_local_to_global::generate_fext_local_to_global_trace(&[]); #[cfg(feature = "instruments")] drop(__sp); @@ -3546,9 +4017,15 @@ fn build_traces( keccak_rc: keccak_rc_trace, ecsm: ecsm_trace, ecdas: ecdas_trace, + fext_load: fext_load_trace, + fext_fma: fext_fma_trace, + fext_store: fext_store_trace, + fext_page: fext_page_trace, memw_registers, local_to_global, touched_memory_cells, + fext_local_to_global, + touched_field_cells, eqs, bytewises, stores, @@ -3589,6 +4066,10 @@ pub struct TableLengths { pub dvrm_padded_rows: u64, pub branch_padded_rows: u64, pub commit_padded_rows: u64, + pub fext_load_padded_rows: u64, + pub fext_fma_padded_rows: u64, + pub fext_store_padded_rows: u64, + pub fext_page_padded_rows: u64, pub decode_rows: u64, pub unique_page_count: u64, pub cycle_count: u64, @@ -3629,6 +4110,12 @@ pub fn count_table_lengths( let mut branch_count = 0usize; let mut commit_count = 0usize; let mut current_commit_index = 0u32; + // FEXT accelerator: one table row per ecall, plus the field-storage access + // chain tracked in `field_state` (its unique cells become FEXT_PAGE rows). + let mut fext_load_count = 0usize; + let mut fext_fma_count = 0usize; + let mut fext_store_count = 0usize; + let mut field_state = FieldStorageState::default(); let partition_memw = |op: &MemwOperation, by_width: &mut [usize; 4], @@ -3719,6 +4206,49 @@ pub fn count_table_lengths( .ok_or_else(|| Error::Execution("commit index exceeds u32 range".into()))?; } + // FEXT accelerator ecalls: mirror `build_traces` — the collectors do the + // register reads and field-storage accesses (into `field_state`), and we + // partition their MEMW ops exactly as the trace build does. + if cpu_op.ecall_fext_load { + let (memw_ops, _) = + collect_fext_load_ops(&cpu_op, &mut register_state, &mut field_state); + for memw_op in &memw_ops { + partition_memw( + memw_op, + &mut memw_by_width, + &mut memw_aligned_count, + &mut memw_register_count, + ); + } + fext_load_count += 1; + } + if cpu_op.ecall_fext_fma { + let (memw_ops, _) = + collect_fext_fma_ops(&cpu_op, &mut register_state, &mut field_state); + for memw_op in &memw_ops { + partition_memw( + memw_op, + &mut memw_by_width, + &mut memw_aligned_count, + &mut memw_register_count, + ); + } + fext_fma_count += 1; + } + if cpu_op.ecall_fext_store { + let (memw_ops, _) = + collect_fext_store_ops(&cpu_op, &mut register_state, &mut field_state); + for memw_op in &memw_ops { + partition_memw( + memw_op, + &mut memw_by_width, + &mut memw_aligned_count, + &mut memw_register_count, + ); + } + fext_store_count += 1; + } + // CPU-side per-instruction-kind counters (non-word; word → CPU32, B5b) let f = &cpu_op.decode.fields; if !f.word_instr && f.is_lt() { @@ -3759,6 +4289,15 @@ pub fn count_table_lengths( mul_count += 2 * dvrm_count; lt_count += dvrm_count; + // FEXT field-storage accesses each send an `old_ts < ts` LT (temporal + // ordering): 3 per LOAD (writes), 12 per FMA (9 reads + 3 writes), 3 per + // STORE (reads) — see each table's `Alu` bus interactions. FEXT_PAGE's + // sorted-keys uniqueness sends at most one addr-LT per touched cell. Upper + // bound on the LT rows these add (LT dedups, so `>=` actual, as the drift + // test requires). + let fext_page_count = field_state.cells.len(); + lt_count += 3 * fext_load_count + 12 * fext_fma_count + 3 * fext_store_count + fext_page_count; + let unique_page_count = memory_state.unique_page_count(page::DEFAULT_PAGE_SIZE as u64); let unique_byte_count = memory_state.cells.len() as u64; let cycle_count = logs.len() as u64; @@ -3778,6 +4317,23 @@ pub fn count_table_lengths( .checked_next_power_of_two() .unwrap_or(usize::MAX) .max(4) as u64, + // FEXT tables pad `count.next_power_of_two().max(4)` (no chunking). + fext_load_padded_rows: fext_load_count + .checked_next_power_of_two() + .unwrap_or(usize::MAX) + .max(4) as u64, + fext_fma_padded_rows: fext_fma_count + .checked_next_power_of_two() + .unwrap_or(usize::MAX) + .max(4) as u64, + fext_store_padded_rows: fext_store_count + .checked_next_power_of_two() + .unwrap_or(usize::MAX) + .max(4) as u64, + fext_page_padded_rows: fext_page_count + .checked_next_power_of_two() + .unwrap_or(usize::MAX) + .max(4) as u64, decode_rows, unique_page_count, cycle_count, @@ -3807,6 +4363,10 @@ impl Traces { use super::ecdas::cols::NUM_COLUMNS as ECDAS_COLS; use super::ecsm::cols::NUM_COLUMNS as ECSM_COLS; use super::eq::cols::NUM_COLUMNS as EQ_COLS; + use super::fext_fma::cols::NUM_COLUMNS as FEXT_FMA_COLS; + use super::fext_load::cols::NUM_COLUMNS as FEXT_LOAD_COLS; + use super::fext_page::cols::NUM_COLUMNS as FEXT_PAGE_COLS; + use super::fext_store::cols::NUM_COLUMNS as FEXT_STORE_COLS; use super::halt::cols::NUM_COLUMNS as HALT_COLS; use super::keccak::cols::NUM_COLUMNS as KECCAK_COLS; use super::keccak_rc::NUM_PRECOMPUTED_COLS as KECCAK_RC_PRECOMPUTED; @@ -3846,6 +4406,10 @@ impl Traces { keccak_rc, ecsm, ecdas, + fext_load, + fext_fma, + fext_store, + fext_page, memw_registers, eqs, bytewises, @@ -3855,6 +4419,8 @@ impl Traces { public_output_bytes: _, local_to_global: _, touched_memory_cells: _, + fext_local_to_global: _, + touched_field_cells: _, } = self; let mut total: u64 = 0; @@ -3913,6 +4479,10 @@ impl Traces { } total += (ecsm.num_rows() * ECSM_COLS) as u64; total += (ecdas.num_rows() * ECDAS_COLS) as u64; + total += (fext_load.num_rows() * FEXT_LOAD_COLS) as u64; + total += (fext_fma.num_rows() * FEXT_FMA_COLS) as u64; + total += (fext_store.num_rows() * FEXT_STORE_COLS) as u64; + total += (fext_page.num_rows() * FEXT_PAGE_COLS) as u64; total } @@ -3954,6 +4524,10 @@ impl Traces { let n_cpu32 = aux_cols(super::cpu32::bus_interactions().len()); let n_ecsm = aux_cols(super::ecsm::bus_interactions().len()); let n_ecdas = aux_cols(super::ecdas::bus_interactions().len()); + let n_fext_load = aux_cols(super::fext_load::bus_interactions().len()); + let n_fext_fma = aux_cols(super::fext_fma::bus_interactions().len()); + let n_fext_store = aux_cols(super::fext_store::bus_interactions().len()); + let n_fext_page = aux_cols(super::fext_page::bus_interactions().len()); let Traces { cpus, @@ -3976,6 +4550,10 @@ impl Traces { keccak_rc, ecsm, ecdas, + fext_load, + fext_fma, + fext_store, + fext_page, memw_registers, eqs, bytewises, @@ -3985,6 +4563,8 @@ impl Traces { public_output_bytes: _, local_to_global: _, touched_memory_cells: _, + fext_local_to_global: _, + touched_field_cells: _, } = self; let mut total: u64 = 0; @@ -4043,6 +4623,10 @@ impl Traces { } total += (ecsm.num_rows() * n_ecsm) as u64; total += (ecdas.num_rows() * n_ecdas) as u64; + total += (fext_load.num_rows() * n_fext_load) as u64; + total += (fext_fma.num_rows() * n_fext_fma) as u64; + total += (fext_store.num_rows() * n_fext_store) as u64; + total += (fext_page.num_rows() * n_fext_page) as u64; total } @@ -4211,6 +4795,12 @@ impl Traces { /// `is_final` marks the last epoch: it applies HALT finalization (zeroize /// registers, require the terminating ECALL). Intermediate epochs (`false`) /// skip HALT and keep their boundary register/memory state. + /// + /// Field-storage carry: without a carried image (this delegate), a continuation + /// epoch reads field cells back as zero — only sound if the program uses no FEXT + /// accelerator ecalls. The continuation driver calls + /// [`Self::from_image_and_logs_carried`] with the previous epoch's final field + /// values instead. #[allow(clippy::too_many_arguments)] pub fn from_image_and_logs( elf: &Elf, @@ -4222,6 +4812,38 @@ impl Traces { is_final: bool, l2g_memory_bookend: bool, #[cfg(feature = "disk-spill")] storage_mode: StorageMode, + ) -> Result { + Self::from_image_and_logs_carried( + elf, + initial_image, + register_init, + logs, + max_rows, + private_input, + is_final, + l2g_memory_bookend, + &HashMap::new(), + #[cfg(feature = "disk-spill")] + storage_mode, + ) + } + + /// Like [`Self::from_image_and_logs`] but seeds field-storage from `carried_field` + /// (the previous epoch's final `(domain, addr) -> value`), so FEXT accelerator + /// ecalls read the carried value instead of zero. Under continuation the driver + /// derives the field boundary + cross-epoch carry from `Traces::touched_field_cells`. + #[allow(clippy::too_many_arguments)] + pub fn from_image_and_logs_carried( + elf: &Elf, + initial_image: &I, + register_init: &[u32], + logs: &[Log], + max_rows: &super::MaxRowsConfig, + private_input: &[u8], + is_final: bool, + l2g_memory_bookend: bool, + carried_field: &HashMap<(u64, u64), u64>, + #[cfg(feature = "disk-spill")] storage_mode: StorageMode, ) -> Result { // A non-final epoch must not contain the program-terminating instruction // (next_pc == 0). Otherwise the CPU sends an ECALL bus token with no HALT @@ -4254,6 +4876,7 @@ impl Traces { let mut register_state = RegisterState::from_init(register_init); #[cfg(feature = "instruments")] let __sp = stark::instruments::span("p2a_collect_cpu"); + let mut field_state = FieldStorageState::with_carried(carried_field.clone()); let ( memw_ops, load_ops, @@ -4265,10 +4888,30 @@ impl Traces { cpu32_ops, ecsm_ops, ecdas_ops, - ) = collect_ops_from_cpu(&cpu_ops, &mut memory_state, &mut register_state); + fext_load_ops, + fext_fma_ops, + fext_store_ops, + ) = collect_ops_from_cpu( + &cpu_ops, + &mut memory_state, + &mut register_state, + &mut field_state, + ); #[cfg(feature = "instruments")] drop(__sp); + // Monolithic runs bookend field-storage with FEXT_PAGE; continuation epochs + // skip FEXT_PAGE (empty ops) and hand the touched cells to the driver, which + // builds the fext_local_to_global bookend + the cross-epoch carry. + let (fext_page_ops, touched_field_cells) = if l2g_memory_bookend { + (Vec::new(), field_state.into_touched_field_cells()) + } else { + ( + field_state.into_page_ops(), + fext_local_to_global::FieldTouches::new(), + ) + }; + #[cfg(feature = "instruments")] let __sp = stark::instruments::span("p2b_collect_all"); let ops = collect_all_ops( @@ -4283,6 +4926,10 @@ impl Traces { cpu32_ops, ecsm_ops, ecdas_ops, + fext_load_ops, + fext_fma_ops, + fext_store_ops, + fext_page_ops, &mut register_state, is_final, ); @@ -4306,6 +4953,7 @@ impl Traces { private_input, is_final, l2g_memory_bookend, + touched_field_cells, ); #[cfg(feature = "instruments")] drop(__sp); @@ -4331,6 +4979,7 @@ impl Traces { let entry_point = cpu_ops.first().map_or(0, |op| op.decode.pc); let register_init = register::register_init_from_entry_point(entry_point); let mut register_state = RegisterState::new(entry_point); + let mut field_state = FieldStorageState::default(); let ( memw_ops, load_ops, @@ -4342,7 +4991,15 @@ impl Traces { cpu32_ops, ecsm_ops, ecdas_ops, - ) = collect_ops_from_cpu(&cpu_ops, &mut memory_state, &mut register_state); + fext_load_ops, + fext_fma_ops, + fext_store_ops, + ) = collect_ops_from_cpu( + &cpu_ops, + &mut memory_state, + &mut register_state, + &mut field_state, + ); let ops = collect_all_ops( cpu_ops, @@ -4356,6 +5013,10 @@ impl Traces { cpu32_ops, ecsm_ops, ecdas_ops, + fext_load_ops, + fext_fma_ops, + fext_store_ops, + field_state.into_page_ops(), &mut register_state, true, ); @@ -4378,6 +5039,7 @@ impl Traces { &[], true, false, + fext_local_to_global::FieldTouches::new(), ) } } diff --git a/prover/src/tables/types.rs b/prover/src/tables/types.rs index fab4aabff..f8c0c8ad0 100644 --- a/prover/src/tables/types.rs +++ b/prover/src/tables/types.rs @@ -359,6 +359,12 @@ pub enum BusId { /// Cross-epoch memory bus: the local-to-global table's per-cell init/fini /// boundary claims, matched across epochs by the final aggregation LogUp. GlobalMemory = 31, + /// Cross-epoch field-storage bus: the FEXT_PAGE per-cell init/fini boundary + /// claims for memory domains 3/4/5, matched across epochs by the + /// GLOBAL_FIELD_MEMORY aggregation. Distinct from [`GlobalMemory`](BusId::GlobalMemory): + /// its token carries the domain (field-storage spans domains 3/4/5, whereas RAM + /// is domain 0 only) and a full field-element value (not a byte). + GlobalFieldMemory = 32, } impl BusId { @@ -388,6 +394,7 @@ impl BusId { BusId::Ecdas => "Ecdas", BusId::Bit => "Bit", BusId::GlobalMemory => "GlobalMemory", + BusId::GlobalFieldMemory => "GlobalFieldMemory", } } } @@ -420,6 +427,7 @@ impl TryFrom for BusId { 28 => Ok(BusId::Ecdas), 30 => Ok(BusId::Bit), 31 => Ok(BusId::GlobalMemory), + 32 => Ok(BusId::GlobalFieldMemory), other => Err(other), } } diff --git a/prover/src/test_utils.rs b/prover/src/test_utils.rs index 6dd28ce71..5f838cc37 100644 --- a/prover/src/test_utils.rs +++ b/prover/src/test_utils.rs @@ -64,6 +64,18 @@ use crate::tables::ecsm::{ EcsmConstraints, bus_interactions as ecsm_bus_interactions, cols as ecsm_cols, }; use crate::tables::eq::{EqConstraints, bus_interactions as eq_bus_interactions, cols as eq_cols}; +use crate::tables::fext_fma::{ + FextFmaConstraints, bus_interactions as fext_fma_bus_interactions, cols as fext_fma_cols, +}; +use crate::tables::fext_load::{ + FextLoadConstraints, bus_interactions as fext_load_bus_interactions, cols as fext_load_cols, +}; +use crate::tables::fext_page::{ + FextPageConstraints, bus_interactions as fext_page_bus_interactions, cols as fext_page_cols, +}; +use crate::tables::fext_store::{ + FextStoreConstraints, bus_interactions as fext_store_bus_interactions, cols as fext_store_cols, +}; use crate::tables::halt::{bus_interactions as halt_bus_interactions, cols as halt_cols}; use crate::tables::keccak::{ KeccakConstraints, bus_interactions as keccak_bus_interactions, cols as keccak_cols, @@ -947,3 +959,51 @@ pub fn create_ecdas_air(proof_options: &ProofOptions) -> ConcreteVmAir ConcreteVmAir { + build_air( + fext_load_cols::NUM_COLUMNS, + fext_load_bus_interactions(), + proof_options, + 1, + FextLoadConstraints, + "FEXT_LOAD", + ) +} + +/// Create FEXT_FMA AIR. +pub fn create_fext_fma_air(proof_options: &ProofOptions) -> ConcreteVmAir { + build_air( + fext_fma_cols::NUM_COLUMNS, + fext_fma_bus_interactions(), + proof_options, + 1, + FextFmaConstraints, + "FEXT_FMA", + ) +} + +/// Create FEXT_STORE AIR. +pub fn create_fext_store_air(proof_options: &ProofOptions) -> ConcreteVmAir { + build_air( + fext_store_cols::NUM_COLUMNS, + fext_store_bus_interactions(), + proof_options, + 1, + FextStoreConstraints, + "FEXT_STORE", + ) +} + +/// Create FEXT_PAGE AIR (field-storage init/finalization bookend). +pub fn create_fext_page_air(proof_options: &ProofOptions) -> ConcreteVmAir { + build_air( + fext_page_cols::NUM_COLUMNS, + fext_page_bus_interactions(), + proof_options, + 1, + FextPageConstraints, + "FEXT_PAGE", + ) +} diff --git a/prover/src/tests/count_table_lengths_drift_tests.rs b/prover/src/tests/count_table_lengths_drift_tests.rs index 6855fcb5b..bc39715fc 100644 --- a/prover/src/tests/count_table_lengths_drift_tests.rs +++ b/prover/src/tests/count_table_lengths_drift_tests.rs @@ -91,3 +91,54 @@ fn count_table_lengths_matches_traces() { // Mirrors hardcoded `halt_rows = 1` in `auto_storage::table_specs`. assert_eq!(traces.halt.main_table.height, 1, "halt_rows"); } + +/// Same drift check for a FEXT-exercising program: the accelerator tables must be +/// accounted for so `auto_storage`'s peak-RAM estimate does not undercount. +#[test] +fn count_table_lengths_matches_fext_traces() { + let (elf, logs, _) = run_asm_elf("fext_bench"); + let max_rows = MaxRowsConfig::default(); + + let predicted = + count_table_lengths(&elf, &logs, &max_rows, &[]).expect("count_table_lengths succeeds"); + let traces = Traces::from_elf_and_logs_minimal(&elf, &logs, &max_rows, &[]) + .expect("trace build succeeds"); + + let sum_heights = |tables: &[stark::trace::TraceTable<_, _>]| -> u64 { + tables.iter().map(|t| t.main_table.height as u64).sum() + }; + + // Sanity: the program actually exercises the accelerator. + assert!( + traces.fext_fma.main_table.height > 4, + "fext_bench should exercise FEXT_FMA (height={})", + traces.fext_fma.main_table.height + ); + + // FEXT tables: one row per ecall / touched cell, no dedup → exact match. + assert_eq!( + predicted.fext_load_padded_rows, traces.fext_load.main_table.height as u64, + "fext_load" + ); + assert_eq!( + predicted.fext_fma_padded_rows, traces.fext_fma.main_table.height as u64, + "fext_fma" + ); + assert_eq!( + predicted.fext_store_padded_rows, traces.fext_store.main_table.height as u64, + "fext_store" + ); + assert_eq!( + predicted.fext_page_padded_rows, traces.fext_page.main_table.height as u64, + "fext_page" + ); + + // LT stays an upper bound (dedup) and now includes the fext-induced + // `old_ts < ts` sends, so it must still cover the actual LT rows. + assert!( + predicted.lt_padded_rows >= sum_heights(&traces.lts), + "lt: predicted={} actual={}", + predicted.lt_padded_rows, + sum_heights(&traces.lts) + ); +} diff --git a/prover/src/tests/fext_fma_tests.rs b/prover/src/tests/fext_fma_tests.rs new file mode 100644 index 000000000..65453818c --- /dev/null +++ b/prover/src/tests/fext_fma_tests.rs @@ -0,0 +1,167 @@ +//! Tests for the FEXT_FMA table: constraint satisfaction on generated traces, +//! the constraint count, and negative checks for a wrong output. + +use crate::tables::fext_fma::{ + FextFmaConstraints, FextFmaOperation, bus_interactions, cols, generate_fext_fma_trace, +}; +use crate::tables::types::{FE, GoldilocksExtension, GoldilocksField, VmTable}; +use math::field::element::FieldElement; +use math::field::extensions_goldilocks::Degree3GoldilocksExtensionField; +use math::field::goldilocks::GoldilocksElement; +use stark::constraints::builder::{ConstraintSet, ProverEvalFolder}; +use stark::frame::Frame; +use stark::table::TableView; +use stark::trace::TraceTable; +use stark::traits::TransitionEvaluationContext; + +type Fp3 = FieldElement; + +/// `a*b + c` over the native Fp3, canonical coefficients. +fn fma(a: [u64; 3], b: [u64; 3], c: [u64; 3]) -> [u64; 3] { + let to_fp3 = |x: [u64; 3]| { + Fp3::from_raw([ + GoldilocksElement::from(x[0]), + GoldilocksElement::from(x[1]), + GoldilocksElement::from(x[2]), + ]) + }; + let r = to_fp3(a) * to_fp3(b) + to_fp3(c); + let v = r.value(); + [ + v[0].canonical_u64(), + v[1].canonical_u64(), + v[2].canonical_u64(), + ] +} + +fn op(a: [u64; 3], b: [u64; 3], c: [u64; 3]) -> FextFmaOperation { + FextFmaOperation { + timestamp: 100, + out_addr: 0x40, + a_addr: 0x10, + b_addr: 0x20, + c_addr: 0x30, + a, + b, + c, + output: fma(a, b, c), + read_old_ts: [[0; 3]; 3], + write_old_ts: [0; 3], + write_old_val: [0; 3], + } +} + +/// Evaluate the FEXT_FMA constraint set on one main-trace row. +fn eval_main_row(main: Vec) -> Vec { + let n = FextFmaConstraints.meta().len(); + let frame = Frame::::new(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); + FextFmaConstraints.eval(&mut folder); + base +} + +fn eval_row(trace: &TraceTable, row: usize) -> Vec { + let main: Vec = (0..cols::NUM_COLUMNS) + .map(|c| *trace.main_table.get(row, c)) + .collect(); + eval_main_row(main) +} + +#[test] +fn fext_fma_constraint_count_is_four() { + // idx 0: IS_BIT(μ); idx 1-3: the three coefficient equations. + assert_eq!(FextFmaConstraints.meta().len(), 4); +} + +#[test] +fn fext_fma_max_degree_is_two() { + assert_eq!(FextFmaConstraints.max_degree(), 2); +} + +#[test] +fn fext_fma_bus_interaction_count() { + // 1 Ecall + 4 register reads + 9 field reads + 3 field writes, each + // field access = consume-old + emit-new + old_ts) -> Vec { + let n = FextLoadConstraints.meta().len(); + let frame = Frame::::new(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); + FextLoadConstraints.eval(&mut folder); + base +} + +fn eval_row(trace: &TraceTable, row: usize) -> Vec { + let main: Vec = (0..cols::NUM_COLUMNS) + .map(|c| *trace.main_table.get(row, c)) + .collect(); + eval_main_row(main) +} + +fn op(addr: u64, coeffs: [u64; 3]) -> FextLoadOperation { + FextLoadOperation { + timestamp: 100, + addr, + coeffs, + old_ts: [0; 3], + old_val: [0; 3], + } +} + +#[test] +fn fext_load_constraint_count_is_one() { + // Only IS_BIT(μ); coefficient range checks are bus interactions. + assert_eq!(FextLoadConstraints.meta().len(), 1); +} + +#[test] +fn fext_load_bus_interaction_count() { + // 1 Ecall receiver + 4 register reads + 3 range checks + 3 field-storage + // writes × (consume-old, emit-new, old_ts, + row: usize, +) -> Vec { + let n = FextLocalToGlobalConstraints.meta().len(); + let get_row = |r: usize| -> Vec { + (0..cols::NUM_COLUMNS) + .map(|c| *trace.main_table.get(r, c)) + .collect() + }; + let frame = Frame::::new(vec![ + TableView::new(vec![get_row(row)], vec![vec![]]), + TableView::new(vec![get_row(row + 1)], 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); + FextLocalToGlobalConstraints.eval(&mut folder); + base +} + +fn boundary(domain: u64, addr: u64) -> FieldCellBoundary { + FieldCellBoundary { + domain, + addr, + init_val: 11, + init_epoch: 1, + final_val: 42, + final_ts: 100, + } +} + +#[test] +fn fext_l2g_constraint_and_bus_counts() { + assert_eq!(FextLocalToGlobalConstraints.meta().len(), 12); + // cross-epoch init receiver + fini sender. + assert_eq!(global_bus_interactions(2).len(), 2); + // epoch-local Memory init receiver + fini sender. + assert_eq!(memory_bus_interactions().len(), 2); + // 4 addr IsHalfword + 2 init_epoch IsHalfword + 1 IsB20 + 1 addr LT = 8. + assert_eq!(range_check_interactions(2).len(), 8); +} + +#[test] +fn fext_l2g_trace_layout_and_padding() { + let cells = vec![ + FieldCellBoundary { + domain: 3, + addr: 0x10, + init_val: 5, + init_epoch: 0, + final_val: 42, + final_ts: 100, + }, + FieldCellBoundary { + domain: 5, + addr: 0x20, + init_val: 9, + init_epoch: 2, + final_val: 7, + final_ts: 200, + }, + ]; + let trace = generate_fext_local_to_global_trace(&cells); + assert_eq!(trace.num_rows(), 4); + + let t = &trace.main_table; + assert_eq!(*t.get(0, cols::DOMAIN), FE::from(3u64)); + assert_eq!(*t.get(0, cols::INIT_VAL), FE::from(5u64)); + assert_eq!(*t.get(0, cols::INIT_EPOCH_0), FE::from(0u64)); + assert_eq!(*t.get(0, cols::FINAL_VAL), FE::from(42u64)); + assert_eq!(*t.get(0, cols::FINAL_TS_0), FE::from(100u64)); + assert_eq!(*t.get(0, cols::MU), FE::one()); + // Row 1: init_epoch 2 → halfword low = 2. + assert_eq!(*t.get(1, cols::INIT_EPOCH_0), FE::from(2u64)); + + for row in 2..4 { + assert_eq!(*t.get(row, cols::MU), FE::zero()); + assert_eq!(*t.get(row, cols::DOMAIN), FE::from(3u64)); + } +} + +#[test] +fn fext_l2g_bitwise_collector_count() { + // 7 lookups per cell: 4 addr IsHalfword + 2 init_epoch IsHalfword + 1 IsB20. + let cells = vec![boundary(3, 0x10), boundary(4, 0x20)]; + assert_eq!(collect_bitwise_from_fext_l2g(&cells, 5).len(), 2 * 7); +} + +#[test] +fn fext_l2g_lt_collector_same_domain_windows() { + // Same-domain consecutive cells yield one addr-LT each; the domain change does not. + let touched = vec![ + (3u64, 0x10u64, 0u64, 0u64), + (3, 0x20, 0, 0), + (4, 0x08, 0, 0), + ]; + // (3,0x10)<(3,0x20) is one LT; (3,0x20)->(4,0x08) crosses domains → none. + assert_eq!(collect_lt_from_touches(&touched).len(), 1); +} + +#[test] +fn fext_l2g_constraints_hold_on_valid_trace() { + let cells = vec![boundary(3, 0x10), boundary(3, 0x20), boundary(4, 0x08)]; + let trace = generate_fext_local_to_global_trace(&cells); + for row in 0..trace.num_rows() - 1 { + for (idx, v) in eval_transition(&trace, row).into_iter().enumerate() { + assert_eq!(v, FE::zero(), "row {row}, constraint {idx} should be zero"); + } + } +} + +#[test] +fn fext_l2g_rejects_forged_domain() { + let mut trace = generate_fext_local_to_global_trace(&[boundary(3, 0x10)]); + trace.main_table.set_fe(0, cols::DOMAIN, FE::from(0u64)); + assert_ne!(eval_transition(&trace, 0)[1], FE::zero()); +} + +#[test] +fn fext_l2g_rejects_domain_decrease() { + let mut trace = generate_fext_local_to_global_trace(&[boundary(3, 0x10), boundary(4, 0x20)]); + trace.main_table.set_fe(0, cols::DOMAIN, FE::from(5u64)); + assert_ne!(eval_transition(&trace, 0)[8], FE::zero()); +} + +#[test] +fn fext_l2g_rejects_active_row_after_padding() { + let mut trace = generate_fext_local_to_global_trace(&[boundary(3, 0x10)]); + trace.main_table.set_fe(2, cols::MU, FE::one()); + assert_ne!(eval_transition(&trace, 1)[5], FE::zero()); +} + +#[test] +fn fext_l2g_rejects_mismatched_same_dom() { + let mut trace = generate_fext_local_to_global_trace(&[boundary(3, 0x10), boundary(3, 0x20)]); + trace.main_table.set_fe(0, cols::SAME_DOM, FE::zero()); + trace.main_table.set_fe(0, cols::SEL_SAME, FE::zero()); + let base = eval_transition(&trace, 0); + assert!(base[6] != FE::zero() || base[8] != FE::zero()); +} + +#[test] +fn fext_l2g_rejects_forged_next_addr() { + let mut trace = generate_fext_local_to_global_trace(&[boundary(3, 0x10), boundary(3, 0x20)]); + trace + .main_table + .set_fe(0, cols::NEXT_ADDR_0, FE::from(0x999u64)); + assert_ne!(eval_transition(&trace, 0)[9], FE::zero()); +} diff --git a/prover/src/tests/fext_page_tests.rs b/prover/src/tests/fext_page_tests.rs new file mode 100644 index 000000000..757918260 --- /dev/null +++ b/prover/src/tests/fext_page_tests.rs @@ -0,0 +1,221 @@ +//! Tests for the FEXT_PAGE bookend table. + +use crate::tables::fext_page::{ + FextPageConstraints, FextPageOperation, bus_interactions, cols, generate_fext_page_trace, +}; +use crate::tables::types::{FE, GoldilocksExtension, GoldilocksField, VmTable}; +use math::field::element::FieldElement; +use stark::constraints::builder::{ConstraintSet, ProverEvalFolder}; +use stark::frame::Frame; +use stark::table::TableView; +use stark::trace::TraceTable; +use stark::traits::TransitionEvaluationContext; + +/// Evaluate every FEXT_PAGE constraint over the transition frame `(row, row+1)`. +/// Per-row constraints see `row`; transition constraints see both. +fn eval_transition( + trace: &TraceTable, + row: usize, +) -> Vec { + let n = FextPageConstraints.meta().len(); + let get_row = |r: usize| -> Vec { + (0..cols::NUM_COLUMNS) + .map(|c| *trace.main_table.get(r, c)) + .collect() + }; + let frame = Frame::::new(vec![ + TableView::new(vec![get_row(row)], vec![vec![]]), + TableView::new(vec![get_row((row + 1) % trace.num_rows())], 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); + FextPageConstraints.eval(&mut folder); + base +} + +fn op(domain: u64, addr: u64) -> FextPageOperation { + FextPageOperation { + domain, + addr, + final_ts: 100, + final_val: 42, + } +} + +#[test] +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, 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); +} + +#[test] +fn fext_page_trace_layout_and_padding() { + let ops = vec![ + FextPageOperation { + domain: 3, + addr: 0x10, + final_ts: 100, + final_val: 42, + }, + FextPageOperation { + domain: 5, + addr: 0x20, + final_ts: 200, + final_val: 7, + }, + ]; + let trace = generate_fext_page_trace(&ops); + assert_eq!(trace.num_rows(), 4); // 2 ops padded to 4 + + let t = &trace.main_table; + assert_eq!(*t.get(0, cols::DOMAIN), FE::from(3u64)); + assert_eq!(*t.get(0, cols::FINAL_VAL), FE::from(42u64)); + assert_eq!(*t.get(0, cols::FINAL_TS_0), FE::from(100u64)); + assert_eq!(*t.get(0, cols::MU), FE::one()); + assert_eq!(*t.get(1, cols::DOMAIN), FE::from(5u64)); + + // Padding rows have μ = 0 and a valid domain (3) so the domain constraint holds. + for row in 2..4 { + assert_eq!(*t.get(row, cols::MU), FE::zero()); + assert_eq!(*t.get(row, cols::DOMAIN), FE::from(3u64)); + } +} + +#[test] +fn fext_page_sorts_by_domain_then_addr() { + // Deliberately unsorted; trace-gen must emit strictly ascending (domain, addr). + let ops = vec![op(5, 0x30), op(3, 0x40), op(4, 0x10), op(3, 0x20)]; + let trace = generate_fext_page_trace(&ops); + let t = &trace.main_table; + + let key = |row: usize| { + ( + *t.get(row, cols::DOMAIN), + *t.get(row, cols::ADDR_0), + *t.get(row, cols::ADDR_1), + ) + }; + // Expected order: (3,0x20), (3,0x40), (4,0x10), (5,0x30). + assert_eq!(key(0), (FE::from(3u64), FE::from(0x20u64), FE::from(0u64))); + assert_eq!(key(1), (FE::from(3u64), FE::from(0x40u64), FE::from(0u64))); + assert_eq!(key(2), (FE::from(4u64), FE::from(0x10u64), FE::from(0u64))); + assert_eq!(key(3), (FE::from(5u64), FE::from(0x30u64), FE::from(0u64))); +} + +#[test] +fn fext_page_same_dom_and_selector_columns() { + // Two domain-3 rows then one domain-4 row (all active), padded to 4. + let ops = vec![op(3, 0x10), op(3, 0x20), op(4, 0x10)]; + let trace = generate_fext_page_trace(&ops); + let t = &trace.main_table; + + // Row 0 → row 1: same domain (3,3), both active ⇒ same_dom=1, sel_same=1. + assert_eq!(*t.get(0, cols::SAME_DOM), FE::one()); + assert_eq!(*t.get(0, cols::SEL_SAME), FE::one()); + // next_addr on row 0 is row 1's addr (0x20). + assert_eq!(*t.get(0, cols::NEXT_ADDR_0), FE::from(0x20u64)); + + // Row 1 → row 2: domains differ (3 vs 4) ⇒ same_dom=0, sel_same=0. + assert_eq!(*t.get(1, cols::SAME_DOM), FE::zero()); + assert_eq!(*t.get(1, cols::SEL_SAME), FE::zero()); + + // Row 2 → row 3: next row is padding (μ=0) ⇒ sel_same=0. + assert_eq!(*t.get(2, cols::SEL_SAME), FE::zero()); +} + +#[test] +fn fext_page_addr_limb_halfword_decomposition() { + // A 64-bit addr with bits set across both limbs and both halves. + let addr = (0xABCDu64 << 48) | (0x1234u64 << 32) | (0x5678u64 << 16) | 0x9ABC; + let trace = generate_fext_page_trace(&[op(3, addr)]); + let t = &trace.main_table; + assert_eq!(*t.get(0, cols::ADDR0_HW_LO), FE::from(0x9ABCu64)); + assert_eq!(*t.get(0, cols::ADDR0_HW_HI), FE::from(0x5678u64)); + assert_eq!(*t.get(0, cols::ADDR1_HW_LO), FE::from(0x1234u64)); + assert_eq!(*t.get(0, cols::ADDR1_HW_HI), FE::from(0xABCDu64)); +} + +#[test] +fn fext_page_constraints_hold_on_valid_trace() { + // Two domain-3 cells and one domain-4 cell: exercises same-domain (addr + // increase) and domain-change transitions plus padding. + let ops = vec![op(3, 0x10), op(3, 0x20), op(4, 0x08)]; + let trace = generate_fext_page_trace(&ops); + for row in 0..trace.num_rows() - 1 { + for (idx, v) in eval_transition(&trace, row).into_iter().enumerate() { + assert_eq!(v, FE::zero(), "row {row}, constraint {idx} should be zero"); + } + } +} + +#[test] +fn fext_page_rejects_forged_domain() { + // Domain outside {3,4,5} must fail the domain constraint (idx 1). + let mut trace = generate_fext_page_trace(&[op(3, 0x10)]); + trace.main_table.set_fe(0, cols::DOMAIN, FE::from(0u64)); // domain 0 = RAM + assert_ne!(eval_transition(&trace, 0)[1], FE::zero()); +} + +#[test] +fn fext_page_rejects_domain_decrease() { + // Sorted output is (3,_),(4,_); forcing the first row's domain to 5 makes the + // domain decrease across the transition, which idx 8 must reject. + let mut trace = generate_fext_page_trace(&[op(3, 0x10), op(4, 0x20)]); + trace.main_table.set_fe(0, cols::DOMAIN, FE::from(5u64)); + assert_ne!(eval_transition(&trace, 0)[8], FE::zero()); +} + +#[test] +fn fext_page_rejects_active_row_after_padding() { + // An active row following a padding row breaks μ non-increasing (idx 5). + let mut trace = generate_fext_page_trace(&[op(3, 0x10)]); + trace.main_table.set_fe(2, cols::MU, FE::one()); // row 1 padding, row 2 "active" + assert_ne!(eval_transition(&trace, 1)[5], FE::zero()); +} + +#[test] +fn fext_page_rejects_mismatched_same_dom() { + // same_dom claims "different" on two equal-domain rows: the selector + // definition (idx 6) or the domain-increase check (idx 8) must reject it. + let mut trace = generate_fext_page_trace(&[op(3, 0x10), op(3, 0x20)]); + trace.main_table.set_fe(0, cols::SAME_DOM, FE::zero()); + trace.main_table.set_fe(0, cols::SEL_SAME, FE::zero()); + let base = eval_transition(&trace, 0); + assert!(base[6] != FE::zero() || base[8] != FE::zero()); +} + +#[test] +fn fext_page_rejects_forged_next_addr() { + // The next-addr copy (idx 9) pins the cross-row LT operand to the real next + // row, so tampering with it is caught. + let mut trace = generate_fext_page_trace(&[op(3, 0x10), op(3, 0x20)]); + trace + .main_table + .set_fe(0, cols::NEXT_ADDR_0, FE::from(0x999u64)); + assert_ne!(eval_transition(&trace, 0)[9], FE::zero()); +} + +#[test] +fn fext_page_rejects_free_last_row_sel_same() { + // CRIT-001 regression: the `sel_same` definition (idx 6) is `except_last`-gated, + // so it never pins the final row's `sel_same`. Since `sel_same` is the addr-LT + // sender's multiplicity, a free last-row value of −1 would cancel a forced `+1` + // LT claim of the same tuple and erase the strict-increase check (enabling a + // duplicate cell). The ungated `IS_BIT(sel_same)` (idx 11) must reject any + // non-{0,1} last-row multiplicity — here the −1 wildcard. + let mut trace = generate_fext_page_trace(&[op(3, 0x10), op(3, 0x20)]); + let last = trace.num_rows() - 1; + trace + .main_table + .set_fe(last, cols::SEL_SAME, FE::zero() - FE::one()); + assert_ne!(eval_transition(&trace, last)[11], FE::zero()); +} diff --git a/prover/src/tests/fext_store_tests.rs b/prover/src/tests/fext_store_tests.rs new file mode 100644 index 000000000..cf670e81b --- /dev/null +++ b/prover/src/tests/fext_store_tests.rs @@ -0,0 +1,123 @@ +//! Tests for the FEXT_STORE table: trace layout, padding, constraint/bus counts, +//! and the IS_BIT(μ) check. + +use crate::tables::fext_store::{ + FextStoreConstraints, FextStoreOperation, bus_interactions, cols, generate_fext_store_trace, +}; +use crate::tables::types::{FE, GoldilocksExtension, GoldilocksField, VmTable}; +use math::field::element::FieldElement; +use stark::constraints::builder::{ConstraintSet, ProverEvalFolder}; +use stark::frame::Frame; +use stark::table::TableView; +use stark::trace::TraceTable; +use stark::traits::TransitionEvaluationContext; + +/// Evaluate every FEXT_STORE constraint over `row` (all are per-row). +fn eval_row(trace: &TraceTable, row: usize) -> Vec { + let n = FextStoreConstraints.meta().len(); + let main: Vec = (0..cols::NUM_COLUMNS) + .map(|c| *trace.main_table.get(row, c)) + .collect(); + let frame = Frame::::new(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); + FextStoreConstraints.eval(&mut folder); + base +} + +fn op(coeffs: [u64; 3]) -> FextStoreOperation { + FextStoreOperation { + timestamp: 100, + src_addr: 0x40, + coeffs, + old_ts: [10, 20, 30], + } +} + +#[test] +fn fext_store_constraint_count() { + // IS_BIT(μ) + 6 word-recompose constraints (one per coefficient word). + assert_eq!(FextStoreConstraints.meta().len(), 7); +} + +#[test] +fn fext_store_bus_interaction_count() { + // 1 Ecall + 1 register read (x10) + 3 field reads (consume + emit + old_ts, + row: usize, +) -> Vec { + let n = GlobalFieldMemoryConstraints.meta().len(); + let get_row = |r: usize| -> Vec { + (0..cols::NUM_COLUMNS) + .map(|c| *trace.main_table.get(r, c)) + .collect() + }; + let frame = Frame::::new(vec![ + TableView::new(vec![get_row(row)], vec![vec![]]), + TableView::new(vec![get_row((row + 1) % trace.num_rows())], 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); + GlobalFieldMemoryConstraints.eval(&mut folder); + base +} + +fn cell(domain: u64, addr: u64) -> FieldCellFinal { + FieldCellFinal { + domain, + addr, + value: 42, + epoch: 2, + } +} + +#[test] +fn global_field_memory_constraint_and_bus_counts() { + // Same sorted-keys shape as FEXT_PAGE: 12 constraints. + assert_eq!(GlobalFieldMemoryConstraints.meta().len(), 12); + // GFM-GENESIS + GFM-FINAL + addr LT + 4 IsHalfword = 7. + assert_eq!(bus_interactions().len(), 7); +} + +#[test] +fn global_field_memory_trace_layout_and_padding() { + let cells = vec![ + FieldCellFinal { + domain: 3, + addr: 0x10, + value: 42, + epoch: 1, + }, + FieldCellFinal { + domain: 5, + addr: 0x20, + value: 7, + epoch: 3, + }, + ]; + let trace = generate_global_field_trace(&cells); + assert_eq!(trace.num_rows(), 4); // 2 cells padded to 4 + + let t = &trace.main_table; + assert_eq!(*t.get(0, cols::DOMAIN), FE::from(3u64)); + assert_eq!(*t.get(0, cols::FINI_VAL), FE::from(42u64)); + assert_eq!(*t.get(0, cols::FINI_EPOCH), FE::from(1u64)); + assert_eq!(*t.get(0, cols::MU), FE::one()); + assert_eq!(*t.get(1, cols::DOMAIN), FE::from(5u64)); + + for row in 2..4 { + assert_eq!(*t.get(row, cols::MU), FE::zero()); + assert_eq!(*t.get(row, cols::DOMAIN), FE::from(3u64)); + } +} + +#[test] +fn global_field_memory_sorts_by_domain_then_addr() { + let cells = vec![cell(5, 0x30), cell(3, 0x40), cell(4, 0x10), cell(3, 0x20)]; + let trace = generate_global_field_trace(&cells); + let t = &trace.main_table; + let key = |row: usize| (*t.get(row, cols::DOMAIN), *t.get(row, cols::ADDR_0)); + assert_eq!(key(0), (FE::from(3u64), FE::from(0x20u64))); + assert_eq!(key(1), (FE::from(3u64), FE::from(0x40u64))); + assert_eq!(key(2), (FE::from(4u64), FE::from(0x10u64))); + assert_eq!(key(3), (FE::from(5u64), FE::from(0x30u64))); +} + +#[test] +fn global_field_memory_addr_limb_halfword_decomposition() { + let addr = (0xABCDu64 << 48) | (0x1234u64 << 32) | (0x5678u64 << 16) | 0x9ABC; + let trace = generate_global_field_trace(&[cell(3, addr)]); + let t = &trace.main_table; + assert_eq!(*t.get(0, cols::ADDR0_HW_LO), FE::from(0x9ABCu64)); + assert_eq!(*t.get(0, cols::ADDR0_HW_HI), FE::from(0x5678u64)); + assert_eq!(*t.get(0, cols::ADDR1_HW_LO), FE::from(0x1234u64)); + assert_eq!(*t.get(0, cols::ADDR1_HW_HI), FE::from(0xABCDu64)); +} + +#[test] +fn global_field_memory_constraints_hold_on_valid_trace() { + let cells = vec![cell(3, 0x10), cell(3, 0x20), cell(4, 0x08)]; + let trace = generate_global_field_trace(&cells); + for row in 0..trace.num_rows() - 1 { + for (idx, v) in eval_transition(&trace, row).into_iter().enumerate() { + assert_eq!(v, FE::zero(), "row {row}, constraint {idx} should be zero"); + } + } +} + +#[test] +fn global_field_memory_rejects_forged_domain() { + let mut trace = generate_global_field_trace(&[cell(3, 0x10)]); + trace.main_table.set_fe(0, cols::DOMAIN, FE::from(0u64)); // domain 0 = RAM + assert_ne!(eval_transition(&trace, 0)[1], FE::zero()); +} + +#[test] +fn global_field_memory_rejects_domain_decrease() { + let mut trace = generate_global_field_trace(&[cell(3, 0x10), cell(4, 0x20)]); + trace.main_table.set_fe(0, cols::DOMAIN, FE::from(5u64)); + assert_ne!(eval_transition(&trace, 0)[8], FE::zero()); +} + +#[test] +fn global_field_memory_rejects_active_row_after_padding() { + let mut trace = generate_global_field_trace(&[cell(3, 0x10)]); + trace.main_table.set_fe(2, cols::MU, FE::one()); // row 1 padding, row 2 "active" + assert_ne!(eval_transition(&trace, 1)[5], FE::zero()); +} + +#[test] +fn global_field_memory_rejects_mismatched_same_dom() { + let mut trace = generate_global_field_trace(&[cell(3, 0x10), cell(3, 0x20)]); + trace.main_table.set_fe(0, cols::SAME_DOM, FE::zero()); + trace.main_table.set_fe(0, cols::SEL_SAME, FE::zero()); + let base = eval_transition(&trace, 0); + assert!(base[6] != FE::zero() || base[8] != FE::zero()); +} + +#[test] +fn global_field_memory_rejects_forged_next_addr() { + let mut trace = generate_global_field_trace(&[cell(3, 0x10), cell(3, 0x20)]); + trace + .main_table + .set_fe(0, cols::NEXT_ADDR_0, FE::from(0x999u64)); + assert_ne!(eval_transition(&trace, 0)[9], FE::zero()); +} + +#[test] +fn global_field_memory_rejects_free_last_row_sel_same() { + // CRIT-001 regression at the cross-epoch anchor: the `sel_same` definition + // (idx 6) is `except_last`-gated, leaving the final anchor row's `sel_same` + // free. As the addr-LT sender's multiplicity, a −1 there would cancel a forced + // `+1` LT claim and duplicate an anchor row (forking cross-epoch history). The + // ungated `IS_BIT(sel_same)` (idx 11) must reject the non-{0,1} multiplicity. + let mut trace = generate_global_field_trace(&[cell(3, 0x10), cell(3, 0x20)]); + let last = trace.num_rows() - 1; + trace + .main_table + .set_fe(last, cols::SEL_SAME, FE::zero() - FE::one()); + assert_ne!(eval_transition(&trace, last)[11], FE::zero()); +} diff --git a/prover/src/tests/mod.rs b/prover/src/tests/mod.rs index 2d66692a9..e62d7d264 100644 --- a/prover/src/tests/mod.rs +++ b/prover/src/tests/mod.rs @@ -47,6 +47,18 @@ pub mod ecsm_tests; #[cfg(test)] pub mod eq_tests; #[cfg(test)] +pub mod fext_fma_tests; +#[cfg(test)] +pub mod fext_load_tests; +#[cfg(test)] +pub mod fext_local_to_global_tests; +#[cfg(test)] +pub mod fext_page_tests; +#[cfg(test)] +pub mod fext_store_tests; +#[cfg(test)] +pub mod global_field_memory_tests; +#[cfg(test)] pub mod keccak_rnd_tests; #[cfg(test)] pub mod load_tests; diff --git a/prover/src/tests/ood_window_ir_tests.rs b/prover/src/tests/ood_window_ir_tests.rs index b4ff5766c..057f20592 100644 --- a/prover/src/tests/ood_window_ir_tests.rs +++ b/prover/src/tests/ood_window_ir_tests.rs @@ -114,4 +114,35 @@ fn all_table_windows_match_captured_ir() { assert_ood_window_matches_ir(&create_keccak_rc_air(&opts), true, "KECCAK_RC"); assert_ood_window_matches_ir(&create_ecsm_air(&opts), true, "ECSM"); assert_ood_window_matches_ir(&create_ecdas_air(&opts), true, "ECDAS"); + // FEXT tables. FEXT_PAGE is the only VM table whose constraint set reads the + // next row beyond the LogUp accumulator (its contiguity/domain-ordering + // checks read DOMAIN/ADDR_0/ADDR_1/MU at row+1), so it must declare them via + // `ConstraintSet::next_row_columns`; the others read only the current row. + assert_ood_window_matches_ir(&create_fext_load_air(&opts), true, "FEXT_LOAD"); + assert_ood_window_matches_ir(&create_fext_fma_air(&opts), true, "FEXT_FMA"); + assert_ood_window_matches_ir(&create_fext_store_air(&opts), true, "FEXT_STORE"); + assert_ood_window_matches_ir(&create_fext_page_air(&opts), true, "FEXT_PAGE"); + // Continuation field-storage aggregation AIRs. GLOBAL_FIELD_MEMORY and the + // epoch-local FEXT_LOCAL_TO_GLOBAL read the next row via the SAME shared + // `SortedKeysLayout::emit_constraints` (DOMAIN/ADDR_0/ADDR_1/MU at row+1) and + // must declare it — the identical soundness-critical contract as FEXT_PAGE, + // previously unguarded here. The global FEXT_L2G aggregation is + // `EmptyConstraints` (its checks are inherited via the equal-root binding), so + // it reads only the LogUp accumulator; covered for completeness. `epoch_label` + // is a bus parameter and does not affect the constraint IR's next-row reads. + assert_ood_window_matches_ir( + &crate::continuation::global_field_memory_air(&opts), + true, + "GLOBAL_FIELD_MEMORY", + ); + assert_ood_window_matches_ir( + &crate::continuation::fext_l2g_memory_air(&opts, 1), + true, + "FEXT_LOCAL_TO_GLOBAL", + ); + assert_ood_window_matches_ir( + &crate::continuation::fext_l2g_global_air(&opts, 1), + true, + "FEXT_L2G_GLOBAL", + ); } diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index ffe9071b2..1e1d589d8 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -385,6 +385,172 @@ fn test_prove_elfs_arith_8() { ); } +/// End-to-end FEXT accelerator test: FEXT_LOAD a/b/c into field-storage, then +/// FEXT_FMA out = a*b + c over the native degree-3 Goldilocks extension. Proves +/// and verifies the full VM (exercises the FEXT_LOAD/FEXT_FMA/FEXT_STORE chips + +/// FEXT_PAGE bookend + their Memory/Alu/Ecall/Memw bus interactions balancing). +#[test] +fn test_prove_elfs_fext() { + let (elf, logs, instructions) = run_asm_elf("test_fext"); + let mut traces = + Traces::from_logs_minimal(&logs, instructions.clone(), &Default::default()).unwrap(); + assert!( + prove_and_verify_vm_minimal(&elf, &mut traces), + "Proof verification failed for test_fext program" + ); +} + +/// Adversarial: a FEXT_STORE read-back forged into the non-canonical `V + p` +/// word pair (same field element mod p, so the field-storage `Memory` read still +/// balances, but a 64-bit value >= p) must be rejected — the `coeff_lt_p` ALU-LT +/// canonicality check is the guard. Complements the AIR-only recompose test in +/// `fext_store_tests.rs` (which never drives the bus lookup). +#[test] +fn test_prove_elfs_fext_rejects_noncanonical_store_readback() { + use crate::tables::fext_store::cols as sc; + const P: u64 = 0xFFFF_FFFF_0000_0001; + + let (elf, logs, instructions) = run_asm_elf("test_fext"); + let mut traces = + Traces::from_logs_minimal(&logs, instructions.clone(), &Default::default()).unwrap(); + + let nrows = traces.fext_store.num_rows(); + let t = &mut traces.fext_store.main_table; + let row = (0..nrows) + .find(|&r| *t.get(r, sc::MU).value() == 1) + .expect("test_fext must have an active FEXT_STORE row"); + let v = *t.get(row, sc::C0_LO).value() | (*t.get(row, sc::C0_HI).value() << 32); + assert!( + v < (1u64 << 32) - 1, + "stored coeff must be small enough for the V+p alias to fit in u64" + ); + let alias = v + P; + let (lo, hi) = (alias & 0xFFFF_FFFF, alias >> 32); + t.set(row, sc::C0_LO, FieldElement::::from(lo)); + t.set(row, sc::C0_HI, FieldElement::::from(hi)); + // Keep the half-word recompose AIR constraints satisfied so the forgery can + // only be caught by the bus-level `coeff_lt_p` check, not the recompose. + t.set( + row, + sc::hw(sc::C0_LO), + FieldElement::::from(lo & 0xFFFF), + ); + t.set( + row, + sc::hw(sc::C0_LO) + 1, + FieldElement::::from(lo >> 16), + ); + t.set( + row, + sc::hw(sc::C0_HI), + FieldElement::::from(hi & 0xFFFF), + ); + t.set( + row, + sc::hw(sc::C0_HI) + 1, + FieldElement::::from(hi >> 16), + ); + + assert!( + !prove_and_verify_vm_minimal(&elf, &mut traces), + "non-canonical STORE read-back (V+p alias) must be rejected" + ); +} + +/// Adversarial: forging a touched field cell's finalized value in the FEXT_PAGE +/// bookend must be rejected — the `Memory`/GlobalFieldMemory token for that cell +/// no longer matches its last access, so the bus cannot balance. Guards the +/// field-storage carry/bookend value integrity (the AIR-only page tests never +/// drive this bus). +#[test] +fn test_prove_elfs_fext_rejects_tampered_field_final_value() { + use crate::tables::fext_page::cols as pc; + + let (elf, logs, instructions) = run_asm_elf("test_fext"); + let mut traces = + Traces::from_logs_minimal(&logs, instructions.clone(), &Default::default()).unwrap(); + + let nrows = traces.fext_page.num_rows(); + let t = &mut traces.fext_page.main_table; + let row = (0..nrows) + .find(|&r| *t.get(r, pc::MU).value() == 1) + .expect("test_fext must have an active FEXT_PAGE row"); + let forged = t.get(row, pc::FINAL_VAL).value().wrapping_add(1); + t.set( + row, + pc::FINAL_VAL, + FieldElement::::from(forged), + ); + + assert!( + !prove_and_verify_vm_minimal(&elf, &mut traces), + "a tampered field-cell final value must be rejected" + ); +} + +/// Regression: the prover must be deterministic for a fixed program. +/// +/// `generate_lt_trace` once ordered its rows by `HashMap` iteration (per-process +/// random), so the LT main-trace Merkle root — and thus the shared Fiat-Shamir +/// LogUp challenges derived from all main roots — varied run to run, which made +/// FEXT_PAGE's composition check flaky in CI. Prove `test_fext` repeatedly and +/// require every table's committed data to match. The grinding nonce and the +/// query openings it selects are excluded: a parallel grinding search legitimately +/// returns different valid nonces. +#[test] +fn test_prover_deterministic_fext() { + use std::hash::{Hash, Hasher}; + let (elf, logs, instructions) = run_asm_elf("test_fext"); + + let prove_core_hash = || -> u64 { + let mut traces = + Traces::from_logs_minimal(&logs, instructions.clone(), &Default::default()).unwrap(); + let proof_options = ProofOptions::default_test_options(); + let table_counts = traces.table_counts(); + let airs = VmAirs::new( + &elf, + &proof_options, + true, + &traces.page_configs, + &table_counts, + None, + true, + None, + None, + None, + ); + let air_trace_pairs = airs.air_trace_pairs(&mut traces); + let mp = multi_prove_ram(air_trace_pairs, &mut DefaultTranscript::::new(&[])).unwrap(); + let mut h = std::collections::hash_map::DefaultHasher::new(); + for p in &mp.proofs { + // Committed data only — nonce/query_list/deep_poly_openings vary with + // the parallel grinding search and are intentionally excluded. + format!( + "{:?}|{:?}|{:?}|{:?}|{:?}|{:?}|{:?}|{:?}", + p.trace_length, + p.lde_trace_main_merkle_root, + p.lde_trace_aux_merkle_root, + p.lde_trace_precomputed_merkle_root, + p.trace_ood_evaluations, + p.composition_poly_root, + p.composition_poly_parts_ood_evaluation, + (&p.fri_layers_merkle_roots, &p.fri_final_poly_coeffs), + ) + .hash(&mut h); + } + h.finish() + }; + + let baseline = prove_core_hash(); + for i in 0..8 { + assert_eq!( + baseline, + prove_core_hash(), + "prover produced nondeterministic committed data on reprove {i}" + ); + } +} + /// Basic arithmetic test with 32 instructions covering: /// - 64-bit ADD with positive, negative, and edge cases /// - 64-bit SUB with underflow, negative results @@ -3409,6 +3575,38 @@ fn test_continuation_pipeline_end_to_end() { ); } +/// FEXT accelerator ecalls under continuation (`l2g_memory_bookend = true`) are now +/// supported: field-storage is carried across epochs by the fext_local_to_global +/// bookend + GlobalFieldMemory aggregation, so trace building no longer rejects them. +/// (End-to-end prove+verify across epochs is `fext_works_under_continuation` in the +/// continuation module.) +#[test] +fn fext_trace_builds_under_continuation() { + use crate::tables::register; + use crate::tables::trace_builder::build_initial_image; + + let (elf, logs, _instructions) = run_asm_elf("test_fext"); + let image = build_initial_image(&elf, &[]); + let register_init = register::register_init_from_entry_point(elf.entry_point); + let result = Traces::from_image_and_logs( + &elf, + &image, + ®ister_init, + &logs, + &MaxRowsConfig::default(), + &[], + true, + true, + #[cfg(feature = "disk-spill")] + stark::storage_mode::StorageMode::Ram, + ); + assert!( + result.is_ok(), + "FEXT trace building under continuation must succeed now: {:?}", + result.err() + ); +} + /// A continuation epoch built with `l2g_memory_bookend = true` proves and verifies: /// PAGE no longer bookends the touched RAM bytes (they self-cancel), and the /// local-to-global table provides their `Memory`-bus init/fini instead. The epoch diff --git a/syscalls/src/syscalls.rs b/syscalls/src/syscalls.rs index 7165dff81..573087931 100644 --- a/syscalls/src/syscalls.rs +++ b/syscalls/src/syscalls.rs @@ -33,6 +33,18 @@ const KECCAK_SYSCALL_NUMBER: usize = usize::MAX - 1; #[cfg(target_arch = "riscv64")] const ECSM_SYSCALL_NUMBER: usize = usize::MAX - 10; +/// Syscall number for the FEXT_LOAD accelerator (-20 as usize). +#[cfg(target_arch = "riscv64")] +const FEXT_LOAD_SYSCALL_NUMBER: usize = usize::MAX - 19; + +/// Syscall number for the FEXT_FMA accelerator (-21 as usize). +#[cfg(target_arch = "riscv64")] +const FEXT_FMA_SYSCALL_NUMBER: usize = usize::MAX - 20; + +/// Syscall number for the FEXT_STORE accelerator (-22 as usize). +#[cfg(target_arch = "riscv64")] +const FEXT_STORE_SYSCALL_NUMBER: usize = usize::MAX - 21; + /// No-op. The `Print` ecall (a7=1) has no receiver on the Ecall bus, so emitting /// it makes the LogUp bus unbalance and the proof fail to verify. Printing isn't /// needed in provable programs, so `print_string` does nothing on every target. @@ -187,6 +199,79 @@ pub fn ecsm_mul(_xr: &mut [u8; 32], _xg: &[u8; 32], _k: &[u8; 32]) { unimplemented!("syscalls are only implemented for riscv64 targets"); } +#[cfg(target_arch = "riscv64")] +/// Store a degree-3 Goldilocks extension element into field-storage at `addr` +/// via the FEXT_LOAD accelerator. `coeffs` are the three coefficients in native +/// form; each must be a canonical field element (`< p`). `addr` is a handle into +/// the accelerator's separate field-storage address space (not RAM). +pub fn fext_load(addr: u64, coeffs: &[u64; 3]) { + unsafe { + asm!( + "ecall", + in("a0") addr, // x10 = field-storage destination address + in("a1") coeffs[0], // x11 = coefficient 0 + in("a2") coeffs[1], // x12 = coefficient 1 + in("a3") coeffs[2], // x13 = coefficient 2 + in("a7") FEXT_LOAD_SYSCALL_NUMBER, + ) + } +} + +#[cfg(not(target_arch = "riscv64"))] +/// Store a degree-3 Goldilocks extension element into field-storage at `addr`. +pub fn fext_load(_addr: u64, _coeffs: &[u64; 3]) { + unimplemented!("syscalls are only implemented for riscv64 targets"); +} + +#[cfg(target_arch = "riscv64")] +/// Compute `out = a*b + c` over the native degree-3 Goldilocks extension via the +/// FEXT_FMA accelerator. All arguments are field-storage handles (not RAM +/// addresses); the result is written to `out_addr`. Argument-to-register mapping +/// follows the spec: a/b/c in A0/A1/A2, output in A3. +pub fn fext_fma(a_addr: u64, b_addr: u64, c_addr: u64, out_addr: u64) { + unsafe { + asm!( + "ecall", + in("a0") a_addr, // x10 = address of a + in("a1") b_addr, // x11 = address of b + in("a2") c_addr, // x12 = address of c + in("a3") out_addr, // x13 = output field-storage address + in("a7") FEXT_FMA_SYSCALL_NUMBER, + ) + } +} + +#[cfg(not(target_arch = "riscv64"))] +/// Compute `out = a*b + c` over the native degree-3 Goldilocks extension. +pub fn fext_fma(_a_addr: u64, _b_addr: u64, _c_addr: u64, _out_addr: u64) { + unimplemented!("syscalls are only implemented for riscv64 targets"); +} + +#[cfg(target_arch = "riscv64")] +/// Read the degree-3 extension element at field-storage address `src_addr` and +/// return its three coefficients (native u64 form) in registers a1/a2/a3. The +/// read-back companion to [`fext_load`] (which reads coeffs from a1/a2/a3). +pub fn fext_store(src_addr: u64) -> [u64; 3] { + let (c0, c1, c2): (u64, u64, u64); + unsafe { + asm!( + "ecall", + in("a0") src_addr, // x10 = field-storage source address + out("a1") c0, // x11 = coefficient 0 (output) + out("a2") c1, // x12 = coefficient 1 (output) + out("a3") c2, // x13 = coefficient 2 (output) + in("a7") FEXT_STORE_SYSCALL_NUMBER, + ) + } + [c0, c1, c2] +} + +#[cfg(not(target_arch = "riscv64"))] +/// Read a degree-3 extension element from field-storage into registers. +pub fn fext_store(_src_addr: u64) -> [u64; 3] { + unimplemented!("syscalls are only implemented for riscv64 targets"); +} + // ============================================================================= // Stub implementations for unsupported std functions // These functions are required by Rust's std zkvm module but are not supported