From 7725f2532e8988377fbd89898d110cbf03c3b4a8 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Tue, 14 Jul 2026 11:57:25 -0300 Subject: [PATCH 01/17] Add FEXT executor syscalls and FMA prover chip --- Cargo.lock | 1 + executor/Cargo.toml | 1 + executor/src/tests/fext_tests.rs | 123 +++++++++++ executor/src/tests/mod.rs | 1 + executor/src/vm/instruction/execution.rs | 79 +++++++ executor/src/vm/memory.rs | 18 ++ prover/src/tables/fext_fma.rs | 249 +++++++++++++++++++++++ prover/src/tables/mod.rs | 1 + prover/src/tests/fext_fma_tests.rs | 150 ++++++++++++++ prover/src/tests/mod.rs | 2 + syscalls/src/syscalls.rs | 55 +++++ 11 files changed, 680 insertions(+) create mode 100644 executor/src/tests/fext_tests.rs create mode 100644 prover/src/tables/fext_fma.rs create mode 100644 prover/src/tests/fext_fma_tests.rs diff --git a/Cargo.lock b/Cargo.lock index 5bfab63d4..c50a807c7 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1220,6 +1220,7 @@ version = "0.1.0" dependencies = [ "ecsm", "ethrex-guest-program", + "math", "rkyv", "rustc-demangle", "serde", diff --git a/executor/Cargo.toml b/executor/Cargo.toml index 5d1e4ae49..0726209f5 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/src/tests/fext_tests.rs b/executor/src/tests/fext_tests.rs new file mode 100644 index 000000000..64b54d59e --- /dev/null +++ b/executor/src/tests/fext_tests.rs @@ -0,0 +1,123 @@ +//! 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, +}; +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, out).unwrap(); + registers.write(11, a).unwrap(); + registers.write(12, b).unwrap(); + registers.write(13, c).unwrap(); + Instruction::EcallEbreak + .run(&mut pc, &mut registers, memory) + .unwrap(); +} + +#[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" + ); + } +} 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..39cff9f2e 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,10 @@ 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, } /// Syscall number for KeccakPermute (u64::MAX - 1 = 0xFFFF_FFFF_FFFF_FFFE). @@ -31,6 +38,16 @@ 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; + /// `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 +62,8 @@ 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), _ => Err(()), } } @@ -55,6 +74,8 @@ impl TryFrom for SyscallNumbers { pub enum Accelerator { Keccak, Ecsm, + FextLoad, + FextFma, } impl SyscallNumbers { @@ -65,6 +86,8 @@ 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::Print | SyscallNumbers::Panic | SyscallNumbers::Commit @@ -98,6 +121,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 agree bit-for-bit. +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 +499,38 @@ 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). + // x10 = output address, x11/x12/x13 = addresses of a/b/c, + // all in field-storage. + let out_addr = registers.read(10)?; + let a_addr = registers.read(11)?; + let b_addr = registers.read(12)?; + let c_addr = registers.read(13)?; + 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::Halt => { // halt return Ok(Log { @@ -636,6 +713,8 @@ 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), } // ============================================================================= diff --git a/executor/src/vm/memory.rs b/executor/src/vm/memory.rs index ea3b06c20..43c74d4f0 100644 --- a/executor/src/vm/memory.rs +++ b/executor/src/vm/memory.rs @@ -65,6 +65,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 { @@ -164,6 +170,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/src/tables/fext_fma.rs b/prover/src/tables/fext_fma.rs new file mode 100644 index 000000000..aec8716eb --- /dev/null +++ b/prover/src/tables/fext_fma.rs @@ -0,0 +1,249 @@ +//! 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 (this phase) +//! - **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 (out/a/b/c addresses). +//! +//! The field-storage reads of `a,b,c` and the write of `output` (memory domains +//! 3/4/5), plus the domain init/finalization, are added in the field-storage +//! phase; until then the coefficient columns are free witness bound only by the +//! arithmetic constraints. +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, zeroed_fe_vec}; + +/// Column indices for the FEXT_FMA table. +pub mod cols { + // Timestamp (DWordWL: 2 cols) + pub const TIMESTAMP_0: usize = 0; + pub const TIMESTAMP_1: usize = 1; + + // Operand addresses (each DWordWL). Registers: x10=out, x11=a, x12=b, x13=c. + 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 (1 for real rows, 0 for padding). + pub const MU: usize = 22; + + pub const NUM_COLUMNS: usize = 23; +} + +/// FEXT_FMA syscall number split into the two 32-bit limbs the `Ecall` bus carries. +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: `output = a*b + c`, with operand addresses. +#[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, + /// Coefficients of `a`, `b`, `c` (canonical field elements). + pub a: [u64; 3], + pub b: [u64; 3], + pub c: [u64; 3], + /// Result coefficients `a*b + c` (canonical). + pub output: [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`), which satisfies the +/// arithmetic constraints (`0 = 0`) and `IS_BIT μ`. +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 (i, base) in [cols::A0, cols::B0, cols::C0].into_iter().enumerate() { + let coeffs = [op.a, op.b, op.c][i]; + for (k, &v) in coeffs.iter().enumerate() { + table.set_fe(row, base + k, FE::from(v)); + } + } + for (k, &v) in op.output.iter().enumerate() { + table.set_fe(row, cols::OUT0 + k, FE::from(v)); + } + + table.set_fe(row, cols::MU, FE::one()); + } + + trace +} + +/// A single MEMW register-read interaction (24-element CO24 read: `old == value`, +/// `is_register = 1`, `write2 = 1`). `reg` is the register index; the register +/// file is byte-addressed ×2, so the base address is `2*reg`. +fn memw_register_read(addr_lo: usize, addr_hi: usize, reg: u64) -> BusInteraction { + let addr = |col| BusValue::Packed { + start_column: col, + packing: Packing::Direct, + }; + let ts = |col| BusValue::Packed { + start_column: col, + packing: Packing::Direct, + }; + BusInteraction::sender( + BusId::Memw, + Multiplicity::Column(cols::MU), + vec![ + // old[0..7] = [addr_lo, addr_hi, 0, 0, 0, 0, 0, 0] + addr(addr_lo), + addr(addr_hi), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + // is_register = 1 + BusValue::constant(1), + // base_address = [2*reg, 0] + BusValue::constant(2 * reg), + BusValue::constant(0), + // value[0..7] = same as old (read) + addr(addr_lo), + addr(addr_hi), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + BusValue::constant(0), + // timestamp + ts(cols::TIMESTAMP_0), + ts(cols::TIMESTAMP_1), + // w2 = 1, w4 = 0, w8 = 0 (register = 2 words) + BusValue::constant(1), + BusValue::constant(0), + BusValue::constant(0), + ], + ) +} + +/// Bus interactions for the FEXT_FMA table (this phase: `Ecall` receiver + +/// 4 register reads). Field-storage `Memory` tokens are added later. +pub fn bus_interactions() -> Vec { + vec![ + // Receive the ECALL from the CPU, keyed by the FEXT_FMA syscall number. + 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(FMA_SYSCALL_LO), + BusValue::constant(FMA_SYSCALL_HI), + ], + ), + // Register reads: x10=out, x11=a, x12=b, x13=c. + memw_register_read(cols::OUT_ADDR_0, cols::OUT_ADDR_1, 10), + memw_register_read(cols::A_ADDR_0, cols::A_ADDR_1, 11), + memw_register_read(cols::B_ADDR_0, cols::B_ADDR_1, 12), + memw_register_read(cols::C_ADDR_0, cols::C_ADDR_1, 13), + ] +} + +/// 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/mod.rs b/prover/src/tables/mod.rs index 0a86e4149..f43f1d804 100644 --- a/prover/src/tables/mod.rs +++ b/prover/src/tables/mod.rs @@ -32,6 +32,7 @@ pub mod dvrm; pub mod ecdas; pub mod ecsm; pub mod eq; +pub mod fext_fma; pub mod global_memory; pub mod halt; pub mod keccak; diff --git a/prover/src/tests/fext_fma_tests.rs b/prover/src/tests/fext_fma_tests.rs new file mode 100644 index 000000000..2912668b3 --- /dev/null +++ b/prover/src/tests/fext_fma_tests.rs @@ -0,0 +1,150 @@ +//! 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), + } +} + +/// 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 receiver + 4 register reads. + assert_eq!(bus_interactions().len(), 5); +} + +#[test] +fn fext_fma_constraints_hold_on_valid_trace() { + let ops = vec![ + op([1, 0, 0], [1, 0, 0], [0, 0, 0]), + op([0, 1, 0], [0, 1, 0], [0, 0, 0]), // w*w = w^2 + op([0, 0, 1], [0, 0, 1], [0, 0, 0]), // w^2*w^2 = 2w + op([1, 2, 3], [4, 5, 6], [7, 8, 9]), + op([12345, 67890, 111213], [222324, 252627, 282930], [1, 2, 3]), + ]; + let trace = generate_fext_fma_trace(&ops); + + // Real rows and padding rows all satisfy every constraint. + for row in 0..trace.num_rows() { + for (idx, v) in eval_row(&trace, row).into_iter().enumerate() { + assert_eq!(v, FE::zero(), "row {row}, constraint {idx} nonzero"); + } + } +} + +#[test] +fn fext_fma_detects_wrong_output() { + let ops = vec![op([1, 2, 3], [4, 5, 6], [7, 8, 9])]; + let mut trace = generate_fext_fma_trace(&ops); + // Corrupt out1 (constraint index 2). + trace.main_table.set_fe(0, cols::OUT1, FE::from(999_999u64)); + let vals = eval_row(&trace, 0); + assert_ne!( + vals[2], + FE::zero(), + "corrupted out1 must break constraint 2" + ); +} + +#[test] +fn fext_fma_detects_non_bit_mu() { + let ops = vec![op([1, 2, 3], [4, 5, 6], [7, 8, 9])]; + let mut trace = generate_fext_fma_trace(&ops); + trace.main_table.set_fe(0, cols::MU, FE::from(2u64)); + let vals = eval_row(&trace, 0); + assert_ne!( + vals[0], + FE::zero(), + "μ = 2 must break IS_BIT (constraint 0)" + ); +} + +#[test] +fn fext_fma_trace_shape() { + let ops = vec![op([1, 2, 3], [4, 5, 6], [7, 8, 9])]; + let trace = generate_fext_fma_trace(&ops); + // 1 op → padded to min 4 rows. + assert_eq!(trace.num_rows(), 4); + // Real row has μ = 1, padding rows μ = 0. + assert_eq!(*trace.main_table.get(0, cols::MU), FE::one()); + for row in 1..4 { + assert_eq!(*trace.main_table.get(row, cols::MU), FE::zero()); + } +} diff --git a/prover/src/tests/mod.rs b/prover/src/tests/mod.rs index 4085f3bc5..ec3558214 100644 --- a/prover/src/tests/mod.rs +++ b/prover/src/tests/mod.rs @@ -47,6 +47,8 @@ pub mod ecsm_tests; #[cfg(test)] pub mod eq_tests; #[cfg(test)] +pub mod fext_fma_tests; +#[cfg(test)] pub mod keccak_rnd_tests; #[cfg(test)] pub mod load_tests; diff --git a/syscalls/src/syscalls.rs b/syscalls/src/syscalls.rs index 491315ecb..c197ec352 100644 --- a/syscalls/src/syscalls.rs +++ b/syscalls/src/syscalls.rs @@ -24,6 +24,14 @@ 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; + /// 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. @@ -156,6 +164,53 @@ 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`. +pub fn fext_fma(out_addr: u64, a_addr: u64, b_addr: u64, c_addr: u64) { + unsafe { + asm!( + "ecall", + in("a0") out_addr, // x10 = output field-storage address + in("a1") a_addr, // x11 = address of a + in("a2") b_addr, // x12 = address of b + in("a3") c_addr, // x13 = address of c + 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(_out_addr: u64, _a_addr: u64, _b_addr: u64, _c_addr: u64) { + 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 From 81941ef379663d19760529e3d035eba4234c2fb7 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Tue, 14 Jul 2026 12:13:09 -0300 Subject: [PATCH 02/17] Add FEXT_LOAD prover chip with range checks --- prover/src/tables/fext_load.rs | 200 ++++++++++++++++++++++++++++ prover/src/tables/mod.rs | 1 + prover/src/tests/fext_load_tests.rs | 101 ++++++++++++++ prover/src/tests/mod.rs | 2 + 4 files changed, 304 insertions(+) create mode 100644 prover/src/tables/fext_load.rs create mode 100644 prover/src/tests/fext_load_tests.rs diff --git a/prover/src/tables/fext_load.rs b/prover/src/tables/fext_load.rs new file mode 100644 index 000000000..db67ec54c --- /dev/null +++ b/prover/src/tables/fext_load.rs @@ -0,0 +1,200 @@ +//! 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 coefficient `< p` (canonical +//! Goldilocks element) via the ALU `LT` bus, and writes them into field-storage +//! (memory domains 3/4/5) at the destination address. +//! +//! ## Bus interactions (this phase) +//! - **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. +//! +//! The field-storage writes (memory domains 3/4/5, value = `lo + 2^32*hi` per +//! coefficient) and the domain init/finalization are added in the field-storage +//! phase. Unlike the draft spec, this write is a genuine memory *write*, not a +//! read-assert (draft bug: `output = value` forces `old == value`). +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; +use stark::lookup::{BusInteraction, BusValue, 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, 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; + + pub const NUM_COLUMNS: usize = 11; + + /// Low-limb column of coefficient `i` (`i` in 0..3). + pub const fn coeff(i: usize) -> usize { + C0_0 + 2 * 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], +} + +/// 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, &c) in op.coeffs.iter().enumerate() { + table.set_dword_wl(row, cols::coeff(i), c); + } + 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), + ], + ) +} + +/// `coeff < p` on the unified ALU bus: `[coeff(DWordWL), p(DWordWL), opsel(LT), 1, 0]` +/// (unsigned, non-inverted, asserting the result is 1). +fn coeff_lt_p(coeff_lo: usize) -> BusInteraction { + BusInteraction::sender( + BusId::Alu, + Multiplicity::Column(cols::MU), + vec![ + BusValue::Packed { + start_column: coeff_lo, + packing: Packing::DWordWL, + }, + BusValue::constant(P_LO), + BusValue::constant(P_HI), + BusValue::constant(alu_op::LT as u64), + BusValue::constant(1), + BusValue::constant(0), + ], + ) +} + +/// Bus interactions for FEXT_LOAD (this phase): `Ecall` receiver + 4 register +/// reads + 3 `< p` range checks. Field-storage writes are added later. +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(cols::coeff(i))); + } + interactions +} + +/// FEXT_LOAD constraints: idx 0 is `IS_BIT(μ)`. Coefficient canonicality is +/// enforced by the ALU `LT` bus interactions, not by 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/mod.rs b/prover/src/tables/mod.rs index f43f1d804..0fc46673c 100644 --- a/prover/src/tables/mod.rs +++ b/prover/src/tables/mod.rs @@ -33,6 +33,7 @@ pub mod ecdas; pub mod ecsm; pub mod eq; pub mod fext_fma; +pub mod fext_load; pub mod global_memory; pub mod halt; pub mod keccak; diff --git a/prover/src/tests/fext_load_tests.rs b/prover/src/tests/fext_load_tests.rs new file mode 100644 index 000000000..a628c1608 --- /dev/null +++ b/prover/src/tests/fext_load_tests.rs @@ -0,0 +1,101 @@ +//! Tests for the FEXT_LOAD table: constraint count, bus count, trace layout, +//! and the μ bit constraint. + +use crate::tables::fext_load::{ + FextLoadConstraints, FextLoadOperation, bus_interactions, cols, generate_fext_load_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; + +fn eval_main_row(main: Vec) -> 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, + } +} + +#[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. + assert_eq!(bus_interactions().len(), 8); +} + +#[test] +fn fext_load_trace_decomposes_coeffs_into_words() { + // Coefficient with both limbs non-zero. + let coeff = 0x1234_5678_9ABC_DEF0u64; + let trace = generate_fext_load_trace(&[op(0xAA, [coeff, 7, 0])]); + let t = &trace.main_table; + + // addr and timestamp low/high limbs. + assert_eq!(*t.get(0, cols::ADDR_0), FE::from(0xAAu64)); + assert_eq!(*t.get(0, cols::ADDR_1), FE::from(0u64)); + assert_eq!(*t.get(0, cols::TIMESTAMP_0), FE::from(100u64)); + + // coeff 0 split into words. + assert_eq!(*t.get(0, cols::C0_0), FE::from(0x9ABC_DEF0u64)); + assert_eq!(*t.get(0, cols::C0_1), FE::from(0x1234_5678u64)); + // coeff 1 = 7 (low limb only). + assert_eq!(*t.get(0, cols::C1_0), FE::from(7u64)); + assert_eq!(*t.get(0, cols::C1_1), FE::from(0u64)); + + assert_eq!(*t.get(0, cols::MU), FE::one()); +} + +#[test] +fn fext_load_trace_shape_and_padding() { + let trace = generate_fext_load_trace(&[op(1, [1, 2, 3])]); + assert_eq!(trace.num_rows(), 4); + assert_eq!(*trace.main_table.get(0, cols::MU), FE::one()); + for row in 1..4 { + assert_eq!(*trace.main_table.get(row, cols::MU), FE::zero()); + } +} + +#[test] +fn fext_load_mu_bit_constraint_holds_and_detects_violation() { + let mut trace = generate_fext_load_trace(&[op(1, [1, 2, 3])]); + // Valid: every row satisfies IS_BIT(μ). + for row in 0..trace.num_rows() { + assert_eq!(eval_row(&trace, row)[0], FE::zero(), "row {row}"); + } + // μ = 2 breaks it. + trace.main_table.set_fe(0, cols::MU, FE::from(2u64)); + assert_ne!(eval_row(&trace, 0)[0], FE::zero()); +} diff --git a/prover/src/tests/mod.rs b/prover/src/tests/mod.rs index ec3558214..4a3359ed2 100644 --- a/prover/src/tests/mod.rs +++ b/prover/src/tests/mod.rs @@ -49,6 +49,8 @@ pub mod eq_tests; #[cfg(test)] pub mod fext_fma_tests; #[cfg(test)] +pub mod fext_load_tests; +#[cfg(test)] pub mod keccak_rnd_tests; #[cfg(test)] pub mod load_tests; From ee53fe391071b10ffc13c0275ebf4dac99b7f81f Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Tue, 14 Jul 2026 15:08:52 -0300 Subject: [PATCH 03/17] Add FEXT field-storage memory argument and E2E --- bin/cli/src/main.rs | 12 +- executor/programs/asm/test_fext.s | 43 ++++ executor/src/tests/fext_tests.rs | 40 ++- executor/src/vm/instruction/execution.rs | 32 ++- prover/src/lib.rs | 22 +- prover/src/tables/cpu.rs | 12 + prover/src/tables/fext_fma.rs | 233 ++++++++++++----- prover/src/tables/fext_load.rs | 177 +++++++++++-- prover/src/tables/fext_page.rs | 121 +++++++++ prover/src/tables/mod.rs | 1 + prover/src/tables/trace_builder.rs | 305 ++++++++++++++++++++++- prover/src/test_utils.rs | 45 ++++ prover/src/tests/fext_fma_tests.rs | 8 +- prover/src/tests/fext_load_tests.rs | 7 +- prover/src/tests/fext_page_tests.rs | 45 ++++ prover/src/tests/mod.rs | 2 + prover/src/tests/prove_elfs_tests.rs | 15 ++ syscalls/src/syscalls.rs | 15 +- 18 files changed, 1016 insertions(+), 119 deletions(-) create mode 100644 executor/programs/asm/test_fext.s create mode 100644 prover/src/tables/fext_page.rs create mode 100644 prover/src/tests/fext_page_tests.rs diff --git a/bin/cli/src/main.rs b/bin/cli/src/main.rs index 95c3050b7..63ce828da 100644 --- a/bin/cli/src/main.rs +++ b/bin/cli/src/main.rs @@ -397,7 +397,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)> = None; let cycle_count = if let Some(ref output_path) = flamegraph.path { // Shared execute+flamegraph path (executor::flamegraph) instead of @@ -465,6 +465,8 @@ 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; // 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` @@ -497,6 +499,8 @@ 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, None => {} } } @@ -511,16 +515,18 @@ 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)); } 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)) = 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); } } diff --git a/executor/programs/asm/test_fext.s b/executor/programs/asm/test_fext.s new file mode 100644 index 000000000..42c0712b8 --- /dev/null +++ b/executor/programs/asm/test_fext.s @@ -0,0 +1,43 @@ + .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 + + # 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 index 64b54d59e..087ca9f37 100644 --- a/executor/src/tests/fext_tests.rs +++ b/executor/src/tests/fext_tests.rs @@ -48,15 +48,47 @@ 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, out).unwrap(); - registers.write(11, a).unwrap(); - registers.write(12, b).unwrap(); - registers.write(13, c).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"); +} + #[test] fn fext_load_then_fma_matches_reference() { let mut memory = Memory::default(); diff --git a/executor/src/vm/instruction/execution.rs b/executor/src/vm/instruction/execution.rs index 39cff9f2e..9d41de6d2 100644 --- a/executor/src/vm/instruction/execution.rs +++ b/executor/src/vm/instruction/execution.rs @@ -124,8 +124,8 @@ fn ecsm_addr_ok(addr: u64, max_offset: u64) -> bool { /// 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 agree bit-for-bit. -fn fext_fma(a: [u64; 3], b: [u64; 3], c: [u64; 3]) -> [u64; 3] { +/// 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([ @@ -518,12 +518,26 @@ impl Instruction { } SyscallNumbers::FextFma => { // FEXT_FMA(-21): output = a*b + c over Fp[x]/(x^3-2). - // x10 = output address, x11/x12/x13 = addresses of a/b/c, - // all in field-storage. - let out_addr = registers.read(10)?; - let a_addr = registers.read(11)?; - let b_addr = registers.read(12)?; - let c_addr = registers.read(13)?; + // 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); @@ -715,6 +729,8 @@ pub enum ExecutionError { 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/prover/src/lib.rs b/prover/src/lib.rs index bd72a3670..e09ddd736 100644 --- a/prover/src/lib.rs +++ b/prover/src/lib.rs @@ -53,7 +53,8 @@ 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_ecsm_air, create_eq_air, create_fext_fma_air, create_fext_load_air, + create_fext_page_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, @@ -78,8 +79,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_page. +pub const FIXED_TABLE_COUNT: usize = 13; /// Number of chunks for each split table. /// The verifier needs this to reconstruct matching AIRs. @@ -260,6 +261,9 @@ pub(crate) struct VmAirs { pub keccak_rc: VmAir, pub ecsm: VmAir, pub ecdas: VmAir, + pub fext_load: VmAir, + pub fext_fma: VmAir, + pub fext_page: VmAir, pub register: VmAir, pub pages: Vec, pub memw_registers: Vec, @@ -285,6 +289,9 @@ 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_page.as_ref(), &mut traces.fext_page, &()), (self.register.as_ref(), &mut traces.register, &()), ]; if self.include_halt { @@ -359,6 +366,9 @@ 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_page.as_ref(), self.register.as_ref(), ]; if self.include_halt { @@ -532,6 +542,9 @@ 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_page: VmAir = Box::new(create_fext_page_air(proof_options)); let register: VmAir = if let Some((commitment, num_preprocessed_cols)) = register_preprocessed { Box::new( @@ -638,6 +651,9 @@ impl VmAirs { keccak_rc, ecsm, ecdas, + fext_load, + fext_fma, + fext_page, register, pages, memw_registers, diff --git a/prover/src/tables/cpu.rs b/prover/src/tables/cpu.rs index 781bb02b0..2ca286ba5 100644 --- a/prover/src/tables/cpu.rs +++ b/prover/src/tables/cpu.rs @@ -188,6 +188,10 @@ 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, } impl CpuOperation { @@ -235,6 +239,12 @@ 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; // 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 +363,8 @@ impl CpuOperation { ecall_keccak, keccak_state_addr, ecall_ecsm, + ecall_fext_load, + ecall_fext_fma, } } diff --git a/prover/src/tables/fext_fma.rs b/prover/src/tables/fext_fma.rs index aec8716eb..f2ffd8a6e 100644 --- a/prover/src/tables/fext_fma.rs +++ b/prover/src/tables/fext_fma.rs @@ -10,14 +10,17 @@ //! 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 (this phase) +//! ## 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 (out/a/b/c addresses). +//! - **Sender** on `Memw` ×4: register reads of x10/x11/x12/x13 (out/a/b/c 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. //! -//! The field-storage reads of `a,b,c` and the write of `output` (memory domains -//! 3/4/5), plus the domain init/finalization, are added in the field-storage -//! phase; until then the coefficient columns are free witness bound only by the -//! arithmetic constraints. +//! 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; @@ -26,11 +29,12 @@ use executor::vm::instruction::execution::FEXT_FMA_SYSCALL_NUMBER; use crate::constraints::templates::emit_is_bit; -use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField, VmTable, zeroed_fe_vec}; +use super::types::{ + BusId, FE, GoldilocksExtension, GoldilocksField, VmTable, alu_op, zeroed_fe_vec, +}; /// Column indices for the FEXT_FMA table. pub mod cols { - // Timestamp (DWordWL: 2 cols) pub const TIMESTAMP_0: usize = 0; pub const TIMESTAMP_1: usize = 1; @@ -60,17 +64,43 @@ pub mod cols { pub const OUT1: usize = 20; pub const OUT2: usize = 21; - /// Multiplicity bit (1 for real rows, 0 for padding). + /// Multiplicity bit. pub const MU: usize = 22; - pub const NUM_COLUMNS: usize = 23; + // 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 + } } -/// FEXT_FMA syscall number split into the two 32-bit limbs the `Ecall` bus carries. 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: `output = a*b + c`, with operand addresses. +/// One FEXT_FMA invocation. #[derive(Debug, Clone)] pub struct FextFmaOperation { pub timestamp: u64, @@ -78,17 +108,20 @@ pub struct FextFmaOperation { pub a_addr: u64, pub b_addr: u64, pub c_addr: u64, - /// Coefficients of `a`, `b`, `c` (canonical field elements). pub a: [u64; 3], pub b: [u64; 3], pub c: [u64; 3], - /// Result coefficients `a*b + c` (canonical). 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`), which satisfies the -/// arithmetic constraints (`0 = 0`) and `IS_BIT μ`. +/// of two (min 4). Padding rows are all-zero (`μ = 0`). pub fn generate_fext_fma_trace( ops: &[FextFmaOperation], ) -> TraceTable { @@ -107,14 +140,16 @@ pub fn generate_fext_fma_trace( 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 (i, base) in [cols::A0, cols::B0, cols::C0].into_iter().enumerate() { - let coeffs = [op.a, op.b, op.c][i]; - for (k, &v) in coeffs.iter().enumerate() { - table.set_fe(row, base + k, FE::from(v)); + 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 (k, &v) in op.output.iter().enumerate() { - table.set_fe(row, cols::OUT0 + k, FE::from(v)); + 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()); @@ -123,49 +158,41 @@ pub fn generate_fext_fma_trace( trace } -/// A single MEMW register-read interaction (24-element CO24 read: `old == value`, -/// `is_register = 1`, `write2 = 1`). `reg` is the register index; the register -/// file is byte-addressed ×2, so the base address is `2*reg`. -fn memw_register_read(addr_lo: usize, addr_hi: usize, reg: u64) -> BusInteraction { - let addr = |col| BusValue::Packed { +fn direct(col: usize) -> BusValue { + BusValue::Packed { start_column: col, packing: Packing::Direct, - }; - let ts = |col| 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![ - // old[0..7] = [addr_lo, addr_hi, 0, 0, 0, 0, 0, 0] - addr(addr_lo), - addr(addr_hi), + direct(lo), + direct(hi), BusValue::constant(0), BusValue::constant(0), BusValue::constant(0), BusValue::constant(0), BusValue::constant(0), BusValue::constant(0), - // is_register = 1 BusValue::constant(1), - // base_address = [2*reg, 0] BusValue::constant(2 * reg), BusValue::constant(0), - // value[0..7] = same as old (read) - addr(addr_lo), - addr(addr_hi), + direct(lo), + direct(hi), BusValue::constant(0), BusValue::constant(0), BusValue::constant(0), BusValue::constant(0), BusValue::constant(0), BusValue::constant(0), - // timestamp - ts(cols::TIMESTAMP_0), - ts(cols::TIMESTAMP_1), - // w2 = 1, w4 = 0, w8 = 0 (register = 2 words) + direct(cols::TIMESTAMP_0), + direct(cols::TIMESTAMP_1), BusValue::constant(1), BusValue::constant(0), BusValue::constant(0), @@ -173,33 +200,115 @@ fn memw_register_read(addr_lo: usize, addr_hi: usize, reg: u64) -> BusInteractio ) } -/// Bus interactions for the FEXT_FMA table (this phase: `Ecall` receiver + -/// 4 register reads). Field-storage `Memory` tokens are added later. +/// `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 { - vec![ - // Receive the ECALL from the CPU, keyed by the FEXT_FMA syscall number. + 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, - }, + direct(cols::TIMESTAMP_0), + direct(cols::TIMESTAMP_1), BusValue::constant(FMA_SYSCALL_LO), BusValue::constant(FMA_SYSCALL_HI), ], ), - // Register reads: x10=out, x11=a, x12=b, x13=c. - memw_register_read(cols::OUT_ADDR_0, cols::OUT_ADDR_1, 10), - memw_register_read(cols::A_ADDR_0, cols::A_ADDR_1, 11), - memw_register_read(cols::B_ADDR_0, cols::B_ADDR_1, 12), - memw_register_read(cols::C_ADDR_0, cols::C_ADDR_1, 13), - ] + 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: diff --git a/prover/src/tables/fext_load.rs b/prover/src/tables/fext_load.rs index db67ec54c..d6c3f634a 100644 --- a/prover/src/tables/fext_load.rs +++ b/prover/src/tables/fext_load.rs @@ -2,21 +2,26 @@ //! 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 coefficient `< p` (canonical -//! Goldilocks element) via the ALU `LT` bus, and writes them into field-storage -//! (memory domains 3/4/5) at the destination address. +//! 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`). //! -//! ## Bus interactions (this phase) +//! 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. -//! -//! The field-storage writes (memory domains 3/4/5, value = `lo + 2^32*hi` per -//! coefficient) and the domain init/finalization are added in the field-storage -//! phase. Unlike the draft spec, this write is a genuine memory *write*, not a -//! read-assert (draft bug: `output = value` forces `old == value`). +//! - **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, Multiplicity, Packing}; +use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing}; use stark::trace::TraceTable; use executor::vm::instruction::execution::FEXT_LOAD_SYSCALL_NUMBER; @@ -24,7 +29,7 @@ use executor::vm::instruction::execution::FEXT_LOAD_SYSCALL_NUMBER; use crate::constraints::templates::emit_is_bit; use super::types::{ - BusId, FE, GoldilocksExtension, GoldilocksField, VmTable, alu_op, zeroed_fe_vec, + BusId, FE, GoldilocksExtension, GoldilocksField, SHIFT_32, VmTable, alu_op, zeroed_fe_vec, }; /// Column indices for the FEXT_LOAD table. @@ -48,12 +53,32 @@ pub mod cols { /// Multiplicity bit. pub const MU: usize = 10; - pub const NUM_COLUMNS: usize = 11; + // 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; @@ -72,6 +97,10 @@ pub struct FextLoadOperation { 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, @@ -90,8 +119,10 @@ pub fn generate_fext_load_trace( 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, &c) in op.coeffs.iter().enumerate() { - table.set_dword_wl(row, cols::coeff(i), c); + 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()); } @@ -138,19 +169,20 @@ fn memw_register_read(lo: usize, hi: usize, reg: u64) -> BusInteraction { ) } -/// `coeff < p` on the unified ALU bus: `[coeff(DWordWL), p(DWordWL), opsel(LT), 1, 0]` -/// (unsigned, non-inverted, asserting the result is 1). -fn coeff_lt_p(coeff_lo: usize) -> BusInteraction { +/// `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: coeff_lo, + start_column: lhs_lo, packing: Packing::DWordWL, }, - BusValue::constant(P_LO), - BusValue::constant(P_HI), + rhs_lo, + rhs_hi, BusValue::constant(alu_op::LT as u64), BusValue::constant(1), BusValue::constant(0), @@ -158,8 +190,100 @@ fn coeff_lt_p(coeff_lo: usize) -> BusInteraction { ) } -/// Bus interactions for FEXT_LOAD (this phase): `Ecall` receiver + 4 register -/// reads + 3 `< p` range checks. Field-storage writes are added later. +/// 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( @@ -184,13 +308,16 @@ pub fn bus_interactions() -> Vec { memw_register_read(cols::C2_0, cols::C2_1, 13), ]; for i in 0..3 { - interactions.push(coeff_lt_p(cols::coeff(i))); + 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 is -/// enforced by the ALU `LT` bus interactions, not by polynomial constraints. +/// 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 { diff --git a/prover/src/tables/fext_page.rs b/prover/src/tables/fext_page.rs new file mode 100644 index 000000000..b2f2f3fbb --- /dev/null +++ b/prover/src/tables/fext_page.rs @@ -0,0 +1,121 @@ +//! 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. +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; +use stark::lookup::{BusInteraction, BusValue, Multiplicity, Packing}; +use stark::trace::TraceTable; + +use crate::constraints::templates::emit_is_bit; + +use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField, VmTable, zeroed_fe_vec}; + +/// 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; + + pub const NUM_COLUMNS: usize = 7; +} + +/// 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). Padding rows are all-zero (`μ = 0`) and contribute nothing. +pub fn generate_fext_page_trace( + ops: &[FextPageOperation], +) -> 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_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()); + } + + 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. +pub fn bus_interactions() -> Vec { + 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), + ], + ), + ] +} + +/// FEXT_PAGE constraints: idx 0 is `IS_BIT(μ)`. +pub struct FextPageConstraints; + +impl ConstraintSet for FextPageConstraints { + fn eval>(&self, b: &mut B) { + emit_is_bit(b, 0, cols::MU, None); + } +} diff --git a/prover/src/tables/mod.rs b/prover/src/tables/mod.rs index 0fc46673c..b609a270d 100644 --- a/prover/src/tables/mod.rs +++ b/prover/src/tables/mod.rs @@ -34,6 +34,7 @@ pub mod ecsm; pub mod eq; pub mod fext_fma; pub mod fext_load; +pub mod fext_page; pub mod global_memory; pub mod halt; pub mod keccak; diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 5c6b3085e..8a9c7d921 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -50,6 +50,9 @@ 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_page; use super::halt; use super::keccak::{self, KeccakOperation}; use super::keccak_rc; @@ -538,6 +541,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 +553,8 @@ fn collect_ops_from_cpu( 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 +566,8 @@ 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(); // 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 +662,19 @@ 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); + } + // --- 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 +730,8 @@ fn collect_ops_from_cpu( cpu32_ops, ecsm_ops, ecdas_ops, + fext_load_ops, + fext_fma_ops, ) } @@ -948,6 +971,162 @@ 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)>, +} + +impl FieldStorageState { + /// Current `(value, last_ts)` of a cell (`(0, 0)` if never touched — the + /// zero-init token FEXT_PAGE emits). + fn read(&self, domain: u64, addr: u64) -> (u64, u64) { + self.cells.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. + 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 + } +} + +/// 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 register read/write operations (M1, M3, M5) from CpuOperation, /// pushing them into `memw_ops`. fn collect_register_ops_from_cpu( @@ -1484,6 +1663,40 @@ 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 +} + /// Checks whether a MEMW operation qualifies for the aligned fast path (MEMW_A). /// /// An operation is aligned if: @@ -2079,7 +2292,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 +2941,15 @@ 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_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 @@ -2765,6 +2992,10 @@ 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_page_ops: Vec, } /// Chunk raw ops and generate one trace table per chunk. When `storage_mode` @@ -2819,6 +3050,9 @@ fn collect_all_ops( cpu32_ops: Vec, ecsm_ops: Vec, ecdas_ops: Vec, + fext_load_ops: Vec, + fext_fma_ops: Vec, + fext_page_ops: Vec, register_state: &mut RegisterState, is_final: bool, ) -> CollectedOps { @@ -2961,6 +3195,9 @@ fn collect_all_ops( cpu32_ops, ecsm_ops, ecdas_ops, + fext_load_ops, + fext_fma_ops, + fext_page_ops, } } @@ -3004,6 +3241,9 @@ fn build_traces( cpu32_ops, ecsm_ops, ecdas_ops, + fext_load_ops, + fext_fma_ops, + fext_page_ops, } = ops; // ===================================================================== @@ -3011,6 +3251,8 @@ 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)); // ===================================================================== // PHASE 4: All → Bitwise lookups @@ -3365,6 +3607,10 @@ 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_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 +3623,7 @@ 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); #[cfg(feature = "disk-spill")] let sequential = storage_mode == StorageMode::Disk || cfg!(not(feature = "parallel")); @@ -3418,6 +3665,9 @@ 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_page_slot, gen_fext_page); }); } else { cpus_slot = Some(gen_cpus()); @@ -3445,6 +3695,9 @@ 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_page_slot = Some(gen_fext_page()); } const PHASE5_RAN: &str = "phase 5 generation ran in one of the branches above"; @@ -3479,6 +3732,9 @@ 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_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. @@ -3546,6 +3802,9 @@ 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_page: fext_page_trace, memw_registers, local_to_global, touched_memory_cells, @@ -3807,6 +4066,9 @@ 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::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 +4108,9 @@ impl Traces { keccak_rc, ecsm, ecdas, + fext_load, + fext_fma, + fext_page, memw_registers, eqs, bytewises, @@ -3913,6 +4178,9 @@ 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_page.num_rows() * FEXT_PAGE_COLS) as u64; total } @@ -3954,6 +4222,9 @@ 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_page = aux_cols(super::fext_page::bus_interactions().len()); let Traces { cpus, @@ -3976,6 +4247,9 @@ impl Traces { keccak_rc, ecsm, ecdas, + fext_load, + fext_fma, + fext_page, memw_registers, eqs, bytewises, @@ -4043,6 +4317,9 @@ 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_page.num_rows() * n_fext_page) as u64; total } @@ -4254,6 +4531,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::default(); let ( memw_ops, load_ops, @@ -4265,7 +4543,14 @@ 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, + ) = collect_ops_from_cpu( + &cpu_ops, + &mut memory_state, + &mut register_state, + &mut field_state, + ); #[cfg(feature = "instruments")] drop(__sp); @@ -4283,6 +4568,9 @@ impl Traces { cpu32_ops, ecsm_ops, ecdas_ops, + fext_load_ops, + fext_fma_ops, + field_state.into_page_ops(), &mut register_state, is_final, ); @@ -4331,6 +4619,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 +4631,14 @@ 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, + ) = collect_ops_from_cpu( + &cpu_ops, + &mut memory_state, + &mut register_state, + &mut field_state, + ); let ops = collect_all_ops( cpu_ops, @@ -4356,6 +4652,9 @@ impl Traces { cpu32_ops, ecsm_ops, ecdas_ops, + fext_load_ops, + fext_fma_ops, + field_state.into_page_ops(), &mut register_state, true, ); diff --git a/prover/src/test_utils.rs b/prover/src/test_utils.rs index 6dd28ce71..92b7c5d4d 100644 --- a/prover/src/test_utils.rs +++ b/prover/src/test_utils.rs @@ -64,6 +64,15 @@ 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::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 +956,39 @@ 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_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/fext_fma_tests.rs b/prover/src/tests/fext_fma_tests.rs index 2912668b3..1f00a5b77 100644 --- a/prover/src/tests/fext_fma_tests.rs +++ b/prover/src/tests/fext_fma_tests.rs @@ -45,6 +45,9 @@ fn op(a: [u64; 3], b: [u64; 3], c: [u64; 3]) -> FextFmaOperation { b, c, output: fma(a, b, c), + read_old_ts: [[0; 3]; 3], + write_old_ts: [0; 3], + write_old_val: [0; 3], } } @@ -86,8 +89,9 @@ fn fext_fma_max_degree_is_two() { #[test] fn fext_fma_bus_interaction_count() { - // 1 Ecall receiver + 4 register reads. - assert_eq!(bus_interactions().len(), 5); + // 1 Ecall + 4 register reads + 9 field reads + 3 field writes, each + // field access = consume-old + emit-new + old_ts FextLoadOperation { timestamp: 100, addr, coeffs, + old_ts: [0; 3], + old_val: [0; 3], } } @@ -52,8 +54,9 @@ fn fext_load_constraint_count_is_one() { #[test] fn fext_load_bus_interaction_count() { - // 1 Ecall receiver + 4 register reads + 3 range checks. - assert_eq!(bus_interactions().len(), 8); + // 1 Ecall receiver + 4 register reads + 3 range checks + 3 field-storage + // writes × (consume-old, emit-new, old_ts Date: Tue, 14 Jul 2026 18:11:33 -0300 Subject: [PATCH 04/17] Add FEXT_STORE accelerator and benchmark --- bin/cli/src/main.rs | 17 +- executor/programs/asm/fext_bench.s | 44 +++ executor/programs/asm/test_fext.s | 6 + .../rust/fext_baseline/.cargo/config.toml | 5 + .../programs/rust/fext_baseline/Cargo.lock | 331 ++++++++++++++++++ .../programs/rust/fext_baseline/Cargo.toml | 9 + .../programs/rust/fext_baseline/src/main.rs | 77 ++++ executor/src/tests/fext_tests.rs | 36 +- executor/src/vm/instruction/execution.rs | 22 ++ prover/benches/vm_prover_benchmark.rs | 2 + prover/src/lib.rs | 13 +- prover/src/tables/cpu.rs | 5 + prover/src/tables/fext_store.rs | 279 +++++++++++++++ prover/src/tables/mod.rs | 1 + prover/src/tables/trace_builder.rs | 105 ++++++ prover/src/test_utils.rs | 15 + prover/src/tests/fext_store_tests.rs | 73 ++++ prover/src/tests/mod.rs | 2 + prover/src/tests/prove_elfs_tests.rs | 4 +- syscalls/src/syscalls.rs | 29 ++ 20 files changed, 1065 insertions(+), 10 deletions(-) create mode 100644 executor/programs/asm/fext_bench.s create mode 100644 executor/programs/rust/fext_baseline/.cargo/config.toml create mode 100644 executor/programs/rust/fext_baseline/Cargo.lock create mode 100644 executor/programs/rust/fext_baseline/Cargo.toml create mode 100644 executor/programs/rust/fext_baseline/src/main.rs create mode 100644 prover/src/tables/fext_store.rs create mode 100644 prover/src/tests/fext_store_tests.rs diff --git a/bin/cli/src/main.rs b/bin/cli/src/main.rs index 63ce828da..ec19185ad 100644 --- a/bin/cli/src/main.rs +++ b/bin/cli/src/main.rs @@ -397,7 +397,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, 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 @@ -467,6 +467,7 @@ fn cmd_execute( 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` @@ -501,6 +502,7 @@ fn cmd_execute( 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 => {} } } @@ -515,18 +517,27 @@ fn cmd_execute( } if cycles { - accel_counts = Some((keccak_calls, ecsm_calls, fext_load_calls, fext_fma_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, fext_load_calls, fext_fma_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/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 index 42c0712b8..57d451483 100644 --- a/executor/programs/asm/test_fext.s +++ b/executor/programs/asm/test_fext.s @@ -35,6 +35,12 @@ main: 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 diff --git a/executor/programs/rust/fext_baseline/.cargo/config.toml b/executor/programs/rust/fext_baseline/.cargo/config.toml new file mode 100644 index 000000000..ca99a3f45 --- /dev/null +++ b/executor/programs/rust/fext_baseline/.cargo/config.toml @@ -0,0 +1,5 @@ +[target.riscv64im-lambda-vm-elf] +rustflags = [ + "--cfg", "getrandom_backend=\"custom\"", + "-C", "passes=lower-atomic" +] diff --git a/executor/programs/rust/fext_baseline/Cargo.lock b/executor/programs/rust/fext_baseline/Cargo.lock new file mode 100644 index 000000000..1357d3ef3 --- /dev/null +++ b/executor/programs/rust/fext_baseline/Cargo.lock @@ -0,0 +1,331 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 4 + +[[package]] +name = "base64" +version = "0.13.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9e1b586273c5702936fe7b7d6896644d8be71e6314cfe09d3167c95f712589e8" + +[[package]] +name = "cfg-if" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801" + +[[package]] +name = "const-default" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0b396d1f76d455557e1218ec8066ae14bba60b4b36ecd55577ba979f5db7ecaa" + +[[package]] +name = "critical-section" +version = "1.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "790eea4361631c5e7d22598ecd5723ff611904e3344ce8720784c93e3d83d40b" + +[[package]] +name = "embedded-alloc" +version = "0.6.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8f2de9133f68db0d4627ad69db767726c99ff8585272716708227008d3f1bddd" +dependencies = [ + "const-default", + "critical-section", + "linked_list_allocator", + "rlsf", +] + +[[package]] +name = "embedded-hal" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "361a90feb7004eca4019fb28352a9465666b24f840f5c3cddf0ff13920590b89" + +[[package]] +name = "fext_baseline" +version = "0.1.0" +dependencies = [ + "lambda-vm-syscalls", +] + +[[package]] +name = "getrandom" +version = "0.2.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ff2abc00be7fca6ebc474524697ae276ad847ad0a6b3faa4bcb027e9a4614ad0" +dependencies = [ + "cfg-if", + "libc", + "wasi", +] + +[[package]] +name = "getrandom" +version = "0.3.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "899def5c37c4fd7b2664648c28120ecec138e4d395b459e5ca34f9cce2dd77fd" +dependencies = [ + "cfg-if", + "libc", + "r-efi", + "wasip2", +] + +[[package]] +name = "lambda-vm-syscalls" +version = "0.1.0" +dependencies = [ + "embedded-alloc", + "getrandom 0.2.17", + "getrandom 0.3.4", + "lazy_static", + "rand", + "riscv", + "thiserror", +] + +[[package]] +name = "lazy_static" +version = "1.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe" + +[[package]] +name = "libc" +version = "0.2.186" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "68ab91017fe16c622486840e4c83c9a37afeff978bd239b5293d61ece587de66" + +[[package]] +name = "linked_list_allocator" +version = "0.10.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2b23ac50abb8261cb38c6e2a7192d3302e0836dac1628f6a93b82b4fad185897" + +[[package]] +name = "paste" +version = "1.0.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "57c0d7b74b563b49d38dae00a0c37d4d6de9b432382b2892f0574ddcae73fd0a" + +[[package]] +name = "ppv-lite86" +version = "0.2.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "85eae3c4ed2f50dcfe72643da4befc30deadb458a9b590d720cde2f2b1e97da9" +dependencies = [ + "zerocopy", +] + +[[package]] +name = "proc-macro2" +version = "1.0.106" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "quote" +version = "1.0.46" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dfbc457d0c7a0759a614551b11a6409e5951f6c7537be1f1b7682b9ae9230368" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "r-efi" +version = "5.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "69cdb34c158ceb288df11e18b4bd39de994f6657d83847bdffdbd7f346754b0f" + +[[package]] +name = "rand" +version = "0.9.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b9ef1d0d795eb7d84685bca4f72f3649f064e6641543d3a8c415898726a57b41" +dependencies = [ + "rand_chacha", + "rand_core", +] + +[[package]] +name = "rand_chacha" +version = "0.9.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d3022b5f1df60f26e1ffddd6c66e8aa15de382ae63b3a0c1bfc0e4d3e3f325cb" +dependencies = [ + "ppv-lite86", + "rand_core", +] + +[[package]] +name = "rand_core" +version = "0.9.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "76afc826de14238e6e8c374ddcc1fa19e374fd8dd986b0d2af0d02377261d83c" +dependencies = [ + "getrandom 0.3.4", +] + +[[package]] +name = "riscv" +version = "0.15.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b05cfa3f7b30c84536a9025150d44d26b8e1cc20ddf436448d74cd9591eefb25" +dependencies = [ + "critical-section", + "embedded-hal", + "paste", + "riscv-macros", + "riscv-pac", +] + +[[package]] +name = "riscv-macros" +version = "0.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7d323d13972c1b104aa036bc692cd08b822c8bbf23d79a27c526095856499799" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.118", +] + +[[package]] +name = "riscv-pac" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8188909339ccc0c68cfb5a04648313f09621e8b87dc03095454f1a11f6c5d436" + +[[package]] +name = "rlsf" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1646a59a9734b8b7a0ac51689388a60fe1625d4b956348e9de07591a1478457a" +dependencies = [ + "cfg-if", + "const-default", + "libc", + "rustversion", + "svgbobdoc", +] + +[[package]] +name = "rustversion" +version = "1.0.23" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cf54715a573b99ac80df0bc206da022bcd442c974952c7b9720069370852e21f" + +[[package]] +name = "svgbobdoc" +version = "0.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f2c04b93fc15d79b39c63218f15e3fdffaa4c227830686e3b7c5f41244eb3e50" +dependencies = [ + "base64", + "proc-macro2", + "quote", + "syn 1.0.109", + "unicode-width", +] + +[[package]] +name = "syn" +version = "1.0.109" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "syn" +version = "2.0.118" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1b9ae57f904213ebb649ce6895b8a66c66f0203b9319718f69a5612a065b1422" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "thiserror" +version = "1.0.69" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b6aaf5339b578ea85b50e080feb250a3e8ae8cfcdff9a461c9ec2904bc923f52" +dependencies = [ + "thiserror-impl", +] + +[[package]] +name = "thiserror-impl" +version = "1.0.69" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4fee6c4efc90059e10f81e6d42c60a18f76588c3d74cb83a0b242a2b6c7504c1" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.118", +] + +[[package]] +name = "unicode-ident" +version = "1.0.24" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75" + +[[package]] +name = "unicode-width" +version = "0.1.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7dd6e30e90baa6f72411720665d41d89b9a3d039dc45b8faea1ddd07f617f6af" + +[[package]] +name = "wasi" +version = "0.11.1+wasi-snapshot-preview1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ccf3ec651a847eb01de73ccad15eb7d99f80485de043efb2f370cd654f4ea44b" + +[[package]] +name = "wasip2" +version = "1.0.4+wasi-0.2.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b67efb37e106e55ce722a510d6b5f9c17f083e5fc79afc2badeb12cc313d9487" +dependencies = [ + "wit-bindgen", +] + +[[package]] +name = "wit-bindgen" +version = "0.57.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1ebf944e87a7c253233ad6766e082e3cd714b5d03812acc24c318f549614536e" + +[[package]] +name = "zerocopy" +version = "0.8.54" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b7cbbc0a705a0fd05cc3676525980d2bf5a9bc4adac6d6475209a7887cf59d19" +dependencies = [ + "zerocopy-derive", +] + +[[package]] +name = "zerocopy-derive" +version = "0.8.54" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e2e817b7b52d0c7358d3246da9d69935ebb18116b2b102b4230dac079b4862f5" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.118", +] diff --git a/executor/programs/rust/fext_baseline/Cargo.toml b/executor/programs/rust/fext_baseline/Cargo.toml new file mode 100644 index 000000000..21269cd0d --- /dev/null +++ b/executor/programs/rust/fext_baseline/Cargo.toml @@ -0,0 +1,9 @@ +[workspace] + +[package] +name = "fext_baseline" +version = "0.1.0" +edition = "2024" + +[dependencies] +lambda-vm-syscalls = { path = "../../../../syscalls" } diff --git a/executor/programs/rust/fext_baseline/src/main.rs b/executor/programs/rust/fext_baseline/src/main.rs new file mode 100644 index 000000000..c04ea34b8 --- /dev/null +++ b/executor/programs/rust/fext_baseline/src/main.rs @@ -0,0 +1,77 @@ +//! Software baseline for the FEXT accelerator benchmark: computes N iterations +//! of `a = a*b + c` over the degree-3 Goldilocks extension `Fp[x]/(x^3 - 2)` in +//! plain RISC-V (no accelerator). Compared against `fext_bench.s` (same N via +//! FEXT_FMA) to measure the accelerator's proving-cost benefit. +use core::hint::black_box; +use lambda_vm_syscalls as syscalls; + +const P: u64 = 0xFFFF_FFFF_0000_0001; // Goldilocks prime, 2^64 - 2^32 + 1. + +/// Reduce a 128-bit product to a Goldilocks field element using +/// `2^64 ≡ 2^32 - 1` and `2^96 ≡ -1 (mod p)`. Representative of the real +/// reduction's instruction cost (overflow-safe). +#[inline(always)] +fn gold_reduce(x: u128) -> u64 { + let lo = x as u64; + let hi = (x >> 64) as u64; + let hi_hi = hi >> 32; + let hi_lo = hi & 0xFFFF_FFFF; + + let (a, borrow) = lo.overflowing_sub(hi_hi); + let a = if borrow { a.wrapping_add(P) } else { a }; + let t = hi_lo.wrapping_mul(0xFFFF_FFFF); + let (r, carry) = a.overflowing_add(t); + if carry { r.wrapping_sub(P) } else { r } +} + +#[inline(always)] +fn gmul(a: u64, b: u64) -> u64 { + gold_reduce((a as u128) * (b as u128)) +} + +#[inline(always)] +fn gadd(a: u64, b: u64) -> u64 { + let s = a as u128 + b as u128; + if s >= P as u128 { (s - P as u128) as u64 } else { s as u64 } +} + +/// `a*b + c` over Fp3 with `w^3 = 2` (same formula as the FEXT_FMA chip). +#[inline(always)] +fn fp3_fma(a: [u64; 3], b: [u64; 3], c: [u64; 3]) -> [u64; 3] { + let dbl = |x| gadd(x, x); + let o0 = gadd( + gadd(gmul(a[0], b[0]), dbl(gadd(gmul(a[1], b[2]), gmul(a[2], b[1])))), + c[0], + ); + let o1 = gadd( + gadd(gadd(gmul(a[0], b[1]), gmul(a[1], b[0])), dbl(gmul(a[2], b[2]))), + c[1], + ); + let o2 = gadd( + gadd(gadd(gmul(a[0], b[2]), gmul(a[1], b[1])), gmul(a[2], b[0])), + c[2], + ); + [o0, o1, o2] +} + +pub fn main() { + // black_box prevents constant-folding; the runtime loop bound prevents + // unrolling; feeding `a` back makes each iteration depend on the previous. + let mut a = [black_box(1u64), black_box(2), black_box(3)]; + let b = [black_box(4u64), black_box(5), black_box(6)]; + let c = [black_box(7u64), black_box(8), black_box(9)]; + + let n = black_box(4096u32); + let mut i = 0u32; + while i < n { + a = fp3_fma(black_box(a), b, c); + i += 1; + } + + // Commit the result so the loop is observable (not dead-code eliminated). + let mut out = [0u8; 24]; + out[0..8].copy_from_slice(&a[0].to_le_bytes()); + out[8..16].copy_from_slice(&a[1].to_le_bytes()); + out[16..24].copy_from_slice(&a[2].to_le_bytes()); + syscalls::syscalls::commit(&out); +} diff --git a/executor/src/tests/fext_tests.rs b/executor/src/tests/fext_tests.rs index 087ca9f37..e5e68be3b 100644 --- a/executor/src/tests/fext_tests.rs +++ b/executor/src/tests/fext_tests.rs @@ -3,7 +3,7 @@ use crate::vm::instruction::decoding::Instruction; use crate::vm::instruction::execution::{ - ExecutionError, FEXT_FMA_SYSCALL_NUMBER, FEXT_LOAD_SYSCALL_NUMBER, + ExecutionError, FEXT_FMA_SYSCALL_NUMBER, FEXT_LOAD_SYSCALL_NUMBER, FEXT_STORE_SYSCALL_NUMBER, }; use crate::vm::memory::Memory; use crate::vm::registers::Registers; @@ -89,6 +89,40 @@ fn fext_fma_rejects_overlapping_addresses() { 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(); diff --git a/executor/src/vm/instruction/execution.rs b/executor/src/vm/instruction/execution.rs index 9d41de6d2..b14cb7f27 100644 --- a/executor/src/vm/instruction/execution.rs +++ b/executor/src/vm/instruction/execution.rs @@ -23,6 +23,8 @@ pub enum SyscallNumbers { 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). @@ -48,6 +50,11 @@ pub const FEXT_LOAD_SYSCALL_NUMBER: u64 = u64::MAX - 19; /// 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; @@ -64,6 +71,7 @@ impl TryFrom for SyscallNumbers { 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(()), } } @@ -76,6 +84,7 @@ pub enum Accelerator { Ecsm, FextLoad, FextFma, + FextStore, } impl SyscallNumbers { @@ -88,6 +97,7 @@ impl SyscallNumbers { 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 @@ -545,6 +555,18 @@ impl Instruction { 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 { 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/lib.rs b/prover/src/lib.rs index e09ddd736..f63eecd15 100644 --- a/prover/src/lib.rs +++ b/prover/src/lib.rs @@ -54,8 +54,8 @@ 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_fext_fma_air, create_fext_load_air, - create_fext_page_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_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, }; @@ -79,8 +79,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, fext_load, fext_fma, fext_page. -pub const FIXED_TABLE_COUNT: usize = 13; +/// 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. @@ -263,6 +263,7 @@ pub(crate) struct VmAirs { 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, @@ -291,6 +292,7 @@ impl VmAirs { (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, &()), ]; @@ -368,6 +370,7 @@ impl VmAirs { 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(), ]; @@ -544,6 +547,7 @@ impl VmAirs { 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 { @@ -653,6 +657,7 @@ impl VmAirs { ecdas, fext_load, fext_fma, + fext_store, fext_page, register, pages, diff --git a/prover/src/tables/cpu.rs b/prover/src/tables/cpu.rs index 2ca286ba5..f9d243d0d 100644 --- a/prover/src/tables/cpu.rs +++ b/prover/src/tables/cpu.rs @@ -192,6 +192,8 @@ pub struct CpuOperation { 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 { @@ -245,6 +247,8 @@ impl CpuOperation { && 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 @@ -365,6 +369,7 @@ impl CpuOperation { ecall_ecsm, ecall_fext_load, ecall_fext_fma, + ecall_fext_store, } } diff --git a/prover/src/tables/fext_store.rs b/prover/src/tables/fext_store.rs new file mode 100644 index 000000000..f29a427d3 --- /dev/null +++ b/prover/src/tables/fext_store.rs @@ -0,0 +1,279 @@ +//! 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; + + pub const NUM_COLUMNS: usize = 17; + + /// 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 + } +} + +const STORE_SYSCALL_LO: u64 = FEXT_STORE_SYSCALL_NUMBER & 0xFFFF_FFFF; +const STORE_SYSCALL_HI: u64 = FEXT_STORE_SYSCALL_NUMBER >> 32; + +/// 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]); + } + 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), + ], + ) +} + +/// `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, + )); + } + interactions +} + +/// FEXT_STORE constraints: idx 0 is `IS_BIT(μ)`. +pub struct FextStoreConstraints; + +impl ConstraintSet for FextStoreConstraints { + fn eval>(&self, b: &mut B) { + emit_is_bit(b, 0, cols::MU, None); + } +} diff --git a/prover/src/tables/mod.rs b/prover/src/tables/mod.rs index b609a270d..5bca51291 100644 --- a/prover/src/tables/mod.rs +++ b/prover/src/tables/mod.rs @@ -35,6 +35,7 @@ pub mod eq; pub mod fext_fma; pub mod fext_load; pub mod fext_page; +pub mod fext_store; pub mod global_memory; pub mod halt; pub mod keccak; diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 8a9c7d921..3a788ea71 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -53,6 +53,7 @@ use super::eq; use super::fext_fma; use super::fext_load; use super::fext_page; +use super::fext_store; use super::halt; use super::keccak::{self, KeccakOperation}; use super::keccak_rc; @@ -555,6 +556,7 @@ fn collect_ops_from_cpu( 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); @@ -568,6 +570,7 @@ fn collect_ops_from_cpu( 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 @@ -674,6 +677,11 @@ fn collect_ops_from_cpu( 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 @@ -732,6 +740,7 @@ fn collect_ops_from_cpu( ecdas_ops, fext_load_ops, fext_fma_ops, + fext_store_ops, ) } @@ -1127,6 +1136,65 @@ fn collect_fext_fma_ops( ) } +/// 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( @@ -1697,6 +1765,19 @@ fn collect_lt_from_fext_fma(ops: &[fext_fma::FextFmaOperation]) -> Vec Vec { + let mut lt_ops = Vec::with_capacity(ops.len() * 3); + for op in ops { + for d in 0..3 { + lt_ops.push(LtOperation::new(op.old_ts[d], op.timestamp, false)); + } + } + lt_ops +} + /// Checks whether a MEMW operation qualifies for the aligned fast path (MEMW_A). /// /// An operation is aligned if: @@ -2947,6 +3028,9 @@ pub struct Traces { /// 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, @@ -2995,6 +3079,7 @@ struct CollectedOps { // Field-extension accelerator chips. fext_load_ops: Vec, fext_fma_ops: Vec, + fext_store_ops: Vec, fext_page_ops: Vec, } @@ -3052,6 +3137,7 @@ fn collect_all_ops( 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, @@ -3197,6 +3283,7 @@ fn collect_all_ops( ecdas_ops, fext_load_ops, fext_fma_ops, + fext_store_ops, fext_page_ops, } } @@ -3243,6 +3330,7 @@ fn build_traces( ecdas_ops, fext_load_ops, fext_fma_ops, + fext_store_ops, fext_page_ops, } = ops; @@ -3253,6 +3341,7 @@ fn build_traces( 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)); // ===================================================================== // PHASE 4: All → Bitwise lookups @@ -3610,6 +3699,7 @@ fn build_traces( // 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) = @@ -3624,6 +3714,7 @@ fn build_traces( (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")); @@ -3667,6 +3758,7 @@ fn build_traces( 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 { @@ -3697,6 +3789,7 @@ fn build_traces( 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()); } @@ -3734,6 +3827,7 @@ fn build_traces( 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`, @@ -3804,6 +3898,7 @@ fn build_traces( 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, @@ -4069,6 +4164,7 @@ impl Traces { 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; @@ -4110,6 +4206,7 @@ impl Traces { ecdas, fext_load, fext_fma, + fext_store, fext_page, memw_registers, eqs, @@ -4180,6 +4277,7 @@ impl Traces { 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 } @@ -4224,6 +4322,7 @@ impl Traces { 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 { @@ -4249,6 +4348,7 @@ impl Traces { ecdas, fext_load, fext_fma, + fext_store, fext_page, memw_registers, eqs, @@ -4319,6 +4419,7 @@ impl Traces { 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 } @@ -4545,6 +4646,7 @@ impl Traces { ecdas_ops, fext_load_ops, fext_fma_ops, + fext_store_ops, ) = collect_ops_from_cpu( &cpu_ops, &mut memory_state, @@ -4570,6 +4672,7 @@ impl Traces { ecdas_ops, fext_load_ops, fext_fma_ops, + fext_store_ops, field_state.into_page_ops(), &mut register_state, is_final, @@ -4633,6 +4736,7 @@ impl Traces { ecdas_ops, fext_load_ops, fext_fma_ops, + fext_store_ops, ) = collect_ops_from_cpu( &cpu_ops, &mut memory_state, @@ -4654,6 +4758,7 @@ impl Traces { ecdas_ops, fext_load_ops, fext_fma_ops, + fext_store_ops, field_state.into_page_ops(), &mut register_state, true, diff --git a/prover/src/test_utils.rs b/prover/src/test_utils.rs index 92b7c5d4d..5f838cc37 100644 --- a/prover/src/test_utils.rs +++ b/prover/src/test_utils.rs @@ -73,6 +73,9 @@ use crate::tables::fext_load::{ 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, @@ -981,6 +984,18 @@ pub fn create_fext_fma_air(proof_options: &ProofOptions) -> ConcreteVmAir 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( diff --git a/prover/src/tests/fext_store_tests.rs b/prover/src/tests/fext_store_tests.rs new file mode 100644 index 000000000..b2db83ec1 --- /dev/null +++ b/prover/src/tests/fext_store_tests.rs @@ -0,0 +1,73 @@ +//! 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; +use stark::constraints::builder::ConstraintSet; + +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_one() { + // Only IS_BIT(μ). + assert_eq!(FextStoreConstraints.meta().len(), 1); +} + +#[test] +fn fext_store_bus_interaction_count() { + // 1 Ecall + 1 register read (x10) + 3 field reads (consume + emit + old_ts [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 From 6cc1bc2c39deb5870034343e8c7aad034c8e61e1 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Thu, 16 Jul 2026 12:04:36 -0300 Subject: [PATCH 05/17] Constrain FEXT_STORE read-back coefficients to canonical form --- prover/src/tables/fext_store.rs | 84 +++++++++++++++++++++++++++- prover/src/tables/trace_builder.rs | 32 ++++++++++- prover/src/tests/fext_store_tests.rs | 11 ++-- 3 files changed, 119 insertions(+), 8 deletions(-) diff --git a/prover/src/tables/fext_store.rs b/prover/src/tables/fext_store.rs index f29a427d3..fd347ca51 100644 --- a/prover/src/tables/fext_store.rs +++ b/prover/src/tables/fext_store.rs @@ -51,7 +51,14 @@ pub mod cols { /// Multiplicity bit. pub const MU: usize = 16; - pub const NUM_COLUMNS: usize = 17; + // 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 { @@ -61,11 +68,22 @@ pub mod cols { 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 { @@ -96,6 +114,15 @@ pub fn generate_fext_store_trace( 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()); } @@ -187,6 +214,37 @@ fn memw_register_write(reg: u64, lo: usize, hi: usize) -> BusInteraction { ) } +/// `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( @@ -266,14 +324,36 @@ pub fn bus_interactions() -> Vec { 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(μ)`. +/// 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/trace_builder.rs b/prover/src/tables/trace_builder.rs index 3a788ea71..6430db499 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -1769,15 +1769,44 @@ fn collect_lt_from_fext_fma(ops: &[fext_fma::FextFmaOperation]) -> Vec Vec { - let mut lt_ops = Vec::with_capacity(ops.len() * 3); + 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 +} + /// Checks whether a MEMW operation qualifies for the aligned fast path (MEMW_A). /// /// An operation is aligned if: @@ -3410,6 +3439,7 @@ 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| add_padding_byte_checks(h, num_padding_rows)), ]; if let Some(image) = initial_image diff --git a/prover/src/tests/fext_store_tests.rs b/prover/src/tests/fext_store_tests.rs index b2db83ec1..2902af824 100644 --- a/prover/src/tests/fext_store_tests.rs +++ b/prover/src/tests/fext_store_tests.rs @@ -17,16 +17,17 @@ fn op(coeffs: [u64; 3]) -> FextStoreOperation { } #[test] -fn fext_store_constraint_count_is_one() { - // Only IS_BIT(μ). - assert_eq!(FextStoreConstraints.meta().len(), 1); +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 Date: Thu, 16 Jul 2026 12:42:39 -0300 Subject: [PATCH 06/17] reject FEXT accelerator ecalls under continuation --- prover/src/lib.rs | 13 ++++++++++++ prover/src/tables/trace_builder.rs | 13 ++++++++++++ prover/src/tests/prove_elfs_tests.rs | 30 ++++++++++++++++++++++++++++ 3 files changed, 56 insertions(+) diff --git a/prover/src/lib.rs b/prover/src/lib.rs index 375ff2e05..419c06249 100644 --- a/prover/src/lib.rs +++ b/prover/src/lib.rs @@ -203,6 +203,12 @@ pub enum Error { /// A non-final continuation epoch contains the program-terminating /// instruction. The terminating instruction must be in the final epoch. HaltInNonFinalEpoch, + /// A FEXT (field-extension) accelerator ecall was used under continuation. + /// Field-storage is not carried across epochs yet (only RAM and registers + /// are), so a value written in one epoch would read back as zero in the + /// next — an unsound reset. Rejected until L2G field-storage carry lands; + /// prove monolithically in the meantime. + FextInContinuation, /// Recursion host-side helper failed (guest-input encoding or /// commitment recompute — see the `recursion` module). Recursion(String), @@ -234,6 +240,13 @@ impl fmt::Display for Error { "the program-terminating instruction must be in the final epoch" ) } + Error::FextInContinuation => { + write!( + f, + "FEXT accelerator ecalls are not supported under continuation \ + (field-storage is not carried across epochs); prove monolithically" + ) + } Error::Recursion(msg) => write!(f, "recursion helper error: {msg}"), } } diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 6430db499..1034a6c64 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -3337,6 +3337,19 @@ fn build_traces( is_final: bool, l2g_memory_bookend: bool, ) -> Result { + // Interim soundness guard: field-storage is NOT carried across continuation + // epochs (RAM and registers are, but `field_state` resets to default each + // epoch), so a FEXT value written in one epoch would read back as zero in the + // next — an unsound reset. Reject any FEXT accelerator use under continuation + // until L2G field-storage carry lands (monolithic proving is unaffected, as it + // carries field-storage within the single proof via the FEXT_PAGE bookend). + if l2g_memory_bookend + && (!ops.fext_load_ops.is_empty() + || !ops.fext_fma_ops.is_empty() + || !ops.fext_store_ops.is_empty()) + { + return Err(Error::FextInContinuation); + } let CollectedOps { cpu_ops, memw_ops, diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index 325e52788..9a4a0312b 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -3381,6 +3381,36 @@ fn test_continuation_pipeline_end_to_end() { ); } +/// FEXT accelerator ecalls under continuation (`l2g_memory_bookend = true`) are +/// rejected: field-storage is not carried across epochs, so a written value would +/// read back as zero in the next epoch. The guard must fire before any trace is built. +#[test] +fn fext_rejected_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, + ); + match result { + Err(crate::Error::FextInContinuation) => {} + Err(e) => panic!("expected FextInContinuation, got a different error: {e}"), + Ok(_) => panic!("expected FextInContinuation, but trace building succeeded"), + } +} + /// 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 From 1fe2996ed0fe94d04861157adbb31f8e8556a6d5 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Thu, 16 Jul 2026 14:08:14 -0300 Subject: [PATCH 07/17] Pin FEXT_PAGE domain to {3,4,5} to prevent forged Memory-bus tokens --- prover/src/tables/fext_page.rs | 23 ++++++++++++++++++++++- prover/src/tests/fext_page_tests.rs | 5 +++-- 2 files changed, 25 insertions(+), 3 deletions(-) diff --git a/prover/src/tables/fext_page.rs b/prover/src/tables/fext_page.rs index b2f2f3fbb..e3aa780f7 100644 --- a/prover/src/tables/fext_page.rs +++ b/prover/src/tables/fext_page.rs @@ -68,6 +68,12 @@ pub fn generate_fext_page_trace( table.set_fe(row, cols::MU, FE::one()); } + // Padding rows carry a valid domain (3) so the ungated domain constraint + // holds on every row; μ = 0 keeps them out of the bus. + for row in ops.len()..num_rows { + table.set_fe(row, cols::DOMAIN, FE::from(3u64)); + } + trace } @@ -111,11 +117,26 @@ pub fn bus_interactions() -> Vec { ] } -/// FEXT_PAGE constraints: idx 0 is `IS_BIT(μ)`. +/// FEXT_PAGE constraints: idx 0 is `IS_BIT(μ)`, idx 1 pins the domain to +/// `{3, 4, 5}` (the field-storage coefficient domains). pub struct FextPageConstraints; impl ConstraintSet for FextPageConstraints { fn eval>(&self, b: &mut B) { emit_is_bit(b, 0, cols::MU, None); + + // Domain ∈ {3, 4, 5}: `(D - 3)(D - 4)(D - 5) = 0`. The domain feeds the + // shared Memory bus, so leaving it a free witness would let a prover forge + // tokens in another domain's chain (e.g. domain 0 = RAM). Ungated (degree + // 3, within budget); padding rows carry domain 3 so it holds everywhere. + let d = b.main(0, cols::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)); + } + + fn max_degree(&self) -> usize { + 3 } } diff --git a/prover/src/tests/fext_page_tests.rs b/prover/src/tests/fext_page_tests.rs index 21af77cbe..b257068ac 100644 --- a/prover/src/tests/fext_page_tests.rs +++ b/prover/src/tests/fext_page_tests.rs @@ -8,7 +8,7 @@ use stark::constraints::builder::ConstraintSet; #[test] fn fext_page_constraint_and_bus_counts() { - assert_eq!(FextPageConstraints.meta().len(), 1); // IS_BIT(μ) + assert_eq!(FextPageConstraints.meta().len(), 2); // IS_BIT(μ) + domain ∈ {3,4,5} assert_eq!(bus_interactions().len(), 2); // init receiver + fini sender } @@ -38,8 +38,9 @@ fn fext_page_trace_layout_and_padding() { assert_eq!(*t.get(0, cols::MU), FE::one()); assert_eq!(*t.get(1, cols::DOMAIN), FE::from(5u64)); - // Padding rows have μ = 0. + // 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)); } } From cb34b38a2c6e65e24241174de4e611e0e5f1bd05 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Thu, 16 Jul 2026 14:47:40 -0300 Subject: [PATCH 08/17] Enforce FEXT_PAGE (domain, addr) uniqueness with a sorted-keys argument --- prover/src/tables/fext_page.rs | 181 ++++++++++++++++++++++++++-- prover/src/tables/trace_builder.rs | 39 ++++++ prover/src/tests/fext_page_tests.rs | 167 ++++++++++++++++++++++++- 3 files changed, 370 insertions(+), 17 deletions(-) diff --git a/prover/src/tables/fext_page.rs b/prover/src/tables/fext_page.rs index e3aa780f7..862cffa92 100644 --- a/prover/src/tables/fext_page.rs +++ b/prover/src/tables/fext_page.rs @@ -12,13 +12,26 @@ //! //! Field-storage is zero-initialized (scratch, single-proof scope), so `init` is //! the constant 0 rather than a committed column. -use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; +//! +//! ## 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, RowDomain}; use stark::lookup::{BusInteraction, BusValue, Multiplicity, Packing}; use stark::trace::TraceTable; use crate::constraints::templates::emit_is_bit; -use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField, VmTable, zeroed_fe_vec}; +use super::types::{ + BusId, FE, GoldilocksExtension, GoldilocksField, VmTable, alu_op, zeroed_fe_vec, +}; /// Column indices for the FEXT_PAGE table. pub mod cols { @@ -35,7 +48,25 @@ pub mod cols { /// Multiplicity bit. pub const MU: usize = 6; - pub const NUM_COLUMNS: usize = 7; + // --- 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. @@ -48,10 +79,15 @@ pub struct FextPageOperation { } /// Generates the FEXT_PAGE trace (one row per touched cell, padded to next power -/// of two, min 4). Padding rows are all-zero (`μ = 0`) and contribute nothing. +/// 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), @@ -66,14 +102,50 @@ pub fn generate_fext_page_trace( 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()); + + // Half-word range-check decomposition of the two 32-bit addr limbs. + let lo = op.addr & 0xFFFF_FFFF; + let hi = op.addr >> 32; + table.set_fe(row, cols::ADDR0_HW_LO, FE::from(lo & 0xFFFF)); + table.set_fe(row, cols::ADDR0_HW_HI, FE::from(lo >> 16)); + table.set_fe(row, cols::ADDR1_HW_LO, FE::from(hi & 0xFFFF)); + table.set_fe(row, cols::ADDR1_HW_HI, FE::from(hi >> 16)); } - // Padding rows carry a valid domain (3) so the ungated domain constraint - // holds on every row; μ = 0 keeps them out of the bus. + // Padding rows carry a valid domain (3) so the domain constraint holds; μ = 0 + // keeps them out of the bus. for row in ops.len()..num_rows { table.set_fe(row, cols::DOMAIN, FE::from(3u64)); } + // Cross-row helpers: copy the next row's addr, and set the same-domain flag + // and LT selector. The last row's transition is exempt, so it keeps zeros. + for row in 0..num_rows - 1 { + let next_addr_0 = *table.get(row + 1, cols::ADDR_0); + let next_addr_1 = *table.get(row + 1, cols::ADDR_1); + let cur_dom = *table.get(row, cols::DOMAIN); + let next_dom = *table.get(row + 1, cols::DOMAIN); + let next_active = *table.get(row + 1, cols::MU) == FE::one(); + let same = cur_dom == next_dom; + + table.set_fe(row, cols::NEXT_ADDR_0, next_addr_0); + table.set_fe(row, cols::NEXT_ADDR_1, next_addr_1); + table.set_fe( + row, + cols::SAME_DOM, + if same { FE::one() } else { FE::zero() }, + ); + table.set_fe( + row, + cols::SEL_SAME, + if same && next_active { + FE::one() + } else { + FE::zero() + }, + ); + } + trace } @@ -84,8 +156,19 @@ fn direct(col: usize) -> BusValue { } } +/// `IsHalfword[col]` — range-check that the column holds 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)], + ) +} + /// Bus interactions: emit the zero-init token and consume the final token for -/// each touched cell. +/// each touched cell, plus the uniqueness argument's `addr[i] < addr[i+1]` ALU +/// lookup and the addr-limb range checks. pub fn bus_interactions() -> Vec { vec![ // init: emit [domain, addr, ts=0, value=0] @@ -114,26 +197,98 @@ pub fn bus_interactions() -> Vec { direct(cols::FINAL_VAL), ], ), + // uniqueness: addr[i] < addr[i+1] on same-domain active transitions. + // Sound because the addr limbs are pinned to `[0, 2^32)` half-words. + BusInteraction::sender( + BusId::Alu, + Multiplicity::Column(cols::SEL_SAME), + vec![ + BusValue::Packed { + start_column: cols::ADDR_0, + packing: Packing::DWordWL, + }, + BusValue::Packed { + start_column: cols::NEXT_ADDR_0, + packing: Packing::DWordWL, + }, + BusValue::constant(alu_op::LT as u64), + BusValue::constant(1), + BusValue::constant(0), + ], + ), + is_halfword(cols::ADDR0_HW_LO), + is_halfword(cols::ADDR0_HW_HI), + is_halfword(cols::ADDR1_HW_LO), + is_halfword(cols::ADDR1_HW_HI), ] } -/// FEXT_PAGE constraints: idx 0 is `IS_BIT(μ)`, idx 1 pins the domain to -/// `{3, 4, 5}` (the field-storage coefficient domains). +/// 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). pub struct FextPageConstraints; impl ConstraintSet for FextPageConstraints { fn eval>(&self, b: &mut B) { emit_is_bit(b, 0, cols::MU, None); - // Domain ∈ {3, 4, 5}: `(D - 3)(D - 4)(D - 5) = 0`. The domain feeds the - // shared Memory bus, so leaving it a free witness would let a prover forge - // tokens in another domain's chain (e.g. domain 0 = RAM). Ungated (degree - // 3, within budget); padding rows carry domain 3 so it holds everywhere. + // Domain ∈ {3, 4, 5}: `(D - 3)(D - 4)(D - 5) = 0`. Ungated (degree 3, + // within budget); padding rows carry domain 3 so it holds everywhere. let d = b.main(0, cols::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, cols::SAME_DOM, None); + + // Addr-limb recompose: `ADDR_k = hw_lo + 2^16 * hw_hi`. With the + // `IsHalfword` range checks this pins each limb to `[0, 2^32)`. + let two16 = b.const_base(1 << 16); + let a0 = b.main(0, cols::ADDR_0); + let a0_lo = b.main(0, cols::ADDR0_HW_LO); + let a0_hi = b.main(0, cols::ADDR0_HW_HI); + b.emit_base(3, a0 - (a0_lo + two16.clone() * a0_hi)); + let a1 = b.main(0, cols::ADDR_1); + let a1_lo = b.main(0, cols::ADDR1_HW_LO); + let a1_hi = b.main(0, cols::ADDR1_HW_HI); + b.emit_base(4, a1 - (a1_lo + two16.clone() * a1_hi)); + + // --- transition constraints (read the next row) -------------------- + let tr = RowDomain::except_last(1); + let one = b.one(); + let two = b.const_base(2); + + let mu_cur = b.main(0, cols::MU); + let mu_next = b.main(1, cols::MU); + let same = b.main(0, cols::SAME_DOM); + let sel = b.main(0, cols::SEL_SAME); + let d_cur = b.main(0, cols::DOMAIN); + let d_next = b.main(1, cols::DOMAIN); + + // μ non-increasing: active rows are contiguous at the top. + b.emit_base_rows(5, tr, mu_next.clone() * (one.clone() - mu_cur)); + + // sel_same = μ_next · same_dom. + b.emit_base_rows(6, tr, sel.clone() - mu_next.clone() * same); + + // same_dom (active) ⇒ equal domain. + b.emit_base_rows(7, tr, sel.clone() * (d_next.clone() - d_cur.clone())); + + // ¬same_dom (active) ⇒ domain increases by 1 or 2. sel_diff = μ_next − sel. + 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)); + + // next_addr copies feed the cross-row LT. + let na0 = b.main(0, cols::NEXT_ADDR_0); + let addr0_next = b.main(1, cols::ADDR_0); + b.emit_base_rows(9, tr, na0 - addr0_next); + let na1 = b.main(0, cols::NEXT_ADDR_1); + let addr1_next = b.main(1, cols::ADDR_1); + b.emit_base_rows(10, tr, na1 - addr1_next); } fn max_degree(&self) -> usize { diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 1034a6c64..14e7f36a1 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -1807,6 +1807,43 @@ fn collect_bitwise_from_fext_store( 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: @@ -3384,6 +3421,7 @@ fn build_traces( 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)); // ===================================================================== // PHASE 4: All → Bitwise lookups @@ -3453,6 +3491,7 @@ fn build_traces( 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 diff --git a/prover/src/tests/fext_page_tests.rs b/prover/src/tests/fext_page_tests.rs index b257068ac..726689528 100644 --- a/prover/src/tests/fext_page_tests.rs +++ b/prover/src/tests/fext_page_tests.rs @@ -3,13 +3,58 @@ use crate::tables::fext_page::{ FextPageConstraints, FextPageOperation, bus_interactions, cols, generate_fext_page_trace, }; -use crate::tables::types::FE; -use stark::constraints::builder::ConstraintSet; +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)], 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() { - assert_eq!(FextPageConstraints.meta().len(), 2); // IS_BIT(μ) + domain ∈ {3,4,5} - assert_eq!(bus_interactions().len(), 2); // init receiver + fini sender + // IS_BIT(μ), domain ∈ {3,4,5}, IS_BIT(same_dom), 2 addr recompose, + // μ non-increasing, sel_same def, same-domain⇒equal, domain-increase, + // 2 next-addr copies = 11. + assert_eq!(FextPageConstraints.meta().len(), 11); + // init receiver + fini sender + addr LT + 4 IsHalfword = 7. + assert_eq!(bus_interactions().len(), 7); } #[test] @@ -44,3 +89,117 @@ fn fext_page_trace_layout_and_padding() { 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()); +} From d575215221e6a7c58144141638e5a0a6592965fd Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Thu, 16 Jul 2026 14:55:46 -0300 Subject: [PATCH 09/17] Add adversarial test for FEXT_STORE non-canonical output rejection --- prover/src/tests/fext_store_tests.rs | 53 ++++++++++++++++++++++++++-- 1 file changed, 51 insertions(+), 2 deletions(-) diff --git a/prover/src/tests/fext_store_tests.rs b/prover/src/tests/fext_store_tests.rs index 2902af824..cf670e81b 100644 --- a/prover/src/tests/fext_store_tests.rs +++ b/prover/src/tests/fext_store_tests.rs @@ -4,8 +4,34 @@ use crate::tables::fext_store::{ FextStoreConstraints, FextStoreOperation, bus_interactions, cols, generate_fext_store_trace, }; -use crate::tables::types::FE; -use stark::constraints::builder::ConstraintSet; +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 { @@ -72,3 +98,26 @@ fn fext_store_trace_shape() { assert_eq!(*trace.main_table.get(row, cols::MU), FE::zero()); } } + +#[test] +fn fext_store_constraints_hold_on_valid_trace() { + // Coefficients spanning both words exercise every recompose constraint. + let trace = generate_fext_store_trace(&[op([11, 22, 33]), op([44, 55, (7u64 << 32) | 6])]); + for row in 0..trace.num_rows() { + for (idx, v) in eval_row(&trace, row).into_iter().enumerate() { + assert_eq!(v, FE::zero(), "row {row}, constraint {idx} should be zero"); + } + } +} + +#[test] +fn fext_store_rejects_noncanonical_halfword_decomposition() { + // Tampering a coefficient's low half so it no longer recomposes to the word + // must break the word-recompose constraint (idx 1 for C0_LO). Without it a + // prover could hand a non-canonical (lo, hi) back to the destination register. + let mut trace = generate_fext_store_trace(&[op([11, 22, 33])]); + trace + .main_table + .set_fe(0, cols::hw(cols::C0_LO), FE::from(0xDEADu64)); + assert_ne!(eval_row(&trace, 0)[1], FE::zero()); +} From ee0b3f8189f7dd5ea2a263ef637b506f13013254 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Thu, 16 Jul 2026 14:57:09 -0300 Subject: [PATCH 10/17] Fix FEXT_FMA register-mapping comments and add literal Fp3 test vectors --- prover/src/tables/fext_fma.rs | 4 ++-- prover/src/tests/fext_fma_tests.rs | 13 +++++++++++++ 2 files changed, 15 insertions(+), 2 deletions(-) diff --git a/prover/src/tables/fext_fma.rs b/prover/src/tables/fext_fma.rs index f2ffd8a6e..c8649140f 100644 --- a/prover/src/tables/fext_fma.rs +++ b/prover/src/tables/fext_fma.rs @@ -12,7 +12,7 @@ //! //! ## 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 (out/a/b/c addrs). +//! - **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. @@ -38,7 +38,7 @@ pub mod cols { pub const TIMESTAMP_0: usize = 0; pub const TIMESTAMP_1: usize = 1; - // Operand addresses (each DWordWL). Registers: x10=out, x11=a, x12=b, x13=c. + // 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; diff --git a/prover/src/tests/fext_fma_tests.rs b/prover/src/tests/fext_fma_tests.rs index 1f00a5b77..65453818c 100644 --- a/prover/src/tests/fext_fma_tests.rs +++ b/prover/src/tests/fext_fma_tests.rs @@ -152,3 +152,16 @@ fn fext_fma_trace_shape() { assert_eq!(*trace.main_table.get(row, cols::MU), FE::zero()); } } + +#[test] +fn fext_fma_literal_fp3_vectors() { + // Hand-computed against the basis {1, w, w²} with w³ = 2, anchoring the Fp3 + // reduction independently of the field implementation (the constraint tests + // above reuse the same `fma` helper, so a literal is a distinct check). + assert_eq!(fma([0, 1, 0], [0, 1, 0], [0, 0, 0]), [0, 0, 1]); // w · w = w² + assert_eq!(fma([0, 0, 1], [0, 1, 0], [0, 0, 0]), [2, 0, 0]); // w² · w = w³ = 2 + assert_eq!(fma([0, 0, 1], [0, 0, 1], [0, 0, 0]), [0, 2, 0]); // w² · w² = w⁴ = 2w + assert_eq!(fma([1, 1, 0], [1, 1, 0], [0, 0, 0]), [1, 2, 1]); // (1 + w)² = 1 + 2w + w² + assert_eq!(fma([1, 1, 1], [0, 1, 0], [0, 0, 0]), [2, 1, 1]); // (1 + w + w²)·w = 2 + w + w² + assert_eq!(fma([0, 1, 0], [0, 1, 0], [5, 0, 0]), [5, 0, 1]); // w · w + 5 +} From fd363813b1ad837459fced22e92f56a6a47a4f34 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Fri, 17 Jul 2026 11:00:58 -0300 Subject: [PATCH 11/17] Sort LT trace rows into a canonical order to make the prover deterministic --- prover/src/tables/lt.rs | 5 ++- prover/src/tests/prove_elfs_tests.rs | 63 ++++++++++++++++++++++++++++ 2 files changed, 67 insertions(+), 1 deletion(-) 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/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs index 9a4a0312b..7f80db239 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -388,6 +388,69 @@ fn test_prove_elfs_fext() { ); } +/// 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 From 274cf638deef8a98867d2a3dce2f6d393db5ab20 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Fri, 17 Jul 2026 12:52:57 -0300 Subject: [PATCH 12/17] Force the portable Goldilocks modular-add on x86_64 to isolate a codegen-sensitive CI failure --- crypto/math/src/field/goldilocks.rs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/crypto/math/src/field/goldilocks.rs b/crypto/math/src/field/goldilocks.rs index 1d60ee5b2..688f7a5f3 100644 --- a/crypto/math/src/field/goldilocks.rs +++ b/crypto/math/src/field/goldilocks.rs @@ -221,9 +221,11 @@ fn reduce128(x: u128) -> u64 { /// /// # Safety /// Caller must ensure x + y < 2^64 + ORDER. +// EXPERIMENT (codegen-sensitive CI failure): x86 inline-asm variant disabled so the +// portable path is used on x86_64 too. Revert (restore `target_arch = "x86_64"`) if CI stays red. #[inline(always)] -#[cfg(target_arch = "x86_64")] -unsafe fn add_no_canonicalize_trashing_input(x: u64, y: u64) -> u64 { +#[cfg(any())] +unsafe fn add_no_canonicalize_trashing_input_asm(x: u64, y: u64) -> u64 { let res_wrapped: u64; let adjustment: u64; unsafe { @@ -241,7 +243,6 @@ unsafe fn add_no_canonicalize_trashing_input(x: u64, y: u64) -> u64 { } #[inline(always)] -#[cfg(not(target_arch = "x86_64"))] unsafe fn add_no_canonicalize_trashing_input(x: u64, y: u64) -> u64 { let (res_wrapped, carry) = x.overflowing_add(y); res_wrapped.wrapping_add(EPSILON * (carry as u64)) From 6be6aa67c10261810c257cf8c50d6d79be5f7ff2 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Fri, 17 Jul 2026 14:48:11 -0300 Subject: [PATCH 13/17] Set codegen-units=1 to probe a codegen-sensitive CI-only FEXT failure --- Cargo.toml | 5 +++++ crypto/math/src/field/goldilocks.rs | 7 +++---- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index 8f9bbe7d3..69b593dae 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -29,3 +29,8 @@ debug = true # For profiling with samply/perf, build with: # CARGO_PROFILE_RELEASE_DEBUG=1 cargo build --release + +# EXPERIMENT: codegen-units=1 to test a codegen-sensitive CI-only failure +# (FEXT_PAGE composition). Keeps opt-level=3 (runtime perf), only slows builds. +[profile.release] +codegen-units = 1 diff --git a/crypto/math/src/field/goldilocks.rs b/crypto/math/src/field/goldilocks.rs index 688f7a5f3..1d60ee5b2 100644 --- a/crypto/math/src/field/goldilocks.rs +++ b/crypto/math/src/field/goldilocks.rs @@ -221,11 +221,9 @@ fn reduce128(x: u128) -> u64 { /// /// # Safety /// Caller must ensure x + y < 2^64 + ORDER. -// EXPERIMENT (codegen-sensitive CI failure): x86 inline-asm variant disabled so the -// portable path is used on x86_64 too. Revert (restore `target_arch = "x86_64"`) if CI stays red. #[inline(always)] -#[cfg(any())] -unsafe fn add_no_canonicalize_trashing_input_asm(x: u64, y: u64) -> u64 { +#[cfg(target_arch = "x86_64")] +unsafe fn add_no_canonicalize_trashing_input(x: u64, y: u64) -> u64 { let res_wrapped: u64; let adjustment: u64; unsafe { @@ -243,6 +241,7 @@ unsafe fn add_no_canonicalize_trashing_input_asm(x: u64, y: u64) -> u64 { } #[inline(always)] +#[cfg(not(target_arch = "x86_64"))] unsafe fn add_no_canonicalize_trashing_input(x: u64, y: u64) -> u64 { let (res_wrapped, carry) = x.overflowing_add(y); res_wrapped.wrapping_add(EPSILON * (carry as u64)) From 22fad311ccd74d56f6df8c65aa6a8a0933c9d9ab Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Fri, 17 Jul 2026 15:21:50 -0300 Subject: [PATCH 14/17] Try opt-level=1 to probe the codegen-sensitive CI-only FEXT failure --- Cargo.toml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index 69b593dae..cff926f34 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -30,7 +30,9 @@ debug = true # For profiling with samply/perf, build with: # CARGO_PROFILE_RELEASE_DEBUG=1 cargo build --release -# EXPERIMENT: codegen-units=1 to test a codegen-sensitive CI-only failure -# (FEXT_PAGE composition). Keeps opt-level=3 (runtime perf), only slows builds. +# EXPERIMENT: probe a codegen-sensitive CI-only failure (FEXT_PAGE composition). +# codegen-units=1 didn't help; try opt-level=1 (a bigger codegen change). If this +# makes CI green, bisect per-crate opt-level to find the miscompiled crate. [profile.release] codegen-units = 1 +opt-level = 1 From b39ffa8cf9fac059643234fe32caa0746a592985 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Fri, 17 Jul 2026 15:29:23 -0300 Subject: [PATCH 15/17] Temp: prover-tests CI runs only test_prove_elfs_fext --- .github/workflows/pr_main.yaml | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/.github/workflows/pr_main.yaml b/.github/workflows/pr_main.yaml index cb10ec72a..2c1f9e8c2 100644 --- a/.github/workflows/pr_main.yaml +++ b/.github/workflows/pr_main.yaml @@ -292,13 +292,9 @@ jobs: retention-days: 1 test-prover: - name: Prover tests (${{ matrix.partition }}/4) + name: Prover tests (fext-only experiment) needs: build-prover-tests runs-on: ubuntu-latest - strategy: - fail-fast: false - matrix: - partition: [1, 2, 3, 4] steps: - name: Checkout sources uses: actions/checkout@v4 @@ -367,11 +363,11 @@ jobs: with: name: prover-tests - - name: Run prover tests (shard ${{ matrix.partition }}/4) + - name: Run prover tests (fext only) run: | cargo nextest run \ --archive-file prover-tests.tar.zst \ - --partition hash:${{ matrix.partition }}/4 \ + -E 'test(=tests::prove_elfs_tests::test_prove_elfs_fext)' \ --test-threads=1 test-prover-comprehensive: From 95883814d3566400cc387e89a0ab5ab0b3533323 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Fri, 17 Jul 2026 15:38:22 -0300 Subject: [PATCH 16/17] Try opt-level=0 to test if the FEXT miscompile is optimization-driven --- Cargo.toml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index cff926f34..2bc894367 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -31,8 +31,9 @@ debug = true # CARGO_PROFILE_RELEASE_DEBUG=1 cargo build --release # EXPERIMENT: probe a codegen-sensitive CI-only failure (FEXT_PAGE composition). -# codegen-units=1 didn't help; try opt-level=1 (a bigger codegen change). If this -# makes CI green, bisect per-crate opt-level to find the miscompiled crate. +# codegen-units=1 and opt-level=1 both still failed; try opt-level=0 (minimal +# optimization). If this passes, it's optimization-driven; if it still fails, the +# miscompile is not optimization-driven and needs escalation. [profile.release] codegen-units = 1 -opt-level = 1 +opt-level = 0 From 582fea33f7d704f6e0602168f9d00881b9ef7704 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Fri, 17 Jul 2026 15:51:45 -0300 Subject: [PATCH 17/17] Force-inline verify_rounds_2_to_4 to dodge a CI-only miscompile --- Cargo.toml | 8 -------- crypto/stark/src/verifier.rs | 1 + 2 files changed, 1 insertion(+), 8 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index 2bc894367..8f9bbe7d3 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -29,11 +29,3 @@ debug = true # For profiling with samply/perf, build with: # CARGO_PROFILE_RELEASE_DEBUG=1 cargo build --release - -# EXPERIMENT: probe a codegen-sensitive CI-only failure (FEXT_PAGE composition). -# codegen-units=1 and opt-level=1 both still failed; try opt-level=0 (minimal -# optimization). If this passes, it's optimization-driven; if it still fails, the -# miscompile is not optimization-driven and needs escalation. -[profile.release] -codegen-units = 1 -opt-level = 0 diff --git a/crypto/stark/src/verifier.rs b/crypto/stark/src/verifier.rs index f78bf6e34..e5d93b10a 100644 --- a/crypto/stark/src/verifier.rs +++ b/crypto/stark/src/verifier.rs @@ -1393,6 +1393,7 @@ pub trait IsStarkVerifier< } /// Verifies a single table after round 1 has been replayed. + #[inline(always)] fn verify_rounds_2_to_4( air: &dyn AIR, proof: StarkProofView<'_, Field, FieldExtension, PI>,