Feat/fext accelerator fix

bin/cli/src/main.rs

@@ -412,7 +412,7 @@ fn cmd_execute(
     // below (the flamegraph path drives execution inside the executor and does
     // not expose per-log data). `None` means "not counted", so the accel lines
     // are omitted rather than printed as misleading zeros.
-    let mut accel_counts: Option<(u64, u64)> = None;
+    let mut accel_counts: Option<(u64, u64, u64, u64, u64)> = None;
 
     let cycle_count = if let Some(ref output_path) = flamegraph.path {
         // Shared execute+flamegraph path (executor::flamegraph) instead of
@@ -480,6 +480,9 @@ fn cmd_execute(
         let mut cycle_count: u64 = 0;
         let mut keccak_calls: u64 = 0;
         let mut ecsm_calls: u64 = 0;
+        let mut fext_load_calls: u64 = 0;
+        let mut fext_fma_calls: u64 = 0;
+        let mut fext_store_calls: u64 = 0;
         // Reused per chunk: `(current_pc, a7)` for logs whose a7 matches an
         // accelerator syscall number. This is a cheap superset — a non-ECALL
         // instruction can hold the same value in src1 — that `accelerator_of`
@@ -512,6 +515,9 @@ fn cmd_execute(
                 match accelerator_of(executor.instructions.get(pc), a7) {
                     Some(Accelerator::Keccak) => keccak_calls += 1,
                     Some(Accelerator::Ecsm) => ecsm_calls += 1,
+                    Some(Accelerator::FextLoad) => fext_load_calls += 1,
+                    Some(Accelerator::FextFma) => fext_fma_calls += 1,
+                    Some(Accelerator::FextStore) => fext_store_calls += 1,
                     None => {}
                 }
             }
@@ -526,16 +532,27 @@ fn cmd_execute(
         }
 
         if cycles {
-            accel_counts = Some((keccak_calls, ecsm_calls));
+            accel_counts = Some((
+                keccak_calls,
+                ecsm_calls,
+                fext_load_calls,
+                fext_fma_calls,
+                fext_store_calls,
+            ));
         }
         cycle_count
     };
 
     if cycles {
         println!("Cycles: {}", cycle_count);
-        if let Some((keccak_calls, ecsm_calls)) = accel_counts {
+        if let Some((keccak_calls, ecsm_calls, fext_load_calls, fext_fma_calls, fext_store_calls)) =
+            accel_counts
+        {
             println!("Keccak calls: {}", keccak_calls);
             println!("Ecsm calls: {}", ecsm_calls);
+            println!("Fext load calls: {}", fext_load_calls);
+            println!("Fext fma calls: {}", fext_fma_calls);
+            println!("Fext store calls: {}", fext_store_calls);
         }
     }
 

crypto/stark/src/constraints/builder.rs

@@ -277,6 +277,17 @@ pub trait ConstraintSet<F: IsField, E: IsField>: Send + Sync {
         2
     }
 
+    /// Main-trace columns this set reads on the NEXT row (via `main(1, col)`).
+    /// The verifier opens OOD next-row evaluations only for these columns (unioned
+    /// with the LogUp accumulator); an undeclared next-row read is pruned and
+    /// reconstructed as zero, silently corrupting this table's transition eval.
+    /// Statically declared so the verify/recursion path never materializes the IR;
+    /// a test asserts the IR's actual next-row reads are a subset of this. Default
+    /// empty (most tables read only the current row).
+    fn next_row_columns(&self) -> Vec<usize> {
+        Vec::new()
+    }
+
     /// Idx-ordered metadata, derived by running [`Self::eval`] through a
     /// [`MetaBuilder`] (which records the `{kind, end_exemptions}` at each
     /// `emit_*`). Never overridden — the body is the source.

crypto/stark/src/lookup.rs

@@ -1004,16 +1004,19 @@ where
     }
 
     fn trace_ood_next_row_columns(&self) -> Vec<usize> {
-        // The only transition constraint that reads the next row is the circular
-        // LogUp accumulator, and after forward accumulation it reads only the
-        // accumulated column there (all committed terms and absorbed operands
-        // read the current row). Its full-width index is the main width plus the
-        // accumulated column's aux index. No interactions => no next-row reads.
-        if self.auxiliary_trace_build_data.interactions.is_empty() {
-            Vec::new()
-        } else {
-            vec![self.trace_layout.0 + self.logup.acc_column_idx]
+        // Columns read on the next row: the table's own constraint-set reads
+        // (`main(1, ·)`, statically declared) plus, when the table has LogUp
+        // interactions, the circular accumulator's aux column (main width + its
+        // aux index). The verifier opens OOD next-row evaluations only for these;
+        // a next-row read that is not declared here is pruned and reconstructed as
+        // zero, silently corrupting this table's transition evaluation.
+        let mut cols = self.constraint_set.next_row_columns();
+        if !self.auxiliary_trace_build_data.interactions.is_empty() {
+            cols.push(self.trace_layout.0 + self.logup.acc_column_idx);
         }
+        cols.sort_unstable();
+        cols.dedup();
+        cols
     }
 
     fn has_trace_interaction(&self) -> bool {

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

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

executor/programs/asm/test_fext.s

@@ -0,0 +1,49 @@
+	.attribute	5, "rv64i2p1_m2p0_zmmul1p0"
+	.globl	main
+main:
+	# FEXT_LOAD a = (1, 2, 3) into field-storage address 1.
+	# a0 = field-storage address, a1/a2/a3 = coefficients, a7 = -20.
+	li	a0, 1
+	li	a1, 1
+	li	a2, 2
+	li	a3, 3
+	li	a7, -20
+	ecall
+
+	# FEXT_LOAD b = (4, 5, 6) into field-storage address 2.
+	li	a0, 2
+	li	a1, 4
+	li	a2, 5
+	li	a3, 6
+	li	a7, -20
+	ecall
+
+	# FEXT_LOAD c = (7, 8, 9) into field-storage address 3.
+	li	a0, 3
+	li	a1, 7
+	li	a2, 8
+	li	a3, 9
+	li	a7, -20
+	ecall
+
+	# FEXT_FMA: out(addr 4) = a(addr 1) * b(addr 2) + c(addr 3).
+	# a0/a1/a2 = a/b/c addresses, a3 = output address, a7 = -21.
+	li	a0, 1
+	li	a1, 2
+	li	a2, 3
+	li	a3, 4
+	li	a7, -21
+	ecall
+
+	# FEXT_STORE: read result (addr 4) back into registers a1/a2/a3.
+	# a0 = field-storage source address, a7 = -22.
+	li	a0, 4
+	li	a7, -22
+	ecall
+
+	# Halt.
+	li	a0, 0
+	li	a7, 93
+	ecall
+.Lfunc_end1:
+	.size	main, .Lfunc_end1-main

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