From 4711613076877a895652585506fed6faaa3b3a62 Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Sun, 8 Jun 2025 17:59:52 -0400 Subject: [PATCH 01/32] Establish entry --- .../native/compiler/src/asm/compiler.rs | 9 +++++ .../native/compiler/src/asm/instruction.rs | 8 +++++ .../native/compiler/src/conversion/mod.rs | 9 +++++ .../native/compiler/src/ir/instructions.rs | 7 ++++ extensions/native/compiler/src/ir/poseidon.rs | 34 +++++++++++++++++++ 5 files changed, 67 insertions(+) diff --git a/extensions/native/compiler/src/asm/compiler.rs b/extensions/native/compiler/src/asm/compiler.rs index a09c8a217e..e75e6b1f9f 100644 --- a/extensions/native/compiler/src/asm/compiler.rs +++ b/extensions/native/compiler/src/asm/compiler.rs @@ -489,6 +489,15 @@ impl + TwoAdicField> AsmCo DslIr::HintBitsF(var, len) => { self.push(AsmInstruction::HintBits(var.fp(), len), debug_info); } + DslIr::Poseidon2MultiObserve(dst, init_pos, arr_ptr, len) => { + match dst { + Array::Dyn(dst, _) => self.push( + AsmInstruction::Poseidon2MultiObserve(dst.fp(), init_pos.fp(), arr_ptr.fp(), len.get_var().fp()), + debug_info, + ), + _ => unimplemented!(), + } + }, DslIr::Poseidon2PermuteBabyBear(dst, src) => match (dst, src) { (Array::Dyn(dst, _), Array::Dyn(src, _)) => self.push( AsmInstruction::Poseidon2Permute(dst.fp(), src.fp()), diff --git a/extensions/native/compiler/src/asm/instruction.rs b/extensions/native/compiler/src/asm/instruction.rs index 1aa5ea8527..cd4990b08b 100644 --- a/extensions/native/compiler/src/asm/instruction.rs +++ b/extensions/native/compiler/src/asm/instruction.rs @@ -110,6 +110,11 @@ pub enum AsmInstruction { /// Halt. Halt, + /// Absorbs multiple base elements into a duplex transcript with Poseidon2 permutation + /// (sponge_state, init_pos, arr_ptr, len) + /// Returns the final index position of hash sponge + Poseidon2MultiObserve(i32, i32, i32, i32), + /// Perform a Poseidon2 permutation on state starting at address `lhs` /// and store new state at `rhs`. /// (a, b) are pointers to (lhs, rhs). @@ -334,6 +339,9 @@ impl> AsmInstruction { AsmInstruction::Trap => write!(f, "trap"), AsmInstruction::Halt => write!(f, "halt"), AsmInstruction::HintBits(src, len) => write!(f, "hint_bits ({})fp, {}", src, len), + AsmInstruction::Poseidon2MultiObserve(dst, init_pos, arr, len) => { + write!(f, "poseidon2_multi_observe ({})fp, ({})fp ({})fp ({})fp", dst, init_pos, arr, len) + } AsmInstruction::Poseidon2Permute(dst, lhs) => { write!(f, "poseidon2_permute ({})fp, ({})fp", dst, lhs) } diff --git a/extensions/native/compiler/src/conversion/mod.rs b/extensions/native/compiler/src/conversion/mod.rs index 9c3fc8d752..dc73d6fbab 100644 --- a/extensions/native/compiler/src/conversion/mod.rs +++ b/extensions/native/compiler/src/conversion/mod.rs @@ -441,6 +441,15 @@ fn convert_instruction>( AS::Native, AS::Native, )], + AsmInstruction::Poseidon2MultiObserve(dst, init, arr, len) => vec![], + // vec![inst( + // options.opcode_with_offset(Poseidon2Opcode::PERM_POS2), + // i32_f(dst), + // i32_f(src), + // F::ZERO, + // AS::Native, + // AS::Native, + // )], AsmInstruction::Poseidon2Compress(dst, src1, src2) => vec![inst( options.opcode_with_offset(Poseidon2Opcode::COMP_POS2), i32_f(dst), diff --git a/extensions/native/compiler/src/ir/instructions.rs b/extensions/native/compiler/src/ir/instructions.rs index 9159c5775b..0e7f1aad55 100644 --- a/extensions/native/compiler/src/ir/instructions.rs +++ b/extensions/native/compiler/src/ir/instructions.rs @@ -208,6 +208,13 @@ pub enum DslIr { /// Permutes an array of Bn254 elements using Poseidon2 (output = p2_permute(array)). Should /// only be used when target is a circuit. CircuitPoseidon2Permute([Var; 3]), + /// Absorbs an array of baby bear elements into a duplex transcript with Poseidon2 permutations (output = p2_multi_observe(array, els)). + Poseidon2MultiObserve( + Array>, // sponge_state (array) + Var, // initial input_ptr position + Ptr, // input array (els) + Usize, // len of els + ), // Miscellaneous instructions. /// Prints a variable. diff --git a/extensions/native/compiler/src/ir/poseidon.rs b/extensions/native/compiler/src/ir/poseidon.rs index 12ec526c89..395d735b59 100644 --- a/extensions/native/compiler/src/ir/poseidon.rs +++ b/extensions/native/compiler/src/ir/poseidon.rs @@ -1,6 +1,8 @@ use openvm_native_compiler_derive::iter_zip; use openvm_stark_backend::p3_field::FieldAlgebra; +use crate::ir::Variable; + use super::{Array, ArrayLike, Builder, Config, DslIr, Ext, Felt, MemIndex, Ptr, Usize, Var}; pub const DIGEST_SIZE: usize = 8; @@ -8,6 +10,38 @@ pub const HASH_RATE: usize = 8; pub const PERMUTATION_WIDTH: usize = 16; impl Builder { + /// Extends native VM ability to observe multiple base elements in one opcode operation + /// Absorbs elements sequentially at the RATE portion of sponge state and performs as many permutations as necessary. + /// Returns the index position of the input_ptr and the final sponge state. + /// + /// [Reference](https://docs.rs/p3-poseidon2/latest/p3_poseidon2/struct.Poseidon2.html) + pub fn poseidon2_multi_observe( + &mut self, + sponge_state: &Array>, + input_ptr: Ptr, + io_full_ptr: Ptr, + arr: &Array>, + ) -> Usize { + match sponge_state { + Array::Fixed(values) => { + panic!("Poseidon2 permutation is not allowed on fixed arrays"); + } + Array::Dyn(ptr, len) => { + let init_pos: Var = Var::uninit(self); + self.assign(&init_pos, io_full_ptr.address - input_ptr.address); + + self.operations.push(DslIr::Poseidon2MultiObserve( + sponge_state.clone(), + init_pos, + *ptr, + len.clone(), + )); + + Usize::Var(init_pos) + } + } + } + /// Applies the Poseidon2 permutation to the given array. /// /// [Reference](https://docs.rs/p3-poseidon2/latest/p3_poseidon2/struct.Poseidon2.html) From 0354d4e7ad7a414de2262be3f8a3f3de9aa40f5c Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Tue, 10 Jun 2025 03:28:47 -0400 Subject: [PATCH 02/32] Add opcode MULTI_OBSERVE --- extensions/native/circuit/src/extension.rs | 1 + .../native/circuit/src/poseidon2/chip.rs | 41 ++++++++++++++++++- .../native/circuit/src/poseidon2/tests.rs | 4 +- .../native/compiler/src/asm/compiler.rs | 11 ++--- .../native/compiler/src/conversion/mod.rs | 21 ++++++---- .../native/compiler/src/ir/instructions.rs | 2 +- extensions/native/compiler/src/ir/poseidon.rs | 38 ++++++++++------- extensions/native/compiler/src/lib.rs | 1 + 8 files changed, 86 insertions(+), 33 deletions(-) diff --git a/extensions/native/circuit/src/extension.rs b/extensions/native/circuit/src/extension.rs index 385c9392ac..c7dba9f87c 100644 --- a/extensions/native/circuit/src/extension.rs +++ b/extensions/native/circuit/src/extension.rs @@ -203,6 +203,7 @@ impl VmExtension for Native { VerifyBatchOpcode::VERIFY_BATCH.global_opcode(), Poseidon2Opcode::PERM_POS2.global_opcode(), Poseidon2Opcode::COMP_POS2.global_opcode(), + Poseidon2Opcode::MULTI_OBSERVE.global_opcode(), ], )?; diff --git a/extensions/native/circuit/src/poseidon2/chip.rs b/extensions/native/circuit/src/poseidon2/chip.rs index 426b089a9c..d2bb11b2b4 100644 --- a/extensions/native/circuit/src/poseidon2/chip.rs +++ b/extensions/native/circuit/src/poseidon2/chip.rs @@ -9,7 +9,7 @@ use openvm_circuit::{ use openvm_instructions::{instruction::Instruction, program::DEFAULT_PC_STEP, LocalOpcode}; use openvm_native_compiler::{ conversion::AS, - Poseidon2Opcode::{COMP_POS2, PERM_POS2}, + Poseidon2Opcode::{COMP_POS2, PERM_POS2, MULTI_OBSERVE}, VerifyBatchOpcode::VERIFY_BATCH, }; use openvm_poseidon2_air::{Poseidon2Config, Poseidon2SubAir, Poseidon2SubChip}; @@ -485,6 +485,43 @@ impl InstructionExecutor initial_log_height: initial_log_height as usize, top_level, }); + } else if instruction.opcode == MULTI_OBSERVE.global_opcode() { + let &Instruction { + a: output_register, + b: input_register_1, + c: input_register_2, + d: input_register_3, + e: register_address_space, + f: data_address_space, + .. + } = instruction; + + let (_, sponge_ptr) = memory.read_cell(data_address_space, output_register); + let (_, arr_ptr) = memory.read_cell(data_address_space, input_register_2); + + let init_pos_read = memory.read_cell(register_address_space, input_register_1); + let mut pos = init_pos_read.1.as_canonical_u32() as usize; + + let len_read = memory.read_cell(register_address_space, input_register_3); + let len = len_read.1.as_canonical_u32() as usize; + + for i in 0..len { + let mod_pos = pos % CHUNK; + let n_read = memory.read_cell(register_address_space, arr_ptr + F::from_canonical_usize(i)); + let n_f = n_read.1; + + memory.write_cell(register_address_space, sponge_ptr + F::from_canonical_usize(mod_pos), n_f); + pos += 1; + + if pos % CHUNK == 0 { + let (_, sponge_state) = memory.read::<{CHUNK * 2}>(register_address_space, sponge_ptr); + let output = self.subchip.permute(sponge_state); + memory.write::<{CHUNK * 2}>(data_address_space, sponge_ptr, std::array::from_fn(|i| output[i])); + } + } + + let mod_pos = pos % CHUNK; + memory.write_cell(register_address_space, input_register_1, F::from_canonical_usize(mod_pos)); } else { unreachable!() } @@ -501,6 +538,8 @@ impl InstructionExecutor String::from("PERM_POS2") } else if opcode == COMP_POS2.global_opcode().as_usize() { String::from("COMP_POS2") + } else if opcode == MULTI_OBSERVE.global_opcode().as_usize() { + String::from("MULTI_OBSERVE") } else { unreachable!("unsupported opcode: {}", opcode) } diff --git a/extensions/native/circuit/src/poseidon2/tests.rs b/extensions/native/circuit/src/poseidon2/tests.rs index 32a0e483a3..6d703c549b 100644 --- a/extensions/native/circuit/src/poseidon2/tests.rs +++ b/extensions/native/circuit/src/poseidon2/tests.rs @@ -434,7 +434,8 @@ fn tester_with_random_poseidon2_ops(num_ops: usize) -> VmChipTester { tester.write(e, lhs, data); - } + }, + MULTI_OBSERVE => {} } tester.execute(&mut chip, &instruction); @@ -449,6 +450,7 @@ fn tester_with_random_poseidon2_ops(num_ops: usize) -> VmChipTester(e, dst); assert_eq!(hash, actual); } + MULTI_OBSERVE => {} } } tester.build().load(chip).finalize() diff --git a/extensions/native/compiler/src/asm/compiler.rs b/extensions/native/compiler/src/asm/compiler.rs index e75e6b1f9f..1ae79bcb58 100644 --- a/extensions/native/compiler/src/asm/compiler.rs +++ b/extensions/native/compiler/src/asm/compiler.rs @@ -490,13 +490,10 @@ impl + TwoAdicField> AsmCo self.push(AsmInstruction::HintBits(var.fp(), len), debug_info); } DslIr::Poseidon2MultiObserve(dst, init_pos, arr_ptr, len) => { - match dst { - Array::Dyn(dst, _) => self.push( - AsmInstruction::Poseidon2MultiObserve(dst.fp(), init_pos.fp(), arr_ptr.fp(), len.get_var().fp()), - debug_info, - ), - _ => unimplemented!(), - } + self.push( + AsmInstruction::Poseidon2MultiObserve(dst.fp(), init_pos.fp(), arr_ptr.fp(), len.get_var().fp()), + debug_info, + ); }, DslIr::Poseidon2PermuteBabyBear(dst, src) => match (dst, src) { (Array::Dyn(dst, _), Array::Dyn(src, _)) => self.push( diff --git a/extensions/native/compiler/src/conversion/mod.rs b/extensions/native/compiler/src/conversion/mod.rs index dc73d6fbab..aab0274550 100644 --- a/extensions/native/compiler/src/conversion/mod.rs +++ b/extensions/native/compiler/src/conversion/mod.rs @@ -441,15 +441,18 @@ fn convert_instruction>( AS::Native, AS::Native, )], - AsmInstruction::Poseidon2MultiObserve(dst, init, arr, len) => vec![], - // vec![inst( - // options.opcode_with_offset(Poseidon2Opcode::PERM_POS2), - // i32_f(dst), - // i32_f(src), - // F::ZERO, - // AS::Native, - // AS::Native, - // )], + AsmInstruction::Poseidon2MultiObserve(dst, init, arr, len) => vec![ + Instruction { + opcode: options.opcode_with_offset(Poseidon2Opcode::MULTI_OBSERVE), + a: i32_f(dst), + b: i32_f(init), + c: i32_f(arr), + d: i32_f(len), + e: AS::Native.to_field(), + f: AS::Native.to_field(), + g: F::ZERO, + } + ], AsmInstruction::Poseidon2Compress(dst, src1, src2) => vec![inst( options.opcode_with_offset(Poseidon2Opcode::COMP_POS2), i32_f(dst), diff --git a/extensions/native/compiler/src/ir/instructions.rs b/extensions/native/compiler/src/ir/instructions.rs index 0e7f1aad55..8f5025ee2f 100644 --- a/extensions/native/compiler/src/ir/instructions.rs +++ b/extensions/native/compiler/src/ir/instructions.rs @@ -210,7 +210,7 @@ pub enum DslIr { CircuitPoseidon2Permute([Var; 3]), /// Absorbs an array of baby bear elements into a duplex transcript with Poseidon2 permutations (output = p2_multi_observe(array, els)). Poseidon2MultiObserve( - Array>, // sponge_state (array) + Ptr, // sponge_state Var, // initial input_ptr position Ptr, // input array (els) Usize, // len of els diff --git a/extensions/native/compiler/src/ir/poseidon.rs b/extensions/native/compiler/src/ir/poseidon.rs index 395d735b59..7bd35dc4a9 100644 --- a/extensions/native/compiler/src/ir/poseidon.rs +++ b/extensions/native/compiler/src/ir/poseidon.rs @@ -16,28 +16,38 @@ impl Builder { /// /// [Reference](https://docs.rs/p3-poseidon2/latest/p3_poseidon2/struct.Poseidon2.html) pub fn poseidon2_multi_observe( - &mut self, + &mut self, sponge_state: &Array>, input_ptr: Ptr, io_full_ptr: Ptr, arr: &Array>, ) -> Usize { + let buffer_size: Var = Var::uninit(self); + self.assign(&buffer_size, C::N::from_canonical_usize(HASH_RATE)); + match sponge_state { - Array::Fixed(values) => { + Array::Fixed(_) => { panic!("Poseidon2 permutation is not allowed on fixed arrays"); } - Array::Dyn(ptr, len) => { - let init_pos: Var = Var::uninit(self); - self.assign(&init_pos, io_full_ptr.address - input_ptr.address); - - self.operations.push(DslIr::Poseidon2MultiObserve( - sponge_state.clone(), - init_pos, - *ptr, - len.clone(), - )); - - Usize::Var(init_pos) + Array::Dyn(sponge_ptr, _) => { + match arr { + Array::Fixed(_) => { + panic!("Base elements input must be dynamic"); + } + Array::Dyn(ptr, len) => { + let init_pos: Var = Var::uninit(self); + self.assign(&init_pos, buffer_size - (io_full_ptr.address - input_ptr.address)); + + self.operations.push(DslIr::Poseidon2MultiObserve( + *sponge_ptr, + init_pos, + *ptr, + len.clone(), + )); + + Usize::Var(init_pos) + } + } } } } diff --git a/extensions/native/compiler/src/lib.rs b/extensions/native/compiler/src/lib.rs index ef28b37139..66c786fbd9 100644 --- a/extensions/native/compiler/src/lib.rs +++ b/extensions/native/compiler/src/lib.rs @@ -184,6 +184,7 @@ pub enum NativePhantom { pub enum Poseidon2Opcode { PERM_POS2, COMP_POS2, + MULTI_OBSERVE, } /// Opcodes for FRI opening proofs. From 5b12fe866c5aa2ebbaa2dcb52a230ad3de0ff160 Mon Sep 17 00:00:00 2001 From: Rohit Narurkar Date: Thu, 5 Jun 2025 16:10:06 +0100 Subject: [PATCH 03/32] feat: rewrite sample_ext using new IR instruction --- extensions/native/compiler/src/asm/compiler.rs | 9 +++++++++ extensions/native/compiler/src/ir/builder.rs | 4 ++++ extensions/native/compiler/src/ir/instructions.rs | 3 +++ extensions/native/compiler/tests/ext.rs | 7 ++++--- extensions/native/recursion/src/challenger/duplex.rs | 4 +++- 5 files changed, 23 insertions(+), 4 deletions(-) diff --git a/extensions/native/compiler/src/asm/compiler.rs b/extensions/native/compiler/src/asm/compiler.rs index 1ae79bcb58..0e0db9cff9 100644 --- a/extensions/native/compiler/src/asm/compiler.rs +++ b/extensions/native/compiler/src/asm/compiler.rs @@ -623,6 +623,15 @@ impl + TwoAdicField> AsmCo debug_info, ); } + DslIr::ExtFromBaseVec(ext, base_vec) => { + assert_eq!(base_vec.len(), EF::D); + for (i, base) in base_vec.into_iter().enumerate() { + self.push( + AsmInstruction::CopyF(ext.fp() + (i as i32), base.fp()), + debug_info.clone(), + ); + } + } _ => unimplemented!(), } } diff --git a/extensions/native/compiler/src/ir/builder.rs b/extensions/native/compiler/src/ir/builder.rs index 966c0db21c..64c62e64fa 100644 --- a/extensions/native/compiler/src/ir/builder.rs +++ b/extensions/native/compiler/src/ir/builder.rs @@ -620,6 +620,10 @@ impl Builder { self.witness_space.get(id.value()).unwrap() } + pub fn ext_from_base_vec(&mut self, ext: Ext, base_vec: Vec>) { + self.push(DslIr::ExtFromBaseVec(ext, base_vec)); + } + /// Throws an error. pub fn error(&mut self) { self.operations.trace_push(DslIr::Error()); diff --git a/extensions/native/compiler/src/ir/instructions.rs b/extensions/native/compiler/src/ir/instructions.rs index 8f5025ee2f..c15b49d95d 100644 --- a/extensions/native/compiler/src/ir/instructions.rs +++ b/extensions/native/compiler/src/ir/instructions.rs @@ -248,6 +248,9 @@ pub enum DslIr { /// Operation to halt the program. Should be the last instruction in the program. Halt, + /// Samples an ext from a vector of felts. + ExtFromBaseVec(Ext, Vec>), + // Public inputs for circuits. /// Publish a field element as the ith public value. Should only be used when target is a /// circuit. diff --git a/extensions/native/compiler/tests/ext.rs b/extensions/native/compiler/tests/ext.rs index 5da70cb53b..70584fd926 100644 --- a/extensions/native/compiler/tests/ext.rs +++ b/extensions/native/compiler/tests/ext.rs @@ -35,7 +35,7 @@ fn test_ext2felt() { } #[test] -fn test_ext_from_base_slice() { +fn test_ext_from_base_vec() { const D: usize = 4; type F = BabyBear; type EF = BinomialExtensionField; @@ -52,8 +52,9 @@ fn test_ext_from_base_slice() { let val = EF::from_base_slice(base_slice); let expected: Ext<_, _> = builder.constant(val); - let felts = base_slice.map(|e| builder.constant::>(e)); - let actual = builder.ext_from_base_slice(&felts); + let felts = base_slice.map(|e| builder.constant::>(e)).to_vec(); + let actual = builder.uninit(); + builder.ext_from_base_vec(actual, felts); builder.assert_ext_eq(actual, expected); builder.halt(); diff --git a/extensions/native/recursion/src/challenger/duplex.rs b/extensions/native/recursion/src/challenger/duplex.rs index 7c0cd4dd88..2d45d896be 100644 --- a/extensions/native/recursion/src/challenger/duplex.rs +++ b/extensions/native/recursion/src/challenger/duplex.rs @@ -101,7 +101,9 @@ impl DuplexChallengerVariable { let b = self.sample(builder); let c = self.sample(builder); let d = self.sample(builder); - builder.ext_from_base_slice(&[a, b, c, d]) + let ext = builder.uninit(); + builder.ext_from_base_vec(ext, vec![a, b, c, d]); + ext } fn sample_bits(&self, builder: &mut Builder, nb_bits: RVar) -> Array> From e074e270a4b7493f5f837b3f175a3e6c9a807cc8 Mon Sep 17 00:00:00 2001 From: Rohit Narurkar Date: Tue, 10 Jun 2025 09:55:07 +0100 Subject: [PATCH 04/32] chore(doc): update comment --- extensions/native/compiler/src/ir/instructions.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/extensions/native/compiler/src/ir/instructions.rs b/extensions/native/compiler/src/ir/instructions.rs index c15b49d95d..6cd6e4a77a 100644 --- a/extensions/native/compiler/src/ir/instructions.rs +++ b/extensions/native/compiler/src/ir/instructions.rs @@ -248,7 +248,7 @@ pub enum DslIr { /// Operation to halt the program. Should be the last instruction in the program. Halt, - /// Samples an ext from a vector of felts. + /// Packs a vector of felts into an ext. ExtFromBaseVec(Ext, Vec>), // Public inputs for circuits. From 9860915c8cffab347e5bae2e0f8041fe269cefd4 Mon Sep 17 00:00:00 2001 From: Rohit Narurkar Date: Wed, 11 Jun 2025 13:50:47 +0100 Subject: [PATCH 05/32] feat(openvm_circuit): store span info in cycle tracker for convenient debug info --- crates/vm/src/arch/segment.rs | 14 ++++--- crates/vm/src/metrics/cycle_tracker/mod.rs | 42 +++++++++++++++---- .../src/constraints/halo2/compiler.rs | 4 +- 3 files changed, 43 insertions(+), 17 deletions(-) diff --git a/crates/vm/src/arch/segment.rs b/crates/vm/src/arch/segment.rs index 634632ce2b..642b50e756 100644 --- a/crates/vm/src/arch/segment.rs +++ b/crates/vm/src/arch/segment.rs @@ -282,16 +282,18 @@ impl> ExecutionSegment { Some(SysPhantom::CtStart) => { #[cfg(feature = "bench-metrics")] - metrics - .cycle_tracker - .start(dsl_instr.cloned().unwrap_or("Default".to_string())) + metrics.cycle_tracker.start( + dsl_instr.cloned().unwrap_or("Default".to_string()), + metrics.cycle_count, + ) } Some(SysPhantom::CtEnd) => { #[cfg(feature = "bench-metrics")] - metrics - .cycle_tracker - .end(dsl_instr.cloned().unwrap_or("Default".to_string())) + metrics.cycle_tracker.end( + dsl_instr.cloned().unwrap_or("Default".to_string()), + metrics.cycle_count, + ) } _ => {} } diff --git a/crates/vm/src/metrics/cycle_tracker/mod.rs b/crates/vm/src/metrics/cycle_tracker/mod.rs index b1ef065451..27a457c7c4 100644 --- a/crates/vm/src/metrics/cycle_tracker/mod.rs +++ b/crates/vm/src/metrics/cycle_tracker/mod.rs @@ -1,7 +1,18 @@ +/// Stats for a nested span in the execution segment that is tracked by the [`CycleTracker`]. +#[derive(Clone, Debug, Default)] +pub struct SpanInfo { + /// The name of the span. + tag: String, + /// The cycle count at which the span starts. + start: usize, +} + #[derive(Clone, Debug, Default)] pub struct CycleTracker { /// Stack of span names, with most recent at the end - stack: Vec, + stack: Vec, + /// Depth of the stack. + depth: usize, } impl CycleTracker { @@ -14,25 +25,34 @@ impl CycleTracker { } /// Starts a new cycle tracker span for the given name. - /// If a span already exists for the given name, it ends the existing span and pushes a new one - /// to the vec. - pub fn start(&mut self, mut name: String) { + /// If a span already exists for the given name, it ends the existing span and pushes a new one to the vec. + pub fn start(&mut self, mut name: String, cycles_count: usize) { // hack to remove "CT-" prefix if name.starts_with("CT-") { name = name.split_off(3); } - self.stack.push(name); + self.stack.push(SpanInfo { + tag: name.clone(), + start: cycles_count, + }); + let padding = "│ ".repeat(self.depth); + tracing::info!("{}┌╴{}", padding, name); + self.depth += 1; } /// Ends the cycle tracker span for the given name. /// If no span exists for the given name, it panics. - pub fn end(&mut self, mut name: String) { + pub fn end(&mut self, mut name: String, cycles_count: usize) { // hack to remove "CT-" prefix if name.starts_with("CT-") { name = name.split_off(3); } - let stack_top = self.stack.pop(); - assert_eq!(stack_top.unwrap(), name, "Stack top does not match name"); + let SpanInfo { tag, start } = self.stack.pop().unwrap(); + assert_eq!(tag, name, "Stack top does not match name"); + self.depth -= 1; + let padding = "│ ".repeat(self.depth); + let span_cycles = cycles_count - start; + tracing::info!("{}└╴{} cycles", padding, span_cycles); } /// Ends the current cycle tracker span. @@ -42,7 +62,11 @@ impl CycleTracker { /// Get full name of span with all parent names separated by ";" in flamegraph format pub fn get_full_name(&self) -> String { - self.stack.join(";") + self.stack + .iter() + .map(|span_info| span_info.tag.clone()) + .collect::>() + .join(";") } } diff --git a/extensions/native/compiler/src/constraints/halo2/compiler.rs b/extensions/native/compiler/src/constraints/halo2/compiler.rs index ce108addaa..6b831e596b 100644 --- a/extensions/native/compiler/src/constraints/halo2/compiler.rs +++ b/extensions/native/compiler/src/constraints/halo2/compiler.rs @@ -493,11 +493,11 @@ impl Halo2ConstraintCompiler { } DslIr::CycleTrackerStart(_name) => { #[cfg(feature = "bench-metrics")] - cell_tracker.start(_name); + cell_tracker.start(_name, 0); } DslIr::CycleTrackerEnd(_name) => { #[cfg(feature = "bench-metrics")] - cell_tracker.end(_name); + cell_tracker.end(_name, 0); } DslIr::CircuitPublish(val, index) => { public_values[index] = vars[&val.0]; From 0107c85965523d2bd7b2ca25456e95b89cbfcce6 Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Wed, 11 Jun 2025 17:12:41 -0400 Subject: [PATCH 06/32] Fix annotation, address spaces and register assignments --- extensions/native/circuit/src/poseidon2/chip.rs | 14 +++++++------- extensions/native/compiler/src/conversion/mod.rs | 4 ++-- extensions/native/compiler/src/ir/instructions.rs | 2 +- extensions/native/compiler/src/ir/poseidon.rs | 5 ++--- 4 files changed, 12 insertions(+), 13 deletions(-) diff --git a/extensions/native/circuit/src/poseidon2/chip.rs b/extensions/native/circuit/src/poseidon2/chip.rs index d2bb11b2b4..f26db6ffe7 100644 --- a/extensions/native/circuit/src/poseidon2/chip.rs +++ b/extensions/native/circuit/src/poseidon2/chip.rs @@ -490,14 +490,14 @@ impl InstructionExecutor a: output_register, b: input_register_1, c: input_register_2, - d: input_register_3, + d: data_address_space, e: register_address_space, - f: data_address_space, + f: input_register_3, .. } = instruction; - let (_, sponge_ptr) = memory.read_cell(data_address_space, output_register); - let (_, arr_ptr) = memory.read_cell(data_address_space, input_register_2); + let (_, sponge_ptr) = memory.read_cell(register_address_space, output_register); + let (_, arr_ptr) = memory.read_cell(register_address_space, input_register_2); let init_pos_read = memory.read_cell(register_address_space, input_register_1); let mut pos = init_pos_read.1.as_canonical_u32() as usize; @@ -507,14 +507,14 @@ impl InstructionExecutor for i in 0..len { let mod_pos = pos % CHUNK; - let n_read = memory.read_cell(register_address_space, arr_ptr + F::from_canonical_usize(i)); + let n_read = memory.read_cell(data_address_space, arr_ptr + F::from_canonical_usize(i)); let n_f = n_read.1; - memory.write_cell(register_address_space, sponge_ptr + F::from_canonical_usize(mod_pos), n_f); + memory.write_cell(data_address_space, sponge_ptr + F::from_canonical_usize(mod_pos), n_f); pos += 1; if pos % CHUNK == 0 { - let (_, sponge_state) = memory.read::<{CHUNK * 2}>(register_address_space, sponge_ptr); + let (_, sponge_state) = memory.read::<{CHUNK * 2}>(data_address_space, sponge_ptr); let output = self.subchip.permute(sponge_state); memory.write::<{CHUNK * 2}>(data_address_space, sponge_ptr, std::array::from_fn(|i| output[i])); } diff --git a/extensions/native/compiler/src/conversion/mod.rs b/extensions/native/compiler/src/conversion/mod.rs index aab0274550..f8da82c30b 100644 --- a/extensions/native/compiler/src/conversion/mod.rs +++ b/extensions/native/compiler/src/conversion/mod.rs @@ -447,9 +447,9 @@ fn convert_instruction>( a: i32_f(dst), b: i32_f(init), c: i32_f(arr), - d: i32_f(len), + d: AS::Native.to_field(), e: AS::Native.to_field(), - f: AS::Native.to_field(), + f: i32_f(len), g: F::ZERO, } ], diff --git a/extensions/native/compiler/src/ir/instructions.rs b/extensions/native/compiler/src/ir/instructions.rs index 6cd6e4a77a..24654cb70f 100644 --- a/extensions/native/compiler/src/ir/instructions.rs +++ b/extensions/native/compiler/src/ir/instructions.rs @@ -212,7 +212,7 @@ pub enum DslIr { Poseidon2MultiObserve( Ptr, // sponge_state Var, // initial input_ptr position - Ptr, // input array (els) + Ptr, // input array (base elements) Usize, // len of els ), diff --git a/extensions/native/compiler/src/ir/poseidon.rs b/extensions/native/compiler/src/ir/poseidon.rs index 7bd35dc4a9..ee9bc0d87d 100644 --- a/extensions/native/compiler/src/ir/poseidon.rs +++ b/extensions/native/compiler/src/ir/poseidon.rs @@ -12,14 +12,13 @@ pub const PERMUTATION_WIDTH: usize = 16; impl Builder { /// Extends native VM ability to observe multiple base elements in one opcode operation /// Absorbs elements sequentially at the RATE portion of sponge state and performs as many permutations as necessary. - /// Returns the index position of the input_ptr and the final sponge state. + /// Returns the index position of the next input_ptr. /// /// [Reference](https://docs.rs/p3-poseidon2/latest/p3_poseidon2/struct.Poseidon2.html) pub fn poseidon2_multi_observe( &mut self, sponge_state: &Array>, input_ptr: Ptr, - io_full_ptr: Ptr, arr: &Array>, ) -> Usize { let buffer_size: Var = Var::uninit(self); @@ -36,7 +35,7 @@ impl Builder { } Array::Dyn(ptr, len) => { let init_pos: Var = Var::uninit(self); - self.assign(&init_pos, buffer_size - (io_full_ptr.address - input_ptr.address)); + self.assign(&init_pos, input_ptr.address - sponge_ptr.address); self.operations.push(DslIr::Poseidon2MultiObserve( *sponge_ptr, From b0c782a83b6064d0e90f75a3a02e7e43ef122aa7 Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Tue, 15 Jul 2025 20:25:27 -0400 Subject: [PATCH 07/32] Consolidate MultiObserve chip debugging --- crates/vm/src/system/memory/controller/mod.rs | 2 +- extensions/native/circuit/src/extension.rs | 16 +- extensions/native/circuit/src/lib.rs | 2 + .../native/circuit/src/multi_observe/mod.rs | 620 ++++++++++++++++++ .../native/circuit/src/poseidon2/air.rs | 2 +- .../native/circuit/src/poseidon2/trace.rs | 2 +- vm_run_output.log | 0 7 files changed, 638 insertions(+), 6 deletions(-) create mode 100644 extensions/native/circuit/src/multi_observe/mod.rs create mode 100644 vm_run_output.log diff --git a/crates/vm/src/system/memory/controller/mod.rs b/crates/vm/src/system/memory/controller/mod.rs index 680a03ab8e..32a81ffd2b 100644 --- a/crates/vm/src/system/memory/controller/mod.rs +++ b/crates/vm/src/system/memory/controller/mod.rs @@ -59,7 +59,7 @@ pub const MERKLE_AIR_OFFSET: usize = 1; pub const BOUNDARY_AIR_OFFSET: usize = 0; #[repr(C)] -#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)] +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize, Default)] pub struct RecordId(pub usize); pub type MemoryImage = AddressMap; diff --git a/extensions/native/circuit/src/extension.rs b/extensions/native/circuit/src/extension.rs index c7dba9f87c..68666ac872 100644 --- a/extensions/native/circuit/src/extension.rs +++ b/extensions/native/circuit/src/extension.rs @@ -1,4 +1,4 @@ -use air::VerifyBatchBus; +use poseidon2::air::VerifyBatchBus; use alu_native_adapter::AluNativeAdapterChip; use branch_native_adapter::BranchNativeAdapterChip; use derive_more::derive::From; @@ -30,7 +30,8 @@ use strum::IntoEnumIterator; use crate::{ adapters::{convert_adapter::ConvertAdapterChip, *}, - chip::NativePoseidon2Chip, + poseidon2::chip::NativePoseidon2Chip, + multi_observe::NativeMultiObserveChip, phantom::*, *, }; @@ -76,6 +77,7 @@ pub enum NativeExecutor { FieldExtension(FieldExtensionChip), FriReducedOpening(FriReducedOpeningChip), VerifyBatch(NativePoseidon2Chip), + MultiObserve(NativeMultiObserveChip), } #[derive(From, ChipUsageGetter, Chip, AnyEnum)] @@ -203,10 +205,18 @@ impl VmExtension for Native { VerifyBatchOpcode::VERIFY_BATCH.global_opcode(), Poseidon2Opcode::PERM_POS2.global_opcode(), Poseidon2Opcode::COMP_POS2.global_opcode(), - Poseidon2Opcode::MULTI_OBSERVE.global_opcode(), ], )?; + let multi_observe_chip = NativeMultiObserveChip::new( + builder.system_port(), + offline_memory.clone(), + Poseidon2Config::default(), + ); + inventory.add_executor(multi_observe_chip, [ + Poseidon2Opcode::MULTI_OBSERVE.global_opcode(), + ])?; + builder.add_phantom_sub_executor( NativeHintInputSubEx, PhantomDiscriminant(NativePhantom::HintInput as u16), diff --git a/extensions/native/circuit/src/lib.rs b/extensions/native/circuit/src/lib.rs index 46c6bc890f..883c4d0834 100644 --- a/extensions/native/circuit/src/lib.rs +++ b/extensions/native/circuit/src/lib.rs @@ -8,6 +8,7 @@ mod fri; mod jal; mod loadstore; mod poseidon2; +mod multi_observe; pub use branch_eq::*; pub use castf::*; @@ -17,6 +18,7 @@ pub use fri::*; pub use jal::*; pub use loadstore::*; pub use poseidon2::*; +pub use multi_observe::*; mod extension; pub use extension::*; diff --git a/extensions/native/circuit/src/multi_observe/mod.rs b/extensions/native/circuit/src/multi_observe/mod.rs new file mode 100644 index 0000000000..e9bfe34f56 --- /dev/null +++ b/extensions/native/circuit/src/multi_observe/mod.rs @@ -0,0 +1,620 @@ +use std::{borrow::{Borrow, BorrowMut}, sync::{Arc, Mutex}}; +use openvm_circuit::system::memory::offline_checker::{MemoryReadAuxCols, MemoryWriteAuxCols}; +use openvm_circuit_primitives_derive::AlignedBorrow; +use openvm_poseidon2_air::Poseidon2SubChip; +use openvm_circuit::{ + arch::{ExecutionBridge, ExecutionState, ExecutionError, InstructionExecutor, SystemPort}, + system::memory::{offline_checker::MemoryBridge, MemoryAddress, MemoryController, OfflineMemory, RecordId}, +}; +use openvm_circuit_primitives::utils::not; +use openvm_instructions::{instruction::Instruction, program::DEFAULT_PC_STEP, LocalOpcode}; +use openvm_native_compiler::{ + conversion::AS, + Poseidon2Opcode::MULTI_OBSERVE +}; +use openvm_poseidon2_air::Poseidon2Config; +use openvm_stark_backend::{ + interaction::InteractionBuilder, + p3_air::{Air, AirBuilder, BaseAir}, + p3_field::{Field, FieldAlgebra, PrimeField32}, + p3_matrix::Matrix, + rap::{BaseAirWithPublicValues, PartitionedBaseAir} +}; +use serde::{Deserialize, Serialize}; +use openvm_circuit::system::memory::{MemoryAuxColsFactory}; +use openvm_circuit_primitives::utils::next_power_of_two_or_zero; +use openvm_stark_backend::{ + config::{StarkGenericConfig, Val}, + p3_matrix::dense::RowMajorMatrix, + prover::types::AirProofInput, + AirRef, Chip, ChipUsageGetter, +}; +const CHUNK: usize = 8; + +#[repr(C)] +#[derive(AlignedBorrow)] +pub struct NativeMultiObserveCols { + pub enable: T, + pub is_first: T, + pub is_final: T, + + pub pc: T, + pub state_idx: T, + pub remaining_len: T, + pub counter: T, + pub should_permute: T, + + /// The initial timestamp of the instruction, which must be identical for first row + /// and all following intermediate observation rows. + pub first_timestamp: T, + pub curr_timestamp: T, + + pub read_state_ptr: MemoryReadAuxCols, + pub read_input_ptr: MemoryReadAuxCols, + pub state_ptr: T, + pub input_ptr: T, + + pub read_init_pos: MemoryReadAuxCols, + pub read_len: MemoryReadAuxCols, + pub init_pos: T, + pub len: T, + + pub read_data: MemoryReadAuxCols, + pub write_data: MemoryWriteAuxCols, + pub data: T, + + pub read_sponge_state: MemoryReadAuxCols, + pub write_sponge_state: MemoryWriteAuxCols, + pub permutation_input: [T; 2 * CHUNK], + pub permutation_output: [T; 2 * CHUNK], + + pub write_final_idx: MemoryWriteAuxCols, + pub final_idx: T, + + pub input_register_1: T, + pub input_register_2: T, + pub input_register_3: T, + pub output_register: T, +} + +#[derive(Clone, Debug)] +pub struct NativeMultiObserveAir { + pub execution_bridge: ExecutionBridge, + pub memory_bridge: MemoryBridge, + pub(crate) address_space: F, +} +impl BaseAir for NativeMultiObserveAir { + fn width(&self) -> usize { + NativeMultiObserveCols::::width() + } +} +impl BaseAirWithPublicValues for NativeMultiObserveAir {} +impl PartitionedBaseAir for NativeMultiObserveAir {} + +impl Air for NativeMultiObserveAir { + fn eval(&self, builder: &mut AB) { + let main = builder.main(); + let local = main.row_slice(0); + let local: &NativeMultiObserveCols = (*local).borrow(); + let next = main.row_slice(1); + let next: &NativeMultiObserveCols = (*next).borrow(); + + let &NativeMultiObserveCols { + enable, + is_first, + is_final, + + // TODO: Should pass to execution bridge for Poseidon2 permutation + // Example: + // self.execution_bridge + // .execute_and_increment_pc( + // is_permute.clone() + // * AB::F::from_canonical_usize(PERM_POS2.global_opcode().as_usize()) + // + is_compress + // * AB::F::from_canonical_usize(COMP_POS2.global_opcode().as_usize()), + // [ + // output_register.into(), + // input_register_1.into(), + // input_register_2.into(), + // self.address_space.into(), + // self.address_space.into(), + // ], + // ExecutionState::new(pc, start_timestamp), + // AB::Expr::from_canonical_u32(NUM_SIMPLE_ACCESSES), + // ) + // .eval(builder, simple); + pc: _, + + state_idx, + remaining_len, + counter, + should_permute, + first_timestamp, + curr_timestamp, + read_state_ptr, + read_input_ptr, + state_ptr, + input_ptr, + read_init_pos, + read_len, + init_pos, + len, + read_data, + write_data, + data, + read_sponge_state, + write_sponge_state, + permutation_input, + permutation_output, + write_final_idx, + final_idx, + input_register_1, + input_register_2, + input_register_3, + output_register, + } = local; + + builder.assert_bool(enable); + builder.assert_bool(is_first); + builder.assert_bool(is_final); + builder.assert_bool(should_permute); + + // Row transitions + + // Each row must operate one element + builder + .when(next.enable) + .when(not(next.is_first)) + .assert_eq(next.counter, counter + AB::F::ONE); + builder + .when(next.enable) + .when(not(next.is_first)) + .assert_eq(next.remaining_len, remaining_len - AB::F::ONE); + + // After each permutation, the sponge state index must revert to 0 + builder + .when(should_permute) + .when(not(next.is_first)) + .assert_eq(next.state_idx, AB::F::ZERO); + + // Boundary conditions + // At the first row, counter must be 0, remaining_len must be len + builder + .when(is_first) + .assert_eq(counter, AB::F::ZERO); + builder + .when(is_first) + .assert_eq(remaining_len, len); + + // At the last row, counter must be len - 1, remaining_len must be 1 + builder + .when(is_final) + .assert_eq(counter, len - AB::F::ONE); + builder + .when(is_final) + .assert_eq(remaining_len, AB::F::ONE); + + // Fields that remain constant for a single MULTI_OBSERVE call + builder + .when(next.enable) + .when(not(next.is_first)) + .assert_eq(state_ptr, next.state_ptr); + builder + .when(next.enable) + .when(not(next.is_first)) + .assert_eq(input_ptr, next.input_ptr); + builder + .when(next.enable) + .when(not(next.is_first)) + .assert_eq(init_pos, next.init_pos); + builder + .when(next.enable) + .when(not(next.is_first)) + .assert_eq(len, next.len); + builder + .when(next.enable) + .when(not(next.is_first)) + .assert_eq(input_register_1, next.input_register_1); + builder + .when(next.enable) + .when(not(next.is_first)) + .assert_eq(input_register_2, next.input_register_2); + builder + .when(next.enable) + .when(not(next.is_first)) + .assert_eq(input_register_3, next.input_register_3); + builder + .when(next.enable) + .when(not(next.is_first)) + .assert_eq(output_register, next.output_register); + + // Memory operations + self.memory_bridge + .read( + MemoryAddress::new(self.address_space, output_register), + [state_ptr], + first_timestamp, + &read_state_ptr, + ) + .eval(builder, is_first); + + self.memory_bridge + .read( + MemoryAddress::new(self.address_space, input_register_2), + [input_ptr], + first_timestamp + AB::F::ONE, + &read_input_ptr, + ) + .eval(builder, is_first); + + self.memory_bridge + .read( + MemoryAddress::new(self.address_space, input_register_1), + [init_pos], + first_timestamp + AB::F::TWO, + &read_init_pos, + ) + .eval(builder, is_first); + + self.memory_bridge + .read( + MemoryAddress::new(self.address_space, input_register_3), + [len], + first_timestamp + AB::F::from_canonical_usize(3), + &read_len, + ) + .eval(builder, is_first); + + self.memory_bridge + .read( + MemoryAddress::new(self.address_space, input_ptr + counter), + [data], + first_timestamp + curr_timestamp + is_first * AB::F::from_canonical_usize(4), + &read_data + ) + .eval(builder, is_first); + + self.memory_bridge + .write( + MemoryAddress::new( + self.address_space, + state_ptr + state_idx, + ), + [data], + first_timestamp + curr_timestamp + is_first * AB::F::from_canonical_usize(4) + AB::F::ONE, + &write_data, + ) + .eval(builder, enable); + + self.memory_bridge + .read( + MemoryAddress::new( + self.address_space, + state_ptr, + ), + permutation_input, + first_timestamp + curr_timestamp + is_first * AB::F::from_canonical_usize(4) + AB::F::TWO, + &read_sponge_state, + ) + .eval(builder, should_permute); + + self.memory_bridge + .write( + MemoryAddress::new( + self.address_space, + state_ptr + ), + permutation_output, + first_timestamp + curr_timestamp + is_first * AB::F::from_canonical_usize(4) + AB::F::from_canonical_usize(3), + &write_sponge_state, + ) + .eval(builder, should_permute); + + self.memory_bridge + .write( + MemoryAddress::new( + self.address_space, + input_register_1, + ), + [final_idx], + first_timestamp + curr_timestamp + is_first * AB::F::from_canonical_usize(4) + should_permute * AB::F::TWO + AB::F::TWO, + &write_final_idx + ) + .eval(builder, is_final); + } +} + +#[repr(C)] +#[derive(Debug, Clone, Serialize, Deserialize, Default)] +#[serde(bound = "F: Field")] +pub struct TranscriptObservationRecord { + pub from_state: ExecutionState, + pub instruction: Instruction, + pub curr_timestamp: usize, + + pub state_idx: usize, + + pub is_first: bool, + pub is_final: bool, + pub remaining_len: usize, + pub counter: usize, + pub should_permute: bool, + + pub read_state_ptr: RecordId, + pub read_input_ptr: RecordId, + pub state_ptr: F, + pub input_ptr: F, + + pub read_init_pos: RecordId, + pub init_pos: F, + pub read_len: RecordId, + pub len: usize, + + pub read_input_data: RecordId, + pub write_input_data: RecordId, + pub input_data: F, + + pub read_sponge_state: RecordId, + pub write_sponge_state: RecordId, + pub permutation_input: [F; 2 * CHUNK], + pub permutation_output: [F; 2 * CHUNK], + + pub write_final_idx: RecordId, + pub final_idx: F, + + pub input_register_1: F, + pub input_register_2: F, + pub input_register_3: F, + pub output_register: F, +} + +#[derive(Debug, Clone, Serialize, Deserialize, Default)] +#[serde(bound = "F: Field")] +pub struct NativeMultiObserveRecordSet { + pub transcript_observation_records: Vec>, +} + +pub struct NativeMultiObserveChip { + pub(super) air: NativeMultiObserveAir, + pub record_set: NativeMultiObserveRecordSet, + pub height: usize, + pub(super) offline_memory: Arc>>, + pub(super) subchip: Poseidon2SubChip, +} + +impl NativeMultiObserveChip { + pub fn new( + port: SystemPort, + offline_memory: Arc>>, + poseidon2_config: Poseidon2Config, + ) -> Self { + let air = NativeMultiObserveAir { + execution_bridge: ExecutionBridge::new(port.execution_bus, port.program_bus), + memory_bridge: port.memory_bridge, + address_space: F::from_canonical_u32(AS::Native as u32), + }; + Self { + record_set: Default::default(), + air, + height: 0, + offline_memory, + subchip: Poseidon2SubChip::new(poseidon2_config.constants), + } + } + + fn record_to_row( + &self, + record: &TranscriptObservationRecord, + aux_cols_factory: &MemoryAuxColsFactory, + slice: &mut [F], + memory: &OfflineMemory, + ) { + let cols: &mut NativeMultiObserveCols = slice.borrow_mut(); + + cols.enable = F::ONE; + cols.is_first = if record.is_first { F::ONE } else { F::ZERO }; + cols.is_final = if record.is_final { F::ONE } else { F::ZERO }; + cols.should_permute = if record.should_permute { F::ONE } else { F::ZERO }; + + let read_state_ptr_record = memory.record_by_id(record.read_state_ptr); + let read_input_ptr_record = memory.record_by_id(record.read_input_ptr); + let read_init_pos_record = memory.record_by_id(record.read_init_pos); + let read_len_record = memory.record_by_id(record.read_len); + + let read_data_record = memory.record_by_id(record.read_input_data); + let write_data_record = memory.record_by_id(record.write_input_data); + + let read_sponge_record = memory.record_by_id(record.read_sponge_state); + let write_sponge_record = memory.record_by_id(record.write_sponge_state); + + cols.state_ptr = record.state_ptr; + cols.input_ptr = record.input_ptr; + cols.init_pos = record.init_pos; + cols.len = F::from_canonical_usize(record.len); + cols.data = record.input_data; + cols.curr_timestamp = F::from_canonical_usize(record.curr_timestamp); + + cols.permutation_input = record.permutation_input; + cols.permutation_output = record.permutation_output; + + cols.state_idx = cols.state_idx; + cols.remaining_len = cols.remaining_len; + cols.counter = cols.counter; + cols.final_idx = record.final_idx; + + cols.first_timestamp = F::from_canonical_u32(record.from_state.timestamp); + cols.pc = F::from_canonical_u32(record.from_state.pc); + + cols.input_register_1 = record.input_register_1; + cols.input_register_2 = record.input_register_2; + cols.input_register_3 = record.input_register_3; + cols.output_register = record.output_register; + + aux_cols_factory.generate_read_aux(read_state_ptr_record, &mut cols.read_state_ptr); + aux_cols_factory.generate_read_aux(read_input_ptr_record, &mut cols.read_input_ptr); + aux_cols_factory.generate_read_aux(read_init_pos_record, &mut cols.read_init_pos); + aux_cols_factory.generate_read_aux(read_len_record, &mut cols.read_len); + aux_cols_factory.generate_read_aux(read_data_record, &mut cols.read_data); + aux_cols_factory.generate_write_aux(write_data_record, &mut cols.write_data); + + aux_cols_factory.generate_read_aux(read_sponge_record, &mut cols.read_sponge_state); + aux_cols_factory.generate_write_aux(write_sponge_record, &mut cols.write_sponge_state); + + let write_final_idx_record = memory.record_by_id(record.write_final_idx); + aux_cols_factory.generate_write_aux(write_final_idx_record, &mut cols.write_final_idx); + } + + fn generate_trace(self) -> RowMajorMatrix { + let width = self.trace_width(); + let height = next_power_of_two_or_zero(self.height); + let mut flat_trace = F::zero_vec(width * height); + + let memory = self.offline_memory.lock().unwrap(); + let aux_cols_factory = memory.aux_cols_factory(); + let mut used_cells = 0; + for record in self.record_set.transcript_observation_records.iter() { + self.record_to_row( + record, + &aux_cols_factory, + &mut flat_trace[used_cells..], + &memory, + ); + used_cells += width; + } + + RowMajorMatrix::new(flat_trace, width) + } +} + +impl InstructionExecutor for NativeMultiObserveChip { + fn execute( + &mut self, + memory: &mut MemoryController, + instruction: &Instruction, + from_state: ExecutionState, + ) -> Result, ExecutionError> { + let mut observation_records: Vec> = vec![]; + + let &Instruction { + a: output_register, + b: input_register_1, + c: input_register_2, + d: data_address_space, + e: register_address_space, + f: input_register_3, + .. + } = instruction; + + let (read_sponge_ptr, sponge_ptr) = memory.read_cell(register_address_space, output_register); + let (read_arr_ptr, arr_ptr) = memory.read_cell(register_address_space, input_register_2); + let (read_init_pos, pos) = memory.read_cell(register_address_space, input_register_1); + let init_pos = pos.clone(); + let mut pos = pos.as_canonical_u32() as usize; + let (read_len, len) = memory.read_cell(register_address_space, input_register_3); + let len = len.as_canonical_u32() as usize; + + let mut curr_timestamp = 0usize; + + for i in 0..len { + let mut record: TranscriptObservationRecord = TranscriptObservationRecord { + from_state, + curr_timestamp, + instruction: instruction.clone(), + state_idx: pos % CHUNK, + remaining_len: len - i, + counter: i, + read_state_ptr: read_sponge_ptr, + read_input_ptr: read_arr_ptr, + state_ptr: sponge_ptr, + input_ptr: arr_ptr, + read_init_pos: read_init_pos, + init_pos, + read_len, + len, + input_register_1, + input_register_2, + input_register_3, + output_register, + ..Default::default() + }; + + let (n_read, n_f) = memory.read_cell(data_address_space, arr_ptr + F::from_canonical_usize(i)); + record.read_input_data = n_read; + record.input_data = n_f; + curr_timestamp += 1; + + let (n_write, _) = memory.write_cell(data_address_space, sponge_ptr + F::from_canonical_usize(record.state_idx), record.input_data); + record.write_input_data = n_write; + curr_timestamp += 1; + + pos += 1; + + if pos % CHUNK == 0 { + record.should_permute = true; + let (read_sponge_record, permutation_input) = memory.read::<{CHUNK * 2}>(data_address_space, sponge_ptr); + let output = self.subchip.permute(permutation_input); + let (write_sponge_record, _) = memory.write::<{CHUNK * 2}>(data_address_space, sponge_ptr, std::array::from_fn(|i| output[i])); + + curr_timestamp += 2; + + record.read_sponge_state = read_sponge_record; + record.write_sponge_state = write_sponge_record; + record.permutation_input = permutation_input; + record.permutation_output = output; + } + + observation_records.push(record); + self.height += 1; + } + + let mod_pos = pos % CHUNK; + let (write_final, final_idx) = memory.write_cell(register_address_space, input_register_1, F::from_canonical_usize(mod_pos)); + + if observation_records.len() > 0 { + observation_records[0].is_first = true; + observation_records[len - 1].is_final = true; + observation_records[len - 1].write_final_idx = write_final; + observation_records[len - 1].final_idx = final_idx; + } + + Ok(ExecutionState { + pc: from_state.pc + DEFAULT_PC_STEP, + timestamp: memory.timestamp(), + }) + } + + fn get_opcode_name(&self, opcode: usize) -> String { + if opcode == MULTI_OBSERVE.global_opcode().as_usize() { + String::from("MULTI_OBSERVE") + } else { + unreachable!("unsupported opcode: {}", opcode) + } + } +} + +impl ChipUsageGetter for NativeMultiObserveChip { + fn air_name(&self) -> String { + "MultiObserve".to_string() + } + + fn current_trace_height(&self) -> usize { + self.height + } + + fn trace_width(&self) -> usize { + NativeMultiObserveCols::::width() + } +} + +impl Chip + for NativeMultiObserveChip> +where + Val: PrimeField32, +{ + fn air(&self) -> AirRef { + Arc::new(self.air.clone()) + } + fn generate_air_proof_input(self) -> AirProofInput { + AirProofInput::simple_no_pis(self.generate_trace()) + } +} \ No newline at end of file diff --git a/extensions/native/circuit/src/poseidon2/air.rs b/extensions/native/circuit/src/poseidon2/air.rs index 5ed28abd60..50ecde3459 100644 --- a/extensions/native/circuit/src/poseidon2/air.rs +++ b/extensions/native/circuit/src/poseidon2/air.rs @@ -21,8 +21,8 @@ use openvm_stark_backend::{ }; use crate::{ - chip::{NUM_INITIAL_READS, NUM_SIMPLE_ACCESSES}, poseidon2::{ + chip::{NUM_INITIAL_READS, NUM_SIMPLE_ACCESSES}, columns::{ InsideRowSpecificCols, NativePoseidon2Cols, SimplePoseidonSpecificCols, TopLevelSpecificCols, diff --git a/extensions/native/circuit/src/poseidon2/trace.rs b/extensions/native/circuit/src/poseidon2/trace.rs index df8547767f..76e9df018f 100644 --- a/extensions/native/circuit/src/poseidon2/trace.rs +++ b/extensions/native/circuit/src/poseidon2/trace.rs @@ -15,9 +15,9 @@ use openvm_stark_backend::{ }; use crate::{ - chip::{SimplePoseidonRecord, NUM_INITIAL_READS}, poseidon2::{ chip::{ + SimplePoseidonRecord, NUM_INITIAL_READS, CellRecord, IncorporateRowRecord, IncorporateSiblingRecord, InsideRowRecord, NativePoseidon2Chip, VerifyBatchRecord, }, diff --git a/vm_run_output.log b/vm_run_output.log new file mode 100644 index 0000000000..e69de29bb2 From c837427a821d124b3b4827f9aa93da821c7836e9 Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Wed, 16 Jul 2025 18:47:45 -0400 Subject: [PATCH 08/32] Preserve testing environment --- extensions/native/circuit/Cargo.toml | 1 - .../native/circuit/src/multi_observe/mod.rs | 3 + .../native/recursion/tests/recursion.rs | 92 ++++++++++++++++++- 3 files changed, 91 insertions(+), 5 deletions(-) diff --git a/extensions/native/circuit/Cargo.toml b/extensions/native/circuit/Cargo.toml index 5d5913b4be..e48af8f70a 100644 --- a/extensions/native/circuit/Cargo.toml +++ b/extensions/native/circuit/Cargo.toml @@ -19,7 +19,6 @@ openvm-instructions = { workspace = true } openvm-rv32im-circuit = { workspace = true } openvm-native-compiler = { workspace = true } - strum.workspace = true itertools.workspace = true tracing.workspace = true diff --git a/extensions/native/circuit/src/multi_observe/mod.rs b/extensions/native/circuit/src/multi_observe/mod.rs index e9bfe34f56..49452de1e1 100644 --- a/extensions/native/circuit/src/multi_observe/mod.rs +++ b/extensions/native/circuit/src/multi_observe/mod.rs @@ -154,6 +154,7 @@ impl Air for NativeMultiObserveAir { output_register, } = local; + /* _debug builder.assert_bool(enable); builder.assert_bool(is_first); builder.assert_bool(is_final); @@ -321,6 +322,8 @@ impl Air for NativeMultiObserveAir { &write_final_idx ) .eval(builder, is_final); + + */ } } diff --git a/extensions/native/recursion/tests/recursion.rs b/extensions/native/recursion/tests/recursion.rs index 8f354f3316..1fc5166473 100644 --- a/extensions/native/recursion/tests/recursion.rs +++ b/extensions/native/recursion/tests/recursion.rs @@ -1,13 +1,30 @@ -use openvm_circuit::arch::{instructions::program::Program, SystemConfig, VmConfig, VmExecutor}; +use openvm_circuit::arch::{instructions::program::Program, SystemConfig, VmConfig, VmExecutor, verify_single, VirtualMachine,}; use openvm_native_circuit::{Native, NativeConfig}; -use openvm_native_compiler::{asm::AsmBuilder, ir::Felt}; -use openvm_native_recursion::testing_utils::inner::run_recursive_test; +use openvm_native_compiler::{ + prelude::*, + asm::{AsmBuilder, AsmCompiler}, ir::Felt, + conversion::{convert_program, CompilerOptions}, +}; +use openvm_native_recursion::{testing_utils::inner::run_recursive_test, challenger::duplex::DuplexChallengerVariable}; use openvm_stark_backend::{ config::{Domain, StarkGenericConfig}, p3_commit::PolynomialSpace, p3_field::{extension::BinomialExtensionField, FieldAlgebra}, }; -use openvm_stark_sdk::{config::FriParameters, p3_baby_bear::BabyBear, utils::ProofInputForTest}; +use openvm_stark_sdk::{ + config::FriParameters, + p3_baby_bear::BabyBear, + utils::ProofInputForTest, + config::{ + baby_bear_poseidon2::BabyBearPoseidon2Engine, + fri_params::standard_fri_params_with_100_bits_conjectured_security, + }, + engine::StarkFriEngine, + utils::create_seeded_rng, +}; +use rand::Rng; +pub type F = BabyBear; +pub type E = BinomialExtensionField; fn fibonacci_program(a: u32, b: u32, n: u32) -> Program { type F = BabyBear; @@ -79,3 +96,70 @@ fn test_fibonacci_program_halo2_verify() { let fib_program_stark = fibonacci_program_test_proof_input(0, 1, 32); run_static_verifier_test(fib_program_stark, FriParameters::new_for_testing(3)); } + +#[test] +fn test_multi_observe() { + let mut builder = AsmBuilder::>::default(); + + build_test_program(&mut builder); + + // Fill in test program logic + builder.halt(); + + let compilation_options = CompilerOptions::default().with_cycle_tracker(); + let mut compiler = AsmCompiler::new(compilation_options.word_size); + compiler.build(builder.operations); + let asm_code = compiler.code(); + + // let program = Program::from_instructions(&instructions); + let program: Program<_> = convert_program(asm_code, compilation_options); + + let poseidon2_max_constraint_degree = 3; + + let fri_params = if matches!(std::env::var("OPENVM_FAST_TEST"), Ok(x) if &x == "1") { + FriParameters { + log_blowup: 3, + log_final_poly_len: 0, + num_queries: 2, + proof_of_work_bits: 0, + } + } else { + standard_fri_params_with_100_bits_conjectured_security(3) + }; + + let engine = BabyBearPoseidon2Engine::new(fri_params); + + let config = NativeConfig::aggregation(0, poseidon2_max_constraint_degree); + let vm = VirtualMachine::new(engine, config); + + let pk = vm.keygen(); + let result = vm.execute_and_generate(program, vec![]).unwrap(); + let proofs = vm.prove(&pk, result); + for proof in proofs { + verify_single(&vm.engine, &pk.get_vk(), &proof).expect("Verification failed"); + } +} + +fn build_test_program( + builder: &mut Builder, +) { + let sample_len: usize = 10; + + let mut rng = create_seeded_rng(); + let sample_input: Array> = builder.dyn_array(sample_len); + builder.range(0, sample_len).for_each(|idx_vec, builder| { + let f_u32: u32 = rng.gen_range(1..1 << 30); + builder.set(&sample_input, idx_vec[0], C::F::from_canonical_u32(f_u32)); + }); + + /* _debug + builder.range(0, sample_len).for_each(|idx_vec, builder| { + let f = builder.get(&sample_input, idx_vec[0]); + builder.print_f(f); + }); + */ + + // MultiObserve + // let mut challenger = DuplexChallengerVariable::new(builder); + // builder.poseidon2_multi_observe(&challenger.sponge_state, challenger.input_ptr, &sample_input); +} \ No newline at end of file From fe98b6c98eb2d7c4113b9c528278fcc91c164fe1 Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Thu, 17 Jul 2025 19:18:54 -0400 Subject: [PATCH 09/32] Fix constraints --- .../native/circuit/src/multi_observe/mod.rs | 178 +++++++++++------- .../native/recursion/tests/recursion.rs | 7 +- 2 files changed, 109 insertions(+), 76 deletions(-) diff --git a/extensions/native/circuit/src/multi_observe/mod.rs b/extensions/native/circuit/src/multi_observe/mod.rs index 49452de1e1..6457085109 100644 --- a/extensions/native/circuit/src/multi_observe/mod.rs +++ b/extensions/native/circuit/src/multi_observe/mod.rs @@ -103,28 +103,7 @@ impl Air for NativeMultiObserveAir { enable, is_first, is_final, - - // TODO: Should pass to execution bridge for Poseidon2 permutation - // Example: - // self.execution_bridge - // .execute_and_increment_pc( - // is_permute.clone() - // * AB::F::from_canonical_usize(PERM_POS2.global_opcode().as_usize()) - // + is_compress - // * AB::F::from_canonical_usize(COMP_POS2.global_opcode().as_usize()), - // [ - // output_register.into(), - // input_register_1.into(), - // input_register_2.into(), - // self.address_space.into(), - // self.address_space.into(), - // ], - // ExecutionState::new(pc, start_timestamp), - // AB::Expr::from_canonical_u32(NUM_SIMPLE_ACCESSES), - // ) - // .eval(builder, simple); - pc: _, - + pc, state_idx, remaining_len, counter, @@ -154,12 +133,66 @@ impl Air for NativeMultiObserveAir { output_register, } = local; - /* _debug - builder.assert_bool(enable); - builder.assert_bool(is_first); - builder.assert_bool(is_final); - builder.assert_bool(should_permute); + self.execution_bridge + .execute_and_increment_pc( + AB::F::from_canonical_usize(MULTI_OBSERVE.global_opcode().as_usize()), + [ + output_register.into(), + input_register_1.into(), + input_register_2.into(), + self.address_space.into(), + self.address_space.into(), + input_register_3.into(), + ], + ExecutionState::new(pc, first_timestamp), + AB::Expr::from_canonical_u32(4), + ) + .eval(builder, is_first); + + // Memory operations + self.memory_bridge + .read( + MemoryAddress::new(self.address_space, output_register), + [state_ptr], + first_timestamp, + &read_state_ptr, + ) + .eval(builder, is_first); + + self.memory_bridge + .read( + MemoryAddress::new(self.address_space, input_register_2), + [input_ptr], + first_timestamp + AB::F::ONE, + &read_input_ptr, + ) + .eval(builder, is_first); + self.memory_bridge + .read( + MemoryAddress::new(self.address_space, input_register_1), + [init_pos], + first_timestamp + AB::F::TWO, + &read_init_pos, + ) + .eval(builder, is_first); + + self.memory_bridge + .read( + MemoryAddress::new(self.address_space, input_register_3), + [len], + first_timestamp + AB::F::from_canonical_usize(3), + &read_len, + ) + .eval(builder, is_first); + + + // builder.assert_bool(enable); + // builder.assert_bool(is_first); + // builder.assert_bool(is_final); + // builder.assert_bool(should_permute); + + /* _debug // Row transitions // Each row must operate one element @@ -229,42 +262,7 @@ impl Air for NativeMultiObserveAir { .when(not(next.is_first)) .assert_eq(output_register, next.output_register); - // Memory operations - self.memory_bridge - .read( - MemoryAddress::new(self.address_space, output_register), - [state_ptr], - first_timestamp, - &read_state_ptr, - ) - .eval(builder, is_first); - - self.memory_bridge - .read( - MemoryAddress::new(self.address_space, input_register_2), - [input_ptr], - first_timestamp + AB::F::ONE, - &read_input_ptr, - ) - .eval(builder, is_first); - - self.memory_bridge - .read( - MemoryAddress::new(self.address_space, input_register_1), - [init_pos], - first_timestamp + AB::F::TWO, - &read_init_pos, - ) - .eval(builder, is_first); - self.memory_bridge - .read( - MemoryAddress::new(self.address_space, input_register_3), - [len], - first_timestamp + AB::F::from_canonical_usize(3), - &read_len, - ) - .eval(builder, is_first); self.memory_bridge .read( @@ -424,11 +422,11 @@ impl NativeMultiObserveChip { let read_init_pos_record = memory.record_by_id(record.read_init_pos); let read_len_record = memory.record_by_id(record.read_len); - let read_data_record = memory.record_by_id(record.read_input_data); - let write_data_record = memory.record_by_id(record.write_input_data); - - let read_sponge_record = memory.record_by_id(record.read_sponge_state); - let write_sponge_record = memory.record_by_id(record.write_sponge_state); + // _debug + // let read_data_record = memory.record_by_id(record.read_input_data); + // let write_data_record = memory.record_by_id(record.write_input_data); + // let read_sponge_record = memory.record_by_id(record.read_sponge_state); + // let write_sponge_record = memory.record_by_id(record.write_sponge_state); cols.state_ptr = record.state_ptr; cols.input_ptr = record.input_ptr; @@ -457,14 +455,15 @@ impl NativeMultiObserveChip { aux_cols_factory.generate_read_aux(read_input_ptr_record, &mut cols.read_input_ptr); aux_cols_factory.generate_read_aux(read_init_pos_record, &mut cols.read_init_pos); aux_cols_factory.generate_read_aux(read_len_record, &mut cols.read_len); - aux_cols_factory.generate_read_aux(read_data_record, &mut cols.read_data); - aux_cols_factory.generate_write_aux(write_data_record, &mut cols.write_data); - aux_cols_factory.generate_read_aux(read_sponge_record, &mut cols.read_sponge_state); - aux_cols_factory.generate_write_aux(write_sponge_record, &mut cols.write_sponge_state); + // _debug + // aux_cols_factory.generate_read_aux(read_data_record, &mut cols.read_data); + // aux_cols_factory.generate_write_aux(write_data_record, &mut cols.write_data); + // aux_cols_factory.generate_read_aux(read_sponge_record, &mut cols.read_sponge_state); + // aux_cols_factory.generate_write_aux(write_sponge_record, &mut cols.write_sponge_state); - let write_final_idx_record = memory.record_by_id(record.write_final_idx); - aux_cols_factory.generate_write_aux(write_final_idx_record, &mut cols.write_final_idx); + // let write_final_idx_record = memory.record_by_id(record.write_final_idx); + // aux_cols_factory.generate_write_aux(write_final_idx_record, &mut cols.write_final_idx); } fn generate_trace(self) -> RowMajorMatrix { @@ -517,7 +516,34 @@ impl InstructionExecutor for NativeMultiObserveChip { let len = len.as_canonical_u32() as usize; let mut curr_timestamp = 0usize; + + let head_record: TranscriptObservationRecord = TranscriptObservationRecord { + from_state, + instruction: instruction.clone(), + is_first: true, + state_idx: pos % CHUNK, + remaining_len: len, + counter: 0, + read_state_ptr: read_sponge_ptr, + read_input_ptr: read_arr_ptr, + state_ptr: sponge_ptr, + input_ptr: arr_ptr, + read_init_pos: read_init_pos, + init_pos, + read_len, + len, + input_register_1, + input_register_2, + input_register_3, + output_register, + ..Default::default() + }; + + self.height += 1; + observation_records.push(head_record); + + /* _debug for i in 0..len { let mut record: TranscriptObservationRecord = TranscriptObservationRecord { from_state, @@ -580,6 +606,12 @@ impl InstructionExecutor for NativeMultiObserveChip { observation_records[len - 1].final_idx = final_idx; } + */ + + for record in observation_records { + self.record_set.transcript_observation_records.push(record); + } + Ok(ExecutionState { pc: from_state.pc + DEFAULT_PC_STEP, timestamp: memory.timestamp(), diff --git a/extensions/native/recursion/tests/recursion.rs b/extensions/native/recursion/tests/recursion.rs index 1fc5166473..ef0d0f932b 100644 --- a/extensions/native/recursion/tests/recursion.rs +++ b/extensions/native/recursion/tests/recursion.rs @@ -128,8 +128,9 @@ fn test_multi_observe() { }; let engine = BabyBearPoseidon2Engine::new(fri_params); + let mut config = NativeConfig::aggregation(0, poseidon2_max_constraint_degree); + config.system.memory_config.max_access_adapter_n = 16; - let config = NativeConfig::aggregation(0, poseidon2_max_constraint_degree); let vm = VirtualMachine::new(engine, config); let pk = vm.keygen(); @@ -160,6 +161,6 @@ fn build_test_program( */ // MultiObserve - // let mut challenger = DuplexChallengerVariable::new(builder); - // builder.poseidon2_multi_observe(&challenger.sponge_state, challenger.input_ptr, &sample_input); + let mut challenger = DuplexChallengerVariable::new(builder); + builder.poseidon2_multi_observe(&challenger.sponge_state, challenger.input_ptr, &sample_input); } \ No newline at end of file From 99b059370301ed5d03484304b777e178aedf0e21 Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Thu, 17 Jul 2025 20:38:24 -0400 Subject: [PATCH 10/32] Fix constraints --- .../native/circuit/src/multi_observe/mod.rs | 84 +++++++++++-------- 1 file changed, 48 insertions(+), 36 deletions(-) diff --git a/extensions/native/circuit/src/multi_observe/mod.rs b/extensions/native/circuit/src/multi_observe/mod.rs index 6457085109..88b43d9f0f 100644 --- a/extensions/native/circuit/src/multi_observe/mod.rs +++ b/extensions/native/circuit/src/multi_observe/mod.rs @@ -6,7 +6,7 @@ use openvm_circuit::{ arch::{ExecutionBridge, ExecutionState, ExecutionError, InstructionExecutor, SystemPort}, system::memory::{offline_checker::MemoryBridge, MemoryAddress, MemoryController, OfflineMemory, RecordId}, }; -use openvm_circuit_primitives::utils::not; +use openvm_circuit_primitives::utils::{not, and}; use openvm_instructions::{instruction::Instruction, program::DEFAULT_PC_STEP, LocalOpcode}; use openvm_native_compiler::{ conversion::AS, @@ -48,6 +48,7 @@ pub struct NativeMultiObserveCols { /// and all following intermediate observation rows. pub first_timestamp: T, pub curr_timestamp: T, + pub final_timestamp_increment: T, pub read_state_ptr: MemoryReadAuxCols, pub read_input_ptr: MemoryReadAuxCols, @@ -110,6 +111,7 @@ impl Air for NativeMultiObserveAir { should_permute, first_timestamp, curr_timestamp, + final_timestamp_increment, read_state_ptr, read_input_ptr, state_ptr, @@ -145,7 +147,7 @@ impl Air for NativeMultiObserveAir { input_register_3.into(), ], ExecutionState::new(pc, first_timestamp), - AB::Expr::from_canonical_u32(4), + final_timestamp_increment, ) .eval(builder, is_first); @@ -186,11 +188,23 @@ impl Air for NativeMultiObserveAir { ) .eval(builder, is_first); - - // builder.assert_bool(enable); - // builder.assert_bool(is_first); - // builder.assert_bool(is_final); - // builder.assert_bool(should_permute); + self.memory_bridge + .write( + MemoryAddress::new( + self.address_space, + input_register_1, + ), + [final_idx], + first_timestamp + curr_timestamp + is_first * AB::F::from_canonical_usize(4) + should_permute * AB::F::from_canonical_usize(4), + // + (AB::F::ONE - is_first) * AB::F::TWO, // _debug + &write_final_idx + ) + .eval(builder, is_final); + + builder.assert_bool(enable); + builder.assert_bool(is_first); + builder.assert_bool(is_final); + builder.assert_bool(should_permute); /* _debug // Row transitions @@ -309,17 +323,7 @@ impl Air for NativeMultiObserveAir { ) .eval(builder, should_permute); - self.memory_bridge - .write( - MemoryAddress::new( - self.address_space, - input_register_1, - ), - [final_idx], - first_timestamp + curr_timestamp + is_first * AB::F::from_canonical_usize(4) + should_permute * AB::F::TWO + AB::F::TWO, - &write_final_idx - ) - .eval(builder, is_final); + */ } @@ -332,6 +336,7 @@ pub struct TranscriptObservationRecord { pub from_state: ExecutionState, pub instruction: Instruction, pub curr_timestamp: usize, + pub final_timestamp_increment: usize, pub state_idx: usize, @@ -434,6 +439,7 @@ impl NativeMultiObserveChip { cols.len = F::from_canonical_usize(record.len); cols.data = record.input_data; cols.curr_timestamp = F::from_canonical_usize(record.curr_timestamp); + cols.final_timestamp_increment = F::from_canonical_usize(record.final_timestamp_increment); cols.permutation_input = record.permutation_input; cols.permutation_output = record.permutation_output; @@ -451,10 +457,12 @@ impl NativeMultiObserveChip { cols.input_register_3 = record.input_register_3; cols.output_register = record.output_register; - aux_cols_factory.generate_read_aux(read_state_ptr_record, &mut cols.read_state_ptr); - aux_cols_factory.generate_read_aux(read_input_ptr_record, &mut cols.read_input_ptr); - aux_cols_factory.generate_read_aux(read_init_pos_record, &mut cols.read_init_pos); - aux_cols_factory.generate_read_aux(read_len_record, &mut cols.read_len); + if record.is_first { + aux_cols_factory.generate_read_aux(read_state_ptr_record, &mut cols.read_state_ptr); + aux_cols_factory.generate_read_aux(read_input_ptr_record, &mut cols.read_input_ptr); + aux_cols_factory.generate_read_aux(read_init_pos_record, &mut cols.read_init_pos); + aux_cols_factory.generate_read_aux(read_len_record, &mut cols.read_len); + } // _debug // aux_cols_factory.generate_read_aux(read_data_record, &mut cols.read_data); @@ -462,8 +470,10 @@ impl NativeMultiObserveChip { // aux_cols_factory.generate_read_aux(read_sponge_record, &mut cols.read_sponge_state); // aux_cols_factory.generate_write_aux(write_sponge_record, &mut cols.write_sponge_state); - // let write_final_idx_record = memory.record_by_id(record.write_final_idx); - // aux_cols_factory.generate_write_aux(write_final_idx_record, &mut cols.write_final_idx); + if record.is_final { + let write_final_idx_record = memory.record_by_id(record.write_final_idx); + aux_cols_factory.generate_write_aux(write_final_idx_record, &mut cols.write_final_idx); + } } fn generate_trace(self) -> RowMajorMatrix { @@ -478,7 +488,7 @@ impl NativeMultiObserveChip { self.record_to_row( record, &aux_cols_factory, - &mut flat_trace[used_cells..], + &mut flat_trace[used_cells..used_cells + width], &memory, ); used_cells += width; @@ -515,8 +525,6 @@ impl InstructionExecutor for NativeMultiObserveChip { let (read_len, len) = memory.read_cell(register_address_space, input_register_3); let len = len.as_canonical_u32() as usize; - let mut curr_timestamp = 0usize; - let head_record: TranscriptObservationRecord = TranscriptObservationRecord { from_state, instruction: instruction.clone(), @@ -541,9 +549,9 @@ impl InstructionExecutor for NativeMultiObserveChip { self.height += 1; observation_records.push(head_record); - - /* _debug + let mut curr_timestamp = 4usize; + for i in 0..len { let mut record: TranscriptObservationRecord = TranscriptObservationRecord { from_state, @@ -567,6 +575,7 @@ impl InstructionExecutor for NativeMultiObserveChip { ..Default::default() }; + /* _debug let (n_read, n_f) = memory.read_cell(data_address_space, arr_ptr + F::from_canonical_usize(i)); record.read_input_data = n_read; record.input_data = n_f; @@ -591,22 +600,25 @@ impl InstructionExecutor for NativeMultiObserveChip { record.permutation_input = permutation_input; record.permutation_output = output; } + */ observation_records.push(record); self.height += 1; } + let mod_pos = pos % CHUNK; let (write_final, final_idx) = memory.write_cell(register_address_space, input_register_1, F::from_canonical_usize(mod_pos)); + curr_timestamp += 1; - if observation_records.len() > 0 { - observation_records[0].is_first = true; - observation_records[len - 1].is_final = true; - observation_records[len - 1].write_final_idx = write_final; - observation_records[len - 1].final_idx = final_idx; - } + observation_records[0].is_first = true; + observation_records.last_mut().unwrap().is_final = true; + observation_records.last_mut().unwrap().write_final_idx = write_final; + observation_records.last_mut().unwrap().final_idx = final_idx; - */ + for record in &mut observation_records { + record.final_timestamp_increment = curr_timestamp; + } for record in observation_records { self.record_set.transcript_observation_records.push(record); From ddd2f30bc78fca16f4003680f16ba66e491ae81f Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Thu, 17 Jul 2025 21:06:55 -0400 Subject: [PATCH 11/32] Fix constraints --- .../native/circuit/src/multi_observe/mod.rs | 36 +++++++++---------- 1 file changed, 18 insertions(+), 18 deletions(-) diff --git a/extensions/native/circuit/src/multi_observe/mod.rs b/extensions/native/circuit/src/multi_observe/mod.rs index 88b43d9f0f..71a1c64d2b 100644 --- a/extensions/native/circuit/src/multi_observe/mod.rs +++ b/extensions/native/circuit/src/multi_observe/mod.rs @@ -188,18 +188,18 @@ impl Air for NativeMultiObserveAir { ) .eval(builder, is_first); - self.memory_bridge - .write( - MemoryAddress::new( - self.address_space, - input_register_1, - ), - [final_idx], - first_timestamp + curr_timestamp + is_first * AB::F::from_canonical_usize(4) + should_permute * AB::F::from_canonical_usize(4), - // + (AB::F::ONE - is_first) * AB::F::TWO, // _debug - &write_final_idx - ) - .eval(builder, is_final); + // self.memory_bridge + // .write( + // MemoryAddress::new( + // self.address_space, + // input_register_1, + // ), + // [final_idx], + // first_timestamp + curr_timestamp + is_first * AB::F::from_canonical_usize(4) + should_permute * AB::F::from_canonical_usize(4), + // // + (AB::F::ONE - is_first) * AB::F::TWO, // _debug + // &write_final_idx + // ) + // .eval(builder, is_final); builder.assert_bool(enable); builder.assert_bool(is_first); @@ -471,8 +471,8 @@ impl NativeMultiObserveChip { // aux_cols_factory.generate_write_aux(write_sponge_record, &mut cols.write_sponge_state); if record.is_final { - let write_final_idx_record = memory.record_by_id(record.write_final_idx); - aux_cols_factory.generate_write_aux(write_final_idx_record, &mut cols.write_final_idx); + // let write_final_idx_record = memory.record_by_id(record.write_final_idx); + // aux_cols_factory.generate_write_aux(write_final_idx_record, &mut cols.write_final_idx); } } @@ -608,13 +608,13 @@ impl InstructionExecutor for NativeMultiObserveChip { let mod_pos = pos % CHUNK; - let (write_final, final_idx) = memory.write_cell(register_address_space, input_register_1, F::from_canonical_usize(mod_pos)); - curr_timestamp += 1; + // let (write_final, final_idx) = memory.write_cell(register_address_space, input_register_1, F::from_canonical_usize(mod_pos)); + // curr_timestamp += 1; observation_records[0].is_first = true; observation_records.last_mut().unwrap().is_final = true; - observation_records.last_mut().unwrap().write_final_idx = write_final; - observation_records.last_mut().unwrap().final_idx = final_idx; + // observation_records.last_mut().unwrap().write_final_idx = write_final; + // observation_records.last_mut().unwrap().final_idx = final_idx; for record in &mut observation_records { record.final_timestamp_increment = curr_timestamp; From 67a2aed5c7b7f4e2afa9e622152fa2b289123ba3 Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Thu, 17 Jul 2025 21:50:58 -0400 Subject: [PATCH 12/32] Fix constraints --- .../native/circuit/src/multi_observe/mod.rs | 94 +++++++++++-------- 1 file changed, 53 insertions(+), 41 deletions(-) diff --git a/extensions/native/circuit/src/multi_observe/mod.rs b/extensions/native/circuit/src/multi_observe/mod.rs index 71a1c64d2b..061f25deec 100644 --- a/extensions/native/circuit/src/multi_observe/mod.rs +++ b/extensions/native/circuit/src/multi_observe/mod.rs @@ -37,6 +37,7 @@ pub struct NativeMultiObserveCols { pub enable: T, pub is_first: T, pub is_final: T, + pub is_observe: T, pub pc: T, pub state_idx: T, @@ -104,6 +105,7 @@ impl Air for NativeMultiObserveAir { enable, is_first, is_final, + is_observe, pc, state_idx, remaining_len, @@ -188,6 +190,27 @@ impl Air for NativeMultiObserveAir { ) .eval(builder, is_first); + self.memory_bridge + .read( + MemoryAddress::new(self.address_space, input_ptr + counter - AB::F::ONE), + [data], + first_timestamp + curr_timestamp, + &read_data + ) + .eval(builder, is_observe); + + self.memory_bridge + .write( + MemoryAddress::new( + self.address_space, + state_ptr + state_idx, + ), + [data], + first_timestamp + curr_timestamp + AB::F::ONE, + &write_data, + ) + .eval(builder, is_observe); + // self.memory_bridge // .write( // MemoryAddress::new( @@ -201,10 +224,10 @@ impl Air for NativeMultiObserveAir { // ) // .eval(builder, is_final); - builder.assert_bool(enable); - builder.assert_bool(is_first); - builder.assert_bool(is_final); - builder.assert_bool(should_permute); + // builder.assert_bool(enable); + // builder.assert_bool(is_first); + // builder.assert_bool(is_final); + // builder.assert_bool(should_permute); /* _debug // Row transitions @@ -278,26 +301,9 @@ impl Air for NativeMultiObserveAir { - self.memory_bridge - .read( - MemoryAddress::new(self.address_space, input_ptr + counter), - [data], - first_timestamp + curr_timestamp + is_first * AB::F::from_canonical_usize(4), - &read_data - ) - .eval(builder, is_first); + - self.memory_bridge - .write( - MemoryAddress::new( - self.address_space, - state_ptr + state_idx, - ), - [data], - first_timestamp + curr_timestamp + is_first * AB::F::from_canonical_usize(4) + AB::F::ONE, - &write_data, - ) - .eval(builder, enable); + self.memory_bridge .read( @@ -341,6 +347,7 @@ pub struct TranscriptObservationRecord { pub state_idx: usize, pub is_first: bool, + pub is_observe: bool, pub is_final: bool, pub remaining_len: usize, pub counter: usize, @@ -420,6 +427,7 @@ impl NativeMultiObserveChip { cols.enable = F::ONE; cols.is_first = if record.is_first { F::ONE } else { F::ZERO }; cols.is_final = if record.is_final { F::ONE } else { F::ZERO }; + cols.is_observe = if !record.is_first { F::ONE } else { F::ZERO }; cols.should_permute = if record.should_permute { F::ONE } else { F::ZERO }; let read_state_ptr_record = memory.record_by_id(record.read_state_ptr); @@ -427,12 +435,6 @@ impl NativeMultiObserveChip { let read_init_pos_record = memory.record_by_id(record.read_init_pos); let read_len_record = memory.record_by_id(record.read_len); - // _debug - // let read_data_record = memory.record_by_id(record.read_input_data); - // let write_data_record = memory.record_by_id(record.write_input_data); - // let read_sponge_record = memory.record_by_id(record.read_sponge_state); - // let write_sponge_record = memory.record_by_id(record.write_sponge_state); - cols.state_ptr = record.state_ptr; cols.input_ptr = record.input_ptr; cols.init_pos = record.init_pos; @@ -444,9 +446,9 @@ impl NativeMultiObserveChip { cols.permutation_input = record.permutation_input; cols.permutation_output = record.permutation_output; - cols.state_idx = cols.state_idx; - cols.remaining_len = cols.remaining_len; - cols.counter = cols.counter; + cols.state_idx = F::from_canonical_usize(record.state_idx); + cols.remaining_len = F::from_canonical_usize(record.remaining_len); + cols.counter = F::from_canonical_usize(record.counter); cols.final_idx = record.final_idx; cols.first_timestamp = F::from_canonical_u32(record.from_state.timestamp); @@ -464,11 +466,19 @@ impl NativeMultiObserveChip { aux_cols_factory.generate_read_aux(read_len_record, &mut cols.read_len); } - // _debug - // aux_cols_factory.generate_read_aux(read_data_record, &mut cols.read_data); - // aux_cols_factory.generate_write_aux(write_data_record, &mut cols.write_data); - // aux_cols_factory.generate_read_aux(read_sponge_record, &mut cols.read_sponge_state); - // aux_cols_factory.generate_write_aux(write_sponge_record, &mut cols.write_sponge_state); + if record.is_observe { + let read_data_record = memory.record_by_id(record.read_input_data); + let write_data_record = memory.record_by_id(record.write_input_data); + aux_cols_factory.generate_read_aux(read_data_record, &mut cols.read_data); + aux_cols_factory.generate_write_aux(write_data_record, &mut cols.write_data); + } + + if record.should_permute { + // let read_sponge_record = memory.record_by_id(record.read_sponge_state); + // let write_sponge_record = memory.record_by_id(record.write_sponge_state); + // aux_cols_factory.generate_read_aux(read_sponge_record, &mut cols.read_sponge_state); + // aux_cols_factory.generate_write_aux(write_sponge_record, &mut cols.write_sponge_state); + } if record.is_final { // let write_final_idx_record = memory.record_by_id(record.write_final_idx); @@ -551,15 +561,17 @@ impl InstructionExecutor for NativeMultiObserveChip { observation_records.push(head_record); let mut curr_timestamp = 4usize; + for i in 0..len { let mut record: TranscriptObservationRecord = TranscriptObservationRecord { from_state, curr_timestamp, instruction: instruction.clone(), + is_observe: true, state_idx: pos % CHUNK, - remaining_len: len - i, - counter: i, + remaining_len: len - i - 1, + counter: i + 1, read_state_ptr: read_sponge_ptr, read_input_ptr: read_arr_ptr, state_ptr: sponge_ptr, @@ -575,7 +587,6 @@ impl InstructionExecutor for NativeMultiObserveChip { ..Default::default() }; - /* _debug let (n_read, n_f) = memory.read_cell(data_address_space, arr_ptr + F::from_canonical_usize(i)); record.read_input_data = n_read; record.input_data = n_f; @@ -587,6 +598,8 @@ impl InstructionExecutor for NativeMultiObserveChip { pos += 1; + /* _debug + if pos % CHUNK == 0 { record.should_permute = true; let (read_sponge_record, permutation_input) = memory.read::<{CHUNK * 2}>(data_address_space, sponge_ptr); @@ -606,7 +619,6 @@ impl InstructionExecutor for NativeMultiObserveChip { self.height += 1; } - let mod_pos = pos % CHUNK; // let (write_final, final_idx) = memory.write_cell(register_address_space, input_register_1, F::from_canonical_usize(mod_pos)); // curr_timestamp += 1; From 9bf9b78844455dcf097c797cb6582ea6feaf2ebe Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Sun, 20 Jul 2025 04:25:16 -0400 Subject: [PATCH 13/32] Fix constraint --- .../native/circuit/src/multi_observe/mod.rs | 68 ++++++++----------- 1 file changed, 28 insertions(+), 40 deletions(-) diff --git a/extensions/native/circuit/src/multi_observe/mod.rs b/extensions/native/circuit/src/multi_observe/mod.rs index 061f25deec..65bc17cbea 100644 --- a/extensions/native/circuit/src/multi_observe/mod.rs +++ b/extensions/native/circuit/src/multi_observe/mod.rs @@ -211,6 +211,30 @@ impl Air for NativeMultiObserveAir { ) .eval(builder, is_observe); + self.memory_bridge + .read( + MemoryAddress::new( + self.address_space, + state_ptr, + ), + permutation_input, + first_timestamp + curr_timestamp + AB::F::TWO, + &read_sponge_state, + ) + .eval(builder, should_permute); + + self.memory_bridge + .write( + MemoryAddress::new( + self.address_space, + state_ptr + ), + permutation_output, + first_timestamp + curr_timestamp + AB::F::from_canonical_usize(3), + &write_sponge_state, + ) + .eval(builder, should_permute); + // self.memory_bridge // .write( // MemoryAddress::new( @@ -298,39 +322,6 @@ impl Air for NativeMultiObserveAir { .when(next.enable) .when(not(next.is_first)) .assert_eq(output_register, next.output_register); - - - - - - - - self.memory_bridge - .read( - MemoryAddress::new( - self.address_space, - state_ptr, - ), - permutation_input, - first_timestamp + curr_timestamp + is_first * AB::F::from_canonical_usize(4) + AB::F::TWO, - &read_sponge_state, - ) - .eval(builder, should_permute); - - self.memory_bridge - .write( - MemoryAddress::new( - self.address_space, - state_ptr - ), - permutation_output, - first_timestamp + curr_timestamp + is_first * AB::F::from_canonical_usize(4) + AB::F::from_canonical_usize(3), - &write_sponge_state, - ) - .eval(builder, should_permute); - - - */ } } @@ -474,10 +465,10 @@ impl NativeMultiObserveChip { } if record.should_permute { - // let read_sponge_record = memory.record_by_id(record.read_sponge_state); - // let write_sponge_record = memory.record_by_id(record.write_sponge_state); - // aux_cols_factory.generate_read_aux(read_sponge_record, &mut cols.read_sponge_state); - // aux_cols_factory.generate_write_aux(write_sponge_record, &mut cols.write_sponge_state); + let read_sponge_record = memory.record_by_id(record.read_sponge_state); + let write_sponge_record = memory.record_by_id(record.write_sponge_state); + aux_cols_factory.generate_read_aux(read_sponge_record, &mut cols.read_sponge_state); + aux_cols_factory.generate_write_aux(write_sponge_record, &mut cols.write_sponge_state); } if record.is_final { @@ -598,8 +589,6 @@ impl InstructionExecutor for NativeMultiObserveChip { pos += 1; - /* _debug - if pos % CHUNK == 0 { record.should_permute = true; let (read_sponge_record, permutation_input) = memory.read::<{CHUNK * 2}>(data_address_space, sponge_ptr); @@ -613,7 +602,6 @@ impl InstructionExecutor for NativeMultiObserveChip { record.permutation_input = permutation_input; record.permutation_output = output; } - */ observation_records.push(record); self.height += 1; From a639d7475853de1c6bce42f3d2f3460b8efbc8aa Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Sun, 20 Jul 2025 04:46:30 -0400 Subject: [PATCH 14/32] Fix constraints --- .../native/circuit/src/multi_observe/mod.rs | 39 +++++++++---------- .../native/recursion/tests/recursion.rs | 23 ++++++++++- 2 files changed, 41 insertions(+), 21 deletions(-) diff --git a/extensions/native/circuit/src/multi_observe/mod.rs b/extensions/native/circuit/src/multi_observe/mod.rs index 65bc17cbea..9fb49a3fe2 100644 --- a/extensions/native/circuit/src/multi_observe/mod.rs +++ b/extensions/native/circuit/src/multi_observe/mod.rs @@ -235,18 +235,17 @@ impl Air for NativeMultiObserveAir { ) .eval(builder, should_permute); - // self.memory_bridge - // .write( - // MemoryAddress::new( - // self.address_space, - // input_register_1, - // ), - // [final_idx], - // first_timestamp + curr_timestamp + is_first * AB::F::from_canonical_usize(4) + should_permute * AB::F::from_canonical_usize(4), - // // + (AB::F::ONE - is_first) * AB::F::TWO, // _debug - // &write_final_idx - // ) - // .eval(builder, is_final); + self.memory_bridge + .write( + MemoryAddress::new( + self.address_space, + input_register_1, + ), + [final_idx], + first_timestamp + curr_timestamp + is_first * AB::F::from_canonical_usize(4) + is_observe * AB::F::TWO + should_permute * AB::F::TWO, + &write_final_idx + ) + .eval(builder, is_final); // builder.assert_bool(enable); // builder.assert_bool(is_first); @@ -364,7 +363,7 @@ pub struct TranscriptObservationRecord { pub permutation_output: [F; 2 * CHUNK], pub write_final_idx: RecordId, - pub final_idx: F, + pub final_idx: usize, pub input_register_1: F, pub input_register_2: F, @@ -440,7 +439,7 @@ impl NativeMultiObserveChip { cols.state_idx = F::from_canonical_usize(record.state_idx); cols.remaining_len = F::from_canonical_usize(record.remaining_len); cols.counter = F::from_canonical_usize(record.counter); - cols.final_idx = record.final_idx; + cols.final_idx = F::from_canonical_usize(record.final_idx); cols.first_timestamp = F::from_canonical_u32(record.from_state.timestamp); cols.pc = F::from_canonical_u32(record.from_state.pc); @@ -472,8 +471,8 @@ impl NativeMultiObserveChip { } if record.is_final { - // let write_final_idx_record = memory.record_by_id(record.write_final_idx); - // aux_cols_factory.generate_write_aux(write_final_idx_record, &mut cols.write_final_idx); + let write_final_idx_record = memory.record_by_id(record.write_final_idx); + aux_cols_factory.generate_write_aux(write_final_idx_record, &mut cols.write_final_idx); } } @@ -608,13 +607,13 @@ impl InstructionExecutor for NativeMultiObserveChip { } let mod_pos = pos % CHUNK; - // let (write_final, final_idx) = memory.write_cell(register_address_space, input_register_1, F::from_canonical_usize(mod_pos)); - // curr_timestamp += 1; + let (write_final, _) = memory.write_cell(register_address_space, input_register_1, F::from_canonical_usize(mod_pos)); + curr_timestamp += 1; observation_records[0].is_first = true; observation_records.last_mut().unwrap().is_final = true; - // observation_records.last_mut().unwrap().write_final_idx = write_final; - // observation_records.last_mut().unwrap().final_idx = final_idx; + observation_records.last_mut().unwrap().write_final_idx = write_final; + observation_records.last_mut().unwrap().final_idx = mod_pos; for record in &mut observation_records { record.final_timestamp_increment = curr_timestamp; diff --git a/extensions/native/recursion/tests/recursion.rs b/extensions/native/recursion/tests/recursion.rs index ef0d0f932b..8a76b48553 100644 --- a/extensions/native/recursion/tests/recursion.rs +++ b/extensions/native/recursion/tests/recursion.rs @@ -144,6 +144,26 @@ fn test_multi_observe() { fn build_test_program( builder: &mut Builder, ) { + let sample_lens: Vec = vec![0, 10, 20]; + let mut rng = create_seeded_rng(); + let challenger = DuplexChallengerVariable::new(builder); + + for l in sample_lens { + let sample_input: Array> = builder.dyn_array(l); + builder.range(0, l).for_each(|idx_vec, builder| { + let f_u32: u32 = rng.gen_range(1..1 << 30); + builder.set(&sample_input, idx_vec[0], C::F::from_canonical_u32(f_u32)); + }); + + builder.poseidon2_multi_observe(&challenger.sponge_state, challenger.input_ptr, &sample_input); + } + + + + + + + /* _debug let sample_len: usize = 10; let mut rng = create_seeded_rng(); @@ -161,6 +181,7 @@ fn build_test_program( */ // MultiObserve - let mut challenger = DuplexChallengerVariable::new(builder); + let challenger = DuplexChallengerVariable::new(builder); builder.poseidon2_multi_observe(&challenger.sponge_state, challenger.input_ptr, &sample_input); + */ } \ No newline at end of file From a7e29b52b4a2f3d83468b80aef27dd420bdd9278 Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Sun, 20 Jul 2025 05:04:57 -0400 Subject: [PATCH 15/32] Complete constraints --- .../native/circuit/src/multi_observe/mod.rs | 68 +++++++++++++------ 1 file changed, 48 insertions(+), 20 deletions(-) diff --git a/extensions/native/circuit/src/multi_observe/mod.rs b/extensions/native/circuit/src/multi_observe/mod.rs index 9fb49a3fe2..2de8e28a69 100644 --- a/extensions/native/circuit/src/multi_observe/mod.rs +++ b/extensions/native/circuit/src/multi_observe/mod.rs @@ -6,7 +6,7 @@ use openvm_circuit::{ arch::{ExecutionBridge, ExecutionState, ExecutionError, InstructionExecutor, SystemPort}, system::memory::{offline_checker::MemoryBridge, MemoryAddress, MemoryController, OfflineMemory, RecordId}, }; -use openvm_circuit_primitives::utils::{not, and}; +use openvm_circuit_primitives::utils::not; use openvm_instructions::{instruction::Instruction, program::DEFAULT_PC_STEP, LocalOpcode}; use openvm_native_compiler::{ conversion::AS, @@ -247,32 +247,36 @@ impl Air for NativeMultiObserveAir { ) .eval(builder, is_final); - // builder.assert_bool(enable); - // builder.assert_bool(is_first); - // builder.assert_bool(is_final); - // builder.assert_bool(should_permute); - - /* _debug - // Row transitions + // Binary indicators columns + builder.assert_bool(enable); + builder.assert_bool(is_first); + builder.assert_bool(is_observe); + builder.assert_bool(is_final); + builder.assert_bool(should_permute); - // Each row must operate one element + // Except header rows, any other rows must observe an element + // All rows following the header row must observe an element + builder + .when(enable) + .assert_eq(is_first + is_observe, AB::F::ONE); builder + .when(is_observe) .when(next.enable) .when(not(next.is_first)) - .assert_eq(next.counter, counter + AB::F::ONE); + .assert_eq(next.is_observe, AB::F::ONE); + + // Each non-header row must process a field element builder .when(next.enable) .when(not(next.is_first)) - .assert_eq(next.remaining_len, remaining_len - AB::F::ONE); - - // After each permutation, the sponge state index must revert to 0 + .assert_eq(next.counter, counter + AB::F::ONE); builder - .when(should_permute) + .when(next.enable) .when(not(next.is_first)) - .assert_eq(next.state_idx, AB::F::ZERO); + .assert_eq(next.remaining_len, remaining_len - AB::F::ONE); // Boundary conditions - // At the first row, counter must be 0, remaining_len must be len + // At the header row, counter must be 0, remaining_len must be len builder .when(is_first) .assert_eq(counter, AB::F::ZERO); @@ -280,13 +284,38 @@ impl Air for NativeMultiObserveAir { .when(is_first) .assert_eq(remaining_len, len); - // At the last row, counter must be len - 1, remaining_len must be 1 + // At the final row, counter must be len, remaining_len must be 0 builder .when(is_final) - .assert_eq(counter, len - AB::F::ONE); + .assert_eq(counter, len); builder .when(is_final) - .assert_eq(remaining_len, AB::F::ONE); + .assert_eq(remaining_len, AB::F::ZERO); + + // After each permutation, the sponge state index must revert to 0 + builder + .when(should_permute) + .when(not(next.is_first)) + .assert_eq(next.state_idx, AB::F::ZERO); + + // Timestamp constraints + builder + .when(is_first) + .assert_eq(curr_timestamp, AB::F::ZERO); + builder + .when(is_first) + .when(not(is_final)) + .assert_eq(next.curr_timestamp - curr_timestamp, AB::F::from_canonical_usize(4)); + builder + .when(is_observe) + .when(not(is_final)) + .when(not(should_permute)) + .assert_eq(next.curr_timestamp - curr_timestamp, AB::F::TWO); + builder + .when(is_observe) + .when(not(is_final)) + .when(should_permute) + .assert_eq(next.curr_timestamp - curr_timestamp, AB::F::from_canonical_usize(4)); // Fields that remain constant for a single MULTI_OBSERVE call builder @@ -321,7 +350,6 @@ impl Air for NativeMultiObserveAir { .when(next.enable) .when(not(next.is_first)) .assert_eq(output_register, next.output_register); - */ } } From 704de9d8f31e4f5ccddbf25fb25e85b20fa63559 Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Sun, 20 Jul 2025 05:05:16 -0400 Subject: [PATCH 16/32] Remove debug code --- .../native/recursion/tests/recursion.rs | 27 ------------------- 1 file changed, 27 deletions(-) diff --git a/extensions/native/recursion/tests/recursion.rs b/extensions/native/recursion/tests/recursion.rs index 8a76b48553..f8b440e2ae 100644 --- a/extensions/native/recursion/tests/recursion.rs +++ b/extensions/native/recursion/tests/recursion.rs @@ -157,31 +157,4 @@ fn build_test_program( builder.poseidon2_multi_observe(&challenger.sponge_state, challenger.input_ptr, &sample_input); } - - - - - - - /* _debug - let sample_len: usize = 10; - - let mut rng = create_seeded_rng(); - let sample_input: Array> = builder.dyn_array(sample_len); - builder.range(0, sample_len).for_each(|idx_vec, builder| { - let f_u32: u32 = rng.gen_range(1..1 << 30); - builder.set(&sample_input, idx_vec[0], C::F::from_canonical_u32(f_u32)); - }); - - /* _debug - builder.range(0, sample_len).for_each(|idx_vec, builder| { - let f = builder.get(&sample_input, idx_vec[0]); - builder.print_f(f); - }); - */ - - // MultiObserve - let challenger = DuplexChallengerVariable::new(builder); - builder.poseidon2_multi_observe(&challenger.sponge_state, challenger.input_ptr, &sample_input); - */ } \ No newline at end of file From b6d2fcfe787da4c780a0f81b5075deb4d0e75dca Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Sun, 20 Jul 2025 23:03:35 -0400 Subject: [PATCH 17/32] Remove multi observe logic from poseidon2 chip --- .../native/circuit/src/poseidon2/chip.rs | 41 +------------------ vm_run_output.log | 1 + 2 files changed, 2 insertions(+), 40 deletions(-) diff --git a/extensions/native/circuit/src/poseidon2/chip.rs b/extensions/native/circuit/src/poseidon2/chip.rs index f26db6ffe7..426b089a9c 100644 --- a/extensions/native/circuit/src/poseidon2/chip.rs +++ b/extensions/native/circuit/src/poseidon2/chip.rs @@ -9,7 +9,7 @@ use openvm_circuit::{ use openvm_instructions::{instruction::Instruction, program::DEFAULT_PC_STEP, LocalOpcode}; use openvm_native_compiler::{ conversion::AS, - Poseidon2Opcode::{COMP_POS2, PERM_POS2, MULTI_OBSERVE}, + Poseidon2Opcode::{COMP_POS2, PERM_POS2}, VerifyBatchOpcode::VERIFY_BATCH, }; use openvm_poseidon2_air::{Poseidon2Config, Poseidon2SubAir, Poseidon2SubChip}; @@ -485,43 +485,6 @@ impl InstructionExecutor initial_log_height: initial_log_height as usize, top_level, }); - } else if instruction.opcode == MULTI_OBSERVE.global_opcode() { - let &Instruction { - a: output_register, - b: input_register_1, - c: input_register_2, - d: data_address_space, - e: register_address_space, - f: input_register_3, - .. - } = instruction; - - let (_, sponge_ptr) = memory.read_cell(register_address_space, output_register); - let (_, arr_ptr) = memory.read_cell(register_address_space, input_register_2); - - let init_pos_read = memory.read_cell(register_address_space, input_register_1); - let mut pos = init_pos_read.1.as_canonical_u32() as usize; - - let len_read = memory.read_cell(register_address_space, input_register_3); - let len = len_read.1.as_canonical_u32() as usize; - - for i in 0..len { - let mod_pos = pos % CHUNK; - let n_read = memory.read_cell(data_address_space, arr_ptr + F::from_canonical_usize(i)); - let n_f = n_read.1; - - memory.write_cell(data_address_space, sponge_ptr + F::from_canonical_usize(mod_pos), n_f); - pos += 1; - - if pos % CHUNK == 0 { - let (_, sponge_state) = memory.read::<{CHUNK * 2}>(data_address_space, sponge_ptr); - let output = self.subchip.permute(sponge_state); - memory.write::<{CHUNK * 2}>(data_address_space, sponge_ptr, std::array::from_fn(|i| output[i])); - } - } - - let mod_pos = pos % CHUNK; - memory.write_cell(register_address_space, input_register_1, F::from_canonical_usize(mod_pos)); } else { unreachable!() } @@ -538,8 +501,6 @@ impl InstructionExecutor String::from("PERM_POS2") } else if opcode == COMP_POS2.global_opcode().as_usize() { String::from("COMP_POS2") - } else if opcode == MULTI_OBSERVE.global_opcode().as_usize() { - String::from("MULTI_OBSERVE") } else { unreachable!("unsupported opcode: {}", opcode) } diff --git a/vm_run_output.log b/vm_run_output.log index e69de29bb2..feb1f17353 100644 --- a/vm_run_output.log +++ b/vm_run_output.log @@ -0,0 +1 @@ +error: package ID specification `ceno-recursion-verifier` did not match any packages From b6629caaf2e1b2de6de1adc7aaa796f531716d80 Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Tue, 22 Jul 2025 18:40:43 -0400 Subject: [PATCH 18/32] Resolve minor build issue --- crates/vm/src/metrics/cycle_tracker/mod.rs | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/crates/vm/src/metrics/cycle_tracker/mod.rs b/crates/vm/src/metrics/cycle_tracker/mod.rs index 27a457c7c4..c9fe306ca3 100644 --- a/crates/vm/src/metrics/cycle_tracker/mod.rs +++ b/crates/vm/src/metrics/cycle_tracker/mod.rs @@ -2,9 +2,9 @@ #[derive(Clone, Debug, Default)] pub struct SpanInfo { /// The name of the span. - tag: String, + pub tag: String, /// The cycle count at which the span starts. - start: usize, + pub start: usize, } #[derive(Clone, Debug, Default)] @@ -21,7 +21,10 @@ impl CycleTracker { } pub fn top(&self) -> Option<&String> { - self.stack.last() + match self.stack.last() { + Some(span) => Some(&span.tag), + _ => None + } } /// Starts a new cycle tracker span for the given name. From 831470c9d5fbc4cd15c60dc87b2f7b75b2c28a2e Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Tue, 22 Jul 2025 18:42:17 -0400 Subject: [PATCH 19/32] Resolve minor build issue --- crates/vm/src/metrics/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crates/vm/src/metrics/mod.rs b/crates/vm/src/metrics/mod.rs index 916e8251ac..fe73dce25d 100644 --- a/crates/vm/src/metrics/mod.rs +++ b/crates/vm/src/metrics/mod.rs @@ -117,7 +117,7 @@ impl VmMetrics { .map(|(_, func)| (*func).clone()) .unwrap(); if pc == self.current_fn.start { - self.cycle_tracker.start(self.current_fn.name.clone()); + self.cycle_tracker.start(self.current_fn.name.clone(), 0); } else { while let Some(name) = self.cycle_tracker.top() { if name == &self.current_fn.name { From 30e2e3f6198bf5ef9590f14ddade9b2305ab2bfc Mon Sep 17 00:00:00 2001 From: kunxian xia Date: Thu, 7 Aug 2025 11:19:01 +0800 Subject: [PATCH 20/32] set log_blowup=1 --- extensions/native/recursion/tests/recursion.rs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/extensions/native/recursion/tests/recursion.rs b/extensions/native/recursion/tests/recursion.rs index f8b440e2ae..8cb585d365 100644 --- a/extensions/native/recursion/tests/recursion.rs +++ b/extensions/native/recursion/tests/recursion.rs @@ -118,13 +118,14 @@ fn test_multi_observe() { let fri_params = if matches!(std::env::var("OPENVM_FAST_TEST"), Ok(x) if &x == "1") { FriParameters { - log_blowup: 3, + // max constraint degree = 2^log_blowup + 1 + log_blowup: 1, log_final_poly_len: 0, num_queries: 2, proof_of_work_bits: 0, } } else { - standard_fri_params_with_100_bits_conjectured_security(3) + standard_fri_params_with_100_bits_conjectured_security(1) }; let engine = BabyBearPoseidon2Engine::new(fri_params); @@ -157,4 +158,4 @@ fn build_test_program( builder.poseidon2_multi_observe(&challenger.sponge_state, challenger.input_ptr, &sample_input); } -} \ No newline at end of file +} From b3f2557595ce98682903d1182e2fe1983b119b38 Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Sun, 10 Aug 2025 16:42:19 -0400 Subject: [PATCH 21/32] Debug constraints --- extensions/native/circuit/src/extension.rs | 12 +- extensions/native/circuit/src/lib.rs | 2 - .../native/circuit/src/multi_observe/mod.rs | 102 +++++----- .../native/circuit/src/poseidon2/air.rs | 129 +++++++++++-- .../native/circuit/src/poseidon2/chip.rs | 175 +++++++++++++++++- .../native/circuit/src/poseidon2/columns.rs | 70 ++++++- .../native/circuit/src/poseidon2/trace.rs | 93 +++++++++- .../native/recursion/tests/recursion.rs | 2 + 8 files changed, 494 insertions(+), 91 deletions(-) diff --git a/extensions/native/circuit/src/extension.rs b/extensions/native/circuit/src/extension.rs index 68666ac872..1ee1af6885 100644 --- a/extensions/native/circuit/src/extension.rs +++ b/extensions/native/circuit/src/extension.rs @@ -31,7 +31,6 @@ use strum::IntoEnumIterator; use crate::{ adapters::{convert_adapter::ConvertAdapterChip, *}, poseidon2::chip::NativePoseidon2Chip, - multi_observe::NativeMultiObserveChip, phantom::*, *, }; @@ -77,7 +76,6 @@ pub enum NativeExecutor { FieldExtension(FieldExtensionChip), FriReducedOpening(FriReducedOpeningChip), VerifyBatch(NativePoseidon2Chip), - MultiObserve(NativeMultiObserveChip), } #[derive(From, ChipUsageGetter, Chip, AnyEnum)] @@ -205,18 +203,10 @@ impl VmExtension for Native { VerifyBatchOpcode::VERIFY_BATCH.global_opcode(), Poseidon2Opcode::PERM_POS2.global_opcode(), Poseidon2Opcode::COMP_POS2.global_opcode(), + Poseidon2Opcode::MULTI_OBSERVE.global_opcode(), ], )?; - let multi_observe_chip = NativeMultiObserveChip::new( - builder.system_port(), - offline_memory.clone(), - Poseidon2Config::default(), - ); - inventory.add_executor(multi_observe_chip, [ - Poseidon2Opcode::MULTI_OBSERVE.global_opcode(), - ])?; - builder.add_phantom_sub_executor( NativeHintInputSubEx, PhantomDiscriminant(NativePhantom::HintInput as u16), diff --git a/extensions/native/circuit/src/lib.rs b/extensions/native/circuit/src/lib.rs index 883c4d0834..46c6bc890f 100644 --- a/extensions/native/circuit/src/lib.rs +++ b/extensions/native/circuit/src/lib.rs @@ -8,7 +8,6 @@ mod fri; mod jal; mod loadstore; mod poseidon2; -mod multi_observe; pub use branch_eq::*; pub use castf::*; @@ -18,7 +17,6 @@ pub use fri::*; pub use jal::*; pub use loadstore::*; pub use poseidon2::*; -pub use multi_observe::*; mod extension; pub use extension::*; diff --git a/extensions/native/circuit/src/multi_observe/mod.rs b/extensions/native/circuit/src/multi_observe/mod.rs index 2de8e28a69..0faaf33819 100644 --- a/extensions/native/circuit/src/multi_observe/mod.rs +++ b/extensions/native/circuit/src/multi_observe/mod.rs @@ -137,58 +137,58 @@ impl Air for NativeMultiObserveAir { output_register, } = local; - self.execution_bridge - .execute_and_increment_pc( - AB::F::from_canonical_usize(MULTI_OBSERVE.global_opcode().as_usize()), - [ - output_register.into(), - input_register_1.into(), - input_register_2.into(), - self.address_space.into(), - self.address_space.into(), - input_register_3.into(), - ], - ExecutionState::new(pc, first_timestamp), - final_timestamp_increment, - ) - .eval(builder, is_first); - - // Memory operations - self.memory_bridge - .read( - MemoryAddress::new(self.address_space, output_register), - [state_ptr], - first_timestamp, - &read_state_ptr, - ) - .eval(builder, is_first); - - self.memory_bridge - .read( - MemoryAddress::new(self.address_space, input_register_2), - [input_ptr], - first_timestamp + AB::F::ONE, - &read_input_ptr, - ) - .eval(builder, is_first); - - self.memory_bridge - .read( - MemoryAddress::new(self.address_space, input_register_1), - [init_pos], - first_timestamp + AB::F::TWO, - &read_init_pos, - ) - .eval(builder, is_first); + // self.execution_bridge + // .execute_and_increment_pc( + // AB::F::from_canonical_usize(MULTI_OBSERVE.global_opcode().as_usize()), + // [ + // output_register.into(), + // input_register_1.into(), + // input_register_2.into(), + // self.address_space.into(), + // self.address_space.into(), + // input_register_3.into(), + // ], + // ExecutionState::new(pc, first_timestamp), + // final_timestamp_increment, + // ) + // .eval(builder, is_first); + + // // Memory operations + // self.memory_bridge + // .read( + // MemoryAddress::new(self.address_space, output_register), + // [state_ptr], + // first_timestamp, + // &read_state_ptr, + // ) + // .eval(builder, is_first); + + // self.memory_bridge + // .read( + // MemoryAddress::new(self.address_space, input_register_2), + // [input_ptr], + // first_timestamp + AB::F::ONE, + // &read_input_ptr, + // ) + // .eval(builder, is_first); + + // self.memory_bridge + // .read( + // MemoryAddress::new(self.address_space, input_register_1), + // [init_pos], + // first_timestamp + AB::F::TWO, + // &read_init_pos, + // ) + // .eval(builder, is_first); - self.memory_bridge - .read( - MemoryAddress::new(self.address_space, input_register_3), - [len], - first_timestamp + AB::F::from_canonical_usize(3), - &read_len, - ) - .eval(builder, is_first); + // self.memory_bridge + // .read( + // MemoryAddress::new(self.address_space, input_register_3), + // [len], + // first_timestamp + AB::F::from_canonical_usize(3), + // &read_len, + // ) + // .eval(builder, is_first); self.memory_bridge .read( diff --git a/extensions/native/circuit/src/poseidon2/air.rs b/extensions/native/circuit/src/poseidon2/air.rs index 50ecde3459..3c9f49f783 100644 --- a/extensions/native/circuit/src/poseidon2/air.rs +++ b/extensions/native/circuit/src/poseidon2/air.rs @@ -7,7 +7,7 @@ use openvm_circuit::{ use openvm_circuit_primitives::utils::not; use openvm_instructions::LocalOpcode; use openvm_native_compiler::{ - Poseidon2Opcode::{COMP_POS2, PERM_POS2}, + Poseidon2Opcode::{COMP_POS2, PERM_POS2, MULTI_OBSERVE}, VerifyBatchOpcode::VERIFY_BATCH, }; use openvm_poseidon2_air::{Poseidon2SubAir, BABY_BEAR_POSEIDON2_HALF_FULL_ROUNDS}; @@ -20,16 +20,13 @@ use openvm_stark_backend::{ rap::{BaseAirWithPublicValues, PartitionedBaseAir}, }; -use crate::{ - poseidon2::{ +use crate::poseidon2::{ chip::{NUM_INITIAL_READS, NUM_SIMPLE_ACCESSES}, columns::{ - InsideRowSpecificCols, NativePoseidon2Cols, SimplePoseidonSpecificCols, - TopLevelSpecificCols, + InsideRowSpecificCols, MultiObserveCols, NativePoseidon2Cols, SimplePoseidonSpecificCols, TopLevelSpecificCols }, CHUNK, - }, -}; + }; #[derive(Clone, Debug)] pub struct NativePoseidon2Air { @@ -72,6 +69,7 @@ impl Air incorporate_sibling, inside_row, simple, + multi_observe_row, end_inside_row, end_top_level, start_top_level, @@ -99,7 +97,8 @@ impl Air builder.assert_bool(incorporate_sibling); builder.assert_bool(inside_row); builder.assert_bool(simple); - let enabled = incorporate_row + incorporate_sibling + inside_row + simple; + builder.assert_bool(multi_observe_row); + let enabled = incorporate_row + incorporate_sibling + inside_row + simple + multi_observe_row; builder.assert_bool(enabled.clone()); builder.assert_bool(end_inside_row); builder.when(end_inside_row).assert_one(inside_row); @@ -117,14 +116,14 @@ impl Air builder.assert_eq(end.clone() * next.incorporate_row, next.start_top_level); // poseidon2 constraints are always checked - let mut sub_builder = - SubAirBuilder::, AB::F>::new( - builder, - 0..self.subair.width(), - ); - self.subair.eval(&mut sub_builder); + // let mut sub_builder = + // SubAirBuilder::, AB::F>::new( + // builder, + // 0..self.subair.width(), + // ); + // self.subair.eval(&mut sub_builder); - //// inside row constraints + // inside row constraints let inside_row_specific: &InsideRowSpecificCols = specific[..InsideRowSpecificCols::::width()].borrow(); @@ -680,6 +679,106 @@ impl Air &write_data_2, ) .eval(builder, simple * is_permute); + + // multi_observe contraints + let multi_observe_specific: &MultiObserveCols = + specific[..MultiObserveCols::::width()].borrow(); + // _debug + // inner: _, + // incorporate_row, + // incorporate_sibling, + // inside_row, + // simple, + // multi_observe_row, + // end_inside_row, + // end_top_level, + // start_top_level, + // very_first_timestamp, + // start_timestamp, + // opened_element_size_inv, + // initial_opened_index, + // opened_base_pointer, + // is_exhausted, + // specific, + let &MultiObserveCols { + pc, + final_timestamp_increment, + state_ptr, + input_ptr, + init_pos, + len, + is_first, + is_last, + start_idx, + end_idx, + aux_after_start, + aux_before_end, + read_data, + write_data, + data, + read_sponge_state, + write_sponge_state, + permutation_input, + permutation_output, + write_final_idx, + final_idx, + input_register_1, + input_register_2, + input_register_3, + output_register + } = multi_observe_specific; + + self.execution_bridge + .execute_and_increment_pc( + AB::F::from_canonical_usize(MULTI_OBSERVE.global_opcode().as_usize()), + [ + output_register.into(), + input_register_1.into(), + input_register_2.into(), + self.address_space.into(), + self.address_space.into(), + input_register_3.into(), + ], + ExecutionState::new(pc, very_first_timestamp), + final_timestamp_increment, + ) + .eval(builder, multi_observe_row * is_first); + + self.memory_bridge + .read( + MemoryAddress::new(self.address_space, output_register), + [state_ptr], + very_first_timestamp, + &read_data[0], + ) + .eval(builder, multi_observe_row * is_first); + + self.memory_bridge + .read( + MemoryAddress::new(self.address_space, input_register_2), + [input_ptr], + very_first_timestamp + AB::F::ONE, + &read_data[1], + ) + .eval(builder, multi_observe_row * is_first); + + self.memory_bridge + .read( + MemoryAddress::new(self.address_space, input_register_1), + [init_pos], + very_first_timestamp + AB::F::TWO, + &read_data[2], + ) + .eval(builder, multi_observe_row * is_first); + + self.memory_bridge + .read( + MemoryAddress::new(self.address_space, input_register_3), + [len], + very_first_timestamp + AB::F::from_canonical_usize(3), + &read_data[3], + ) + .eval(builder, multi_observe_row * is_first); } } diff --git a/extensions/native/circuit/src/poseidon2/chip.rs b/extensions/native/circuit/src/poseidon2/chip.rs index 426b089a9c..695c99083e 100644 --- a/extensions/native/circuit/src/poseidon2/chip.rs +++ b/extensions/native/circuit/src/poseidon2/chip.rs @@ -9,7 +9,7 @@ use openvm_circuit::{ use openvm_instructions::{instruction::Instruction, program::DEFAULT_PC_STEP, LocalOpcode}; use openvm_native_compiler::{ conversion::AS, - Poseidon2Opcode::{COMP_POS2, PERM_POS2}, + Poseidon2Opcode::{COMP_POS2, PERM_POS2, MULTI_OBSERVE}, VerifyBatchOpcode::VERIFY_BATCH, }; use openvm_poseidon2_air::{Poseidon2Config, Poseidon2SubAir, Poseidon2SubChip}; @@ -120,11 +120,53 @@ pub struct SimplePoseidonRecord { pub p2_input: [F; 2 * CHUNK], } +#[repr(C)] +#[derive(Debug, Clone, Serialize, Deserialize, Default)] +#[serde(bound = "F: Field")] +pub struct TranscriptObservationRecord { + pub from_state: ExecutionState, + pub instruction: Instruction, + pub start_idx: usize, + pub end_idx: usize, + pub is_first: bool, + pub is_last: bool, + pub curr_timestamp_increment: usize, + pub final_timestamp_increment: usize, + + // pub read_state_ptr: RecordId, + // pub read_input_ptr: RecordId, + pub state_ptr: F, + pub input_ptr: F, + + // pub read_init_pos: RecordId, + pub init_pos: F, + // pub read_len: RecordId, + pub len: usize, + + pub read_input_data: [RecordId; CHUNK], + pub write_input_data: [RecordId; CHUNK], + pub input_data: [F; CHUNK], + + pub read_sponge_state: RecordId, + pub write_sponge_state: RecordId, + pub permutation_input: [F; 2 * CHUNK], + pub permutation_output: [F; 2 * CHUNK], + + pub write_final_idx: RecordId, + pub final_idx: usize, + + pub input_register_1: F, + pub input_register_2: F, + pub input_register_3: F, + pub output_register: F, +} + #[derive(Debug, Clone, Serialize, Deserialize, Default)] #[serde(bound = "F: Field")] pub struct NativePoseidon2RecordSet { pub verify_batch_records: Vec>, pub simple_permute_records: Vec>, + pub transcript_observation_records: Vec>, } pub struct NativePoseidon2Chip { @@ -259,6 +301,133 @@ impl InstructionExecutor p2_input, }); self.height += 1; + } else if instruction.opcode == MULTI_OBSERVE.global_opcode() { + let mut observation_records: Vec> = vec![]; + + let &Instruction { + a: output_register, + b: input_register_1, + c: input_register_2, + d: data_address_space, + e: register_address_space, + f: input_register_3, + .. + } = instruction; + + let (read_sponge_ptr, sponge_ptr) = memory.read_cell(register_address_space, output_register); + let (read_arr_ptr, arr_ptr) = memory.read_cell(register_address_space, input_register_2); + let (read_init_pos, pos) = memory.read_cell(register_address_space, input_register_1); + let init_pos = pos.clone(); + let mut pos = pos.as_canonical_u32() as usize; + let (read_len, len) = memory.read_cell(register_address_space, input_register_3); + let mut len = len.as_canonical_u32() as usize; + + let mut header_record: TranscriptObservationRecord = TranscriptObservationRecord { + from_state, + instruction: instruction.clone(), + curr_timestamp_increment: 0, + is_first: true, + state_ptr: sponge_ptr, + input_ptr: arr_ptr, + init_pos, + len, + input_register_1, + input_register_2, + input_register_3, + output_register, + ..Default::default() + }; + header_record.read_input_data[0] = read_sponge_ptr; + header_record.read_input_data[1] = read_arr_ptr; + header_record.read_input_data[2] = read_init_pos; + header_record.read_input_data[3] = read_len; + + observation_records.push(header_record); + self.height += 1; + + // Observe bytes + let mut observation_chunks: Vec<(usize, usize, bool)> = vec![]; + while len > 0 { + if len >= (CHUNK - pos) { + observation_chunks.push((pos.clone(), CHUNK.clone(), true)); + pos = 0; + len -= CHUNK - pos; + } else { + observation_chunks.push((pos.clone(), pos + len, false)); + pos = pos + len; + len = 0; + } + } + + // _debug + println!("=> observation_chunks: {:?}", observation_chunks); + + let mut curr_timestamp = 4usize; + + /* _debug + let mut input_idx: usize = 0; + for chunk in observation_chunks { + let mut record: TranscriptObservationRecord = TranscriptObservationRecord { + from_state, + instruction: instruction.clone(), + + start_idx: chunk.0, + end_idx: chunk.1, + + curr_timestamp_increment: curr_timestamp, + state_ptr: sponge_ptr, + input_ptr: arr_ptr, + init_pos, + len, + input_register_1, + input_register_2, + input_register_3, + output_register, + ..Default::default() + }; + + for j in chunk.0..chunk.1 { + let (n_read, n_f) = memory.read_cell(data_address_space, arr_ptr + F::from_canonical_usize(input_idx)); + record.read_input_data[j] = n_read; + record.input_data[j] = n_f; + input_idx += 1; + curr_timestamp += 1; + + let (n_write, _) = memory.write_cell(data_address_space, sponge_ptr + F::from_canonical_usize(j), n_f); + record.write_input_data[j] = n_write; + curr_timestamp += 1; + } + + if record.end_idx >= CHUNK { + let (read_sponge_record, permutation_input) = memory.read::<{CHUNK * 2}>(data_address_space, sponge_ptr); + let output = self.subchip.permute(permutation_input); + let (write_sponge_record, _) = memory.write::<{CHUNK * 2}>(data_address_space, sponge_ptr, std::array::from_fn(|i| output[i])); + + curr_timestamp += 2; + + record.read_sponge_state = read_sponge_record; + record.write_sponge_state = write_sponge_record; + record.permutation_input = permutation_input; + record.permutation_output = output; + } + + observation_records.push(record); + self.height += 1; + } + + let last_record = observation_records.last_mut().unwrap(); + let (write_final, _) = memory.write_cell(register_address_space, input_register_1, F::from_canonical_usize(last_record.end_idx)); + curr_timestamp += 1; + last_record.is_last = true; + last_record.write_final_idx = write_final; + */ + + for record in &mut observation_records { + record.final_timestamp_increment = curr_timestamp; + } + for record in observation_records { + self.record_set.transcript_observation_records.push(record); + } } else if instruction.opcode == VERIFY_BATCH.global_opcode() { let &Instruction { a: dim_register, @@ -501,7 +670,9 @@ impl InstructionExecutor String::from("PERM_POS2") } else if opcode == COMP_POS2.global_opcode().as_usize() { String::from("COMP_POS2") - } else { + } else if opcode == MULTI_OBSERVE.global_opcode().as_usize() { + String::from("MULTI_OBSERVE") + }else { unreachable!("unsupported opcode: {}", opcode) } } diff --git a/extensions/native/circuit/src/poseidon2/columns.rs b/extensions/native/circuit/src/poseidon2/columns.rs index 6c47c23245..5b88e29d66 100644 --- a/extensions/native/circuit/src/poseidon2/columns.rs +++ b/extensions/native/circuit/src/poseidon2/columns.rs @@ -28,6 +28,8 @@ pub struct NativePoseidon2Cols { pub inside_row: T, /// Indicates that this row is a simple row. pub simple: T, + /// Indicates that this row is a multi_observe row. + pub multi_observe_row: T, /// Indicates the last row in an inside-row block. pub end_inside_row: T, @@ -60,15 +62,16 @@ pub struct NativePoseidon2Cols { /// indicates that cell `i + 1` inside a chunk is exhausted. pub is_exhausted: [T; CHUNK - 1], - pub specific: [T; max3( + pub specific: [T; max4( TopLevelSpecificCols::::width(), InsideRowSpecificCols::::width(), SimplePoseidonSpecificCols::::width(), + MultiObserveCols::::width(), )], } -const fn max3(a: usize, b: usize, c: usize) -> usize { - const_max(a, const_max(b, c)) +const fn max4(a: usize, b: usize, c: usize, d: usize) -> usize { + const_max(a, const_max(b, const_max(c, d))) } #[repr(C)] #[derive(AlignedBorrow)] @@ -200,3 +203,64 @@ pub struct SimplePoseidonSpecificCols { pub write_data_1: MemoryWriteAuxCols, pub write_data_2: MemoryWriteAuxCols, } + +#[repr(C)] +#[derive(AlignedBorrow, Copy, Clone)] +pub struct MultiObserveCols { + // Program states + pub pc: T, + pub final_timestamp_increment: T, + + // Initial reads from registers + pub state_ptr: T, + pub input_ptr: T, + pub init_pos: T, + pub len: T, + + pub is_first: T, + pub is_last: T, + pub start_idx: T, + pub end_idx: T, + pub aux_after_start: [T; CHUNK], + pub aux_before_end: [T; CHUNK], + + // Transcript observation + pub read_data: [MemoryReadAuxCols; CHUNK], + pub write_data: [MemoryWriteAuxCols; CHUNK], + pub data: [T; CHUNK], + + // Permutation + pub read_sponge_state: MemoryReadAuxCols, + pub write_sponge_state: MemoryWriteAuxCols, + pub permutation_input: [T; 2 * CHUNK], + pub permutation_output: [T; 2 * CHUNK], + + // Final write back and registers + pub write_final_idx: MemoryWriteAuxCols, + pub final_idx: T, + + pub input_register_1: T, + pub input_register_2: T, + pub input_register_3: T, + pub output_register: T, +} + +// _debug +// pub struct NativeMultiObserveCols { +// pub enable: T, +// pub is_first: T, +// pub is_final: T, +// pub is_observe: T, + +// pub pc: T, +// pub state_idx: T, +// pub remaining_len: T, +// pub counter: T, +// pub should_permute: T, + +// /// The initial timestamp of the instruction, which must be identical for first row +// /// and all following intermediate observation rows. +// pub first_timestamp: T, +// pub curr_timestamp: T, +// pub final_timestamp_increment: T, +// } diff --git a/extensions/native/circuit/src/poseidon2/trace.rs b/extensions/native/circuit/src/poseidon2/trace.rs index 76e9df018f..c39a38a9d7 100644 --- a/extensions/native/circuit/src/poseidon2/trace.rs +++ b/extensions/native/circuit/src/poseidon2/trace.rs @@ -15,18 +15,15 @@ use openvm_stark_backend::{ }; use crate::{ - poseidon2::{ + chip::TranscriptObservationRecord, poseidon2::{ chip::{ - SimplePoseidonRecord, NUM_INITIAL_READS, - CellRecord, IncorporateRowRecord, IncorporateSiblingRecord, InsideRowRecord, - NativePoseidon2Chip, VerifyBatchRecord, + CellRecord, IncorporateRowRecord, IncorporateSiblingRecord, InsideRowRecord, NativePoseidon2Chip, SimplePoseidonRecord, VerifyBatchRecord, NUM_INITIAL_READS }, columns::{ - InsideRowSpecificCols, NativePoseidon2Cols, SimplePoseidonSpecificCols, - TopLevelSpecificCols, + InsideRowSpecificCols, MultiObserveCols, NativePoseidon2Cols, SimplePoseidonSpecificCols, TopLevelSpecificCols }, CHUNK, - }, + } }; impl ChipUsageGetter for NativePoseidon2Chip @@ -432,6 +429,76 @@ impl NativePoseidon2Chip, + aux_cols_factory: &MemoryAuxColsFactory, + slice: &mut [F], + memory: &OfflineMemory, + ) { + let cols: &mut NativePoseidon2Cols = slice.borrow_mut(); + cols.very_first_timestamp = F::from_canonical_u32(record.from_state.timestamp); + cols.start_timestamp = F::from_canonical_usize(record.from_state.timestamp as usize + record.curr_timestamp_increment); + cols.multi_observe_row = F::ONE; + + let specific: &mut MultiObserveCols = + cols.specific[..MultiObserveCols::::width()].borrow_mut(); + + specific.pc = F::from_canonical_u32(record.from_state.pc); + specific.is_first = if record.is_first { F::ONE } else { F::ZERO }; + specific.is_last = if record.is_last { F::ONE } else { F::ZERO }; + specific.final_timestamp_increment = F::from_canonical_usize(record.final_timestamp_increment); + specific.state_ptr = record.state_ptr; + specific.input_ptr = record.input_ptr; + specific.init_pos = record.init_pos; + specific.len = F::from_canonical_usize(record.len); + + if record.is_first { + let read_state_ptr_record = memory.record_by_id(record.read_input_data[0]); + let read_input_ptr_record = memory.record_by_id(record.read_input_data[1]); + let read_init_pos_record = memory.record_by_id(record.read_input_data[2]); + let read_len_record = memory.record_by_id(record.read_input_data[3]); + aux_cols_factory.generate_read_aux(read_state_ptr_record, &mut specific.read_data[0]); + aux_cols_factory.generate_read_aux(read_input_ptr_record, &mut specific.read_data[1]); + aux_cols_factory.generate_read_aux(read_init_pos_record, &mut specific.read_data[2]); + aux_cols_factory.generate_read_aux(read_len_record, &mut specific.read_data[3]); + } else { + for i in record.start_idx..CHUNK { + specific.aux_after_start[i] = F::ONE; + } + for i in 0..record.end_idx { + specific.aux_before_end[i] = F::ONE; + } + for i in record.start_idx..record.end_idx { + let read_data_record = memory.record_by_id(record.read_input_data[i]); + let write_data_record = memory.record_by_id(record.write_input_data[i]); + aux_cols_factory.generate_read_aux(read_data_record, &mut specific.read_data[i]); + aux_cols_factory.generate_write_aux(write_data_record, &mut specific.write_data[i]); + specific.data[i] = record.input_data[i]; + } + + if record.end_idx >= CHUNK { + let read_sponge_record = memory.record_by_id(record.read_sponge_state); + let write_sponge_record = memory.record_by_id(record.write_sponge_state); + aux_cols_factory.generate_read_aux(read_sponge_record, &mut specific.read_sponge_state); + aux_cols_factory.generate_write_aux(write_sponge_record, &mut specific.write_sponge_state); + specific.permutation_input = record.permutation_input; + specific.permutation_output = record.permutation_output; + } + } + + if record.is_last { + specific.final_idx = F::from_canonical_usize(record.final_idx); + let write_final_idx_record = memory.record_by_id(record.write_final_idx); + aux_cols_factory.generate_write_aux(write_final_idx_record, &mut specific.write_final_idx); + } + + specific.input_register_1 = record.input_register_1; + specific.input_register_2 = record.input_register_2; + specific.input_register_3 = record.input_register_3; + specific.output_register = record.output_register; + } + fn generate_trace(self) -> RowMajorMatrix { let width = self.trace_width(); let height = next_power_of_two_or_zero(self.height); @@ -459,6 +526,18 @@ impl NativePoseidon2Chip record: {:?}", record); + + self.multi_observe_record_to_row( + record, + &aux_cols_factory, + &mut flat_trace[used_cells..used_cells + width], + &memory, + ); + used_cells += width; + } // poseidon2 constraints are always checked // following can be optimized to only hash [0; _] once flat_trace[used_cells..] diff --git a/extensions/native/recursion/tests/recursion.rs b/extensions/native/recursion/tests/recursion.rs index 8cb585d365..ce5b761061 100644 --- a/extensions/native/recursion/tests/recursion.rs +++ b/extensions/native/recursion/tests/recursion.rs @@ -119,12 +119,14 @@ fn test_multi_observe() { let fri_params = if matches!(std::env::var("OPENVM_FAST_TEST"), Ok(x) if &x == "1") { FriParameters { // max constraint degree = 2^log_blowup + 1 + // _debug log_blowup: 1, log_final_poly_len: 0, num_queries: 2, proof_of_work_bits: 0, } } else { + // _debug standard_fri_params_with_100_bits_conjectured_security(1) }; From ab395c9a8236325fd36f8102a255d328ee9b7d7a Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Sun, 10 Aug 2025 17:16:08 -0400 Subject: [PATCH 22/32] Debug constraints --- .../native/circuit/src/poseidon2/air.rs | 28 ++++++++++++++-- .../native/circuit/src/poseidon2/chip.rs | 25 ++++++++------- .../native/circuit/src/poseidon2/columns.rs | 1 + .../native/circuit/src/poseidon2/trace.rs | 32 +++++++++++-------- .../native/recursion/tests/recursion.rs | 2 -- 5 files changed, 58 insertions(+), 30 deletions(-) diff --git a/extensions/native/circuit/src/poseidon2/air.rs b/extensions/native/circuit/src/poseidon2/air.rs index 3c9f49f783..f879ab15af 100644 --- a/extensions/native/circuit/src/poseidon2/air.rs +++ b/extensions/native/circuit/src/poseidon2/air.rs @@ -2,7 +2,7 @@ use std::{array::from_fn, borrow::Borrow, sync::Arc}; use openvm_circuit::{ arch::{ExecutionBridge, ExecutionState}, - system::memory::{offline_checker::MemoryBridge, MemoryAddress}, + system::memory::{offline_checker::MemoryBridge, MemoryAddress, CHUNK}, }; use openvm_circuit_primitives::utils::not; use openvm_instructions::LocalOpcode; @@ -25,7 +25,6 @@ use crate::poseidon2::{ columns::{ InsideRowSpecificCols, MultiObserveCols, NativePoseidon2Cols, SimplePoseidonSpecificCols, TopLevelSpecificCols }, - CHUNK, }; #[derive(Clone, Debug)] @@ -709,6 +708,7 @@ impl Air len, is_first, is_last, + curr_len, start_idx, end_idx, aux_after_start, @@ -779,6 +779,30 @@ impl Air &read_data[3], ) .eval(builder, multi_observe_row * is_first); + + for i in 0..CHUNK { + let i_var = AB::F::from_canonical_usize(i); + self.memory_bridge + .read( + MemoryAddress::new(self.address_space, input_ptr + curr_len + i_var - start_idx), + [data[i]], + start_timestamp + i_var * AB::F::TWO - start_idx * AB::F::TWO, + &read_data[i] + ) + .eval(builder, aux_after_start[i] * aux_before_end[i]); + + self.memory_bridge + .write( + MemoryAddress::new( + self.address_space, + state_ptr + i_var, + ), + [data[i]], + start_timestamp + i_var * AB::F::TWO - start_idx * AB::F::TWO + AB::F::ONE, + &write_data[i], + ) + .eval(builder, aux_after_start[i] * aux_before_end[i]); + } } } diff --git a/extensions/native/circuit/src/poseidon2/chip.rs b/extensions/native/circuit/src/poseidon2/chip.rs index 695c99083e..41063df42d 100644 --- a/extensions/native/circuit/src/poseidon2/chip.rs +++ b/extensions/native/circuit/src/poseidon2/chip.rs @@ -142,6 +142,7 @@ pub struct TranscriptObservationRecord { pub init_pos: F, // pub read_len: RecordId, pub len: usize, + pub curr_len: usize, pub read_input_data: [RecordId; CHUNK], pub write_input_data: [RecordId; CHUNK], @@ -363,8 +364,6 @@ impl InstructionExecutor println!("=> observation_chunks: {:?}", observation_chunks); let mut curr_timestamp = 4usize; - - /* _debug let mut input_idx: usize = 0; for chunk in observation_chunks { let mut record: TranscriptObservationRecord = TranscriptObservationRecord { @@ -379,6 +378,7 @@ impl InstructionExecutor input_ptr: arr_ptr, init_pos, len, + curr_len: input_idx, input_register_1, input_register_2, input_register_3, @@ -398,22 +398,23 @@ impl InstructionExecutor curr_timestamp += 1; } - if record.end_idx >= CHUNK { - let (read_sponge_record, permutation_input) = memory.read::<{CHUNK * 2}>(data_address_space, sponge_ptr); - let output = self.subchip.permute(permutation_input); - let (write_sponge_record, _) = memory.write::<{CHUNK * 2}>(data_address_space, sponge_ptr, std::array::from_fn(|i| output[i])); + // if record.end_idx >= CHUNK { + // let (read_sponge_record, permutation_input) = memory.read::<{CHUNK * 2}>(data_address_space, sponge_ptr); + // let output = self.subchip.permute(permutation_input); + // let (write_sponge_record, _) = memory.write::<{CHUNK * 2}>(data_address_space, sponge_ptr, std::array::from_fn(|i| output[i])); - curr_timestamp += 2; + // curr_timestamp += 2; - record.read_sponge_state = read_sponge_record; - record.write_sponge_state = write_sponge_record; - record.permutation_input = permutation_input; - record.permutation_output = output; - } + // record.read_sponge_state = read_sponge_record; + // record.write_sponge_state = write_sponge_record; + // record.permutation_input = permutation_input; + // record.permutation_output = output; + // } observation_records.push(record); self.height += 1; } + /* _debug let last_record = observation_records.last_mut().unwrap(); let (write_final, _) = memory.write_cell(register_address_space, input_register_1, F::from_canonical_usize(last_record.end_idx)); diff --git a/extensions/native/circuit/src/poseidon2/columns.rs b/extensions/native/circuit/src/poseidon2/columns.rs index 5b88e29d66..f29890d3f7 100644 --- a/extensions/native/circuit/src/poseidon2/columns.rs +++ b/extensions/native/circuit/src/poseidon2/columns.rs @@ -219,6 +219,7 @@ pub struct MultiObserveCols { pub is_first: T, pub is_last: T, + pub curr_len: T, pub start_idx: T, pub end_idx: T, pub aux_after_start: [T; CHUNK], diff --git a/extensions/native/circuit/src/poseidon2/trace.rs b/extensions/native/circuit/src/poseidon2/trace.rs index c39a38a9d7..ce4600b8a9 100644 --- a/extensions/native/circuit/src/poseidon2/trace.rs +++ b/extensions/native/circuit/src/poseidon2/trace.rs @@ -452,6 +452,7 @@ impl NativePoseidon2Chip NativePoseidon2Chip NativePoseidon2Chip= CHUNK { - let read_sponge_record = memory.record_by_id(record.read_sponge_state); - let write_sponge_record = memory.record_by_id(record.write_sponge_state); - aux_cols_factory.generate_read_aux(read_sponge_record, &mut specific.read_sponge_state); - aux_cols_factory.generate_write_aux(write_sponge_record, &mut specific.write_sponge_state); - specific.permutation_input = record.permutation_input; - specific.permutation_output = record.permutation_output; - } + // if record.end_idx >= CHUNK { + // let read_sponge_record = memory.record_by_id(record.read_sponge_state); + // let write_sponge_record = memory.record_by_id(record.write_sponge_state); + // aux_cols_factory.generate_read_aux(read_sponge_record, &mut specific.read_sponge_state); + // aux_cols_factory.generate_write_aux(write_sponge_record, &mut specific.write_sponge_state); + // specific.permutation_input = record.permutation_input; + // specific.permutation_output = record.permutation_output; + // } } - if record.is_last { - specific.final_idx = F::from_canonical_usize(record.final_idx); - let write_final_idx_record = memory.record_by_id(record.write_final_idx); - aux_cols_factory.generate_write_aux(write_final_idx_record, &mut specific.write_final_idx); - } + // if record.is_last { + // specific.final_idx = F::from_canonical_usize(record.final_idx); + // let write_final_idx_record = memory.record_by_id(record.write_final_idx); + // aux_cols_factory.generate_write_aux(write_final_idx_record, &mut specific.write_final_idx); + // } specific.input_register_1 = record.input_register_1; specific.input_register_2 = record.input_register_2; diff --git a/extensions/native/recursion/tests/recursion.rs b/extensions/native/recursion/tests/recursion.rs index ce5b761061..8cb585d365 100644 --- a/extensions/native/recursion/tests/recursion.rs +++ b/extensions/native/recursion/tests/recursion.rs @@ -119,14 +119,12 @@ fn test_multi_observe() { let fri_params = if matches!(std::env::var("OPENVM_FAST_TEST"), Ok(x) if &x == "1") { FriParameters { // max constraint degree = 2^log_blowup + 1 - // _debug log_blowup: 1, log_final_poly_len: 0, num_queries: 2, proof_of_work_bits: 0, } } else { - // _debug standard_fri_params_with_100_bits_conjectured_security(1) }; From e48121a6e44e60e339f14b16472c3fd8b441715e Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Sun, 10 Aug 2025 18:49:17 -0400 Subject: [PATCH 23/32] Debug constraints --- .../native/circuit/src/multi_observe/mod.rs | 82 +++++++++---------- .../native/circuit/src/poseidon2/air.rs | 65 +++++++++++++++ .../native/circuit/src/poseidon2/chip.rs | 29 +++---- .../native/circuit/src/poseidon2/columns.rs | 1 + .../native/circuit/src/poseidon2/trace.rs | 20 +++-- 5 files changed, 131 insertions(+), 66 deletions(-) diff --git a/extensions/native/circuit/src/multi_observe/mod.rs b/extensions/native/circuit/src/multi_observe/mod.rs index 0faaf33819..51833cec7f 100644 --- a/extensions/native/circuit/src/multi_observe/mod.rs +++ b/extensions/native/circuit/src/multi_observe/mod.rs @@ -190,50 +190,50 @@ impl Air for NativeMultiObserveAir { // ) // .eval(builder, is_first); - self.memory_bridge - .read( - MemoryAddress::new(self.address_space, input_ptr + counter - AB::F::ONE), - [data], - first_timestamp + curr_timestamp, - &read_data - ) - .eval(builder, is_observe); + // self.memory_bridge + // .read( + // MemoryAddress::new(self.address_space, input_ptr + counter - AB::F::ONE), + // [data], + // first_timestamp + curr_timestamp, + // &read_data + // ) + // .eval(builder, is_observe); - self.memory_bridge - .write( - MemoryAddress::new( - self.address_space, - state_ptr + state_idx, - ), - [data], - first_timestamp + curr_timestamp + AB::F::ONE, - &write_data, - ) - .eval(builder, is_observe); + // self.memory_bridge + // .write( + // MemoryAddress::new( + // self.address_space, + // state_ptr + state_idx, + // ), + // [data], + // first_timestamp + curr_timestamp + AB::F::ONE, + // &write_data, + // ) + // .eval(builder, is_observe); - self.memory_bridge - .read( - MemoryAddress::new( - self.address_space, - state_ptr, - ), - permutation_input, - first_timestamp + curr_timestamp + AB::F::TWO, - &read_sponge_state, - ) - .eval(builder, should_permute); + // self.memory_bridge + // .read( + // MemoryAddress::new( + // self.address_space, + // state_ptr, + // ), + // permutation_input, + // first_timestamp + curr_timestamp + AB::F::TWO, + // &read_sponge_state, + // ) + // .eval(builder, should_permute); - self.memory_bridge - .write( - MemoryAddress::new( - self.address_space, - state_ptr - ), - permutation_output, - first_timestamp + curr_timestamp + AB::F::from_canonical_usize(3), - &write_sponge_state, - ) - .eval(builder, should_permute); + // self.memory_bridge + // .write( + // MemoryAddress::new( + // self.address_space, + // state_ptr + // ), + // permutation_output, + // first_timestamp + curr_timestamp + AB::F::from_canonical_usize(3), + // &write_sponge_state, + // ) + // .eval(builder, should_permute); self.memory_bridge .write( diff --git a/extensions/native/circuit/src/poseidon2/air.rs b/extensions/native/circuit/src/poseidon2/air.rs index f879ab15af..2c17736aa9 100644 --- a/extensions/native/circuit/src/poseidon2/air.rs +++ b/extensions/native/circuit/src/poseidon2/air.rs @@ -716,6 +716,7 @@ impl Air read_data, write_data, data, + should_permute, read_sponge_state, write_sponge_state, permutation_input, @@ -803,6 +804,70 @@ impl Air ) .eval(builder, aux_after_start[i] * aux_before_end[i]); } + + for i in 0..(CHUNK - 1) { + builder + .when(aux_after_start[i]) + .assert_one(aux_after_start[i + 1]); + } + + for i in 1..CHUNK { + builder + .when(aux_before_end[i]) + .assert_one(aux_before_end[i - 1]); + } + + builder + .when(multi_observe_row * (AB::Expr::ONE - is_first)) + .assert_eq( + aux_after_start[0] + + aux_after_start[1] + + aux_after_start[2] + + aux_after_start[3] + + aux_after_start[4] + + aux_after_start[5] + + aux_after_start[6] + + aux_after_start[7], + AB::Expr::from_canonical_usize(CHUNK) - start_idx.into() + ); + + builder + .when(multi_observe_row * (AB::Expr::ONE - is_first)) + .assert_eq( + aux_before_end[0] + + aux_before_end[1] + + aux_before_end[2] + + aux_before_end[3] + + aux_before_end[4] + + aux_before_end[5] + + aux_before_end[6] + + aux_before_end[7], + end_idx + ); + + self.memory_bridge + .read( + MemoryAddress::new( + self.address_space, + state_ptr, + ), + permutation_input, + start_timestamp + end_idx * AB::F::TWO - start_idx * AB::F::TWO, + &read_sponge_state, + ) + .eval(builder, multi_observe_row * should_permute); + + self.memory_bridge + .write( + MemoryAddress::new( + self.address_space, + state_ptr + ), + permutation_output, + start_timestamp + end_idx * AB::F::TWO - start_idx * AB::F::TWO + AB::F::ONE, + &write_sponge_state, + ) + .eval(builder, multi_observe_row * should_permute); } } diff --git a/extensions/native/circuit/src/poseidon2/chip.rs b/extensions/native/circuit/src/poseidon2/chip.rs index 41063df42d..0e8cd9e1bc 100644 --- a/extensions/native/circuit/src/poseidon2/chip.rs +++ b/extensions/native/circuit/src/poseidon2/chip.rs @@ -132,17 +132,13 @@ pub struct TranscriptObservationRecord { pub is_last: bool, pub curr_timestamp_increment: usize, pub final_timestamp_increment: usize, - - // pub read_state_ptr: RecordId, - // pub read_input_ptr: RecordId, + pub state_ptr: F, pub input_ptr: F, - - // pub read_init_pos: RecordId, pub init_pos: F, - // pub read_len: RecordId, pub len: usize, pub curr_len: usize, + pub should_permute: bool, pub read_input_data: [RecordId; CHUNK], pub write_input_data: [RecordId; CHUNK], @@ -398,18 +394,19 @@ impl InstructionExecutor curr_timestamp += 1; } - // if record.end_idx >= CHUNK { - // let (read_sponge_record, permutation_input) = memory.read::<{CHUNK * 2}>(data_address_space, sponge_ptr); - // let output = self.subchip.permute(permutation_input); - // let (write_sponge_record, _) = memory.write::<{CHUNK * 2}>(data_address_space, sponge_ptr, std::array::from_fn(|i| output[i])); + if record.end_idx >= CHUNK { + let (read_sponge_record, permutation_input) = memory.read::<{CHUNK * 2}>(data_address_space, sponge_ptr); + let output = self.subchip.permute(permutation_input); + let (write_sponge_record, _) = memory.write::<{CHUNK * 2}>(data_address_space, sponge_ptr, std::array::from_fn(|i| output[i])); - // curr_timestamp += 2; + curr_timestamp += 2; - // record.read_sponge_state = read_sponge_record; - // record.write_sponge_state = write_sponge_record; - // record.permutation_input = permutation_input; - // record.permutation_output = output; - // } + record.should_permute = true; + record.read_sponge_state = read_sponge_record; + record.write_sponge_state = write_sponge_record; + record.permutation_input = permutation_input; + record.permutation_output = output; + } observation_records.push(record); self.height += 1; diff --git a/extensions/native/circuit/src/poseidon2/columns.rs b/extensions/native/circuit/src/poseidon2/columns.rs index f29890d3f7..e768c35d0f 100644 --- a/extensions/native/circuit/src/poseidon2/columns.rs +++ b/extensions/native/circuit/src/poseidon2/columns.rs @@ -231,6 +231,7 @@ pub struct MultiObserveCols { pub data: [T; CHUNK], // Permutation + pub should_permute: T, pub read_sponge_state: MemoryReadAuxCols, pub write_sponge_state: MemoryWriteAuxCols, pub permutation_input: [T; 2 * CHUNK], diff --git a/extensions/native/circuit/src/poseidon2/trace.rs b/extensions/native/circuit/src/poseidon2/trace.rs index ce4600b8a9..98eb5728b7 100644 --- a/extensions/native/circuit/src/poseidon2/trace.rs +++ b/extensions/native/circuit/src/poseidon2/trace.rs @@ -470,6 +470,8 @@ impl NativePoseidon2Chip specific.aux_after_start - {:?}", specific.aux_after_start); for i in 0..record.end_idx { specific.aux_before_end[i] = F::ONE; } @@ -480,15 +482,15 @@ impl NativePoseidon2Chip= CHUNK { - // let read_sponge_record = memory.record_by_id(record.read_sponge_state); - // let write_sponge_record = memory.record_by_id(record.write_sponge_state); - // aux_cols_factory.generate_read_aux(read_sponge_record, &mut specific.read_sponge_state); - // aux_cols_factory.generate_write_aux(write_sponge_record, &mut specific.write_sponge_state); - // specific.permutation_input = record.permutation_input; - // specific.permutation_output = record.permutation_output; - // } + if record.should_permute { + let read_sponge_record = memory.record_by_id(record.read_sponge_state); + let write_sponge_record = memory.record_by_id(record.write_sponge_state); + aux_cols_factory.generate_read_aux(read_sponge_record, &mut specific.read_sponge_state); + aux_cols_factory.generate_write_aux(write_sponge_record, &mut specific.write_sponge_state); + specific.should_permute = F::ONE; + specific.permutation_input = record.permutation_input; + specific.permutation_output = record.permutation_output; + } } // if record.is_last { From a04ac451c52307d1335c1b7760ee98efbefa4499 Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Sun, 10 Aug 2025 19:23:18 -0400 Subject: [PATCH 24/32] Debug constraints --- .../native/circuit/src/multi_observe/mod.rs | 22 +++++++------- .../native/circuit/src/poseidon2/air.rs | 29 ++++++++----------- .../native/circuit/src/poseidon2/chip.rs | 10 +++---- .../native/circuit/src/poseidon2/trace.rs | 16 +++++----- .../native/recursion/tests/recursion.rs | 19 ++++++++++-- 5 files changed, 52 insertions(+), 44 deletions(-) diff --git a/extensions/native/circuit/src/multi_observe/mod.rs b/extensions/native/circuit/src/multi_observe/mod.rs index 51833cec7f..f3988f08c1 100644 --- a/extensions/native/circuit/src/multi_observe/mod.rs +++ b/extensions/native/circuit/src/multi_observe/mod.rs @@ -235,17 +235,17 @@ impl Air for NativeMultiObserveAir { // ) // .eval(builder, should_permute); - self.memory_bridge - .write( - MemoryAddress::new( - self.address_space, - input_register_1, - ), - [final_idx], - first_timestamp + curr_timestamp + is_first * AB::F::from_canonical_usize(4) + is_observe * AB::F::TWO + should_permute * AB::F::TWO, - &write_final_idx - ) - .eval(builder, is_final); + // self.memory_bridge + // .write( + // MemoryAddress::new( + // self.address_space, + // input_register_1, + // ), + // [final_idx], + // first_timestamp + curr_timestamp + is_first * AB::F::from_canonical_usize(4) + is_observe * AB::F::TWO + should_permute * AB::F::TWO, + // &write_final_idx + // ) + // .eval(builder, is_final); // Binary indicators columns builder.assert_bool(enable); diff --git a/extensions/native/circuit/src/poseidon2/air.rs b/extensions/native/circuit/src/poseidon2/air.rs index 2c17736aa9..434051d31b 100644 --- a/extensions/native/circuit/src/poseidon2/air.rs +++ b/extensions/native/circuit/src/poseidon2/air.rs @@ -682,23 +682,6 @@ impl Air // multi_observe contraints let multi_observe_specific: &MultiObserveCols = specific[..MultiObserveCols::::width()].borrow(); - // _debug - // inner: _, - // incorporate_row, - // incorporate_sibling, - // inside_row, - // simple, - // multi_observe_row, - // end_inside_row, - // end_top_level, - // start_top_level, - // very_first_timestamp, - // start_timestamp, - // opened_element_size_inv, - // initial_opened_index, - // opened_base_pointer, - // is_exhausted, - // specific, let &MultiObserveCols { pc, final_timestamp_increment, @@ -868,6 +851,18 @@ impl Air &write_sponge_state, ) .eval(builder, multi_observe_row * should_permute); + + self.memory_bridge + .write( + MemoryAddress::new( + self.address_space, + input_register_1, + ), + [final_idx], + start_timestamp + is_first * AB::F::from_canonical_usize(4) + (end_idx - start_idx) * AB::F::TWO + should_permute * AB::F::TWO, + &write_final_idx + ) + .eval(builder, multi_observe_row * is_last); } } diff --git a/extensions/native/circuit/src/poseidon2/chip.rs b/extensions/native/circuit/src/poseidon2/chip.rs index 0e8cd9e1bc..ab61f24260 100644 --- a/extensions/native/circuit/src/poseidon2/chip.rs +++ b/extensions/native/circuit/src/poseidon2/chip.rs @@ -132,7 +132,7 @@ pub struct TranscriptObservationRecord { pub is_last: bool, pub curr_timestamp_increment: usize, pub final_timestamp_increment: usize, - + pub state_ptr: F, pub input_ptr: F, pub init_pos: F, @@ -411,14 +411,14 @@ impl InstructionExecutor observation_records.push(record); self.height += 1; } - /* _debug let last_record = observation_records.last_mut().unwrap(); - let (write_final, _) = memory.write_cell(register_address_space, input_register_1, F::from_canonical_usize(last_record.end_idx)); - curr_timestamp += 1; + let final_idx = last_record.end_idx % CHUNK; + let (write_final, _) = memory.write_cell(register_address_space, input_register_1, F::from_canonical_usize(final_idx)); last_record.is_last = true; last_record.write_final_idx = write_final; - */ + last_record.final_idx = final_idx; + curr_timestamp += 1; for record in &mut observation_records { record.final_timestamp_increment = curr_timestamp; diff --git a/extensions/native/circuit/src/poseidon2/trace.rs b/extensions/native/circuit/src/poseidon2/trace.rs index 98eb5728b7..b113dd9029 100644 --- a/extensions/native/circuit/src/poseidon2/trace.rs +++ b/extensions/native/circuit/src/poseidon2/trace.rs @@ -445,8 +445,6 @@ impl NativePoseidon2Chip::width()].borrow_mut(); specific.pc = F::from_canonical_u32(record.from_state.pc); - specific.is_first = if record.is_first { F::ONE } else { F::ZERO }; - specific.is_last = if record.is_last { F::ONE } else { F::ZERO }; specific.final_timestamp_increment = F::from_canonical_usize(record.final_timestamp_increment); specific.state_ptr = record.state_ptr; specific.input_ptr = record.input_ptr; @@ -455,6 +453,7 @@ impl NativePoseidon2Chip NativePoseidon2Chip specific.aux_after_start - {:?}", specific.aux_after_start); for i in 0..record.end_idx { specific.aux_before_end[i] = F::ONE; } @@ -493,11 +490,12 @@ impl NativePoseidon2Chip( builder: &mut Builder, ) { - let sample_lens: Vec = vec![0, 10, 20]; + let sample_lens: Vec = vec![0, 1, 2, 3]; + // let sample_lens: Vec = vec![0, 10, 20]; + let mut rng = create_seeded_rng(); let challenger = DuplexChallengerVariable::new(builder); @@ -156,6 +158,19 @@ fn build_test_program( builder.set(&sample_input, idx_vec[0], C::F::from_canonical_u32(f_u32)); }); - builder.poseidon2_multi_observe(&challenger.sponge_state, challenger.input_ptr, &sample_input); + let next_input_ptr = builder.poseidon2_multi_observe(&challenger.sponge_state, challenger.input_ptr, &sample_input); + + builder.assign( + &challenger.input_ptr, + challenger.io_empty_ptr + next_input_ptr.clone(), + ); + builder.if_ne(next_input_ptr, Usize::from(0)).then_or_else( + |builder| { + builder.assign(&challenger.output_ptr, challenger.io_empty_ptr); + }, + |builder| { + builder.assign(&challenger.output_ptr, challenger.io_full_ptr); + }, + ); } } From 694fb2fcccd28ee44f6cf34d59f25ea5ca5614cb Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Sun, 10 Aug 2025 20:31:32 -0400 Subject: [PATCH 25/32] Remove standalone chip --- .../native/circuit/src/multi_observe/mod.rs | 694 ------------------ .../native/circuit/src/poseidon2/air.rs | 52 ++ .../native/circuit/src/poseidon2/chip.rs | 8 +- .../native/circuit/src/poseidon2/trace.rs | 3 - 4 files changed, 55 insertions(+), 702 deletions(-) delete mode 100644 extensions/native/circuit/src/multi_observe/mod.rs diff --git a/extensions/native/circuit/src/multi_observe/mod.rs b/extensions/native/circuit/src/multi_observe/mod.rs deleted file mode 100644 index f3988f08c1..0000000000 --- a/extensions/native/circuit/src/multi_observe/mod.rs +++ /dev/null @@ -1,694 +0,0 @@ -use std::{borrow::{Borrow, BorrowMut}, sync::{Arc, Mutex}}; -use openvm_circuit::system::memory::offline_checker::{MemoryReadAuxCols, MemoryWriteAuxCols}; -use openvm_circuit_primitives_derive::AlignedBorrow; -use openvm_poseidon2_air::Poseidon2SubChip; -use openvm_circuit::{ - arch::{ExecutionBridge, ExecutionState, ExecutionError, InstructionExecutor, SystemPort}, - system::memory::{offline_checker::MemoryBridge, MemoryAddress, MemoryController, OfflineMemory, RecordId}, -}; -use openvm_circuit_primitives::utils::not; -use openvm_instructions::{instruction::Instruction, program::DEFAULT_PC_STEP, LocalOpcode}; -use openvm_native_compiler::{ - conversion::AS, - Poseidon2Opcode::MULTI_OBSERVE -}; -use openvm_poseidon2_air::Poseidon2Config; -use openvm_stark_backend::{ - interaction::InteractionBuilder, - p3_air::{Air, AirBuilder, BaseAir}, - p3_field::{Field, FieldAlgebra, PrimeField32}, - p3_matrix::Matrix, - rap::{BaseAirWithPublicValues, PartitionedBaseAir} -}; -use serde::{Deserialize, Serialize}; -use openvm_circuit::system::memory::{MemoryAuxColsFactory}; -use openvm_circuit_primitives::utils::next_power_of_two_or_zero; -use openvm_stark_backend::{ - config::{StarkGenericConfig, Val}, - p3_matrix::dense::RowMajorMatrix, - prover::types::AirProofInput, - AirRef, Chip, ChipUsageGetter, -}; -const CHUNK: usize = 8; - -#[repr(C)] -#[derive(AlignedBorrow)] -pub struct NativeMultiObserveCols { - pub enable: T, - pub is_first: T, - pub is_final: T, - pub is_observe: T, - - pub pc: T, - pub state_idx: T, - pub remaining_len: T, - pub counter: T, - pub should_permute: T, - - /// The initial timestamp of the instruction, which must be identical for first row - /// and all following intermediate observation rows. - pub first_timestamp: T, - pub curr_timestamp: T, - pub final_timestamp_increment: T, - - pub read_state_ptr: MemoryReadAuxCols, - pub read_input_ptr: MemoryReadAuxCols, - pub state_ptr: T, - pub input_ptr: T, - - pub read_init_pos: MemoryReadAuxCols, - pub read_len: MemoryReadAuxCols, - pub init_pos: T, - pub len: T, - - pub read_data: MemoryReadAuxCols, - pub write_data: MemoryWriteAuxCols, - pub data: T, - - pub read_sponge_state: MemoryReadAuxCols, - pub write_sponge_state: MemoryWriteAuxCols, - pub permutation_input: [T; 2 * CHUNK], - pub permutation_output: [T; 2 * CHUNK], - - pub write_final_idx: MemoryWriteAuxCols, - pub final_idx: T, - - pub input_register_1: T, - pub input_register_2: T, - pub input_register_3: T, - pub output_register: T, -} - -#[derive(Clone, Debug)] -pub struct NativeMultiObserveAir { - pub execution_bridge: ExecutionBridge, - pub memory_bridge: MemoryBridge, - pub(crate) address_space: F, -} -impl BaseAir for NativeMultiObserveAir { - fn width(&self) -> usize { - NativeMultiObserveCols::::width() - } -} -impl BaseAirWithPublicValues for NativeMultiObserveAir {} -impl PartitionedBaseAir for NativeMultiObserveAir {} - -impl Air for NativeMultiObserveAir { - fn eval(&self, builder: &mut AB) { - let main = builder.main(); - let local = main.row_slice(0); - let local: &NativeMultiObserveCols = (*local).borrow(); - let next = main.row_slice(1); - let next: &NativeMultiObserveCols = (*next).borrow(); - - let &NativeMultiObserveCols { - enable, - is_first, - is_final, - is_observe, - pc, - state_idx, - remaining_len, - counter, - should_permute, - first_timestamp, - curr_timestamp, - final_timestamp_increment, - read_state_ptr, - read_input_ptr, - state_ptr, - input_ptr, - read_init_pos, - read_len, - init_pos, - len, - read_data, - write_data, - data, - read_sponge_state, - write_sponge_state, - permutation_input, - permutation_output, - write_final_idx, - final_idx, - input_register_1, - input_register_2, - input_register_3, - output_register, - } = local; - - // self.execution_bridge - // .execute_and_increment_pc( - // AB::F::from_canonical_usize(MULTI_OBSERVE.global_opcode().as_usize()), - // [ - // output_register.into(), - // input_register_1.into(), - // input_register_2.into(), - // self.address_space.into(), - // self.address_space.into(), - // input_register_3.into(), - // ], - // ExecutionState::new(pc, first_timestamp), - // final_timestamp_increment, - // ) - // .eval(builder, is_first); - - // // Memory operations - // self.memory_bridge - // .read( - // MemoryAddress::new(self.address_space, output_register), - // [state_ptr], - // first_timestamp, - // &read_state_ptr, - // ) - // .eval(builder, is_first); - - // self.memory_bridge - // .read( - // MemoryAddress::new(self.address_space, input_register_2), - // [input_ptr], - // first_timestamp + AB::F::ONE, - // &read_input_ptr, - // ) - // .eval(builder, is_first); - - // self.memory_bridge - // .read( - // MemoryAddress::new(self.address_space, input_register_1), - // [init_pos], - // first_timestamp + AB::F::TWO, - // &read_init_pos, - // ) - // .eval(builder, is_first); - - // self.memory_bridge - // .read( - // MemoryAddress::new(self.address_space, input_register_3), - // [len], - // first_timestamp + AB::F::from_canonical_usize(3), - // &read_len, - // ) - // .eval(builder, is_first); - - // self.memory_bridge - // .read( - // MemoryAddress::new(self.address_space, input_ptr + counter - AB::F::ONE), - // [data], - // first_timestamp + curr_timestamp, - // &read_data - // ) - // .eval(builder, is_observe); - - // self.memory_bridge - // .write( - // MemoryAddress::new( - // self.address_space, - // state_ptr + state_idx, - // ), - // [data], - // first_timestamp + curr_timestamp + AB::F::ONE, - // &write_data, - // ) - // .eval(builder, is_observe); - - // self.memory_bridge - // .read( - // MemoryAddress::new( - // self.address_space, - // state_ptr, - // ), - // permutation_input, - // first_timestamp + curr_timestamp + AB::F::TWO, - // &read_sponge_state, - // ) - // .eval(builder, should_permute); - - // self.memory_bridge - // .write( - // MemoryAddress::new( - // self.address_space, - // state_ptr - // ), - // permutation_output, - // first_timestamp + curr_timestamp + AB::F::from_canonical_usize(3), - // &write_sponge_state, - // ) - // .eval(builder, should_permute); - - // self.memory_bridge - // .write( - // MemoryAddress::new( - // self.address_space, - // input_register_1, - // ), - // [final_idx], - // first_timestamp + curr_timestamp + is_first * AB::F::from_canonical_usize(4) + is_observe * AB::F::TWO + should_permute * AB::F::TWO, - // &write_final_idx - // ) - // .eval(builder, is_final); - - // Binary indicators columns - builder.assert_bool(enable); - builder.assert_bool(is_first); - builder.assert_bool(is_observe); - builder.assert_bool(is_final); - builder.assert_bool(should_permute); - - // Except header rows, any other rows must observe an element - // All rows following the header row must observe an element - builder - .when(enable) - .assert_eq(is_first + is_observe, AB::F::ONE); - builder - .when(is_observe) - .when(next.enable) - .when(not(next.is_first)) - .assert_eq(next.is_observe, AB::F::ONE); - - // Each non-header row must process a field element - builder - .when(next.enable) - .when(not(next.is_first)) - .assert_eq(next.counter, counter + AB::F::ONE); - builder - .when(next.enable) - .when(not(next.is_first)) - .assert_eq(next.remaining_len, remaining_len - AB::F::ONE); - - // Boundary conditions - // At the header row, counter must be 0, remaining_len must be len - builder - .when(is_first) - .assert_eq(counter, AB::F::ZERO); - builder - .when(is_first) - .assert_eq(remaining_len, len); - - // At the final row, counter must be len, remaining_len must be 0 - builder - .when(is_final) - .assert_eq(counter, len); - builder - .when(is_final) - .assert_eq(remaining_len, AB::F::ZERO); - - // After each permutation, the sponge state index must revert to 0 - builder - .when(should_permute) - .when(not(next.is_first)) - .assert_eq(next.state_idx, AB::F::ZERO); - - // Timestamp constraints - builder - .when(is_first) - .assert_eq(curr_timestamp, AB::F::ZERO); - builder - .when(is_first) - .when(not(is_final)) - .assert_eq(next.curr_timestamp - curr_timestamp, AB::F::from_canonical_usize(4)); - builder - .when(is_observe) - .when(not(is_final)) - .when(not(should_permute)) - .assert_eq(next.curr_timestamp - curr_timestamp, AB::F::TWO); - builder - .when(is_observe) - .when(not(is_final)) - .when(should_permute) - .assert_eq(next.curr_timestamp - curr_timestamp, AB::F::from_canonical_usize(4)); - - // Fields that remain constant for a single MULTI_OBSERVE call - builder - .when(next.enable) - .when(not(next.is_first)) - .assert_eq(state_ptr, next.state_ptr); - builder - .when(next.enable) - .when(not(next.is_first)) - .assert_eq(input_ptr, next.input_ptr); - builder - .when(next.enable) - .when(not(next.is_first)) - .assert_eq(init_pos, next.init_pos); - builder - .when(next.enable) - .when(not(next.is_first)) - .assert_eq(len, next.len); - builder - .when(next.enable) - .when(not(next.is_first)) - .assert_eq(input_register_1, next.input_register_1); - builder - .when(next.enable) - .when(not(next.is_first)) - .assert_eq(input_register_2, next.input_register_2); - builder - .when(next.enable) - .when(not(next.is_first)) - .assert_eq(input_register_3, next.input_register_3); - builder - .when(next.enable) - .when(not(next.is_first)) - .assert_eq(output_register, next.output_register); - } -} - -#[repr(C)] -#[derive(Debug, Clone, Serialize, Deserialize, Default)] -#[serde(bound = "F: Field")] -pub struct TranscriptObservationRecord { - pub from_state: ExecutionState, - pub instruction: Instruction, - pub curr_timestamp: usize, - pub final_timestamp_increment: usize, - - pub state_idx: usize, - - pub is_first: bool, - pub is_observe: bool, - pub is_final: bool, - pub remaining_len: usize, - pub counter: usize, - pub should_permute: bool, - - pub read_state_ptr: RecordId, - pub read_input_ptr: RecordId, - pub state_ptr: F, - pub input_ptr: F, - - pub read_init_pos: RecordId, - pub init_pos: F, - pub read_len: RecordId, - pub len: usize, - - pub read_input_data: RecordId, - pub write_input_data: RecordId, - pub input_data: F, - - pub read_sponge_state: RecordId, - pub write_sponge_state: RecordId, - pub permutation_input: [F; 2 * CHUNK], - pub permutation_output: [F; 2 * CHUNK], - - pub write_final_idx: RecordId, - pub final_idx: usize, - - pub input_register_1: F, - pub input_register_2: F, - pub input_register_3: F, - pub output_register: F, -} - -#[derive(Debug, Clone, Serialize, Deserialize, Default)] -#[serde(bound = "F: Field")] -pub struct NativeMultiObserveRecordSet { - pub transcript_observation_records: Vec>, -} - -pub struct NativeMultiObserveChip { - pub(super) air: NativeMultiObserveAir, - pub record_set: NativeMultiObserveRecordSet, - pub height: usize, - pub(super) offline_memory: Arc>>, - pub(super) subchip: Poseidon2SubChip, -} - -impl NativeMultiObserveChip { - pub fn new( - port: SystemPort, - offline_memory: Arc>>, - poseidon2_config: Poseidon2Config, - ) -> Self { - let air = NativeMultiObserveAir { - execution_bridge: ExecutionBridge::new(port.execution_bus, port.program_bus), - memory_bridge: port.memory_bridge, - address_space: F::from_canonical_u32(AS::Native as u32), - }; - Self { - record_set: Default::default(), - air, - height: 0, - offline_memory, - subchip: Poseidon2SubChip::new(poseidon2_config.constants), - } - } - - fn record_to_row( - &self, - record: &TranscriptObservationRecord, - aux_cols_factory: &MemoryAuxColsFactory, - slice: &mut [F], - memory: &OfflineMemory, - ) { - let cols: &mut NativeMultiObserveCols = slice.borrow_mut(); - - cols.enable = F::ONE; - cols.is_first = if record.is_first { F::ONE } else { F::ZERO }; - cols.is_final = if record.is_final { F::ONE } else { F::ZERO }; - cols.is_observe = if !record.is_first { F::ONE } else { F::ZERO }; - cols.should_permute = if record.should_permute { F::ONE } else { F::ZERO }; - - let read_state_ptr_record = memory.record_by_id(record.read_state_ptr); - let read_input_ptr_record = memory.record_by_id(record.read_input_ptr); - let read_init_pos_record = memory.record_by_id(record.read_init_pos); - let read_len_record = memory.record_by_id(record.read_len); - - cols.state_ptr = record.state_ptr; - cols.input_ptr = record.input_ptr; - cols.init_pos = record.init_pos; - cols.len = F::from_canonical_usize(record.len); - cols.data = record.input_data; - cols.curr_timestamp = F::from_canonical_usize(record.curr_timestamp); - cols.final_timestamp_increment = F::from_canonical_usize(record.final_timestamp_increment); - - cols.permutation_input = record.permutation_input; - cols.permutation_output = record.permutation_output; - - cols.state_idx = F::from_canonical_usize(record.state_idx); - cols.remaining_len = F::from_canonical_usize(record.remaining_len); - cols.counter = F::from_canonical_usize(record.counter); - cols.final_idx = F::from_canonical_usize(record.final_idx); - - cols.first_timestamp = F::from_canonical_u32(record.from_state.timestamp); - cols.pc = F::from_canonical_u32(record.from_state.pc); - - cols.input_register_1 = record.input_register_1; - cols.input_register_2 = record.input_register_2; - cols.input_register_3 = record.input_register_3; - cols.output_register = record.output_register; - - if record.is_first { - aux_cols_factory.generate_read_aux(read_state_ptr_record, &mut cols.read_state_ptr); - aux_cols_factory.generate_read_aux(read_input_ptr_record, &mut cols.read_input_ptr); - aux_cols_factory.generate_read_aux(read_init_pos_record, &mut cols.read_init_pos); - aux_cols_factory.generate_read_aux(read_len_record, &mut cols.read_len); - } - - if record.is_observe { - let read_data_record = memory.record_by_id(record.read_input_data); - let write_data_record = memory.record_by_id(record.write_input_data); - aux_cols_factory.generate_read_aux(read_data_record, &mut cols.read_data); - aux_cols_factory.generate_write_aux(write_data_record, &mut cols.write_data); - } - - if record.should_permute { - let read_sponge_record = memory.record_by_id(record.read_sponge_state); - let write_sponge_record = memory.record_by_id(record.write_sponge_state); - aux_cols_factory.generate_read_aux(read_sponge_record, &mut cols.read_sponge_state); - aux_cols_factory.generate_write_aux(write_sponge_record, &mut cols.write_sponge_state); - } - - if record.is_final { - let write_final_idx_record = memory.record_by_id(record.write_final_idx); - aux_cols_factory.generate_write_aux(write_final_idx_record, &mut cols.write_final_idx); - } - } - - fn generate_trace(self) -> RowMajorMatrix { - let width = self.trace_width(); - let height = next_power_of_two_or_zero(self.height); - let mut flat_trace = F::zero_vec(width * height); - - let memory = self.offline_memory.lock().unwrap(); - let aux_cols_factory = memory.aux_cols_factory(); - let mut used_cells = 0; - for record in self.record_set.transcript_observation_records.iter() { - self.record_to_row( - record, - &aux_cols_factory, - &mut flat_trace[used_cells..used_cells + width], - &memory, - ); - used_cells += width; - } - - RowMajorMatrix::new(flat_trace, width) - } -} - -impl InstructionExecutor for NativeMultiObserveChip { - fn execute( - &mut self, - memory: &mut MemoryController, - instruction: &Instruction, - from_state: ExecutionState, - ) -> Result, ExecutionError> { - let mut observation_records: Vec> = vec![]; - - let &Instruction { - a: output_register, - b: input_register_1, - c: input_register_2, - d: data_address_space, - e: register_address_space, - f: input_register_3, - .. - } = instruction; - - let (read_sponge_ptr, sponge_ptr) = memory.read_cell(register_address_space, output_register); - let (read_arr_ptr, arr_ptr) = memory.read_cell(register_address_space, input_register_2); - let (read_init_pos, pos) = memory.read_cell(register_address_space, input_register_1); - let init_pos = pos.clone(); - let mut pos = pos.as_canonical_u32() as usize; - let (read_len, len) = memory.read_cell(register_address_space, input_register_3); - let len = len.as_canonical_u32() as usize; - - let head_record: TranscriptObservationRecord = TranscriptObservationRecord { - from_state, - instruction: instruction.clone(), - is_first: true, - state_idx: pos % CHUNK, - remaining_len: len, - counter: 0, - read_state_ptr: read_sponge_ptr, - read_input_ptr: read_arr_ptr, - state_ptr: sponge_ptr, - input_ptr: arr_ptr, - read_init_pos: read_init_pos, - init_pos, - read_len, - len, - input_register_1, - input_register_2, - input_register_3, - output_register, - ..Default::default() - }; - - self.height += 1; - observation_records.push(head_record); - - let mut curr_timestamp = 4usize; - - - for i in 0..len { - let mut record: TranscriptObservationRecord = TranscriptObservationRecord { - from_state, - curr_timestamp, - instruction: instruction.clone(), - is_observe: true, - state_idx: pos % CHUNK, - remaining_len: len - i - 1, - counter: i + 1, - read_state_ptr: read_sponge_ptr, - read_input_ptr: read_arr_ptr, - state_ptr: sponge_ptr, - input_ptr: arr_ptr, - read_init_pos: read_init_pos, - init_pos, - read_len, - len, - input_register_1, - input_register_2, - input_register_3, - output_register, - ..Default::default() - }; - - let (n_read, n_f) = memory.read_cell(data_address_space, arr_ptr + F::from_canonical_usize(i)); - record.read_input_data = n_read; - record.input_data = n_f; - curr_timestamp += 1; - - let (n_write, _) = memory.write_cell(data_address_space, sponge_ptr + F::from_canonical_usize(record.state_idx), record.input_data); - record.write_input_data = n_write; - curr_timestamp += 1; - - pos += 1; - - if pos % CHUNK == 0 { - record.should_permute = true; - let (read_sponge_record, permutation_input) = memory.read::<{CHUNK * 2}>(data_address_space, sponge_ptr); - let output = self.subchip.permute(permutation_input); - let (write_sponge_record, _) = memory.write::<{CHUNK * 2}>(data_address_space, sponge_ptr, std::array::from_fn(|i| output[i])); - - curr_timestamp += 2; - - record.read_sponge_state = read_sponge_record; - record.write_sponge_state = write_sponge_record; - record.permutation_input = permutation_input; - record.permutation_output = output; - } - - observation_records.push(record); - self.height += 1; - } - - let mod_pos = pos % CHUNK; - let (write_final, _) = memory.write_cell(register_address_space, input_register_1, F::from_canonical_usize(mod_pos)); - curr_timestamp += 1; - - observation_records[0].is_first = true; - observation_records.last_mut().unwrap().is_final = true; - observation_records.last_mut().unwrap().write_final_idx = write_final; - observation_records.last_mut().unwrap().final_idx = mod_pos; - - for record in &mut observation_records { - record.final_timestamp_increment = curr_timestamp; - } - - for record in observation_records { - self.record_set.transcript_observation_records.push(record); - } - - Ok(ExecutionState { - pc: from_state.pc + DEFAULT_PC_STEP, - timestamp: memory.timestamp(), - }) - } - - fn get_opcode_name(&self, opcode: usize) -> String { - if opcode == MULTI_OBSERVE.global_opcode().as_usize() { - String::from("MULTI_OBSERVE") - } else { - unreachable!("unsupported opcode: {}", opcode) - } - } -} - -impl ChipUsageGetter for NativeMultiObserveChip { - fn air_name(&self) -> String { - "MultiObserve".to_string() - } - - fn current_trace_height(&self) -> usize { - self.height - } - - fn trace_width(&self) -> usize { - NativeMultiObserveCols::::width() - } -} - -impl Chip - for NativeMultiObserveChip> -where - Val: PrimeField32, -{ - fn air(&self) -> AirRef { - Arc::new(self.air.clone()) - } - fn generate_air_proof_input(self) -> AirProofInput { - AirProofInput::simple_no_pis(self.generate_trace()) - } -} \ No newline at end of file diff --git a/extensions/native/circuit/src/poseidon2/air.rs b/extensions/native/circuit/src/poseidon2/air.rs index 434051d31b..9fb30edc46 100644 --- a/extensions/native/circuit/src/poseidon2/air.rs +++ b/extensions/native/circuit/src/poseidon2/air.rs @@ -682,6 +682,8 @@ impl Air // multi_observe contraints let multi_observe_specific: &MultiObserveCols = specific[..MultiObserveCols::::width()].borrow(); + let next_multi_observe_specific: &MultiObserveCols = + next.specific[..MultiObserveCols::::width()].borrow(); let &MultiObserveCols { pc, final_timestamp_increment, @@ -712,6 +714,16 @@ impl Air output_register } = multi_observe_specific; + builder + .when(multi_observe_row) + .assert_bool(is_first); + builder + .when(multi_observe_row) + .assert_bool(is_last); + builder + .when(multi_observe_row) + .assert_bool(should_permute); + self.execution_bridge .execute_and_increment_pc( AB::F::from_canonical_usize(MULTI_OBSERVE.global_opcode().as_usize()), @@ -863,6 +875,46 @@ impl Air &write_final_idx ) .eval(builder, multi_observe_row * is_last); + + builder + .when(next.multi_observe_row) + .when(not(next_multi_observe_specific.is_first)) + .assert_eq(state_ptr, next_multi_observe_specific.state_ptr); + + builder + .when(next.multi_observe_row) + .when(not(next_multi_observe_specific.is_first)) + .assert_eq(input_ptr, next_multi_observe_specific.input_ptr); + + builder + .when(next.multi_observe_row) + .when(not(next_multi_observe_specific.is_first)) + .assert_eq(init_pos, next_multi_observe_specific.init_pos); + + builder + .when(next.multi_observe_row) + .when(not(next_multi_observe_specific.is_first)) + .assert_eq(len, next_multi_observe_specific.len); + + builder + .when(next.multi_observe_row) + .when(not(next_multi_observe_specific.is_first)) + .assert_eq(input_register_1, next_multi_observe_specific.input_register_1); + + builder + .when(next.multi_observe_row) + .when(not(next_multi_observe_specific.is_first)) + .assert_eq(input_register_2, next_multi_observe_specific.input_register_2); + + builder + .when(next.multi_observe_row) + .when(not(next_multi_observe_specific.is_first)) + .assert_eq(input_register_3, next_multi_observe_specific.input_register_3); + + builder + .when(next.multi_observe_row) + .when(not(next_multi_observe_specific.is_first)) + .assert_eq(output_register, next_multi_observe_specific.output_register); } } diff --git a/extensions/native/circuit/src/poseidon2/chip.rs b/extensions/native/circuit/src/poseidon2/chip.rs index ab61f24260..d706b8c19b 100644 --- a/extensions/native/circuit/src/poseidon2/chip.rs +++ b/extensions/native/circuit/src/poseidon2/chip.rs @@ -317,6 +317,7 @@ impl InstructionExecutor let init_pos = pos.clone(); let mut pos = pos.as_canonical_u32() as usize; let (read_len, len) = memory.read_cell(register_address_space, input_register_3); + let init_len = len.as_canonical_u32() as usize; let mut len = len.as_canonical_u32() as usize; let mut header_record: TranscriptObservationRecord = TranscriptObservationRecord { @@ -327,7 +328,7 @@ impl InstructionExecutor state_ptr: sponge_ptr, input_ptr: arr_ptr, init_pos, - len, + len: init_len, input_register_1, input_register_2, input_register_3, @@ -356,9 +357,6 @@ impl InstructionExecutor } } - // _debug - println!("=> observation_chunks: {:?}", observation_chunks); - let mut curr_timestamp = 4usize; let mut input_idx: usize = 0; for chunk in observation_chunks { @@ -373,7 +371,7 @@ impl InstructionExecutor state_ptr: sponge_ptr, input_ptr: arr_ptr, init_pos, - len, + len: init_len, curr_len: input_idx, input_register_1, input_register_2, diff --git a/extensions/native/circuit/src/poseidon2/trace.rs b/extensions/native/circuit/src/poseidon2/trace.rs index b113dd9029..e2c0192be4 100644 --- a/extensions/native/circuit/src/poseidon2/trace.rs +++ b/extensions/native/circuit/src/poseidon2/trace.rs @@ -531,9 +531,6 @@ impl NativePoseidon2Chip record: {:?}", record); - self.multi_observe_record_to_row( record, &aux_cols_factory, From e4b20465c4eb7ebaf89b43d2e944a48f452a41d8 Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Sun, 10 Aug 2025 20:58:09 -0400 Subject: [PATCH 26/32] Populate poseidon2 columns --- extensions/native/circuit/src/poseidon2/air.rs | 12 ++++++------ extensions/native/circuit/src/poseidon2/trace.rs | 1 + 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/extensions/native/circuit/src/poseidon2/air.rs b/extensions/native/circuit/src/poseidon2/air.rs index 9fb30edc46..da65a5d970 100644 --- a/extensions/native/circuit/src/poseidon2/air.rs +++ b/extensions/native/circuit/src/poseidon2/air.rs @@ -115,12 +115,12 @@ impl Air builder.assert_eq(end.clone() * next.incorporate_row, next.start_top_level); // poseidon2 constraints are always checked - // let mut sub_builder = - // SubAirBuilder::, AB::F>::new( - // builder, - // 0..self.subair.width(), - // ); - // self.subair.eval(&mut sub_builder); + let mut sub_builder = + SubAirBuilder::, AB::F>::new( + builder, + 0..self.subair.width(), + ); + self.subair.eval(&mut sub_builder); // inside row constraints diff --git a/extensions/native/circuit/src/poseidon2/trace.rs b/extensions/native/circuit/src/poseidon2/trace.rs index e2c0192be4..49a65eb4e0 100644 --- a/extensions/native/circuit/src/poseidon2/trace.rs +++ b/extensions/native/circuit/src/poseidon2/trace.rs @@ -436,6 +436,7 @@ impl NativePoseidon2Chip, ) { + self.generate_subair_cols(record.permutation_input, slice); let cols: &mut NativePoseidon2Cols = slice.borrow_mut(); cols.very_first_timestamp = F::from_canonical_u32(record.from_state.timestamp); cols.start_timestamp = F::from_canonical_usize(record.from_state.timestamp as usize + record.curr_timestamp_increment); From 76c1db6cd3ce822419b0d3931592aa441c0e6d3d Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Sun, 10 Aug 2025 21:11:23 -0400 Subject: [PATCH 27/32] Reduce columns --- extensions/native/circuit/src/poseidon2/air.rs | 9 +++++---- extensions/native/circuit/src/poseidon2/columns.rs | 2 -- extensions/native/circuit/src/poseidon2/trace.rs | 2 -- 3 files changed, 5 insertions(+), 8 deletions(-) diff --git a/extensions/native/circuit/src/poseidon2/air.rs b/extensions/native/circuit/src/poseidon2/air.rs index da65a5d970..a088f9ac93 100644 --- a/extensions/native/circuit/src/poseidon2/air.rs +++ b/extensions/native/circuit/src/poseidon2/air.rs @@ -704,8 +704,6 @@ impl Air should_permute, read_sponge_state, write_sponge_state, - permutation_input, - permutation_output, write_final_idx, final_idx, input_register_1, @@ -840,13 +838,16 @@ impl Air end_idx ); + let full_sponge_input = from_fn::<_, {CHUNK * 2}, _>(|i| local.inner.inputs[i]); + let full_sponge_output = from_fn::<_, {CHUNK * 2}, _>(|i| local.inner.ending_full_rounds[BABY_BEAR_POSEIDON2_HALF_FULL_ROUNDS - 1].post[i]); + self.memory_bridge .read( MemoryAddress::new( self.address_space, state_ptr, ), - permutation_input, + full_sponge_input, start_timestamp + end_idx * AB::F::TWO - start_idx * AB::F::TWO, &read_sponge_state, ) @@ -858,7 +859,7 @@ impl Air self.address_space, state_ptr ), - permutation_output, + full_sponge_output, start_timestamp + end_idx * AB::F::TWO - start_idx * AB::F::TWO + AB::F::ONE, &write_sponge_state, ) diff --git a/extensions/native/circuit/src/poseidon2/columns.rs b/extensions/native/circuit/src/poseidon2/columns.rs index e768c35d0f..8bd45477ba 100644 --- a/extensions/native/circuit/src/poseidon2/columns.rs +++ b/extensions/native/circuit/src/poseidon2/columns.rs @@ -234,8 +234,6 @@ pub struct MultiObserveCols { pub should_permute: T, pub read_sponge_state: MemoryReadAuxCols, pub write_sponge_state: MemoryWriteAuxCols, - pub permutation_input: [T; 2 * CHUNK], - pub permutation_output: [T; 2 * CHUNK], // Final write back and registers pub write_final_idx: MemoryWriteAuxCols, diff --git a/extensions/native/circuit/src/poseidon2/trace.rs b/extensions/native/circuit/src/poseidon2/trace.rs index 49a65eb4e0..6b36665d17 100644 --- a/extensions/native/circuit/src/poseidon2/trace.rs +++ b/extensions/native/circuit/src/poseidon2/trace.rs @@ -486,8 +486,6 @@ impl NativePoseidon2Chip Date: Mon, 11 Aug 2025 04:39:34 -0400 Subject: [PATCH 28/32] Add more constraints --- .../native/circuit/src/poseidon2/air.rs | 30 +++++++++++++++++++ .../native/circuit/src/poseidon2/chip.rs | 7 +++-- .../native/circuit/src/poseidon2/columns.rs | 22 +------------- .../native/recursion/tests/recursion.rs | 5 ++-- 4 files changed, 38 insertions(+), 26 deletions(-) diff --git a/extensions/native/circuit/src/poseidon2/air.rs b/extensions/native/circuit/src/poseidon2/air.rs index a088f9ac93..79c65b062a 100644 --- a/extensions/native/circuit/src/poseidon2/air.rs +++ b/extensions/native/circuit/src/poseidon2/air.rs @@ -877,6 +877,25 @@ impl Air ) .eval(builder, multi_observe_row * is_last); + // Field transitions + builder + .when(next.multi_observe_row) + .when(not(next_multi_observe_specific.is_first)) + .assert_eq(next_multi_observe_specific.curr_len, multi_observe_specific.curr_len + end_idx - start_idx); + + // Boundary conditions + builder + .when(multi_observe_row) + .when(is_first) + .assert_zero(curr_len); + + builder + .when(multi_observe_row) + .when(is_last) + .assert_eq(curr_len + (end_idx - start_idx), len); + + + // Field consistency builder .when(next.multi_observe_row) .when(not(next_multi_observe_specific.is_first)) @@ -916,6 +935,17 @@ impl Air .when(next.multi_observe_row) .when(not(next_multi_observe_specific.is_first)) .assert_eq(output_register, next_multi_observe_specific.output_register); + + // Timestamp constraints + builder + .when(next.multi_observe_row) + .when(not(next_multi_observe_specific.is_first)) + .assert_eq(very_first_timestamp, next.very_first_timestamp); + + builder + .when(next.multi_observe_row) + .when(not(next_multi_observe_specific.is_first)) + .assert_eq(next.start_timestamp, start_timestamp + is_first * AB::F::from_canonical_usize(4) + (end_idx - start_idx) * AB::F::TWO + should_permute * AB::F::TWO); } } diff --git a/extensions/native/circuit/src/poseidon2/chip.rs b/extensions/native/circuit/src/poseidon2/chip.rs index d706b8c19b..fd4a6bc64e 100644 --- a/extensions/native/circuit/src/poseidon2/chip.rs +++ b/extensions/native/circuit/src/poseidon2/chip.rs @@ -315,6 +315,7 @@ impl InstructionExecutor let (read_arr_ptr, arr_ptr) = memory.read_cell(register_address_space, input_register_2); let (read_init_pos, pos) = memory.read_cell(register_address_space, input_register_1); let init_pos = pos.clone(); + let mut pos = pos.as_canonical_u32() as usize; let (read_len, len) = memory.read_cell(register_address_space, input_register_3); let init_len = len.as_canonical_u32() as usize; @@ -348,15 +349,15 @@ impl InstructionExecutor while len > 0 { if len >= (CHUNK - pos) { observation_chunks.push((pos.clone(), CHUNK.clone(), true)); - pos = 0; len -= CHUNK - pos; + pos = 0; } else { observation_chunks.push((pos.clone(), pos + len, false)); - pos = pos + len; len = 0; + pos = pos + len; } } - + let mut curr_timestamp = 4usize; let mut input_idx: usize = 0; for chunk in observation_chunks { diff --git a/extensions/native/circuit/src/poseidon2/columns.rs b/extensions/native/circuit/src/poseidon2/columns.rs index 8bd45477ba..fe0fce881a 100644 --- a/extensions/native/circuit/src/poseidon2/columns.rs +++ b/extensions/native/circuit/src/poseidon2/columns.rs @@ -243,24 +243,4 @@ pub struct MultiObserveCols { pub input_register_2: T, pub input_register_3: T, pub output_register: T, -} - -// _debug -// pub struct NativeMultiObserveCols { -// pub enable: T, -// pub is_first: T, -// pub is_final: T, -// pub is_observe: T, - -// pub pc: T, -// pub state_idx: T, -// pub remaining_len: T, -// pub counter: T, -// pub should_permute: T, - -// /// The initial timestamp of the instruction, which must be identical for first row -// /// and all following intermediate observation rows. -// pub first_timestamp: T, -// pub curr_timestamp: T, -// pub final_timestamp_increment: T, -// } +} \ No newline at end of file diff --git a/extensions/native/recursion/tests/recursion.rs b/extensions/native/recursion/tests/recursion.rs index 8794632db5..b08645eaf1 100644 --- a/extensions/native/recursion/tests/recursion.rs +++ b/extensions/native/recursion/tests/recursion.rs @@ -145,8 +145,9 @@ fn test_multi_observe() { fn build_test_program( builder: &mut Builder, ) { - let sample_lens: Vec = vec![0, 1, 2, 3]; - // let sample_lens: Vec = vec![0, 10, 20]; + // let sample_lens: Vec = vec![10, 2, 0, 3, 20]; + let sample_lens: Vec = vec![2, 30]; + let mut rng = create_seeded_rng(); let challenger = DuplexChallengerVariable::new(builder); From af58970fa38b390950109d42d027c35adaba34b2 Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Mon, 11 Aug 2025 04:42:56 -0400 Subject: [PATCH 29/32] Remove debug flags --- extensions/native/circuit/src/poseidon2/air.rs | 1 - extensions/native/recursion/tests/recursion.rs | 4 +--- 2 files changed, 1 insertion(+), 4 deletions(-) diff --git a/extensions/native/circuit/src/poseidon2/air.rs b/extensions/native/circuit/src/poseidon2/air.rs index 79c65b062a..dcd241a65a 100644 --- a/extensions/native/circuit/src/poseidon2/air.rs +++ b/extensions/native/circuit/src/poseidon2/air.rs @@ -894,7 +894,6 @@ impl Air .when(is_last) .assert_eq(curr_len + (end_idx - start_idx), len); - // Field consistency builder .when(next.multi_observe_row) diff --git a/extensions/native/recursion/tests/recursion.rs b/extensions/native/recursion/tests/recursion.rs index b08645eaf1..2147a18203 100644 --- a/extensions/native/recursion/tests/recursion.rs +++ b/extensions/native/recursion/tests/recursion.rs @@ -145,9 +145,7 @@ fn test_multi_observe() { fn build_test_program( builder: &mut Builder, ) { - // let sample_lens: Vec = vec![10, 2, 0, 3, 20]; - let sample_lens: Vec = vec![2, 30]; - + let sample_lens: Vec = vec![10, 2, 0, 3, 20]; let mut rng = create_seeded_rng(); let challenger = DuplexChallengerVariable::new(builder); From e7e88b84166e358b318ec3526eb92482c90b4654 Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Tue, 12 Aug 2025 19:33:48 -0400 Subject: [PATCH 30/32] Grammatic correction --- .../native/circuit/src/poseidon2/air.rs | 20 ++++++++++--------- .../native/circuit/src/poseidon2/chip.rs | 6 ++---- .../native/circuit/src/poseidon2/trace.rs | 4 ++-- 3 files changed, 15 insertions(+), 15 deletions(-) diff --git a/extensions/native/circuit/src/poseidon2/air.rs b/extensions/native/circuit/src/poseidon2/air.rs index dcd241a65a..ac8caff1aa 100644 --- a/extensions/native/circuit/src/poseidon2/air.rs +++ b/extensions/native/circuit/src/poseidon2/air.rs @@ -122,7 +122,7 @@ impl Air ); self.subair.eval(&mut sub_builder); - // inside row constraints + //// inside row constraints let inside_row_specific: &InsideRowSpecificCols = specific[..InsideRowSpecificCols::::width()].borrow(); @@ -679,7 +679,7 @@ impl Air ) .eval(builder, simple * is_permute); - // multi_observe contraints + //// multi_observe contraints let multi_observe_specific: &MultiObserveCols = specific[..MultiObserveCols::::width()].borrow(); let next_multi_observe_specific: &MultiObserveCols = @@ -749,8 +749,8 @@ impl Air self.memory_bridge .read( - MemoryAddress::new(self.address_space, input_register_2), - [input_ptr], + MemoryAddress::new(self.address_space, input_register_1), + [init_pos], very_first_timestamp + AB::F::ONE, &read_data[1], ) @@ -758,13 +758,13 @@ impl Air self.memory_bridge .read( - MemoryAddress::new(self.address_space, input_register_1), - [init_pos], + MemoryAddress::new(self.address_space, input_register_2), + [input_ptr], very_first_timestamp + AB::F::TWO, &read_data[2], ) .eval(builder, multi_observe_row * is_first); - + self.memory_bridge .read( MemoryAddress::new(self.address_space, input_register_3), @@ -811,7 +811,8 @@ impl Air } builder - .when(multi_observe_row * (AB::Expr::ONE - is_first)) + .when(multi_observe_row) + .when(not(is_first)) .assert_eq( aux_after_start[0] + aux_after_start[1] @@ -825,7 +826,8 @@ impl Air ); builder - .when(multi_observe_row * (AB::Expr::ONE - is_first)) + .when(multi_observe_row) + .when(not(is_first)) .assert_eq( aux_before_end[0] + aux_before_end[1] diff --git a/extensions/native/circuit/src/poseidon2/chip.rs b/extensions/native/circuit/src/poseidon2/chip.rs index fd4a6bc64e..47ffc156d5 100644 --- a/extensions/native/circuit/src/poseidon2/chip.rs +++ b/extensions/native/circuit/src/poseidon2/chip.rs @@ -312,8 +312,8 @@ impl InstructionExecutor } = instruction; let (read_sponge_ptr, sponge_ptr) = memory.read_cell(register_address_space, output_register); - let (read_arr_ptr, arr_ptr) = memory.read_cell(register_address_space, input_register_2); let (read_init_pos, pos) = memory.read_cell(register_address_space, input_register_1); + let (read_arr_ptr, arr_ptr) = memory.read_cell(register_address_space, input_register_2); let init_pos = pos.clone(); let mut pos = pos.as_canonical_u32() as usize; @@ -422,9 +422,7 @@ impl InstructionExecutor for record in &mut observation_records { record.final_timestamp_increment = curr_timestamp; } - for record in observation_records { - self.record_set.transcript_observation_records.push(record); - } + self.record_set.transcript_observation_records.extend(observation_records); } else if instruction.opcode == VERIFY_BATCH.global_opcode() { let &Instruction { a: dim_register, diff --git a/extensions/native/circuit/src/poseidon2/trace.rs b/extensions/native/circuit/src/poseidon2/trace.rs index 6b36665d17..9a2c2b4cb1 100644 --- a/extensions/native/circuit/src/poseidon2/trace.rs +++ b/extensions/native/circuit/src/poseidon2/trace.rs @@ -460,8 +460,8 @@ impl NativePoseidon2Chip Date: Tue, 12 Aug 2025 22:32:27 -0400 Subject: [PATCH 31/32] Add constraints --- extensions/native/circuit/src/poseidon2/air.rs | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/extensions/native/circuit/src/poseidon2/air.rs b/extensions/native/circuit/src/poseidon2/air.rs index ac8caff1aa..e1fca5c827 100644 --- a/extensions/native/circuit/src/poseidon2/air.rs +++ b/extensions/native/circuit/src/poseidon2/air.rs @@ -884,7 +884,7 @@ impl Air .when(next.multi_observe_row) .when(not(next_multi_observe_specific.is_first)) .assert_eq(next_multi_observe_specific.curr_len, multi_observe_specific.curr_len + end_idx - start_idx); - + // Boundary conditions builder .when(multi_observe_row) @@ -896,6 +896,16 @@ impl Air .when(is_last) .assert_eq(curr_len + (end_idx - start_idx), len); + builder + .when(next.multi_observe_row) + .when(not(next_multi_observe_specific.is_first)) + .assert_one(multi_observe_row); + + builder + .when(multi_observe_row) + .when(not(is_last)) + .assert_one(next.multi_observe_row); + // Field consistency builder .when(next.multi_observe_row) From b7351bbaa6a4952c155e4b3336880a4b1d04cf42 Mon Sep 17 00:00:00 2001 From: kunxian xia Date: Wed, 13 Aug 2025 20:19:07 +0800 Subject: [PATCH 32/32] remove unrelated log file --- vm_run_output.log | 1 - 1 file changed, 1 deletion(-) delete mode 100644 vm_run_output.log diff --git a/vm_run_output.log b/vm_run_output.log deleted file mode 100644 index feb1f17353..0000000000 --- a/vm_run_output.log +++ /dev/null @@ -1 +0,0 @@ -error: package ID specification `ceno-recursion-verifier` did not match any packages