Field vm/3mi whir

bin/cli/src/main.rs

@@ -931,7 +931,7 @@ fn cmd_execute(
                     Some(Accelerator::Keccak) => keccak_calls += 1,
                     Some(Accelerator::Blake3) => blake3_calls += 1,
                     Some(Accelerator::Ecsm) => ecsm_calls += 1,
-                    None => {}
+                    Some(Accelerator::P1w16 | Accelerator::Fp3Mac) | None => {}
                 }
             }
             if cycle_budget.is_some_and(|budget| cycle_count >= budget) {

crypto/stark/src/constraints/builder.rs

@@ -463,6 +463,69 @@ impl<F: IsField, E: IsField> ConstraintBuilder<F, E> for MetaBuilder {
     }
 }
 
+// =============================================================================
+// NextRowReads — the columns a body reads at a later row
+// =============================================================================
+
+/// Records the trace columns a [`ConstraintSet`] body reads at frame offset
+/// `≥ 1`, which the verifier must open at `g·z`. Like [`MetaBuilder`] it does
+/// no field work, so it also runs where IR capture does not (the guest).
+#[derive(Default)]
+pub struct NextRowReads {
+    main: core::cell::RefCell<std::collections::BTreeSet<usize>>,
+    aux: core::cell::RefCell<std::collections::BTreeSet<usize>>,
+}
+
+impl NextRowReads {
+    pub fn new() -> Self {
+        Self::default()
+    }
+
+    /// Full-width `[main | aux]` indices, sorted.
+    pub fn into_columns(self, main_width: usize) -> Vec<usize> {
+        let main = self.main.into_inner();
+        let aux = self.aux.into_inner();
+        main.into_iter()
+            .chain(aux.into_iter().map(|c| main_width + c))
+            .collect()
+    }
+}
+
+impl<F: IsField, E: IsField> ConstraintBuilder<F, E> for NextRowReads {
+    type Expr = Nil;
+    type ExprE = Nil;
+
+    fn main(&self, offset: usize, col: usize) -> Nil {
+        if offset > 0 {
+            self.main.borrow_mut().insert(col);
+        }
+        Nil
+    }
+    fn aux(&self, offset: usize, col: usize) -> Nil {
+        if offset > 0 {
+            self.aux.borrow_mut().insert(col);
+        }
+        Nil
+    }
+    fn challenge(&self, _idx: usize) -> Nil {
+        Nil
+    }
+    fn alpha_pow(&self, _idx: usize) -> Nil {
+        Nil
+    }
+    fn table_offset(&self) -> Nil {
+        Nil
+    }
+    fn const_base(&self, _v: u64) -> Nil {
+        Nil
+    }
+    fn const_signed(&self, _v: i64) -> Nil {
+        Nil
+    }
+    fn emit_base_rows(&mut self, _constraint_idx: usize, _rows: RowDomain, _e: Nil) {}
+    fn emit_ext_rows(&mut self, _constraint_idx: usize, _rows: RowDomain, _e: Nil) {}
+}
+
 // =============================================================================
 // Shared AIR plumbing: run a ConstraintSet through the folders
 // =============================================================================

crypto/stark/src/lookup.rs

@@ -992,6 +992,8 @@ pub struct AirWithBuses<
     /// Maximum number of bus elements across all interactions.
     /// Used to compute the correct number of alpha powers.
     max_bus_elements: usize,
+    /// Full-width columns some transition constraint reads at the next row.
+    next_row_columns: Vec<usize>,
 }
 
 /// Cloning an `AirWithBuses` copies its derived artifacts — the MetaBuilder-run
@@ -1025,6 +1027,7 @@ impl<
             precomputed_columns: self.precomputed_columns.clone(),
             name: self.name.clone(),
             max_bus_elements: self.max_bus_elements,
+            next_row_columns: self.next_row_columns.clone(),
         }
     }
 }
@@ -1088,6 +1091,22 @@ impl<
             .max()
             .unwrap_or(0);
 
+        // The verifier opens only these columns at `g·z`: the wrapped set's
+        // next-row reads plus the LogUp accumulator. Multi-row steps keep the
+        // accumulator alone (see `the_prover_cannot_prove_a_step_size_two_air`).
+        let mut next_row_columns = if step_size == 1 {
+            let mut reads = crate::constraints::builder::NextRowReads::new();
+            constraint_set.eval(&mut reads);
+            reads.into_columns(trace_layout.0)
+        } else {
+            Vec::new()
+        };
+        if num_interactions > 0 {
+            next_row_columns.push(trace_layout.0 + logup.acc_column_idx);
+        }
+        next_row_columns.sort_unstable();
+        next_row_columns.dedup();
+
         // Create context
         let context = AirContext {
             proof_options: proof_options.clone(),
@@ -1113,6 +1132,7 @@ impl<
             precomputed_columns: None,
             name: None,
             max_bus_elements,
+            next_row_columns,
         }
     }
 
