diff --git a/CHANGELOG.md b/CHANGELOG.md index b69bb3f1a2..387d708dd6 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,4 +1,12 @@ # Changelog +## v0.30.0 (Unreleased) + +#### Features + +- Added `trace`, `trace.CONST`, and `trace.event("...")` assembly as syntactic sugar for emitting optional read-only trace events ([#3478](https://github.com/0xMiden/miden-vm/pull/3478)). +#### Changes + +- [BREAKING] Reduced the precompile STARK relation from 12 AIRs to 10 by merging the chunk/node/sponge and EC point/group stores ([#3464](https://github.com/0xMiden/miden-vm/pull/3464)). ## v0.29.0 (2026-08-04) diff --git a/Cargo.lock b/Cargo.lock index e925b839c4..32d7a5ac07 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2053,7 +2053,7 @@ checksum = "cf8baf1c55e62ffcace7a9f06f4bd9cd3f0c4beb022d3b367256b91b87513d98" [[package]] name = "miden-ace-codegen" -version = "0.29.0" +version = "0.30.0" dependencies = [ "miden-constraint-compiler", "miden-core", @@ -2063,7 +2063,7 @@ dependencies = [ [[package]] name = "miden-air" -version = "0.29.0" +version = "0.30.0" dependencies = [ "insta", "miden-ace-codegen", @@ -2080,7 +2080,7 @@ dependencies = [ [[package]] name = "miden-assembly" -version = "0.29.0" +version = "0.30.0" dependencies = [ "env_logger", "insta", @@ -2100,7 +2100,7 @@ dependencies = [ [[package]] name = "miden-assembly-syntax" -version = "0.29.0" +version = "0.30.0" dependencies = [ "env_logger", "log", @@ -2124,7 +2124,7 @@ dependencies = [ [[package]] name = "miden-assembly-syntax-cst" -version = "0.29.0" +version = "0.30.0" dependencies = [ "miden-debug-types", "miden-rowan", @@ -2135,7 +2135,7 @@ dependencies = [ [[package]] name = "miden-bench" -version = "0.29.0" +version = "0.30.0" dependencies = [ "clap", "miden-lifted-stark", @@ -2165,7 +2165,7 @@ dependencies = [ [[package]] name = "miden-constraint-compiler" -version = "0.29.0" +version = "0.30.0" dependencies = [ "miden-core", "miden-crypto", @@ -2173,7 +2173,7 @@ dependencies = [ [[package]] name = "miden-core" -version = "0.29.0" +version = "0.30.0" dependencies = [ "criterion", "derive_more", @@ -2197,7 +2197,7 @@ dependencies = [ [[package]] name = "miden-core-lib" -version = "0.29.0" +version = "0.30.0" dependencies = [ "criterion", "env_logger", @@ -2225,7 +2225,7 @@ dependencies = [ [[package]] name = "miden-core-lib-codegen" -version = "0.29.0" +version = "0.30.0" dependencies = [ "miden-core", "miden-precompiles", @@ -2233,7 +2233,7 @@ dependencies = [ [[package]] name = "miden-crypto" -version = "0.29.0" +version = "0.30.0" dependencies = [ "assert_matches", "blake3", @@ -2283,7 +2283,7 @@ dependencies = [ [[package]] name = "miden-crypto-derive" -version = "0.29.0" +version = "0.30.0" dependencies = [ "miden-field", "quote", @@ -2292,7 +2292,7 @@ dependencies = [ [[package]] name = "miden-crypto-smt-codspeed-bench" -version = "0.29.0" +version = "0.30.0" dependencies = [ "codspeed-criterion-compat", "miden-crypto", @@ -2301,7 +2301,7 @@ dependencies = [ [[package]] name = "miden-crypto-wycheproof-tests" -version = "0.29.0" +version = "0.30.0" dependencies = [ "ed25519-dalek", "hex", @@ -2315,7 +2315,7 @@ dependencies = [ [[package]] name = "miden-debug-types" -version = "0.29.0" +version = "0.30.0" dependencies = [ "memchr", "miden-crypto", @@ -2335,7 +2335,7 @@ dependencies = [ [[package]] name = "miden-field" -version = "0.29.0" +version = "0.30.0" dependencies = [ "miden-serde-utils", "num-bigint 0.5.1", @@ -2354,7 +2354,7 @@ dependencies = [ [[package]] name = "miden-format" -version = "0.29.0" +version = "0.30.0" dependencies = [ "clap", "miden-assembly-syntax-cst", @@ -2378,7 +2378,7 @@ dependencies = [ [[package]] name = "miden-lifted-air" -version = "0.29.0" +version = "0.30.0" dependencies = [ "miden-field", "p3-air", @@ -2391,7 +2391,7 @@ dependencies = [ [[package]] name = "miden-lifted-stark" -version = "0.29.0" +version = "0.30.0" dependencies = [ "criterion", "miden-lifted-air", @@ -2422,7 +2422,7 @@ dependencies = [ [[package]] name = "miden-mast-package" -version = "0.29.0" +version = "0.30.0" dependencies = [ "hashbrown 0.17.1", "log", @@ -2478,7 +2478,7 @@ dependencies = [ [[package]] name = "miden-package-registry" -version = "0.29.0" +version = "0.30.0" dependencies = [ "miden-assembly-syntax", "miden-core", @@ -2494,7 +2494,7 @@ dependencies = [ [[package]] name = "miden-package-registry-local" -version = "0.29.0" +version = "0.30.0" dependencies = [ "clap", "miden-assembly-syntax", @@ -2511,7 +2511,7 @@ dependencies = [ [[package]] name = "miden-precompiles" -version = "0.29.0" +version = "0.30.0" dependencies = [ "miden-core", "miden-crypto", @@ -2519,7 +2519,7 @@ dependencies = [ [[package]] name = "miden-precompiles-prover" -version = "0.29.0" +version = "0.30.0" dependencies = [ "insta", "k256", @@ -2542,7 +2542,7 @@ dependencies = [ [[package]] name = "miden-processor" -version = "0.29.0" +version = "0.30.0" dependencies = [ "hashbrown 0.17.1", "insta", @@ -2569,7 +2569,7 @@ dependencies = [ [[package]] name = "miden-project" -version = "0.29.0" +version = "0.30.0" dependencies = [ "miden-assembly-syntax", "miden-core", @@ -2588,7 +2588,7 @@ dependencies = [ [[package]] name = "miden-prover" -version = "0.29.0" +version = "0.30.0" dependencies = [ "miden-air", "miden-assembly", @@ -2615,7 +2615,7 @@ dependencies = [ [[package]] name = "miden-serde-utils" -version = "0.29.0" +version = "0.30.0" dependencies = [ "p3-field", "p3-goldilocks", @@ -2625,7 +2625,7 @@ dependencies = [ [[package]] name = "miden-stark-transcript" -version = "0.29.0" +version = "0.30.0" dependencies = [ "p3-challenger", "p3-field", @@ -2635,7 +2635,7 @@ dependencies = [ [[package]] name = "miden-stateful-hasher" -version = "0.29.0" +version = "0.30.0" dependencies = [ "p3-bn254", "p3-field", @@ -2646,7 +2646,7 @@ dependencies = [ [[package]] name = "miden-test-serde-macros" -version = "0.29.0" +version = "0.30.0" dependencies = [ "proc-macro2", "proptest", @@ -2658,7 +2658,7 @@ dependencies = [ [[package]] name = "miden-test-utils" -version = "0.29.0" +version = "0.30.0" dependencies = [ "env_logger", "miden-air", @@ -2677,7 +2677,7 @@ dependencies = [ [[package]] name = "miden-utils-core-derive" -version = "0.29.0" +version = "0.30.0" dependencies = [ "proc-macro2", "quote", @@ -2686,7 +2686,7 @@ dependencies = [ [[package]] name = "miden-utils-diagnostics" -version = "0.29.0" +version = "0.30.0" dependencies = [ "miden-debug-types", "miden-miette", @@ -2695,7 +2695,7 @@ dependencies = [ [[package]] name = "miden-utils-indexing" -version = "0.29.0" +version = "0.30.0" dependencies = [ "miden-serde-utils", "miden-test-serde-macros", @@ -2707,7 +2707,7 @@ dependencies = [ [[package]] name = "miden-utils-sync" -version = "0.29.0" +version = "0.30.0" dependencies = [ "lock_api", "loom", @@ -2717,7 +2717,7 @@ dependencies = [ [[package]] name = "miden-verifier" -version = "0.29.0" +version = "0.30.0" dependencies = [ "miden-air", "miden-core", @@ -2732,7 +2732,7 @@ dependencies = [ [[package]] name = "miden-vm" -version = "0.29.0" +version = "0.30.0" dependencies = [ "assert_cmd", "clap", @@ -2761,7 +2761,7 @@ dependencies = [ [[package]] name = "miden-vm-blake3-bench" -version = "0.29.0" +version = "0.30.0" dependencies = [ "clap", "codspeed-criterion-compat", @@ -2776,7 +2776,7 @@ dependencies = [ [[package]] name = "miden-vm-precompiles-bench" -version = "0.29.0" +version = "0.30.0" dependencies = [ "codspeed-criterion-compat", "miden-core", @@ -2788,7 +2788,7 @@ dependencies = [ [[package]] name = "miden-vm-synthetic-bench" -version = "0.29.0" +version = "0.30.0" dependencies = [ "codspeed-criterion-compat", "miden-assembly", @@ -2805,7 +2805,7 @@ dependencies = [ [[package]] name = "midenc-hir-type" -version = "0.10.0" +version = "0.11.0" dependencies = [ "miden-formatting", "miden-serde-utils", diff --git a/Cargo.toml b/Cargo.toml index 95ede4f893..e14cc4709b 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -59,7 +59,7 @@ rust-version = "1.96.1" # Private workspace members inherit this version. Publishable crates keep their # own package versions so release tooling can publish only the crates selected # for a release. -version = "0.29.0" +version = "0.30.0" [profile.optimized] inherits = "release" @@ -81,39 +81,39 @@ opt-level = 0 [workspace.dependencies] # Workspace crates -miden-ace-codegen = { path = "./crates/ace-codegen", version = "0.29", default-features = false } -miden-air = { path = "./air", version = "0.29", default-features = false } -miden-assembly = { path = "./crates/assembly", version = "0.29", default-features = false } -miden-assembly-syntax = { path = "./crates/assembly-syntax", version = "0.29", default-features = false } -miden-assembly-syntax-cst = { path = "./crates/assembly-syntax-cst", version = "0.29", default-features = false } -miden-constraint-compiler = { path = "./crates/miden-constraint-compiler", version = "0.29", default-features = false } -miden-core = { path = "./core", version = "0.29", default-features = false } -miden-crypto = { path = "./crates/crypto", version = "0.29", default-features = false } -miden-crypto-derive = { path = "./crates/crypto-derive", version = "0.29", default-features = false } -miden-debug-types = { path = "./crates/debug-types", version = "0.29", default-features = false } -miden-field = { path = "./crates/field", version = "0.29", default-features = false } -miden-lifted-air = { path = "./crates/lifted-air", version = "0.29", default-features = false } -miden-lifted-stark = { path = "./crates/lifted-stark", version = "0.29", default-features = false } -miden-mast-package = { path = "./crates/mast-package", version = "0.29", default-features = false } -miden-package-registry = { path = "./crates/package-registry", version = "0.29", default-features = false } -miden-precompiles = { path = "./crates/precompiles", version = "0.29", default-features = false } -miden-precompiles-prover = { path = "./crates/precompiles-prover", version = "0.29", default-features = false } -miden-core-lib-codegen = { path = "./crates/lib/core/codegen", version = "0.29", default-features = false } -miden-processor = { path = "./processor", version = "0.29", default-features = false } +miden-ace-codegen = { path = "./crates/ace-codegen", version = "0.30", default-features = false } +miden-air = { path = "./air", version = "0.30", default-features = false } +miden-assembly = { path = "./crates/assembly", version = "0.30", default-features = false } +miden-assembly-syntax = { path = "./crates/assembly-syntax", version = "0.30", default-features = false } +miden-assembly-syntax-cst = { path = "./crates/assembly-syntax-cst", version = "0.30", default-features = false } +miden-constraint-compiler = { path = "./crates/miden-constraint-compiler", version = "0.30", default-features = false } +miden-core = { path = "./core", version = "0.30", default-features = false } +miden-crypto = { path = "./crates/crypto", version = "0.30", default-features = false } +miden-crypto-derive = { path = "./crates/crypto-derive", version = "0.30", default-features = false } +miden-debug-types = { path = "./crates/debug-types", version = "0.30", default-features = false } +miden-field = { path = "./crates/field", version = "0.30", default-features = false } +miden-lifted-air = { path = "./crates/lifted-air", version = "0.30", default-features = false } +miden-lifted-stark = { path = "./crates/lifted-stark", version = "0.30", default-features = false } +miden-mast-package = { path = "./crates/mast-package", version = "0.30", default-features = false } +miden-package-registry = { path = "./crates/package-registry", version = "0.30", default-features = false } +miden-precompiles = { path = "./crates/precompiles", version = "0.30", default-features = false } +miden-precompiles-prover = { path = "./crates/precompiles-prover", version = "0.30", default-features = false } +miden-core-lib-codegen = { path = "./crates/lib/core/codegen", version = "0.30", default-features = false } +miden-processor = { path = "./processor", version = "0.30", default-features = false } miden-test-serde-macros = { path = "./crates/test-serde-macros", default-features = false } -miden-project = { path = "./crates/project", version = "0.29", default-features = false } -miden-prover = { path = "./prover", version = "0.29", default-features = false } -miden-core-lib = { path = "./crates/lib/core", version = "0.29", default-features = false } -miden-serde-utils = { path = "./crates/serde-utils", version = "0.29", default-features = false } -miden-stark-transcript = { path = "./crates/stark-transcript", version = "0.29", default-features = false } -miden-stateful-hasher = { path = "./crates/stateful-hasher", version = "0.29", default-features = false } -midenc-hir-type = { path = "./crates/midenc-hir-type", version = "0.10", default-features = false } -miden-utils-core-derive = { path = "./crates/utils-core-derive", version = "0.29", default-features = false } -miden-utils-diagnostics = { path = "./crates/utils-diagnostics", version = "0.29", default-features = false } -miden-utils-indexing = { path = "./crates/utils-indexing", version = "0.29", default-features = false } -miden-utils-sync = { path = "./crates/utils-sync", version = "0.29", default-features = false } +miden-project = { path = "./crates/project", version = "0.30", default-features = false } +miden-prover = { path = "./prover", version = "0.30", default-features = false } +miden-core-lib = { path = "./crates/lib/core", version = "0.30", default-features = false } +miden-serde-utils = { path = "./crates/serde-utils", version = "0.30", default-features = false } +miden-stark-transcript = { path = "./crates/stark-transcript", version = "0.30", default-features = false } +miden-stateful-hasher = { path = "./crates/stateful-hasher", version = "0.30", default-features = false } +midenc-hir-type = { path = "./crates/midenc-hir-type", version = "0.11", default-features = false } +miden-utils-core-derive = { path = "./crates/utils-core-derive", version = "0.30", default-features = false } +miden-utils-diagnostics = { path = "./crates/utils-diagnostics", version = "0.30", default-features = false } +miden-utils-indexing = { path = "./crates/utils-indexing", version = "0.30", default-features = false } +miden-utils-sync = { path = "./crates/utils-sync", version = "0.30", default-features = false } miden-utils-testing = { path = "./crates/test-utils", package = "miden-test-utils" } -miden-verifier = { path = "./verifier", version = "0.29", default-features = false } +miden-verifier = { path = "./verifier", version = "0.30", default-features = false } # Miden crates miden-formatting = { version = "0.1", default-features = false } diff --git a/air/Cargo.toml b/air/Cargo.toml index 6c1dc42a53..356cc4c2d5 100644 --- a/air/Cargo.toml +++ b/air/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "miden-air" -version = "0.29.0" +version = "0.30.0" description = "Algebraic intermediate representation of Miden VM processor" documentation = "https://docs.rs/miden-air" readme = "README.md" diff --git a/air/src/constraints/chiplets/memory.rs b/air/src/constraints/chiplets/memory.rs index 882adb068e..7f830ba3c1 100644 --- a/air/src/constraints/chiplets/memory.rs +++ b/air/src/constraints/chiplets/memory.rs @@ -256,7 +256,7 @@ mod tests { use miden_core::{ Felt, - field::{PrimeCharacteristicRing, QuadFelt}, + field::{Field, PrimeCharacteristicRing, QuadFelt}, }; use miden_crypto::stark::{ air::{AirBuilder, ExtensionBuilder, PermutationAirBuilder, RowWindow}, @@ -395,13 +395,21 @@ mod tests { row.chiplets[19] = Felt::new_unchecked(hi); } - fn eval_memory_constraints(row: &ChipletCols) -> Vec { - let next = memory_row(); + fn eval_memory_window( + local: &ChipletCols, + next: &ChipletCols, + flags: &ChipletFlags, + ) -> Vec { let mut builder = ConstraintEvalBuilder::new(); - enforce_memory_constraints(&mut builder, row, &next, &memory_flags()); + enforce_memory_constraints(&mut builder, local, next, flags); builder.evaluations } + fn eval_memory_constraints(row: &ChipletCols) -> Vec { + let next = memory_row(); + eval_memory_window(row, &next, &memory_flags()) + } + fn assert_constraints_accept(row: &ChipletCols) { let evaluations = eval_memory_constraints(row); assert!( @@ -435,6 +443,167 @@ mod tests { assert_constraints_reject(&invalid); } + // SAME-CLOCK ACCESS TESTS + // ============================================================================================ + + #[derive(Clone, Copy, Debug)] + enum AccessType { + Read, + Write, + } + + impl AccessType { + fn is_read(self) -> Felt { + match self { + Self::Read => Felt::ONE, + Self::Write => Felt::ZERO, + } + } + } + + #[derive(Clone, Copy, Debug)] + enum AccessSize { + Element(u8), + Word, + } + + fn set_access_size(row: &mut ChipletCols, size: AccessSize) { + let cols = memory_cols(row); + match size { + AccessSize::Element(index) => { + assert!(index < 4, "element index must be in the range 0..4"); + cols.is_word = Felt::ZERO; + cols.idx0 = Felt::new_unchecked(u64::from(index & 1)); + cols.idx1 = Felt::new_unchecked(u64::from(index >> 1)); + }, + AccessSize::Word => { + cols.is_word = Felt::ONE; + cols.idx0 = Felt::ZERO; + cols.idx1 = Felt::ZERO; + }, + } + } + + fn same_key_memory_rows( + local_access: AccessType, + next_access: AccessType, + ) -> (ChipletCols, ChipletCols) { + let mut local = memory_row(); + let mut next = memory_row(); + let values = [ + Felt::new_unchecked(1), + Felt::new_unchecked(2), + Felt::new_unchecked(3), + Felt::new_unchecked(4), + ]; + + for (row, access) in [(&mut local, local_access), (&mut next, next_access)] { + let cols = memory_cols(row); + cols.is_read = access.is_read(); + cols.is_word = Felt::ONE; + cols.word_addr = Felt::new_unchecked(4); + cols.clk = Felt::new_unchecked(7); + cols.values = values; + } + memory_cols(&mut next).is_same_ctx_and_addr = Felt::ONE; + + // word_addr = 4 * (w0 + 2^16 * w1), with (w0, w1) = (1, 0). + set_word_addr_limbs(&mut local, 1, 0); + set_word_addr_limbs(&mut next, 1, 0); + + (local, next) + } + + fn eval_memory_transition( + local: &ChipletCols, + next: &ChipletCols, + ) -> Vec { + let flags = ChipletFlags { + is_active: Felt::ONE, + is_transition: Felt::ONE, + is_last: Felt::ZERO, + next_is_first: Felt::ZERO, + }; + eval_memory_window(local, next, &flags) + } + + /// Ensures that repeating `(ctx, word_addr, clk)` is valid only when both accesses are reads. + /// In particular, this prevents overlapping multi-memory operations such as `crypto_stream` + /// from reading and writing the same word in one clock cycle. + #[test] + fn same_key_memory_rows_allow_only_reads() { + for (local_access, next_access) in [ + (AccessType::Read, AccessType::Read), + (AccessType::Read, AccessType::Write), + (AccessType::Write, AccessType::Read), + (AccessType::Write, AccessType::Write), + ] { + let (local, next) = same_key_memory_rows(local_access, next_access); + let evaluations = eval_memory_transition(&local, &next); + let accepted = evaluations.iter().all(|value| *value == QuadFelt::ZERO); + let should_accept = + matches!((local_access, next_access), (AccessType::Read, AccessType::Read)); + assert_eq!( + accepted, should_accept, + "unexpected result for {local_access:?}/{next_access:?}", + ); + } + } + + /// Repeating `(ctx, word_addr, clk)` is safe for any combination of read access sizes. This is + /// required when operations such as `horner_eval_base` or ACE read multiple elements from the + /// same word in one clock cycle. + #[test] + fn same_key_memory_rows_allow_all_read_access_sizes() { + for (local_size, next_size) in [ + (AccessSize::Word, AccessSize::Word), + (AccessSize::Word, AccessSize::Element(2)), + (AccessSize::Element(1), AccessSize::Word), + (AccessSize::Element(0), AccessSize::Element(1)), + ] { + let (mut local, mut next) = same_key_memory_rows(AccessType::Read, AccessType::Read); + set_access_size(&mut local, local_size); + set_access_size(&mut next, next_size); + + let evaluations = eval_memory_transition(&local, &next); + assert!( + evaluations.iter().all(|value| *value == QuadFelt::ZERO), + "same-clock {local_size:?}/{next_size:?} reads should be accepted; got \ + {evaluations:?}", + ); + } + } + + /// Same-clock accesses at different word addresses may contain reads or writes. This covers the + /// two distinct word accesses emitted by operations such as `mem_stream` and `adv_pipe`. + #[test] + fn same_clock_memory_rows_at_different_addresses_allow_reads_and_writes() { + for (local_access, next_access) in [ + (AccessType::Read, AccessType::Read), + (AccessType::Read, AccessType::Write), + (AccessType::Write, AccessType::Read), + (AccessType::Write, AccessType::Write), + ] { + let (local, mut next) = same_key_memory_rows(local_access, next_access); + { + let next = memory_cols(&mut next); + next.word_addr = Felt::new_unchecked(8); + next.values = [Felt::ZERO; 4]; + next.d0 = Felt::new_unchecked(4); + next.d_inv = Felt::new_unchecked(4).inverse(); + next.is_same_ctx_and_addr = Felt::ZERO; + } + set_word_addr_limbs(&mut next, 2, 0); + + let evaluations = eval_memory_transition(&local, &next); + assert!( + evaluations.iter().all(|value| *value == QuadFelt::ZERO), + "same-clock accesses to different words should be accepted for \ + {local_access:?}/{next_access:?}; got {evaluations:?}", + ); + } + } + // EMPTY-SECTION BOUNDARY REGRESSION TESTS // ============================================================================================ // The memory chiplet's first-row initialization ("values not being written must be zero") is @@ -463,16 +632,6 @@ mod tests { build_chiplet_selectors(&mut builder, local, next).memory } - fn eval_memory_window( - local: &ChipletCols, - next: &ChipletCols, - flags: &ChipletFlags, - ) -> Vec { - let mut builder = ConstraintEvalBuilder::new(); - enforce_memory_constraints(&mut builder, local, next, flags); - builder.evaluations - } - #[test] fn memory_first_row_init_enforced_when_bitwise_empty() { // Empty-bitwise layout: the memory section begins directly after a controller row, so the diff --git a/core/Cargo.toml b/core/Cargo.toml index 3e89f9cd29..8db1161d9c 100644 --- a/core/Cargo.toml +++ b/core/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "miden-core" -version = "0.29.0" +version = "0.30.0" description = "Miden VM core components" documentation = "https://docs.rs/miden-core" readme = "README.md" diff --git a/core/src/events/sys_events.rs b/core/src/events/sys_events.rs index 1d523a06f4..2f5d1f7466 100644 --- a/core/src/events/sys_events.rs +++ b/core/src/events/sys_events.rs @@ -413,13 +413,14 @@ pub enum SystemEvent { // -------------------------------------------------------------------------------------------- /// Signals an optional, read-only trace event to the host. /// - /// When `emit` observes this system event ID at stack position 0, the VM forwards the user - /// trace event ID at stack position 1 to the host's trace handler. This is typically emitted - /// as `push. push. emit`. Trace handlers can observe - /// the processor state, but cannot mutate VM state or the advice provider. If no handler is - /// registered for the user trace event ID, the event is a no-op. - /// - /// Hosts are expected to not raise an error if they encounter a `user_trace_id` for which no + /// Assembly programs emit trace events with `trace`, `trace.CONST`, or `trace.event("...")`. + /// When the underlying `emit` observes this system event ID at stack position 0, the VM + /// forwards the user trace event ID at stack position 1 to the host's trace handler. The + /// immediate form lowers to `push. push. emit drop drop`. + /// Trace handlers can observe the processor state, but cannot mutate VM state or the advice + /// provider. If no handler is registered for the user trace event ID, the event is a no-op. + /// + /// Hosts are expected not to raise an error if they encounter a `user_trace_id` for which no /// trace handler is registered. /// /// Inputs: diff --git a/core/src/operations/mod.rs b/core/src/operations/mod.rs index f3df6736d2..36afb0f112 100644 --- a/core/src/operations/mod.rs +++ b/core/src/operations/mod.rs @@ -174,7 +174,8 @@ pub enum Operation { /// assembly (`emit.event("...")` or `emit.CONST` where `CONST=event("...")`). /// - System events are identified by reserved [`SystemEvent`](crate::events::SystemEvent) IDs. /// Most are handled by the VM; `SystemEvent::TraceEvent` triggers the host's optional - /// read-only trace handler for the trace event id at stack position 1. + /// read-only trace handler for the trace event id at stack position 1. Assembly exposes this + /// through `trace`, `trace.CONST`, and `trace.event("...")`. /// - Any non system event ID is forwarded to the host's regular event handler. /// /// This operation does not change the state of the user stack aside from reading the value. diff --git a/crates/ace-codegen/Cargo.toml b/crates/ace-codegen/Cargo.toml index ae8134556f..0c8d316684 100644 --- a/crates/ace-codegen/Cargo.toml +++ b/crates/ace-codegen/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "miden-ace-codegen" -version = "0.29.0" +version = "0.30.0" description = "ACE circuit codegen for Plonky3-based Miden AIRs." documentation = "https://docs.rs/miden-ace-codegen" readme = "README.md" diff --git a/crates/assembly-syntax-cst/Cargo.toml b/crates/assembly-syntax-cst/Cargo.toml index c53c189891..f93081fc64 100644 --- a/crates/assembly-syntax-cst/Cargo.toml +++ b/crates/assembly-syntax-cst/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "miden-assembly-syntax-cst" -version = "0.29.0" +version = "0.30.0" description = "Lossless concrete syntax tree support for the Miden Assembly language" documentation = "https://docs.rs/miden-assembly-syntax-cst" readme = "README.md" diff --git a/crates/assembly-syntax/Cargo.toml b/crates/assembly-syntax/Cargo.toml index b33e950109..875a94b57a 100644 --- a/crates/assembly-syntax/Cargo.toml +++ b/crates/assembly-syntax/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "miden-assembly-syntax" -version = "0.29.0" +version = "0.30.0" description = "Parsing and semantic analysis of the Miden Assembly language" documentation = "https://docs.rs/miden-assembly-syntax" readme = "README.md" diff --git a/crates/assembly-syntax/src/ast/instruction/mod.rs b/crates/assembly-syntax/src/ast/instruction/mod.rs index 604af74f63..d1beb07ba6 100644 --- a/crates/assembly-syntax/src/ast/instruction/mod.rs +++ b/crates/assembly-syntax/src/ast/instruction/mod.rs @@ -287,6 +287,10 @@ pub enum Instruction { // ----- event decorators -------------------------------------------------------------------- Emit, EmitImm(ImmFelt), + + // ----- traces (read-only events) ----------------------------------------------------------- + Trace, + TraceImm(ImmFelt), } impl Instruction { diff --git a/crates/assembly-syntax/src/ast/instruction/print.rs b/crates/assembly-syntax/src/ast/instruction/print.rs index 394252eec2..00c6b8073c 100644 --- a/crates/assembly-syntax/src/ast/instruction/print.rs +++ b/crates/assembly-syntax/src/ast/instruction/print.rs @@ -337,6 +337,18 @@ impl PrettyPrint for Instruction { Self::Emit => const_text("emit"), Self::EmitImm(value) => inst_with_felt_imm("emit", value), + // ----- traces (read-only events) ---------------------------------------------------- + Self::Trace => const_text("trace"), + // `trace.` is invalid syntax, so to support a `print -> parse` round trip + // we print the equivalent `push. trace drop` sequence instead. + Self::TraceImm(value) => { + let value = match value { + Immediate::Value(value) => display(*value), + Immediate::Constant(name) => text(name), + }; + flatten(const_text("push") + const_text(".") + value + const_text(" trace drop")) + }, + // Handled by the early return for !has_textual_representation() Self::DebugVar(_) => unreachable!(), } diff --git a/crates/assembly-syntax/src/ast/tests.rs b/crates/assembly-syntax/src/ast/tests.rs index 68cfc78b2f..ba2e3ae6b2 100644 --- a/crates/assembly-syntax/src/ast/tests.rs +++ b/crates/assembly-syntax/src/ast/tests.rs @@ -1,5 +1,6 @@ use alloc::{string::ToString, vec::Vec}; +use miden_core::events::EventId; use miden_debug_types::{SourceSpan, Span}; use miden_utils_diagnostics::Report; use pretty_assertions::assert_eq; @@ -1622,6 +1623,65 @@ end assert_eq!(&formatted, expected); } +/// `TraceImm` is printed as the equivalent `push. trace drop` sequence, since `trace.` +/// is not valid syntax. +#[test] +fn test_trace_roundtrip_formatting() { + let trace_name = "test::trace::roundtrip"; + let trace_id = EventId::from_name(trace_name).as_felt(); + + let source = format!( + "\ +begin + push.1 + trace + drop + trace.event(\"{trace_name}\") +end +" + ); + + let context = SyntaxTestContext::default(); + let source = source_file!(&context, source); + let module = context.parse_program_source_file(source).unwrap_or_else(|err| panic!("{err}")); + let formatted = module.to_string(); + let expected = format!( + "\ +namespace $exec + +begin + push.1 + trace + drop + push.{trace_id} trace drop +end +" + ); + assert_eq!(&formatted, &expected); + + // The printed output must parse back. + let source = source_file!(&context, &expected); + let reparsed = context.parse_program_source_file(source).unwrap_or_else(|err| panic!("{err}")); + let expanded = format!( + "\ +namespace $exec + +begin + push.1 + trace + drop + push.{trace_id} + trace + drop +end +" + ); + let source = source_file!(&context, &expanded); + let expanded_module = + context.parse_program_source_file(source).unwrap_or_else(|err| panic!("{err}")); + assert_eq!(reparsed, expanded_module); +} + #[test] fn cannot_mem_store_word() { let context = SyntaxTestContext::default(); diff --git a/crates/assembly-syntax/src/ast/visit.rs b/crates/assembly-syntax/src/ast/visit.rs index 8eab36a781..ee80ff943e 100644 --- a/crates/assembly-syntax/src/ast/visit.rs +++ b/crates/assembly-syntax/src/ast/visit.rs @@ -476,7 +476,7 @@ where | MemStoreImm(imm) | MemStoreWBeImm(imm) | MemStoreWLeImm(imm) => visitor.visit_immediate_u32(imm), - EmitImm(imm) => visitor.visit_immediate_felt(imm), + EmitImm(imm) | TraceImm(imm) => visitor.visit_immediate_felt(imm), SysEvent(sys_event) => visitor.visit_system_event(Span::new(span, sys_event)), Exec(target) => visitor.visit_exec(target), Call(target) => visitor.visit_call(target), @@ -505,7 +505,7 @@ where | MemStoreWLe | MemStream | AdvPipe | AdvPush | AdvPushW | AdvLoadW | Hash | HMerge | HPerm | MTreeGet | MTreeSet | MTreeMerge | MTreeVerify | FriExt2Fold4 | DynExec | DynCall | DebugVar(_) | HornerBase | HornerExt | CryptoStream | EvalCircuit - | LogDeferred | Emit => ControlFlow::Continue(()), + | LogDeferred | Emit | Trace => ControlFlow::Continue(()), } } @@ -1040,7 +1040,7 @@ where | MemStoreImm(imm) | MemStoreWBeImm(imm) | MemStoreWLeImm(imm) => visitor.visit_mut_immediate_u32(imm), - EmitImm(imm) => visitor.visit_mut_immediate_felt(imm), + EmitImm(imm) | TraceImm(imm) => visitor.visit_mut_immediate_felt(imm), SysEvent(sys_event) => visitor.visit_mut_system_event(Span::new(span, sys_event)), Exec(target) => visitor.visit_mut_exec(target), Call(target) => visitor.visit_mut_call(target), @@ -1069,7 +1069,7 @@ where | MemStoreWLe | MemStream | AdvPipe | AdvPush | AdvPushW | AdvLoadW | Hash | HMerge | HPerm | MTreeGet | MTreeSet | MTreeMerge | MTreeVerify | FriExt2Fold4 | DynExec | DynCall | DebugVar(_) | HornerBase | HornerExt | EvalCircuit | CryptoStream - | LogDeferred | Emit => ControlFlow::Continue(()), + | LogDeferred | Emit | Trace => ControlFlow::Continue(()), } } diff --git a/crates/assembly-syntax/src/parser/cst/instructions.rs b/crates/assembly-syntax/src/parser/cst/instructions.rs index efdd2ffa36..49782ec7b2 100644 --- a/crates/assembly-syntax/src/parser/cst/instructions.rs +++ b/crates/assembly-syntax/src/parser/cst/instructions.rs @@ -377,6 +377,10 @@ static PRIMITIVE_SPECS: &[PrimitiveSpec] = &[ spelling: "emit", build: || Instruction::Emit, }, + PrimitiveSpec { + spelling: "trace", + build: || Instruction::Trace, + }, PrimitiveSpec { spelling: "eval_circuit", build: || Instruction::EvalCircuit, @@ -1207,7 +1211,12 @@ fn lower_extended_instruction( lower_invocation_instruction(context, span, &tokens, build) }, - ExtendedInstructionKind::Emit => lower_emit_instruction(context, span, &tokens), + ExtendedInstructionKind::Emit => { + lower_event_imm_instruction(context, span, &tokens, "emit", Instruction::EmitImm) + }, + ExtendedInstructionKind::Trace => { + lower_event_imm_instruction(context, span, &tokens, "trace", Instruction::TraceImm) + }, ExtendedInstructionKind::ErrorCode(build) => { lower_error_code_instruction(context, span, &tokens, spec.keyword, build) }, @@ -1224,6 +1233,7 @@ enum ExtendedInstructionKind { Push, Invocation(fn(ast::InvocationTarget) -> Instruction), Emit, + Trace, ErrorCode(fn(ast::ErrorMsg) -> Instruction), } @@ -1252,6 +1262,10 @@ static EXTENDED_INSTRUCTION_SPECS: &[ExtendedInstructionSpec] = &[ keyword: "emit", kind: ExtendedInstructionKind::Emit, }, + ExtendedInstructionSpec { + keyword: "trace", + kind: ExtendedInstructionKind::Trace, + }, ExtendedInstructionSpec { keyword: "assert", kind: ExtendedInstructionKind::ErrorCode(Instruction::AssertWithError), @@ -1343,15 +1357,17 @@ fn lower_invocation_instruction( Ok(Some(vec![inst_op(instruction_span, build(target))])) } -/// Lowers `emit.` and `emit.event("name")`. -fn lower_emit_instruction( +/// Lowers `emit.` / `emit.event("name")` and `trace.` / `trace.event("name")`. +fn lower_event_imm_instruction( context: &mut LoweringContext<'_>, instruction_span: SourceSpan, tokens: &[SyntaxToken], + keyword: &str, + builder: fn(ast::ImmFelt) -> Instruction, ) -> Result>, ParsingError> { if tokens.len() < 3 || tokens[0].kind() != SyntaxKind::Ident - || tokens[0].text() != "emit" + || tokens[0].text() != keyword || tokens[1].kind() != SyntaxKind::Dot { return Ok(None); @@ -1360,10 +1376,7 @@ fn lower_emit_instruction( match &tokens[2..] { [name] if name.kind() == SyntaxKind::Ident && name.text() != "event" => { let name = context.lower_constant_ident_token(name)?; - Ok(Some(vec![inst_op( - instruction_span, - Instruction::EmitImm(Immediate::Constant(name)), - )])) + Ok(Some(vec![inst_op(instruction_span, builder(Immediate::Constant(name)))])) }, [event, lparen, string, rparen] if event.kind() == SyntaxKind::Ident @@ -1376,7 +1389,7 @@ fn lower_emit_instruction( let event_id = EventId::from_name(value.as_ref()).as_felt(); Ok(Some(vec![inst_op( instruction_span, - Instruction::EmitImm(Immediate::Value(Span::new(instruction_span, event_id))), + builder(Immediate::Value(Span::new(instruction_span, event_id))), )])) }, _ => Ok(None), diff --git a/crates/assembly-syntax/src/parser/tests.rs b/crates/assembly-syntax/src/parser/tests.rs index 1ea91baa00..6f80e8a635 100644 --- a/crates/assembly-syntax/src/parser/tests.rs +++ b/crates/assembly-syntax/src/parser/tests.rs @@ -640,6 +640,7 @@ begin adv.insert_hdword adv.push_mapvaln emit + trace mem_load u32div add.1 @@ -751,6 +752,8 @@ begin procref.foo::bar emit.EVENT_ID emit.event(\"abc\") + trace.EVENT_ID + trace.event(\"abc\") assert.err=\"oops\" u32assert.err=ERR_CODE end diff --git a/crates/assembly-syntax/src/sema/passes/const_eval.rs b/crates/assembly-syntax/src/sema/passes/const_eval.rs index 746316ed12..db315e5f39 100644 --- a/crates/assembly-syntax/src/sema/passes/const_eval.rs +++ b/crates/assembly-syntax/src/sema/passes/const_eval.rs @@ -143,20 +143,23 @@ where } fn visit_mut_inst(&mut self, inst: &mut Span) -> ControlFlow<()> { use crate::ast::Instruction; - if let Instruction::EmitImm(Immediate::Constant(name)) = &**inst { + if let Instruction::EmitImm(Immediate::Constant(name)) + | Instruction::TraceImm(Immediate::Constant(name)) = &**inst + { let span = name.span(); match self.env.get(name) { Ok(Some( CachedConstantValue::Miss(ConstantExpr::Hash(HashKind::Event, _)) | CachedConstantValue::Hit(ConstantValue::Hash(HashKind::Event, _)), )) => { - // CHANGE: allow `emit.EVENT` when `EVENT` was defined via + // CHANGE: allow `emit.EVENT` / `trace.EVENT` when `EVENT` was defined via // const.EVENT = event("...") // NOTE: This function only validates the kind; the actual resolution to a Felt // happens below in `visit_mut_immediate_felt` just like other Felt immediates. // Enabled syntax: // const.EVT = event("...") // emit.EVT + // trace.EVT }, Ok(Some(CachedConstantValue::Miss(expr @ ConstantExpr::Var(_)))) => { // A reference to another constant was used, try to evaluate the expression @@ -181,12 +184,15 @@ where } }, Ok(Some(_)) => { - // CHANGE: disallow `emit.CONST` unless CONST is defined via `event("...")`. + // CHANGE: disallow `emit.CONST` / `trace.CONST` unless CONST is defined via + // `event("...")`. // Examples which now error: // const.BAD = 42 // emit.BAD + // trace.BAD // const.W = word("foo") // emit.W + // trace.W self.errors.push( ConstEvalError::InvalidConstant { span, diff --git a/crates/assembly/Cargo.toml b/crates/assembly/Cargo.toml index fb28258e3e..7c467608c4 100644 --- a/crates/assembly/Cargo.toml +++ b/crates/assembly/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "miden-assembly" -version = "0.29.0" +version = "0.30.0" description = "Miden VM assembly language" documentation = "https://docs.rs/miden-assembly" readme = "README.md" diff --git a/crates/assembly/src/instruction/mod.rs b/crates/assembly/src/instruction/mod.rs index fe062421ff..53409222ec 100644 --- a/crates/assembly/src/instruction/mod.rs +++ b/crates/assembly/src/instruction/mod.rs @@ -6,6 +6,7 @@ use miden_assembly_syntax::{ }; use miden_core::{ Felt, WORD_SIZE, ZERO, + events::SystemEvent, operations::{AssemblyOp, Operation}, }; @@ -601,6 +602,28 @@ impl Assembler { let event_id_value = event_id.expect_value(); block_builder.push_ops([Push(event_id_value), Emit, Drop]); }, + + // trace: reads the trace ID from the top of the stack and expands to + // `push., emit, drop`, leaving the stack unchanged. + Instruction::Trace => { + // The trace ID is already on the stack. In addition we need the system event which + // triggers traces. + let sys_event_id = SystemEvent::TraceEvent.event_id().as_felt(); + block_builder.push_ops([Push(sys_event_id), Emit, Drop]); + }, + // trace.: expands to + // `push., push., emit, drop, drop`, leaving the stack unchanged. + Instruction::TraceImm(trace_id) => { + let trace_id_value = trace_id.expect_value(); + let sys_event_id = SystemEvent::TraceEvent.event_id().as_felt(); + block_builder.push_ops([ + Push(trace_id_value), + Push(sys_event_id), + Emit, + Drop, + Drop, + ]); + }, } Ok(None) diff --git a/crates/assembly/src/tests.rs b/crates/assembly/src/tests.rs index 2a103ab87a..ca9e210e23 100644 --- a/crates/assembly/src/tests.rs +++ b/crates/assembly/src/tests.rs @@ -3855,7 +3855,7 @@ pub proc foo exec.::test::mod1::bar end" Ok(()) } -// EMIT EVENT SYNTAX VALIDATION +// EVENT SYNTAX VALIDATION // ================================================================================================ #[test] @@ -3897,6 +3897,45 @@ fn emit_const_must_be_event_hash() { .expect_err(r#"emit.CONST should require const defined via event("...")"#); } +#[test] +fn trace_u32_immediate_is_rejected() { + let context = TestContext::new(); + let program_source = r#" + begin + trace.32 + end + "#; + context + .assemble(program_source) + .expect_err(r#"trace. should be rejected; only event("...") is allowed"#); +} + +#[test] +fn trace_const_must_be_event_hash() { + let context = TestContext::new(); + // CONST defined as plain number should not be accepted by trace.CONST + let program_source = r#" + const BAD = 100 + begin + trace.BAD + end + "#; + context + .assemble(program_source) + .expect_err(r#"trace.CONST should require const defined via event("...")"#); + + // CONST defined via word("...") should also be rejected by trace.CONST + let program_source = r#" + const BADW = word("foo") + begin + trace.BADW + end + "#; + context + .assemble(program_source) + .expect_err(r#"trace.CONST should require const defined via event("...")"#); +} + #[test] #[should_panic(expected = "expected 3 lines, but got 1")] fn assert_diagnostic_lines_rejects_missing_actual_lines() { @@ -4140,6 +4179,43 @@ fn emit_instruction_digest() { assert_ne!(procedure_digests[1], procedure_digests[2]); } +/// Ensures that the arguments of `trace` do indeed modify the digest of a basic block. +#[test] +fn trace_instruction_digest() { + let context = TestContext::new(); + + let program_source = r#" + const EVT1 = event("miden::test::trace_one") + const EVT2 = event("miden::test::trace_two") + + proc foo + trace.EVT1 + end + + proc bar + trace.EVT2 + end + + begin + # specific impl irrelevant + exec.foo + exec.bar + end + "#; + + let program = context.assemble(program_source).unwrap(); + + let procedure_digests: Vec = program.mast_forest().procedure_digests().collect(); + + // foo, bar and entrypoint + assert_eq!(3, procedure_digests.len()); + + // Ensure that foo, bar and entrypoint all have different digests + assert_ne!(procedure_digests[0], procedure_digests[1]); + assert_ne!(procedure_digests[0], procedure_digests[2]); + assert_ne!(procedure_digests[1], procedure_digests[2]); +} + /// Tests that emitting events with immediate values has the same MAST representation /// regardless of whether using emit.value or push.value emit syntax #[test] @@ -4190,6 +4266,66 @@ fn emit_syntax_equivalence() { assert_eq!(program3.num_procedures(), 1); } +/// Tests that trace events have the same MAST representation regardless of whether the trace ID +/// is provided as a constant, inline event name, stack value, or fully expanded event sequence. +#[test] +fn trace_syntax_equivalence() { + let context = TestContext::new(); + + // First program uses a constant. + let program1_source = r#" + const EVT = event("miden::test::trace_equiv") + begin + trace.EVT + end + "#; + + // Second program uses inline trace.event("..."). + let program2_source = r#" + begin + trace.event("miden::test::trace_equiv") + end + "#; + + // Third program provides the trace ID on the stack. + let program3_source = r#" + const EVT = event("miden::test::trace_equiv") + begin + push.EVT + trace + drop + end + "#; + + // Fourth program uses the fully expanded trace event sequence. + let program4_source = r#" + const EVT = event("miden::test::trace_equiv") + const SYS_TRACE = event("sys::trace_event") + begin + push.EVT + push.SYS_TRACE + emit + drop + drop + end + "#; + + let program1 = context.assemble(program1_source).unwrap(); + let program2 = context.assemble(program2_source).unwrap(); + let program3 = context.assemble(program3_source).unwrap(); + let program4 = context.assemble(program4_source).unwrap(); + + let digest1 = program1.hash(); + assert_eq!(digest1, program2.hash(), "constant and inline trace forms differ"); + assert_eq!(digest1, program3.hash(), "immediate and stack trace forms differ"); + assert_eq!(digest1, program4.hash(), "trace and expanded emit forms differ"); + + assert_eq!(program1.num_procedures(), 1); + assert_eq!(program2.num_procedures(), 1); + assert_eq!(program3.num_procedures(), 1); + assert_eq!(program4.num_procedures(), 1); +} + /// Since `foo` and `bar` have the same body, we only expect them to be added once to the program. #[test] fn duplicate_procedure() { diff --git a/crates/crypto-derive/Cargo.toml b/crates/crypto-derive/Cargo.toml index 1f2e562ed8..a66d86194c 100644 --- a/crates/crypto-derive/Cargo.toml +++ b/crates/crypto-derive/Cargo.toml @@ -9,7 +9,7 @@ name = "miden-crypto-derive" readme = "README.md" repository.workspace = true rust-version.workspace = true -version = "0.29.0" +version = "0.30.0" [lib] doctest = false diff --git a/crates/crypto/Cargo.toml b/crates/crypto/Cargo.toml index 5200732c52..fd5ffa18c8 100644 --- a/crates/crypto/Cargo.toml +++ b/crates/crypto/Cargo.toml @@ -10,7 +10,7 @@ name = "miden-crypto" readme.workspace = true repository.workspace = true rust-version.workspace = true -version = "0.29.0" +version = "0.30.0" [[bin]] bench = false diff --git a/crates/debug-types/Cargo.toml b/crates/debug-types/Cargo.toml index f633adecf8..606e5a1d53 100644 --- a/crates/debug-types/Cargo.toml +++ b/crates/debug-types/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "miden-debug-types" -version = "0.29.0" +version = "0.30.0" description = "Core source-level debugging information types used throughout the Miden toolchain" documentation = "https://docs.rs/miden-debug-types" readme = "README.md" diff --git a/crates/field/Cargo.toml b/crates/field/Cargo.toml index 6ee9062cda..e2c1511f5a 100644 --- a/crates/field/Cargo.toml +++ b/crates/field/Cargo.toml @@ -10,7 +10,7 @@ name = "miden-field" readme = "README.md" repository.workspace = true rust-version.workspace = true -version = "0.29.0" +version = "0.30.0" [lib] crate-type = ["rlib"] diff --git a/crates/lib/core/Cargo.toml b/crates/lib/core/Cargo.toml index 340e39151b..bd78fcb122 100644 --- a/crates/lib/core/Cargo.toml +++ b/crates/lib/core/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "miden-core-lib" -version = "0.29.0" +version = "0.30.0" description = "Miden VM core library" documentation = "https://docs.rs/miden-core-lib" readme = "README.md" diff --git a/crates/lib/core/asm/miden-project.toml b/crates/lib/core/asm/miden-project.toml index bec8bbb71f..4bf7e5c036 100644 --- a/crates/lib/core/asm/miden-project.toml +++ b/crates/lib/core/asm/miden-project.toml @@ -1,13 +1,13 @@ [package] name = "miden-core" -version = "0.29.0" +version = "0.30.0" [lib] namespace = "miden::core" path = "mod.masm" [dependencies] -miden-precompiles = { version = "0.29", linkage = "dynamic" } +miden-precompiles = { version = "0.30", linkage = "dynamic" } [profile.release] # Always produce debug information, as it can be stripped later by the VM diff --git a/crates/lifted-air/Cargo.toml b/crates/lifted-air/Cargo.toml index f66151035b..f3f74e7edc 100644 --- a/crates/lifted-air/Cargo.toml +++ b/crates/lifted-air/Cargo.toml @@ -7,7 +7,7 @@ name = "miden-lifted-air" readme.workspace = true repository.workspace = true rust-version.workspace = true -version = "0.29.0" +version = "0.30.0" [lib] doctest = true diff --git a/crates/lifted-stark/Cargo.toml b/crates/lifted-stark/Cargo.toml index 207a8a8bee..3a4ec84af8 100644 --- a/crates/lifted-stark/Cargo.toml +++ b/crates/lifted-stark/Cargo.toml @@ -7,7 +7,7 @@ name = "miden-lifted-stark" readme = "README.md" repository.workspace = true rust-version.workspace = true -version = "0.29.0" +version = "0.30.0" [lib] doctest = false diff --git a/crates/lifted-stark/src/lib.rs b/crates/lifted-stark/src/lib.rs index e7aaa49aa8..4f31451fa1 100644 --- a/crates/lifted-stark/src/lib.rs +++ b/crates/lifted-stark/src/lib.rs @@ -78,9 +78,10 @@ pub mod verifier; pub use config::{GenericStarkConfig, StarkConfig}; pub use debug::check_constraints; -// `domain` and `order` are internal modules, but these error types surface through the public -// `ProverError` / `VerifierError`, so they need a public path of their own. -pub use domain::DomainError; +// `domain` and `order` are internal modules. Their error types surface through the public +// `ProverError` / `VerifierError`, and quotient-degree derivation is part of the relation +// configuration contract, so these items need public paths of their own. +pub use domain::{DomainError, log_quotient_degree}; pub use order::ShapeError; pub use preprocessed::{Preprocessed, PreprocessedValidationError}; pub use prover::{ProverError, ProverInstance}; diff --git a/crates/mast-package/Cargo.toml b/crates/mast-package/Cargo.toml index 376b3efbee..943cbc80e7 100644 --- a/crates/mast-package/Cargo.toml +++ b/crates/mast-package/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "miden-mast-package" -version = "0.29.0" +version = "0.30.0" description = "Package containing a compiled Miden MAST artifact with declared dependencies and exports" documentation = "https://docs.rs/miden-mast-package" readme = "README.md" diff --git a/crates/mast-package/src/package/manifest.rs b/crates/mast-package/src/package/manifest.rs index d95910feff..3e6e4de3d9 100644 --- a/crates/mast-package/src/package/manifest.rs +++ b/crates/mast-package/src/package/manifest.rs @@ -55,6 +55,10 @@ pub struct PackageManifest { pub(super) modules: BTreeMap, PackageModule>, /// The libraries (packages) linked against by this package, which must be provided when /// executing the program. + #[cfg_attr( + any(test, feature = "arbitrary"), + proptest(strategy = "arbitrary_dependencies()") + )] pub(super) dependencies: Vec, /// The (optional) entrypoint function for this package, if it is executable #[cfg_attr(any(test, feature = "arbitrary"), proptest(value = "None"))] @@ -673,6 +677,19 @@ impl fmt::Debug for TypeExport { } } +#[cfg(any(test, feature = "arbitrary"))] +fn arbitrary_dependencies() -> impl Strategy> { + proptest::collection::vec(any::(), 0..10).prop_filter( + "package dependencies must have unique ids", + |dependencies| { + use alloc::collections::BTreeSet; + + let mut seen = BTreeSet::new(); + dependencies.iter().all(|dependency| seen.insert(dependency.id().clone())) + }, + ) +} + fn normalize_export(export: &mut PackageExport) -> Result<(), ManifestValidationError> { let canonical_path = canonicalize_export_path(export.path().as_ref())?; diff --git a/crates/miden-constraint-compiler/Cargo.toml b/crates/miden-constraint-compiler/Cargo.toml index e186a2c8bb..de723d03f0 100644 --- a/crates/miden-constraint-compiler/Cargo.toml +++ b/crates/miden-constraint-compiler/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "miden-constraint-compiler" -version = "0.29.0" +version = "0.30.0" description = "Constraint compiler for Plonky3-based Miden AIRs." documentation = "https://docs.rs/miden-constraint-compiler" readme = "README.md" diff --git a/crates/miden-format/Cargo.toml b/crates/miden-format/Cargo.toml index 1bb31a4f83..42f90c63d9 100644 --- a/crates/miden-format/Cargo.toml +++ b/crates/miden-format/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "miden-format" -version = "0.29.0" +version = "0.30.0" description = "Formatter for the Miden Assembly language" documentation = "https://docs.rs/miden-format" readme = "README.md" diff --git a/crates/midenc-hir-type/Cargo.toml b/crates/midenc-hir-type/Cargo.toml index 652b18773c..c78095dd8b 100644 --- a/crates/midenc-hir-type/Cargo.toml +++ b/crates/midenc-hir-type/Cargo.toml @@ -1,7 +1,7 @@ [package] name = "midenc-hir-type" description = "Type system and utilities for Miden HIR" -version = "0.10.0" +version = "0.11.0" rust-version.workspace = true authors.workspace = true repository.workspace = true diff --git a/crates/package-registry-local/Cargo.toml b/crates/package-registry-local/Cargo.toml index 4a53cb0c5a..82c20a0803 100644 --- a/crates/package-registry-local/Cargo.toml +++ b/crates/package-registry-local/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "miden-package-registry-local" -version = "0.29.0" +version = "0.30.0" description = "Filesystem-backed local package registry for Miden packages" documentation = "https://docs.rs/miden-package-registry-local" readme = "README.md" diff --git a/crates/package-registry/Cargo.toml b/crates/package-registry/Cargo.toml index 82cd29f715..ba21c9eefe 100644 --- a/crates/package-registry/Cargo.toml +++ b/crates/package-registry/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "miden-package-registry" -version = "0.29.0" +version = "0.30.0" description = "Package registry interfaces and dependency resolution for Miden packages" documentation = "https://docs.rs/miden-package-registry" readme = "README.md" diff --git a/crates/precompiles-prover/src/ace.rs b/crates/precompiles-prover/src/ace.rs index 0a6fa14b83..5898c5471e 100644 --- a/crates/precompiles-prover/src/ace.rs +++ b/crates/precompiles-prover/src/ace.rs @@ -7,50 +7,122 @@ use alloc::vec::Vec; -use miden_ace_codegen::{AceCircuit, AceConfig, AceError, build_multi_air_ace_circuit}; -use miden_core::field::QuadFelt; +use miden_ace_codegen::{AceCircuit, AceConfig, AceError, LayoutKind, build_multi_air_ace_circuit}; +use miden_core::{Felt, field::QuadFelt}; -use crate::session::ChipletAir; +use crate::session::{ChipletAir, NUM_CHIPLETS}; // MULTI-AIR ACE CIRCUIT // ================================================================================================ +/// Per-AIR trace regions are padded to this width before concatenation, matching the LMCS wire +/// alignment used by the commitment scheme. +const LMCS_ALIGNMENT: usize = 8; + +/// Number of quotient chunks the precompile relation commits to. +/// +/// The lifted STARK verifier derives this quantity symbolically from the AIRs. Deriving it through +/// the same implementation keeps the ACE circuit's READ layout coupled to the proof protocol. +fn num_quotient_chunks() -> usize { + let max_log_quotient_degree = ChipletAir::all() + .iter() + .map(miden_lifted_stark::log_quotient_degree::) + .max() + .expect("the chiplet stack is non-empty"); + 1usize << max_log_quotient_degree +} + +/// ACE codegen settings for the precompile chiplet relation. +fn precompile_ace_config() -> AceConfig { + AceConfig { + num_quotient_chunks: num_quotient_chunks(), + layout: LayoutKind::Masm, + num_airs: NUM_CHIPLETS, + } +} + /// Builds the ACE circuit for the precompile chiplet multi-AIR relation. /// /// The circuit uses the stable [`ChipletAir::all`] instance order as its canonical ACE fold order /// and aligns trace regions to eight base-field elements. These choices define the committed ACE /// encoding; they do not prescribe the lifted STARK proof order. The cross-chiplet LogUp identity /// is checked separately by `ChipletMultiAir::eval_external`. -pub fn build_precompile_multi_air_ace_circuit( - config: AceConfig, -) -> Result, AceError> { - const LMCS_ALIGNMENT: usize = 8; - +pub fn build_precompile_multi_air_ace_circuit() -> Result, AceError> { let airs = ChipletAir::all(); let proof_order: Vec<_> = (0..airs.len()).collect(); - build_multi_air_ace_circuit(&airs, &proof_order, config, LMCS_ALIGNMENT) + build_multi_air_ace_circuit::( + &airs, + &proof_order, + precompile_ace_config(), + LMCS_ALIGNMENT, + ) } #[cfg(test)] mod tests { - use miden_ace_codegen::{AceConfig, LayoutKind}; + use alloc::{format, string::String, vec::Vec}; + + use miden_core::{Felt, field::QuadFelt}; - use super::build_precompile_multi_air_ace_circuit; - use crate::session::NUM_CHIPLETS; + use super::{build_precompile_multi_air_ace_circuit, precompile_ace_config}; + use crate::session::{ChipletAir, NUM_CHIPLETS}; #[test] fn precompile_multi_air_ace_circuit_builds() { - let config = AceConfig { - num_quotient_chunks: 8, - layout: LayoutKind::Masm, - num_airs: NUM_CHIPLETS, - }; - - let circuit = build_precompile_multi_air_ace_circuit(config) - .expect("precompile multi-AIR ACE circuit"); + let circuit = + build_precompile_multi_air_ace_circuit().expect("precompile multi-AIR ACE circuit"); assert_eq!(circuit.layout().counts.num_public, crate::logup::NUM_PUBLIC_VALUES); assert_eq!(circuit.layout().counts.num_aux_boundary, NUM_CHIPLETS); assert!(circuit.layout().counts.preprocessed_width >= 8); } + + /// Pin the complete quotient-degree vector, not merely its maximum: otherwise a chiplet could + /// drift between degrees while another chiplet kept the relation-wide maximum unchanged. + #[test] + fn quotient_chunks_match_the_symbolic_derivation() { + const EXPECTED: [(&str, u8); NUM_CHIPLETS] = [ + ("ChunkNodeSponge", 2), + ("Poseidon2", 2), + ("KeccakRound", 2), + ("BytePairLut", 1), + ("TranscriptEval", 1), + ("UintStoreMul", 1), + ("UintAdd", 1), + ("EcPointStoreGroups", 1), + ("EcGroupAdd", 1), + ("EcMsm", 1), + ]; + + let derived: Vec<(String, u8)> = ChipletAir::all() + .iter() + .map(|air| { + ( + format!("{air:?}"), + miden_lifted_stark::log_quotient_degree::(air), + ) + }) + .collect(); + let expected: Vec<(String, u8)> = + EXPECTED.iter().map(|(name, degree)| ((*name).into(), *degree)).collect(); + assert_eq!( + derived, expected, + "a chiplet's quotient degree moved; if intended, re-mint the relation digest" + ); + + let max = derived.iter().map(|(_, degree)| *degree).max().expect("non-empty stack"); + let expected_chunks = 1usize << max; + assert_eq!( + precompile_ace_config().num_quotient_chunks, + expected_chunks, + "the ACE circuit must read exactly the quotient chunks the proof carries" + ); + let circuit = + build_precompile_multi_air_ace_circuit().expect("precompile multi-AIR ACE circuit"); + assert_eq!( + circuit.layout().counts.num_quotient_chunks, + expected_chunks, + "the built circuit must preserve the derived quotient arity" + ); + } } diff --git a/crates/precompiles-prover/src/ec/add/mod.rs b/crates/precompiles-prover/src/ec/add/mod.rs index 38a650b5cc..03589b204b 100644 --- a/crates/precompiles-prover/src/ec/add/mod.rs +++ b/crates/precompiles-prover/src/ec/add/mod.rs @@ -829,9 +829,10 @@ where ); // col 11: the result-membership cert provide, alone. −1 per mint // op (negative ⇒ provide), naming the fresh result `r` and its - // group. Consumed by `r`'s point-store row (`EcPointStore`), - // discharging its on-curve obligation without the MAC trio; the - // bus balances because a fresh result is minted by exactly one op. + // group. Consumed by `r`'s point-store row (the point band of + // `EcPointStoreGroupsAir`), discharging its on-curve obligation + // without the MAC trio; the bus balances because a fresh result + // is minted by exactly one op. let cert_group: LB::Expr = local[CELL_GROUP].into(); let cert_r: LB::Expr = local[CELL_R].into(); frac_col!( diff --git a/crates/precompiles-prover/src/ec/groups.rs b/crates/precompiles-prover/src/ec/groups.rs index f7f54dc33d..6fd1d0faef 100644 --- a/crates/precompiles-prover/src/ec/groups.rs +++ b/crates/precompiles-prover/src/ec/groups.rs @@ -74,9 +74,9 @@ pub const COL_MULT: usize = 5; pub const NUM_MAIN_COLS: usize = 6; // Aux: the single LogUp running-sum column (one fraction). -const NUM_LOGUP_COLS: usize = 1; +pub(crate) const NUM_LOGUP_COLS: usize = 1; const AUX_WIDTH: usize = 1; -const COLUMN_SHAPE: [usize; NUM_LOGUP_COLS] = [1]; +pub(crate) const COLUMN_SHAPE: [usize; NUM_LOGUP_COLS] = [1]; // AIR // ================================================================================================ @@ -118,18 +118,7 @@ impl LiftedAir for EcGroupsAir { } fn eval>(&self, builder: &mut AB) { - let local: [AB::Var; NUM_MAIN_COLS] = current_main(builder.main(), 0); - let next: [AB::Var; NUM_MAIN_COLS] = next_main(builder.main(), 0); - - let ptr: AB::Expr = local[COL_PTR].into(); - let ptr_next: AB::Expr = next[COL_PTR].into(); - - // The ungated chain: ptr = row + 1 for every prover, pads - // included (they are just mult = 0 rows), so ptr → tuple is - // injective by construction. The wrap edge is dropped, keeping - // the cyclic last → first transition free. - builder.when_transition().assert_zero(ptr_next - ptr.clone() - AB::Expr::ONE); - builder.when_first_row().assert_zero(ptr - AB::Expr::ONE); + eval_main(builder, 0); // Phase 2: LogUp. let mut lb = @@ -138,6 +127,25 @@ impl LiftedAir for EcGroupsAir { } } +/// Evaluate this component's base constraints in a main-trace column band. +pub(crate) fn eval_main(builder: &mut AB, main_col_offset: usize) +where + AB: LiftedAirBuilder, +{ + let local: [AB::Var; NUM_MAIN_COLS] = current_main(builder.main(), main_col_offset); + let next: [AB::Var; NUM_MAIN_COLS] = next_main(builder.main(), main_col_offset); + + let ptr: AB::Expr = local[COL_PTR].into(); + let ptr_next: AB::Expr = next[COL_PTR].into(); + + // The ungated chain: ptr = row + 1 for every prover, pads + // included (they are just mult = 0 rows), so ptr → tuple is + // injective by construction. The wrap edge is dropped, keeping + // the cyclic last → first transition free. + builder.when_transition().assert_zero(ptr_next - ptr.clone() - AB::Expr::ONE); + builder.when_first_row().assert_zero(ptr - AB::Expr::ONE); +} + // LOOKUP AIR // ================================================================================================ @@ -162,43 +170,51 @@ where } fn eval(&self, builder: &mut LB) { - let local: [LB::Var; NUM_MAIN_COLS] = current_main(builder.main(), 0); - - // Pads zero the mult cell, so the provide needs no act gate. - let neg_mult: LB::Expr = LB::Expr::ZERO - local[COL_MULT].into(); - - let provide_deg = Deg { v: 1, u: 1 }; - let col_deg = Deg { v: 1, u: 1 }; - - builder.next_column( - |col| { - col.group( - "ec-groups", - |g| { - g.batch( - "ec-groups-fractions", - LB::Expr::ONE, - |b| { - b.insert( - "provide-ecgroup", - neg_mult, - EcGroupMsg { - group_ptr: local[COL_PTR].into(), - a_ptr: local[COL_A_PTR].into(), - b_ptr: local[COL_B_PTR].into(), - bound_ptr: local[COL_BOUND_PTR].into(), - scalar_bound_ptr: local[COL_SBOUND_PTR].into(), - }, - provide_deg, - ); - }, - col_deg, - ); - }, - col_deg, - ); - }, - col_deg, - ); + eval_lookups(builder, 0); } } + +/// Evaluate this component's LogUp columns in a main-trace column band. +pub(crate) fn eval_lookups(builder: &mut LB, main_col_offset: usize) +where + LB: LookupBuilder, +{ + let local: [LB::Var; NUM_MAIN_COLS] = current_main(builder.main(), main_col_offset); + + // Pads zero the mult cell, so the provide needs no act gate. + let neg_mult: LB::Expr = LB::Expr::ZERO - local[COL_MULT].into(); + + let provide_deg = Deg { v: 1, u: 1 }; + let col_deg = Deg { v: 1, u: 1 }; + + builder.next_column( + |col| { + col.group( + "ec-groups", + |g| { + g.batch( + "ec-groups-fractions", + LB::Expr::ONE, + |b| { + b.insert( + "provide-ecgroup", + neg_mult, + EcGroupMsg { + group_ptr: local[COL_PTR].into(), + a_ptr: local[COL_A_PTR].into(), + b_ptr: local[COL_B_PTR].into(), + bound_ptr: local[COL_BOUND_PTR].into(), + scalar_bound_ptr: local[COL_SBOUND_PTR].into(), + }, + provide_deg, + ); + }, + col_deg, + ); + }, + col_deg, + ); + }, + col_deg, + ); +} diff --git a/crates/precompiles-prover/src/ec/mod.rs b/crates/precompiles-prover/src/ec/mod.rs index 055ef732c7..5f13e178cf 100644 --- a/crates/precompiles-prover/src/ec/mod.rs +++ b/crates/precompiles-prover/src/ec/mod.rs @@ -1,12 +1,11 @@ //! EC layer — short-Weierstrass groups and points over the uint layer. //! -//! Three chiplets, two stores and a relation: +//! The production relation packs the two binding stores into one chiplet and keeps group addition +//! separate: //! -//! - [`groups::EcGroupsAir`] — the **group table**: one row per group binding `group_ptr → (a, b, -//! bound, scalar_bound)`; *provides* [`EcGroup`](crate::relations::BusId::EcGroup). -//! - [`EcPointStoreAir`] (this module) — the **point store**: one row per point; *provides* -//! [`EcPoint`](crate::relations::BusId::EcPoint), *consumes* its group's tuple and — unless -//! `is_pai` — the curve-membership MAC trio. +//! - [`point_store_groups::EcPointStoreGroupsAir`] contains the **group table** and **point store** +//! in disjoint column bands over one row range. The standalone [`groups::EcGroupsAir`] and +//! [`EcPointStoreAir`] implementations remain as component AIRs for isolated tests. //! - [`add::EcGroupAddAir`] — the complete group-law addition over the two stores. //! //! Both stores are **binding stores**, deliberately the thinnest @@ -52,6 +51,7 @@ pub mod add; pub mod groups; pub mod msm; +pub mod point_store_groups; pub mod require; pub mod trace; @@ -192,9 +192,9 @@ pub const NUM_MAIN_COLS: usize = 14; // on-curve-cert consume (col 1), and the three trio MAC consumes — each // degree 3, so each sits alone (cols 2-4). The trio and the cert are // mutually-exclusive membership modes. -const NUM_LOGUP_COLS: usize = 5; +pub(crate) const NUM_LOGUP_COLS: usize = 5; const AUX_WIDTH: usize = 5; -const COLUMN_SHAPE: [usize; NUM_LOGUP_COLS] = [1, 2, 1, 1, 1]; +pub(crate) const COLUMN_SHAPE: [usize; NUM_LOGUP_COLS] = [1, 2, 1, 1, 1]; // AIR // ================================================================================================ @@ -236,52 +236,7 @@ impl LiftedAir for EcPointStoreAir { } fn eval>(&self, builder: &mut AB) { - let local: [AB::Var; NUM_MAIN_COLS] = current_main(builder.main(), 0); - let next: [AB::Var; NUM_MAIN_COLS] = next_main(builder.main(), 0); - - let is_pai: AB::Expr = local[COL_IS_PAI].into(); - let is_cert: AB::Expr = local[COL_IS_CERT].into(); - let act: AB::Expr = local[COL_ACT].into(); - let act_next: AB::Expr = next[COL_ACT].into(); - let ptr: AB::Expr = local[COL_PTR].into(); - let ptr_next: AB::Expr = next[COL_PTR].into(); - - // Booleanity. - builder.assert_zero(is_pai.clone() * (AB::Expr::ONE - is_pai.clone())); - builder.assert_zero(is_cert.clone() * (AB::Expr::ONE - is_cert.clone())); - builder.assert_zero(act.clone() * (AB::Expr::ONE - act.clone())); - // A cert point is finite — the two membership modes are exclusive. - builder.assert_zero(is_pai.clone() * is_cert.clone()); - - // PAI rows reference no uints: coordinate / transient ptrs are the - // none-sentinel. - for col in [COL_X_PTR, COL_Y_PTR, COL_U_PTR, COL_W_PTR] { - let cell: AB::Expr = local[col].into(); - builder.assert_zero(is_pai.clone() * cell); - } - // Cert rows carry real coordinates but no MAC transients — the trio - // ptrs are the none-sentinel (the cert discharges membership instead). - for col in [COL_U_PTR, COL_W_PTR] { - let cell: AB::Expr = local[col].into(); - builder.assert_zero(is_cert.clone() * cell); - } - // Inactive rows cannot provide phantom EcPoint tuples: their group and - // membership consumes are act-gated, while the provide self-gates via - // this multiplicity cell. - let point_mult: AB::Expr = local[COL_ECPOINT_MULT].into(); - builder.assert_zero((AB::Expr::ONE - act.clone()) * point_mult); - - // act is monotone (pads only at the tail; the wrap is dropped so - // the cyclic last → first edge stays free)… - builder - .when_transition() - .assert_zero((AB::Expr::ONE - act.clone()) * act_next.clone()); - // …and ptrs are consecutive along the active prefix, starting at 1 - // (an all-pad trace starts at 0). - builder - .when_transition() - .assert_zero(act_next * (ptr_next - ptr.clone() - AB::Expr::ONE)); - builder.when_first_row().assert_zero(ptr - act); + eval_point_store_main(builder, 0); // Phase 2: LogUp. let mut lb = @@ -290,6 +245,59 @@ impl LiftedAir for EcPointStoreAir { } } +/// Evaluate this component's base constraints in a main-trace column band. +pub(crate) fn eval_point_store_main(builder: &mut AB, main_col_offset: usize) +where + AB: LiftedAirBuilder, +{ + let local: [AB::Var; NUM_MAIN_COLS] = current_main(builder.main(), main_col_offset); + let next: [AB::Var; NUM_MAIN_COLS] = next_main(builder.main(), main_col_offset); + + let is_pai: AB::Expr = local[COL_IS_PAI].into(); + let is_cert: AB::Expr = local[COL_IS_CERT].into(); + let act: AB::Expr = local[COL_ACT].into(); + let act_next: AB::Expr = next[COL_ACT].into(); + let ptr: AB::Expr = local[COL_PTR].into(); + let ptr_next: AB::Expr = next[COL_PTR].into(); + + // Booleanity. + builder.assert_zero(is_pai.clone() * (AB::Expr::ONE - is_pai.clone())); + builder.assert_zero(is_cert.clone() * (AB::Expr::ONE - is_cert.clone())); + builder.assert_zero(act.clone() * (AB::Expr::ONE - act.clone())); + // A cert point is finite — the two membership modes are exclusive. + builder.assert_zero(is_pai.clone() * is_cert.clone()); + + // PAI rows reference no uints: coordinate / transient ptrs are the + // none-sentinel. + for col in [COL_X_PTR, COL_Y_PTR, COL_U_PTR, COL_W_PTR] { + let cell: AB::Expr = local[col].into(); + builder.assert_zero(is_pai.clone() * cell); + } + // Cert rows carry real coordinates but no MAC transients — the trio + // ptrs are the none-sentinel (the cert discharges membership instead). + for col in [COL_U_PTR, COL_W_PTR] { + let cell: AB::Expr = local[col].into(); + builder.assert_zero(is_cert.clone() * cell); + } + // Inactive rows cannot provide phantom EcPoint tuples: their group and + // membership consumes are act-gated, while the provide self-gates via + // this multiplicity cell. + let point_mult: AB::Expr = local[COL_ECPOINT_MULT].into(); + builder.assert_zero((AB::Expr::ONE - act.clone()) * point_mult); + + // act is monotone (pads only at the tail; the wrap is dropped so + // the cyclic last → first edge stays free)… + builder + .when_transition() + .assert_zero((AB::Expr::ONE - act.clone()) * act_next.clone()); + // …and ptrs are consecutive along the active prefix, starting at 1 + // (an all-pad trace starts at 0). + builder + .when_transition() + .assert_zero(act_next * (ptr_next - ptr.clone() - AB::Expr::ONE)); + builder.when_first_row().assert_zero(ptr - act); +} + // LOOKUP AIR // ================================================================================================ @@ -314,152 +322,160 @@ where } fn eval(&self, builder: &mut LB) { - let local: [LB::Var; NUM_MAIN_COLS] = current_main(builder.main(), 0); - - let ptr: LB::Expr = local[COL_PTR].into(); - let group_ptr: LB::Expr = local[COL_GROUP_PTR].into(); - let a_ptr: LB::Expr = local[COL_A_PTR].into(); - let b_ptr: LB::Expr = local[COL_B_PTR].into(); - let bound_ptr: LB::Expr = local[COL_BOUND_PTR].into(); - let sbound_ptr: LB::Expr = local[COL_SBOUND_PTR].into(); - let x_ptr: LB::Expr = local[COL_X_PTR].into(); - let y_ptr: LB::Expr = local[COL_Y_PTR].into(); - let u_ptr: LB::Expr = local[COL_U_PTR].into(); - let w_ptr: LB::Expr = local[COL_W_PTR].into(); - let is_pai: LB::Expr = local[COL_IS_PAI].into(); - let is_cert: LB::Expr = local[COL_IS_CERT].into(); - let act: LB::Expr = local[COL_ACT].into(); - - // Pads zero the mult cell, so the provide needs no act gate; the - // consumes do (an all-zero pad row must touch no bus). The trio fires - // on finite, non-cert rows; the cert consume on finite cert rows — - // disjoint, partitioning a finite point's one membership obligation. - let neg_mult: LB::Expr = LB::Expr::ZERO - local[COL_ECPOINT_MULT].into(); - let member_flag: LB::Expr = - act.clone() * (LB::Expr::ONE - is_pai.clone()) * (LB::Expr::ONE - is_cert.clone()); - let cert_flag: LB::Expr = act.clone() * is_cert; - - let one: LB::Expr = LB::Expr::ONE; - let zero: LB::Expr = LB::Expr::ZERO; - - let provide_deg = Deg { v: 1, u: 1 }; - let consume_deg = Deg { v: 1, u: 1 }; - let member_deg = Deg { v: 3, u: 1 }; - let cert_deg = Deg { v: 2, u: 1 }; - let single_deg = Deg { v: 1, u: 2 }; - let paired_deg = Deg { v: 3, u: 2 }; - - // col 0: the point binding, alone — the gated running-sum anchor. - frac_col!( - builder, - "ec-points", - single_deg, - ( - "provide-ecpoint", - neg_mult, - EcPointMsg { - point_ptr: ptr.clone(), - group_ptr: group_ptr.clone(), - x_ptr: x_ptr.clone(), - y_ptr: y_ptr.clone(), - is_pai: is_pai.clone(), - }, - provide_deg - ), - ); - // col 1 (paired, lqd-1): the group binding consume (forcing - // group_ptr onto a real group row and the a/b/bound/sbound cells - // onto its context — for PAI rows the only tie to a real group) - // paired with the closure-cert consume (a fresh group-law - // result's on-curve membership, discharged in place of the trio). - frac_col!( - builder, - "ec-points", - paired_deg, - ( - "consume-ecgroup", - act, - EcGroupMsg { - group_ptr: group_ptr.clone(), - a_ptr: a_ptr.clone(), - b_ptr: b_ptr.clone(), - bound_ptr: bound_ptr.clone(), - scalar_bound_ptr: sbound_ptr.clone(), - }, - consume_deg - ), - ( - "consume-ecgroupadd-cert", - cert_flag, - EcOnCurveCertMsg { - group_ptr: group_ptr.clone(), - r_ptr: ptr.clone() - }, - cert_deg - ), - ); - // cols 2-4: the curve-membership MAC trio (shared r_ptr = w makes - // y² = x³ + ax + b an identity of stored values), each degree 3 - // so each sits alone. - frac_col!( - builder, - "ec-points", - single_deg, - ( - "consume-mac-u", - member_flag.clone(), - UintMulMsg { - kappa_a: one.clone(), - kappa_c: one.clone(), - a_ptr: x_ptr.clone(), - b_ptr: x_ptr.clone(), - c_ptr: a_ptr.clone(), - r_ptr: u_ptr.clone(), - bound_ptr: bound_ptr.clone(), - is_sub: LB::Expr::ZERO, - }, - member_deg - ), - ); - frac_col!( - builder, - "ec-points", - single_deg, - ( - "consume-mac-w", - member_flag.clone(), - UintMulMsg { - kappa_a: one.clone(), - kappa_c: one.clone(), - a_ptr: x_ptr.clone(), - b_ptr: u_ptr.clone(), - c_ptr: b_ptr.clone(), - r_ptr: w_ptr.clone(), - bound_ptr: bound_ptr.clone(), - is_sub: LB::Expr::ZERO, - }, - member_deg - ), - ); - frac_col!( - builder, - "ec-points", - single_deg, - ( - "consume-mac-y", - member_flag, - UintMulMsg { - kappa_a: one, - kappa_c: zero, - a_ptr: y_ptr.clone(), - b_ptr: y_ptr.clone(), - c_ptr: bound_ptr.clone(), - r_ptr: w_ptr.clone(), - bound_ptr: bound_ptr.clone(), - is_sub: LB::Expr::ZERO, - }, - member_deg - ), - ); + eval_point_store_lookups(builder, 0); } } + +/// Evaluate this component's LogUp columns in a main-trace column band. +pub(crate) fn eval_point_store_lookups(builder: &mut LB, main_col_offset: usize) +where + LB: LookupBuilder, +{ + let local: [LB::Var; NUM_MAIN_COLS] = current_main(builder.main(), main_col_offset); + + let ptr: LB::Expr = local[COL_PTR].into(); + let group_ptr: LB::Expr = local[COL_GROUP_PTR].into(); + let a_ptr: LB::Expr = local[COL_A_PTR].into(); + let b_ptr: LB::Expr = local[COL_B_PTR].into(); + let bound_ptr: LB::Expr = local[COL_BOUND_PTR].into(); + let sbound_ptr: LB::Expr = local[COL_SBOUND_PTR].into(); + let x_ptr: LB::Expr = local[COL_X_PTR].into(); + let y_ptr: LB::Expr = local[COL_Y_PTR].into(); + let u_ptr: LB::Expr = local[COL_U_PTR].into(); + let w_ptr: LB::Expr = local[COL_W_PTR].into(); + let is_pai: LB::Expr = local[COL_IS_PAI].into(); + let is_cert: LB::Expr = local[COL_IS_CERT].into(); + let act: LB::Expr = local[COL_ACT].into(); + + // Pads zero the mult cell, so the provide needs no act gate; the + // consumes do (an all-zero pad row must touch no bus). The trio fires + // on finite, non-cert rows; the cert consume on finite cert rows — + // disjoint, partitioning a finite point's one membership obligation. + let neg_mult: LB::Expr = LB::Expr::ZERO - local[COL_ECPOINT_MULT].into(); + let member_flag: LB::Expr = + act.clone() * (LB::Expr::ONE - is_pai.clone()) * (LB::Expr::ONE - is_cert.clone()); + let cert_flag: LB::Expr = act.clone() * is_cert; + + let one: LB::Expr = LB::Expr::ONE; + let zero: LB::Expr = LB::Expr::ZERO; + + let provide_deg = Deg { v: 1, u: 1 }; + let consume_deg = Deg { v: 1, u: 1 }; + let member_deg = Deg { v: 3, u: 1 }; + let cert_deg = Deg { v: 2, u: 1 }; + let single_deg = Deg { v: 1, u: 2 }; + let paired_deg = Deg { v: 3, u: 2 }; + + // col 0: the point binding, alone — the gated running-sum anchor. + frac_col!( + builder, + "ec-points", + single_deg, + ( + "provide-ecpoint", + neg_mult, + EcPointMsg { + point_ptr: ptr.clone(), + group_ptr: group_ptr.clone(), + x_ptr: x_ptr.clone(), + y_ptr: y_ptr.clone(), + is_pai: is_pai.clone(), + }, + provide_deg + ), + ); + // col 1 (paired, lqd-1): the group binding consume (forcing + // group_ptr onto a real group row and the a/b/bound/sbound cells + // onto its context — for PAI rows the only tie to a real group) + // paired with the closure-cert consume (a fresh group-law + // result's on-curve membership, discharged in place of the trio). + frac_col!( + builder, + "ec-points", + paired_deg, + ( + "consume-ecgroup", + act, + EcGroupMsg { + group_ptr: group_ptr.clone(), + a_ptr: a_ptr.clone(), + b_ptr: b_ptr.clone(), + bound_ptr: bound_ptr.clone(), + scalar_bound_ptr: sbound_ptr.clone(), + }, + consume_deg + ), + ( + "consume-ecgroupadd-cert", + cert_flag, + EcOnCurveCertMsg { + group_ptr: group_ptr.clone(), + r_ptr: ptr.clone() + }, + cert_deg + ), + ); + // cols 2-4: the curve-membership MAC trio (shared r_ptr = w makes + // y² = x³ + ax + b an identity of stored values), each degree 3 + // so each sits alone. + frac_col!( + builder, + "ec-points", + single_deg, + ( + "consume-mac-u", + member_flag.clone(), + UintMulMsg { + kappa_a: one.clone(), + kappa_c: one.clone(), + a_ptr: x_ptr.clone(), + b_ptr: x_ptr.clone(), + c_ptr: a_ptr.clone(), + r_ptr: u_ptr.clone(), + bound_ptr: bound_ptr.clone(), + is_sub: LB::Expr::ZERO, + }, + member_deg + ), + ); + frac_col!( + builder, + "ec-points", + single_deg, + ( + "consume-mac-w", + member_flag.clone(), + UintMulMsg { + kappa_a: one.clone(), + kappa_c: one.clone(), + a_ptr: x_ptr.clone(), + b_ptr: u_ptr.clone(), + c_ptr: b_ptr.clone(), + r_ptr: w_ptr.clone(), + bound_ptr: bound_ptr.clone(), + is_sub: LB::Expr::ZERO, + }, + member_deg + ), + ); + frac_col!( + builder, + "ec-points", + single_deg, + ( + "consume-mac-y", + member_flag, + UintMulMsg { + kappa_a: one, + kappa_c: zero, + a_ptr: y_ptr.clone(), + b_ptr: y_ptr.clone(), + c_ptr: bound_ptr.clone(), + r_ptr: w_ptr.clone(), + bound_ptr: bound_ptr.clone(), + is_sub: LB::Expr::ZERO, + }, + member_deg + ), + ); +} diff --git a/crates/precompiles-prover/src/ec/point_store_groups/mod.rs b/crates/precompiles-prover/src/ec/point_store_groups/mod.rs new file mode 100644 index 0000000000..4b419e6906 --- /dev/null +++ b/crates/precompiles-prover/src/ec/point_store_groups/mod.rs @@ -0,0 +1,115 @@ +//! Composite AIR for the EC point store and group table. +//! +//! The two components share a row range in disjoint column bands. Their +//! constraints and LogUp interactions delegate to the same offset-aware +//! evaluators used by the standalone component AIRs. + +pub mod trace; + +use alloc::vec::Vec; + +use miden_core::{Felt, field::QuadFelt, utils::RowMajorMatrix}; +use miden_lifted_air::{BaseAir, LiftedAir, LiftedAirBuilder}; + +use crate::{ + ec::{self, groups}, + logup::{ + CyclicConstraintLookupBuilder, LookupAir, LookupBuilder, NUM_PUBLIC_VALUES, NUM_RANDOMNESS, + NUM_SIGMA_VALUES, + }, + relations::{MAX_MESSAGE_WIDTH, NUM_BUS_IDS}, +}; + +/// First main-trace column of the group-table band. +pub const GROUPS_COL_OFFSET: usize = ec::NUM_MAIN_COLS; + +pub const NUM_MAIN_COLS: usize = ec::NUM_MAIN_COLS + groups::NUM_MAIN_COLS; +pub const NUM_AUX_COLS: usize = ec::NUM_LOGUP_COLS + groups::NUM_LOGUP_COLS; + +const fn column_shape() -> [usize; NUM_AUX_COLS] { + let mut shape = [0usize; NUM_AUX_COLS]; + let mut i = 0; + while i < ec::NUM_LOGUP_COLS { + shape[i] = ec::COLUMN_SHAPE[i]; + i += 1; + } + let mut j = 0; + while j < groups::NUM_LOGUP_COLS { + shape[ec::NUM_LOGUP_COLS + j] = groups::COLUMN_SHAPE[j]; + j += 1; + } + shape +} +const COLUMN_SHAPE: [usize; NUM_AUX_COLS] = column_shape(); + +#[derive(Debug, Default, Clone, Copy)] +pub struct EcPointStoreGroupsAir; + +impl BaseAir for EcPointStoreGroupsAir { + fn width(&self) -> usize { + NUM_MAIN_COLS + } + + fn num_public_values(&self) -> usize { + NUM_PUBLIC_VALUES + } +} + +impl LiftedAir for EcPointStoreGroupsAir { + fn num_randomness(&self) -> usize { + NUM_RANDOMNESS + } + + fn aux_width(&self) -> usize { + NUM_AUX_COLS + } + + fn num_aux_values(&self) -> usize { + NUM_SIGMA_VALUES + } + + fn build_aux_trace( + &self, + main: &RowMajorMatrix, + _air_inputs: &[Felt], + _aux_inputs: &[Felt], + challenges: &[QuadFelt], + ) -> (RowMajorMatrix, Vec) { + trace::build_aux(main, challenges) + } + + fn eval>(&self, builder: &mut AB) { + ec::eval_point_store_main(builder, 0); + groups::eval_main(builder, GROUPS_COL_OFFSET); + + let mut lb = + CyclicConstraintLookupBuilder::new(builder, self, self.preprocessed_width() > 0); + >::eval(self, &mut lb); + } +} + +impl LookupAir for EcPointStoreGroupsAir +where + LB: LookupBuilder, +{ + fn num_columns(&self) -> usize { + NUM_AUX_COLS + } + + fn column_shape(&self) -> &[usize] { + &COLUMN_SHAPE + } + + fn max_message_width(&self) -> usize { + MAX_MESSAGE_WIDTH + } + + fn num_bus_ids(&self) -> usize { + NUM_BUS_IDS + } + + fn eval(&self, builder: &mut LB) { + ec::eval_point_store_lookups(builder, 0); + groups::eval_lookups(builder, GROUPS_COL_OFFSET); + } +} diff --git a/crates/precompiles-prover/src/ec/point_store_groups/trace.rs b/crates/precompiles-prover/src/ec/point_store_groups/trace.rs new file mode 100644 index 0000000000..bd8cb9cb3e --- /dev/null +++ b/crates/precompiles-prover/src/ec/point_store_groups/trace.rs @@ -0,0 +1,49 @@ +//! Trace generation for the merged point-store + ec-groups chiplet. + +use alloc::vec::Vec; + +use miden_core::{ + Felt, + field::QuadFelt, + utils::{Matrix, RowMajorMatrix}, +}; + +use crate::{ + ec::{ + NUM_MAIN_COLS as POINTS_NUM_MAIN_COLS, + groups::NUM_MAIN_COLS as G_NUM_MAIN_COLS, + point_store_groups::{EcPointStoreGroupsAir, NUM_MAIN_COLS}, + trace::{EcStoreRequires, groups_trace_padded_to, points_trace}, + }, + logup::build_logup_aux_trace, +}; + +/// Build the merged main trace at the largest component height. Point rows +/// can be zero-extended because they are activity-gated; group rows use +/// [`groups_trace_padded_to`] to preserve the ungated pointer chain. +pub fn generate_trace(requires: EcStoreRequires) -> RowMajorMatrix { + let mut points_main = points_trace(&requires); + let points_height = points_main.height(); + let groups_main = groups_trace_padded_to(&requires, points_height); + let height = groups_main.height(); + points_main.values.resize(height * POINTS_NUM_MAIN_COLS, Felt::ZERO); + + let mut vals = Vec::with_capacity(height * NUM_MAIN_COLS); + for r in 0..height { + vals.extend_from_slice( + &points_main.values[r * POINTS_NUM_MAIN_COLS..(r + 1) * POINTS_NUM_MAIN_COLS], + ); + vals.extend_from_slice(&groups_main.values[r * G_NUM_MAIN_COLS..(r + 1) * G_NUM_MAIN_COLS]); + } + debug_assert_eq!(vals.len(), height * NUM_MAIN_COLS); + + RowMajorMatrix::new(vals, NUM_MAIN_COLS) +} + +/// Build the merged chiplet's LogUp trace. +pub(crate) fn build_aux( + main: &RowMajorMatrix, + challenges: &[QuadFelt], +) -> (RowMajorMatrix, Vec) { + build_logup_aux_trace(&EcPointStoreGroupsAir, main, challenges) +} diff --git a/crates/precompiles-prover/src/ec/trace.rs b/crates/precompiles-prover/src/ec/trace.rs index 52b88d0e50..e3d9724df4 100644 --- a/crates/precompiles-prover/src/ec/trace.rs +++ b/crates/precompiles-prover/src/ec/trace.rs @@ -335,15 +335,9 @@ impl EcStoreRequires { } } -/// Build **both** EC store main traces from the accumulator (consumed — -/// trace-gen is terminal, so the double-lay hazard is a compile error), -/// returning `(groups_main, points_main)` in -/// [`SessionTraces`](crate::session::SessionTraces) order. Pure reads of -/// the demand ledgers: every cross-chiplet consumer has already fed them -/// — the points' own `EcGroup` consume at intern (the store's -/// bound-ref analogue), the add relation's `EcGroup` / `EcPoint` -/// consumes in [`super::add::trace::generate_trace`], run first by the -/// Session sweep. +/// Build the standalone group and point-store traces for component tests. +/// Callers must record all cross-chiplet requirements before consuming the +/// accumulator here. pub fn generate_traces(requires: EcStoreRequires) -> (RowMajorMatrix, RowMajorMatrix) { (groups_trace(&requires), points_trace(&requires)) } @@ -353,7 +347,20 @@ pub fn generate_traces(requires: EcStoreRequires) -> (RowMajorMatrix, RowM /// `ptr = row + 1` on every row, so pads carry their ptr too — they are /// simply rows whose `mult` (and params) stay zero, touching no bus. fn groups_trace(requires: &EcStoreRequires) -> RowMajorMatrix { - let height = requires.groups.len().next_power_of_two().max(2); + groups_trace_padded_to(requires, 0) +} + +/// [`groups_trace`] with a height floor — for sharing the group table's +/// row range with another AIR (see [`super::point_store_groups`]): pads +/// past the natural height are the table's own padding mechanism +/// (`ptr = row + 1` continued, `mult` and params zero). `min_height` +/// must be 0 or a power of two so the padded height remains a power of two. +pub(crate) fn groups_trace_padded_to( + requires: &EcStoreRequires, + min_height: usize, +) -> RowMajorMatrix { + debug_assert!(min_height == 0 || min_height.is_power_of_two()); + let height = requires.groups.len().next_power_of_two().max(2).max(min_height); let mut vals = Vec::with_capacity(height * G_NUM_MAIN_COLS); for i in 0..height { @@ -377,7 +384,7 @@ fn groups_trace(requires: &EcStoreRequires) -> RowMajorMatrix { /// The point store — one row per point in allocation order /// (ptr = row + 1), padded to a power-of-two height (min 2) with /// all-zero (`act = 0`) rows that touch no bus. -fn points_trace(requires: &EcStoreRequires) -> RowMajorMatrix { +pub(crate) fn points_trace(requires: &EcStoreRequires) -> RowMajorMatrix { let height = requires.points.len().next_power_of_two().max(2); let mut vals = Vec::with_capacity(height * NUM_MAIN_COLS); diff --git a/crates/precompiles-prover/src/hash/chunk/mod.rs b/crates/precompiles-prover/src/hash/chunk/mod.rs index 79b9a3e840..5141319f78 100644 --- a/crates/precompiles-prover/src/hash/chunk/mod.rs +++ b/crates/precompiles-prover/src/hash/chunk/mod.rs @@ -91,7 +91,7 @@ pub const NUM_MAIN_COLS: usize = COL_F_END; pub const NUM_AUX_COLS: usize = 5; /// Per-column fraction counts, matching the pairing above. -const COLUMN_SHAPE: [usize; NUM_AUX_COLS] = [1, 2, 2, 2, 1]; +pub(crate) const COLUMN_SHAPE: [usize; NUM_AUX_COLS] = [1, 2, 2, 2, 1]; // The single exposed σ ([`NUM_SIGMA_VALUES`]) follows the VM-wide σ // contract in [`crate::logup`]; aggregating the Memory64 + Poseidon2In diff --git a/crates/precompiles-prover/src/hash/chunk_node/mod.rs b/crates/precompiles-prover/src/hash/chunk_node/mod.rs index 5453acfea3..f2ddcf962a 100644 --- a/crates/precompiles-prover/src/hash/chunk_node/mod.rs +++ b/crates/precompiles-prover/src/hash/chunk_node/mod.rs @@ -1,5 +1,6 @@ -//! ChunkNode chiplet — the chunk chiplet and the Keccak transcript-DAG -//! node chiplet sharing one row range. +//! Chunk and Keccak transcript-DAG node bands sharing one row range, +//! composed into the merged hash chiplet by +//! [`crate::hash::chunk_node_sponge::ChunkNodeSpongeAir`]. //! //! Both are period-1 (no periodic columns) and their own trace heights //! are otherwise unrelated, so they run **simultaneously** on the same @@ -15,23 +16,11 @@ //! into chunk's — both still close into the one shared σ via the //! standard `acc_next[0] = Σ acc[i]` recurrence, and neither pays the //! degree cost of physically sharing column 0. -//! -//! The shared height is `max` of what each side natively needs -//! (independently `next_power_of_two`-padded, own padding mechanism), -//! not their sum, since they occupy the same rows. - -pub mod trace; -use alloc::vec::Vec; use core::array; -use miden_core::{ - Felt, - deferred::Tag, - field::{PrimeCharacteristicRing, QuadFelt}, - utils::RowMajorMatrix, -}; -use miden_lifted_air::{AirBuilder, BaseAir, LiftedAir, LiftedAirBuilder}; +use miden_core::{Felt, deferred::Tag, field::PrimeCharacteristicRing}; +use miden_lifted_air::{AirBuilder, LiftedAirBuilder}; use miden_precompiles::Keccak256Precompile; use crate::{ @@ -40,11 +29,7 @@ use crate::{ keccak::{node, sponge::KeccakSpongeMsg}, memory64::{CHUNK_ADDR_BASE, Memory64Msg}, }, - logup::{ - CyclicConstraintLookupBuilder, Deg, LookupAir, LookupBatch, LookupBuilder, LookupColumn, - LookupGroup, NUM_PUBLIC_VALUES, NUM_RANDOMNESS, NUM_SIGMA_VALUES, frac_col, - }, - relations::{MAX_MESSAGE_WIDTH, NUM_BUS_IDS}, + logup::{Deg, LookupBatch, LookupBuilder, LookupColumn, LookupGroup, frac_col}, transcript::{ binding::BindingMsg, poseidon2::{Poseidon2InMsg, Poseidon2OutMsg}, @@ -66,501 +51,457 @@ pub const NUM_MAIN_COLS: usize = chunk::NUM_MAIN_COLS + node::NUM_MAIN_COLS; /// = keccak-node's original cols 1..8 unchanged. pub const NUM_AUX_COLS: usize = chunk::NUM_AUX_COLS + node::NUM_AUX_COLS; -const COLUMN_SHAPE: [usize; NUM_AUX_COLS] = [1, 2, 2, 2, 1, 1, 2, 1, 2, 2, 2, 2, 2, 2]; - -// AIR -// ================================================================================================ - -/// ChunkNode chiplet AIR. Period 1 (no periodic columns). -#[derive(Debug, Default, Clone, Copy)] -pub struct ChunkNodeAir; - -impl BaseAir for ChunkNodeAir { - fn width(&self) -> usize { - NUM_MAIN_COLS +const fn column_shape() -> [usize; NUM_AUX_COLS] { + let mut shape = [0usize; NUM_AUX_COLS]; + let mut i = 0; + while i < chunk::NUM_AUX_COLS { + shape[i] = chunk::COLUMN_SHAPE[i]; + i += 1; } - - fn num_public_values(&self) -> usize { - NUM_PUBLIC_VALUES + let mut j = 0; + while j < node::NUM_AUX_COLS { + shape[chunk::NUM_AUX_COLS + j] = node::COLUMN_SHAPE[j]; + j += 1; } + shape } +pub(crate) const COLUMN_SHAPE: [usize; NUM_AUX_COLS] = column_shape(); -impl LiftedAir for ChunkNodeAir { - fn num_randomness(&self) -> usize { - NUM_RANDOMNESS - } - - fn aux_width(&self) -> usize { - NUM_AUX_COLS - } - - fn num_aux_values(&self) -> usize { - NUM_SIGMA_VALUES - } - - fn build_aux_trace( - &self, - main: &RowMajorMatrix, - _air_inputs: &[Felt], - _aux_inputs: &[Felt], - challenges: &[QuadFelt], - ) -> (RowMajorMatrix, Vec) { - trace::build_aux(main, challenges) - } - - fn eval>(&self, builder: &mut AB) { - // ---- CHUNK (verbatim from `chunk::ChunkAir::eval`, cols 0..12) ---- - { - let local: [AB::Var; chunk::NUM_MAIN_COLS] = current_main(builder.main(), 0); - let next: [AB::Var; chunk::NUM_MAIN_COLS] = next_main(builder.main(), 0); - - let chunk_seq_id: AB::Expr = local[chunk::COL_CHUNK_SEQ_ID].into(); - let chunk_seq_id_next: AB::Expr = next[chunk::COL_CHUNK_SEQ_ID].into(); - let perm_seq_id: AB::Expr = local[chunk::COL_PERM_SEQ_ID].into(); - let perm_seq_id_next: AB::Expr = next[chunk::COL_PERM_SEQ_ID].into(); - let act: AB::Expr = local[chunk::COL_ACT].into(); - let act_next: AB::Expr = next[chunk::COL_ACT].into(); - let is_head: AB::Expr = local[chunk::COL_IS_HEAD].into(); - let is_head_next: AB::Expr = next[chunk::COL_IS_HEAD].into(); - - builder.when_first_row().assert_zero(chunk_seq_id.clone()); - - builder - .when_transition() - .assert_zero(chunk_seq_id_next - chunk_seq_id - AB::Expr::ONE); - - builder.when_transition().assert_zero( - (AB::Expr::ONE - is_head_next) * (perm_seq_id_next - perm_seq_id - AB::Expr::ONE), - ); - - builder.assert_bool(local[chunk::COL_ACT]); - builder.when_transition().assert_zero((AB::Expr::ONE - act.clone()) * act_next); - - builder.assert_bool(local[chunk::COL_IS_HEAD]); - builder.assert_zero(is_head * (AB::Expr::ONE - act)); - } - - // ---- KECCAK-NODE (verbatim from `node::KeccakNodeAir::eval`, cols - // `NODE_COL_OFFSET`..`NUM_MAIN_COLS`) ---- - { - let local: [AB::Var; node::NUM_MAIN_COLS] = - current_main(builder.main(), NODE_COL_OFFSET); - let next: [AB::Var; node::NUM_MAIN_COLS] = next_main(builder.main(), NODE_COL_OFFSET); - - let act: AB::Expr = local[node::COL_ACT].into(); - let act_next: AB::Expr = next[node::COL_ACT].into(); - let out_mult: AB::Expr = local[node::COL_OUT_MULT].into(); - - let sponge_seq_id_head: AB::Expr = local[node::COL_SPONGE_SEQ_ID_HEAD].into(); - let sponge_seq_id_head_next: AB::Expr = next[node::COL_SPONGE_SEQ_ID_HEAD].into(); - let n_sponge_perms: AB::Expr = local[node::COL_N_SPONGE_PERMS].into(); - - let chunk_seq_id_head: AB::Expr = local[node::COL_CHUNK_SEQ_ID_HEAD].into(); - let chunk_seq_id_head_next: AB::Expr = next[node::COL_CHUNK_SEQ_ID_HEAD].into(); - let n_chunks: AB::Expr = local[node::COL_N_CHUNKS].into(); - - let _ = next[node::COL_PERM_SEQ_ID_CHUNKS]; - - builder.when_first_row().assert_zero(sponge_seq_id_head.clone()); - builder.when_first_row().assert_zero(chunk_seq_id_head.clone()); - - builder.assert_bool(local[node::COL_ACT]); - builder - .when_transition() - .assert_zero((AB::Expr::ONE - act.clone()) * act_next.clone()); - - builder.assert_zero((AB::Expr::ONE - act) * out_mult); - - builder.when_transition().assert_zero( - act_next.clone() - * (sponge_seq_id_head_next - - sponge_seq_id_head - - AB::Expr::from(Felt::from(32u8)) * n_sponge_perms), - ); - builder - .when_transition() - .assert_zero(act_next * (chunk_seq_id_head_next - chunk_seq_id_head - n_chunks)); - } - - // Phase 2: LogUp argument via the LogUp adapter. - let mut lb = - CyclicConstraintLookupBuilder::new(builder, self, self.preprocessed_width() > 0); - >::eval(self, &mut lb); - } -} - -// LOOKUP AIR +// CONSTRAINTS // ================================================================================================ -impl LookupAir for ChunkNodeAir +/// Evaluate this component's base constraints in a main-trace column band. +pub(crate) fn eval_main(builder: &mut AB, main_col_offset: usize) where - LB: LookupBuilder, + AB: LiftedAirBuilder, { - fn num_columns(&self) -> usize { - NUM_AUX_COLS - } + // Chunk constraints. + { + let local: [AB::Var; chunk::NUM_MAIN_COLS] = current_main(builder.main(), main_col_offset); + let next: [AB::Var; chunk::NUM_MAIN_COLS] = next_main(builder.main(), main_col_offset); + + let chunk_seq_id: AB::Expr = local[chunk::COL_CHUNK_SEQ_ID].into(); + let chunk_seq_id_next: AB::Expr = next[chunk::COL_CHUNK_SEQ_ID].into(); + let perm_seq_id: AB::Expr = local[chunk::COL_PERM_SEQ_ID].into(); + let perm_seq_id_next: AB::Expr = next[chunk::COL_PERM_SEQ_ID].into(); + let act: AB::Expr = local[chunk::COL_ACT].into(); + let act_next: AB::Expr = next[chunk::COL_ACT].into(); + let is_head: AB::Expr = local[chunk::COL_IS_HEAD].into(); + let is_head_next: AB::Expr = next[chunk::COL_IS_HEAD].into(); + + builder.when_first_row().assert_zero(chunk_seq_id.clone()); + + builder + .when_transition() + .assert_zero(chunk_seq_id_next - chunk_seq_id - AB::Expr::ONE); + + builder.when_transition().assert_zero( + (AB::Expr::ONE - is_head_next) * (perm_seq_id_next - perm_seq_id - AB::Expr::ONE), + ); - fn column_shape(&self) -> &[usize] { - &COLUMN_SHAPE - } + builder.assert_bool(local[chunk::COL_ACT]); + builder.when_transition().assert_zero((AB::Expr::ONE - act.clone()) * act_next); - fn max_message_width(&self) -> usize { - MAX_MESSAGE_WIDTH + builder.assert_bool(local[chunk::COL_IS_HEAD]); + builder.assert_zero(is_head * (AB::Expr::ONE - act)); } - fn num_bus_ids(&self) -> usize { - NUM_BUS_IDS - } + // Keccak-node constraints. + { + let local: [AB::Var; node::NUM_MAIN_COLS] = + current_main(builder.main(), main_col_offset + NODE_COL_OFFSET); + let next: [AB::Var; node::NUM_MAIN_COLS] = + next_main(builder.main(), main_col_offset + NODE_COL_OFFSET); - fn eval(&self, builder: &mut LB) { - // ---- CHUNK (verbatim from `chunk::ChunkAir`'s `LookupAir::eval`, aux cols 0..5) ---- - let local: [LB::Var; chunk::NUM_MAIN_COLS] = current_main(builder.main(), 0); - - let chunk_seq_id: LB::Expr = local[chunk::COL_CHUNK_SEQ_ID].into(); - let perm_seq_id: LB::Expr = local[chunk::COL_PERM_SEQ_ID].into(); - let act: LB::Expr = local[chunk::COL_ACT].into(); - let is_head: LB::Expr = local[chunk::COL_IS_HEAD].into(); - let f: [LB::Expr; chunk::NUM_F] = array::from_fn(|i| local[chunk::COL_F_BEGIN + i].into()); - - let chunk_addr_base = - Felt::new(CHUNK_ADDR_BASE).expect("CHUNK_ADDR_BASE fits in canonical Goldilocks"); - let addr0 = - LB::Expr::from(chunk_addr_base) + LB::Expr::from(Felt::from(4u8)) * chunk_seq_id; - let addr1 = addr0.clone() + LB::Expr::ONE; - let addr2 = addr0.clone() + LB::Expr::from(Felt::from(2u8)); - let addr3 = addr0.clone() + LB::Expr::from(Felt::from(3u8)); - - let neg_act: LB::Expr = LB::Expr::ZERO - act.clone(); - - let pos_act: LB::Expr = act.clone(); - let pos_act_head: LB::Expr = act * is_head; - - let rate0_chunk = [f[0].clone(), f[1].clone(), f[2].clone(), f[3].clone()]; - let rate1_chunk = [f[4].clone(), f[5].clone(), f[6].clone(), f[7].clone()]; - let cap_chunk = Tag::CHUNKS.as_word().map(LB::Expr::from); - - let interaction_deg = Deg { v: 1, u: 1 }; - let provides_deg = Deg { v: 1, u: 2 }; - let pair_deg = Deg { v: 3, u: 2 }; - - frac_col!( - builder, - "memory64", - provides_deg, - ( - "lane0", - neg_act.clone(), - Memory64Msg { - addr: addr0, - lo: f[0].clone(), - hi: f[1].clone() - }, - interaction_deg - ), - ); - frac_col!( - builder, - "memory64", - pair_deg, - ( - "lane1", - neg_act.clone(), - Memory64Msg { - addr: addr1, - lo: f[2].clone(), - hi: f[3].clone() - }, - interaction_deg - ), - ( - "lane2", - neg_act.clone(), - Memory64Msg { - addr: addr2, - lo: f[4].clone(), - hi: f[5].clone() - }, - interaction_deg - ), - ); - frac_col!( - builder, - "chunk-flatten", - pair_deg, - ( - "lane3", - neg_act, - Memory64Msg { - addr: addr3, - lo: f[6].clone(), - hi: f[7].clone() - }, - interaction_deg - ), - ( - "rate0", - pos_act.clone(), - Poseidon2InMsg::rate0(perm_seq_id.clone(), rate0_chunk), - interaction_deg - ), - ); - frac_col!( - builder, - "poseidon2-in", - pair_deg, - ( - "rate1", - pos_act, - Poseidon2InMsg::rate1(perm_seq_id.clone(), rate1_chunk), - interaction_deg - ), - ( - "cap", - pos_act_head.clone(), - Poseidon2InMsg::cap(perm_seq_id.clone(), cap_chunk), - interaction_deg - ), - ); + let act: AB::Expr = local[node::COL_ACT].into(); + let act_next: AB::Expr = next[node::COL_ACT].into(); + let out_mult: AB::Expr = local[node::COL_OUT_MULT].into(); - let neg_act_head: LB::Expr = LB::Expr::ZERO - pos_act_head; - frac_col!( - builder, - "chunk-chain", - provides_deg, - ( - "emit", - neg_act_head, - ChunkChainMsg { - chunk_seq_id_head: local[chunk::COL_CHUNK_SEQ_ID].into(), - perm_seq_id_head: perm_seq_id, - }, - interaction_deg - ), - ); + let sponge_seq_id_head: AB::Expr = local[node::COL_SPONGE_SEQ_ID_HEAD].into(); + let sponge_seq_id_head_next: AB::Expr = next[node::COL_SPONGE_SEQ_ID_HEAD].into(); + let n_sponge_perms: AB::Expr = local[node::COL_N_SPONGE_PERMS].into(); - // ---- KECCAK-NODE (verbatim from `node::KeccakNodeAir`'s `LookupAir::eval`, aux cols - // 5..14) ---- - let local: [LB::Var; node::NUM_MAIN_COLS] = current_main(builder.main(), NODE_COL_OFFSET); - - let act: LB::Expr = local[node::COL_ACT].into(); - let sponge_seq_id_head: LB::Expr = local[node::COL_SPONGE_SEQ_ID_HEAD].into(); - let n_sponge_perms: LB::Expr = local[node::COL_N_SPONGE_PERMS].into(); - let chunk_seq_id_head: LB::Expr = local[node::COL_CHUNK_SEQ_ID_HEAD].into(); - let n_chunks: LB::Expr = local[node::COL_N_CHUNKS].into(); - let perm_seq_id_chunks: LB::Expr = local[node::COL_PERM_SEQ_ID_CHUNKS].into(); - let len_bytes: LB::Expr = local[node::COL_LEN_BYTES].into(); - let perm_seq_id_digest_chunks: LB::Expr = local[node::COL_PERM_SEQ_ID_DIGEST_CHUNKS].into(); - let perm_seq_id_keccak: LB::Expr = local[node::COL_PERM_SEQ_ID_KECCAK].into(); - - let d: [LB::Expr; node::NUM_D] = array::from_fn(|i| local[node::COL_D_BEGIN + i].into()); - let h_input_chunks: [LB::Expr; node::NUM_HASH] = - array::from_fn(|i| local[node::COL_H_INPUT_CHUNKS_BEGIN + i].into()); - let h_digest_chunks: [LB::Expr; node::NUM_HASH] = - array::from_fn(|i| local[node::COL_H_DIGEST_CHUNKS_BEGIN + i].into()); - let h_keccak: [LB::Expr; node::NUM_HASH] = - array::from_fn(|i| local[node::COL_H_KECCAK_BEGIN + i].into()); - - let neg_act: LB::Expr = LB::Expr::ZERO - act.clone(); - let pos_act: LB::Expr = act.clone(); - let pos_act_x2: LB::Expr = LB::Expr::from(Felt::from(2u8)) * act; - let out_mult: LB::Expr = local[node::COL_OUT_MULT].into(); - let neg_out_mult: LB::Expr = LB::Expr::ZERO - out_mult; - - let chunk_ptr_head: LB::Expr = LB::Expr::from(Felt::from(4u8)) * chunk_seq_id_head.clone(); - let perm_seq_id_chunks_tail: LB::Expr = - perm_seq_id_chunks.clone() + n_chunks - LB::Expr::ONE; - let digest_addr_base: LB::Expr = LB::Expr::from(Felt::from(100u8)) * sponge_seq_id_head - + LB::Expr::from(Felt::from(3200u32)) * n_sponge_perms - - LB::Expr::from(Felt::from(128u8)); - - let cap_digest_chunks = Tag::CHUNKS.as_word().map(LB::Expr::from); - let cap_keccak = [ - LB::Expr::from(Keccak256Precompile::id()), - LB::Expr::from(Felt::from_u32(Keccak256Precompile::ASSERT_TAG_ID)), - len_bytes.clone(), - LB::Expr::ZERO, - ]; - - let d_rate0 = [d[0].clone(), d[1].clone(), d[2].clone(), d[3].clone()]; - let d_rate1 = [d[4].clone(), d[5].clone(), d[6].clone(), d[7].clone()]; - - frac_col!( - builder, - "handshake-and-chunks-digest", - provides_deg, - ( - "ks-request", - neg_act.clone(), - KeccakSpongeMsg { - sponge_seq_id: local[node::COL_SPONGE_SEQ_ID_HEAD].into(), - chunk_ptr: chunk_ptr_head, - len_bytes: len_bytes.clone() - }, - interaction_deg - ), - ); - frac_col!( - builder, - "handshake-and-chunks-digest", - pair_deg, - ( - "binding-truth", - neg_out_mult, - BindingMsg::truth(h_keccak.clone()), - interaction_deg - ), - ( - "chunk-chain", - pos_act.clone(), - ChunkChainMsg { - chunk_seq_id_head: chunk_seq_id_head.clone(), - perm_seq_id_head: perm_seq_id_chunks - }, - interaction_deg - ), - ); - frac_col!( - builder, - "handshake-and-chunks-digest", - provides_deg, - ( - "p2out-h-input-chunks", - pos_act.clone(), - Poseidon2OutMsg { - perm_seq_id: perm_seq_id_chunks_tail, - digest: h_input_chunks.clone() - }, - interaction_deg - ), - ); + let chunk_seq_id_head: AB::Expr = local[node::COL_CHUNK_SEQ_ID_HEAD].into(); + let chunk_seq_id_head_next: AB::Expr = next[node::COL_CHUNK_SEQ_ID_HEAD].into(); + let n_chunks: AB::Expr = local[node::COL_N_CHUNKS].into(); - let addr_lane = - |j: u8| -> LB::Expr { digest_addr_base.clone() + LB::Expr::from(Felt::from(j)) }; - frac_col!( - builder, - "memory64-d-limbs", - pair_deg, - ( - "d-lane-0", - pos_act_x2.clone(), - Memory64Msg { - addr: addr_lane(0), - lo: d[0].clone(), - hi: d[1].clone() - }, - interaction_deg - ), - ( - "d-lane-1", - pos_act_x2.clone(), - Memory64Msg { - addr: addr_lane(1), - lo: d[2].clone(), - hi: d[3].clone() - }, - interaction_deg - ), - ); - frac_col!( - builder, - "memory64-d-limbs", - pair_deg, - ( - "d-lane-2", - pos_act_x2.clone(), - Memory64Msg { - addr: addr_lane(2), - lo: d[4].clone(), - hi: d[5].clone() - }, - interaction_deg - ), - ( - "d-lane-3", - pos_act_x2, - Memory64Msg { - addr: addr_lane(3), - lo: d[6].clone(), - hi: d[7].clone() - }, - interaction_deg - ), - ); + let _ = next[node::COL_PERM_SEQ_ID_CHUNKS]; - frac_col!( - builder, - "digest-chunks-p2", - pair_deg, - ( - "p2in-rate0", - pos_act.clone(), - Poseidon2InMsg::rate0(perm_seq_id_digest_chunks.clone(), d_rate0), - interaction_deg - ), - ( - "p2in-rate1", - pos_act.clone(), - Poseidon2InMsg::rate1(perm_seq_id_digest_chunks.clone(), d_rate1), - interaction_deg - ), - ); - frac_col!( - builder, - "digest-chunks-p2", - pair_deg, - ( - "p2in-cap", - pos_act.clone(), - Poseidon2InMsg::cap(perm_seq_id_digest_chunks.clone(), cap_digest_chunks), - interaction_deg - ), - ( - "p2out-h-digest-chunks", - pos_act.clone(), - Poseidon2OutMsg { - perm_seq_id: perm_seq_id_digest_chunks, - digest: h_digest_chunks.clone() - }, - interaction_deg - ), - ); + builder.when_first_row().assert_zero(sponge_seq_id_head.clone()); + builder.when_first_row().assert_zero(chunk_seq_id_head.clone()); - frac_col!( - builder, - "keccak-p2", - pair_deg, - ( - "p2in-rate0", - pos_act.clone(), - Poseidon2InMsg::rate0(perm_seq_id_keccak.clone(), h_input_chunks), - interaction_deg - ), - ( - "p2in-rate1", - pos_act.clone(), - Poseidon2InMsg::rate1(perm_seq_id_keccak.clone(), h_digest_chunks), - interaction_deg - ), - ); - frac_col!( - builder, - "keccak-p2", - pair_deg, - ( - "p2in-cap", - pos_act.clone(), - Poseidon2InMsg::cap(perm_seq_id_keccak.clone(), cap_keccak), - interaction_deg - ), - ( - "p2out-h-keccak", - pos_act, - Poseidon2OutMsg { - perm_seq_id: perm_seq_id_keccak, - digest: h_keccak - }, - interaction_deg - ), + builder.assert_bool(local[node::COL_ACT]); + builder + .when_transition() + .assert_zero((AB::Expr::ONE - act.clone()) * act_next.clone()); + + builder.assert_zero((AB::Expr::ONE - act) * out_mult); + + builder.when_transition().assert_zero( + act_next.clone() + * (sponge_seq_id_head_next + - sponge_seq_id_head + - AB::Expr::from(Felt::from(32u8)) * n_sponge_perms), ); + builder + .when_transition() + .assert_zero(act_next * (chunk_seq_id_head_next - chunk_seq_id_head - n_chunks)); } } + +// LOOKUPS +// ================================================================================================ + +/// Evaluate this component's LogUp columns in a main-trace column band. +pub(crate) fn eval_lookups(builder: &mut LB, main_col_offset: usize) +where + LB: LookupBuilder, +{ + // Chunk lookups. + let local: [LB::Var; chunk::NUM_MAIN_COLS] = current_main(builder.main(), main_col_offset); + + let chunk_seq_id: LB::Expr = local[chunk::COL_CHUNK_SEQ_ID].into(); + let perm_seq_id: LB::Expr = local[chunk::COL_PERM_SEQ_ID].into(); + let act: LB::Expr = local[chunk::COL_ACT].into(); + let is_head: LB::Expr = local[chunk::COL_IS_HEAD].into(); + let f: [LB::Expr; chunk::NUM_F] = array::from_fn(|i| local[chunk::COL_F_BEGIN + i].into()); + + let chunk_addr_base = + Felt::new(CHUNK_ADDR_BASE).expect("CHUNK_ADDR_BASE fits in canonical Goldilocks"); + let addr0 = LB::Expr::from(chunk_addr_base) + LB::Expr::from(Felt::from(4u8)) * chunk_seq_id; + let addr1 = addr0.clone() + LB::Expr::ONE; + let addr2 = addr0.clone() + LB::Expr::from(Felt::from(2u8)); + let addr3 = addr0.clone() + LB::Expr::from(Felt::from(3u8)); + + let neg_act: LB::Expr = LB::Expr::ZERO - act.clone(); + + let pos_act: LB::Expr = act.clone(); + let pos_act_head: LB::Expr = act * is_head; + + let rate0_chunk = [f[0].clone(), f[1].clone(), f[2].clone(), f[3].clone()]; + let rate1_chunk = [f[4].clone(), f[5].clone(), f[6].clone(), f[7].clone()]; + let cap_chunk = Tag::CHUNKS.as_word().map(LB::Expr::from); + + let interaction_deg = Deg { v: 1, u: 1 }; + let provides_deg = Deg { v: 1, u: 2 }; + let pair_deg = Deg { v: 3, u: 2 }; + + frac_col!( + builder, + "memory64", + provides_deg, + ( + "lane0", + neg_act.clone(), + Memory64Msg { + addr: addr0, + lo: f[0].clone(), + hi: f[1].clone() + }, + interaction_deg + ), + ); + frac_col!( + builder, + "memory64", + pair_deg, + ( + "lane1", + neg_act.clone(), + Memory64Msg { + addr: addr1, + lo: f[2].clone(), + hi: f[3].clone() + }, + interaction_deg + ), + ( + "lane2", + neg_act.clone(), + Memory64Msg { + addr: addr2, + lo: f[4].clone(), + hi: f[5].clone() + }, + interaction_deg + ), + ); + frac_col!( + builder, + "chunk-flatten", + pair_deg, + ( + "lane3", + neg_act, + Memory64Msg { + addr: addr3, + lo: f[6].clone(), + hi: f[7].clone() + }, + interaction_deg + ), + ( + "rate0", + pos_act.clone(), + Poseidon2InMsg::rate0(perm_seq_id.clone(), rate0_chunk), + interaction_deg + ), + ); + frac_col!( + builder, + "poseidon2-in", + pair_deg, + ( + "rate1", + pos_act, + Poseidon2InMsg::rate1(perm_seq_id.clone(), rate1_chunk), + interaction_deg + ), + ( + "cap", + pos_act_head.clone(), + Poseidon2InMsg::cap(perm_seq_id.clone(), cap_chunk), + interaction_deg + ), + ); + + let neg_act_head: LB::Expr = LB::Expr::ZERO - pos_act_head; + frac_col!( + builder, + "chunk-chain", + provides_deg, + ( + "emit", + neg_act_head, + ChunkChainMsg { + chunk_seq_id_head: local[chunk::COL_CHUNK_SEQ_ID].into(), + perm_seq_id_head: perm_seq_id, + }, + interaction_deg + ), + ); + + // Keccak-node lookups. + let local: [LB::Var; node::NUM_MAIN_COLS] = + current_main(builder.main(), main_col_offset + NODE_COL_OFFSET); + + let act: LB::Expr = local[node::COL_ACT].into(); + let sponge_seq_id_head: LB::Expr = local[node::COL_SPONGE_SEQ_ID_HEAD].into(); + let n_sponge_perms: LB::Expr = local[node::COL_N_SPONGE_PERMS].into(); + let chunk_seq_id_head: LB::Expr = local[node::COL_CHUNK_SEQ_ID_HEAD].into(); + let n_chunks: LB::Expr = local[node::COL_N_CHUNKS].into(); + let perm_seq_id_chunks: LB::Expr = local[node::COL_PERM_SEQ_ID_CHUNKS].into(); + let len_bytes: LB::Expr = local[node::COL_LEN_BYTES].into(); + let perm_seq_id_digest_chunks: LB::Expr = local[node::COL_PERM_SEQ_ID_DIGEST_CHUNKS].into(); + let perm_seq_id_keccak: LB::Expr = local[node::COL_PERM_SEQ_ID_KECCAK].into(); + + let d: [LB::Expr; node::NUM_D] = array::from_fn(|i| local[node::COL_D_BEGIN + i].into()); + let h_input_chunks: [LB::Expr; node::NUM_HASH] = + array::from_fn(|i| local[node::COL_H_INPUT_CHUNKS_BEGIN + i].into()); + let h_digest_chunks: [LB::Expr; node::NUM_HASH] = + array::from_fn(|i| local[node::COL_H_DIGEST_CHUNKS_BEGIN + i].into()); + let h_keccak: [LB::Expr; node::NUM_HASH] = + array::from_fn(|i| local[node::COL_H_KECCAK_BEGIN + i].into()); + + let neg_act: LB::Expr = LB::Expr::ZERO - act.clone(); + let pos_act: LB::Expr = act.clone(); + let pos_act_x2: LB::Expr = LB::Expr::from(Felt::from(2u8)) * act; + let out_mult: LB::Expr = local[node::COL_OUT_MULT].into(); + let neg_out_mult: LB::Expr = LB::Expr::ZERO - out_mult; + + let chunk_ptr_head: LB::Expr = LB::Expr::from(Felt::from(4u8)) * chunk_seq_id_head.clone(); + let perm_seq_id_chunks_tail: LB::Expr = perm_seq_id_chunks.clone() + n_chunks - LB::Expr::ONE; + let digest_addr_base: LB::Expr = LB::Expr::from(Felt::from(100u8)) * sponge_seq_id_head + + LB::Expr::from(Felt::from(3200u32)) * n_sponge_perms + - LB::Expr::from(Felt::from(128u8)); + + let cap_digest_chunks = Tag::CHUNKS.as_word().map(LB::Expr::from); + let cap_keccak = [ + LB::Expr::from(Keccak256Precompile::id()), + LB::Expr::from(Felt::from_u32(Keccak256Precompile::ASSERT_TAG_ID)), + len_bytes.clone(), + LB::Expr::ZERO, + ]; + + let d_rate0 = [d[0].clone(), d[1].clone(), d[2].clone(), d[3].clone()]; + let d_rate1 = [d[4].clone(), d[5].clone(), d[6].clone(), d[7].clone()]; + + frac_col!( + builder, + "handshake-and-chunks-digest", + provides_deg, + ( + "ks-request", + neg_act.clone(), + KeccakSpongeMsg { + sponge_seq_id: local[node::COL_SPONGE_SEQ_ID_HEAD].into(), + chunk_ptr: chunk_ptr_head, + len_bytes: len_bytes.clone() + }, + interaction_deg + ), + ); + frac_col!( + builder, + "handshake-and-chunks-digest", + pair_deg, + ( + "binding-truth", + neg_out_mult, + BindingMsg::truth(h_keccak.clone()), + interaction_deg + ), + ( + "chunk-chain", + pos_act.clone(), + ChunkChainMsg { + chunk_seq_id_head: chunk_seq_id_head.clone(), + perm_seq_id_head: perm_seq_id_chunks + }, + interaction_deg + ), + ); + frac_col!( + builder, + "handshake-and-chunks-digest", + provides_deg, + ( + "p2out-h-input-chunks", + pos_act.clone(), + Poseidon2OutMsg { + perm_seq_id: perm_seq_id_chunks_tail, + digest: h_input_chunks.clone() + }, + interaction_deg + ), + ); + + let addr_lane = + |j: u8| -> LB::Expr { digest_addr_base.clone() + LB::Expr::from(Felt::from(j)) }; + frac_col!( + builder, + "memory64-d-limbs", + pair_deg, + ( + "d-lane-0", + pos_act_x2.clone(), + Memory64Msg { + addr: addr_lane(0), + lo: d[0].clone(), + hi: d[1].clone() + }, + interaction_deg + ), + ( + "d-lane-1", + pos_act_x2.clone(), + Memory64Msg { + addr: addr_lane(1), + lo: d[2].clone(), + hi: d[3].clone() + }, + interaction_deg + ), + ); + frac_col!( + builder, + "memory64-d-limbs", + pair_deg, + ( + "d-lane-2", + pos_act_x2.clone(), + Memory64Msg { + addr: addr_lane(2), + lo: d[4].clone(), + hi: d[5].clone() + }, + interaction_deg + ), + ( + "d-lane-3", + pos_act_x2, + Memory64Msg { + addr: addr_lane(3), + lo: d[6].clone(), + hi: d[7].clone() + }, + interaction_deg + ), + ); + + frac_col!( + builder, + "digest-chunks-p2", + pair_deg, + ( + "p2in-rate0", + pos_act.clone(), + Poseidon2InMsg::rate0(perm_seq_id_digest_chunks.clone(), d_rate0), + interaction_deg + ), + ( + "p2in-rate1", + pos_act.clone(), + Poseidon2InMsg::rate1(perm_seq_id_digest_chunks.clone(), d_rate1), + interaction_deg + ), + ); + frac_col!( + builder, + "digest-chunks-p2", + pair_deg, + ( + "p2in-cap", + pos_act.clone(), + Poseidon2InMsg::cap(perm_seq_id_digest_chunks.clone(), cap_digest_chunks), + interaction_deg + ), + ( + "p2out-h-digest-chunks", + pos_act.clone(), + Poseidon2OutMsg { + perm_seq_id: perm_seq_id_digest_chunks, + digest: h_digest_chunks.clone() + }, + interaction_deg + ), + ); + + frac_col!( + builder, + "keccak-p2", + pair_deg, + ( + "p2in-rate0", + pos_act.clone(), + Poseidon2InMsg::rate0(perm_seq_id_keccak.clone(), h_input_chunks), + interaction_deg + ), + ( + "p2in-rate1", + pos_act.clone(), + Poseidon2InMsg::rate1(perm_seq_id_keccak.clone(), h_digest_chunks), + interaction_deg + ), + ); + frac_col!( + builder, + "keccak-p2", + pair_deg, + ( + "p2in-cap", + pos_act.clone(), + Poseidon2InMsg::cap(perm_seq_id_keccak.clone(), cap_keccak), + interaction_deg + ), + ( + "p2out-h-keccak", + pos_act, + Poseidon2OutMsg { + perm_seq_id: perm_seq_id_keccak, + digest: h_keccak + }, + interaction_deg + ), + ); +} diff --git a/crates/precompiles-prover/src/hash/chunk_node/trace.rs b/crates/precompiles-prover/src/hash/chunk_node/trace.rs deleted file mode 100644 index 2befe9989c..0000000000 --- a/crates/precompiles-prover/src/hash/chunk_node/trace.rs +++ /dev/null @@ -1,63 +0,0 @@ -//! Trace generation for the merged chunk + keccak-node chiplet. - -use alloc::vec::Vec; - -use miden_core::{ - Felt, - field::QuadFelt, - utils::{Matrix, RowMajorMatrix}, -}; - -use crate::{ - hash::{ - chunk::{ - self, - trace::{ChunkRequires, generate_trace_padded_to as chunk_trace}, - }, - chunk_node::{ChunkNodeAir, NODE_COL_OFFSET, NUM_MAIN_COLS}, - keccak::node::{ - self as node, - trace::{KeccakNodeRequires, generate_trace as node_trace}, - }, - }, - logup::build_logup_aux_trace, -}; - -/// Build the merged chunk + keccak-node main trace. Both sides run on -/// the same row range in disjoint column ranges (see the module doc), -/// so the shared height is `max` of what each side natively needs — the -/// keccak-node trace is computed first (its own padding is `act`-gated, -/// so zero-extending it is always sound), then chunk's own trace is -/// padded up to at least that height (chunk's `chunk_seq_id` / -/// `perm_seq_id` chains are unconditional, so it needs its own -/// continuation logic — see `chunk::trace::generate_trace_padded_to`). -pub fn generate_trace(chunk: ChunkRequires, node: KeccakNodeRequires) -> RowMajorMatrix { - let mut node_main = node_trace(node); - let node_height = node_main.height(); - let chunk_main = chunk_trace(chunk, node_height); - let height = chunk_main.height(); - node_main.values.resize(height * node::NUM_MAIN_COLS, Felt::ZERO); - - let mut vals = Vec::with_capacity(height * NUM_MAIN_COLS); - for r in 0..height { - vals.extend_from_slice( - &chunk_main.values[r * chunk::NUM_MAIN_COLS..(r + 1) * chunk::NUM_MAIN_COLS], - ); - vals.extend_from_slice( - &node_main.values[r * node::NUM_MAIN_COLS..(r + 1) * node::NUM_MAIN_COLS], - ); - } - debug_assert_eq!(vals.len(), height * NUM_MAIN_COLS); - debug_assert_eq!(NODE_COL_OFFSET, chunk::NUM_MAIN_COLS); - - RowMajorMatrix::new(vals, NUM_MAIN_COLS) -} - -/// Build the merged chiplet's aux trace via the generic -/// [`build_logup_aux_trace`] driver. -pub(crate) fn build_aux( - main: &RowMajorMatrix, - challenges: &[QuadFelt], -) -> (RowMajorMatrix, Vec) { - build_logup_aux_trace(&ChunkNodeAir, main, challenges) -} diff --git a/crates/precompiles-prover/src/hash/chunk_node_sponge/mod.rs b/crates/precompiles-prover/src/hash/chunk_node_sponge/mod.rs new file mode 100644 index 0000000000..3d6c5acc9e --- /dev/null +++ b/crates/precompiles-prover/src/hash/chunk_node_sponge/mod.rs @@ -0,0 +1,122 @@ +//! Composite AIR for the chunk, Keccak-node, and Keccak-sponge chiplets. +//! +//! The three components share a row range in disjoint column bands. Their +//! constraints and LogUp interactions delegate to the same offset-aware +//! evaluators used by the standalone component AIRs. + +pub mod trace; + +use alloc::vec::Vec; + +use miden_core::{Felt, field::QuadFelt, utils::RowMajorMatrix}; +use miden_lifted_air::{BaseAir, LiftedAir, LiftedAirBuilder}; + +use crate::{ + hash::{ + chunk_node, + keccak::sponge::{self, sponge_program}, + }, + logup::{ + CyclicConstraintLookupBuilder, LookupAir, LookupBuilder, NUM_PUBLIC_VALUES, NUM_RANDOMNESS, + NUM_SIGMA_VALUES, + }, + relations::{MAX_MESSAGE_WIDTH, NUM_BUS_IDS}, +}; + +/// First main-trace column of the sponge band. +pub const SPONGE_COL_OFFSET: usize = chunk_node::NUM_MAIN_COLS; + +pub const NUM_MAIN_COLS: usize = chunk_node::NUM_MAIN_COLS + sponge::NUM_MAIN_COLS; +pub const NUM_AUX_COLS: usize = chunk_node::NUM_AUX_COLS + sponge::NUM_AUX_COLS; + +const fn column_shape() -> [usize; NUM_AUX_COLS] { + let mut shape = [0usize; NUM_AUX_COLS]; + let mut i = 0; + while i < chunk_node::NUM_AUX_COLS { + shape[i] = chunk_node::COLUMN_SHAPE[i]; + i += 1; + } + let mut j = 0; + while j < sponge::NUM_AUX_COLS { + shape[chunk_node::NUM_AUX_COLS + j] = sponge::COLUMN_SHAPE[j]; + j += 1; + } + shape +} +const COLUMN_SHAPE: [usize; NUM_AUX_COLS] = column_shape(); + +#[derive(Debug, Default, Clone, Copy)] +pub struct ChunkNodeSpongeAir; + +impl BaseAir for ChunkNodeSpongeAir { + fn width(&self) -> usize { + NUM_MAIN_COLS + } + + fn num_public_values(&self) -> usize { + NUM_PUBLIC_VALUES + } + + fn periodic_columns(&self) -> Vec> { + sponge_program().to_vec() + } +} + +impl LiftedAir for ChunkNodeSpongeAir { + fn num_randomness(&self) -> usize { + NUM_RANDOMNESS + } + + fn aux_width(&self) -> usize { + NUM_AUX_COLS + } + + fn num_aux_values(&self) -> usize { + NUM_SIGMA_VALUES + } + + fn build_aux_trace( + &self, + main: &RowMajorMatrix, + _air_inputs: &[Felt], + _aux_inputs: &[Felt], + challenges: &[QuadFelt], + ) -> (RowMajorMatrix, Vec) { + trace::build_aux(main, challenges) + } + + fn eval>(&self, builder: &mut AB) { + chunk_node::eval_main(builder, 0); + sponge::eval_main(builder, SPONGE_COL_OFFSET); + + let mut lb = + CyclicConstraintLookupBuilder::new(builder, self, self.preprocessed_width() > 0); + >::eval(self, &mut lb); + } +} + +impl LookupAir for ChunkNodeSpongeAir +where + LB: LookupBuilder, +{ + fn num_columns(&self) -> usize { + NUM_AUX_COLS + } + + fn column_shape(&self) -> &[usize] { + &COLUMN_SHAPE + } + + fn max_message_width(&self) -> usize { + MAX_MESSAGE_WIDTH + } + + fn num_bus_ids(&self) -> usize { + NUM_BUS_IDS + } + + fn eval(&self, builder: &mut LB) { + chunk_node::eval_lookups(builder, 0); + sponge::eval_lookups(builder, SPONGE_COL_OFFSET); + } +} diff --git a/crates/precompiles-prover/src/hash/chunk_node_sponge/trace.rs b/crates/precompiles-prover/src/hash/chunk_node_sponge/trace.rs new file mode 100644 index 0000000000..50b45f11c0 --- /dev/null +++ b/crates/precompiles-prover/src/hash/chunk_node_sponge/trace.rs @@ -0,0 +1,78 @@ +//! Trace generation for the merged chunk + keccak-node + keccak-sponge +//! chiplet. + +use alloc::vec::Vec; + +use miden_core::{ + Felt, + field::QuadFelt, + utils::{Matrix, RowMajorMatrix}, +}; + +use crate::{ + hash::{ + chunk::{ + self, + trace::{ChunkRequires, generate_trace_padded_to as chunk_trace}, + }, + chunk_node_sponge::{ChunkNodeSpongeAir, NUM_MAIN_COLS}, + keccak::{ + node::{ + self as node, + trace::{KeccakNodeRequires, generate_trace as node_trace}, + }, + sponge::{ + self as sponge, + trace::{SpongeRequires, generate_trace_padded_to as sponge_trace}, + }, + }, + }, + logup::build_logup_aux_trace, +}; + +/// Build the merged main trace at the largest component height. Node rows +/// can be zero-extended because they are activity-gated; chunk and sponge +/// use their own padding generators to preserve unconditional chains. +pub fn generate_trace( + chunk: ChunkRequires, + node: KeccakNodeRequires, + sponge: SpongeRequires, +) -> RowMajorMatrix { + let mut node_main = node_trace(node); + let node_height = node_main.height(); + let sponge_main = sponge_trace(sponge, node_height); + let chunk_main = chunk_trace(chunk, sponge_main.height()); + let height = chunk_main.height(); + // The sponge uses at least 32 rows per invocation and therefore + // dominates the chunk trace's ceil(len / 32) rows. + assert_eq!( + height, + sponge_main.height(), + "the sponge band's height must dominate the chunk band's" + ); + node_main.values.resize(height * node::NUM_MAIN_COLS, Felt::ZERO); + + let mut vals = Vec::with_capacity(height * NUM_MAIN_COLS); + for r in 0..height { + vals.extend_from_slice( + &chunk_main.values[r * chunk::NUM_MAIN_COLS..(r + 1) * chunk::NUM_MAIN_COLS], + ); + vals.extend_from_slice( + &node_main.values[r * node::NUM_MAIN_COLS..(r + 1) * node::NUM_MAIN_COLS], + ); + vals.extend_from_slice( + &sponge_main.values[r * sponge::NUM_MAIN_COLS..(r + 1) * sponge::NUM_MAIN_COLS], + ); + } + debug_assert_eq!(vals.len(), height * NUM_MAIN_COLS); + + RowMajorMatrix::new(vals, NUM_MAIN_COLS) +} + +/// Build the merged chiplet's LogUp trace. +pub(crate) fn build_aux( + main: &RowMajorMatrix, + challenges: &[QuadFelt], +) -> (RowMajorMatrix, Vec) { + build_logup_aux_trace(&ChunkNodeSpongeAir, main, challenges) +} diff --git a/crates/precompiles-prover/src/hash/keccak/node/mod.rs b/crates/precompiles-prover/src/hash/keccak/node/mod.rs index 39d5f98916..7d5b43fab8 100644 --- a/crates/precompiles-prover/src/hash/keccak/node/mod.rs +++ b/crates/precompiles-prover/src/hash/keccak/node/mod.rs @@ -171,7 +171,7 @@ pub const NUM_MAIN_COLS: usize = COL_OUT_MULT + 1; /// - col 7/8: keccak-node P2 perm — `Poseidon2In` rate0+rate1, then cap + `Poseidon2Out(H_keccak)`. pub const NUM_AUX_COLS: usize = 9; -const COLUMN_SHAPE: [usize; NUM_AUX_COLS] = [1, 2, 1, 2, 2, 2, 2, 2, 2]; +pub(crate) const COLUMN_SHAPE: [usize; NUM_AUX_COLS] = [1, 2, 1, 2, 2, 2, 2, 2, 2]; // AIR // ================================================================================================ diff --git a/crates/precompiles-prover/src/hash/keccak/round/mod.rs b/crates/precompiles-prover/src/hash/keccak/round/mod.rs index a6e8f63d07..41bb43786c 100644 --- a/crates/precompiles-prover/src/hash/keccak/round/mod.rs +++ b/crates/precompiles-prover/src/hash/keccak/round/mod.rs @@ -126,9 +126,10 @@ fn interleave_lanes(lane_cells: &[Vec; NUM_LANES], height: usize) -> RowMa // AUX COLUMN LAYOUT // ================================================================================================ -/// FLATTENED to lqd 1, repeated per lane: each lane's 10-column band holds -/// 19 fractions (all degree-≤2 multiplicities) split ≤ 2 per column, the -/// band's col 0 a single fraction: +/// Flattened running-sum layout, repeated per lane: each lane's 10-column band holds +/// 19 fractions split ≤ 2 per column, the band's col 0 a single fraction. The flattening does not +/// bring this AIR to `log_quotient_degree = 1`; it derives 2 because the memory64 destination +/// fraction carries degree 5 (see `dst_deg` in the lookup evaluator): /// - band col 0: memory64 dst provide. /// - band col 1: memory64 `src_a` + `src_b` requires. /// - band cols 2–5: 8 `BytePairLut` byte requires verifying `r = a OP b` (or `r = a` on pure-ROL @@ -356,14 +357,14 @@ fn memory_provide_c, V: Copy + Into>( // LOOKUP AIR // ================================================================================================ -/// Aux column shape (FLATTENED to lqd 1), repeated per lane (band-local): -/// - band col 0: memory64 dst provide (one degree-≤3 fraction; lane 0's is the running sum). +/// Aux column shape, repeated per lane (band-local): +/// - band col 0: memory64 dst provide (lane 0's is the running sum). /// - band col 1: memory64 `src_a` + `src_b` requires. /// - band cols 2–5: 8 `BytePairLut` byte requires, two per column. /// - band cols 6–9: 8 `Range16` requires on `rot_limbs`, two per column. /// -/// Every closing constraint is degree ≤ 3, so `log_quotient_degree = 1` -/// (aux blowup factor = 2). Width disregarded. +/// This AIR derives `log_quotient_degree = 2`: the memory64 destination fraction below carries +/// `Deg { v: 5, .. }`. The symbolic derivation is authoritative; trace width does not enter it. const COLUMN_SHAPE: [usize; NUM_AUX_COLS] = build_column_shape(); const fn build_column_shape() -> [usize; NUM_AUX_COLS] { diff --git a/crates/precompiles-prover/src/hash/keccak/sponge/mod.rs b/crates/precompiles-prover/src/hash/keccak/sponge/mod.rs index 6e57066ccf..16c254b0b4 100644 --- a/crates/precompiles-prover/src/hash/keccak/sponge/mod.rs +++ b/crates/precompiles-prover/src/hash/keccak/sponge/mod.rs @@ -318,7 +318,7 @@ pub const PAD_CONST_BYTES: [u8; 8] = [0, 0, 0, 0, 0, 0, 0, 0x80]; /// halves are `lo`/`hi`. Extracts from the already-verified `_LO`/`_HI` /// per-`byte_offset` mask constants, so the per-byte view is correct by /// construction rather than a hand-rederived bit pattern. -const fn mask_byte(lo: u32, hi: u32, byte_idx: usize) -> u8 { +pub(crate) const fn mask_byte(lo: u32, hi: u32, byte_idx: usize) -> u8 { let word = if byte_idx < 4 { lo } else { hi }; ((word >> (8 * (byte_idx % 4))) & 0xff) as u8 } @@ -350,266 +350,266 @@ impl LiftedAir for KeccakSpongeAir { } fn eval>(&self, builder: &mut AB) { - // Phase 1: local row constraints. - let local: [AB::Var; NUM_MAIN_COLS] = current_main(builder.main(), 0); - // Next-row window: the same 27 columns at row r+1. Cyclic at - // row N-1 (`when_transition` gates out the wrap explicitly - // where needed; other transition constraints rely on - // `p_last`/`p_rate_block` factors making the wrap vacuous). - let next: [AB::Var; NUM_MAIN_COLS] = next_main(builder.main(), 0); - - let periodic = builder.periodic_values(); - let p_first: AB::Expr = periodic[PCOL_FIRST].into(); - let p_last: AB::Expr = periodic[PCOL_LAST].into(); - let p_rate_block: AB::Expr = periodic[PCOL_RATE_BLOCK].into(); - let p_capacity: AB::Expr = periodic[PCOL_CAPACITY].into(); - let p_extra: AB::Expr = periodic[PCOL_EXTRA].into(); - let p_state_lane: AB::Expr = p_rate_block.clone() + p_capacity.clone(); - - // Frequently-used local / next-row expressions. - let act: AB::Expr = local[COL_ACT].into(); - let act_next: AB::Expr = next[COL_ACT].into(); - let sponge_seq_id: AB::Expr = local[COL_SPONGE_SEQ_ID].into(); - let sponge_seq_id_next: AB::Expr = next[COL_SPONGE_SEQ_ID].into(); - let bytes_left: AB::Expr = local[COL_BYTES_LEFT].into(); - let bytes_left_next: AB::Expr = next[COL_BYTES_LEFT].into(); - let chunk_ptr: AB::Expr = local[COL_CHUNK_PTR].into(); - let chunk_ptr_next: AB::Expr = next[COL_CHUNK_PTR].into(); - let is_first_block: AB::Expr = local[COL_IS_FIRST_BLOCK_OF_INVOCATION].into(); - let is_first_block_next: AB::Expr = next[COL_IS_FIRST_BLOCK_OF_INVOCATION].into(); - let is_zero: AB::Expr = local[COL_IS_ZERO].into(); - let is_zero_next: AB::Expr = next[COL_IS_ZERO].into(); - let is_chunk_avail: AB::Expr = local[COL_IS_CHUNK_AVAIL].into(); - let is_chunk_avail_next: AB::Expr = next[COL_IS_CHUNK_AVAIL].into(); - let state_prev_lo: AB::Expr = local[COL_STATE_PREV_LO].into(); - let state_prev_hi: AB::Expr = local[COL_STATE_PREV_HI].into(); - let state_new_lo: AB::Expr = local[COL_STATE_NEW_LO].into(); - let state_new_hi: AB::Expr = local[COL_STATE_NEW_HI].into(); - - // Σ b_j (= `is_last_block_period`) and Σ j·b_j (= byte_offset). - let mut b_sum = AB::Expr::ZERO; - let mut b_weighted = AB::Expr::ZERO; - for (j, col) in COL_B_RANGE.enumerate() { - let b_j: AB::Expr = local[col].into(); - b_sum += b_j.clone(); - b_weighted += AB::Expr::from(Felt::from(j as u32)) * b_j; - } - - // Boundary (`when_first_row`) --------------------------- - // `sponge_seq_id` starts at 0 (row counter convention). No - // `chunk_ptr` boundary: the chunk-tape base is pinned per - // invocation by the `KeccakSponge` request (the first - // invocation supplies base 0 by convention), and the chain is - // relaxed at invocation seams — see the `chunk_ptr` chain below. - builder.when_first_row().assert_zero(sponge_seq_id.clone()); - - // Activity ---------------------------------------------- - // Binary: act ∈ {0, 1}. Deg 2. - builder.assert_bool(local[COL_ACT]); - // Sticky-downward: forbids 0 → 1 within [0, N-2]. The cyclic - // wrap is intentionally unconstrained so a 1's-prefix / 0's- - // suffix trace cycles back to `act_0 = 1` on the next loop. - builder - .when_transition() - .assert_zero((AB::Expr::ONE - act.clone()) * act_next.clone()); - // Drop placement: the unique 1 → 0 transition must land at - // slot 31 (where `p_last = 1`) of a last-block period - // (`Σ b_j = 1`). Equivalent to `act · (1 - act')` under the - // sticky-down constraint above; the linear form costs one - // fewer witness multiplication. - builder.when_transition().assert_zero( - (act.clone() - act_next) * (AB::Expr::ONE - p_last.clone() * b_sum.clone()), - ); - - // Row counter ------------------------------------------- - // sponge_seq_id' - sponge_seq_id - 1 = 0. Deg 1. - // `when_transition` keeps the cyclic wrap (which would force - // sponge_seq_id_0 = N) unconstrained. - builder - .when_transition() - .assert_zero(sponge_seq_id_next - sponge_seq_id - AB::Expr::ONE); - - // `is_first_block_of_invocation` structure -------------- - builder.assert_bool(local[COL_IS_FIRST_BLOCK_OF_INVOCATION]); - // Constant within period. `(1 - p_last)` makes the wrap - // vacuous (p_last_{N-1} = 1) and lets `is_first_block` toggle - // at period boundaries. - builder.assert_zero( - (AB::Expr::ONE - p_last.clone()) - * (is_first_block_next.clone() - is_first_block.clone()), - ); + eval_main(builder, 0); - // `bytes_left` decrement chain -------------------------- - // Both branches are gated by `act`: on dead rows `bytes_left` is - // unconstrained, so the all-dead (zero-invocation) trace is - // admissible — the only valid empty-transcript trace (see - // the design notes §`bytes_left` decrement chain). - // On active rows the chain is identical, so it still forbids the - // `act = 1 ∧ is_first_block = 0` cyclic-fixed-point forgery via the - // `M · 136 ≢ 0 mod p` argument (`act` doesn't weaken it — the forgery - // it rules out is fully active). Dead rows are bus-inert, so leaving - // `bytes_left` free there is sound. - // - // Absorb row (`p_rate_block = 1`): decrements by 8. - builder.assert_zero( - act.clone() - * p_rate_block.clone() - * (bytes_left_next.clone() - bytes_left.clone() + AB::Expr::from(Felt::from(8u8))), - ); - // Non-absorb row + no invocation boundary at next row: holds steady. - let enters_new_invocation = p_last.clone() * is_first_block_next.clone(); - builder.assert_zero( - act.clone() - * (AB::Expr::ONE - enters_new_invocation.clone()) - * (AB::Expr::ONE - p_rate_block.clone()) - * (bytes_left_next - bytes_left.clone()), - ); - - // `chunk_ptr` increment chain --------------------------- - // Within an invocation: chunk_ptr' - chunk_ptr - - // (p_rate_block + p_extra · b_sum) · is_chunk_avail = 0 (advance - // by 1 per consumed chunk lane). Rate rows consume on every - // block; the extra rows consume the last block's overshoot - // lanes (gated to the last block by `b_sum`), so `chunk_ptr` - // walks all 4·num_chunks tape lanes contiguously. Gated off at - // invocation seams (`enters_new_invocation`), where the - // `KeccakSponge` request re-pins chunk_ptr to the next - // invocation's chunk-tape base. No global enumeration from 0 — - // per-invocation overlap/gap freedom is enforced by Memory64 - // bus balance against the chunk chiplet's contiguous emissions, - // not by the chain. `when_transition` also keeps the cyclic - // wrap unconstrained. - builder.when_transition().assert_zero( - (AB::Expr::ONE - enters_new_invocation) - * (chunk_ptr_next - - chunk_ptr - - (p_rate_block.clone() + p_extra * b_sum.clone()) * is_chunk_avail.clone()), - ); - - // Chunk zero-fill on `is_chunk_avail = 0` -------------- - // When the chunk chiplet doesn't provide at this row, pin - // `chunk_lo = chunk_hi = 0` so the witness is canonical and - // pre-pad verbatim XORs can't be steered by a - // prover-chosen unpinned chunk value. Effect: any - // under-emission by the chunk chiplet yields a deterministic - // zero-extended digest, caught by the downstream digest - // check at the transcript chiplet. Ungated — pinning chunk - // to 0 on non-rate / dead rows is benign since those rows - // never consume the chunk columns elsewhere. - let chunk_lo_local: AB::Expr = local[COL_CHUNK_LO].into(); - let chunk_hi_local: AB::Expr = local[COL_CHUNK_HI].into(); - builder.assert_zero((AB::Expr::ONE - is_chunk_avail.clone()) * chunk_lo_local); - builder.assert_zero((AB::Expr::ONE - is_chunk_avail.clone()) * chunk_hi_local); - - // Padding state machine --------------------------------- - // Binarity. - builder.assert_bool(local[COL_IS_ZERO]); - builder.assert_bool(local[COL_IS_CHUNK_AVAIL]); - for col in COL_B_RANGE { - builder.assert_bool(local[col]); - } - - // `is_zero` non-decreasing within period. - builder.assert_zero( - (AB::Expr::ONE - p_last.clone()) - * is_zero.clone() - * (AB::Expr::ONE - is_zero_next.clone()), - ); - // `is_chunk_avail` non-increasing within period. - builder.assert_zero( - (AB::Expr::ONE - p_last.clone()) - * (AB::Expr::ONE - is_chunk_avail) - * is_chunk_avail_next, - ); - // Period boundary: pad hasn't fired yet at slot 0. - builder.assert_zero(p_first * is_zero.clone()); - // Selector bits constant within period. - for col in COL_B_RANGE { - let b_j: AB::Expr = local[col].into(); - let b_j_next: AB::Expr = next[col].into(); - builder.assert_zero((AB::Expr::ONE - p_last.clone()) * (b_j_next - b_j)); - } - // Selector sum ties to `is_zero` on non-absorb rows. - builder.assert_zero( - (AB::Expr::ONE - p_rate_block.clone()) * (b_sum.clone() - is_zero.clone()), - ); - - // Pad-must-fire (gated by `act`) ------------------------ - // At slot 31 of any *active* period followed by a new - // invocation, force `is_zero = 1` (the pad fired earlier in - // this period) — i.e. a new invocation may only start right - // after a last block, so no invocation is truncated. Covers - // active→active seams. The last active invocation's last block - // is instead pinned by `act` drop placement (act may drop only - // after a `b_sum = 1` period). The `act` gate makes the cyclic - // wrap from the trailing dead pad region into row 0 vacuous - // (dead rows carry `is_zero = 0`), so an invocation set whose - // total block count isn't a power of two — padded out with dead - // rows — is admissible. Without the gate the wrap would demand - // `is_zero = 1` on the final dead row. - builder.assert_zero(act * p_last * is_first_block_next * (AB::Expr::ONE - is_zero.clone())); - - // Pad-lane tie-down ------------------------------------- - // On the unique pad transition row (`p_rate_block = 1`, - // `is_pad = 1`), pin `byte_offset = bytes_left`. Vacuous - // everywhere else. The `p_rate_block` gate also absorbs - // the period-wrap `is_pad = −1` case, which always lands - // on `p_idx = 31` where `p_rate_block = 0`. - let is_pad: AB::Expr = is_zero_next - is_zero.clone(); - builder.assert_zero(p_rate_block.clone() * is_pad * (b_weighted - bytes_left)); - - // state_prev = 0 on first-block state-lane rows --------- - builder.assert_zero(p_state_lane.clone() * is_first_block.clone() * state_prev_lo.clone()); - builder.assert_zero(p_state_lane * is_first_block * state_prev_hi.clone()); - - // State propagation (no BytePairLut request fires) -------- - // Past-pad rate XORin rows: `state_new = state_prev`. - builder.assert_zero( - p_rate_block.clone() * is_zero.clone() * (state_new_lo.clone() - state_prev_lo.clone()), - ); - builder - .assert_zero(p_rate_block * is_zero * (state_new_hi.clone() - state_prev_hi.clone())); - // Capacity rows: identity passthrough. - builder.assert_zero(p_capacity.clone() * (state_new_lo.clone() - state_prev_lo.clone())); - builder.assert_zero(p_capacity * (state_new_hi.clone() - state_prev_hi.clone())); - - // Byte-shadow linking (ungated) -------------------------- - // Every `_lo`/`_hi` pair below also has an 8-byte little-endian - // shadow (used by the `BytePairLut` requires in Phase 2, which - // range-check and byte-verify the pad/absorb XOR/ANDNOT ops - // directly). Without this link the byte columns would be a - // second, independent free witness disconnected from the halves - // every other bus message (Memory64 prev-perm consume, new-state - // provide, chunk consume) actually reads — pinning them together - // is what makes a `BytePairLut`-verified byte result also the - // value committed elsewhere. Ungated: both sides are otherwise - // free witness on rows where the value is unused, so an honest - // prover always satisfies this by construction. - let chunk_lo: AB::Expr = local[COL_CHUNK_LO].into(); - let chunk_hi: AB::Expr = local[COL_CHUNK_HI].into(); - let cleared_lo: AB::Expr = local[COL_CLEARED_LO].into(); - let cleared_hi: AB::Expr = local[COL_CLEARED_HI].into(); - let padded_lo: AB::Expr = local[COL_PADDED_LO].into(); - let padded_hi: AB::Expr = local[COL_PADDED_HI].into(); - let link = |builder: &mut AB, range: Range, lo: AB::Expr, hi: AB::Expr| { - let bytes: [AB::Var; 8] = array::from_fn(|i| local[range.start + i]); - let [lo_from_bytes, hi_from_bytes]: [AB::Expr; 2] = halves_le(&bytes, 256); - builder.assert_zero(lo_from_bytes - lo); - builder.assert_zero(hi_from_bytes - hi); - }; - link(builder, CHUNK_BYTES_RANGE, chunk_lo, chunk_hi); - link(builder, STATE_PREV_BYTES_RANGE, state_prev_lo, state_prev_hi); - link(builder, STATE_NEW_BYTES_RANGE, state_new_lo, state_new_hi); - link(builder, CLEARED_BYTES_RANGE, cleared_lo, cleared_hi); - link(builder, PADDED_BYTES_RANGE, padded_lo, padded_hi); - - // Phase 2: LogUp argument via the LogUp adapter. + // Phase 2: LogUp. let mut lb = CyclicConstraintLookupBuilder::new(builder, self, self.preprocessed_width() > 0); >::eval(self, &mut lb); } } +/// Evaluate this component's base constraints in a main-trace column band. +pub(crate) fn eval_main(builder: &mut AB, main_col_offset: usize) +where + AB: LiftedAirBuilder, +{ + // Phase 1: local row constraints. + let local: [AB::Var; NUM_MAIN_COLS] = current_main(builder.main(), main_col_offset); + // Next-row window: the same 67 columns at row r+1. Cyclic at + // row N-1 (`when_transition` gates out the wrap explicitly + // where needed; other transition constraints rely on + // `p_last`/`p_rate_block` factors making the wrap vacuous). + let next: [AB::Var; NUM_MAIN_COLS] = next_main(builder.main(), main_col_offset); + + let periodic = builder.periodic_values(); + let p_first: AB::Expr = periodic[PCOL_FIRST].into(); + let p_last: AB::Expr = periodic[PCOL_LAST].into(); + let p_rate_block: AB::Expr = periodic[PCOL_RATE_BLOCK].into(); + let p_capacity: AB::Expr = periodic[PCOL_CAPACITY].into(); + let p_extra: AB::Expr = periodic[PCOL_EXTRA].into(); + let p_state_lane: AB::Expr = p_rate_block.clone() + p_capacity.clone(); + + // Frequently-used local / next-row expressions. + let act: AB::Expr = local[COL_ACT].into(); + let act_next: AB::Expr = next[COL_ACT].into(); + let sponge_seq_id: AB::Expr = local[COL_SPONGE_SEQ_ID].into(); + let sponge_seq_id_next: AB::Expr = next[COL_SPONGE_SEQ_ID].into(); + let bytes_left: AB::Expr = local[COL_BYTES_LEFT].into(); + let bytes_left_next: AB::Expr = next[COL_BYTES_LEFT].into(); + let chunk_ptr: AB::Expr = local[COL_CHUNK_PTR].into(); + let chunk_ptr_next: AB::Expr = next[COL_CHUNK_PTR].into(); + let is_first_block: AB::Expr = local[COL_IS_FIRST_BLOCK_OF_INVOCATION].into(); + let is_first_block_next: AB::Expr = next[COL_IS_FIRST_BLOCK_OF_INVOCATION].into(); + let is_zero: AB::Expr = local[COL_IS_ZERO].into(); + let is_zero_next: AB::Expr = next[COL_IS_ZERO].into(); + let is_chunk_avail: AB::Expr = local[COL_IS_CHUNK_AVAIL].into(); + let is_chunk_avail_next: AB::Expr = next[COL_IS_CHUNK_AVAIL].into(); + let state_prev_lo: AB::Expr = local[COL_STATE_PREV_LO].into(); + let state_prev_hi: AB::Expr = local[COL_STATE_PREV_HI].into(); + let state_new_lo: AB::Expr = local[COL_STATE_NEW_LO].into(); + let state_new_hi: AB::Expr = local[COL_STATE_NEW_HI].into(); + + // Σ b_j (= `is_last_block_period`) and Σ j·b_j (= byte_offset). + let mut b_sum = AB::Expr::ZERO; + let mut b_weighted = AB::Expr::ZERO; + for (j, col) in COL_B_RANGE.enumerate() { + let b_j: AB::Expr = local[col].into(); + b_sum += b_j.clone(); + b_weighted += AB::Expr::from(Felt::from(j as u32)) * b_j; + } + + // Boundary (`when_first_row`) --------------------------- + // `sponge_seq_id` starts at 0 (row counter convention). No + // `chunk_ptr` boundary: the chunk-tape base is pinned per + // invocation by the `KeccakSponge` request (the first + // invocation supplies base 0 by convention), and the chain is + // relaxed at invocation seams — see the `chunk_ptr` chain below. + builder.when_first_row().assert_zero(sponge_seq_id.clone()); + + // Activity ---------------------------------------------- + // Binary: act ∈ {0, 1}. Deg 2. + builder.assert_bool(local[COL_ACT]); + // Sticky-downward: forbids 0 → 1 within [0, N-2]. The cyclic + // wrap is intentionally unconstrained so a 1's-prefix / 0's- + // suffix trace cycles back to `act_0 = 1` on the next loop. + builder + .when_transition() + .assert_zero((AB::Expr::ONE - act.clone()) * act_next.clone()); + // Drop placement: the unique 1 → 0 transition must land at + // slot 31 (where `p_last = 1`) of a last-block period + // (`Σ b_j = 1`). Equivalent to `act · (1 - act')` under the + // sticky-down constraint above; the linear form costs one + // fewer witness multiplication. + builder + .when_transition() + .assert_zero((act.clone() - act_next) * (AB::Expr::ONE - p_last.clone() * b_sum.clone())); + + // Row counter ------------------------------------------- + // sponge_seq_id' - sponge_seq_id - 1 = 0. Deg 1. + // `when_transition` keeps the cyclic wrap (which would force + // sponge_seq_id_0 = N) unconstrained. + builder + .when_transition() + .assert_zero(sponge_seq_id_next - sponge_seq_id - AB::Expr::ONE); + + // `is_first_block_of_invocation` structure -------------- + builder.assert_bool(local[COL_IS_FIRST_BLOCK_OF_INVOCATION]); + // Constant within period. `(1 - p_last)` makes the wrap + // vacuous (p_last_{N-1} = 1) and lets `is_first_block` toggle + // at period boundaries. + builder.assert_zero( + (AB::Expr::ONE - p_last.clone()) * (is_first_block_next.clone() - is_first_block.clone()), + ); + + // `bytes_left` decrement chain -------------------------- + // Both branches are gated by `act`: on dead rows `bytes_left` is + // unconstrained, so the all-dead (zero-invocation) trace is + // admissible — the only valid empty-transcript trace (see + // the design notes §`bytes_left` decrement chain). + // On active rows the chain is identical, so it still forbids the + // `act = 1 ∧ is_first_block = 0` cyclic-fixed-point forgery via the + // `M · 136 ≢ 0 mod p` argument (`act` doesn't weaken it — the forgery + // it rules out is fully active). Dead rows are bus-inert, so leaving + // `bytes_left` free there is sound. + // + // Absorb row (`p_rate_block = 1`): decrements by 8. + builder.assert_zero( + act.clone() + * p_rate_block.clone() + * (bytes_left_next.clone() - bytes_left.clone() + AB::Expr::from(Felt::from(8u8))), + ); + // Non-absorb row + no invocation boundary at next row: holds steady. + let enters_new_invocation = p_last.clone() * is_first_block_next.clone(); + builder.assert_zero( + act.clone() + * (AB::Expr::ONE - enters_new_invocation.clone()) + * (AB::Expr::ONE - p_rate_block.clone()) + * (bytes_left_next - bytes_left.clone()), + ); + + // `chunk_ptr` increment chain --------------------------- + // Within an invocation: chunk_ptr' - chunk_ptr - + // (p_rate_block + p_extra · b_sum) · is_chunk_avail = 0 (advance + // by 1 per consumed chunk lane). Rate rows consume on every + // block; the extra rows consume the last block's overshoot + // lanes (gated to the last block by `b_sum`), so `chunk_ptr` + // walks all 4·num_chunks tape lanes contiguously. Gated off at + // invocation seams (`enters_new_invocation`), where the + // `KeccakSponge` request re-pins chunk_ptr to the next + // invocation's chunk-tape base. No global enumeration from 0 — + // per-invocation overlap/gap freedom is enforced by Memory64 + // bus balance against the chunk chiplet's contiguous emissions, + // not by the chain. `when_transition` also keeps the cyclic + // wrap unconstrained. + builder.when_transition().assert_zero( + (AB::Expr::ONE - enters_new_invocation) + * (chunk_ptr_next + - chunk_ptr + - (p_rate_block.clone() + p_extra * b_sum.clone()) * is_chunk_avail.clone()), + ); + + // Chunk zero-fill on `is_chunk_avail = 0` -------------- + // When the chunk chiplet doesn't provide at this row, pin + // `chunk_lo = chunk_hi = 0` so the witness is canonical and + // pre-pad verbatim XORs can't be steered by a + // prover-chosen unpinned chunk value. Effect: any + // under-emission by the chunk chiplet yields a deterministic + // zero-extended digest, caught by the downstream digest + // check at the transcript chiplet. Ungated — pinning chunk + // to 0 on non-rate / dead rows is benign since those rows + // never consume the chunk columns elsewhere. + let chunk_lo_local: AB::Expr = local[COL_CHUNK_LO].into(); + let chunk_hi_local: AB::Expr = local[COL_CHUNK_HI].into(); + builder.assert_zero((AB::Expr::ONE - is_chunk_avail.clone()) * chunk_lo_local); + builder.assert_zero((AB::Expr::ONE - is_chunk_avail.clone()) * chunk_hi_local); + + // Padding state machine --------------------------------- + // Binarity. + builder.assert_bool(local[COL_IS_ZERO]); + builder.assert_bool(local[COL_IS_CHUNK_AVAIL]); + for col in COL_B_RANGE { + builder.assert_bool(local[col]); + } + + // `is_zero` non-decreasing within period. + builder.assert_zero( + (AB::Expr::ONE - p_last.clone()) * is_zero.clone() * (AB::Expr::ONE - is_zero_next.clone()), + ); + // `is_chunk_avail` non-increasing within period. + builder.assert_zero( + (AB::Expr::ONE - p_last.clone()) * (AB::Expr::ONE - is_chunk_avail) * is_chunk_avail_next, + ); + // Period boundary: pad hasn't fired yet at slot 0. + builder.assert_zero(p_first * is_zero.clone()); + // Selector bits constant within period. + for col in COL_B_RANGE { + let b_j: AB::Expr = local[col].into(); + let b_j_next: AB::Expr = next[col].into(); + builder.assert_zero((AB::Expr::ONE - p_last.clone()) * (b_j_next - b_j)); + } + // Selector sum ties to `is_zero` on non-absorb rows. + builder.assert_zero((AB::Expr::ONE - p_rate_block.clone()) * (b_sum.clone() - is_zero.clone())); + + // Pad-must-fire (gated by `act`) ------------------------ + // At slot 31 of any *active* period followed by a new + // invocation, force `is_zero = 1` (the pad fired earlier in + // this period) — i.e. a new invocation may only start right + // after a last block, so no invocation is truncated. Covers + // active→active seams. The last active invocation's last block + // is instead pinned by `act` drop placement (act may drop only + // after a `b_sum = 1` period). The `act` gate makes the cyclic + // wrap from the trailing dead pad region into row 0 vacuous + // (dead rows carry `is_zero = 0`), so an invocation set whose + // total block count isn't a power of two — padded out with dead + // rows — is admissible. Without the gate the wrap would demand + // `is_zero = 1` on the final dead row. + builder.assert_zero(act * p_last * is_first_block_next * (AB::Expr::ONE - is_zero.clone())); + + // Pad-lane tie-down ------------------------------------- + // On the unique pad transition row (`p_rate_block = 1`, + // `is_pad = 1`), pin `byte_offset = bytes_left`. Vacuous + // everywhere else. The `p_rate_block` gate also absorbs + // the period-wrap `is_pad = −1` case, which always lands + // on `p_idx = 31` where `p_rate_block = 0`. + let is_pad: AB::Expr = is_zero_next - is_zero.clone(); + builder.assert_zero(p_rate_block.clone() * is_pad * (b_weighted - bytes_left)); + + // state_prev = 0 on first-block state-lane rows --------- + builder.assert_zero(p_state_lane.clone() * is_first_block.clone() * state_prev_lo.clone()); + builder.assert_zero(p_state_lane * is_first_block * state_prev_hi.clone()); + + // State propagation (no BytePairLut request fires) -------- + // Past-pad rate XORin rows: `state_new = state_prev`. + builder.assert_zero( + p_rate_block.clone() * is_zero.clone() * (state_new_lo.clone() - state_prev_lo.clone()), + ); + builder.assert_zero(p_rate_block * is_zero * (state_new_hi.clone() - state_prev_hi.clone())); + // Capacity rows: identity passthrough. + builder.assert_zero(p_capacity.clone() * (state_new_lo.clone() - state_prev_lo.clone())); + builder.assert_zero(p_capacity * (state_new_hi.clone() - state_prev_hi.clone())); + + // Byte-shadow linking (ungated) -------------------------- + // Every `_lo`/`_hi` pair below also has an 8-byte little-endian + // shadow (used by the `BytePairLut` requires in Phase 2, which + // range-check and byte-verify the pad/absorb XOR/ANDNOT ops + // directly). Without this link the byte columns would be a + // second, independent free witness disconnected from the halves + // every other bus message (Memory64 prev-perm consume, new-state + // provide, chunk consume) actually reads — pinning them together + // is what makes a `BytePairLut`-verified byte result also the + // value committed elsewhere. Ungated: both sides are otherwise + // free witness on rows where the value is unused, so an honest + // prover always satisfies this by construction. + let chunk_lo: AB::Expr = local[COL_CHUNK_LO].into(); + let chunk_hi: AB::Expr = local[COL_CHUNK_HI].into(); + let cleared_lo: AB::Expr = local[COL_CLEARED_LO].into(); + let cleared_hi: AB::Expr = local[COL_CLEARED_HI].into(); + let padded_lo: AB::Expr = local[COL_PADDED_LO].into(); + let padded_hi: AB::Expr = local[COL_PADDED_HI].into(); + let link = |builder: &mut AB, range: Range, lo: AB::Expr, hi: AB::Expr| { + let bytes: [AB::Var; 8] = array::from_fn(|i| local[range.start + i]); + let [lo_from_bytes, hi_from_bytes]: [AB::Expr; 2] = halves_le(&bytes, 256); + builder.assert_zero(lo_from_bytes - lo); + builder.assert_zero(hi_from_bytes - hi); + }; + link(builder, CHUNK_BYTES_RANGE, chunk_lo, chunk_hi); + link(builder, STATE_PREV_BYTES_RANGE, state_prev_lo, state_prev_hi); + link(builder, STATE_NEW_BYTES_RANGE, state_new_lo, state_new_hi); + link(builder, CLEARED_BYTES_RANGE, cleared_lo, cleared_hi); + link(builder, PADDED_BYTES_RANGE, padded_lo, padded_hi); +} + // LOOKUP AIR // ================================================================================================ @@ -619,7 +619,7 @@ impl LiftedAir for KeccakSpongeAir { /// closing constraint is degree ≤ 5. The chunk-consume fires on rate rows /// and, on the last block, the extra rows [26,29) that mop up overshoot /// lanes (gated by `p_extra · b_sum`). -const COLUMN_SHAPE: [usize; NUM_AUX_COLS] = build_column_shape(); +pub(crate) const COLUMN_SHAPE: [usize; NUM_AUX_COLS] = build_column_shape(); const fn build_column_shape() -> [usize; NUM_AUX_COLS] { let mut shape = [2usize; NUM_AUX_COLS]; @@ -651,398 +651,402 @@ where } fn eval(&self, builder: &mut LB) { - let local: [LB::Var; NUM_MAIN_COLS] = current_main(builder.main(), 0); - let next: [LB::Var; NUM_MAIN_COLS] = next_main(builder.main(), 0); - let periodic = builder.periodic_values(); - let p_first: LB::Expr = periodic[PCOL_FIRST].into(); - let p_rate_block: LB::Expr = periodic[PCOL_RATE_BLOCK].into(); - let p_capacity: LB::Expr = periodic[PCOL_CAPACITY].into(); - let p_rc_active: LB::Expr = periodic[PCOL_RC_ACTIVE].into(); - let p_squeeze_active: LB::Expr = periodic[PCOL_SQUEEZE_ACTIVE].into(); - let p_pad_0x80: LB::Expr = periodic[PCOL_PAD_0X80].into(); - let p_extra: LB::Expr = periodic[PCOL_EXTRA].into(); - let p_idx: LB::Expr = periodic[PCOL_IDX].into(); - let rc_lo: LB::Expr = periodic[PCOL_RC_LO].into(); - let rc_hi: LB::Expr = periodic[PCOL_RC_HI].into(); - let p_state_lane: LB::Expr = p_rate_block.clone() + p_capacity; - - let act: LB::Expr = local[COL_ACT].into(); - let sponge_seq_id: LB::Expr = local[COL_SPONGE_SEQ_ID].into(); - let chunk_ptr: LB::Expr = local[COL_CHUNK_PTR].into(); - let bytes_left: LB::Expr = local[COL_BYTES_LEFT].into(); - let is_first_block: LB::Expr = local[COL_IS_FIRST_BLOCK_OF_INVOCATION].into(); - let is_chunk_avail: LB::Expr = local[COL_IS_CHUNK_AVAIL].into(); - let is_zero: LB::Expr = local[COL_IS_ZERO].into(); - let is_zero_next: LB::Expr = next[COL_IS_ZERO].into(); - let chunk_lo: LB::Expr = local[COL_CHUNK_LO].into(); - let chunk_hi: LB::Expr = local[COL_CHUNK_HI].into(); - let state_prev_lo: LB::Expr = local[COL_STATE_PREV_LO].into(); - let state_prev_hi: LB::Expr = local[COL_STATE_PREV_HI].into(); - let state_new_lo: LB::Expr = local[COL_STATE_NEW_LO].into(); - let state_new_hi: LB::Expr = local[COL_STATE_NEW_HI].into(); - let state_out_lo: LB::Expr = local[COL_STATE_OUT_LO].into(); - let state_out_hi: LB::Expr = local[COL_STATE_OUT_HI].into(); - let cleared_bytes: [LB::Var; 8] = array::from_fn(|i| local[CLEARED_BYTES_RANGE.start + i]); - let padded_bytes: [LB::Var; 8] = array::from_fn(|i| local[PADDED_BYTES_RANGE.start + i]); - let chunk_bytes: [LB::Var; 8] = array::from_fn(|i| local[CHUNK_BYTES_RANGE.start + i]); - let state_prev_bytes: [LB::Var; 8] = - array::from_fn(|i| local[STATE_PREV_BYTES_RANGE.start + i]); - let state_new_bytes: [LB::Var; 8] = - array::from_fn(|i| local[STATE_NEW_BYTES_RANGE.start + i]); - - // Σ b_j (= `is_last_block_period`); `andnot_mask` and - // `padding_mask`, byte-decomposed, as `Σ_j b_j · MASK_BYTE[i][j]` - // inlines (`mask_byte` extracts byte `i` from the existing - // verifier-known `*_LO`/`*_HI` per-`byte_offset` constants, so the - // per-byte tables are correct by construction from the - // already-verified 32-bit ones). - let mut b_sum = LB::Expr::ZERO; - let mut andnot_mask_bytes: [LB::Expr; 8] = array::from_fn(|_| LB::Expr::ZERO); - let mut padding_mask_bytes: [LB::Expr; 8] = array::from_fn(|_| LB::Expr::ZERO); - for (j, col) in COL_B_RANGE.enumerate() { - let b_j: LB::Expr = local[col].into(); - b_sum += b_j.clone(); - for i in 0..8 { - let andnot_byte = mask_byte(ANDNOT_MASK_LO[j], ANDNOT_MASK_HI[j], i); - let padding_byte = mask_byte(PADDING_MASK_LO[j], PADDING_MASK_HI[j], i); - andnot_mask_bytes[i] += LB::Expr::from(Felt::from(andnot_byte)) * b_j.clone(); - padding_mask_bytes[i] += LB::Expr::from(Felt::from(padding_byte)) * b_j.clone(); - } + eval_lookups(builder, 0); + } +} + +/// Evaluate this component's LogUp columns in a main-trace column band. +pub(crate) fn eval_lookups(builder: &mut LB, main_col_offset: usize) +where + LB: LookupBuilder, +{ + let local: [LB::Var; NUM_MAIN_COLS] = current_main(builder.main(), main_col_offset); + let next: [LB::Var; NUM_MAIN_COLS] = next_main(builder.main(), main_col_offset); + let periodic = builder.periodic_values(); + let p_first: LB::Expr = periodic[PCOL_FIRST].into(); + let p_rate_block: LB::Expr = periodic[PCOL_RATE_BLOCK].into(); + let p_capacity: LB::Expr = periodic[PCOL_CAPACITY].into(); + let p_rc_active: LB::Expr = periodic[PCOL_RC_ACTIVE].into(); + let p_squeeze_active: LB::Expr = periodic[PCOL_SQUEEZE_ACTIVE].into(); + let p_pad_0x80: LB::Expr = periodic[PCOL_PAD_0X80].into(); + let p_extra: LB::Expr = periodic[PCOL_EXTRA].into(); + let p_idx: LB::Expr = periodic[PCOL_IDX].into(); + let rc_lo: LB::Expr = periodic[PCOL_RC_LO].into(); + let rc_hi: LB::Expr = periodic[PCOL_RC_HI].into(); + let p_state_lane: LB::Expr = p_rate_block.clone() + p_capacity; + + let act: LB::Expr = local[COL_ACT].into(); + let sponge_seq_id: LB::Expr = local[COL_SPONGE_SEQ_ID].into(); + let chunk_ptr: LB::Expr = local[COL_CHUNK_PTR].into(); + let bytes_left: LB::Expr = local[COL_BYTES_LEFT].into(); + let is_first_block: LB::Expr = local[COL_IS_FIRST_BLOCK_OF_INVOCATION].into(); + let is_chunk_avail: LB::Expr = local[COL_IS_CHUNK_AVAIL].into(); + let is_zero: LB::Expr = local[COL_IS_ZERO].into(); + let is_zero_next: LB::Expr = next[COL_IS_ZERO].into(); + let chunk_lo: LB::Expr = local[COL_CHUNK_LO].into(); + let chunk_hi: LB::Expr = local[COL_CHUNK_HI].into(); + let state_prev_lo: LB::Expr = local[COL_STATE_PREV_LO].into(); + let state_prev_hi: LB::Expr = local[COL_STATE_PREV_HI].into(); + let state_new_lo: LB::Expr = local[COL_STATE_NEW_LO].into(); + let state_new_hi: LB::Expr = local[COL_STATE_NEW_HI].into(); + let state_out_lo: LB::Expr = local[COL_STATE_OUT_LO].into(); + let state_out_hi: LB::Expr = local[COL_STATE_OUT_HI].into(); + let cleared_bytes: [LB::Var; 8] = array::from_fn(|i| local[CLEARED_BYTES_RANGE.start + i]); + let padded_bytes: [LB::Var; 8] = array::from_fn(|i| local[PADDED_BYTES_RANGE.start + i]); + let chunk_bytes: [LB::Var; 8] = array::from_fn(|i| local[CHUNK_BYTES_RANGE.start + i]); + let state_prev_bytes: [LB::Var; 8] = + array::from_fn(|i| local[STATE_PREV_BYTES_RANGE.start + i]); + let state_new_bytes: [LB::Var; 8] = array::from_fn(|i| local[STATE_NEW_BYTES_RANGE.start + i]); + + // Σ b_j (= `is_last_block_period`); `andnot_mask` and + // `padding_mask`, byte-decomposed, as `Σ_j b_j · MASK_BYTE[i][j]` + // inlines (`mask_byte` extracts byte `i` from the existing + // verifier-known `*_LO`/`*_HI` per-`byte_offset` constants, so the + // per-byte tables are correct by construction from the + // already-verified 32-bit ones). + let mut b_sum = LB::Expr::ZERO; + let mut andnot_mask_bytes: [LB::Expr; 8] = array::from_fn(|_| LB::Expr::ZERO); + let mut padding_mask_bytes: [LB::Expr; 8] = array::from_fn(|_| LB::Expr::ZERO); + for (j, col) in COL_B_RANGE.enumerate() { + let b_j: LB::Expr = local[col].into(); + b_sum += b_j.clone(); + for i in 0..8 { + let andnot_byte = mask_byte(ANDNOT_MASK_LO[j], ANDNOT_MASK_HI[j], i); + let padding_byte = mask_byte(PADDING_MASK_LO[j], PADDING_MASK_HI[j], i); + andnot_mask_bytes[i] += LB::Expr::from(Felt::from(andnot_byte)) * b_j.clone(); + padding_mask_bytes[i] += LB::Expr::from(Felt::from(padding_byte)) * b_j.clone(); } + } - // Derived signals (see the design notes - // §"Derived multiplicity signals"). - let is_intra: LB::Expr = LB::Expr::ONE - is_first_block.clone(); - let is_first_row_of_invocation: LB::Expr = p_first * is_first_block; - let is_pad: LB::Expr = is_zero_next.clone() - is_zero; - let is_verbatim: LB::Expr = LB::Expr::ONE - is_zero_next; - - // Per-row address expressions. - let hundred_seq = LB::Expr::from(Felt::from(100u8)) * sponge_seq_id.clone(); - let ninety_nine_idx = LB::Expr::from(Felt::from(99u8)) * p_idx.clone(); - let addr_state_lane_prev = - hundred_seq.clone() - ninety_nine_idx.clone() - LB::Expr::from(Felt::from(128u8)); - let addr_state_lane_new = hundred_seq.clone() - ninety_nine_idx.clone(); - let addr_rc = hundred_seq.clone() - + LB::Expr::from(Felt::from(28u8)) * p_idx - + LB::Expr::from(Felt::from(25u8)); - let addr_squeeze = - hundred_seq.clone() - ninety_nine_idx + LB::Expr::from(Felt::from(3072u32)); - let addr_lane16 = hundred_seq - LB::Expr::from(Felt::from(2484u32)); - let chunk_addr_base = - Felt::new(CHUNK_ADDR_BASE).expect("CHUNK_ADDR_BASE fits in canonical Goldilocks"); - let addr_chunk = LB::Expr::from(chunk_addr_base) + chunk_ptr.clone(); - - // Per-message multiplicity factors, all gated by `act`. - let mult_prev_perm: LB::Expr = LB::Expr::from(Felt::from(2u8)) * act.clone() * is_intra; - let mult_new_state: LB::Expr = - LB::Expr::ZERO - LB::Expr::from(Felt::from(2u8)) * act.clone(); - let mult_rc: LB::Expr = - LB::Expr::ZERO - LB::Expr::from(Felt::from(1u8)) * act.clone() * p_rc_active; - let mult_squeeze: LB::Expr = - LB::Expr::from(Felt::from(2u8)) * act.clone() * p_squeeze_active * b_sum.clone(); - let mult_lane16_consume: LB::Expr = - LB::Expr::from(Felt::from(2u8)) * act.clone() * b_sum.clone(); - let mult_lane16_provide: LB::Expr = - LB::Expr::ZERO - LB::Expr::from(Felt::from(2u8)) * act.clone() * b_sum.clone(); - - let andnot_tag = LB::Expr::from(Felt::from(BytePairOp::AndNot.tag())); - let xor_tag = LB::Expr::from(Felt::from(BytePairOp::Xor.tag())); - - let interaction_deg = Deg { v: 1, u: 1 }; - // FLATTENED to lqd 2: the mutex outer flags are folded into each - // insert's multiplicity (sound — the one-hot flags are binary on the - // rows where they fire, the precondition the mutex fold already - // relied on), and the 13 fractions are partitioned ≤ 3 per column - // so every closing constraint is degree ≤ 5. Column-degree hints are - // ignored on the constraint path. - let pair_deg = Deg { v: 4, u: 2 }; - let triple_deg = Deg { v: 5, u: 3 }; - let solo_deg = Deg { v: 4, u: 1 }; - let mixed_deg = Deg { v: 5, u: 2 }; - - // col 0 (running sum): Memory64 state-lane new-state + prev-perm — the - // two lowest-degree fractions, so the gated last-row close stays ≤ 5. + // Derived signals (see the design notes + // §"Derived multiplicity signals"). + let is_intra: LB::Expr = LB::Expr::ONE - is_first_block.clone(); + let is_first_row_of_invocation: LB::Expr = p_first * is_first_block; + let is_pad: LB::Expr = is_zero_next.clone() - is_zero; + let is_verbatim: LB::Expr = LB::Expr::ONE - is_zero_next; + + // Per-row address expressions. + let hundred_seq = LB::Expr::from(Felt::from(100u8)) * sponge_seq_id.clone(); + let ninety_nine_idx = LB::Expr::from(Felt::from(99u8)) * p_idx.clone(); + let addr_state_lane_prev = + hundred_seq.clone() - ninety_nine_idx.clone() - LB::Expr::from(Felt::from(128u8)); + let addr_state_lane_new = hundred_seq.clone() - ninety_nine_idx.clone(); + let addr_rc = hundred_seq.clone() + + LB::Expr::from(Felt::from(28u8)) * p_idx + + LB::Expr::from(Felt::from(25u8)); + let addr_squeeze = hundred_seq.clone() - ninety_nine_idx + LB::Expr::from(Felt::from(3072u32)); + let addr_lane16 = hundred_seq - LB::Expr::from(Felt::from(2484u32)); + let chunk_addr_base = + Felt::new(CHUNK_ADDR_BASE).expect("CHUNK_ADDR_BASE fits in canonical Goldilocks"); + let addr_chunk = LB::Expr::from(chunk_addr_base) + chunk_ptr.clone(); + + // Per-message multiplicity factors, all gated by `act`. + let mult_prev_perm: LB::Expr = LB::Expr::from(Felt::from(2u8)) * act.clone() * is_intra; + let mult_new_state: LB::Expr = LB::Expr::ZERO - LB::Expr::from(Felt::from(2u8)) * act.clone(); + let mult_rc: LB::Expr = + LB::Expr::ZERO - LB::Expr::from(Felt::from(1u8)) * act.clone() * p_rc_active; + let mult_squeeze: LB::Expr = + LB::Expr::from(Felt::from(2u8)) * act.clone() * p_squeeze_active * b_sum.clone(); + let mult_lane16_consume: LB::Expr = + LB::Expr::from(Felt::from(2u8)) * act.clone() * b_sum.clone(); + let mult_lane16_provide: LB::Expr = + LB::Expr::ZERO - LB::Expr::from(Felt::from(2u8)) * act.clone() * b_sum.clone(); + + let andnot_tag = LB::Expr::from(Felt::from(BytePairOp::AndNot.tag())); + let xor_tag = LB::Expr::from(Felt::from(BytePairOp::Xor.tag())); + + let interaction_deg = Deg { v: 1, u: 1 }; + // FLATTENED to lqd 2: the mutex outer flags are folded into each + // insert's multiplicity (sound — the one-hot flags are binary on the + // rows where they fire, the precondition the mutex fold already + // relied on), and the 13 fractions are partitioned ≤ 3 per column + // so every closing constraint is degree ≤ 5. Column-degree hints are + // ignored on the constraint path. + let pair_deg = Deg { v: 4, u: 2 }; + let triple_deg = Deg { v: 5, u: 3 }; + let solo_deg = Deg { v: 4, u: 1 }; + let mixed_deg = Deg { v: 5, u: 2 }; + + // col 0 (running sum): Memory64 state-lane new-state + prev-perm — the + // two lowest-degree fractions, so the gated last-row close stays ≤ 5. + frac_col!( + builder, + "memory64", + pair_deg, + ( + "new-state", + p_state_lane.clone() * mult_new_state.clone(), + Memory64Msg { + addr: addr_state_lane_new.clone(), + lo: state_new_lo.clone(), + hi: state_new_hi.clone(), + }, + interaction_deg + ), + ( + "prev-perm", + p_state_lane.clone() * mult_prev_perm.clone(), + Memory64Msg { + addr: addr_state_lane_prev.clone(), + lo: state_prev_lo.clone(), + hi: state_prev_hi.clone(), + }, + interaction_deg + ), + ); + // col 1: Memory64 state-lane rc + lane-16 0x80 consume / provide. + frac_col!( + builder, + "memory64", + triple_deg, + ( + "rc", + p_state_lane.clone() * mult_rc.clone(), + Memory64Msg { + addr: addr_rc.clone(), + lo: rc_lo.clone(), + hi: rc_hi.clone() + }, + interaction_deg + ), + ( + "lane16-consume", + p_pad_0x80.clone() * mult_lane16_consume.clone(), + Memory64Msg { + addr: addr_lane16.clone(), + lo: state_prev_lo.clone(), + hi: state_prev_hi.clone(), + }, + interaction_deg + ), + ( + "lane16-provide", + p_pad_0x80.clone() * mult_lane16_provide.clone(), + Memory64Msg { + addr: addr_lane16.clone(), + lo: state_new_lo.clone(), + hi: state_new_hi.clone(), + }, + interaction_deg + ), + ); + // col 2: Memory64 squeeze — a degree-4 multiplicity, alone (closing 4). + frac_col!( + builder, + "memory64", + solo_deg, + ( + "squeeze", + p_state_lane.clone() * mult_squeeze.clone(), + Memory64Msg { + addr: addr_squeeze.clone(), + lo: state_out_lo.clone(), + hi: state_out_hi.clone() + }, + interaction_deg + ), + ); + + // cols 3..15: pad-row `BytePairLut` requests, split into three + // four-column groups: `andnot` (mask, chunk) → cleared, + // `xor-padding` (cleared, padding_mask) → padded, and `xor-state` + // (state_prev, padded) → state_new. Each group checks eight bytes, + // two per column. + let pad_mult = p_rate_block.clone() * is_pad * act.clone(); + for pair in 0..4 { + let i0 = pair * 2; + let i1 = i0 + 1; frac_col!( builder, - "memory64", + "byte-pair-lut", pair_deg, ( - "new-state", - p_state_lane.clone() * mult_new_state.clone(), - Memory64Msg { - addr: addr_state_lane_new.clone(), - lo: state_new_lo.clone(), - hi: state_new_hi.clone(), + "andnot", + pad_mult.clone(), + BytePairLutMsg { + op: andnot_tag.clone(), + a: andnot_mask_bytes[i0].clone(), + b: chunk_bytes[i0].into(), + c: cleared_bytes[i0].into() }, interaction_deg ), ( - "prev-perm", - p_state_lane.clone() * mult_prev_perm.clone(), - Memory64Msg { - addr: addr_state_lane_prev.clone(), - lo: state_prev_lo.clone(), - hi: state_prev_hi.clone(), + "andnot", + pad_mult.clone(), + BytePairLutMsg { + op: andnot_tag.clone(), + a: andnot_mask_bytes[i1].clone(), + b: chunk_bytes[i1].into(), + c: cleared_bytes[i1].into() }, interaction_deg ), ); - // col 1: Memory64 state-lane rc + lane-16 0x80 consume / provide. + } + for pair in 0..4 { + let i0 = pair * 2; + let i1 = i0 + 1; frac_col!( builder, - "memory64", - triple_deg, + "byte-pair-lut", + pair_deg, ( - "rc", - p_state_lane.clone() * mult_rc.clone(), - Memory64Msg { - addr: addr_rc.clone(), - lo: rc_lo.clone(), - hi: rc_hi.clone() + "xor-padding", + pad_mult.clone(), + BytePairLutMsg { + op: xor_tag.clone(), + a: cleared_bytes[i0].into(), + b: padding_mask_bytes[i0].clone(), + c: padded_bytes[i0].into() }, interaction_deg ), ( - "lane16-consume", - p_pad_0x80.clone() * mult_lane16_consume.clone(), - Memory64Msg { - addr: addr_lane16.clone(), - lo: state_prev_lo.clone(), - hi: state_prev_hi.clone(), + "xor-padding", + pad_mult.clone(), + BytePairLutMsg { + op: xor_tag.clone(), + a: cleared_bytes[i1].into(), + b: padding_mask_bytes[i1].clone(), + c: padded_bytes[i1].into() + }, + interaction_deg + ), + ); + } + for pair in 0..4 { + let i0 = pair * 2; + let i1 = i0 + 1; + frac_col!( + builder, + "byte-pair-lut", + pair_deg, + ( + "xor-state", + pad_mult.clone(), + BytePairLutMsg { + op: xor_tag.clone(), + a: state_prev_bytes[i0].into(), + b: padded_bytes[i0].into(), + c: state_new_bytes[i0].into() }, interaction_deg ), ( - "lane16-provide", - p_pad_0x80.clone() * mult_lane16_provide.clone(), - Memory64Msg { - addr: addr_lane16.clone(), - lo: state_new_lo.clone(), - hi: state_new_hi.clone(), + "xor-state", + pad_mult.clone(), + BytePairLutMsg { + op: xor_tag.clone(), + a: state_prev_bytes[i1].into(), + b: padded_bytes[i1].into(), + c: state_new_bytes[i1].into() }, interaction_deg ), ); - // col 2: Memory64 squeeze — a degree-4 multiplicity, alone (closing 4). + } + + // cols 15..19: verbatim `xor-state` (state_prev, chunk) → + // state_new, 8 bytes. + let verbatim_mult = p_rate_block.clone() * is_verbatim * act.clone(); + for pair in 0..4 { + let i0 = pair * 2; + let i1 = i0 + 1; frac_col!( builder, - "memory64", - solo_deg, + "byte-pair-lut", + pair_deg, ( - "squeeze", - p_state_lane.clone() * mult_squeeze.clone(), - Memory64Msg { - addr: addr_squeeze.clone(), - lo: state_out_lo.clone(), - hi: state_out_hi.clone() + "xor-state-verbatim", + verbatim_mult.clone(), + BytePairLutMsg { + op: xor_tag.clone(), + a: state_prev_bytes[i0].into(), + b: chunk_bytes[i0].into(), + c: state_new_bytes[i0].into() + }, + interaction_deg + ), + ( + "xor-state-verbatim", + verbatim_mult.clone(), + BytePairLutMsg { + op: xor_tag.clone(), + a: state_prev_bytes[i1].into(), + b: chunk_bytes[i1].into(), + c: state_new_bytes[i1].into() }, interaction_deg ), ); + } - // cols 3..7: pad-row `BytePairLut` byte requires, 8 bytes each — - // `andnot` (mask, chunk) → cleared, `xor-padding` (cleared, - // padding_mask) → padded, `xor-state` (state_prev, padded) → - // state_new. Same 8-byte-request pattern the round chiplet uses; - // each op verifies its own row's bytes directly, no intermediate - // chiplet or chain trick. - let pad_mult = p_rate_block.clone() * is_pad * act.clone(); - for pair in 0..4 { - let i0 = pair * 2; - let i1 = i0 + 1; - frac_col!( - builder, - "byte-pair-lut", - pair_deg, - ( - "andnot", - pad_mult.clone(), - BytePairLutMsg { - op: andnot_tag.clone(), - a: andnot_mask_bytes[i0].clone(), - b: chunk_bytes[i0].into(), - c: cleared_bytes[i0].into() - }, - interaction_deg - ), - ( - "andnot", - pad_mult.clone(), - BytePairLutMsg { - op: andnot_tag.clone(), - a: andnot_mask_bytes[i1].clone(), - b: chunk_bytes[i1].into(), - c: cleared_bytes[i1].into() - }, - interaction_deg - ), - ); - } - for pair in 0..4 { - let i0 = pair * 2; - let i1 = i0 + 1; - frac_col!( - builder, - "byte-pair-lut", - pair_deg, - ( - "xor-padding", - pad_mult.clone(), - BytePairLutMsg { - op: xor_tag.clone(), - a: cleared_bytes[i0].into(), - b: padding_mask_bytes[i0].clone(), - c: padded_bytes[i0].into() - }, - interaction_deg - ), - ( - "xor-padding", - pad_mult.clone(), - BytePairLutMsg { - op: xor_tag.clone(), - a: cleared_bytes[i1].into(), - b: padding_mask_bytes[i1].clone(), - c: padded_bytes[i1].into() - }, - interaction_deg - ), - ); - } - for pair in 0..4 { - let i0 = pair * 2; - let i1 = i0 + 1; - frac_col!( - builder, - "byte-pair-lut", - pair_deg, - ( - "xor-state", - pad_mult.clone(), - BytePairLutMsg { - op: xor_tag.clone(), - a: state_prev_bytes[i0].into(), - b: padded_bytes[i0].into(), - c: state_new_bytes[i0].into() - }, - interaction_deg - ), - ( - "xor-state", - pad_mult.clone(), - BytePairLutMsg { - op: xor_tag.clone(), - a: state_prev_bytes[i1].into(), - b: padded_bytes[i1].into(), - c: state_new_bytes[i1].into() - }, - interaction_deg - ), - ); - } - - // cols 7..11: verbatim `xor-state` (state_prev, chunk) → - // state_new, 8 bytes. - let verbatim_mult = p_rate_block.clone() * is_verbatim * act.clone(); - for pair in 0..4 { - let i0 = pair * 2; - let i1 = i0 + 1; - frac_col!( - builder, - "byte-pair-lut", - pair_deg, - ( - "xor-state-verbatim", - verbatim_mult.clone(), - BytePairLutMsg { - op: xor_tag.clone(), - a: state_prev_bytes[i0].into(), - b: chunk_bytes[i0].into(), - c: state_new_bytes[i0].into() - }, - interaction_deg - ), - ( - "xor-state-verbatim", - verbatim_mult.clone(), - BytePairLutMsg { - op: xor_tag.clone(), - a: state_prev_bytes[i1].into(), - b: chunk_bytes[i1].into(), - c: state_new_bytes[i1].into() - }, - interaction_deg - ), - ); - } - - // cols 11..15: lane-16 `xor-lane16` (state_prev, PAD_CONST) → - // state_new, 8 bytes. `PAD_CONST_BYTES` is a plain constant (not - // selector-dependent), so the `b` field is a literal per byte. - let lane16_mult = p_pad_0x80.clone() * b_sum.clone() * act.clone(); - for pair in 0..4 { - let i0 = pair * 2; - let i1 = i0 + 1; - frac_col!( - builder, - "byte-pair-lut", - pair_deg, - ( - "xor-lane16", - lane16_mult.clone(), - BytePairLutMsg { - op: xor_tag.clone(), - a: state_prev_bytes[i0].into(), - b: LB::Expr::from(Felt::from(PAD_CONST_BYTES[i0])), - c: state_new_bytes[i0].into() - }, - interaction_deg - ), - ( - "xor-lane16", - lane16_mult.clone(), - BytePairLutMsg { - op: xor_tag.clone(), - a: state_prev_bytes[i1].into(), - b: LB::Expr::from(Felt::from(PAD_CONST_BYTES[i1])), - c: state_new_bytes[i1].into() - }, - interaction_deg - ), - ); - } - - // col 5: the KeccakSponge request + the chunk consume (a degree-4 - // multiplicity, paired → closing 5). Two independent inserts on - // different buses, bus-prefix-distinguished encodings keeping the - // contributions algebraically distinct. + // cols 19..23: lane-16 `xor-lane16` (state_prev, PAD_CONST) → + // state_new, 8 bytes. `PAD_CONST_BYTES` is a plain constant (not + // selector-dependent), so the `b` field is a literal per byte. + let lane16_mult = p_pad_0x80.clone() * b_sum.clone() * act.clone(); + for pair in 0..4 { + let i0 = pair * 2; + let i1 = i0 + 1; frac_col!( builder, - "ks-and-chunk", - mixed_deg, + "byte-pair-lut", + pair_deg, ( - "ks-request", - act.clone() * is_first_row_of_invocation.clone(), - KeccakSpongeMsg { - sponge_seq_id: sponge_seq_id.clone(), - chunk_ptr: chunk_ptr.clone(), - len_bytes: bytes_left.clone(), + "xor-lane16", + lane16_mult.clone(), + BytePairLutMsg { + op: xor_tag.clone(), + a: state_prev_bytes[i0].into(), + b: LB::Expr::from(Felt::from(PAD_CONST_BYTES[i0])), + c: state_new_bytes[i0].into() }, interaction_deg ), ( - "chunk-consume", - act.clone() - * (p_rate_block.clone() + p_extra.clone() * b_sum.clone()) - * is_chunk_avail.clone(), - Memory64Msg { - addr: addr_chunk.clone(), - lo: chunk_lo.clone(), - hi: chunk_hi.clone() + "xor-lane16", + lane16_mult.clone(), + BytePairLutMsg { + op: xor_tag.clone(), + a: state_prev_bytes[i1].into(), + b: LB::Expr::from(Felt::from(PAD_CONST_BYTES[i1])), + c: state_new_bytes[i1].into() }, interaction_deg ), ); } + + // col 23: the KeccakSponge request + the chunk consume (a degree-4 + // multiplicity, paired → closing 5). Two independent inserts on + // different buses, bus-prefix-distinguished encodings keeping the + // contributions algebraically distinct. + frac_col!( + builder, + "ks-and-chunk", + mixed_deg, + ( + "ks-request", + act.clone() * is_first_row_of_invocation.clone(), + KeccakSpongeMsg { + sponge_seq_id: sponge_seq_id.clone(), + chunk_ptr: chunk_ptr.clone(), + len_bytes: bytes_left.clone(), + }, + interaction_deg + ), + ( + "chunk-consume", + act.clone() + * (p_rate_block.clone() + p_extra.clone() * b_sum.clone()) + * is_chunk_avail.clone(), + Memory64Msg { + addr: addr_chunk.clone(), + lo: chunk_lo.clone(), + hi: chunk_hi.clone() + }, + interaction_deg + ), + ); } diff --git a/crates/precompiles-prover/src/hash/keccak/sponge/trace.rs b/crates/precompiles-prover/src/hash/keccak/sponge/trace.rs index 670e677bc5..07c2a8a510 100644 --- a/crates/precompiles-prover/src/hash/keccak/sponge/trace.rs +++ b/crates/precompiles-prover/src/hash/keccak/sponge/trace.rs @@ -382,8 +382,24 @@ fn compute_block_snapshots(inv: &Invocation, layout: &InvocationLayout) -> Vec RowMajorMatrix { + generate_trace_padded_to(requires, 0) +} + +/// Same as [`generate_trace`], but the trace height is at least `min_height` +/// (still rounded up to a power of two) — lets a caller sharing this +/// chiplet's row range with another AIR (see `hash::chunk_node_sponge`) pad +/// the sponge's trace up to match the other side's height. Pads past the +/// natural height are the sponge's own trailing inactive rows (`act = 0`, +/// the `sponge_seq_id` / `bytes_left` chains continued). +pub(crate) fn generate_trace_padded_to( + requires: SpongeRequires, + min_height: usize, +) -> RowMajorMatrix { let active_rows = requires.total_active_rows() as usize; - let height = active_rows.next_power_of_two().max(SPONGE_PERIOD); + let min_height = min_height + .checked_next_power_of_two() + .expect("minimum sponge trace height exceeds the host power-of-two range"); + let height = active_rows.next_power_of_two().max(SPONGE_PERIOD).max(min_height); let mut trace = Vec::with_capacity(height * NUM_MAIN_COLS); @@ -642,6 +658,8 @@ pub(crate) fn build_aux( mod tests { use std::vec; + use miden_core::utils::Matrix; + use super::*; #[test] @@ -672,4 +690,10 @@ mod tests { // lanes past the input). assert_eq!(Invocation { input: vec![0; 200] }.chunk_lanes(), 28); } + + #[test] + fn padded_height_rounds_the_floor_to_a_power_of_two() { + let trace = generate_trace_padded_to(SpongeRequires::new(), 33); + assert_eq!(trace.height(), 64); + } } diff --git a/crates/precompiles-prover/src/hash/mod.rs b/crates/precompiles-prover/src/hash/mod.rs index b2b4c27fa8..52a1d2b9cc 100644 --- a/crates/precompiles-prover/src/hash/mod.rs +++ b/crates/precompiles-prover/src/hash/mod.rs @@ -9,5 +9,6 @@ pub mod chunk; pub mod chunk_node; +pub mod chunk_node_sponge; pub mod keccak; pub mod memory64; diff --git a/crates/precompiles-prover/src/relations.rs b/crates/precompiles-prover/src/relations.rs index b41b91c5f3..bbf9cfb5f1 100644 --- a/crates/precompiles-prover/src/relations.rs +++ b/crates/precompiles-prover/src/relations.rs @@ -22,13 +22,13 @@ //! | 6 | `Poseidon2In` | `poseidon2::Poseidon2Air` | `(perm_seq_id, tag, c0, c1, c2, c3)`, `tag ∈ {0, 1, 2}` for rate0/rate1/cap | //! | 7 | `Poseidon2Out` | `poseidon2::Poseidon2Air` | `(perm_seq_id, d0, d1, d2, d3)` — digest = first 4 lanes of post-perm state | //! | 8 | `Binding` | transcript eval chips | `(h0, h1, h2, h3, value_tag, ptr)` — node hash ↦ typed value (self-referential) | -//! | 9 | `ChunkChain` | `chunk::ChunkAir` | `(chunk_seq_id_head, perm_seq_id_head)` — per-invocation chain head, in chunk's native namespace | -//! | 10 | `UintVal` | `uint::UintStoreAir` | `(ptr, bound_ptr, offset, c0..c3)` — 256-bit uint half: 4×32-bit recombined view at offset ∈ {0, 1} | +//! | 9 | `ChunkChain` | `hash::chunk_node_sponge::ChunkNodeSpongeAir` (chunk band) | `(chunk_seq_id_head, perm_seq_id_head)` — per-invocation chain head, in chunk's native namespace | +//! | 10 | `UintVal` | `uint::store_mul::UintStoreMulAir` (store band) | `(ptr, bound_ptr, c0..c7)` — complete 256-bit value as 8×32-bit recombined limbs | //! | 11 | `UintAdd` | `uint::add::UintAddAir` | `(bound_ptr, a_ptr, b_ptr, c_ptr)` — asserts `a + b ≡ c (mod p)` for uints sharing `bound_ptr` | //! | 12 | `UintMul` | `uint::mul::UintMulAir` | `(kappa_a, kappa_c, a_ptr, b_ptr, c_ptr, r_ptr, bound_ptr)` — asserts `κₐ·a·b + κ_c·c ≡ r (mod p)` for uints sharing `bound_ptr` | -//! | 13 | `UintLimbs` | `uint::UintStoreAir` | `(ptr, bound_ptr, offset, l0..l7)` — 256-bit uint half: raw 8×16-bit limb view at offset ∈ {0, 1} | -//! | 14 | `EcGroup` | `ec::groups::EcGroupsAir` | `(group_ptr, a_ptr, b_ptr, bound_ptr, scalar_bound_ptr)` — a short-Weierstrass group binding its curve context (params + base-field modulus + scalar-field modulus, the latter = `bound_ptr` while unconstrained) | -//! | 15 | `EcPoint` | `ec::EcPointStoreAir` | `(point_ptr, group_ptr, x_ptr, y_ptr, is_pai)` — a stored on-curve point (or the group's ∞ when `is_pai`) | +//! | 13 | `UintLimbs` | `uint::store_mul::UintStoreMulAir` (store band) | `(ptr, bound_ptr, l0..l15)` — raw 16×16-bit limb view of the complete 256-bit uint | +//! | 14 | `EcGroup` | `ec::point_store_groups::EcPointStoreGroupsAir` (group band) | `(group_ptr, a_ptr, b_ptr, bound_ptr, scalar_bound_ptr)` — a short-Weierstrass group binding its curve context (params + base-field modulus + scalar-field modulus, the latter = `bound_ptr` while unconstrained) | +//! | 15 | `EcPoint` | `ec::point_store_groups::EcPointStoreGroupsAir` (point band) | `(point_ptr, group_ptr, x_ptr, y_ptr, is_pai)` — a stored on-curve point (or the group's ∞ when `is_pai`) | //! | 16 | `EcGroupAdd` | `ec::add::EcGroupAddAir` | `(group_ptr, p_ptr, q_ptr, r_ptr)` — asserts `R = P + Q` in the group | //! | 17 | `EcOnCurveCert` | `ec::add::EcGroupAddAir`, `ec::msm::EcMsmAir` | `(group_ptr, r_ptr)` — an on-curve membership certificate for a fresh point `r`: provided by its minting op (a group-law add result, or an MSM `neg`'s value `−P`), consumed by `r`'s point-store row in place of the on-curve MAC trio | //! | 18 | `MsmTerm` | `ec::msm::EcMsmAir` | `(expr_ptr, idx, base_ptr, scalar_ptr)` — one term `P × s` of MSM expression `expr_ptr` at position `idx` | diff --git a/crates/precompiles-prover/src/session/mod.rs b/crates/precompiles-prover/src/session/mod.rs index 4e396c4e48..2a7f4159eb 100644 --- a/crates/precompiles-prover/src/session/mod.rs +++ b/crates/precompiles-prover/src/session/mod.rs @@ -1,4 +1,4 @@ -//! Orchestration facade over the thirteen-chiplet stack: the Keccak +//! Orchestration facade over the ten-chiplet stack: the Keccak //! transcript, the uint store and its arithmetic relations, and the EC //! layer (group table + point store + group-law add). //! @@ -47,16 +47,17 @@ use crate::{ require, trace::{EcExprPtr, EcMsmRequires, generate_trace as msm_trace}, }, - trace::{EcGroupPtr, generate_traces as ec_store_traces}, + point_store_groups::trace::generate_trace as ec_store_trace, + trace::EcGroupPtr, }, hash::{ chunk::trace::ChunkRequires, - chunk_node::trace::generate_trace as chunk_node_trace, + chunk_node_sponge::trace::generate_trace as chunk_node_sponge_trace, keccak::{ digest::KeccakDigest, node::trace::KeccakNodeRequires, round::{RoundRequires, generate_trace as round_trace}, - sponge::trace::{SpongeRequires, generate_trace as sponge_trace}, + sponge::trace::SpongeRequires, }, }, math::{U256, from_limbs32, to_limbs32}, @@ -84,7 +85,7 @@ pub mod strategies; pub use prove::{ChipletAir, ChipletMultiAir, VerifyError, verify_deferred, verify_stark}; /// Number of chiplets in the stack (= the width of [`SessionTraces::mains`]). -pub const NUM_CHIPLETS: usize = 12; +pub const NUM_CHIPLETS: usize = 10; /// Stateful builder over the full chiplet stack. /// @@ -455,9 +456,11 @@ impl Session { self.eval.assert_no_stray_values(); // EcCreate rows hash the group pointer and bind it through their EcPoint consume. let eval = trace_span!("eval", eval_trace(self.eval, root)); - let chunk_node = trace_span!("chunk_node", chunk_node_trace(self.chunk, self.node)); + let chunk_node_sponge = trace_span!( + "chunk_node_sponge", + chunk_node_sponge_trace(self.chunk, self.node, self.sponge) + ); let p2 = trace_span!("poseidon2", p2_trace(self.p2)); - let sponge = trace_span!("keccak_sponge", sponge_trace(self.sponge)); let round = trace_span!("keccak_round", round_trace(self.round, &mut self.bpl)); // The relation traces route their store demand as they lay, so // they run before the store reads its provide multiplicities; @@ -480,19 +483,17 @@ impl Session { // (which is traced last, below). let ec_add = trace_span!("ec_add", ec_add_trace(self.ec.add, &mut self.ec.store, &mut self.bpl)); - let (ec_groups, ec) = trace_span!("ec_store", ec_store_traces(self.ec.store)); + let ec = trace_span!("ec_store", ec_store_trace(self.ec.store)); let bpl = trace_span!("byte_pair_lut", bpl_trace(self.bpl)); SessionTraces { - chunk_node, + chunk_node_sponge, p2, round, bpl, - sponge, eval, uint, add, - ec_groups, ec, ec_add, msm, @@ -507,19 +508,17 @@ impl Default for Session { } } -/// The twelve chiplet main traces plus the transcript root, ready to +/// The ten chiplet main traces plus the transcript root, ready to /// feed `prove_multi` or a bus-balance check. #[derive(Debug)] pub struct SessionTraces { - chunk_node: RowMajorMatrix, + chunk_node_sponge: RowMajorMatrix, p2: RowMajorMatrix, round: RowMajorMatrix, bpl: RowMajorMatrix, - sponge: RowMajorMatrix, eval: RowMajorMatrix, uint: RowMajorMatrix, add: RowMajorMatrix, - ec_groups: RowMajorMatrix, ec: RowMajorMatrix, ec_add: RowMajorMatrix, msm: RowMajorMatrix, @@ -527,41 +526,37 @@ pub struct SessionTraces { } impl SessionTraces { - /// The twelve main traces in canonical chiplet order: chunk-node, - /// poseidon2, round, byte_pair_lut, sponge, eval, uint-store-mul, - /// uint-add, ec-groups, ec-points, ec-add, ec-msm. The AIRs, provers, - /// and public values a caller assembles must line up with this order. + /// The ten main traces in canonical chiplet order: chunk-node-sponge, + /// poseidon2, round, byte_pair_lut, eval, uint-store-mul, uint-add, + /// ec-point-store-groups, ec-add, ec-msm. The AIRs, provers, and + /// public values a caller assembles must line up with this order. pub fn mains(&self) -> [&RowMajorMatrix; NUM_CHIPLETS] { [ - &self.chunk_node, + &self.chunk_node_sponge, &self.p2, &self.round, &self.bpl, - &self.sponge, &self.eval, &self.uint, &self.add, - &self.ec_groups, &self.ec, &self.ec_add, &self.msm, ] } - /// The twelve main traces by value in [`mains`](Self::mains) order, + /// The ten main traces by value in [`mains`](Self::mains) order, /// consuming the bundle — lets the prover take ownership rather than /// clone the (potentially large) traces. pub fn into_mains(self) -> Vec> { vec![ - self.chunk_node, + self.chunk_node_sponge, self.p2, self.round, self.bpl, - self.sponge, self.eval, self.uint, self.add, - self.ec_groups, self.ec, self.ec_add, self.msm, diff --git a/crates/precompiles-prover/src/session/preprocessed_cache.rs b/crates/precompiles-prover/src/session/preprocessed_cache.rs index 3ba403a046..1f9ca2566c 100644 --- a/crates/precompiles-prover/src/session/preprocessed_cache.rs +++ b/crates/precompiles-prover/src/session/preprocessed_cache.rs @@ -1,7 +1,7 @@ //! Process-lifetime caching of the chiplet stack's preprocessed bundle. //! //! `Preprocessed::build` LDEs and commits the fixed `BytePairLut` table — a -//! pure function of the (fixed, 12-AIR) chiplet list and the STARK config's +//! pure function of the fixed ten-chiplet list and the STARK config's //! blowup/LMCS/DFT — yet both `prove_stark` and `verify_stark` rebuild it on //! every call. Under `std`, each hash function's bundle is built once per //! process and reused via `OnceLock`; without `std` (e.g. a `no_std` @@ -49,7 +49,7 @@ where } } -/// The AIR list never varies across calls (the fixed 12-chiplet stack), and +/// The AIR list never varies across calls (the fixed ten-chiplet stack), and /// `Preprocessed::build` reads only `statement.airs()` — never the public /// inputs — so a scratch statement with dummy public inputs builds the exact /// same bundle as the real per-proof statement would. diff --git a/crates/precompiles-prover/src/session/prove.rs b/crates/precompiles-prover/src/session/prove.rs index b34c5d7c72..0dc4e7fddd 100644 --- a/crates/precompiles-prover/src/session/prove.rs +++ b/crates/precompiles-prover/src/session/prove.rs @@ -1,6 +1,6 @@ //! Multi-AIR proving for the chiplet stack. //! -//! [`ChipletAir`] wraps the twelve heterogeneous AIRs into one enum (the +//! [`ChipletAir`] wraps the ten heterogeneous AIRs into one enum (the //! `MultiAir::Air` type); [`ChipletMultiAir`] owns them and closes the //! cross-chiplet LogUp identity — `Σ σ = 0` — in //! [`MultiAir::eval_external`]. @@ -36,11 +36,8 @@ const MAX_STARK_PROOF_BYTES: usize = 64 * 1024 * 1024; use crate::{ ProveError, - ec::{EcPointStoreAir, add::EcGroupAddAir, groups::EcGroupsAir, msm::EcMsmAir}, - hash::{ - chunk_node::ChunkNodeAir, - keccak::{round::KeccakRoundAir, sponge::KeccakSpongeAir}, - }, + ec::{add::EcGroupAddAir, msm::EcMsmAir, point_store_groups::EcPointStoreGroupsAir}, + hash::{chunk_node_sponge::ChunkNodeSpongeAir, keccak::round::KeccakRoundAir}, logup::{Challenges, LookupMessage, lookup_challenges_from_slice, sigma_sum}, primitives::byte_pair_lut::BytePairLutAir, session::{NUM_CHIPLETS, SessionTraces, fixed_ecgroup_msgs, fixed_uintval_msgs}, @@ -56,21 +53,19 @@ use crate::{ uint::{add::UintAddAir, store_mul::UintStoreMulAir}, }; -/// The twelve chiplet AIRs wrapped into one enum — the heterogeneous +/// The ten chiplet AIRs wrapped into one enum — the heterogeneous /// `MultiAir::Air` type. Variant order is the canonical /// [`SessionTraces::mains`] order. #[derive(Clone, Debug)] pub enum ChipletAir { - ChunkNode, + ChunkNodeSponge, Poseidon2, KeccakRound, BytePairLut, - KeccakSponge, TranscriptEval, UintStoreMul, UintAdd, - EcGroups, - EcPointStore, + EcPointStoreGroups, EcGroupAdd, EcMsm, } @@ -78,16 +73,14 @@ pub enum ChipletAir { macro_rules! delegate { ($self:ident, $method:ident $(, $arg:expr)*) => { match $self { - ChipletAir::ChunkNode => ChunkNodeAir.$method($($arg),*), + ChipletAir::ChunkNodeSponge => ChunkNodeSpongeAir.$method($($arg),*), ChipletAir::Poseidon2 => Poseidon2Air.$method($($arg),*), ChipletAir::KeccakRound => KeccakRoundAir.$method($($arg),*), ChipletAir::BytePairLut => BytePairLutAir.$method($($arg),*), - ChipletAir::KeccakSponge => KeccakSpongeAir.$method($($arg),*), ChipletAir::TranscriptEval => TranscriptEvalAir.$method($($arg),*), ChipletAir::UintStoreMul => UintStoreMulAir.$method($($arg),*), ChipletAir::UintAdd => UintAddAir.$method($($arg),*), - ChipletAir::EcGroups => EcGroupsAir.$method($($arg),*), - ChipletAir::EcPointStore => EcPointStoreAir.$method($($arg),*), + ChipletAir::EcPointStoreGroups => EcPointStoreGroupsAir.$method($($arg),*), ChipletAir::EcGroupAdd => EcGroupAddAir.$method($($arg),*), ChipletAir::EcMsm => EcMsmAir.$method($($arg),*), } @@ -103,19 +96,17 @@ where } impl ChipletAir { - /// The twelve AIRs in canonical [`SessionTraces::mains`] order. + /// The ten AIRs in canonical [`SessionTraces::mains`] order. pub fn all() -> [ChipletAir; NUM_CHIPLETS] { [ - ChipletAir::ChunkNode, + ChipletAir::ChunkNodeSponge, ChipletAir::Poseidon2, ChipletAir::KeccakRound, ChipletAir::BytePairLut, - ChipletAir::KeccakSponge, ChipletAir::TranscriptEval, ChipletAir::UintStoreMul, ChipletAir::UintAdd, - ChipletAir::EcGroups, - ChipletAir::EcPointStore, + ChipletAir::EcPointStoreGroups, ChipletAir::EcGroupAdd, ChipletAir::EcMsm, ] @@ -161,23 +152,21 @@ impl LiftedAir for ChipletAir { } fn eval>(&self, builder: &mut AB) { match self { - ChipletAir::ChunkNode => eval_lifted(&ChunkNodeAir, builder), + ChipletAir::ChunkNodeSponge => eval_lifted(&ChunkNodeSpongeAir, builder), ChipletAir::Poseidon2 => eval_lifted(&Poseidon2Air, builder), ChipletAir::KeccakRound => eval_lifted(&KeccakRoundAir, builder), ChipletAir::BytePairLut => eval_lifted(&BytePairLutAir, builder), - ChipletAir::KeccakSponge => eval_lifted(&KeccakSpongeAir, builder), ChipletAir::TranscriptEval => eval_lifted(&TranscriptEvalAir, builder), ChipletAir::UintStoreMul => eval_lifted(&UintStoreMulAir, builder), ChipletAir::UintAdd => eval_lifted(&UintAddAir, builder), - ChipletAir::EcGroups => eval_lifted(&EcGroupsAir, builder), - ChipletAir::EcPointStore => eval_lifted(&EcPointStoreAir, builder), + ChipletAir::EcPointStoreGroups => eval_lifted(&EcPointStoreGroupsAir, builder), ChipletAir::EcGroupAdd => eval_lifted(&EcGroupAddAir, builder), ChipletAir::EcMsm => eval_lifted(&EcMsmAir, builder), } } } -/// The chiplet stack as a [`MultiAir`]: owns the thirteen AIRs (in canonical +/// The chiplet stack as a [`MultiAir`]: owns the ten AIRs (in canonical /// order) and closes the cross-chiplet LogUp identity — `Σ σ = 0` over /// every AIR's committed residue — in [`eval_external`](Self::eval_external). #[derive(Debug, Clone)] @@ -252,7 +241,7 @@ impl MultiAir for ChipletMultiAir { impl SessionTraces { /// Build the [`ProverStatement`]: the [`ChipletMultiAir`] + the shared - /// `air_inputs` (the transcript root) + the thirteen main traces in + /// `air_inputs` (the transcript root) + the ten main traces in /// canonical [`mains`](Self::mains) order. fn prover_statement(&self) -> ProverStatement { let statement = Statement::new(ChipletMultiAir::new(), self.air_inputs(), Vec::new()) @@ -261,10 +250,8 @@ impl SessionTraces { ProverStatement::new(statement, mains).expect("chiplet trace shapes are valid") } - /// Per-AIR `check_constraints` under the legacy fast test config — a cheap - /// local-constraint sanity pass (catches AIR regressions before the more - /// opaque `prove` failure; no cross-chiplet bus balance, which only the - /// full prove/verify closes via `eval_external`). + /// `check_constraints` under the legacy fast test config — a cheap constraint sanity pass + /// covering each AIR and the cross-chiplet assertion returned by `eval_external`. pub fn check(&self) { check_constraints(&self.prover_statement(), test_challenger()); } @@ -469,3 +456,32 @@ pub enum VerifyError { #[error("deferred proof is not STARK-backed")] InvalidDeferredProof, } + +#[cfg(test)] +mod tests { + use miden_core::field::PrimeCharacteristicRing; + + use super::*; + + /// The external assertion is part of the production relation but excluded from the ACE + /// circuit digest. This test guards its cardinality; raw bus-balance tests cover the + /// underlying lookup semantics independently. + #[test] + fn chiplet_multi_air_exposes_the_sigma_closure() { + let challenges = [ + QuadFelt::new([Felt::from(3u32), Felt::from(5u32)]), + QuadFelt::new([Felt::from(7u32), Felt::from(11u32)]), + ]; + let aux_values: [[QuadFelt; 1]; NUM_CHIPLETS] = core::array::from_fn(|i| { + [QuadFelt::new([Felt::from((i + 1) as u32), Felt::from((2 * i + 1) as u32)])] + }); + let aux_refs: Vec<&[QuadFelt]> = aux_values.iter().map(<[QuadFelt; 1]>::as_slice).collect(); + + let assertions = ChipletMultiAir::new() + .eval_external(&challenges, &[], &[], &aux_refs, &[]) + .expect("fixed boundary denominators are non-zero for the fixture"); + + assert_eq!(assertions.len(), 1, "the relation exposes exactly one external assertion"); + assert_ne!(assertions[0], QuadFelt::ZERO, "the closure fixture must be non-vacuous"); + } +} diff --git a/crates/precompiles-prover/src/snapshots/miden_precompiles_prover__stark_config__tests__precompile_relation_digest_matches_current_air.snap b/crates/precompiles-prover/src/snapshots/miden_precompiles_prover__stark_config__tests__precompile_relation_digest_matches_current_air.snap index e0bf3b31dc..92ff8152a9 100644 --- a/crates/precompiles-prover/src/snapshots/miden_precompiles_prover__stark_config__tests__precompile_relation_digest_matches_current_air.snap +++ b/crates/precompiles-prover/src/snapshots/miden_precompiles_prover__stark_config__tests__precompile_relation_digest_matches_current_air.snap @@ -2,7 +2,7 @@ source: crates/precompiles-prover/src/stark_config.rs expression: snapshot --- -num_inputs: 3128 -num_eval_gates: 9664 -stream_len: 12680 -relation_digest: [15901056294547705196, 13548154566962352054, 13148050606838836712, 2433548564999773594] +num_inputs: 3072 +num_eval_gates: 9576 +stream_len: 12592 +relation_digest: [14908530032554120817, 6253902297572432860, 17042470880692173314, 1364863901074227591] diff --git a/crates/precompiles-prover/src/stark_config.rs b/crates/precompiles-prover/src/stark_config.rs index 82b72a69a2..dc4b1edb29 100644 --- a/crates/precompiles-prover/src/stark_config.rs +++ b/crates/precompiles-prover/src/stark_config.rs @@ -48,10 +48,10 @@ const COMPRESSION_INPUTS: usize = 2; /// the lifted STARK protocol outside this circuit hash. /// Keep this in sync with [`crate::ace::build_precompile_multi_air_ace_circuit`]. pub const PRECOMPILE_RELATION_DIGEST: RelationDigest = [ - Felt::new_unchecked(15901056294547705196), - Felt::new_unchecked(13548154566962352054), - Felt::new_unchecked(13148050606838836712), - Felt::new_unchecked(2433548564999773594), + Felt::new_unchecked(14908530032554120817), + Felt::new_unchecked(6253902297572432860), + Felt::new_unchecked(17042470880692173314), + Felt::new_unchecked(1364863901074227591), ]; /// Default hash function for compatibility APIs such as /// [`SessionTraces::prove`](crate::session::SessionTraces::prove). @@ -69,7 +69,7 @@ pub const DEFAULT_HASH_FUNCTION: miden_core::proof::HashFunction = /// evolve together: every chiplet AIR in /// [`ChipletAir`](crate::session::ChipletAir) closes at a `log_quotient_degree` /// well under the core VM's degree-8 constraints (see the -/// `log_quotient_degrees_fit_the_blowup` test), so `log_blowup` could be +/// `ace::tests::quotient_chunks_match_the_symbolic_derivation` test), so `log_blowup` could be /// lowered independently of the core VM in the future. That has not been done /// here, and doing so would need a dedicated security review of the /// resulting FRI parameters before use outside benchmarking. @@ -168,10 +168,9 @@ mod tests { extern crate alloc; use alloc::{format, vec::Vec}; - use miden_ace_codegen::{AceConfig, LayoutKind}; use miden_core::{Felt, crypto::hash::Poseidon2}; - use crate::{ace, session::NUM_CHIPLETS}; + use crate::ace; const PROTOCOL_ID: u64 = 0; const REGEN_HINT: &str = "update PRECOMPILE_RELATION_DIGEST in crates/precompiles-prover/src/stark_config.rs and accept the insta snapshot"; @@ -179,12 +178,7 @@ mod tests { /// Snapshot test: catches any precompile chiplet AIR change that alters the constraint circuit. #[test] fn precompile_relation_digest_matches_current_air() { - let config = AceConfig { - num_quotient_chunks: 8, - layout: LayoutKind::Masm, - num_airs: NUM_CHIPLETS, - }; - let circuit = ace::build_precompile_multi_air_ace_circuit(config).unwrap(); + let circuit = ace::build_precompile_multi_air_ace_circuit().unwrap(); let encoded = circuit.to_ace().unwrap(); let circuit_commitment: [Felt; 4] = encoded.circuit_hash().into(); diff --git a/crates/precompiles-prover/src/tests/bus_balance.rs b/crates/precompiles-prover/src/tests/bus_balance.rs index 7475c1dee1..11fd6dc8f8 100644 --- a/crates/precompiles-prover/src/tests/bus_balance.rs +++ b/crates/precompiles-prover/src/tests/bus_balance.rs @@ -10,11 +10,8 @@ use miden_core::{Felt, field::QuadFelt, utils::RowMajorMatrix}; use miden_lifted_air::LiftedAir; use crate::{ - ec::{EcPointStoreAir, add::EcGroupAddAir, groups::EcGroupsAir, msm::EcMsmAir}, - hash::{ - chunk_node::ChunkNodeAir, - keccak::{round::KeccakRoundAir, sponge::KeccakSpongeAir}, - }, + ec::{add::EcGroupAddAir, msm::EcMsmAir, point_store_groups::EcPointStoreGroupsAir}, + hash::{chunk_node_sponge::ChunkNodeSpongeAir, keccak::round::KeccakRoundAir}, logup::LookupMessage, primitives::byte_pair_lut::BytePairLutAir, session::{ChipletAir, NUM_CHIPLETS, fixed_ecgroup_msgs, fixed_uintval_msgs}, @@ -87,18 +84,20 @@ pub(crate) fn session_stack_residual( .find_map(|(replacement_idx, main)| (*replacement_idx == idx).then_some(*main)) .unwrap_or(mains[idx]); match air { - ChipletAir::ChunkNode => fold_balance(&ChunkNodeAir, main, challenges, &mut net), + ChipletAir::ChunkNodeSponge => { + fold_balance(&ChunkNodeSpongeAir, main, challenges, &mut net) + }, ChipletAir::Poseidon2 => fold_balance(&Poseidon2Air, main, challenges, &mut net), ChipletAir::KeccakRound => fold_balance(&KeccakRoundAir, main, challenges, &mut net), ChipletAir::BytePairLut => fold_balance(&BytePairLutAir, main, challenges, &mut net), - ChipletAir::KeccakSponge => fold_balance(&KeccakSpongeAir, main, challenges, &mut net), ChipletAir::TranscriptEval => { fold_balance(&TranscriptEvalAir, main, challenges, &mut net) }, ChipletAir::UintStoreMul => fold_balance(&UintStoreMulAir, main, challenges, &mut net), ChipletAir::UintAdd => fold_balance(&UintAddAir, main, challenges, &mut net), - ChipletAir::EcGroups => fold_balance(&EcGroupsAir, main, challenges, &mut net), - ChipletAir::EcPointStore => fold_balance(&EcPointStoreAir, main, challenges, &mut net), + ChipletAir::EcPointStoreGroups => { + fold_balance(&EcPointStoreGroupsAir, main, challenges, &mut net) + }, ChipletAir::EcGroupAdd => fold_balance(&EcGroupAddAir, main, challenges, &mut net), ChipletAir::EcMsm => fold_balance(&EcMsmAir, main, challenges, &mut net), } diff --git a/crates/precompiles-prover/src/tests/deferred_state.rs b/crates/precompiles-prover/src/tests/deferred_state.rs index 33ffa2a6aa..48c9d382b5 100644 --- a/crates/precompiles-prover/src/tests/deferred_state.rs +++ b/crates/precompiles-prover/src/tests/deferred_state.rs @@ -1,24 +1,32 @@ use std::{format, string::String, sync::Arc, vec, vec::Vec}; use k256::{ProjectivePoint, elliptic_curve::sec1::ToSec1Point}; +use miden_air::lookup::Challenges; use miden_core::{ Felt, deferred::{ DeferredState, DeferredStateWire, Digest, Node as VmNode, PrecompileRegistry, TRUE_DIGEST as VM_TRUE_DIGEST, TRUE_INDEX, Tag, WireEntry, }, + field::QuadFelt, proof::{DeferredProof, HashFunction, StarkProof}, }; use miden_precompiles::{ CurveId, CurvePrecompile, Keccak256Precompile, UintDomain, UintPrecompile, }; +use rand::{Rng, RngExt, SeedableRng, rngs::StdRng}; use crate::{ deferred::{DeferredSession, session_from_deferred_state}, - hash::keccak::sponge::trace::keccak_oracle, + hash::{ + chunk_node_sponge::SPONGE_COL_OFFSET, + keccak::sponge::{COL_ACT as SPONGE_COL_ACT, SPONGE_PERIOD, trace::keccak_oracle}, + }, math::{U256, from_hex, to_limbs32}, prove_deferred_state, + relations::{MAX_MESSAGE_WIDTH, NUM_BUS_IDS}, session::{Session, SessionTraces, VerifyError, verify_deferred}, + tests::bus_balance::session_stack_residual, transcript::poseidon2::P2Digest, }; @@ -478,3 +486,65 @@ fn prove_deferred_state_round_trips_for_every_hash_function() { } } } + +/// Reconstruct the full ten-chiplet LogUp balance, including verifier-side fixed-boundary +/// consumes. This checks the generated traces against each AIR's lookup evaluator; +/// `eval_external` is tested separately in `session::prove`. +fn assert_session_balanced(traces: &SessionTraces, rng: &mut impl Rng) { + let challenges = Challenges::new( + QuadFelt::new([Felt::new(rng.random()).unwrap(), Felt::new(rng.random()).unwrap()]), + QuadFelt::new([Felt::new(rng.random()).unwrap(), Felt::new(rng.random()).unwrap()]), + MAX_MESSAGE_WIDTH, + NUM_BUS_IDS, + ); + let mains = traces.mains(); + let residual = session_stack_residual(&mains, &[], &challenges); + assert!( + residual.is_empty(), + "session stack imbalance: {} unmatched denom(s); e.g. net {:?} on {}", + residual.len(), + residual.first().map(|(m, _)| *m), + residual.first().map(|(_, s)| s.as_str()).unwrap_or(""), + ); +} + +/// Exercises the merged sponge band on multi-block (`> 136`-byte) messages. +/// The default full-proof fixtures use the single-block input `b"abc"`; this +/// test covers cross-block state, invocation seams, overshoot lanes, padding, +/// and final squeezing through both constraint and bus-balance checks. +#[test] +fn merged_chunk_node_sponge_multi_block_checks_and_balances() { + let mut rng = StdRng::seed_from_u64(0xc0de_5b09); + // 137: first byte past the rate boundary (2 blocks, pad in block 2). + // 271: rate boundary − 1 across two blocks. 300, 407: overshoot variety. + for len in [137usize, 271, 300, 407] { + let input: Vec = (0..len).map(|i| i as u8).collect(); + let traces = keccak_session_traces(&input); + // Inspect the production merged band rather than inferring activity from the input. This + // fails if trace construction silently truncates the sponge invocation. + let merged = traces.mains()[0]; + let active_sponge_rows = merged + .values + .chunks_exact(merged.width) + .filter(|row| row[SPONGE_COL_OFFSET + SPONGE_COL_ACT] == Felt::ONE) + .count(); + assert!( + active_sponge_rows > SPONGE_PERIOD, + "case len={len} must activate more than one sponge block, got {active_sponge_rows} rows" + ); + traces.check(); + assert_session_balanced(&traces, &mut rng); + } +} + +/// Explicit full prove+verify of a multi-block Keccak session — the +/// end-to-end counterpart to the fast check/balance guard above, closing +/// the merged-AIR multi-block gap through the real STARK path. +#[test] +#[ignore = "full prove/verify round-trip; run explicitly"] +fn prove_deferred_state_round_trips_for_multi_block_keccak() { + let synthetic = synthetic_keccak_state(&(0u8..200).collect::>()); + let proof = prove_deferred_state(&synthetic.state, HashFunction::Blake3_256) + .expect("multi-block keccak session should prove"); + verify_deferred(&proof).expect("multi-block keccak session should verify"); +} diff --git a/crates/precompiles-prover/src/tests/ec_add.rs b/crates/precompiles-prover/src/tests/ec_add.rs index d1346049e8..773a58f65f 100644 --- a/crates/precompiles-prover/src/tests/ec_add.rs +++ b/crates/precompiles-prover/src/tests/ec_add.rs @@ -28,14 +28,17 @@ use rand::{Rng, RngExt, SeedableRng, rngs::StdRng}; use crate::logup::{NUM_PUBLIC_VALUES, sigma_sum}; use crate::{ ec::{ - COL_IS_CERT, EcPointStoreAir, EcRequire, NUM_MAIN_COLS as POINT_COLS, + COL_IS_CERT, EcRequire, add::{ CELL_R, COL_CANCEL, COL_DBL, COL_GEN, COL_MINTS, COL_PAI_P, COL_PAI_Q, EcGroupAddAir, NUM_MAIN_COLS as ADD_COLS, PERIOD, ROW_RES, trace::{EcAddRequires, generate_trace as ec_add_trace}, }, - groups::EcGroupsAir, - trace::{EcGroupPtr, EcPointPtr, EcStoreRequires, generate_traces as ec_store_traces}, + point_store_groups::{ + EcPointStoreGroupsAir, NUM_MAIN_COLS as POINTS_GROUPS_COLS, + trace::generate_trace as ec_points_groups_trace, + }, + trace::{EcGroupPtr, EcPointPtr, EcStoreRequires}, }, math::{U256, from_hex}, primitives::byte_pair_lut::{BytePairLutAir, BytePairLutRequires, generate_trace as bpl_trace}, @@ -77,14 +80,14 @@ const FP: u32 = 1000; /// The arithmetic + EC chiplet subset, in canonical /// [`SessionTraces::mains`](crate::session::SessionTraces::mains) order: -/// byte-pair LUT, uint store+mul, uint add, EC groups, EC points, EC add. -const NUM_STACK: usize = 6; +/// byte-pair LUT, uint store+mul, uint add, EC points+groups, EC add. +const NUM_STACK: usize = 5; /// Bare-requires stack over the arithmetic + EC chiplet subset — the EC /// layer's analogue of the Session sweep, driven through [`EcRequire`]. /// The subset is bus-closed: `Range16` nets against the LUT, `UintVal` / /// `UintLimbs` / `UintAdd` / `UintMul` / `EcGroup` / `EcPoint` all net -/// within the six chiplets. +/// within the five chiplets. struct EcStack { store: UintStoreRequires, /// The pinned modulus's handle. @@ -133,18 +136,18 @@ impl EcStack { /// accumulator and routes the demand its rows consume, so relations /// run before the store / EC stores read their provide ledgers and /// every `Range16` consumer fires before the LUT — and bundle the - /// six main traces in [`NUM_STACK`] order. + /// five main traces in [`NUM_STACK`] order. fn traces(mut self) -> EcStackTraces { let mut bpl = BytePairLutRequires::new(); let add = uint_add_trace(self.adds, &mut self.store); let ec_add = ec_add_trace(self.ec_add, &mut self.ec, &mut bpl); let uint = uint_store_mul_trace(self.store, self.muls, &mut bpl); - let (ec_groups, ec_points) = ec_store_traces(self.ec); - EcStackTraces([bpl_trace(bpl), uint, add, ec_groups, ec_points, ec_add]) + let ec_points_groups = ec_points_groups_trace(self.ec); + EcStackTraces([bpl_trace(bpl), uint, add, ec_points_groups, ec_add]) } } -/// The six subset main traces, with the per-chiplet check / balance / +/// The five subset main traces, with the per-chiplet check / balance / /// prove harness over them. struct EcStackTraces([RowMajorMatrix; NUM_STACK]); @@ -154,13 +157,12 @@ fn stack_airs() -> [ChipletAir; NUM_STACK] { ChipletAir::BytePairLut, ChipletAir::UintStoreMul, ChipletAir::UintAdd, - ChipletAir::EcGroups, - ChipletAir::EcPointStore, + ChipletAir::EcPointStoreGroups, ChipletAir::EcGroupAdd, ] } -/// The subset as a [`MultiAir`] over the seven [`stack_airs`] in +/// The subset as a [`MultiAir`] over the five [`stack_airs`] in /// [`NUM_STACK`] order, closing the same cross-AIR `Σ σ = 0` bus identity /// as the full [`ChipletMultiAir`](crate::session::ChipletMultiAir) — the /// subset is bus-closed, so the residue sum vanishes. Drives the @@ -198,18 +200,20 @@ impl MultiAir for EcStackMultiAir { impl EcStackTraces { fn mains(&self) -> [&RowMajorMatrix; NUM_STACK] { - let [a, b, c, d, e, f] = &self.0; - [a, b, c, d, e, f] + let [a, b, c, d, e] = &self.0; + [a, b, c, d, e] } /// The EcGroupAdd main — the tamper tests' target. fn ec_add_main(&self) -> &RowMajorMatrix { - &self.0[5] + &self.0[4] } - /// The EcPointStore main — the closure-cert necessity tests' target. + /// The EcPointStoreGroups main — the closure-cert necessity tests' + /// target (the point-store band sits at columns 0..14, so the point + /// tamper helpers only need the merged row stride). fn ec_points_main(&self) -> &RowMajorMatrix { - &self.0[4] + &self.0[3] } /// Per-chiplet local-constraint check (one AIR at a time, no @@ -230,7 +234,7 @@ impl EcStackTraces { } /// The subset's [`ProverStatement`]: the [`EcStackMultiAir`] + the dummy - /// shared `air_inputs` + the seven main traces in [`NUM_STACK`] order. + /// shared `air_inputs` + the five main traces in [`NUM_STACK`] order. fn prover_statement(&self) -> ProverStatement { let statement = Statement::new(EcStackMultiAir::new(), Self::dummy_air_inputs(), Vec::new()) @@ -277,9 +281,8 @@ fn stack_residual(mains: &[&RowMajorMatrix; NUM_STACK], rng: &mut impl Rng fold_balance(&BytePairLutAir, mains[0], &challenges, &mut net); fold_balance(&UintStoreMulAir, mains[1], &challenges, &mut net); fold_balance(&UintAddAir, mains[2], &challenges, &mut net); - fold_balance(&EcGroupsAir, mains[3], &challenges, &mut net); - fold_balance(&EcPointStoreAir, mains[4], &challenges, &mut net); - fold_balance(&EcGroupAddAir, mains[5], &challenges, &mut net); + fold_balance(&EcPointStoreGroupsAir, mains[3], &challenges, &mut net); + fold_balance(&EcGroupAddAir, mains[4], &challenges, &mut net); net.into_values().filter(|(m, _)| *m != Felt::ZERO).count() } @@ -328,7 +331,8 @@ fn tamper_cell(m: &mut RowMajorMatrix, row: usize, cell: usize, v: u32) { m.values[row * ADD_COLS + cell] = Felt::from(v); } -/// Clone the EcPointStore main and rewrite one column of a given row. +/// Clone the EcPointStoreGroups main and rewrite one point-store-band +/// column of a given row. fn tamper_ec_points( main: &RowMajorMatrix, row: usize, @@ -336,7 +340,7 @@ fn tamper_ec_points( v: u32, ) -> RowMajorMatrix { let mut m = main.clone(); - m.values[row * POINT_COLS + col] = Felt::from(v); + m.values[row * POINTS_GROUPS_COLS + col] = Felt::from(v); m } @@ -653,7 +657,7 @@ fn double_forged_as_generic_unbalances() { check_ec_add(&forged); let mut mains = traces.mains(); - mains[5] = &forged; + mains[4] = &forged; assert_ne!(stack_residual(&mains, &mut rng), 0); } @@ -711,7 +715,7 @@ fn finite_forged_as_pai_unbalances() { check_ec_add(&forged); let mut mains = traces.mains(); - mains[5] = &forged; + mains[4] = &forged; assert_ne!(stack_residual(&mains, &mut rng), 0); } @@ -734,7 +738,7 @@ fn double_forged_as_cancel_unbalances() { check_ec_add(&forged); let mut mains = traces.mains(); - mains[5] = &forged; + mains[4] = &forged; assert_ne!(stack_residual(&mains, &mut rng), 0); } @@ -767,7 +771,7 @@ fn ed25519_torsion_forged_as_double_unbalances() { check_ec_add(&forged); let mut mains = traces.mains(); - mains[5] = &forged; + mains[4] = &forged; assert_ne!(stack_residual(&mains, &mut rng), 0); } @@ -790,7 +794,7 @@ fn forged_result_ptr_unbalances() { check_ec_add(&forged); let mut mains = traces.mains(); - mains[5] = &forged; + mains[4] = &forged; assert_ne!(stack_residual(&mains, &mut rng), 0); } @@ -853,9 +857,9 @@ fn cert_point_forged_as_trio_unbalances() { let traces = k1.stack.traces(); let forged = tamper_ec_points(traces.ec_points_main(), r.addr() as usize - 1, COL_IS_CERT, 0); - crate::tests::check_local(EcPointStoreAir, &forged); + crate::tests::check_local(EcPointStoreGroupsAir, &forged); let mut rng = StdRng::seed_from_u64(0xecad_dce3); let mut mains = traces.mains(); - mains[4] = &forged; + mains[3] = &forged; assert_ne!(stack_residual(&mains, &mut rng), 0); } diff --git a/crates/precompiles-prover/src/tests/ec_dag.rs b/crates/precompiles-prover/src/tests/ec_dag.rs index e362d3f50b..530cc1f416 100644 --- a/crates/precompiles-prover/src/tests/ec_dag.rs +++ b/crates/precompiles-prover/src/tests/ec_dag.rs @@ -239,7 +239,7 @@ fn ec_dag_double_proves() { // the cross-chiplet bus: a mismatched or dangling provide. // ============================================================================ -/// Net unmatched LogUp denominators across the full thirteen-chiplet +/// Net unmatched LogUp denominators across the full ten-chiplet /// stack (0 ⟺ every bus closes), with the `eval` main replaced by /// `eval_main`. fn dag_residual( @@ -247,7 +247,7 @@ fn dag_residual( eval_main: &RowMajorMatrix, rng: &mut impl Rng, ) -> usize { - dag_residual_with(traces, eval_main, traces.mains()[10], rng) + dag_residual_with(traces, eval_main, traces.mains()[8], rng) } /// [`dag_residual`] with the `EcGroupAdd` (ec_add) main also overridden — @@ -261,7 +261,7 @@ fn dag_residual_with( ) -> usize { let mains = traces.mains(); let challenges = Challenges::new(rand_qf(rng), rand_qf(rng), MAX_MESSAGE_WIDTH, NUM_BUS_IDS); - session_stack_residual(&mains, &[(5, eval_main), (10, add_main)], &challenges).len() + session_stack_residual(&mains, &[(4, eval_main), (8, add_main)], &challenges).len() } /// First row whose `col` flag is 1 (width taken from the matrix, so this @@ -316,7 +316,7 @@ fn dag_pai_payload_must_be_true_true() { // A PAI VALUE node has no coordinate children. Its canonical payload is // `(TRUE_DIGEST, TRUE_DIGEST)`, i.e. zero digest in both rate halves. let traces = ec_dag_pai_traces(); - let eval = traces.mains()[5]; + let eval = traces.mains()[4]; let row = first_row_with_flag(eval, COL_IS_EC_PAI); let forged = tamper(eval, row, &[(COL_LHS_BEGIN, Felt::ONE)]); @@ -332,7 +332,7 @@ fn dag_finite_forged_as_pai_unbalances() { // consumer, and the coord children / Poseidon2 messages dangle. let traces = ec_dag_3g_traces(); let mut rng = StdRng::seed_from_u64(0xec_da9_f01); - let eval = traces.mains()[5]; + let eval = traces.mains()[4]; assert_eq!(dag_residual(&traces, eval, &mut rng), 0, "honest stack must balance"); let row = first_row_with_flag(eval, COL_IS_EC_CREATE); @@ -365,7 +365,7 @@ fn dag_sub_result_forged_unbalances() { // `ec_is` consumer — the rearrangement is load-bearing, not decorative. let traces = ec_dag_sub_from_pai_traces(); let mut rng = StdRng::seed_from_u64(0xec_da9_f03); - let eval = traces.mains()[5]; + let eval = traces.mains()[4]; assert_eq!(dag_residual(&traces, eval, &mut rng), 0, "honest stack must balance"); let row = first_ec_op_row(eval, COL_IS_SUB); diff --git a/crates/precompiles-prover/src/tests/ec_msm.rs b/crates/precompiles-prover/src/tests/ec_msm.rs index c56507bd3e..7f5dea4878 100644 --- a/crates/precompiles-prover/src/tests/ec_msm.rs +++ b/crates/precompiles-prover/src/tests/ec_msm.rs @@ -559,7 +559,7 @@ fn msm_resolve_duplicate_base_rejected() { #[should_panic(expected = "constraint not satisfied")] fn msm_resolve_run_expr_must_be_constant() { let traces = msm_resolve_two_term_traces(); - let eval = traces.mains()[5]; // the transcript-eval main + let eval = traces.mains()[4]; // the transcript-eval main let ncols = eval.width(); // The first absorb row of a 2-term run is non-boundary. diff --git a/crates/precompiles-prover/src/tests/mod.rs b/crates/precompiles-prover/src/tests/mod.rs index e0aa53391d..f3771d8ad3 100644 --- a/crates/precompiles-prover/src/tests/mod.rs +++ b/crates/precompiles-prover/src/tests/mod.rs @@ -90,17 +90,12 @@ where check_local_inputs(air, main, vec![Felt::ZERO; n]); } -/// The per-AIR `log_quotient_degree` — replicated from the public -/// `constraint_degree()` because 0.26 keeps the framework's own -/// `domain::log_quotient_degree` `pub(crate)`. This is the value the lqd -/// design-target smoke tests assert (= `⌈log₂ max(d−1, 1)⌉`, `d` the max -/// base/ext constraint-degree multiple). +/// The per-AIR quotient degree used by the design-target smoke tests. pub(crate) fn log_quotient_degree(air: &A) -> u8 where A: LiftedAir, { - let d = air.constraint_degree().max(); - miden_lifted_air::log2_ceil_u8(d.saturating_sub(1).max(1)) + miden_lifted_stark::log_quotient_degree::(air) } /// The `[preprocessed ++ main]` matrix the lookup eval reads for a chiplet diff --git a/crates/precompiles-prover/src/tests/uint_dag.rs b/crates/precompiles-prover/src/tests/uint_dag.rs index f5d078a13f..09e0e68def 100644 --- a/crates/precompiles-prover/src/tests/uint_dag.rs +++ b/crates/precompiles-prover/src/tests/uint_dag.rs @@ -111,10 +111,10 @@ fn horner_sign_alternation_full_stack() { // 22 eval rows (AND + zero + 6 leaves + 13 value ops + Is) pad to 32; fixed // uints live only in the store and verifier boundary correction, not eval rows. // The add relation count is unchanged; mul no longer has its own main - // (shares the store's merged trace at index 7). + // (shares the store's merged trace at index 5). let mains = traces.mains(); - assert_eq!(mains[5].height(), 32, "eval: 22 rows pad to 32"); - assert_eq!(mains[7].height(), 16, "uint-add: 7 two-row blocks pad to 8"); + assert_eq!(mains[4].height(), 32, "eval: 22 rows pad to 32"); + assert_eq!(mains[6].height(), 16, "uint-add: 7 two-row blocks pad to 8"); traces.check(); assert_balanced(&traces, &mut rng); @@ -153,9 +153,9 @@ fn op_dedup_collapses_repeated_nodes() { // Two recorded add ops (r once, w once), not three. let mains = traces.mains(); - assert_eq!(mains[7].height(), 4, "uint-add: exactly two two-row blocks"); + assert_eq!(mains[6].height(), 4, "uint-add: exactly two two-row blocks"); // r's single row carries out_mult 2 (consumed twice by w). - let eval = mains[5]; + let eval = mains[4]; let r_row = (0..eval.height()) .find(|row| { eval.values[row * EVAL_NUM_MAIN_COLS + COL_IS_ADD] == Felt::ONE @@ -261,12 +261,12 @@ fn forged_result_ptr_unbalances() { let mut rng = StdRng::seed_from_u64(0xf043_0001); let traces = mul_statement(&mut rng); - let mut tampered = traces.mains()[5].clone(); + let mut tampered = traces.mains()[4].clone(); let row = find_op_row(&tampered, COL_IS_MUL); tampered.values[row * EVAL_NUM_MAIN_COLS + COL_PTR] += Felt::ONE; let mut mains = traces.mains(); - mains[5] = &tampered; + mains[4] = &tampered; let [alpha, beta] = random_challenges(&mut rng); let challenges = Challenges::new(alpha, beta, MAX_MESSAGE_WIDTH, NUM_BUS_IDS); let residual = session_stack_residual(&mains, &[], &challenges); @@ -296,7 +296,7 @@ fn reencoded_op_id_passes_constraints_but_unbalances() { let root = session.assert_and_fold([claim]); let traces = session.finish(root); - let mut tampered = traces.mains()[5].clone(); + let mut tampered = traces.mains()[4].clone(); let row = find_op_row(&tampered, COL_IS_ADD); tampered.values[row * EVAL_NUM_MAIN_COLS + COL_IS_ADD] = Felt::ZERO; tampered.values[row * EVAL_NUM_MAIN_COLS + COL_IS_SUB] = Felt::ONE; @@ -308,7 +308,7 @@ fn reencoded_op_id_passes_constraints_but_unbalances() { // …but the bus refuses the re-encoded cap + re-wired relation. let mut mains = traces.mains(); - mains[5] = &tampered; + mains[4] = &tampered; let [alpha, beta] = random_challenges(&mut rng); let challenges = Challenges::new(alpha, beta, MAX_MESSAGE_WIDTH, NUM_BUS_IDS); let residual = session_stack_residual(&mains, &[], &challenges); diff --git a/crates/precompiles-prover/src/tests/vm_uint.rs b/crates/precompiles-prover/src/tests/vm_uint.rs index 284b00600f..78e6ebbb23 100644 --- a/crates/precompiles-prover/src/tests/vm_uint.rs +++ b/crates/precompiles-prover/src/tests/vm_uint.rs @@ -73,7 +73,7 @@ fn pin_claim_rows_commit_pin_ptr_but_vm_uint_rows_commit_bound_ptr() { let root = session.assert_and(root1, eq); let traces = session.finish(root); - let eval = traces.mains()[5]; + let eval = traces.mains()[4]; let row_value = |row: usize, col: usize| eval.values[row * EVAL_NUM_MAIN_COLS + col]; let pin_row = (0..eval.height()) diff --git a/crates/precompiles-prover/src/transcript/eval/mod.rs b/crates/precompiles-prover/src/transcript/eval/mod.rs index 27210020aa..5a3c826386 100644 --- a/crates/precompiles-prover/src/transcript/eval/mod.rs +++ b/crates/precompiles-prover/src/transcript/eval/mod.rs @@ -3,13 +3,13 @@ //! //! The narrow, central hasher + binder for the transcript DAG. Each //! active row evaluates one node: it hashes the node's preimage on -//! Poseidon2 and settles the node's `Binding`-bus tuple. The eval chip is -//! the sole provider of the `Binding` bus, except `KeccakNodeAir`, which -//! fuses its own terminal keccak `True` (there is no transient Keccak — -//! see the design notes). Domain chiplets (the `UintStore`, -//! `UintAdd` / `UintMul`, EC store/add/MSM chiplets) stay ptr-only and never -//! touch `Binding`; this chip hashes their DAG nodes and ptr-references their -//! relations. +//! Poseidon2 and settles the node's `Binding`-bus tuple. The eval chip +//! is the sole provider of the `Binding` bus, except the Keccak-node +//! band of `ChunkNodeSpongeAir`, which fuses its own terminal keccak +//! `True` (there is no transient Keccak — see the design notes). Domain +//! chiplets (the `UintStore`, `UintAdd` / `UintMul`, EC store/add/MSM +//! chiplets) stay ptr-only and never touch `Binding`; this chip hashes +//! their DAG nodes and ptr-references their relations. //! //! Node kinds are dispatched by a uniform one-hot `is_and + is_zero + //! is_uint_leaf + Σ op-flags = act`: the **Transcript AND-combinator** @@ -134,11 +134,10 @@ pub const COL_H_END: usize = COL_H_BEGIN + DIGEST_WIDTH; /// consumes — the row provides `Binding(0, True)` only. Boolean. pub const COL_IS_ZERO: usize = COL_H_END; /// Provide multiplicity for this node's `Binding(h, True)` = number of -/// parents that consume it (DAG sharing / dedup, mirroring -/// `KeccakNodeAir`'s `out_mult`). A plain count pinned to the -/// consumer count by `Binding` bus balance — not range-checked (see -/// the design notes); `0` on the root (no parent) and on -/// inactive rows. +/// parents that consume it (DAG sharing / dedup, mirroring the +/// Keccak-node band's `out_mult`). A plain count pinned to the consumer +/// count by `Binding` bus balance — not range-checked (see the design +/// notes); `0` on the root (no parent) and on inactive rows. pub const COL_OUT_MULT: usize = COL_IS_ZERO + 1; // ================================================================ diff --git a/crates/project/Cargo.toml b/crates/project/Cargo.toml index a9ab5b8bdf..4d239688ba 100644 --- a/crates/project/Cargo.toml +++ b/crates/project/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "miden-project" -version = "0.29.0" +version = "0.30.0" description = "Interface for working with Miden projects" documentation = "https://docs.rs/miden-project" readme = "README.md" diff --git a/crates/serde-utils/Cargo.toml b/crates/serde-utils/Cargo.toml index 6049d8c3cc..60d9237dae 100644 --- a/crates/serde-utils/Cargo.toml +++ b/crates/serde-utils/Cargo.toml @@ -10,7 +10,7 @@ name = "miden-serde-utils" readme = "README.md" repository.workspace = true rust-version.workspace = true -version = "0.29.0" +version = "0.30.0" [features] default = ["std"] diff --git a/crates/stark-transcript/Cargo.toml b/crates/stark-transcript/Cargo.toml index d4060b8523..91821a673b 100644 --- a/crates/stark-transcript/Cargo.toml +++ b/crates/stark-transcript/Cargo.toml @@ -7,7 +7,7 @@ name = "miden-stark-transcript" readme.workspace = true repository.workspace = true rust-version.workspace = true -version = "0.29.0" +version = "0.30.0" [lib] doctest = false diff --git a/crates/stateful-hasher/Cargo.toml b/crates/stateful-hasher/Cargo.toml index b33e059c6c..3447db2433 100644 --- a/crates/stateful-hasher/Cargo.toml +++ b/crates/stateful-hasher/Cargo.toml @@ -7,7 +7,7 @@ name = "miden-stateful-hasher" readme.workspace = true repository.workspace = true rust-version.workspace = true -version = "0.29.0" +version = "0.30.0" [lib] doctest = false diff --git a/crates/test-serde-macros/Cargo.toml b/crates/test-serde-macros/Cargo.toml index 400a263170..11f758044d 100644 --- a/crates/test-serde-macros/Cargo.toml +++ b/crates/test-serde-macros/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "miden-test-serde-macros" -version = "0.29.0" +version = "0.30.0" description = "Proc macros for serde roundtrip testing in Miden VM" readme = "README.md" categories = ["development-tools::testing", "no-std"] diff --git a/crates/test-utils/Cargo.toml b/crates/test-utils/Cargo.toml index a8176e59a3..d2f06e2e52 100644 --- a/crates/test-utils/Cargo.toml +++ b/crates/test-utils/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "miden-test-utils" -version = "0.29.0" +version = "0.30.0" description = "Test utilities for Miden VM programs" readme = "README.md" categories = ["development-tools::testing", "no-std"] diff --git a/crates/utils-core-derive/Cargo.toml b/crates/utils-core-derive/Cargo.toml index 1b566c4291..773c32d045 100644 --- a/crates/utils-core-derive/Cargo.toml +++ b/crates/utils-core-derive/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "miden-utils-core-derive" -version = "0.29.0" +version = "0.30.0" description = "Proc macro to derive enum dispatch trait implementations on miden-core structs" readme = "README.md" categories = ["development-tools::procedural-macro-helpers", "no-std"] diff --git a/crates/utils-diagnostics/Cargo.toml b/crates/utils-diagnostics/Cargo.toml index d5000e481d..af48676ff7 100644 --- a/crates/utils-diagnostics/Cargo.toml +++ b/crates/utils-diagnostics/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "miden-utils-diagnostics" -version = "0.29.0" +version = "0.30.0" description = "Diagnostic infrastructure used in the Miden assembler and VM" documentation = "https://docs.rs/miden-utils-diagnostics" readme = "README.md" diff --git a/crates/utils-indexing/Cargo.toml b/crates/utils-indexing/Cargo.toml index 5e48c7fc6e..4ab193a31b 100644 --- a/crates/utils-indexing/Cargo.toml +++ b/crates/utils-indexing/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "miden-utils-indexing" -version = "0.29.0" +version = "0.30.0" description = "Type-safe u32-indexed vector utilities for Miden" readme = "README.md" categories = ["development-tools", "no-std"] diff --git a/crates/utils-sync/Cargo.toml b/crates/utils-sync/Cargo.toml index 16fef49d72..24b21f34cc 100644 --- a/crates/utils-sync/Cargo.toml +++ b/crates/utils-sync/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "miden-utils-sync" -version = "0.29.0" +version = "0.30.0" description = "no-std compatible locking primitives for the Miden project" documentation = "https://docs.rs/miden-utils-sync" readme = "README.md" diff --git a/docs/src/design/chiplets/memory.md b/docs/src/design/chiplets/memory.md index 772d338aab..c796046bdd 100644 --- a/docs/src/design/chiplets/memory.md +++ b/docs/src/design/chiplets/memory.md @@ -182,7 +182,7 @@ where: - `idx0` and `idx1` are selector columns used to identify which element in the word is being accessed. Specifically, the index within the word is computed as `idx1 * 2 + idx0`. - However, when `ew` is set to $1$ (indicating that a word is accessed), these columns are meaningless and are set to $0$. - `clk` contains clock cycle at which the memory operation happened. Values in this column must increase monotonically for a given context and memory word but there can be gaps between two consecutive values of up to $2^{32}$. - - When the context and word address are unchanged, `clk` may stay the same, but only read operations are allowed. + - When the context and word address are unchanged, `clk` may stay the same, but only read operations are allowed. This includes any combination of word and element reads; a write may not share the same `(ctx, word_addr, clk)` tuple with any other access. - `v0, v1, v2, v3` columns contain field elements stored at a given context/word/clock cycle after the memory operation. - Columns `d0` and `d1` contain lower and upper $16$ bits of the delta between two consecutive context IDs, addresses, or clock cycles. Specifically: - When the context changes within a frame, these columns contain $(ctx' - ctx)$ in the "next" row. diff --git a/docs/src/user_docs/assembly/events.md b/docs/src/user_docs/assembly/events.md index dcc2275e87..00b4133bf1 100644 --- a/docs/src/user_docs/assembly/events.md +++ b/docs/src/user_docs/assembly/events.md @@ -15,6 +15,8 @@ Event names should be as unique as possible to avoid collisions with other libra - **`emit`** - Interrupts execution, hands control to host (1 cycle) - **`emit.`** - Expands to `push. emit drop` (3 cycles). Immediate IDs must come from `event("...")` constants or inline `event("...")`. +- **`trace`** - Emits the trace ID at the top of the stack as an optional, read-only trace event without consuming it (3 cycles) +- **`trace.`** - Emits a stack-neutral trace event (5 cycles). Immediate IDs must come from `event("...")` constants or inline `trace.event("...")`. ```miden # Using a constant @@ -36,27 +38,26 @@ push. emit drop ### Trace Events (optional read-only events) -Trace events are a special class of optional, read-only events. Unlike regular custom events, they cannot mutate the advice provider, and emitting one for which the host has no handler registered should not result in an error. +Trace events are a special class of optional, read-only events. Unlike regular custom events, they cannot mutate the advice provider, and a trace event with no registered handler is a no-op. -A trace event is emitted by pushing the user trace event ID and then the `sys::trace_event` system event ID before `emit`. +Use the `trace` instruction to emit a trace event. Like `emit`, the bare form reads an ID from the top of the stack without consuming it. The immediate forms accept IDs derived from event names, either through an `event("...")` constant or inline. ```miden +# Using a constant const MY_TRACE = event("miden_debug::println") -const SYS_EVENT = event("sys::trace_event") - -push.MY_TRACE -push.SYS_EVENT -emit -drop -drop +trace.MY_TRACE -# Since `emit.` expands to `push., emit, drop`, this can be shortened too: +# Inline form +trace.event("miden_debug::println") -push.MY_TRACE -emit.SYS_EVENT +# Stack form (any Felt - not validated) +push. +trace drop ``` -When the host trace handler runs, `sys::trace_event` is at stack position 0 and `MY_TRACE` is at stack position 1. Both sequences above are stack-neutral and take 5 cycles. +The bare `trace` instruction takes 3 cycles and leaves the stack unchanged. `trace.MY_TRACE` and `trace.event("...")` are stack-neutral and take 5 cycles. + +As an implementation detail, `trace.` lowers to `push. push. emit drop drop`. Plain `trace` lowers to `push. emit drop`. Thus, when the host trace handler runs, `sys::trace_event` is at stack position 0 and the user trace ID is at stack position 1. On the Rust side, hosts can register trace handlers via `DefaultHost::register_trace_handler`, or implement `SyncHost::on_trace` / `Host::on_trace`. Hosts that do not implement `on_trace` still execute programs containing trace events: the default implementation is a no-op, and trace events are not routed to the regular `on_event` handler. diff --git a/docs/src/user_docs/assembly/instruction_reference.md b/docs/src/user_docs/assembly/instruction_reference.md index 22db570164..854a25b62b 100644 --- a/docs/src/user_docs/assembly/instruction_reference.md +++ b/docs/src/user_docs/assembly/instruction_reference.md @@ -377,6 +377,8 @@ Instructions for communicating with the host through events. | ------------------ | ----------------- | ----------------- | ------ | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | | `emit.` | `[...]` | `[...]` | 3 | Emits an event with the specified `event_id` to the host. The net effect on the operand stack is no change (internally expands to `push. emit drop`). Immediate `event_id` must be defined via `const.ID=event("...")` or inlined as `emit.event("...")`. Events allow programs to communicate contextual information to the host for triggering appropriate actions. Example: `emit.event("foo")` or `emit.MY_EVENT` | | `emit` | `[event_id, ...]` | `[event_id, ...]` | 1 | Emits an event using the `event_id` from the top of the stack. The stack remains unchanged as the event_id is read without consuming it. This instruction reads the event ID from the stack but does not modify the stack depth. Example: with `push.1230` on stack, `emit` reads the event ID 1230 and executes the corresponding event handler. Defined system events are reserved and use names in the `sys::` namespace. | +| `trace.` | `[...]` | `[...]` | 5 | Emits an optional, read-only trace event with the specified `trace_id`. Expands to `push. push. emit drop drop`. Immediate `trace_id` must be defined via `const.ID=event("...")` or inlined as `trace.event("...")`. The instruction is stack-neutral. Example: `trace.event("foo")` or `trace.MY_TRACE`. If no handler is registered for the trace ID, the event is a no-op. | +| `trace` | `[trace_id, ...]` | `[trace_id, ...]` | 3 | Emits an optional, read-only trace event using the `trace_id` at the top of the stack without consuming it. Expands to `push. emit drop`. Trace handlers can inspect processor state but cannot mutate VM state or the advice provider. If no handler is registered for the trace ID, the event is a no-op. | | `log_deferred` | `[_, STMNT, _, ...]` | `[ROOT_NEW, OUT_RATE1, OUT_CAP, ...]` | 1 | Folds `STMNT` from `stack[4..8]` into the VM's rolling deferred root via `ROOT_NEW = rate0(Poseidon2([ROOT_PREV, STMNT, [1,0,0,0]]))`, using the internally maintained previous root and the `Tag::AND` capacity word `[1, 0, 0, 0]`. `STMNT` must be a registered statement for a precompile claim that evaluates to `TRUE`. Writes three output words, normally dropped by wrappers. Core-library facades and internal support code normally wrap this low-level opcode when precompile claims need to be logged. | ## Debugging Operations diff --git a/miden-vm/Cargo.toml b/miden-vm/Cargo.toml index 77f16fa8bd..a271afca25 100644 --- a/miden-vm/Cargo.toml +++ b/miden-vm/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "miden-vm" -version = "0.29.0" +version = "0.30.0" description = "Miden virtual machine" documentation = "https://docs.rs/miden-vm" readme = "README.md" diff --git a/miden-vm/tests/integration/operations/decorators/trace_events.rs b/miden-vm/tests/integration/operations/decorators/trace_events.rs index 0da66de6b3..30774e0c78 100644 --- a/miden-vm/tests/integration/operations/decorators/trace_events.rs +++ b/miden-vm/tests/integration/operations/decorators/trace_events.rs @@ -2,7 +2,7 @@ use std::sync::{Arc, Mutex}; use miden_assembly::Assembler; use miden_processor::{ - DefaultHost, ExecutionOptions, ProcessorState, Program, StackInputs, StackOutputs, + DefaultHost, ExecutionOptions, Felt, ProcessorState, Program, StackInputs, StackOutputs, advice::AdviceInputs, event::{EventName, SystemEvent, TraceError}, }; @@ -11,7 +11,10 @@ use super::TestHost; #[test] fn test_trace_event_handling() { - let trace_event_id = SystemEvent::TraceEvent.event_id().as_u64(); + let first_trace_name = "test::trace::first"; + let second_trace_name = "test::trace::second"; + let first_trace_id = EventName::new(first_trace_name).to_event_id().as_u64(); + let second_trace_id = EventName::new(second_trace_name).to_event_id().as_u64(); // Interleaving events and trace events to verify each get forwarded to the expected handler. let source = format!( @@ -20,25 +23,17 @@ fn test_trace_event_handling() { push.3000 emit drop - push.1000 - push.{trace_event_id} - emit - drop - drop + trace.event(\"{first_trace_name}\") push.4000 emit drop - push.2000 - push.{trace_event_id} - emit - drop - drop + trace.event(\"{second_trace_name}\") swapw dropw end" ); let program: Program = Assembler::default() - .assemble_program("program", &source) + .assemble_program("program", source) .unwrap() .unwrap_program(); let mut host = TestHost::default(); @@ -52,20 +47,15 @@ fn test_trace_event_handling() { .unwrap(); assert_eq!(host.event_handler, vec![3000, 4000]); - assert_eq!(host.trace_handler, vec![1000, 2000]); + assert_eq!(host.trace_handler, vec![first_trace_id, second_trace_id]); } /// Assembles a program that emits a single trace event. -fn trace_emit_program(trace_id_value: &str) -> String { - let trace_event_id = SystemEvent::TraceEvent.event_id().as_u64(); +fn trace_emit_program(trace_name: &str) -> String { format!( "\ begin - push.{trace_id_value} - push.{trace_event_id} - emit - drop - drop + trace.event(\"{trace_name}\") end" ) } @@ -73,8 +63,9 @@ fn trace_emit_program(trace_id_value: &str) -> String { /// An unhandled trace event must not abort execution. #[test] fn test_unhandled_trace_does_not_raise_error() { + let trace_name = "test::trace::unhandled"; let program: Program = Assembler::default() - .assemble_program("program", trace_emit_program("12345")) + .assemble_program("program", trace_emit_program(trace_name)) .unwrap() .unwrap_program(); @@ -94,28 +85,19 @@ fn test_unhandled_trace_does_not_raise_error() { #[test] fn test_trace_handler_registry() { - let trace_name = EventName::new("test::trace::going_through_registry"); - let trace_id = trace_name.to_event_id().as_u64(); + let trace_name = "test::trace::going_through_registry"; + let trace_id = EventName::new(trace_name).to_event_id().as_u64(); // Emit the same registered trace id twice. - let trace_event_id = SystemEvent::TraceEvent.event_id().as_u64(); let source = format!( "\ begin - push.{trace_id} - push.{trace_event_id} - emit - drop - drop - push.{trace_id} - push.{trace_event_id} - emit - drop - drop + trace.event(\"{trace_name}\") + trace.event(\"{trace_name}\") end" ); let program: Program = Assembler::default() - .assemble_program("program", &source) + .assemble_program("program", source) .unwrap() .unwrap_program(); @@ -129,7 +111,8 @@ fn test_trace_handler_registry() { }; let mut host = DefaultHost::default(); - host.register_trace_handler(trace_name, Arc::new(recorder)).unwrap(); + host.register_trace_handler(EventName::new(trace_name), Arc::new(recorder)) + .unwrap(); miden_processor::execute_sync( &program, @@ -143,3 +126,64 @@ fn test_trace_handler_registry() { let recorded = recorded.lock().unwrap(); assert_eq!(*recorded, vec![trace_id, trace_id]); } + +/// A trace event generated via the `trace` instruction, reading the trace ID from the stack. +#[test] +fn test_trace_event_from_stack() { + let source = "\ + begin + trace + end"; + let program: Program = Assembler::default() + .assemble_program("program", source) + .unwrap() + .unwrap_program(); + + let mut host = TestHost::default(); + let output = miden_processor::execute_sync( + &program, + StackInputs::new(&[Felt::from_u32(1000)]).unwrap(), + AdviceInputs::default(), + &mut host, + ExecutionOptions::default(), + ) + .unwrap(); + + assert_eq!(host.trace_handler, vec![1000]); + assert!(host.event_handler.is_empty()); + assert_eq!(output.stack.get_element(0).unwrap().as_canonical_u64(), 1000); +} + +/// A trace event generated manually by pushing the trace ID and the `sys::trace_event` system +/// event ID onto the stack before `emit`, without using the `trace` instruction. +#[test] +fn test_trace_event_manual_emit() { + let trace_event_id = SystemEvent::TraceEvent.event_id().as_u64(); + let source = format!( + "\ + begin + push.1000 + push.{trace_event_id} + emit + drop + drop + end" + ); + let program: Program = Assembler::default() + .assemble_program("program", source) + .unwrap() + .unwrap_program(); + + let mut host = TestHost::default(); + miden_processor::execute_sync( + &program, + StackInputs::default(), + AdviceInputs::default(), + &mut host, + ExecutionOptions::default(), + ) + .unwrap(); + + assert_eq!(host.trace_handler, vec![1000]); + assert!(host.event_handler.is_empty()); +} diff --git a/miden-vm/tests/integration/operations/sys_ops.rs b/miden-vm/tests/integration/operations/sys_ops.rs index eae5ba937c..9823eefb1f 100644 --- a/miden-vm/tests/integration/operations/sys_ops.rs +++ b/miden-vm/tests/integration/operations/sys_ops.rs @@ -1,6 +1,6 @@ use miden_processor::{ ExecutionError, ProcessorState, ZERO, - event::{EventName, NoopEventHandler, SystemEvent}, + event::{EventName, NoopEventHandler}, mast, operation::OperationError, }; @@ -98,23 +98,19 @@ fn emit() { #[test] fn emit_trace_event_without_handler() { - let trace_name = EventName::new("test::emit_trace::no_handler"); - let trace_id = trace_name.to_event_id().as_felt(); - let trace_sys_event_id = SystemEvent::TraceEvent.event_id(); + let trace_name = "test::emit_trace::no_handler"; - let source = format!("push.{trace_id} push.{trace_sys_event_id} emit drop drop"); + let source = format!("trace.event(\"{trace_name}\")"); let test = build_op_test!(&source, &[0, 0, 0, 0]); test.check_constraints(); } #[test] fn emit_trace_event_with_handler() { - let trace_name = EventName::new("test::emit_trace::handler"); - let trace_id = trace_name.to_event_id(); - let trace_sys_event_id = SystemEvent::TraceEvent.event_id(); + let trace_name = "test::emit_trace::handler"; - let source = format!("push.{trace_id} push.{trace_sys_event_id} emit drop drop"); + let source = format!("trace.event(\"{trace_name}\")"); let test = build_op_test!(&source, &[0, 0, 0, 0]) - .with_trace_handler(trace_name, |_: &ProcessorState| Ok(())); + .with_trace_handler(EventName::new(trace_name), |_: &ProcessorState| Ok(())); test.check_constraints(); } diff --git a/processor/Cargo.toml b/processor/Cargo.toml index 5458cbfa2c..118bf2da9e 100644 --- a/processor/Cargo.toml +++ b/processor/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "miden-processor" -version = "0.29.0" +version = "0.30.0" description = "Miden VM processor" documentation = "https://docs.rs/miden-processor" readme = "README.md" diff --git a/processor/src/host/handlers.rs b/processor/src/host/handlers.rs index 8c605eed07..cdebb6043c 100644 --- a/processor/src/host/handlers.rs +++ b/processor/src/host/handlers.rs @@ -180,10 +180,16 @@ impl Debug for EventHandlerRegistry { /// Handles an optional, read-only trace event emitted by the VM. /// -/// Trace events are emitted by pushing the user trace event ID and then -/// [`SystemEvent::TraceEvent`] onto the stack before `emit`. When the handler runs, -/// [`SystemEvent::TraceEvent`] is at stack position 0 and the user trace event ID is at position -/// 1. The handler receives a read-only [`ProcessorState`] and cannot return advice mutations. +/// Assembly programs emit trace events with `trace`, `trace.CONST`, or `trace.event("...")`. When +/// the handler runs, [`SystemEvent::TraceEvent`] is at stack position 0 and the user trace event ID +/// is at position 1. The handler receives a read-only [`ProcessorState`] and cannot return advice +/// mutations. +/// +/// The instruction expansions are: +/// +/// - `trace` expands to `push. emit drop`. +/// - `trace.CONST` and `trace.event("...")` expand to `push. push. emit +/// drop drop`. pub trait TraceHandler: Send + Sync + 'static { /// Handles the trace event when triggered. fn on_trace(&self, process: &ProcessorState) -> Result<(), TraceError>; diff --git a/processor/src/host/mod.rs b/processor/src/host/mod.rs index 2db7517959..d78b225d2a 100644 --- a/processor/src/host/mod.rs +++ b/processor/src/host/mod.rs @@ -129,7 +129,7 @@ pub trait SyncHost: BaseHost { /// Trace events are optional, read-only events. [`SystemEvent::TraceEvent`] is at stack /// position 0 and the user trace event ID is at position 1 when this handler is called. The /// handler cannot mutate the advice provider. Hosts that do not care about trace events can use - /// this default no-op implementation. Hosts are expected to not raise an error on encountering + /// this default no-op implementation. Hosts are expected not to raise an error on encountering /// a trace event for which no handler is registered. /// /// Return errors without event names or IDs - the caller will enrich them via @@ -176,7 +176,7 @@ pub trait Host: BaseHost { /// Trace events are optional, read-only events. [`SystemEvent::TraceEvent`] is at stack /// position 0 and the user trace event ID is at position 1 when this handler is called. The /// handler cannot mutate the advice provider. Hosts that do not care about trace events can use - /// this default no-op implementation. Hosts are expected to nat raise an error on encountering + /// this default no-op implementation. Hosts are expected not to raise an error on encountering /// a trace event for which no handler is registered. /// /// Return errors without event names or IDs - the caller will enrich them via diff --git a/processor/src/test_utils/non_tracing_test_host.rs b/processor/src/test_utils/non_tracing_test_host.rs index df8a637b30..ec45bff81b 100644 --- a/processor/src/test_utils/non_tracing_test_host.rs +++ b/processor/src/test_utils/non_tracing_test_host.rs @@ -71,7 +71,7 @@ mod tests { use miden_assembly::Assembler; use super::NonTracingTestHost; - use crate::{AdviceInputs, ExecutionOptions, Program, StackInputs, event::SystemEvent}; + use crate::{AdviceInputs, ExecutionOptions, Program, StackInputs}; /// A host which does not implement `on_trace` should still execute trace events gracefully via /// the default no-op implementation, and trace events must not be routed to `on_event`. @@ -80,7 +80,6 @@ mod tests { const REGULAR_EVENT_ID_1: u64 = 3000; const REGULAR_EVENT_ID_2: u64 = 4000; const TRACE_ID: u32 = 1000; - let trace_sys_event_id = SystemEvent::TraceEvent.event_id().as_u64(); let source = format!( "\ @@ -89,9 +88,7 @@ mod tests { emit drop push.{TRACE_ID} - push.{trace_sys_event_id} - emit - drop + trace drop push.{REGULAR_EVENT_ID_2} emit diff --git a/processor/src/test_utils/test_host.rs b/processor/src/test_utils/test_host.rs index 3327f8e246..9d51f23ccd 100644 --- a/processor/src/test_utils/test_host.rs +++ b/processor/src/test_utils/test_host.rs @@ -211,26 +211,21 @@ mod tests { use miden_assembly::Assembler; use super::TestHost; - use crate::{AdviceInputs, ExecutionOptions, Program, StackInputs, event::SystemEvent}; + use crate::{AdviceInputs, ExecutionOptions, Program, StackInputs}; #[test] fn test_host_records_trace_and_snapshot() { const TRACE_ID_1: u64 = 100; const TRACE_ID_2: u64 = 200; - let trace_sys_event_id = SystemEvent::TraceEvent.event_id().as_u64(); let source = format!( "\ begin push.{TRACE_ID_1} - push.{trace_sys_event_id} - emit - drop + trace drop push.{TRACE_ID_2} - push.{trace_sys_event_id} - emit - drop + trace drop end" ); diff --git a/processor/src/tests/mod.rs b/processor/src/tests/mod.rs index c4f2cba554..31f42a4663 100644 --- a/processor/src/tests/mod.rs +++ b/processor/src/tests/mod.rs @@ -17,7 +17,7 @@ use crate::{ BaseHost, DefaultHost, FastProcessor, KernelDescriptor, LoadedMastForest, ONE, ProcessorState, Program, StackInputs, SyncHost, Word, ZERO, advice::{AdviceInputs, AdviceMap, AdviceMutation}, - event::{EventError, EventHandler, EventName, SystemEvent, TraceError, TraceHandler}, + event::{EventError, EventHandler, EventName, TraceError, TraceHandler}, operation::Operation, }; @@ -284,18 +284,15 @@ fn test_diagnostic_host_event_error_uses_emit_location() { } #[test] -fn test_diagnostic_host_trace_error_uses_emit_location() { +fn test_diagnostic_host_trace_error_uses_trace_location() { let trace = EventName::new("test::host_trace_error"); let trace_id = trace.to_event_id(); - let trace_sys_event_id = SystemEvent::TraceEvent.event_id(); let source_manager = Arc::new(DefaultSourceManager::default()); let source = format!( " begin - push.{trace_id} - push.{trace_sys_event_id} - emit + trace.event(\"{trace}\") end" ); let package = Assembler::new(source_manager.clone()) @@ -319,11 +316,10 @@ fn test_diagnostic_host_trace_error_uses_emit_location() { // Name and id of the user defined trace event are shown format!(" x error during processing of event '{trace}' (ID: {trace_id})"), " `-> dummy host trace failure", - regex!(r#",-\[.*:5:13\]"#), - format!(" 4 | push.{trace_sys_event_id}"), - " 5 | emit", - regex!(r#":\s+\^\^\^"#), - " 6 | end", + regex!(r#",-\[.*:3:13\]"#), + r#" 3 | trace.event("test::host_trace_error")"#, + regex!(r#":\s+\^+"#), + " 4 | end", " `----" ); } diff --git a/processor/src/trace/chiplets/memory/mod.rs b/processor/src/trace/chiplets/memory/mod.rs index f302168f4b..76657054eb 100644 --- a/processor/src/trace/chiplets/memory/mod.rs +++ b/processor/src/trace/chiplets/memory/mod.rs @@ -165,7 +165,7 @@ impl Memory { /// /// # Errors /// - Returns an error if the address is equal or greater than 2^32. - /// - Returns an error if the same address is accessed more than once in the same clock cycle. + /// - Returns an error if the addressed word was previously written in the same clock cycle. pub fn read(&mut self, ctx: ContextId, addr: Felt, clk: RowIndex) -> Result { let addr: u32 = addr .as_canonical_u64() @@ -183,7 +183,7 @@ impl Memory { /// # Errors /// - Returns an error if the address is equal or greater than 2^32. /// - Returns an error if the address is not aligned to a word boundary. - /// - Returns an error if the same address is accessed more than once in the same clock cycle. + /// - Returns an error if the addressed word was previously written in the same clock cycle. pub fn read_word( &mut self, ctx: ContextId, diff --git a/processor/src/trace/chiplets/memory/segment.rs b/processor/src/trace/chiplets/memory/segment.rs index 84c7d63b7b..d3db2bccaa 100644 --- a/processor/src/trace/chiplets/memory/segment.rs +++ b/processor/src/trace/chiplets/memory/segment.rs @@ -114,7 +114,7 @@ impl MemorySegmentTrace { /// If the element at the specified address hasn't been previously written to, ZERO is returned. /// /// # Errors - /// - Returns an error if the same address is accessed more than once in the same clock cycle. + /// - Returns an error if the addressed word was previously written in the same clock cycle. pub fn read(&mut self, ctx: ContextId, addr: u32, clk: Felt) -> Result { let (word_addr, addr_idx_in_word) = addr_to_word_addr_and_idx(addr); @@ -138,7 +138,7 @@ impl MemorySegmentTrace { /// - Assumes that the address is word aligned. /// /// # Errors - /// - Returns an error if the same address is accessed more than once in the same clock cycle. + /// - Returns an error if the addressed word was previously written in the same clock cycle. pub fn read_word( &mut self, ctx: ContextId, @@ -283,7 +283,7 @@ impl MemorySegmentTrace { /// was read. /// /// # Errors - /// - Returns an error if the same address is accessed more than once in the same clock cycle. + /// - Returns an error if the addressed word was previously written in the same clock cycle. fn read_word_helper( &mut self, ctx: ContextId, diff --git a/processor/tests/async_compat.rs b/processor/tests/async_compat.rs index bfc376e5aa..39706ce365 100644 --- a/processor/tests/async_compat.rs +++ b/processor/tests/async_compat.rs @@ -6,7 +6,7 @@ use miden_processor::{ BaseHost, DefaultHost, ExecutionOptions, FastProcessor, Felt, FutureMaybeSend, Host, LoadedMastForest, ProcessorState, StackInputs, Word, advice::{AdviceInputs, AdviceMutation}, - event::{EventError, EventName, SystemEvent, TraceError}, + event::{EventError, EventName, TraceError}, }; struct YieldingAsyncHost { @@ -76,15 +76,10 @@ fn simple_program() -> miden_processor::Program { } fn emit_trace_program() -> miden_processor::Program { - let trace_name = EventName::new("test::async::trace_emit"); - let trace_id = trace_name.to_event_id().as_u64(); - let trace_sys_event_id = SystemEvent::TraceEvent.event_id(); + let trace_name = "test::async::trace_emit"; Assembler::default() - .assemble_program( - "program", - format!("begin push.{trace_id} push.{trace_sys_event_id} emit drop drop end"), - ) + .assemble_program("program", format!("begin trace.event(\"{trace_name}\") end")) .expect("program should compile") .unwrap_program() } diff --git a/prover/Cargo.toml b/prover/Cargo.toml index b61c2eb765..fa70089b49 100644 --- a/prover/Cargo.toml +++ b/prover/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "miden-prover" -version = "0.29.0" +version = "0.30.0" description = "Miden VM prover" documentation = "https://docs.rs/miden-prover" readme = "README.md" diff --git a/tools/miden-core-fuzz/Cargo.lock b/tools/miden-core-fuzz/Cargo.lock index 89120cafec..ec4e418bce 100644 --- a/tools/miden-core-fuzz/Cargo.lock +++ b/tools/miden-core-fuzz/Cargo.lock @@ -717,7 +717,7 @@ checksum = "cf8baf1c55e62ffcace7a9f06f4bd9cd3f0c4beb022d3b367256b91b87513d98" [[package]] name = "miden-assembly" -version = "0.29.0" +version = "0.30.0" dependencies = [ "log", "miden-assembly-syntax", @@ -732,7 +732,7 @@ dependencies = [ [[package]] name = "miden-assembly-syntax" -version = "0.29.0" +version = "0.30.0" dependencies = [ "log", "miden-assembly-syntax-cst", @@ -751,7 +751,7 @@ dependencies = [ [[package]] name = "miden-assembly-syntax-cst" -version = "0.29.0" +version = "0.30.0" dependencies = [ "miden-debug-types", "miden-rowan", @@ -761,7 +761,7 @@ dependencies = [ [[package]] name = "miden-core" -version = "0.29.0" +version = "0.30.0" dependencies = [ "derive_more", "log", @@ -792,7 +792,7 @@ dependencies = [ [[package]] name = "miden-crypto" -version = "0.29.0" +version = "0.30.0" dependencies = [ "blake3", "cc", @@ -831,7 +831,7 @@ dependencies = [ [[package]] name = "miden-crypto-derive" -version = "0.29.0" +version = "0.30.0" dependencies = [ "quote", "syn 2.0.119", @@ -839,7 +839,7 @@ dependencies = [ [[package]] name = "miden-debug-types" -version = "0.29.0" +version = "0.30.0" dependencies = [ "memchr", "miden-crypto", @@ -857,7 +857,7 @@ dependencies = [ [[package]] name = "miden-field" -version = "0.29.0" +version = "0.30.0" dependencies = [ "miden-serde-utils", "num-bigint 0.5.1", @@ -883,7 +883,7 @@ dependencies = [ [[package]] name = "miden-lifted-air" -version = "0.29.0" +version = "0.30.0" dependencies = [ "p3-air", "p3-challenger", @@ -895,7 +895,7 @@ dependencies = [ [[package]] name = "miden-lifted-stark" -version = "0.29.0" +version = "0.30.0" dependencies = [ "miden-lifted-air", "miden-stark-transcript", @@ -916,7 +916,7 @@ dependencies = [ [[package]] name = "miden-mast-package" -version = "0.29.0" +version = "0.30.0" dependencies = [ "hashbrown", "log", @@ -968,7 +968,7 @@ dependencies = [ [[package]] name = "miden-package-registry" -version = "0.29.0" +version = "0.30.0" dependencies = [ "miden-assembly-syntax", "miden-core", @@ -982,7 +982,7 @@ dependencies = [ [[package]] name = "miden-project" -version = "0.29.0" +version = "0.30.0" dependencies = [ "miden-assembly-syntax", "miden-core", @@ -1007,7 +1007,7 @@ dependencies = [ [[package]] name = "miden-serde-utils" -version = "0.29.0" +version = "0.30.0" dependencies = [ "p3-field", "p3-goldilocks", @@ -1016,7 +1016,7 @@ dependencies = [ [[package]] name = "miden-stark-transcript" -version = "0.29.0" +version = "0.30.0" dependencies = [ "p3-challenger", "p3-field", @@ -1026,7 +1026,7 @@ dependencies = [ [[package]] name = "miden-stateful-hasher" -version = "0.29.0" +version = "0.30.0" dependencies = [ "p3-field", "p3-symmetric", @@ -1034,7 +1034,7 @@ dependencies = [ [[package]] name = "miden-utils-core-derive" -version = "0.29.0" +version = "0.30.0" dependencies = [ "proc-macro2", "quote", @@ -1043,7 +1043,7 @@ dependencies = [ [[package]] name = "miden-utils-diagnostics" -version = "0.29.0" +version = "0.30.0" dependencies = [ "miden-debug-types", "miden-miette", @@ -1052,7 +1052,7 @@ dependencies = [ [[package]] name = "miden-utils-indexing" -version = "0.29.0" +version = "0.30.0" dependencies = [ "miden-serde-utils", "proptest", @@ -1062,7 +1062,7 @@ dependencies = [ [[package]] name = "miden-utils-sync" -version = "0.29.0" +version = "0.30.0" dependencies = [ "lock_api", "loom", @@ -1072,7 +1072,7 @@ dependencies = [ [[package]] name = "midenc-hir-type" -version = "0.10.0" +version = "0.11.0" dependencies = [ "miden-formatting", "miden-serde-utils", diff --git a/tools/miden-crypto-fuzz/Cargo.lock b/tools/miden-crypto-fuzz/Cargo.lock index ce60c399dd..ecf4867284 100644 --- a/tools/miden-crypto-fuzz/Cargo.lock +++ b/tools/miden-crypto-fuzz/Cargo.lock @@ -513,7 +513,7 @@ dependencies = [ [[package]] name = "miden-crypto" -version = "0.29.0" +version = "0.30.0" dependencies = [ "blake3", "cc", @@ -553,7 +553,7 @@ dependencies = [ [[package]] name = "miden-crypto-derive" -version = "0.29.0" +version = "0.30.0" dependencies = [ "quote", "syn 2.0.119", @@ -569,7 +569,7 @@ dependencies = [ [[package]] name = "miden-field" -version = "0.29.0" +version = "0.30.0" dependencies = [ "miden-serde-utils", "num-bigint 0.5.1", @@ -586,7 +586,7 @@ dependencies = [ [[package]] name = "miden-lifted-air" -version = "0.29.0" +version = "0.30.0" dependencies = [ "p3-air", "p3-challenger", @@ -598,7 +598,7 @@ dependencies = [ [[package]] name = "miden-lifted-stark" -version = "0.29.0" +version = "0.30.0" dependencies = [ "miden-lifted-air", "miden-stark-transcript", @@ -619,7 +619,7 @@ dependencies = [ [[package]] name = "miden-serde-utils" -version = "0.29.0" +version = "0.30.0" dependencies = [ "p3-field", "p3-goldilocks", @@ -628,7 +628,7 @@ dependencies = [ [[package]] name = "miden-stark-transcript" -version = "0.29.0" +version = "0.30.0" dependencies = [ "p3-challenger", "p3-field", @@ -638,7 +638,7 @@ dependencies = [ [[package]] name = "miden-stateful-hasher" -version = "0.29.0" +version = "0.30.0" dependencies = [ "p3-field", "p3-symmetric", diff --git a/tools/miden-serde-utils-fuzz/Cargo.lock b/tools/miden-serde-utils-fuzz/Cargo.lock index 71950bca25..ac86503707 100644 --- a/tools/miden-serde-utils-fuzz/Cargo.lock +++ b/tools/miden-serde-utils-fuzz/Cargo.lock @@ -101,7 +101,7 @@ dependencies = [ [[package]] name = "miden-serde-utils" -version = "0.29.0" +version = "0.30.0" dependencies = [ "p3-field", "p3-goldilocks", diff --git a/verifier/Cargo.toml b/verifier/Cargo.toml index 0a9c523e09..ec16ac1584 100644 --- a/verifier/Cargo.toml +++ b/verifier/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "miden-verifier" -version = "0.29.0" +version = "0.30.0" description = "Miden VM execution verifier" documentation = "https://docs.rs/miden-verifier" readme = "README.md"