diff --git a/Cargo.lock b/Cargo.lock index 2a33cafb4..c0e45d8a0 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -604,9 +604,11 @@ dependencies = [ name = "executor" version = "0.1.0" dependencies = [ + "crypto", "ecsm", "k256", "lambda-vm-syscalls", + "math", "rustc-demangle", "serde", "serde_json", diff --git a/bin/cli/src/main.rs b/bin/cli/src/main.rs index d65abf60c..6ccb70dd8 100644 --- a/bin/cli/src/main.rs +++ b/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) { diff --git a/crypto/stark/src/constraints/builder.rs b/crypto/stark/src/constraints/builder.rs index 983c8ef3d..ff53e25ca 100644 --- a/crypto/stark/src/constraints/builder.rs +++ b/crypto/stark/src/constraints/builder.rs @@ -463,6 +463,69 @@ impl ConstraintBuilder 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>, + aux: core::cell::RefCell>, +} + +impl NextRowReads { + pub fn new() -> Self { + Self::default() + } + + /// Full-width `[main | aux]` indices, sorted. + pub fn into_columns(self, main_width: usize) -> Vec { + 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 ConstraintBuilder 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 // ============================================================================= diff --git a/crypto/stark/src/lookup.rs b/crypto/stark/src/lookup.rs index 664c0510f..7390002a8 100644 --- a/crypto/stark/src/lookup.rs +++ b/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, } /// 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 { - // 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 { diff --git a/crypto/stark/src/tests/bus_tests/soundness_tests.rs b/crypto/stark/src/tests/bus_tests/soundness_tests.rs index 157802cdf..9b2165004 100644 --- a/crypto/stark/src/tests/bus_tests/soundness_tests.rs +++ b/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 for Increment { + fn eval>(&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::::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::::new(&[]), + ) + .expect("proving"); + assert!( + Verifier::multi_verify( + &[&air], + &proof, + &mut DefaultTranscript::::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] diff --git a/executor/Cargo.toml b/executor/Cargo.toml index 91ae64ae9..204b79f42 100644 --- a/executor/Cargo.toml +++ b/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` diff --git a/executor/programs/rust/fp3mac_precompile/.cargo/config.toml b/executor/programs/rust/fp3mac_precompile/.cargo/config.toml new file mode 100644 index 000000000..ca99a3f45 --- /dev/null +++ b/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" +] diff --git a/executor/programs/rust/fp3mac_precompile/Cargo.lock b/executor/programs/rust/fp3mac_precompile/Cargo.lock new file mode 100644 index 000000000..63e9295cb --- /dev/null +++ b/executor/programs/rust/fp3mac_precompile/Cargo.lock @@ -0,0 +1,251 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 4 + +[[package]] +name = "cfg-if" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801" + +[[package]] +name = "critical-section" +version = "1.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "790eea4361631c5e7d22598ecd5723ff611904e3344ce8720784c93e3d83d40b" + +[[package]] +name = "embedded-hal" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "361a90feb7004eca4019fb28352a9465666b24f840f5c3cddf0ff13920590b89" + +[[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 = "fp3mac_precompile" +version = "0.1.0" +dependencies = [ + "lambda-vm-syscalls", +] + +[[package]] +name = "lambda-vm-syscalls" +version = "0.1.0" +dependencies = [ + "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 = "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", +] + +[[package]] +name = "riscv-pac" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8188909339ccc0c68cfb5a04648313f09621e8b87dc03095454f1a11f6c5d436" + +[[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", +] + +[[package]] +name = "unicode-ident" +version = "1.0.24" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75" + +[[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", +] diff --git a/executor/programs/rust/fp3mac_precompile/Cargo.toml b/executor/programs/rust/fp3mac_precompile/Cargo.toml new file mode 100644 index 000000000..658bc02ab --- /dev/null +++ b/executor/programs/rust/fp3mac_precompile/Cargo.toml @@ -0,0 +1,9 @@ +[workspace] + +[package] +name = "fp3mac_precompile" +version = "0.1.0" +edition = "2024" + +[dependencies] +lambda-vm-syscalls = { path = "../../../../syscalls" } diff --git a/executor/programs/rust/fp3mac_precompile/src/main.rs b/executor/programs/rust/fp3mac_precompile/src/main.rs new file mode 100644 index 000000000..f64c003c4 --- /dev/null +++ b/executor/programs/rust/fp3mac_precompile/src/main.rs @@ -0,0 +1,34 @@ +use lambda_vm_syscalls::syscalls; + +/// Cells the Horner runs over. +const CELLS: usize = 48; + +// Exercises the cubic-extension multiply-add ecall: a Horner evaluation +// `acc ← acc·al + x` over pseudo-random canonical cells (edge values first), +// committing the three words of `acc`. +pub fn main() { + const P: u64 = 0xFFFF_FFFF_0000_0001; + let mut seed = 0x9E37_79B9_7F4A_7C15u64; + let mut next = || { + seed = seed.wrapping_add(0x9E37_79B9_7F4A_7C15); + let mut z = seed; + z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9); + z = (z ^ (z >> 27)).wrapping_mul(0x94D0_49BB_1331_11EB); + (z ^ (z >> 31)) % P + }; + let mut state: [u64; 6] = [0, 0, 0, next(), next(), next()]; + let edges: [[u64; 3]; 3] = [[0, 1, P - 1], [P - 1, P - 1, P - 1], [0xFFFF_FFFF, 0, 1]]; + for k in 0..CELLS { + let x = if k < edges.len() { + edges[k] + } else { + [next(), next(), next()] + }; + syscalls::fp3mac(&mut state, &x); + } + let mut output = Vec::with_capacity(3 * 8); + for w in &state[..3] { + output.extend_from_slice(&w.to_le_bytes()); + } + syscalls::commit(&output); +} diff --git a/executor/programs/rust/p1w16_precompile/.cargo/config.toml b/executor/programs/rust/p1w16_precompile/.cargo/config.toml new file mode 100644 index 000000000..ca99a3f45 --- /dev/null +++ b/executor/programs/rust/p1w16_precompile/.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/p1w16_precompile/Cargo.lock b/executor/programs/rust/p1w16_precompile/Cargo.lock new file mode 100644 index 000000000..9eb4587f5 --- /dev/null +++ b/executor/programs/rust/p1w16_precompile/Cargo.lock @@ -0,0 +1,251 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 4 + +[[package]] +name = "cfg-if" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801" + +[[package]] +name = "critical-section" +version = "1.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "790eea4361631c5e7d22598ecd5723ff611904e3344ce8720784c93e3d83d40b" + +[[package]] +name = "embedded-hal" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "361a90feb7004eca4019fb28352a9465666b24f840f5c3cddf0ff13920590b89" + +[[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 = "p1w16_precompile" +version = "0.1.0" +dependencies = [ + "lambda-vm-syscalls", +] + +[[package]] +name = "lambda-vm-syscalls" +version = "0.1.0" +dependencies = [ + "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 = "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", +] + +[[package]] +name = "riscv-pac" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8188909339ccc0c68cfb5a04648313f09621e8b87dc03095454f1a11f6c5d436" + +[[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", +] + +[[package]] +name = "unicode-ident" +version = "1.0.24" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75" + +[[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", +] diff --git a/executor/programs/rust/p1w16_precompile/Cargo.toml b/executor/programs/rust/p1w16_precompile/Cargo.toml new file mode 100644 index 000000000..caa44245c --- /dev/null +++ b/executor/programs/rust/p1w16_precompile/Cargo.toml @@ -0,0 +1,9 @@ +[workspace] + +[package] +name = "p1w16_precompile" +version = "0.1.0" +edition = "2024" + +[dependencies] +lambda-vm-syscalls = { path = "../../../../syscalls" } diff --git a/executor/programs/rust/p1w16_precompile/src/main.rs b/executor/programs/rust/p1w16_precompile/src/main.rs new file mode 100644 index 000000000..782b02459 --- /dev/null +++ b/executor/programs/rust/p1w16_precompile/src/main.rs @@ -0,0 +1,21 @@ +use lambda_vm_syscalls::syscalls; + +// Exercises the width-16 Poseidon1 ecall: a chain of permutations from a +// state with edge values (0, 1, p − 1), committing every lane of the last. +pub fn main() { + const P: u64 = 0xFFFF_FFFF_0000_0001; + let mut state: [u64; 16] = core::array::from_fn(|i| match i % 4 { + 0 => 0, + 1 => 1, + 2 => P - 1, + _ => (i as u64) * 0x0123_4567_89AB_CDEF % P, + }); + for _ in 0..5 { + syscalls::p1w16_permute(&mut state); + } + let mut output = Vec::with_capacity(16 * 8); + for lane in state { + output.extend_from_slice(&lane.to_le_bytes()); + } + syscalls::commit(&output); +} diff --git a/executor/src/tests/fp3mac_tests.rs b/executor/src/tests/fp3mac_tests.rs new file mode 100644 index 000000000..751b863c0 --- /dev/null +++ b/executor/src/tests/fp3mac_tests.rs @@ -0,0 +1,110 @@ +//! Tests for the cubic-extension multiply-add syscall. + +use crate::vm::instruction::decoding::Instruction; +use crate::vm::instruction::execution::{ExecutionError, FP3MAC_SYSCALL_NUMBER, fp3mac}; +use crate::vm::memory::Memory; +use crate::vm::registers::Registers; + +const STATE_ADDR: u64 = 0x1000; +const CELL_ADDR: u64 = 0x2000; +const P: u64 = math::field::goldilocks::GOLDILOCKS_PRIME; + +fn run(memory: &mut Memory, state: u64, cell: u64) -> Result<(), ExecutionError> { + let mut pc = 0; + let mut registers = Registers::default(); + registers.write(17, FP3MAC_SYSCALL_NUMBER).unwrap(); + registers.write(10, state).unwrap(); + registers.write(11, cell).unwrap(); + Instruction::EcallEbreak + .run(&mut pc, &mut registers, memory) + .map(|_| ()) +} + +fn store(memory: &mut Memory, addr: u64, words: &[u64]) { + for (i, &w) in words.iter().enumerate() { + memory.store_doubleword(addr + 8 * i as u64, w).unwrap(); + } +} + +fn load(memory: &Memory, addr: u64) -> [u64; N] { + core::array::from_fn(|i| memory.load_doubleword(addr + 8 * i as u64).unwrap()) +} + +#[test] +fn test_fp3mac_syscall_multiplies_and_adds_in_place() { + let state: [u64; 6] = core::array::from_fn(|i| (i as u64 + 3) * 0x0123_4567_89AB_CDEF % P); + let x = [P - 1, 7, 0x8000_0000_0000_0001 % P]; + let mut memory = Memory::default(); + store(&mut memory, STATE_ADDR, &state); + store(&mut memory, CELL_ADDR, &x); + run(&mut memory, STATE_ADDR, CELL_ADDR).unwrap(); + let out: [u64; 6] = load(&memory, STATE_ADDR); + assert_eq!(out[..3], fp3mac(state, x)); + assert_eq!(out[3..], state[3..], "al is left alone"); + assert_eq!(load::<3>(&memory, CELL_ADDR), x, "the cell is left alone"); +} + +/// `t·t² = t³ = 2`: the extension is `Fp[t]/(t³ − 2)`. +#[test] +fn test_fp3mac_reduces_by_t_cubed_minus_two() { + assert_eq!(fp3mac([0, 1, 0, 0, 0, 1], [0, 0, 0]), [2, 0, 0]); + assert_eq!(fp3mac([0, 0, 1, 0, 0, 1], [5, 0, 0]), [5, 2, 0]); +} + +#[test] +fn test_fp3mac_syscall_rejects_non_canonical_input() { + for k in 0..9 { + let mut words = [1u64; 9]; + words[k] = P; + let mut memory = Memory::default(); + store(&mut memory, STATE_ADDR, &words[..6]); + store(&mut memory, CELL_ADDR, &words[6..]); + let err = run(&mut memory, STATE_ADDR, CELL_ADDR).unwrap_err(); + assert!( + matches!(err, ExecutionError::Fp3MacNonCanonicalInput(v) if v == P), + "word {k}" + ); + } +} + +#[test] +fn test_fp3mac_syscall_rejects_unaligned_addresses() { + let mut memory = Memory::default(); + assert!(matches!( + run(&mut memory, 0x1001, CELL_ADDR).unwrap_err(), + ExecutionError::UnalignedFp3MacAddress(0x1001) + )); + assert!(matches!( + run(&mut memory, STATE_ADDR, 0x2004).unwrap_err(), + ExecutionError::UnalignedFp3MacAddress(0x2004) + )); +} + +#[test] +fn test_fp3mac_syscall_rejects_overflowing_ranges() { + let mut memory = Memory::default(); + let addr = u64::MAX - 39; + assert!(matches!( + run(&mut memory, addr, CELL_ADDR).unwrap_err(), + ExecutionError::Fp3MacAddressOverflow(a) if a == addr + )); + let cell = u64::MAX - 15; + assert!(matches!( + run(&mut memory, STATE_ADDR, cell).unwrap_err(), + ExecutionError::Fp3MacAddressOverflow(a) if a == cell + )); +} + +#[test] +fn test_fp3mac_syscall_rejects_overlapping_operands() { + let mut memory = Memory::default(); + assert!(matches!( + run(&mut memory, STATE_ADDR, STATE_ADDR + 40).unwrap_err(), + ExecutionError::Fp3MacOverlap(..) + )); + assert!(matches!( + run(&mut memory, STATE_ADDR + 16, STATE_ADDR).unwrap_err(), + ExecutionError::Fp3MacOverlap(..) + )); + run(&mut memory, STATE_ADDR, STATE_ADDR + 48).unwrap(); +} diff --git a/executor/src/tests/mod.rs b/executor/src/tests/mod.rs index 662a116d5..3ac97e4f7 100644 --- a/executor/src/tests/mod.rs +++ b/executor/src/tests/mod.rs @@ -1,6 +1,8 @@ pub mod blake3_tests; pub mod ecsm_tests; pub mod flamegraph_tests; +pub mod fp3mac_tests; pub mod hint_tests; pub mod keccak_tests; pub mod memory_tests; +pub mod p1w16_tests; diff --git a/executor/src/tests/p1w16_tests.rs b/executor/src/tests/p1w16_tests.rs new file mode 100644 index 000000000..6f13f603a --- /dev/null +++ b/executor/src/tests/p1w16_tests.rs @@ -0,0 +1,81 @@ +//! Tests for the width-16 Poseidon1 permutation syscall. + +use crate::vm::instruction::decoding::Instruction; +use crate::vm::instruction::execution::{ExecutionError, P1W16_SYSCALL_NUMBER}; +use crate::vm::memory::Memory; +use crate::vm::registers::Registers; + +const STATE_ADDR: u64 = 0x1000; +const P: u64 = math::field::goldilocks::GOLDILOCKS_PRIME; + +fn run_p1w16(memory: &mut Memory, addr: u64) -> Result<(), ExecutionError> { + let mut pc = 0; + let mut registers = Registers::default(); + registers.write(17, P1W16_SYSCALL_NUMBER).unwrap(); + registers.write(10, addr).unwrap(); + Instruction::EcallEbreak + .run(&mut pc, &mut registers, memory) + .map(|_| ()) +} + +fn store_state(memory: &mut Memory, state: &[u64; 16]) { + for (i, &w) in state.iter().enumerate() { + memory + .store_doubleword(STATE_ADDR + 8 * i as u64, w) + .unwrap(); + } +} + +fn load_state(memory: &Memory) -> [u64; 16] { + core::array::from_fn(|i| memory.load_doubleword(STATE_ADDR + 8 * i as u64).unwrap()) +} + +#[test] +fn test_p1w16_syscall_permutes_in_place() { + let input: [u64; 16] = core::array::from_fn(|i| (i as u64 + 1) * 0x0123_4567_89AB_CDEF % P); + let mut memory = Memory::default(); + store_state(&mut memory, &input); + run_p1w16(&mut memory, STATE_ADDR).unwrap(); + + use crypto::hash::poseidon1_w16::{Fp, permute}; + let expected = permute(input.map(Fp::from)).map(|v| v.canonical()); + assert_eq!(load_state(&memory), expected); + assert_ne!(expected, input); +} + +#[test] +fn test_p1w16_syscall_accepts_the_largest_canonical_word() { + let mut input = [0u64; 16]; + input[15] = P - 1; + let mut memory = Memory::default(); + store_state(&mut memory, &input); + run_p1w16(&mut memory, STATE_ADDR).unwrap(); +} + +#[test] +fn test_p1w16_syscall_rejects_non_canonical_input() { + let mut input = [0u64; 16]; + input[15] = P; + let mut memory = Memory::default(); + store_state(&mut memory, &input); + let err = run_p1w16(&mut memory, STATE_ADDR).unwrap_err(); + assert!(matches!(err, ExecutionError::P1w16NonCanonicalInput(v) if v == P)); +} + +#[test] +fn test_p1w16_syscall_rejects_unaligned_state_addr() { + let mut memory = Memory::default(); + let err = run_p1w16(&mut memory, 0x1001).unwrap_err(); + assert!(matches!( + err, + ExecutionError::UnalignedP1w16StateAddress(0x1001) + )); +} + +#[test] +fn test_p1w16_syscall_rejects_overflowing_state_range() { + let mut memory = Memory::default(); + let addr = u64::MAX - 87; + let err = run_p1w16(&mut memory, addr).unwrap_err(); + assert!(matches!(err, ExecutionError::P1w16StateAddressOverflow(a) if a == addr)); +} diff --git a/executor/src/vm/instruction/execution.rs b/executor/src/vm/instruction/execution.rs index aa0c5e9bf..b7147c664 100644 --- a/executor/src/vm/instruction/execution.rs +++ b/executor/src/vm/instruction/execution.rs @@ -17,6 +17,10 @@ pub enum SyscallNumbers { // Placeholder discriminant. The actual syscall value is // BLAKE3_ABSORB_SYSCALL_NUMBER. Blake3Absorb = 4, + // Placeholder discriminant. The actual syscall value is P1W16_SYSCALL_NUMBER. + P1w16Permute = 5, + // Placeholder discriminant. The actual syscall value is FP3MAC_SYSCALL_NUMBER. + Fp3Mac = 7, Commit = 64, Halt = 93, // Placeholder discriminant. The actual syscall value is ECSM_SYSCALL_NUMBER. @@ -32,6 +36,27 @@ pub enum SyscallNumbers { pub const KECCAK_SYSCALL_NUMBER: u64 = u64::MAX - 1; const KECCAK_STATE_BYTES: u64 = 25 * 8; +/// Syscall number for the width-16 Poseidon1 permutation accelerator +/// (u64::MAX - 5 = 0xFFFF_FFFF_FFFF_FFFA). +/// +/// ABI: `x10` points to an 8-byte-aligned `[u64; 16]` Goldilocks state, permuted +/// in place. Every input word must be canonical (`< p`): the chip range-checks +/// the input and output encodings, so a non-canonical word would make the trace +/// unprovable and is rejected here up front. +pub const P1W16_SYSCALL_NUMBER: u64 = u64::MAX - 5; +const P1W16_STATE_BYTES: u64 = 16 * 8; + +/// Syscall number for the cubic-extension multiply-add accelerator +/// (u64::MAX - 7 = 0xFFFF_FFFF_FFFF_FFF8). +/// +/// ABI: `x10` points to an 8-byte-aligned `[acc0, acc1, acc2, al0, al1, al2]` +/// and `x11` to an 8-byte-aligned `[x0, x1, x2]`, Goldilocks words. In +/// `Fp3 = Fp[t]/(t³ − 2)` it computes `acc ← acc·al + x` and writes the three +/// `acc` words back in place. Every word read must be canonical (`< p`). +pub const FP3MAC_SYSCALL_NUMBER: u64 = u64::MAX - 7; +const FP3MAC_STATE_BYTES: u64 = 6 * 8; +const FP3MAC_CELL_BYTES: u64 = 3 * 8; + /// Syscall number for the BLAKE3 6-round compression accelerator /// (u64::MAX - 2 = 0xFFFF_FFFF_FFFF_FFFD). /// @@ -190,6 +215,31 @@ const _: () = { /// largest per-access offset is added: the 32-byte operands reach offset +31 (last byte). const LOW_LIMB: u64 = 1 << 32; +/// The Goldilocks prime, the bound every Poseidon1 state word must sit below. +const GOLDILOCKS_P: u64 = math::field::goldilocks::GOLDILOCKS_PRIME; + +/// Width-16 Poseidon1 over canonical Goldilocks words, the host side of the +/// accelerator: the permutation the LFM's `Hash16` rows use. +pub fn p1w16_permute(state: [u64; 16]) -> [u64; 16] { + use crypto::hash::poseidon1_w16::{Fp, permute}; + permute(state.map(Fp::from)).map(|v| v.canonical()) +} + +/// `acc·al + x` in `Fp[t]/(t³ − 2)` over canonical Goldilocks words, the host +/// side of the FP3MAC accelerator: the prover's cubic extension. +pub fn fp3mac(state: [u64; 6], x: [u64; 3]) -> [u64; 3] { + use math::field::element::FieldElement; + use math::field::extensions_goldilocks::Degree3GoldilocksExtensionField; + use math::field::goldilocks::GoldilocksField; + type Fp = FieldElement; + type Fp3 = FieldElement; + let ext = |w: [u64; 3]| Fp3::new(w.map(Fp::from)); + let acc = ext([state[0], state[1], state[2]]); + let al = ext([state[3], state[4], state[5]]); + let out = acc * al + ext(x); + (*out.value()).map(|v| v.canonical()) +} + impl TryFrom for SyscallNumbers { type Error = (); fn try_from(value: u64) -> Result { @@ -201,6 +251,8 @@ impl TryFrom for SyscallNumbers { v if v == KECCAK_SYSCALL_NUMBER => Ok(SyscallNumbers::KeccakPermute), v if v == BLAKE3_SYSCALL_NUMBER => Ok(SyscallNumbers::Blake3Compress), v if v == BLAKE3_ABSORB_SYSCALL_NUMBER => Ok(SyscallNumbers::Blake3Absorb), + v if v == P1W16_SYSCALL_NUMBER => Ok(SyscallNumbers::P1w16Permute), + v if v == FP3MAC_SYSCALL_NUMBER => Ok(SyscallNumbers::Fp3Mac), v if v == ECSM_SYSCALL_NUMBER => Ok(SyscallNumbers::Ecsm), v if v == HINT_SYSCALL_NUMBER => Ok(SyscallNumbers::Hint), _ => Err(()), @@ -214,6 +266,8 @@ pub enum Accelerator { Keccak, Blake3, Ecsm, + P1w16, + Fp3Mac, } impl SyscallNumbers { @@ -229,6 +283,8 @@ impl SyscallNumbers { // calls" that no longer track BLAKE3 rows. SyscallNumbers::Blake3Absorb => Some(Accelerator::Blake3), SyscallNumbers::Ecsm => Some(Accelerator::Ecsm), + SyscallNumbers::P1w16Permute => Some(Accelerator::P1w16), + SyscallNumbers::Fp3Mac => Some(Accelerator::Fp3Mac), SyscallNumbers::Print | SyscallNumbers::Panic | SyscallNumbers::Commit @@ -637,6 +693,62 @@ impl Instruction { } src2_val = state_addr; } + SyscallNumbers::P1w16Permute => { + let state_addr = registers.read(10)?; + if !state_addr.is_multiple_of(8) { + return Err(ExecutionError::UnalignedP1w16StateAddress(state_addr)); + } + state_addr + .checked_add(P1W16_STATE_BYTES - 1) + .ok_or(ExecutionError::P1w16StateAddressOverflow(state_addr))?; + + let mut state = [0u64; 16]; + for (i, lane) in state.iter_mut().enumerate() { + *lane = memory.load_doubleword(state_addr + (i as u64) * 8)?; + if *lane >= GOLDILOCKS_P { + return Err(ExecutionError::P1w16NonCanonicalInput(*lane)); + } + } + for (i, lane) in p1w16_permute(state).iter().enumerate() { + memory.store_doubleword(state_addr + (i as u64) * 8, *lane)?; + } + src2_val = state_addr; + } + SyscallNumbers::Fp3Mac => { + let state_addr = registers.read(10)?; + let cell_addr = registers.read(11)?; + for (addr, bytes) in [ + (state_addr, FP3MAC_STATE_BYTES), + (cell_addr, FP3MAC_CELL_BYTES), + ] { + if !addr.is_multiple_of(8) { + return Err(ExecutionError::UnalignedFp3MacAddress(addr)); + } + addr.checked_add(bytes - 1) + .ok_or(ExecutionError::Fp3MacAddressOverflow(addr))?; + } + // The chip accesses all nine words at one timestamp. + if state_addr < cell_addr + FP3MAC_CELL_BYTES + && cell_addr < state_addr + FP3MAC_STATE_BYTES + { + return Err(ExecutionError::Fp3MacOverlap(state_addr, cell_addr)); + } + let mut state = [0u64; 6]; + for (i, w) in state.iter_mut().enumerate() { + *w = memory.load_doubleword(state_addr + (i as u64) * 8)?; + } + let mut x = [0u64; 3]; + for (i, w) in x.iter_mut().enumerate() { + *w = memory.load_doubleword(cell_addr + (i as u64) * 8)?; + } + if let Some(&w) = state.iter().chain(&x).find(|&&w| w >= GOLDILOCKS_P) { + return Err(ExecutionError::Fp3MacNonCanonicalInput(w)); + } + for (i, w) in fp3mac(state, x).iter().enumerate() { + memory.store_doubleword(state_addr + (i as u64) * 8, *w)?; + } + src2_val = state_addr; + } SyscallNumbers::Blake3Compress => { // BLAKE3 6-round compression on a 176-byte region at the // address in x10 (layout: see BLAKE3_SYSCALL_NUMBER docs). @@ -1017,6 +1129,20 @@ pub enum ExecutionError { UnalignedKeccakStateAddress(u64), #[error("Keccak state address range overflows: {0:#018x}")] KeccakStateAddressOverflow(u64), + #[error("Unaligned Poseidon1 state address: {0:#018x}")] + UnalignedP1w16StateAddress(u64), + #[error("Poseidon1 state address range overflows: {0:#018x}")] + P1w16StateAddressOverflow(u64), + #[error("Poseidon1 input word is not a canonical Goldilocks element: {0:#018x}")] + P1w16NonCanonicalInput(u64), + #[error("Unaligned FP3MAC operand address: {0:#018x}")] + UnalignedFp3MacAddress(u64), + #[error("FP3MAC operand address range overflows: {0:#018x}")] + Fp3MacAddressOverflow(u64), + #[error("FP3MAC input word is not a canonical Goldilocks element: {0:#018x}")] + Fp3MacNonCanonicalInput(u64), + #[error("FP3MAC state {0:#018x} and cell {1:#018x} overlap")] + Fp3MacOverlap(u64, u64), #[error("Unaligned BLAKE3 state address: {0:#018x}")] UnalignedBlake3StateAddress(u64), #[error("BLAKE3 state address range overflows: {0:#018x}")] diff --git a/prover/Cargo.toml b/prover/Cargo.toml index 6d6b59744..d55505719 100644 --- a/prover/Cargo.toml +++ b/prover/Cargo.toml @@ -22,6 +22,14 @@ instruments = ["stark/instruments"] nvtx = ["cuda", "instruments", "stark/nvtx"] profile-markers = ["stark/profile-markers"] disk-spill = ["stark/disk-spill"] +# Field VM at constraint degree 3, proved at blowup 2. +fvm-d3 = [] +# Field VM at constraint degree 4, proved at blowup 4. +fvm-d4 = [] +# Field VM with 2 general-purpose registers. +fvm-narrow = [] +# Field VM with a single general-purpose register. +fvm-n1 = [] # The BLAKE3 round count, for the `LFM_HASH` arm and — since the P-a flip — for # the commitment backends the whole prover commits under. Off = 7 rounds # (standard BLAKE3, externally anchored); on = the 6-round A6R variant, which is diff --git a/prover/src/block_whir.rs b/prover/src/block_whir.rs index 35560ae3a..9f348443e 100644 --- a/prover/src/block_whir.rs +++ b/prover/src/block_whir.rs @@ -5186,9 +5186,39 @@ impl BlockWhirProof { /// What a verifier derives from the program and a statement before any root, /// once the statement's checks pass. The host verifier and the recursion's tree /// plan both start from it, so they check one statement the same way. +/// A frame's AIR set: the Lambda VM's, or an owned list of other AIRs (the Field +/// VM's, behind a unit-public-input adapter) verified with the same emitters. +#[allow(clippy::large_enum_variant)] +pub(crate) enum FrameAirs { + Vm(VmAirs), + #[cfg(all(test, feature = "parallel"))] + Owned(Vec>>), +} + +impl FrameAirs { + pub(crate) fn air_refs( + &self, + ) -> Vec<&dyn stark::traits::AIR> { + match self { + FrameAirs::Vm(airs) => airs.air_refs(), + #[cfg(all(test, feature = "parallel"))] + FrameAirs::Owned(airs) => airs.iter().map(|a| a.as_ref()).collect(), + } + } + + /// The Lambda VM's AIRs; `None` for an owned set. + pub(crate) fn vm(&self) -> Option<&VmAirs> { + match self { + FrameAirs::Vm(airs) => Some(airs), + #[cfg(all(test, feature = "parallel"))] + FrameAirs::Owned(_) => None, + } + } +} + pub(crate) struct BlockFrame { pub(crate) page_configs: Vec, - pub(crate) airs: VmAirs, + pub(crate) airs: FrameAirs, /// Per table in [`VmAirs::air_refs`] order: the AIR's width and the stated /// height in variables. pub(crate) shapes: Vec<(usize, usize)>, @@ -5299,7 +5329,7 @@ pub(crate) fn block_frame( } Ok(BlockFrame { page_configs, - airs, + airs: FrameAirs::Vm(airs), shapes, config, order, @@ -5421,7 +5451,11 @@ pub(crate) fn verify_block_whir_traced( // The proof's tables are in group order, so the statements are taken in // that order too. let statements: Vec> = order.iter().map(|&i| statements[i]).collect(); - let prepared_columns = prepared_tables(airs, page_configs, format)?; + let prepared_columns = prepared_tables( + airs.vm().expect("a block's frame holds the VM's AIRs"), + page_configs, + format, + )?; let tag = block_statement_tag(&format.zf.base); Ok(crate::with_block_hash!(format.zf.base, |H| { diff --git a/prover/src/field_vm/air.rs b/prover/src/field_vm/air.rs new file mode 100644 index 000000000..c253f4cf2 --- /dev/null +++ b/prover/src/field_vm/air.rs @@ -0,0 +1,702 @@ +//! The `FIELD_VM` chip: one row per state. +//! +//! Spec: `spec/src/field_vm.toml`. Every `ExtField` variable takes three base +//! columns, and every `ExtField` constraint is emitted as three base +//! constraints with the `x³ = 2` reduction. + +use core::ops::{Add, Mul, Sub}; + +use stark::constraints::boundary::BoundaryConstraint; +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet, RowDomain}; +use stark::lookup::{ + BoundaryConstraintBuilder, BusInteraction, BusValue, LinearTerm, Multiplicity, Packing, +}; +use stark::trace::TraceTable; + +use super::executor::{Execution, State, Step}; +use super::isa::{Instr, N, NUM_REGS, Program}; +use super::mux::{D, MuxTables, Split, T, split_powers}; +use crate::tables::types::{BusId, FE, FEE, GoldilocksExtension, GoldilocksField, zeroed_fe_vec}; + +type F = GoldilocksField; +type E = GoldilocksExtension; + +pub mod cols { + use super::super::isa::N; + use super::super::mux::T; + + pub const PC: usize = 0; + /// `argument_registers[4]`, for `d, a, b, c`. + pub const ARG_REG: usize = 1; + /// `argument_scalars[4]`. + pub const ARG_SCALE: usize = ARG_REG + 4; + /// `argument_offsets[4]`. + pub const ARG_OFFSET: usize = ARG_SCALE + 4; + /// `mem_flags[4]`. + pub const MEM_FLAG: usize = ARG_OFFSET + 4; + /// `hint_input[N]`. + pub const HINT_IN: usize = MEM_FLAG + 4; + pub const HINT_OUT: usize = HINT_IN + N; + /// `registers[N]`, three columns each. + pub const REGS: usize = HINT_OUT + 1; + pub const ZERO: usize = REGS + 3 * N; + pub const OUT_INV: usize = ZERO + 1; + /// `arg_reg_pows_computed[4][T]`. + pub const POWS: usize = OUT_INV + 3; + /// The base address of each argument that reads memory (the spec's + /// `args_premem`, kept only where it differs from `args`). + pub const ADDR: usize = POWS + 4 * T; + pub const ARGS: usize = ADDR + 4; + pub const SEL: usize = ARGS + 12; + pub const NUM_COLUMNS: usize = SEL + 1; + + pub const fn reg(g: usize) -> usize { + REGS + 3 * g + } + /// `x_i^{split_exponent(k)}` for `k = 1..=T`. + pub const fn pow(i: usize, k: usize) -> usize { + POWS + i * T + (k - 1) + } + pub const fn addr(i: usize) -> usize { + ADDR + i + } + pub const fn arg(i: usize) -> usize { + ARGS + 3 * i + } +} + +/// Bit `i` of the packed flags: `mem_flags` (0..4), `hint_output` (4), `hint_input` (5..). +pub const FLAG_HINT_OUT: u32 = 4; +pub const FLAG_HINT_IN: u32 = 5; +/// Bits per register index in the packed argument registers. +pub const REG_BITS: u32 = 8; + +const _: () = assert!(FLAG_HINT_IN as usize + N <= 64 && NUM_REGS <= 1 << REG_BITS); + +/// The eleven base values of one `FIELD_VM_DECODE` tuple: `pc`, the leftover +/// `imm0`/`imm1` of `c`, the other `imm0`s, the other `imm1`s, the flags and +/// the packed register indices. +pub fn decode_tuple(pc: u64, instr: &Instr) -> [FE; 11] { + let args = instr.args(); + let mut flags = 0u64; + for (i, a) in args.iter().enumerate() { + flags |= (a.mem as u64) << i; + } + flags |= (instr.hint_out as u64) << FLAG_HINT_OUT; + for g in 0..N { + flags |= (instr.hint_in[g] as u64) << (FLAG_HINT_IN as usize + g); + } + let regs = args.iter().enumerate().fold(0u64, |acc, (i, a)| { + acc | (a.reg as u64) << (REG_BITS as usize * i) + }); + [ + FE::from(pc), + args[3].scale, + args[3].offset, + args[0].scale, + args[1].scale, + args[2].scale, + args[0].offset, + args[1].offset, + args[2].offset, + FE::from(flags), + FE::from(regs), + ] +} + +// ========================================================================= +// Trace generation +// ========================================================================= + +fn set_ext(row: &mut [FE], col: usize, v: &FEE) { + row[col..col + 3].copy_from_slice(v.value()); +} + +/// One FIELD_VM row; `out_inv` is `args[0]⁻¹`, or zero when it is zero. +fn fill_row(row: &mut [FE], program: &Program, step: &Step, out_inv: &FEE) { + let State { zero, pc, regs } = step.state; + let instr = &program.instrs[pc as usize]; + row[cols::PC] = FE::from(pc); + for (i, a) in instr.args().iter().enumerate() { + let x = FE::from(a.reg as u64); + row[cols::ARG_REG + i] = x; + row[cols::ARG_SCALE + i] = a.scale; + row[cols::ARG_OFFSET + i] = a.offset; + row[cols::MEM_FLAG + i] = FE::from(a.mem as u64); + let pows = split_powers(x); + for (k, p) in pows.iter().enumerate().skip(1) { + row[cols::pow(i, k)] = *p; + } + if a.mem { + row[cols::addr(i)] = step.args_premem[i].value()[0]; + } + set_ext(row, cols::arg(i), &step.args[i]); + } + for (g, r) in regs.iter().enumerate() { + row[cols::HINT_IN + g] = FE::from(instr.hint_in[g] as u64); + set_ext(row, cols::reg(g), r); + } + row[cols::HINT_OUT] = FE::from(instr.hint_out as u64); + row[cols::ZERO] = FE::from(zero as u64); + set_ext(row, cols::OUT_INV, out_inv); +} + +/// Rows per block of the parallel fill; each block inverts its `args[0]` in +/// one batch. +const FILL_BLOCK: usize = 4096; + +/// A FIELD_VM table of `rows` rows whose row `r` holds `step(r)`. +fn fill_table<'a>( + program: &Program, + rows: usize, + step: impl Fn(usize) -> &'a Step + Sync, +) -> TraceTable { + let width = cols::NUM_COLUMNS; + let mut data = zeroed_fe_vec(rows * width); + let fill = |(b, block): (usize, &mut [FE])| { + let first = b * FILL_BLOCK; + let n = block.len() / width; + let mut inv: Vec = (0..n) + .map(|r| { + let d = step(first + r).args[0]; + if d == FEE::zero() { FEE::one() } else { d } + }) + .collect(); + FEE::inplace_batch_inverse(&mut inv).expect("no zero left to invert"); + for (r, row) in block.chunks_mut(width).enumerate() { + let st = step(first + r); + let out_inv = if st.args[0] == FEE::zero() { + FEE::zero() + } else { + inv[r] + }; + fill_row(row, program, st, &out_inv); + } + }; + #[cfg(feature = "parallel")] + { + use rayon::prelude::*; + data.par_chunks_mut(FILL_BLOCK * width) + .enumerate() + .for_each(fill); + } + #[cfg(not(feature = "parallel"))] + data.chunks_mut(FILL_BLOCK * width) + .enumerate() + .for_each(fill); + TraceTable::new_main(data, width, 1) +} + +/// The padding share (in percent) a single power-of-two table may waste +/// before it is split: `FVM_SEGMENT_WASTE`, default 25. Shared with DECODE. +pub fn max_waste_percent() -> usize { + std::env::var("FVM_SEGMENT_WASTE") + .ok() + .and_then(|v| v.parse().ok()) + .unwrap_or(25) +} + +/// Whether `rows` padded rows over `used` real ones stay within the waste bound. +pub fn within_waste(used: usize, rows: usize) -> bool { + (rows - used) * 100 <= rows * max_waste_percent() +} + +/// A split must save at least this share (in percent) of the whole table's +/// rows to pay for the extra table: `FVM_SPLIT_MIN_SAVE`, default 0. +pub fn min_save_percent() -> usize { + std::env::var("FVM_SPLIT_MIN_SAVE") + .ok() + .and_then(|v| v.parse().ok()) + .unwrap_or(0) +} + +/// Whether splitting `left` into `half` and the rest saves enough of `total`. +pub fn split_pays(left: usize, half: usize, total: usize, min_rows: usize) -> bool { + let full = left.next_power_of_two().max(min_rows); + let split = half + (left - half).next_power_of_two().max(min_rows); + full.saturating_sub(split) * 100 >= total * min_save_percent() +} + +/// At most this many FIELD_VM segments when no cap forces more. +pub const MAX_SEGMENTS: usize = 4; + +/// `(real steps, rows)` per segment. A segment that is not the last holds +/// `rows − 1` steps and repeats the next segment's first row as its last, so +/// the transition out of its last step is checked inside it. A single +/// power-of-two table is used when it wastes at most a quarter of its rows. +/// `max_rows` caps every segment (tests use it to force long chains). +pub fn segment_plan(steps: usize, min_rows: usize, max_rows: Option) -> Vec<(usize, usize)> { + // `FVM_ONE_SEGMENT`: one segment, so the boundary states are the start + // and the halt, both program text. + if max_rows.is_none() && std::env::var_os("FVM_ONE_SEGMENT").is_some() { + return vec![(steps, steps.next_power_of_two().max(min_rows))]; + } + let cap = max_rows.unwrap_or(usize::MAX); + let mut plan = Vec::new(); + let mut left = steps; + loop { + let full = left.next_power_of_two().max(min_rows); + let rows = (full / 2).min(cap).max(min_rows); + let fits = full <= cap; + let last_allowed = max_rows.is_none() && plan.len() + 1 == MAX_SEGMENTS; + let pays = max_rows.is_some() || split_pays(left, rows - 1, steps, min_rows); + if fits && (within_waste(left, full) || last_allowed || rows > left || !pays) { + plan.push((left, full)); + return plan; + } + plan.push((rows - 1, rows)); + left -= rows - 1; + } +} + +pub struct Segments { + pub traces: Vec>, + pub public: Vec, + /// DECODE multiplicities, padding and repeated rows included. + pub decode_mult: Vec, + /// MEM multiplicities, repeated rows included. + pub mem_mult: Vec, +} + +/// The FIELD_VM segments of `exec`, the last padded with halt steps. +pub fn generate_segments( + program: &Program, + exec: &Execution, + min_rows: usize, + max_rows: Option, +) -> Segments { + let halt = *exec + .steps + .last() + .expect("an execution ends with a halt step"); + let plan = segment_plan(exec.steps.len(), min_rows, max_rows); + let mut decode_mult = exec.decode_mult.clone(); + let mut mem_mult = exec.mem_mult.clone(); + let (mut traces, mut public) = (Vec::new(), Vec::new()); + let mut start = 0; + for (k, &(real, rows)) in plan.iter().enumerate() { + let last = k + 1 == plan.len(); + let mut trace = fill_table(program, rows, |row| { + if row < real { + &exec.steps[start + row] + } else if last { + &halt + } else { + &exec.steps[start + real] + } + }); + // The state bus is signed: each segment contributes +1 at its first + // state and -1 at its final state. The transition constraint below + // leaves just these two endpoint rows available for nonzero SEL. + trace.main_table.set(0, cols::SEL, FE::one()); + trace.main_table.set(rows - 1, cols::SEL, -FE::one()); + if last { + decode_mult[halt.state.pc as usize] += (rows - real) as u64; + } else { + // The repeated row looks up the program and memory once more. + let repeat = &exec.steps[start + real]; + decode_mult[repeat.state.pc as usize] += 1; + let instr = &program.instrs[repeat.state.pc as usize]; + for (i, a) in instr.args().iter().enumerate() { + if a.mem { + mem_mult[repeat.args_premem[i].value()[0].canonical() as usize] += 1; + } + } + } + public.push(FvmPublicInputs { + last_row: rows - 1, + first: state_words(&exec.steps[start].state), + last: if last { + halt_words() + } else { + state_words(&exec.steps[start + real].state) + }, + }); + traces.push(trace); + start += real; + } + Segments { + traces, + public, + decode_mult, + mem_mult, + } +} + +// ========================================================================= +// Bus interactions +// ========================================================================= + +fn direct(c: usize) -> BusValue { + BusValue::Packed { + start_column: c, + packing: Packing::Direct, + } +} + +/// - **Sends** `FIELD_VM_DECODE[decode_tuple]` once per row. +/// - **Sends** `FIELD_VM_MEM[addr[i], 0, 0] -> args[i]` when `mem_flags[i]`. +pub fn bus_interactions() -> Vec { + let mut flags: Vec = (0..4) + .map(|i| LinearTerm::Column { + coefficient: 1 << i, + column: cols::MEM_FLAG + i, + }) + .collect(); + flags.push(LinearTerm::Column { + coefficient: 1 << FLAG_HINT_OUT, + column: cols::HINT_OUT, + }); + flags.extend((0..N).map(|g| LinearTerm::Column { + coefficient: 1 << (FLAG_HINT_IN as usize + g), + column: cols::HINT_IN + g, + })); + let regs = (0..4) + .map(|i| LinearTerm::Column { + coefficient: 1 << (REG_BITS as usize * i), + column: cols::ARG_REG + i, + }) + .collect(); + + let mut decode = vec![ + direct(cols::PC), + direct(cols::ARG_SCALE + 3), + direct(cols::ARG_OFFSET + 3), + ]; + decode.extend((0..3).map(|i| direct(cols::ARG_SCALE + i))); + decode.extend((0..3).map(|i| direct(cols::ARG_OFFSET + i))); + decode.push(BusValue::linear(flags)); + decode.push(BusValue::linear(regs)); + + let mut interactions = vec![BusInteraction::sender( + BusId::FieldVmDecode, + Multiplicity::One, + decode, + )]; + interactions.push(BusInteraction::sender( + BusId::FieldVmState, + Multiplicity::Column(cols::SEL), + [cols::PC, cols::ZERO] + .into_iter() + .chain(cols::REGS..cols::REGS + 3 * N) + .map(direct) + .collect(), + )); + for i in 0..4 { + let values = (0..3) + .map(|k| { + if k == 0 { + direct(cols::addr(i)) + } else { + BusValue::constant(0) + } + }) + .chain((0..3).map(|k| direct(cols::arg(i) + k))) + .collect(); + interactions.push(BusInteraction::sender( + BusId::FieldVmMem, + Multiplicity::Column(cols::MEM_FLAG + i), + values, + )); + } + interactions +} + +// ========================================================================= +// Constraints +// ========================================================================= + +type Ext3 = [X; 3]; + +fn ext_add>(a: &Ext3, b: &Ext3) -> Ext3 { + core::array::from_fn(|k| a[k].clone() + b[k].clone()) +} + +fn ext_sub>(a: &Ext3, b: &Ext3) -> Ext3 { + core::array::from_fn(|k| a[k].clone() - b[k].clone()) +} + +fn ext_scale>(s: &X, a: &Ext3) -> Ext3 { + core::array::from_fn(|k| s.clone() * a[k].clone()) +} + +/// `a · b` in `F[w]/(w³ − 2)`. +fn ext_mul + Mul>( + a: &Ext3, + b: &Ext3, + two: &X, +) -> Ext3 { + let m = |i: usize, j: usize| a[i].clone() * b[j].clone(); + [ + m(0, 0) + two.clone() * (m(1, 2) + m(2, 1)), + m(0, 1) + m(1, 0) + two.clone() * m(2, 2), + m(0, 2) + m(1, 1) + m(2, 0), + ] +} + +#[derive(Clone, Default)] +pub struct FieldVmConstraints { + tables: MuxTables, +} + +impl FieldVmConstraints { + pub fn new() -> Self { + Self::default() + } +} + +struct Emitter { + idx: usize, +} + +impl Emitter { + fn all>(&mut self, b: &mut B, e: B::Expr) { + b.emit_base(self.idx, e); + self.idx += 1; + } + + fn next>(&mut self, b: &mut B, e: B::Expr) { + b.emit_base_rows(self.idx, RowDomain::except_last(1), e); + self.idx += 1; + } +} + +fn ext_col>(b: &B, off: usize, col: usize) -> Ext3 { + core::array::from_fn(|k| b.main(off, col + k)) +} + +fn all_regs>(b: &B, off: usize) -> Vec> { + let mut regs = vec![ + [b.main(off, cols::ZERO), b.zero(), b.zero()], + [b.main(off, cols::PC), b.zero(), b.zero()], + ]; + regs.extend((0..N).map(|g| ext_col(b, off, cols::reg(g)))); + regs +} + +/// `Σ_k pow_{i,k} Σ_l s[k][l] x_i^l`, skipping zero coefficients so the +/// captured degree is the real one. +fn eval_split>(b: &B, s: &Split, i: usize) -> B::Expr { + let x = b.main(0, cols::ARG_REG + i); + let mut acc: Option = None; + for (k, split) in s.iter().enumerate() { + let mut inner: Option = None; + let mut x_pow: Option = None; + for c in split.iter() { + if *c != FE::zero() { + let coeff = b.const_base(c.canonical()); + let term = match &x_pow { + None => coeff, + Some(p) => coeff * p.clone(), + }; + inner = Some(match inner { + None => term, + Some(acc) => acc + term, + }); + } + x_pow = Some(match x_pow { + None => x.clone(), + Some(p) => p * x.clone(), + }); + } + let Some(inner) = inner else { continue }; + let term = if k == 0 { + inner + } else { + b.main(0, cols::pow(i, k)) * inner + }; + acc = Some(match acc { + None => term, + Some(a) => a + term, + }); + } + acc.unwrap_or_else(|| b.zero()) +} + +impl ConstraintSet for FieldVmConstraints { + fn max_degree(&self) -> usize { + D + } + + fn eval>(&self, b: &mut B) { + let mut em = Emitter { idx: 0 }; + let one = b.one(); + let two = b.const_base(2); + let bit = |b: &B, c: usize| { + let x = b.main(0, c); + x.clone() * (x - b.one()) + }; + + // SEL is supported only at rows 0 and h-1. On transition rows + // 0..h-3 this zeros SEL at the next row, covering rows 1..h-2; + // the first and final rows remain the segment boundary claims. + b.emit_base_rows(em.idx, RowDomain::except_last(2), b.main(1, cols::SEL)); + em.idx += 1; + + // decode + for i in 0..4 { + let e = bit(b, cols::MEM_FLAG + i); + em.all(b, e); + } + for g in 0..N { + let e = bit(b, cols::HINT_IN + g); + em.all(b, e); + } + let e = bit(b, cols::HINT_OUT); + em.all(b, e); + for i in 0..4 { + let e = eval_split(b, &self.tables.range, i); + em.all(b, e); + } + + // mux + for i in 0..4 { + let x = b.main(0, cols::ARG_REG + i); + let mut prev: Option = None; + for k in (1..).take(T) { + let step = if k == 1 { D - 1 } else { D - 2 }; + let mut p = prev.clone().unwrap_or_else(|| b.one()); + for _ in 0..step { + p = p * x.clone(); + } + let e = b.main(0, cols::pow(i, k)) - p; + em.all(b, e); + prev = Some(b.main(0, cols::pow(i, k))); + } + } + let premem = |b: &B, i: usize, off: usize| -> Ext3 { + let regs = all_regs(b, off); + let mut sum: Ext3 = [b.zero(), b.zero(), b.zero()]; + for (j, r) in regs.iter().enumerate() { + let sel = eval_split(b, &self.tables.mux[j], i); + sum = ext_add(&sum, &ext_scale(&sel, r)); + } + let scaled = ext_scale(&b.main(0, cols::ARG_SCALE + i), &sum); + [ + scaled[0].clone() + b.main(0, cols::ARG_OFFSET + i), + scaled[1].clone(), + scaled[2].clone(), + ] + }; + // memory: before the lookup an argument is its base address when it + // reads memory, and its value otherwise. + let before_lookup = |b: &B, i: usize| -> Ext3 { + let mem = b.main(0, cols::MEM_FLAG + i); + let not_mem = b.one() - mem.clone(); + let arg = ext_col(b, 0, cols::arg(i)); + [ + mem * b.main(0, cols::addr(i)) + not_mem.clone() * arg[0].clone(), + not_mem.clone() * arg[1].clone(), + not_mem * arg[2].clone(), + ] + }; + for i in 1..4 { + for e in ext_sub(&before_lookup(b, i), &premem(b, i, 0)) { + em.all(b, e); + } + } + for e in ext_sub(&before_lookup(b, 0), &premem(b, 0, 1)) { + em.next(b, e); + } + + // fma + let args: Vec> = (0..4).map(|i| ext_col(b, 0, cols::arg(i))).collect(); + let rhs = ext_add(&ext_mul(&args[1], &args[2], &two), &args[3]); + for e in ext_sub(&args[0], &rhs) { + em.all(b, e); + } + + // transition + let not_hint_out = one.clone() - b.main(0, cols::HINT_OUT); + for g in 0..N { + let not_hinted_next = one.clone() - b.main(1, cols::HINT_IN + g); + let not_out_reg = one.clone() - eval_split(b, &self.tables.mux[g + 2], 0); + let diff = ext_sub(&ext_col(b, 1, cols::reg(g)), &ext_col(b, 0, cols::reg(g))); + for e in diff.iter() { + em.next( + b, + not_hinted_next.clone() * not_hint_out.clone() * e.clone(), + ); + } + for e in diff { + em.next(b, not_hinted_next.clone() * not_out_reg.clone() * e); + } + } + let pc_step = b.main(1, cols::PC) - b.main(0, cols::PC) - one.clone(); + em.next(b, not_hint_out * pc_step.clone()); + let not_out_pc = one.clone() - eval_split(b, &self.tables.mux[1], 0); + em.next(b, not_out_pc * pc_step); + let e = bit(b, cols::ZERO); + em.all(b, e); + let zero_next = b.main(1, cols::ZERO); + for e in args[0].iter() { + em.next(b, zero_next.clone() * e.clone()); + } + let not_zero_next = one.clone() - zero_next; + let prod = ext_mul(&args[0], &ext_col(b, 0, cols::OUT_INV), &two); + let target = [one.clone(), b.zero(), b.zero()]; + for e in ext_sub(&prod, &target) { + em.next(b, not_zero_next.clone() * e); + } + } +} + +// ========================================================================= +// Boundary constraints +// ========================================================================= + +/// The state a boundary row pins: `pc`, `ZERO`, then every register +/// component, as canonical words. +pub const STATE_WORDS: usize = 2 + 3 * N; + +pub fn state_words(state: &State) -> Vec { + let mut w = Vec::with_capacity(STATE_WORDS); + w.push(state.pc); + w.push(state.zero as u64); + for r in &state.regs { + w.extend(r.value().iter().map(|c| c.canonical())); + } + w +} + +/// The start state: `PC = 1`, `ZERO = 0`, registers `0`. +pub fn start_words() -> Vec { + state_words(&State::initial()) +} + +/// The halt state: `PC = 0`, `ZERO = 1`, registers `0`. +pub fn halt_words() -> Vec { + let mut w = vec![0; STATE_WORDS]; + w[1] = 1; + w +} + +#[derive( + Clone, Debug, Default, PartialEq, Eq, rkyv::Archive, rkyv::Serialize, rkyv::Deserialize, +)] +pub struct FvmPublicInputs { + /// Index of the last FIELD_VM row; checked against the proof's trace length. + pub last_row: usize, + /// The segment's first-row state ([`state_words`]). + pub first: Vec, + /// The segment's last-row state: the next segment's first, or the halt. + pub last: Vec, +} + +/// First and last rows pinned to the segment's boundary states. +pub struct FieldVmBoundary; + +impl BoundaryConstraintBuilder for FieldVmBoundary { + fn boundary_constraints(pi: &FvmPublicInputs, _: &[FEE]) -> Vec> { + let columns = [cols::PC, cols::ZERO] + .into_iter() + .chain(cols::REGS..cols::REGS + 3 * N); + let mut out = Vec::with_capacity(2 * STATE_WORDS); + for (step, words) in [(0, &pi.first), (pi.last_row, &pi.last)] { + for (c, w) in columns.clone().zip(words) { + out.push(BoundaryConstraint::new_main(c, step, FEE::from(*w))); + } + } + out + } +} diff --git a/prover/src/field_vm/asm.rs b/prover/src/field_vm/asm.rs new file mode 100644 index 000000000..eeb8196c3 --- /dev/null +++ b/prover/src/field_vm/asm.rs @@ -0,0 +1,195 @@ +//! Assembler for the Field VM, with the pseudoinstructions of the spec's +//! "Instruction notation" table and its calling convention. + +use super::isa::{Arg, ENTRY_PC, Instr, Program, REG_PC, REG_ZERO, gpr_index}; + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct Label(usize); + +#[derive(Clone, Copy, Debug)] +enum Fixup { + /// `FMA PC == target`. + Jump, + /// `FMA PC == ZERO * (-PC + (target - 1)) + (PC + 1)`. + JumpZero, + /// `FMA PC == ZERO * (PC - target) + (ZERO + target)`. + JumpNotZero, +} + +#[derive(Default)] +pub struct Asm { + body: Vec, + labels: Vec>, + fixups: Vec<(usize, Label, Fixup)>, +} + +#[derive(Debug, PartialEq, Eq)] +pub enum AsmError { + UnboundLabel(Label), + Invalid { pc: usize, reason: &'static str }, +} + +impl Asm { + pub fn new() -> Self { + Self::default() + } + + /// Address of the next emitted instruction. + pub fn here(&self) -> u64 { + ENTRY_PC + self.body.len() as u64 + } + + pub fn label(&mut self) -> Label { + self.labels.push(None); + Label(self.labels.len() - 1) + } + + pub fn bind(&mut self, l: Label) { + assert!(self.labels[l.0].is_none(), "label bound twice"); + self.labels[l.0] = Some(self.here()); + } + + pub fn emit(&mut self, instr: Instr) -> &mut Self { + self.body.push(instr); + self + } + + /// Marks general-purpose registers as input-hinted by the last instruction. + pub fn hint_in(&mut self, regs: &[u8]) -> &mut Self { + let last = self.body.last_mut().expect("no instruction to hint"); + for &r in regs { + let g = gpr_index(r).expect("only general-purpose registers can be input-hinted"); + last.hint_in[g] = true; + } + self + } + + /// `FMA d == a * b + c`. + pub fn fma(&mut self, d: Arg, a: Arg, b: Arg, c: Arg) -> &mut Self { + self.emit(Instr::new(d, a, b, c, false)) + } + + /// `FMA d == a * b + c, hint out`. + pub fn fma_out(&mut self, d: Arg, a: Arg, b: Arg, c: Arg) -> &mut Self { + self.emit(Instr::new(d, a, b, c, true)) + } + + pub fn add(&mut self, d: Arg, a: Arg, b: Arg) -> &mut Self { + self.fma_out(d, Arg::imm(1), a, b) + } + + /// `d = a - b`. + pub fn sub(&mut self, d: Arg, a: Arg, b: Arg) -> &mut Self { + self.fma_out(d, Arg::imm(-1), b, a) + } + + pub fn mul(&mut self, d: Arg, a: Arg, b: Arg) -> &mut Self { + self.fma_out(d, a, b, Arg::imm(0)) + } + + pub fn mov(&mut self, d: Arg, a: Arg) -> &mut Self { + self.fma_out(d, Arg::imm(0), Arg::imm(0), a) + } + + /// Asserts `MEM[addr] == v`, fixing the cell if it is still free. + pub fn store(&mut self, addr: Arg, v: Arg) -> &mut Self { + assert!(addr.mem); + self.fma(addr, Arg::imm(0), Arg::imm(0), v) + } + + /// `reg = a^{-1}` as `FMA reg == (a + 1) * reg - 1, hint reg`. + /// `a` must not dereference memory nor use `reg`. + pub fn inv(&mut self, reg: u8, a: Arg) -> &mut Self { + assert!( + !a.mem && a.reg != reg, + "INV: `a` must be a register expression not using `reg`" + ); + let a1 = Arg { + offset: a.offset + math::field::element::FieldElement::one(), + ..a + }; + self.fma(Arg::reg(reg), a1, Arg::reg(reg), Arg::imm(-1)) + .hint_in(&[reg]) + } + + fn jump_kind(&mut self, target: Label, kind: Fixup) -> &mut Self { + self.fixups.push((self.body.len(), target, kind)); + self.fma_out(Arg::reg(REG_PC), Arg::imm(0), Arg::imm(0), Arg::imm(0)) + } + + pub fn jump(&mut self, target: Label) -> &mut Self { + self.jump_kind(target, Fixup::Jump) + } + + /// Jumps when the previous instruction's `d` was zero. + pub fn jump_zero(&mut self, target: Label) -> &mut Self { + self.jump_kind(target, Fixup::JumpZero) + } + + /// Jumps when the previous instruction's `d` was nonzero. + pub fn jump_not_zero(&mut self, target: Label) -> &mut Self { + self.jump_kind(target, Fixup::JumpNotZero) + } + + /// `FMA PC == 0, hint out`: jump into the halt loop. + pub fn halt(&mut self) -> &mut Self { + self.fma_out(Arg::reg(REG_PC), Arg::imm(0), Arg::imm(0), Arg::imm(0)) + } + + /// The spec's `CALL`. The new frame pointer is an output hint the oracle + /// answers. `saved` registers go to `MEM[fp - 1 - i]`, `args` (evaluated + /// with the new `fp`) to `MEM[fp + 2 + j]`; the callee leaves its result at + /// `MEM[fp + 2 + args.len()]`, which lands in `ret` before the caller's + /// registers and `fp` are restored. + pub fn call( + &mut self, + target: Label, + fp: u8, + saved: &[u8], + args: &[Arg], + ret: Option, + ) -> &mut Self { + self.fma_out(Arg::mem(fp, 0), Arg::imm(0), Arg::imm(0), Arg::reg(fp)); + for (i, &r) in saved.iter().enumerate() { + self.store(Arg::mem(fp, -1 - i as i64), Arg::reg(r)); + } + for (j, &a) in args.iter().enumerate() { + self.store(Arg::mem(fp, 2 + j as i64), a); + } + self.store(Arg::mem(fp, 1), Arg::lin(REG_PC, 1, 2)); + self.jump(target); + if let Some(r) = ret { + self.mov(Arg::reg(r), Arg::mem(fp, 2 + args.len() as i64)); + } + for (i, &r) in saved.iter().enumerate() { + self.mov(Arg::reg(r), Arg::mem(fp, -1 - i as i64)); + } + self.mov(Arg::reg(fp), Arg::mem(fp, 0)) + } + + /// `FMA PC == MEM[fp + 1], hint out`. + pub fn ret(&mut self, fp: u8) -> &mut Self { + self.fma_out(Arg::reg(REG_PC), Arg::imm(0), Arg::imm(0), Arg::mem(fp, 1)) + } + + pub fn finish(mut self) -> Result { + for &(idx, label, kind) in &self.fixups { + let t = self.labels[label.0].ok_or(AsmError::UnboundLabel(label))? as i64; + let instr = &mut self.body[idx]; + match kind { + Fixup::Jump => instr.c = Arg::imm(t), + Fixup::JumpZero => { + instr.a = Arg::reg(REG_ZERO); + instr.b = Arg::lin(REG_PC, -1, t - 1); + instr.c = Arg::lin(REG_PC, 1, 1); + } + Fixup::JumpNotZero => { + instr.a = Arg::reg(REG_ZERO); + instr.b = Arg::lin(REG_PC, 1, -t); + instr.c = Arg::lin(REG_ZERO, 1, t); + } + } + } + Program::new(self.body).map_err(|(pc, reason)| AsmError::Invalid { pc, reason }) + } +} diff --git a/prover/src/field_vm/bridge.rs b/prover/src/field_vm/bridge.rs new file mode 100644 index 000000000..65d04afce --- /dev/null +++ b/prover/src/field_vm/bridge.rs @@ -0,0 +1,135 @@ +//! The `FIELD_VM_BRIDGE` chip: the cells that cross between the Field VM's +//! memory and the LFM hash-side chips' `LfmMem` bus. +//! +//! One preprocessed row per crossing cell. Every row reads the cell from MEM +//! (`FIELD_VM_MEM` sender, like any Field VM read); an outgoing row then +//! sends it on `LfmMem` with the program's read count, an incoming row +//! receives the hash side's write of it. MEM holds three lanes, `LfmMem` +//! four: the fourth is a witness column, pinned to the preprocessed `L3C` +//! unless the row is a word (a hint, or an incoming cell). + +use stark::config::Commitment; +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet}; +use stark::lookup::{BusInteraction, BusValue, Multiplicity, Packing}; +use stark::proof::options::ProofOptions; +use stark::trace::TraceTable; + +use crate::tables::types::{BusId, FE, GoldilocksExtension, GoldilocksField, zeroed_fe_vec}; + +type F = GoldilocksField; +type E = GoldilocksExtension; + +pub mod cols { + /// The cell's Field VM memory address. + pub const FADDR: usize = 0; + /// The cell's LFM address. + pub const LADDR: usize = 1; + pub const MULT_OUT: usize = 2; + pub const IS_IN: usize = 3; + pub const IS_WORD: usize = 4; + pub const L3C: usize = 5; + pub const IS_REAL: usize = 6; + pub const NUM_PRECOMPUTED_COLS: usize = 7; + pub const V0: usize = NUM_PRECOMPUTED_COLS; + pub const NUM_COLUMNS: usize = V0 + 4; +} + +#[derive(Clone, Debug)] +pub struct BridgeRow { + pub faddr: u64, + pub laddr: u64, + /// Hash-side reads of an outgoing cell; zero for an incoming one. + pub mult_out: u64, + pub is_in: bool, + pub is_word: bool, + /// Lane 3 of a non-word outgoing cell. + pub l3c: FE, +} + +fn fill_prep(rows: &[BridgeRow], min_rows: usize) -> TraceTable { + let height = rows.len().next_power_of_two().max(min_rows); + let mut trace = TraceTable::new_main( + zeroed_fe_vec(height * cols::NUM_COLUMNS), + cols::NUM_COLUMNS, + 1, + ); + let t = &mut trace.main_table; + for (i, r) in rows.iter().enumerate() { + t.set(i, cols::FADDR, FE::from(r.faddr)); + t.set(i, cols::LADDR, FE::from(r.laddr)); + t.set(i, cols::MULT_OUT, FE::from(r.mult_out)); + t.set(i, cols::IS_IN, FE::from(r.is_in as u64)); + t.set(i, cols::IS_WORD, FE::from(r.is_word as u64)); + t.set(i, cols::L3C, r.l3c); + t.set(i, cols::IS_REAL, FE::one()); + } + trace +} + +/// `value(i)` is the four-lane word of row `i`. +pub fn generate_trace( + rows: &[BridgeRow], + value: impl Fn(usize) -> [FE; 4], + min_rows: usize, +) -> TraceTable { + let mut trace = fill_prep(rows, min_rows); + let t = &mut trace.main_table; + for i in 0..rows.len() { + for (k, v) in value(i).into_iter().enumerate() { + t.set(i, cols::V0 + k, v); + } + } + trace +} + +/// The Merkle root of the preprocessed columns. +pub fn commitment(rows: &[BridgeRow], options: &ProofOptions, min_rows: usize) -> Commitment { + let trace = fill_prep(rows, min_rows); + let columns: Vec> = (0..cols::NUM_PRECOMPUTED_COLS) + .map(|c| { + (0..trace.num_rows()) + .map(|r| *trace.main_table.get(r, c)) + .collect() + }) + .collect(); + crate::field_vm::prove::commit_prep(&columns, options) +} + +pub fn bus_interactions() -> Vec { + let direct = |c| BusValue::Packed { + start_column: c, + packing: Packing::Direct, + }; + let word = || { + let mut v = vec![direct(cols::LADDR)]; + v.extend((0..4).map(|k| direct(cols::V0 + k))); + v + }; + vec![ + BusInteraction::sender( + BusId::FieldVmMem, + Multiplicity::Column(cols::IS_REAL), + vec![ + direct(cols::FADDR), + BusValue::constant(0), + BusValue::constant(0), + direct(cols::V0), + direct(cols::V0 + 1), + direct(cols::V0 + 2), + ], + ), + BusInteraction::sender(BusId::LfmMem, Multiplicity::Column(cols::MULT_OUT), word()), + BusInteraction::receiver(BusId::LfmMem, Multiplicity::Column(cols::IS_IN), word()), + ] +} + +#[derive(Clone, Copy, Default)] +pub struct BridgeConstraints; + +impl ConstraintSet for BridgeConstraints { + fn eval>(&self, b: &mut B) { + let free = b.one() - b.main(0, cols::IS_WORD); + let lane3 = b.main(0, cols::V0 + 3) - b.main(0, cols::L3C); + b.emit_base(0, free * lane3); + } +} diff --git a/prover/src/field_vm/cksum.rs b/prover/src/field_vm/cksum.rs new file mode 100644 index 000000000..21c146eb9 --- /dev/null +++ b/prover/src/field_vm/cksum.rs @@ -0,0 +1,410 @@ +//! The `FIELD_VM_CKSUM` chip: option B's binding of the cells that cross +//! between the halves, when the two halves are two proofs. +//! +//! One preprocessed row per crossing cell, in the order both halves agree on. +//! Every real row reads its cell from MEM (`FIELD_VM_MEM`, like any Field VM +//! read) and folds it into a Horner accumulator over Fp³, +//! +//! ```text +//! acc_0 = x_0, acc_{i+1} = acc_i·α + x_{i+1}, s = acc_{n−1}, +//! ``` +//! +//! padding rows keeping it, and the last row sends `(CKSUM_ADDR, s)` on +//! `FIELD_VM_PUBLIC`, so the verifier closes `s` as a public cell. +//! +//! `α` sits in three columns, one value down the table, and the last row +//! sends `(CKSUM_ALPHA_ADDR, α)` too: the verifier closes it at the `α` it +//! draws outside both proofs, from the guest's hash of the crossing cells and +//! the roots committed before this table ([`binding_alpha`]), so the AIR +//! itself does not depend on the proof. The guest +//! computes the same Horner sum over its copies, and the outer verifier checks +//! the two agree: two different vectors agree at a random `α` with +//! probability at most `n / p³`. + +use stark::config::Commitment; +use stark::constraints::builder::{ConstraintBuilder, ConstraintSet, RowDomain}; +use stark::lookup::{BusInteraction, BusValue, Multiplicity, Packing}; +use stark::proof::options::ProofOptions; +use stark::trace::TraceTable; + +use crate::tables::types::{BusId, FE, FEE, GoldilocksExtension, GoldilocksField, zeroed_fe_vec}; + +type F = GoldilocksField; +type E = GoldilocksExtension; + +/// The public-cell address `s` is published under: above every memory address. +pub const CKSUM_ADDR: u64 = 1 << 40; +/// The public-cell address `α` is published under. +pub const CKSUM_ALPHA_ADDR: u64 = CKSUM_ADDR + 1; + +pub mod cols { + /// The cell's Field VM memory address. + pub const FADDR: usize = 0; + pub const IS_REAL: usize = 1; + pub const IS_FIRST: usize = 2; + pub const IS_LAST: usize = 3; + pub const NUM_PRECOMPUTED_COLS: usize = 4; + pub const V0: usize = NUM_PRECOMPUTED_COLS; + pub const ACC0: usize = V0 + 3; + pub const AL0: usize = ACC0 + 3; + pub const NUM_COLUMNS: usize = AL0 + 3; +} + +fn height(n: usize, min_rows: usize) -> usize { + n.next_power_of_two().max(min_rows) +} + +fn fill_prep(faddr: &[u64], min_rows: usize) -> TraceTable { + assert!(!faddr.is_empty(), "a binding covers at least one cell"); + let h = height(faddr.len(), min_rows); + let mut trace = + TraceTable::new_main(zeroed_fe_vec(h * cols::NUM_COLUMNS), cols::NUM_COLUMNS, 1); + let t = &mut trace.main_table; + for (i, &a) in faddr.iter().enumerate() { + t.set(i, cols::FADDR, FE::from(a)); + t.set(i, cols::IS_REAL, FE::one()); + } + t.set(0, cols::IS_FIRST, FE::one()); + t.set(h - 1, cols::IS_LAST, FE::one()); + trace +} + +/// The verifier-side columns for the multilinear path, which cannot rely on +/// the legacy preprocessed root alone to bind these addresses. +pub fn preprocessed_columns(faddr: &[u64], min_rows: usize) -> Vec> { + let trace = fill_prep(faddr, min_rows); + (0..cols::NUM_PRECOMPUTED_COLS) + .map(|c| { + (0..trace.num_rows()) + .map(|r| *trace.main_table.get(r, c)) + .collect() + }) + .collect() +} + +/// `acc·α` in Fp³ = Fp[t]/(t³ − 2), coordinates low first. +fn mul_alpha(a: [X; 3], al: [X; 3], two: X) -> [X; 3] +where + X: Clone + core::ops::Add + core::ops::Mul, +{ + let p = |i: usize, j: usize| a[i].clone() * al[j].clone(); + [ + p(0, 0) + two.clone() * (p(1, 2) + p(2, 1)), + p(0, 1) + p(1, 0) + two * p(2, 2), + p(0, 2) + p(1, 1) + p(2, 0), + ] +} + +/// The trace for the cells at `faddr` holding `values`, and `s`. +pub fn generate_trace( + faddr: &[u64], + values: &[FEE], + alpha: FEE, + min_rows: usize, +) -> (TraceTable, FEE) { + assert_eq!(faddr.len(), values.len(), "one value per crossing cell"); + let mut trace = fill_prep(faddr, min_rows); + let s = horner(values, alpha); + let h = trace.num_rows(); + let t = &mut trace.main_table; + let mut acc = FEE::zero(); + for r in 0..h { + if let Some(v) = values.get(r) { + acc = if r == 0 { *v } else { acc * alpha + v }; + for (k, c) in v.value().iter().enumerate() { + t.set(r, cols::V0 + k, *c); + } + } + for (k, c) in acc.value().iter().enumerate() { + t.set(r, cols::ACC0 + k, *c); + } + for (k, c) in alpha.value().iter().enumerate() { + t.set(r, cols::AL0 + k, *c); + } + } + (trace, s) +} + +/// `Σ_i x_i·α^{n−1−i}`. +pub fn horner(values: &[FEE], alpha: FEE) -> FEE { + values.iter().fold(FEE::zero(), |acc, v| acc * alpha + v) +} + +/// The Merkle root of the preprocessed columns: the verifier rebuilds it from +/// the crossing cells' addresses. +pub fn commitment(faddr: &[u64], options: &ProofOptions, min_rows: usize) -> Commitment { + let trace = fill_prep(faddr, min_rows); + let columns: Vec> = (0..cols::NUM_PRECOMPUTED_COLS) + .map(|c| { + (0..trace.num_rows()) + .map(|r| *trace.main_table.get(r, c)) + .collect() + }) + .collect(); + super::prove::commit_prep(&columns, options) +} + +pub fn bus_interactions() -> Vec { + let direct = |c| BusValue::Packed { + start_column: c, + packing: Packing::Direct, + }; + vec![ + BusInteraction::sender( + BusId::FieldVmMem, + Multiplicity::Column(cols::IS_REAL), + vec![ + direct(cols::FADDR), + BusValue::constant(0), + BusValue::constant(0), + direct(cols::V0), + direct(cols::V0 + 1), + direct(cols::V0 + 2), + ], + ), + BusInteraction::sender( + BusId::FieldVmPublic, + Multiplicity::Column(cols::IS_LAST), + vec![ + BusValue::constant(CKSUM_ADDR), + direct(cols::ACC0), + direct(cols::ACC0 + 1), + direct(cols::ACC0 + 2), + ], + ), + BusInteraction::sender( + BusId::FieldVmPublic, + Multiplicity::Column(cols::IS_LAST), + vec![ + BusValue::constant(CKSUM_ALPHA_ADDR), + direct(cols::AL0), + direct(cols::AL0 + 1), + direct(cols::AL0 + 2), + ], + ), + ] +} + +/// The Horner steps under the `α` of the `AL` columns, which stay one value. +#[derive(Clone, Copy)] +pub struct CksumConstraints; + +impl ConstraintSet for CksumConstraints { + fn eval>(&self, b: &mut B) { + let col = |b: &B, row: usize, c: usize| -> [B::Expr; 3] { + core::array::from_fn(|k| b.main(row, c + k)) + }; + let acc = col(b, 0, cols::ACC0); + let v = col(b, 0, cols::V0); + let first = b.main(0, cols::IS_FIRST); + // The first row starts the sum at its cell. + for k in 0..3 { + b.emit_base(k, first.clone() * (acc[k].clone() - v[k].clone())); + } + // acc' = real'·(acc·α + v') + (1 − real')·acc. + let al = col(b, 0, cols::AL0); + let next_al = col(b, 1, cols::AL0); + let two = b.const_base(2); + let step = mul_alpha(acc.clone(), al.clone(), two); + let next_acc = col(b, 1, cols::ACC0); + let next_v = col(b, 1, cols::V0); + let real = b.main(1, cols::IS_REAL); + let idle = b.one() - real.clone(); + for k in 0..3 { + let want = real.clone() * (step[k].clone() + next_v[k].clone()) + + idle.clone() * acc[k].clone(); + b.emit_base_rows(3 + k, RowDomain::except_last(1), next_acc[k].clone() - want); + } + for k in 0..3 { + b.emit_base_rows( + 6 + k, + RowDomain::except_last(1), + next_al[k].clone() - al[k].clone(), + ); + } + } +} + +/// The guest's hash of the crossing cells, region by region as its memory +/// holds them: width-16 Poseidon1 as an overwrite sponge, the IN and BACK +/// cell counts in lanes 12 and 13, then IN's cells and BACK's, four cells +/// (twelve felts) a permutation, each region's last chunk zero-padded; the +/// digest is lanes 0..4. +pub fn crossing_digest(in_cells: &[[u64; 3]], back_cells: &[[u64; 3]]) -> [u64; 4] { + use crypto::hash::poseidon1_w16::{Fp, permute}; + let mut state = [Fp::zero(); 16]; + state[12] = Fp::from(in_cells.len() as u64); + state[13] = Fp::from(back_cells.len() as u64); + for region in [in_cells, back_cells] { + for chunk in region.chunks(4) { + for lane in &mut state[..12] { + *lane = Fp::zero(); + } + for (i, cell) in chunk.iter().enumerate() { + for (k, x) in cell.iter().enumerate() { + state[3 * i + k] = Fp::from(*x); + } + } + state = permute(state); + } + } + core::array::from_fn(|i| state[i].canonical()) +} + +/// `α` for a binding: Poseidon1 over the guest's digest and MEM's main root +/// (four little-endian words, reduced), under a domain tag; lanes 0..3. +pub fn binding_alpha(c_bin: &[u64; 4], c_fld: &Commitment) -> FEE { + use crypto::hash::poseidon1_w16::{Fp, permute}; + let mut state = [Fp::zero(); 16]; + for (i, w) in c_bin.iter().enumerate() { + state[i] = Fp::from(*w); + } + for (i, chunk) in c_fld.chunks_exact(8).enumerate() { + state[4 + i] = Fp::from(u64::from_le_bytes(chunk.try_into().expect("eight bytes"))); + } + state[12] = Fp::from(u32::from_le_bytes(*b"CKSM") as u64); + let out = permute(state); + FEE::new([out[0], out[1], out[2]]) +} + +/// The domain tag [`field_roots_digest`] starts its sponge with. +pub const ROOTS_TAG: u64 = u32::from_le_bytes(*b"CKRT") as u64; + +/// Digest the ordered roots of the non-CKSUM WHIR groups into the 32-byte +/// commitment input used by [`binding_alpha`]: width-16 Poseidon1 as an +/// overwrite sponge, the tag and the root count in lanes 12 and 13, three +/// roots (each four big-endian words, reduced: the LFM's digest of a +/// commitment) a permutation, the last chunk zero-padded; the digest is lanes +/// 0..4, little-endian. The recursion recomputes it with the LFM's `Hash16`. +pub fn field_roots_digest(roots: &[Commitment]) -> Commitment { + use crypto::hash::poseidon1_w16::{Fp, permute}; + let mut state = [Fp::zero(); 16]; + state[12] = Fp::from(ROOTS_TAG); + state[13] = Fp::from(roots.len() as u64); + for chunk in roots.chunks(3) { + for lane in &mut state[..12] { + *lane = Fp::zero(); + } + for (i, root) in chunk.iter().enumerate() { + for (k, word) in root.chunks_exact(8).enumerate() { + state[4 * i + k] = + Fp::from(u64::from_be_bytes(word.try_into().expect("eight bytes"))); + } + } + state = permute(state); + } + let mut out = [0u8; 32]; + for (lane, bytes) in state.iter().zip(out.chunks_exact_mut(8)) { + bytes.copy_from_slice(&lane.canonical().to_le_bytes()); + } + out +} + +#[cfg(test)] +mod tests { + use super::*; + use math::field::element::FieldElement; + use stark::constraints::builder::ProverEvalFolder; + use stark::frame::Frame; + use stark::table::TableView; + use stark::traits::TransitionEvaluationContext; + + const NUM_CONSTRAINTS: usize = 9; + + fn failing(trace: &TraceTable, row: usize) -> Vec { + let h = trace.num_rows(); + let get = |r: usize| -> Vec { + (0..cols::NUM_COLUMNS) + .map(|c| *trace.main_table.get(r % h, c)) + .collect() + }; + let frame = Frame::::new(vec![ + TableView::new(vec![get(row)], vec![vec![]]), + TableView::new(vec![get(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(); NUM_CONSTRAINTS]; + let mut ext = vec![FieldElement::::zero(); NUM_CONSTRAINTS]; + let mut folder = ProverEvalFolder::new(&ctx, &mut base, &mut ext); + CksumConstraints.eval(&mut folder); + let last = row + 1 == h; + base.iter() + .enumerate() + .filter(|(i, v)| **v != FE::zero() && !(last && *i >= 3)) + .map(|(i, _)| i) + .collect() + } + + fn sample(n: usize) -> (Vec, Vec, FEE) { + let values: Vec = (0..n as u64) + .map(|i| { + FEE::new([ + FE::from(3 * i + 1), + FE::from(i * i + 7), + FE::from(5 * i + 2), + ]) + }) + .collect(); + let alpha = FEE::new([FE::from(11u64), FE::from(13u64), FE::from(17u64)]); + ((0..n as u64).map(|i| 100 + 3 * i).collect(), values, alpha) + } + + #[test] + fn honest_rows_and_padding_satisfy_every_constraint() { + let (faddr, values, alpha) = sample(5); + let (trace, s) = generate_trace(&faddr, &values, alpha, 8); + assert_eq!(s, horner(&values, alpha)); + let last = trace.num_rows() - 1; + let acc: FEE = FEE::new(core::array::from_fn(|k| { + *trace.main_table.get(last, cols::ACC0 + k) + })); + assert_eq!(acc, s, "the last row holds s"); + for row in 0..trace.num_rows() { + assert_eq!(failing(&trace, row), Vec::::new(), "row {row}"); + } + } + + /// A changed cell value with the honest accumulator fails the step that + /// reads it; a changed accumulator fails too. + #[test] + fn a_changed_value_or_accumulator_fails() { + let (faddr, values, alpha) = sample(5); + let (mut trace, _) = generate_trace(&faddr, &values, alpha, 8); + let v = *trace.main_table.get(2, cols::V0); + trace.main_table.set(2, cols::V0, v + FE::one()); + assert!(!failing(&trace, 1).is_empty()); + let (mut trace, _) = generate_trace(&faddr, &values, alpha, 8); + let a = *trace.main_table.get(3, cols::ACC0 + 1); + trace.main_table.set(3, cols::ACC0 + 1, a + FE::one()); + assert!(!failing(&trace, 2).is_empty()); + } + + /// `α` changing down the table fails the step into the changed row. + #[test] + fn a_changed_alpha_fails() { + let (faddr, values, alpha) = sample(5); + let (mut trace, _) = generate_trace(&faddr, &values, alpha, 8); + let a = *trace.main_table.get(6, cols::AL0 + 2); + trace.main_table.set(6, cols::AL0 + 2, a + FE::one()); + assert!(failing(&trace, 5).contains(&8)); + } + + #[test] + fn the_constraint_count_matches_what_eval_emits() { + assert_eq!(CksumConstraints.meta().len(), NUM_CONSTRAINTS); + } + + #[test] + fn the_digest_depends_on_every_cell_and_the_count() { + let cells: Vec<[u64; 3]> = (0..9u64).map(|i| [i, i + 1, i + 2]).collect(); + let d = crossing_digest(&cells[..5], &cells[5..]); + let mut other = cells.clone(); + other[8][2] += 1; + assert_ne!(d, crossing_digest(&other[..5], &other[5..])); + assert_ne!(d, crossing_digest(&cells[..4], &cells[4..])); + assert_ne!(d, crossing_digest(&cells[..5], &cells[5..8])); + } +} diff --git a/prover/src/field_vm/decode.rs b/prover/src/field_vm/decode.rs new file mode 100644 index 000000000..a4e515be3 --- /dev/null +++ b/prover/src/field_vm/decode.rs @@ -0,0 +1,142 @@ +//! The `FIELD_VM_DECODE` chip: the program, as preprocessed columns, plus the +//! per-proof multiplicity. +//! +//! Spec: `spec/src/field_vm_decode.toml`. The four packed `ExtField` columns +//! of the spec are eleven base columns here (the `X²` part of the flags +//! column is always zero, so it is not materialized). +//! +//! Padding rows repeat the halt entry, so they add no instruction to the program. + +use stark::config::Commitment; +use stark::lookup::{BusInteraction, BusValue, Multiplicity, Packing}; +use stark::proof::options::ProofOptions; +use stark::trace::TraceTable; + +use super::air::decode_tuple; +use super::isa::{HALT_PC, Program}; +use crate::tables::types::{BusId, FE, GoldilocksExtension, GoldilocksField, zeroed_fe_vec}; + +pub const NUM_PRECOMPUTED_COLS: usize = 11; +pub const MU: usize = NUM_PRECOMPUTED_COLS; +pub const NUM_COLUMNS: usize = NUM_PRECOMPUTED_COLS + 1; + +/// At most this many DECODE tables. +pub const MAX_CHUNKS: usize = 4; + +/// `(first pc, instructions, rows)` per DECODE table. One power-of-two table +/// when it wastes at most a quarter of its rows, otherwise the largest power of +/// two that fits and the rest. `FVM_DECODE_ONE_CHUNK`: always one table, so +/// the table count and heights grow monotonically with the program (a +/// recursion's shape fixed point needs that). +pub fn chunks(program: &Program, min_rows: usize) -> Vec<(usize, usize, usize)> { + let mut plan = Vec::new(); + let (mut start, mut left) = (0, program.len()); + if std::env::var_os("FVM_DECODE_ONE_CHUNK").is_some() { + return vec![(0, left, left.next_power_of_two().max(min_rows))]; + } + loop { + let full = left.next_power_of_two().max(min_rows); + let half = full / 2; + if super::air::within_waste(left, full) + || plan.len() + 1 == MAX_CHUNKS + || half < min_rows + || half >= left + || !super::air::split_pays(left, half, program.len(), min_rows) + { + plan.push((start, left, full)); + return plan; + } + plan.push((start, half, half)); + start += half; + left -= half; + } +} + +/// One trace per chunk; `mult[pc]` executions of each address. Padding rows +/// repeat the halt entry, with zero multiplicity. +pub fn generate_traces( + program: &Program, + mult: &[u64], + min_rows: usize, +) -> Vec> { + let halt = decode_tuple(HALT_PC, &program.instrs[HALT_PC as usize]); + chunks(program, min_rows) + .into_iter() + .map(|(start, len, rows)| { + let mut trace = TraceTable::new_main(zeroed_fe_vec(rows * NUM_COLUMNS), NUM_COLUMNS, 1); + let t = &mut trace.main_table; + for row in 0..rows { + let pc = start + row; + let tuple = if row < len { + decode_tuple(pc as u64, &program.instrs[pc]) + } else { + halt + }; + for (c, v) in tuple.into_iter().enumerate() { + t.set(row, c, v); + } + if row < len { + t.set(row, MU, FE::from(mult.get(pc).copied().unwrap_or(0))); + } + } + trace + }) + .collect() +} + +pub fn bus_interactions() -> Vec { + vec![BusInteraction::receiver( + BusId::FieldVmDecode, + Multiplicity::Column(MU), + (0..NUM_PRECOMPUTED_COLS) + .map(|c| BusValue::Packed { + start_column: c, + packing: Packing::Direct, + }) + .collect(), + )] +} + +/// The program id: per DECODE table, the Merkle root over the LDE of its +/// preprocessed columns, committed the way the prover commits the trace. +pub fn program_commitment( + program: &Program, + options: &ProofOptions, + min_rows: usize, +) -> Vec { + generate_traces(program, &[], min_rows) + .iter() + .map(|trace| { + let columns: Vec> = (0..NUM_PRECOMPUTED_COLS) + .map(|c| { + (0..trace.num_rows()) + .map(|r| *trace.main_table.get(r, c)) + .collect() + }) + .collect(); + crate::field_vm::prove::commit_prep(&columns, options) + }) + .collect() +} + +/// [`program_commitment`] under the trace trees' leaf `layout`. +pub fn program_commitment_for( + program: &Program, + options: &ProofOptions, + min_rows: usize, + layout: stark::leaf_layout::LeafLayout, +) -> Vec { + generate_traces(program, &[], min_rows) + .iter() + .map(|trace| { + let columns: Vec> = (0..NUM_PRECOMPUTED_COLS) + .map(|c| { + (0..trace.num_rows()) + .map(|r| *trace.main_table.get(r, c)) + .collect() + }) + .collect(); + crate::field_vm::prove::commit_prep_with(&columns, options, layout) + }) + .collect() +} diff --git a/prover/src/field_vm/executor.rs b/prover/src/field_vm/executor.rs new file mode 100644 index 000000000..36345d7fe --- /dev/null +++ b/prover/src/field_vm/executor.rs @@ -0,0 +1,403 @@ +//! Field VM executor. +//! +//! Produces one [`Step`] per trace row. Row `i` holds the state instruction +//! `pc_i` acts on, *after* that instruction's input hints were applied; the +//! instruction's `d` argument reads row `i + 1`. +//! +//! `MEM` is read-only for the proof, but its contents are chosen by the prover: +//! a `d` argument that dereferences a cell nobody has fixed yet defines it as +//! `a * b + c`. Any other read of an unfixed cell is an error. +//! +//! Hints are resolved in this order: +//! - output hint, `d` a register expression with `imm0 != 0`: solved for the +//! register; the halt loop's input hints are all zero; +//! - a single input hint whose instruction is linear in it (e.g. `INV`): solved; +//! - anything else: asked to the [`HintOracle`]. + +use super::isa::{ + Arg, HALT_PC, Instr, N, NUM_REGS, Program, REG_PC, REG_ZERO, START_PC, gpr, gpr_index, +}; +use crate::tables::types::{FE, FEE}; + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct State { + pub zero: bool, + pub pc: u64, + pub regs: [FEE; N], +} + +impl State { + pub fn initial() -> Self { + Self { + zero: false, + pc: START_PC, + regs: [FEE::zero(); N], + } + } + + /// All registers in register-index order. + pub fn all_regs(&self) -> [FEE; NUM_REGS] { + let mut all = [FEE::zero(); NUM_REGS]; + all[REG_ZERO as usize] = if self.zero { FEE::one() } else { FEE::zero() }; + all[REG_PC as usize] = FEE::from(self.pc); + all[2..].copy_from_slice(&self.regs); + all + } +} + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct Step { + pub state: State, + pub args_premem: [FEE; 4], + pub args: [FEE; 4], +} + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum HintKind { + Output, + Input, +} + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct HintRequest { + pub kind: HintKind, + pub pc: u64, + pub reg: u8, + /// For an output hint, the value `a * b + c` that `d` must equal. + pub target: Option, +} + +pub trait HintOracle { + fn hint(&mut self, req: &HintRequest) -> Option; +} + +impl Option> HintOracle for F { + fn hint(&mut self, req: &HintRequest) -> Option { + self(req) + } +} + +pub struct NoHints; + +impl HintOracle for NoHints { + fn hint(&mut self, _: &HintRequest) -> Option { + None + } +} + +#[derive(Clone, Debug, PartialEq, Eq)] +pub enum ExecError { + PcOutOfRange { pc: u64, target: FEE }, + BadAddress { pc: u64, addr: FEE }, + UninitializedRead { pc: u64, addr: u64 }, + FmaViolation { pc: u64 }, + HintCollision { pc: u64, reg: u8 }, + UnresolvedHint { pc: u64, reg: u8 }, + StepLimit, +} + +#[derive(Clone, Debug)] +pub struct Memory { + cells: Vec>, + mult: Vec, +} + +impl Memory { + pub fn new(size: usize) -> Self { + Self { + cells: vec![None; size], + mult: vec![0; size], + } + } + + /// A memory whose first cells are `init` (e.g. the proof being verified). + pub fn with_init(size: usize, init: &[FEE]) -> Self { + assert!(init.len() <= size); + let mut mem = Self::new(size); + for (cell, v) in mem.cells.iter_mut().zip(init) { + *cell = Some(*v); + } + mem + } + + pub fn len(&self) -> usize { + self.cells.len() + } + + pub fn is_empty(&self) -> bool { + self.cells.is_empty() + } + + pub fn get(&self, addr: usize) -> Option { + self.cells[addr] + } + + fn addr(&self, pc: u64, v: &FEE) -> Result { + let [c0, c1, c2] = v.value(); + let a = c0.canonical(); + if *c1 != FE::zero() || *c2 != FE::zero() || a >= self.cells.len() as u64 { + return Err(ExecError::BadAddress { pc, addr: *v }); + } + Ok(a as usize) + } + + fn peek(&self, pc: u64, addr: &FEE) -> Result, ExecError> { + Ok(self.cells[self.addr(pc, addr)?]) + } + + fn read(&mut self, pc: u64, addr: &FEE) -> Result { + let a = self.addr(pc, addr)?; + let v = self.cells[a].ok_or(ExecError::UninitializedRead { pc, addr: a as u64 })?; + self.mult[a] += 1; + Ok(v) + } + + /// Reads `MEM[addr]`, defining it as `v` if nothing fixed it yet. + fn read_or_define(&mut self, pc: u64, addr: &FEE, v: FEE) -> Result { + let a = self.addr(pc, addr)?; + let cell = *self.cells[a].get_or_insert(v); + self.mult[a] += 1; + Ok(cell) + } +} + +#[derive(Clone, Debug)] +pub struct Execution { + /// One step per executed instruction, ending with the first halt step. + pub steps: Vec, + /// Final memory contents; cells never fixed read as zero. + pub mem: Vec, + /// Number of lookups into each memory cell. + pub mem_mult: Vec, + /// Number of executed steps per program address. + pub decode_mult: Vec, +} + +fn arg_value( + pc: u64, + arg: &Arg, + regs: &[FEE; NUM_REGS], + mem: &mut Memory, +) -> Result<(FEE, FEE), ExecError> { + let premem = arg.premem(regs); + let v = if arg.mem { + mem.read(pc, &premem)? + } else { + premem + }; + Ok((premem, v)) +} + +/// `d - (a * b + c)` for `instr` with general-purpose register `g` set to `x`, +/// assuming no output hint (the future state keeps `x`). `None` when a memory +/// argument is not fixed, or its address depends on `x`. +fn residual_at(instr: &Instr, state: &State, g: usize, x: FEE, mem: &Memory) -> Option { + let mut cur = *state; + cur.regs[g] = x; + let regs = cur.all_regs(); + let mut next = cur; + next.pc += 1; + let next_regs = next.all_regs(); + let value = |arg: &Arg, regs: &[FEE; NUM_REGS]| -> Option { + let premem = arg.premem(regs); + if !arg.mem { + return Some(premem); + } + if gpr_index(arg.reg) == Some(g) && arg.scale != FE::zero() { + return None; + } + mem.peek(state.pc, &premem).ok().flatten() + }; + if instr.d.reg == REG_ZERO && instr.d.scale != FE::zero() { + return None; + } + let d = value(&instr.d, &next_regs)?; + let a = value(&instr.a, ®s)?; + let b = value(&instr.b, ®s)?; + let c = value(&instr.c, ®s)?; + Some(d - (a * b + c)) +} + +/// Solves the single input-hinted register `g` of `instr` when the +/// constraint is linear in it. +fn solve_input_hint(instr: &Instr, state: &State, g: usize, mem: &Memory) -> Option { + if instr.hint_out { + return None; + } + let f0 = residual_at(instr, state, g, FEE::zero(), mem)?; + let f1 = residual_at(instr, state, g, FEE::one(), mem)?; + let f2 = residual_at(instr, state, g, FEE::from(2u64), mem)?; + let two = FEE::from(2u64); + let quad = (f2 - f1 * two + f0) * two.inv().ok()?; + if quad != FEE::zero() { + return None; + } + let lin = f1 - f0; + Some(-f0 * lin.inv().ok()?) +} + +fn instr_at(program: &Program, pc: u64, target: FEE) -> Result<&Instr, ExecError> { + program + .instrs + .get(pc as usize) + .ok_or(ExecError::PcOutOfRange { pc, target }) +} + +/// Applies `instr`'s input hints to `state`, which it is about to act on. +fn apply_input_hints( + instr: &Instr, + state: &mut State, + mem: &Memory, + oracle: &mut dyn HintOracle, +) -> Result<(), ExecError> { + if !instr.hint_in.contains(&true) { + return Ok(()); + } + let hinted: Vec = (0..N).filter(|&g| instr.hint_in[g]).collect(); + if state.pc == HALT_PC { + state.regs = [FEE::zero(); N]; + return Ok(()); + } + let solved = match hinted.as_slice() { + [g] => solve_input_hint(instr, state, *g, mem).map(|x| (*g, x)), + _ => None, + }; + for g in hinted { + let x = match solved { + Some((sg, x)) if sg == g => x, + _ => oracle + .hint(&HintRequest { + kind: HintKind::Input, + pc: state.pc, + reg: gpr(g), + target: None, + }) + .ok_or(ExecError::UnresolvedHint { + pc: state.pc, + reg: gpr(g), + })?, + }; + state.regs[g] = x; + } + Ok(()) +} + +pub fn execute( + program: &Program, + mem: Memory, + oracle: &mut dyn HintOracle, + max_steps: usize, +) -> Result { + run(program, mem, oracle, max_steps, None) +} + +/// [`execute`] going on past FMA violations, with the PC of each: a witness +/// that breaks constraints, for proving it anyway. +#[cfg(test)] +pub(crate) fn execute_violating( + program: &Program, + mem: Memory, + oracle: &mut dyn HintOracle, + max_steps: usize, +) -> Result<(Execution, Vec), ExecError> { + let mut violations = Vec::new(); + let exec = run(program, mem, oracle, max_steps, Some(&mut violations))?; + Ok((exec, violations)) +} + +fn run( + program: &Program, + mut mem: Memory, + oracle: &mut dyn HintOracle, + max_steps: usize, + mut violations: Option<&mut Vec>, +) -> Result { + let mut decode_mult = vec![0u64; program.len()]; + let mut steps = Vec::new(); + let mut cur = State::initial(); + + loop { + if steps.len() >= max_steps { + return Err(ExecError::StepLimit); + } + let pc = cur.pc; + let instr = *instr_at(program, pc, FEE::from(pc))?; + let regs = cur.all_regs(); + + let (a_pre, a) = arg_value(pc, &instr.a, ®s, &mut mem)?; + let (b_pre, b) = arg_value(pc, &instr.b, ®s, &mut mem)?; + let (c_pre, c) = arg_value(pc, &instr.c, ®s, &mut mem)?; + let target = a * b + c; + + let mut next = cur; + next.pc = pc + 1; + let d = instr.d; + if instr.hint_out { + let solved = if !d.mem && d.scale != FE::zero() { + Some( + (target - d.offset.to_extension()) + * d.scale.inv().expect("nonzero").to_extension(), + ) + } else { + oracle.hint(&HintRequest { + kind: HintKind::Output, + pc, + reg: d.reg, + target: Some(target), + }) + } + .ok_or(ExecError::UnresolvedHint { pc, reg: d.reg })?; + match gpr_index(d.reg) { + Some(g) => next.regs[g] = solved, + None => { + let [c0, c1, c2] = solved.value(); + if *c1 != FE::zero() || *c2 != FE::zero() { + return Err(ExecError::PcOutOfRange { pc, target: solved }); + } + next.pc = c0.canonical(); + } + } + } + + let next_instr = *instr_at(program, next.pc, FEE::from(next.pc))?; + if let Some(g) = gpr_index(d.reg) + && next_instr.hint_in[g] + { + return Err(ExecError::HintCollision { pc, reg: d.reg }); + } + apply_input_hints(&next_instr, &mut next, &mem, oracle)?; + + let d_pre = d.premem(&next.all_regs()); + let d_val = if d.mem { + mem.read_or_define(pc, &d_pre, target)? + } else { + d_pre + }; + if d_val != target { + match violations.as_deref_mut() { + Some(v) => v.push(pc), + None => return Err(ExecError::FmaViolation { pc }), + } + } + next.zero = d_val == FEE::zero(); + + decode_mult[pc as usize] += 1; + steps.push(Step { + state: cur, + args_premem: [d_pre, a_pre, b_pre, c_pre], + args: [d_val, a, b, c], + }); + if pc == HALT_PC { + break; + } + cur = next; + } + + let mem_vals = mem.cells.iter().map(|c| c.unwrap_or(FEE::zero())).collect(); + Ok(Execution { + steps, + mem: mem_vals, + mem_mult: mem.mult, + decode_mult, + }) +} diff --git a/prover/src/field_vm/generic_fold.rs b/prover/src/field_vm/generic_fold.rs new file mode 100644 index 000000000..7e1d9e0e0 --- /dev/null +++ b/prover/src/field_vm/generic_fold.rs @@ -0,0 +1,466 @@ +//! Shape-independent Field VM driver for WHIR's lean coset fold. + +use super::asm::{Asm, Label}; +use super::isa::{Arg, Program, REG_PC, gpr}; +use crate::tables::types::{FE, FEE, GoldilocksField}; + +const ALPHAS: usize = 8; +const FACTORS: i64 = 14; +const ETAS: i64 = 46; +const ROUND_STRIDE: usize = ETAS as usize + 6 * 32; +const QUERY_BITS: usize = 32; +const OUTPUT_CELLS: usize = 6 * 64; +const WORK_CELLS: usize = OUTPUT_CELLS; + +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct FoldRound { + pub domain_log: usize, + pub block: usize, + /// The lean fold's `half_alpha` values, one per level. + pub alphas: Vec, + pub queries: Vec<(u64, Vec, FEE)>, +} + +/// Data memory for [`kernel`]. The returned prefix is initialized; the trailing +/// workspaces must be left uninitialized in `Memory`, since the VM defines them. +pub fn layout(rounds: &[FoldRound]) -> Vec { + validate_rounds(rounds); + let mut mem = vec![FEE::zero(); 2 + rounds.len() * ROUND_STRIDE]; + for r in rounds { + for (index, values, _) in &r.queries { + assert_eq!(values.len(), r.block); + assert!( + (*index >> r.domain_log) == 0, + "query index exceeds domain bits" + ); + } + } + let headers_end = mem.len(); + let mut query_bases = Vec::with_capacity(rounds.len()); + let mut all_queries = Vec::new(); + for r in rounds { + query_bases.push(mem.len()); + let stride = QUERY_BITS + r.block + 1; + for (index, values, claimed) in &r.queries { + for i in 0..QUERY_BITS { + mem.push(if i < r.domain_log && ((index >> i) & 1) != 0 { + FEE::one() + } else { + FEE::zero() + }); + } + mem.extend(values.iter().copied()); + mem.push(*claimed); + } + all_queries.push((stride, r.queries.len())); + } + let mut workspace_base = mem.len(); + for (i, r) in rounds.iter().enumerate() { + let h = 2 + i * ROUND_STRIDE; + let (record_stride, qcount) = all_queries[i]; + mem[h] = FEE::from(query_bases[i] as u64); + mem[h + 1] = FEE::from(qcount as u64); + mem[h + 2] = FEE::from(record_stride as u64); + mem[h + 3] = FEE::from(workspace_base as u64); + mem[h + 4] = FEE::from(WORK_CELLS as u64); + mem[h + 5] = FEE::from(r.block as u64); + mem[h + 6] = FEE::from(r.domain_log as u64); + mem[h + 7] = FE::from(2u64) + .inv() + .expect("2 is invertible") + .to_extension(); + for (level, alpha) in r.alphas.iter().enumerate() { + mem[h + ALPHAS + level] = *alpha; + } + + let generator = domain_generator(r.domain_log); + let generator_inv = generator.inv().expect("domain generator is nonzero"); + for i in 0..32 { + let f = if i < r.domain_log { + generator_inv.pow(1u64 << i) + } else { + FE::one() + }; + mem[h + FACTORS as usize + i] = (f - FE::one()).to_extension(); + } + let mut current_len = r.block; + for level in 0..r.alphas.len() { + let eta_inv = generator_inv.pow((1usize << r.domain_log) as u64 / current_len as u64); + for t in 0..32 { + let eta_t = if t < current_len / 2 { + eta_inv.pow(t as u64).to_extension() + } else { + FEE::zero() + }; + mem[h + ETAS as usize + level * 32 + t] = eta_t; + } + current_len /= 2; + } + workspace_base += r.queries.len() * WORK_CELLS; + } + mem[0] = FEE::from(headers_end as u64); + mem +} + +/// A single program supports all blocks 2..=64 (powers of two), domain logs +/// through 32, any number of rounds, and any query count. +pub fn kernel() -> Program { + build_kernel() +} + +fn build_kernel() -> Program { + // Generate fixed code for every supported block. The only runtime-varying + // values (alphas, roots, bits, queries) are read from the round header/data. + let mut a = Asm::new(); + // Keep only the three long-lived pointers and two working values in + // registers. The fifth GPR is the sole scratch register. Unused workspace + // cells hold the query end and per-level inverse-point values. + let (rp, qp, wp, x, tmp) = (gpr(0), gpr(1), gpr(2), gpr(3), gpr(4)); + let round = a.label(); + let query = a.label(); + let query_done = a.label(); + let round_done = a.label(); + let halt = a.label(); + a.mov(Arg::reg(rp), Arg::imm(2)); + a.bind(round); + a.sub(Arg::reg(x), Arg::reg(rp), Arg::mem_abs(0)); + a.jump_zero(halt); + a.mov(Arg::reg(qp), Arg::mem(rp, 0)); + // Workspace cell 383 is beyond every fold output. Copy the round's + // one-past-the-end query pointer into each query's workspace as we advance. + // Skip this for empty rounds, which have no workspace. + a.sub(Arg::reg(x), Arg::mem(rp, 1), Arg::imm(0)); + a.jump_zero(round_done); + a.mov(Arg::reg(wp), Arg::mem(rp, 3)); + a.fma( + Arg::mem(wp, 383), + Arg::mem(rp, 1), + Arg::mem(rp, 2), + Arg::mem(rp, 0), + ); + a.bind(query); + + let dispatch = a.here(); + a.mov(Arg::reg(x), Arg::mem(rp, 5)); + let table_pc = dispatch + 2; + a.fma_out( + Arg::reg(REG_PC), + Arg::imm(0), + Arg::imm(0), + Arg::lin(x, 1, table_pc as i64), + ); + let table: Vec