@@ -1275,16 +1295,11 @@ 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]
-        }
+        // Derived in `new` from the wrapped constraint set, plus the LogUp
+        // accumulator: after forward accumulation it is the only LogUp column
+        // read at the next row (committed terms and absorbed operands read the
+        // current row).
+        self.next_row_columns.clone()
     }
 
     fn has_trace_interaction(&self) -> bool {

crypto/stark/src/tests/bus_tests/soundness_tests.rs

@@ -1203,6 +1203,77 @@ fn test_trace_ood_next_row_window_matches_captured_ir() {
     assert_ood_window_matches_ir(&busless, true, "busless");
 }
 
+/// `col0' = col0 + 1` on every row but the last.
+#[derive(Clone)]
+struct Increment;
+
+impl crate::constraints::builder::ConstraintSet<F, E> for Increment {
+    fn eval<B: crate::constraints::builder::ConstraintBuilder<F, E>>(&self, b: &mut B) {
+        let e = b.main(1, 0) - b.main(0, 0) - b.one();
+        b.emit_base_rows(0, crate::constraints::builder::RowDomain::except_last(1), e);
+    }
+}
+
+/// A wrapped constraint set that reads a main column at the next row gets that
+/// column opened at `g·z`, next to the accumulator, and its proofs verify.
+#[test_log::test]
+fn test_next_row_main_reads_are_opened_and_verify() {
+    let opts = ProofOptions::default_test_options();
+    for with_bus in [false, true] {
+        let interactions = if with_bus {
+            vec![
+                BusInteraction::sender(
+                    TEST_BUS,
+                    Multiplicity::Column(1),
+                    Packing::Direct.columns(&[0]),
+                ),
+                BusInteraction::receiver(
+                    TEST_BUS,
+                    Multiplicity::Column(1),
+                    Packing::Direct.columns(&[0]),
+                ),
+            ]
+        } else {
+            vec![]
+        };
+        let air = AirWithBuses::<F, E, NullBoundaryConstraintBuilder, (), _>::new(
+            2,
+            AuxiliaryTraceBuildData { interactions },
+            &opts,
+            1,
+            Increment,
+        );
+        let (main, aux) = air.trace_layout();
+        let expected = if with_bus {
+            vec![0, main + aux - 1]
+        } else {
+            vec![0]
+        };
+        assert_eq!(air.trace_ood_next_row_columns(), expected);
+        assert_ood_window_matches_ir(&air, true, "increment");
+
+        let n = 16u64;
+        let mut trace = TraceTable::from_columns_main(
+            vec![(0..n).map(FE::from).collect(), vec![FE::one(); n as usize]],
+            1,
+        );
+        let proof = multi_prove_ram(
+            vec![(&air, &mut trace, &())],
+            &mut DefaultTranscript::<E>::new(&[]),
+        )
+        .expect("proving");
+        assert!(
+            Verifier::multi_verify(
+                &[&air],
+                &proof,
+                &mut DefaultTranscript::<E>::new(&[]),
+                &FieldElement::zero()
+            ),
+            "with_bus={with_bus}"
+        );
+    }
+}
+
 /// The g·z pruning actually shrinks the proof: a LogUp table opens every column
 /// at z (the current-row block) but only the accumulator at the next row.
 #[test_log::test]

executor/Cargo.toml

@@ -12,6 +12,10 @@ ecsm = { path = "../crypto/ecsm" }
 # `Hint` ecall — same k256 arithmetic the guest verifies against. Production code:
 # `compute_hint` runs in every proving execution of a hint-using guest.
 k256 = { version = "0.13", default-features = false, features = ["arithmetic", "expose-field"] }
+# Host-side width-16 Poseidon1 for the `P1w16Permute` ecall: the same
+# permutation the prover's chip constrains.
+crypto = { path = "../crypto/crypto" }
+math = { path = "../crypto/math" }
 
 [dev-dependencies]
 # Test-only: the guest-side syscall crate re-declares the `hint` selectors as `usize`

executor/programs/rust/fp3mac_precompile/.cargo/config.toml

@@ -0,0 +1,5 @@
+[target.riscv64im-lambda-vm-elf]
+rustflags = [
+  "--cfg", "getrandom_backend=\"custom\"",
+  "-C", "passes=lower-atomic"
+]