From e62e8a15ba261ea700def7e7c1847921ed525ef3 Mon Sep 17 00:00:00 2001 From: Kevin Jue Date: Tue, 16 Jul 2024 22:35:23 -0700 Subject: [PATCH] fix: Allen's Poseidon2 fixes (#1099) --- recursion/compiler/src/asm/compiler.rs | 4 +- recursion/compiler/src/asm/instruction.rs | 30 +++-- recursion/compiler/src/ir/poseidon.rs | 18 ++- .../src/poseidon2_wide/air/control_flow.rs | 122 ++++++++++++++---- .../core/src/poseidon2_wide/air/memory.rs | 11 +- recursion/core/src/poseidon2_wide/air/mod.rs | 4 +- .../src/poseidon2_wide/air/syscall_params.rs | 6 +- .../poseidon2_wide/columns/control_flow.rs | 2 + .../columns/opcode_workspace.rs | 2 + .../poseidon2_wide/columns/syscall_params.rs | 2 +- recursion/core/src/poseidon2_wide/events.rs | 19 +-- recursion/core/src/poseidon2_wide/mod.rs | 17 ++- recursion/core/src/poseidon2_wide/trace.rs | 23 +++- recursion/core/src/runtime/mod.rs | 21 ++- 14 files changed, 209 insertions(+), 72 deletions(-) diff --git a/recursion/compiler/src/asm/compiler.rs b/recursion/compiler/src/asm/compiler.rs index 47797aae68..f2db872bae 100644 --- a/recursion/compiler/src/asm/compiler.rs +++ b/recursion/compiler/src/asm/compiler.rs @@ -517,12 +517,12 @@ impl + TwoAdicField> AsmCo _ => unimplemented!(), } } - DslIr::Poseidon2AbsorbBabyBear(p2_hash_num, input) => match input { + DslIr::Poseidon2AbsorbBabyBear(p2_hash_and_absorb_num, input) => match input { Array::Dyn(input, input_size) => { if let Usize::Var(input_size) = input_size { self.push( AsmInstruction::Poseidon2Absorb( - p2_hash_num.fp(), + p2_hash_and_absorb_num.fp(), input.fp(), input_size.fp(), ), diff --git a/recursion/compiler/src/asm/instruction.rs b/recursion/compiler/src/asm/instruction.rs index 5a38b67a4c..0dc9d5767d 100644 --- a/recursion/compiler/src/asm/instruction.rs +++ b/recursion/compiler/src/asm/instruction.rs @@ -854,17 +854,19 @@ impl> AsmInstruction { false, "".to_string(), ), - AsmInstruction::Poseidon2Absorb(hash_num, input_ptr, input_len) => Instruction::new( - Opcode::Poseidon2Absorb, - i32_f(hash_num), - i32_f_arr(input_ptr), - i32_f_arr(input_len), - F::zero(), - F::zero(), - false, - false, - "".to_string(), - ), + AsmInstruction::Poseidon2Absorb(hash_and_absorb_num, input_ptr, input_len) => { + Instruction::new( + Opcode::Poseidon2Absorb, + i32_f(hash_and_absorb_num), + i32_f_arr(input_ptr), + i32_f_arr(input_len), + F::zero(), + F::zero(), + false, + false, + "".to_string(), + ) + } AsmInstruction::Poseidon2Finalize(hash_num, output_ptr) => Instruction::new( Opcode::Poseidon2Finalize, i32_f(hash_num), @@ -1174,15 +1176,15 @@ impl> AsmInstruction { result, src1, src2 ) } - AsmInstruction::Poseidon2Absorb(hash_num, input_ptr, input_len) => { + AsmInstruction::Poseidon2Absorb(hash_and_absorb_num, input_ptr, input_len) => { write!( f, "poseidon2_absorb ({})fp, {})fp, ({})fp", - hash_num, input_ptr, input_len, + hash_and_absorb_num, input_ptr, input_len, ) } AsmInstruction::Poseidon2Finalize(hash_num, output_ptr) => { - write!(f, "poseidon2_finalize ({})fp, {})fp", hash_num, output_ptr,) + write!(f, "poseidon2_finalize ({})fp, ({})fp", hash_num, output_ptr,) } AsmInstruction::Commit(val, index) => { write!(f, "commit ({})fp ({})fp", val, index) diff --git a/recursion/compiler/src/ir/poseidon.rs b/recursion/compiler/src/ir/poseidon.rs index a69f86c8d6..2f7fde76ff 100644 --- a/recursion/compiler/src/ir/poseidon.rs +++ b/recursion/compiler/src/ir/poseidon.rs @@ -35,9 +35,15 @@ impl Builder { /// Applies the Poseidon2 absorb function to the given array. /// /// Reference: [p3_symmetric::PaddingFreeSponge] - pub fn poseidon2_absorb(&mut self, p2_hash_num: Var, input: &Array>) { - self.operations - .push(DslIr::Poseidon2AbsorbBabyBear(p2_hash_num, input.clone())); + pub fn poseidon2_absorb( + &mut self, + p2_hash_and_absorb_num: Var, + input: &Array>, + ) { + self.operations.push(DslIr::Poseidon2AbsorbBabyBear( + p2_hash_and_absorb_num, + input.clone(), + )); } /// Applies the Poseidon2 finalize to the given hash number. @@ -128,9 +134,13 @@ impl Builder { self.cycle_tracker("poseidon2-hash"); let p2_hash_num = self.p2_hash_num; + let two_power_12: Var<_> = self.eval(C::N::from_canonical_u32(1 << 12)); + self.range(0, array.len()).for_each(|i, builder| { let subarray = builder.get(array, i); - builder.poseidon2_absorb(p2_hash_num, &subarray); + let p2_hash_and_absorb_num: Var<_> = builder.eval(p2_hash_num * two_power_12 + i); + + builder.poseidon2_absorb(p2_hash_and_absorb_num, &subarray); }); let output: Array> = self.dyn_array(DIGEST_SIZE); diff --git a/recursion/core/src/poseidon2_wide/air/control_flow.rs b/recursion/core/src/poseidon2_wide/air/control_flow.rs index 50bcbd984f..2b1f559bf3 100644 --- a/recursion/core/src/poseidon2_wide/air/control_flow.rs +++ b/recursion/core/src/poseidon2_wide/air/control_flow.rs @@ -62,6 +62,10 @@ impl Poseidon2WideChip { local_row.syscall_params(), send_range_check, ); + + builder + .when(local_control_flow.is_syscall_row) + .assert_one(local_is_real); } /// This function will verify that all hash rows are before the compress rows and that the first @@ -80,38 +84,56 @@ impl Poseidon2WideChip { local_is_real: AB::Expr, next_is_real: AB::Expr, ) { - // We require that the first row is an absorb syscall and that the hash_num == 0. + // We require that the first row is an absorb syscall and that the hash_num == 0 and absorb_num == 0. let mut first_row_builder = builder.when_first_row(); first_row_builder.assert_one(local_control_flow.is_absorb); first_row_builder.assert_one(local_control_flow.is_syscall_row); - first_row_builder.assert_zero(local_syscall_params.absorb().hash_num); + first_row_builder.assert_zero(local_opcode_workspace.absorb().hash_num); + first_row_builder.assert_zero(local_opcode_workspace.absorb().absorb_num); first_row_builder.assert_one(local_opcode_workspace.absorb().is_first_hash_row); - let mut transition_builder = builder.when_transition(); - // For absorb rows, constrain the following: - // 1) next row is either an absorb or syscall finalize. - // 2) when last absorb row, then the next row is a syscall row. - // 2) hash_num == hash_num'. + // 1) when last absorb row, then the next row is a either an absorb or finalize syscall row. + // 2) when last absorb row and the next row is an absorb row, then absorb_num' = absorb_num + 1. + // 3) when not last absorb row, then the next row is an absorb non syscall row. + // 4) when not last absorb row, then absorb_num' = absorb_num. + // 5) hash_num == hash_num'. { - let mut absorb_transition_builder = - transition_builder.when(local_control_flow.is_absorb); - absorb_transition_builder + let mut transition_builder = builder.when_transition(); + + let mut absorb_last_row_builder = + transition_builder.when(local_control_flow.is_absorb_last_row); + absorb_last_row_builder .assert_one(next_control_flow.is_absorb + next_control_flow.is_finalize); - absorb_transition_builder - .when(local_opcode_workspace.absorb().is_last_row::()) - .assert_one(next_control_flow.is_syscall_row); + absorb_last_row_builder.assert_one(next_control_flow.is_syscall_row); + absorb_last_row_builder + .when(next_control_flow.is_absorb) + .assert_eq( + next_opcode_workspace.absorb().absorb_num, + local_opcode_workspace.absorb().absorb_num + AB::Expr::one(), + ); + + let mut absorb_not_last_row_builder = + transition_builder.when(local_control_flow.is_absorb_not_last_row); + absorb_not_last_row_builder.assert_one(next_control_flow.is_absorb); + absorb_not_last_row_builder.assert_zero(next_control_flow.is_syscall_row); + absorb_not_last_row_builder.assert_eq( + local_opcode_workspace.absorb().absorb_num, + next_opcode_workspace.absorb().absorb_num, + ); + let mut absorb_transition_builder = + transition_builder.when(local_control_flow.is_absorb); absorb_transition_builder .when(next_control_flow.is_absorb) .assert_eq( - local_syscall_params.absorb().hash_num, - next_syscall_params.absorb().hash_num, + local_opcode_workspace.absorb().hash_num, + next_opcode_workspace.absorb().hash_num, ); absorb_transition_builder .when(next_control_flow.is_finalize) .assert_eq( - local_syscall_params.absorb().hash_num, + local_opcode_workspace.absorb().hash_num, next_syscall_params.finalize().hash_num, ); } @@ -119,8 +141,10 @@ impl Poseidon2WideChip { // For finalize rows, constrain the following: // 1) next row is syscall compress or syscall absorb. // 2) if next row is absorb -> hash_num + 1 == hash_num' - // 3) if next row is absorb -> is_first_hash' == true + // 3) if next row is absorb -> absorb_num' == 0 + // 4) if next row is absorb -> is_first_hash' == true { + let mut transition_builder = builder.when_transition(); let mut finalize_transition_builder = transition_builder.when(local_control_flow.is_finalize); @@ -132,8 +156,11 @@ impl Poseidon2WideChip { .when(next_control_flow.is_absorb) .assert_eq( local_syscall_params.finalize().hash_num + AB::Expr::one(), - next_syscall_params.absorb().hash_num, + next_opcode_workspace.absorb().hash_num, ); + finalize_transition_builder + .when(next_control_flow.is_absorb) + .assert_zero(next_opcode_workspace.absorb().absorb_num); finalize_transition_builder .when(next_control_flow.is_absorb) .assert_one(next_opcode_workspace.absorb().is_first_hash_row); @@ -143,26 +170,33 @@ impl Poseidon2WideChip { // 1) if compress syscall -> next row is a compress output // 2) if compress output -> next row is a compress syscall or not real { + builder.assert_eq( + local_control_flow.is_compress_output, + local_control_flow.is_compress + * (AB::Expr::one() - local_control_flow.is_syscall_row), + ); + + let mut transition_builder = builder.when_transition(); + transition_builder .when(local_control_flow.is_compress) .when(local_control_flow.is_syscall_row) .assert_one(next_control_flow.is_compress_output); + // When we are at a compress output row, then ensure next row is either not real or is a compress syscall row. transition_builder .when(local_control_flow.is_compress_output) .assert_one( - next_control_flow.is_compress + (AB::Expr::one() - next_is_real.clone()), + (AB::Expr::one() - next_is_real.clone()) + + next_control_flow.is_compress * next_control_flow.is_syscall_row, ); - - transition_builder - .when(local_control_flow.is_compress_output) - .when(next_control_flow.is_compress) - .assert_one(next_control_flow.is_syscall_row); } // Constrain that there is only one is_real -> not is real transition. Also contrain that // the last real row is a compress output row. { + let mut transition_builder = builder.when_transition(); + transition_builder .when_not(local_is_real.clone()) .assert_zero(next_is_real.clone()); @@ -194,6 +228,29 @@ impl Poseidon2WideChip { let last_row_ending_cursor_is_seven = local_hash_workspace.last_row_ending_cursor_is_seven.result; + // Verify that the hash_num and absorb_num are correctly decomposed from the syscall + // hash_and_absorb_num param. + // Also range check that both hash_num is within [0, 2^16 - 1] and absorb_num is within [0, 2^12 - 1]; + { + let mut absorb_builder = builder.when(local_control_flow.is_absorb); + + absorb_builder.assert_eq( + local_hash_workspace.hash_num * AB::Expr::from_canonical_u32(1 << 12) + + local_hash_workspace.absorb_num, + local_syscall_params.absorb().hash_and_absorb_num, + ); + builder.send_range_check( + AB::Expr::from_canonical_u8(RangeCheckOpcode::U16 as u8), + local_hash_workspace.hash_num, + send_range_check, + ); + builder.send_range_check( + AB::Expr::from_canonical_u8(RangeCheckOpcode::U12 as u8), + local_hash_workspace.absorb_num, + send_range_check, + ); + } + // Constrain the materialized control flow flags. { let mut absorb_builder = builder.when(local_control_flow.is_absorb); @@ -232,12 +289,16 @@ impl Poseidon2WideChip { local_control_flow.is_absorb * (AB::Expr::one() - local_hash_workspace.is_last_row::()), ); + builder.assert_eq( + local_control_flow.is_absorb_last_row, + local_control_flow.is_absorb * local_hash_workspace.is_last_row::(), + ); builder.assert_eq( local_control_flow.is_absorb_no_perm, local_control_flow.is_absorb * (AB::Expr::one() - local_hash_workspace.do_perm::()), - ) + ); } // For the absorb syscall row, ensure correct value of num_remaining_rows, last_row_num_consumed, @@ -274,7 +335,16 @@ impl Poseidon2WideChip { expected_last_row_ending_cursor, ); - // Range check that num_remaining_rows is between [0, 2^18-1]. + // Range check that input_len < 2^16. This check is only needed for absorb syscall rows, + // but we send it for all absorb rows, since the `is_real` parameter must be an expression + // with at most degree 1. + builder.send_range_check( + AB::Expr::from_canonical_u8(RangeCheckOpcode::U16 as u8), + local_syscall_params.absorb().input_len, + send_range_check, + ); + + // Range check that num_remaining_rows is between [0, 2^16-1]. builder.send_range_check( AB::Expr::from_canonical_u8(RangeCheckOpcode::U16 as u8), local_hash_workspace.num_remaining_rows, diff --git a/recursion/core/src/poseidon2_wide/air/memory.rs b/recursion/core/src/poseidon2_wide/air/memory.rs index 506de55eee..3df855d164 100644 --- a/recursion/core/src/poseidon2_wide/air/memory.rs +++ b/recursion/core/src/poseidon2_wide/air/memory.rs @@ -185,12 +185,21 @@ impl Poseidon2WideChip { } // Verify that all elements of start_mem_idx_bitmap and end_mem_idx_bitmap are bool. + // Also verify that exactly one of the bits in start_mem_idx_bitmap and end_mem_idx_bitmap + // is one. + let mut start_mem_idx_bitmap_sum = AB::Expr::zero(); start_mem_idx_bitmap.iter().for_each(|bit| { absorb_builder.assert_bool(*bit); + start_mem_idx_bitmap_sum += (*bit).into(); }); + absorb_builder.assert_one(start_mem_idx_bitmap_sum); + + let mut end_mem_idx_bitmap_sum = AB::Expr::zero(); end_mem_idx_bitmap.iter().for_each(|bit| { absorb_builder.assert_bool(*bit); + end_mem_idx_bitmap_sum += (*bit).into(); }); + absorb_builder.assert_one(end_mem_idx_bitmap_sum); // Verify correct value of start_mem_idx_bitmap and end_mem_idx_bitmap. let start_mem_idx: AB::Expr = start_mem_idx_bitmap @@ -209,7 +218,7 @@ impl Poseidon2WideChip { // When we are not in the last row, end_mem_idx should be zero. absorb_builder .when_not(opcode_workspace.absorb().is_last_row::()) - .assert_zero(end_mem_idx.clone()); + .assert_zero(end_mem_idx.clone() - AB::Expr::from_canonical_usize(7)); // When we are in the last row, end_mem_idx bitmap should equal last_row_ending_cursor. absorb_builder diff --git a/recursion/core/src/poseidon2_wide/air/mod.rs b/recursion/core/src/poseidon2_wide/air/mod.rs index e69ecb066e..5780b195a5 100644 --- a/recursion/core/src/poseidon2_wide/air/mod.rs +++ b/recursion/core/src/poseidon2_wide/air/mod.rs @@ -4,7 +4,7 @@ //! # Layout of the poseidon2 chip: //! //! All the hash related rows should be in the first part of the chip and all the compress -//! related rows in the second part. E.g. the chip should has this format: +//! related rows in the second part. E.g. the chip should have this format: //! //! absorb row (for hash num 1) //! absorb row (for hash num 1) @@ -34,7 +34,7 @@ //! last_row_ending_cursor will be copied down to all of the rows. Also, for the next absorb/finalize //! syscall, its state_cursor is set to (last_row_ending_cursor + 1) % RATE. //! -//! From num_remaining_rows and syscall column, we know the absorb 's first row and last row. +//! From num_remaining_rows and syscall column, we know the absorb's first row and last row. //! From that fact, we can then enforce the following state writes. //! //! 1. is_first_row && is_last_row -> state writes are [state_cursor..state_cursor + last_row_ending_cursor] diff --git a/recursion/core/src/poseidon2_wide/air/syscall_params.rs b/recursion/core/src/poseidon2_wide/air/syscall_params.rs index db57a2cf7d..a79878e0ac 100644 --- a/recursion/core/src/poseidon2_wide/air/syscall_params.rs +++ b/recursion/core/src/poseidon2_wide/air/syscall_params.rs @@ -73,8 +73,10 @@ impl Poseidon2WideChip { let next_syscall_params = next_syscall.absorb(); absorb_syscall_builder.assert_eq(local_syscall_params.clk, next_syscall_params.clk); - absorb_syscall_builder - .assert_eq(local_syscall_params.hash_num, next_syscall_params.hash_num); + absorb_syscall_builder.assert_eq( + local_syscall_params.hash_and_absorb_num, + next_syscall_params.hash_and_absorb_num, + ); absorb_syscall_builder.assert_eq( local_syscall_params.input_ptr, next_syscall_params.input_ptr, diff --git a/recursion/core/src/poseidon2_wide/columns/control_flow.rs b/recursion/core/src/poseidon2_wide/columns/control_flow.rs index 1280a7a6a1..06b13534b4 100644 --- a/recursion/core/src/poseidon2_wide/columns/control_flow.rs +++ b/recursion/core/src/poseidon2_wide/columns/control_flow.rs @@ -15,6 +15,8 @@ pub struct ControlFlow { pub is_absorb_no_perm: T, /// Specifies if this row is for an absorb that is not the last row. pub is_absorb_not_last_row: T, + /// Specifies if this row is for an absorb that is the last row. + pub is_absorb_last_row: T, /// Specifies if this row is for finalize. pub is_finalize: T, diff --git a/recursion/core/src/poseidon2_wide/columns/opcode_workspace.rs b/recursion/core/src/poseidon2_wide/columns/opcode_workspace.rs index 139db2e329..3ff574f3c6 100644 --- a/recursion/core/src/poseidon2_wide/columns/opcode_workspace.rs +++ b/recursion/core/src/poseidon2_wide/columns/opcode_workspace.rs @@ -62,6 +62,8 @@ pub struct AbsorbWorkspace { pub state_cursor: T, /// Control flow columns. + pub hash_num: T, + pub absorb_num: T, pub is_first_hash_row: T, pub num_remaining_rows: T, pub num_remaining_rows_is_zero: IsZeroOperation, diff --git a/recursion/core/src/poseidon2_wide/columns/syscall_params.rs b/recursion/core/src/poseidon2_wide/columns/syscall_params.rs index b03d6b81ed..7550cfb8a5 100644 --- a/recursion/core/src/poseidon2_wide/columns/syscall_params.rs +++ b/recursion/core/src/poseidon2_wide/columns/syscall_params.rs @@ -67,7 +67,7 @@ pub struct CompressParams { #[repr(C)] pub struct AbsorbParams { pub clk: T, - pub hash_num: T, + pub hash_and_absorb_num: T, pub input_ptr: T, pub input_len: T, } diff --git a/recursion/core/src/poseidon2_wide/events.rs b/recursion/core/src/poseidon2_wide/events.rs index 5d17d27faf..83e22415b2 100644 --- a/recursion/core/src/poseidon2_wide/events.rs +++ b/recursion/core/src/poseidon2_wide/events.rs @@ -28,29 +28,32 @@ pub struct Poseidon2CompressEvent { #[derive(Debug, Clone)] pub struct Poseidon2AbsorbEvent { pub clk: F, - pub hash_num: F, // from a_val - pub input_addr: F, // from b_val - pub input_len: F, // from c_val + pub hash_and_absorb_num: F, // from a_val + pub input_addr: F, // from b_val + pub input_len: F, // from c_val + pub hash_num: F, + pub absorb_num: F, pub iterations: Vec>, - pub is_first_aborb: bool, } impl Poseidon2AbsorbEvent { pub(crate) fn new( clk: F, - hash_num: F, + hash_and_absorb_num: F, input_addr: F, input_len: F, - is_first_absorb: bool, + hash_num: F, + absorb_num: F, ) -> Self { Self { clk, - hash_num, + hash_and_absorb_num, input_addr, input_len, + hash_num, + absorb_num, iterations: Vec::new(), - is_first_aborb: is_first_absorb, } } } diff --git a/recursion/core/src/poseidon2_wide/mod.rs b/recursion/core/src/poseidon2_wide/mod.rs index 14f0af267a..86683d4c3f 100644 --- a/recursion/core/src/poseidon2_wide/mod.rs +++ b/recursion/core/src/poseidon2_wide/mod.rs @@ -206,12 +206,21 @@ pub(crate) mod tests { let prev_ts = BabyBear::from_canonical_usize(i); let absorb_ts = BabyBear::from_canonical_usize(i + 1); let finalize_ts = BabyBear::from_canonical_usize(i + 2); - let hash_num = BabyBear::from_canonical_usize(i); + let hash_num = i as u32; + let absorb_num = 0_u32; + let hash_and_absorb_num = + BabyBear::from_canonical_u32(hash_num * (1 << 12) + absorb_num); let start_addr = BabyBear::from_canonical_usize(i + 1); let input_len = BabyBear::from_canonical_usize(*input_size); - let mut absorb_event = - Poseidon2AbsorbEvent::new(absorb_ts, hash_num, start_addr, input_len, true); + let mut absorb_event = Poseidon2AbsorbEvent::new( + absorb_ts, + hash_and_absorb_num, + start_addr, + input_len, + BabyBear::from_canonical_u32(hash_num), + BabyBear::from_canonical_u32(absorb_num), + ); let mut hash_state = [BabyBear::zero(); WIDTH]; let mut hash_state_cursor = 0; @@ -240,7 +249,7 @@ pub(crate) mod tests { .poseidon2_hash_events .push(Poseidon2HashEvent::Finalize(Poseidon2FinalizeEvent { clk: finalize_ts, - hash_num, + hash_num: BabyBear::from_canonical_u32(hash_num), output_ptr: start_addr, output_records: dummy_memory_access_records( state.as_slice().to_vec(), diff --git a/recursion/core/src/poseidon2_wide/trace.rs b/recursion/core/src/poseidon2_wide/trace.rs index c7371e1b89..66cd6c8163 100644 --- a/recursion/core/src/poseidon2_wide/trace.rs +++ b/recursion/core/src/poseidon2_wide/trace.rs @@ -218,6 +218,7 @@ impl Poseidon2WideChip { control_flow.is_syscall_row = F::from_bool(is_syscall_row); control_flow.is_absorb_no_perm = F::from_bool(!absorb_iter.do_perm); control_flow.is_absorb_not_last_row = F::from_bool(!is_last_row); + control_flow.is_absorb_last_row = F::from_bool(is_last_row); } // Populate the syscall params fields. @@ -226,9 +227,14 @@ impl Poseidon2WideChip { let syscall_params = cols.syscall_params_mut().absorb_mut(); syscall_params.clk = absorb_event.clk; - syscall_params.hash_num = absorb_event.hash_num; + syscall_params.hash_and_absorb_num = absorb_event.hash_and_absorb_num; syscall_params.input_ptr = absorb_event.input_addr; syscall_params.input_len = absorb_event.input_len; + + output.add_range_check_events(&[RangeCheckEvent::new( + RangeCheckOpcode::U16, + absorb_event.input_len.as_canonical_u32() as u16, + )]); } // Populate the memory fields. @@ -248,6 +254,17 @@ impl Poseidon2WideChip { let mut cols = self.convert_mut(&mut absorb_row); let absorb_workspace = cols.opcode_workspace_mut().absorb_mut(); + absorb_workspace.hash_num = absorb_event.hash_num; + output.add_range_check_events(&[RangeCheckEvent::new( + RangeCheckOpcode::U16, + absorb_event.hash_num.as_canonical_u32() as u16, + )]); + absorb_workspace.absorb_num = absorb_event.absorb_num; + output.add_range_check_events(&[RangeCheckEvent::new( + RangeCheckOpcode::U12, + absorb_event.absorb_num.as_canonical_u32() as u16, + )]); + let num_remaining_rows = num_absorb_rows - 1 - iter_num; absorb_workspace.num_remaining_rows = F::from_canonical_usize(num_remaining_rows); output.add_range_check_events(&[RangeCheckEvent::new( @@ -302,11 +319,13 @@ impl Poseidon2WideChip { absorb_workspace.previous_state = absorb_iter.previous_state; absorb_workspace.state_cursor = F::from_canonical_usize(absorb_iter.state_cursor); absorb_workspace.is_first_hash_row = - F::from_bool(iter_num == 0 && absorb_event.is_first_aborb); + F::from_bool(iter_num == 0 && absorb_event.absorb_num.is_zero()); absorb_workspace.start_mem_idx_bitmap[absorb_iter.state_cursor] = F::one(); if is_last_row { absorb_workspace.end_mem_idx_bitmap[last_row_ending_cursor] = F::one(); + } else { + absorb_workspace.end_mem_idx_bitmap[7] = F::one(); } } diff --git a/recursion/core/src/runtime/mod.rs b/recursion/core/src/runtime/mod.rs index cb5b9959d7..57ee7bc3e0 100644 --- a/recursion/core/src/runtime/mod.rs +++ b/recursion/core/src/runtime/mod.rs @@ -737,23 +737,32 @@ where self.nb_poseidons += 1; let (a_val, b_val, c_val) = self.all_rr(&instruction); - let hash_num = a_val[0]; + let hash_and_absorb_num = a_val[0]; let start_addr = b_val[0]; let input_len = c_val[0]; let timestamp = self.clk; + let two_pow_12 = 1 << 12; + + let hash_and_absorb_num_u32 = hash_and_absorb_num.as_canonical_u32(); + let hash_num = F::from_canonical_u32(hash_and_absorb_num_u32 / two_pow_12); + let absorb_num = F::from_canonical_u32(hash_and_absorb_num_u32 % two_pow_12); + + // Double check that hash_num is [0, 2^16 - 1] and absorb_num is [0, 2^12 - 1] since + // that is what the AIR will enforce. + assert!(hash_num.as_canonical_u32() < 1 << 16); + assert!(absorb_num.as_canonical_u32() < 1 << 12); + // We currently don't support an input_len of 0, since it will need special logic in the AIR. assert!(input_len > F::zero()); - let is_first_absorb = self.p2_current_hash_num.is_none() - || self.p2_current_hash_num.unwrap() != hash_num; - let mut absorb_event = Poseidon2AbsorbEvent::new( timestamp, - hash_num, + hash_and_absorb_num, start_addr, input_len, - is_first_absorb, + hash_num, + absorb_num, ); let memory_records: Vec> = (0..input_len.as_canonical_u32())