diff --git a/stwo_cairo_prover/crates/prover/src/cairo_air/opcodes_air.rs b/stwo_cairo_prover/crates/prover/src/cairo_air/opcodes_air.rs index 420c438c..2fc2bbe6 100644 --- a/stwo_cairo_prover/crates/prover/src/cairo_air/opcodes_air.rs +++ b/stwo_cairo_prover/crates/prover/src/cairo_air/opcodes_air.rs @@ -17,9 +17,13 @@ use crate::components::{ assert_eq_opcode_is_double_deref_f_is_imm_f, assert_eq_opcode_is_double_deref_f_is_imm_t, assert_eq_opcode_is_double_deref_t_is_imm_f, generic_opcode, jnz_opcode_is_taken_f_dst_base_fp_f, jnz_opcode_is_taken_f_dst_base_fp_t, - jnz_opcode_is_taken_t_dst_base_fp_f, jnz_opcode_is_taken_t_dst_base_fp_t, memory_address_to_id, - memory_id_to_big, mul_opcode_is_small_f_is_imm_f, mul_opcode_is_small_f_is_imm_t, - range_check_19, range_check_9_9, ret_opcode, verify_instruction, + jnz_opcode_is_taken_t_dst_base_fp_f, jnz_opcode_is_taken_t_dst_base_fp_t, + jump_opcode_is_rel_f_is_imm_f_is_double_deref_f, + jump_opcode_is_rel_f_is_imm_f_is_double_deref_t, + jump_opcode_is_rel_t_is_imm_f_is_double_deref_f, + jump_opcode_is_rel_t_is_imm_t_is_double_deref_f, memory_address_to_id, memory_id_to_big, + mul_opcode_is_small_f_is_imm_f, mul_opcode_is_small_f_is_imm_t, range_check_19, + range_check_9_9, ret_opcode, verify_instruction, }; use crate::input::state_transitions::StateTransitions; @@ -40,6 +44,10 @@ pub struct OpcodeClaim { jnz_f_t: Vec, jnz_t_f: Vec, jnz_t_t: Vec, + jump_f_f_f: Vec, + jump_f_f_t: Vec, + jump_t_f_f: Vec, + jump_t_t_f: Vec, mul_f_f: Vec, mul_f_t: Vec, ret: Vec, @@ -61,6 +69,10 @@ impl OpcodeClaim { self.jnz_f_t.iter().for_each(|c| c.mix_into(channel)); self.jnz_t_f.iter().for_each(|c| c.mix_into(channel)); self.jnz_t_t.iter().for_each(|c| c.mix_into(channel)); + self.jump_f_f_f.iter().for_each(|c| c.mix_into(channel)); + self.jump_f_f_t.iter().for_each(|c| c.mix_into(channel)); + self.jump_t_f_f.iter().for_each(|c| c.mix_into(channel)); + self.jump_t_t_f.iter().for_each(|c| c.mix_into(channel)); self.mul_f_f.iter().for_each(|c| c.mix_into(channel)); self.mul_f_t.iter().for_each(|c| c.mix_into(channel)); self.ret.iter().for_each(|c| c.mix_into(channel)); @@ -83,6 +95,10 @@ impl OpcodeClaim { self.jnz_f_t.iter().map(|c| c.log_sizes()), self.jnz_t_f.iter().map(|c| c.log_sizes()), self.jnz_t_t.iter().map(|c| c.log_sizes()), + self.jump_f_f_f.iter().map(|c| c.log_sizes()), + self.jump_f_f_t.iter().map(|c| c.log_sizes()), + self.jump_t_f_f.iter().map(|c| c.log_sizes()), + self.jump_t_t_f.iter().map(|c| c.log_sizes()), self.mul_f_f.iter().map(|c| c.log_sizes()), self.mul_f_t.iter().map(|c| c.log_sizes()), self.ret.iter().map(|c| c.log_sizes()), @@ -106,6 +122,10 @@ pub struct OpcodesClaimGenerator { jnz_f_t: Vec, jnz_t_f: Vec, jnz_t_t: Vec, + jump_f_f_f: Vec, + jump_f_f_t: Vec, + jump_t_f_f: Vec, + jump_t_t_f: Vec, mul_f_f: Vec, mul_f_t: Vec, ret: Vec, @@ -128,6 +148,10 @@ impl OpcodesClaimGenerator { let mut jnz_f_t = vec![]; let mut jnz_t_f = vec![]; let mut jnz_t_t = vec![]; + let mut jump_f_f_f = vec![]; + let mut jump_f_f_t = vec![]; + let mut jump_t_f_f = vec![]; + let mut jump_t_t_f = vec![]; let mut mul_f_f = vec![]; let mut mul_f_t = vec![]; let mut ret = vec![]; @@ -288,6 +312,58 @@ impl OpcodesClaimGenerator { .jnz_opcode_is_taken_t_dst_base_fp_t, )); } + if !input + .casm_states_by_opcode + .jump_opcode_is_rel_f_is_imm_f_is_double_deref_f + .is_empty() + { + jump_f_f_f.push( + jump_opcode_is_rel_f_is_imm_f_is_double_deref_f::ClaimGenerator::new( + input + .casm_states_by_opcode + .jump_opcode_is_rel_f_is_imm_f_is_double_deref_f, + ), + ); + } + if !input + .casm_states_by_opcode + .jump_opcode_is_rel_f_is_imm_f_is_double_deref_t + .is_empty() + { + jump_f_f_t.push( + jump_opcode_is_rel_f_is_imm_f_is_double_deref_t::ClaimGenerator::new( + input + .casm_states_by_opcode + .jump_opcode_is_rel_f_is_imm_f_is_double_deref_t, + ), + ); + } + if !input + .casm_states_by_opcode + .jump_opcode_is_rel_t_is_imm_f_is_double_deref_f + .is_empty() + { + jump_t_f_f.push( + jump_opcode_is_rel_t_is_imm_f_is_double_deref_f::ClaimGenerator::new( + input + .casm_states_by_opcode + .jump_opcode_is_rel_t_is_imm_f_is_double_deref_f, + ), + ); + } + if !input + .casm_states_by_opcode + .jump_opcode_is_rel_t_is_imm_t_is_double_deref_f + .is_empty() + { + jump_t_t_f.push( + jump_opcode_is_rel_t_is_imm_t_is_double_deref_f::ClaimGenerator::new( + input + .casm_states_by_opcode + .jump_opcode_is_rel_t_is_imm_t_is_double_deref_f, + ), + ); + } // Handle small mul in big mul component. Temporary until airs are written with Rc_3_6_6. // TODO(Ohad): mul small. if !input @@ -329,6 +405,10 @@ impl OpcodesClaimGenerator { jnz_f_t, jnz_t_f, jnz_t_t, + jump_f_f_f, + jump_f_f_t, + jump_t_f_f, + jump_t_t_f, mul_f_f, mul_f_t, ret, @@ -526,6 +606,54 @@ impl OpcodesClaimGenerator { ) }) .unzip(); + let (jump_f_f_f_claims, jump_f_f_f_interaction_gens) = self + .jump_f_f_f + .into_iter() + .map(|gen| { + gen.write_trace( + tree_builder, + memory_address_to_id_trace_generator, + memory_id_to_value_trace_generator, + verify_instruction_trace_generator, + ) + }) + .unzip(); + let (jump_f_f_t_claims, jump_f_f_t_interaction_gens) = self + .jump_f_f_t + .into_iter() + .map(|gen| { + gen.write_trace( + tree_builder, + memory_address_to_id_trace_generator, + memory_id_to_value_trace_generator, + verify_instruction_trace_generator, + ) + }) + .unzip(); + let (jump_t_f_f_claims, jump_t_f_f_interaction_gens) = self + .jump_t_f_f + .into_iter() + .map(|gen| { + gen.write_trace( + tree_builder, + memory_address_to_id_trace_generator, + memory_id_to_value_trace_generator, + verify_instruction_trace_generator, + ) + }) + .unzip(); + let (jump_t_t_f_claims, jump_t_t_f_interaction_gens) = self + .jump_t_t_f + .into_iter() + .map(|gen| { + gen.write_trace( + tree_builder, + memory_address_to_id_trace_generator, + memory_id_to_value_trace_generator, + verify_instruction_trace_generator, + ) + }) + .unzip(); let (mul_f_f_claims, mul_f_f_interaction_gens) = self .mul_f_f .into_iter() @@ -581,6 +709,10 @@ impl OpcodesClaimGenerator { jnz_f_t: jnz_f_t_claims, jnz_t_f: jnz_t_f_claims, jnz_t_t: jnz_t_t_claims, + jump_f_f_f: jump_f_f_f_claims, + jump_f_f_t: jump_f_f_t_claims, + jump_t_f_f: jump_t_f_f_claims, + jump_t_t_f: jump_t_t_f_claims, mul_f_f: mul_f_f_claims, mul_f_t: mul_f_t_claims, ret: ret_claims, @@ -601,6 +733,10 @@ impl OpcodesClaimGenerator { jnz_f_t: jnz_f_t_interaction_gens, jnz_t_f: jnz_t_f_interaction_gens, jnz_t_t: jnz_t_t_interaction_gens, + jump_f_f_f: jump_f_f_f_interaction_gens, + jump_f_f_t: jump_f_f_t_interaction_gens, + jump_t_f_f: jump_t_f_f_interaction_gens, + jump_t_t_f: jump_t_t_f_interaction_gens, mul_f_f: mul_f_f_interaction_gens, mul_f_t: mul_f_t_interaction_gens, ret_interaction_gens, @@ -626,6 +762,10 @@ pub struct OpcodeInteractionClaim { jnz_f_t: Vec, jnz_t_f: Vec, jnz_t_t: Vec, + jump_f_f_f: Vec, + jump_f_f_t: Vec, + jump_t_f_f: Vec, + jump_t_t_f: Vec, mul_f_f: Vec, mul_f_t: Vec, ret: Vec, @@ -647,6 +787,10 @@ impl OpcodeInteractionClaim { self.jnz_f_t.iter().for_each(|c| c.mix_into(channel)); self.jnz_t_f.iter().for_each(|c| c.mix_into(channel)); self.jnz_t_t.iter().for_each(|c| c.mix_into(channel)); + self.jump_f_f_f.iter().for_each(|c| c.mix_into(channel)); + self.jump_f_f_t.iter().for_each(|c| c.mix_into(channel)); + self.jump_t_f_f.iter().for_each(|c| c.mix_into(channel)); + self.jump_t_t_f.iter().for_each(|c| c.mix_into(channel)); self.mul_f_f.iter().for_each(|c| c.mix_into(channel)); self.mul_f_t.iter().for_each(|c| c.mix_into(channel)); self.ret.iter().for_each(|c| c.mix_into(channel)); @@ -759,6 +903,34 @@ impl OpcodeInteractionClaim { None => total_sum, }; } + for interaction_claim in &self.jump_f_f_f { + let (total_sum, claimed_sum) = interaction_claim.logup_sums; + sum += match claimed_sum { + Some((claimed_sum, ..)) => claimed_sum, + None => total_sum, + }; + } + for interaction_claim in &self.jump_f_f_t { + let (total_sum, claimed_sum) = interaction_claim.logup_sums; + sum += match claimed_sum { + Some((claimed_sum, ..)) => claimed_sum, + None => total_sum, + }; + } + for interaction_claim in &self.jump_t_f_f { + let (total_sum, claimed_sum) = interaction_claim.logup_sums; + sum += match claimed_sum { + Some((claimed_sum, ..)) => claimed_sum, + None => total_sum, + }; + } + for interaction_claim in &self.jump_t_t_f { + let (total_sum, claimed_sum) = interaction_claim.logup_sums; + sum += match claimed_sum { + Some((claimed_sum, ..)) => claimed_sum, + None => total_sum, + }; + } for interaction_claim in &self.mul_f_f { let (total_sum, claimed_sum) = interaction_claim.logup_sums; sum += match claimed_sum { @@ -800,6 +972,10 @@ pub struct OpcodesInteractionClaimGenerator { jnz_f_t: Vec, jnz_t_f: Vec, jnz_t_t: Vec, + jump_f_f_f: Vec, + jump_f_f_t: Vec, + jump_t_f_f: Vec, + jump_t_t_f: Vec, mul_f_f: Vec, mul_f_t: Vec, ret_interaction_gens: Vec, @@ -1005,6 +1181,58 @@ impl OpcodesInteractionClaimGenerator { ) }) .collect(); + let jump_f_f_interaction_claims = self + .jump_f_f_f + .into_iter() + .map(|gen| { + gen.write_interaction_trace( + tree_builder, + &interaction_elements.memory_address_to_id, + &interaction_elements.memory_id_to_value, + &interaction_elements.opcodes, + &interaction_elements.verify_instruction, + ) + }) + .collect(); + let jump_f_t_interaction_claims = self + .jump_f_f_t + .into_iter() + .map(|gen| { + gen.write_interaction_trace( + tree_builder, + &interaction_elements.memory_address_to_id, + &interaction_elements.memory_id_to_value, + &interaction_elements.opcodes, + &interaction_elements.verify_instruction, + ) + }) + .collect(); + let jump_t_f_interaction_claims = self + .jump_t_f_f + .into_iter() + .map(|gen| { + gen.write_interaction_trace( + tree_builder, + &interaction_elements.memory_address_to_id, + &interaction_elements.memory_id_to_value, + &interaction_elements.opcodes, + &interaction_elements.verify_instruction, + ) + }) + .collect(); + let jump_t_t_interaction_claims = self + .jump_t_t_f + .into_iter() + .map(|gen| { + gen.write_interaction_trace( + tree_builder, + &interaction_elements.memory_address_to_id, + &interaction_elements.memory_id_to_value, + &interaction_elements.opcodes, + &interaction_elements.verify_instruction, + ) + }) + .collect(); let mul_f_f_interaction_claims = self .mul_f_f .into_iter() @@ -1062,6 +1290,10 @@ impl OpcodesInteractionClaimGenerator { jnz_f_t: jnz_f_t_interaction_claims, jnz_t_f: jnz_t_f_interaction_claims, jnz_t_t: jnz_t_t_interaction_claims, + jump_f_f_f: jump_f_f_interaction_claims, + jump_f_f_t: jump_f_t_interaction_claims, + jump_t_f_f: jump_t_f_interaction_claims, + jump_t_t_f: jump_t_t_interaction_claims, mul_f_f: mul_f_f_interaction_claims, mul_f_t: mul_f_t_interaction_claims, ret: ret_interaction_claims, @@ -1085,6 +1317,10 @@ pub struct OpcodeComponents { jnz_f_t: Vec, jnz_t_f: Vec, jnz_t_t: Vec, + jump_f_f_f: Vec, + jump_f_f_t: Vec, + jump_t_f_f: Vec, + jump_t_t_f: Vec, mul_f_f: Vec, mul_f_t: Vec, ret: Vec, @@ -1454,6 +1690,102 @@ impl OpcodeComponents { ) }) .collect_vec(); + let jump_f_f_components = claim + .jump_f_f_f + .iter() + .zip(interaction_claim.jump_f_f_f.iter()) + .map(|(&claim, &interaction_claim)| { + jump_opcode_is_rel_f_is_imm_f_is_double_deref_f::Component::new( + tree_span_provider, + jump_opcode_is_rel_f_is_imm_f_is_double_deref_f::Eval { + claim, + memoryaddresstoid_lookup_elements: interaction_elements + .memory_address_to_id + .clone(), + memoryidtobig_lookup_elements: interaction_elements + .memory_id_to_value + .clone(), + opcodes_lookup_elements: interaction_elements.opcodes.clone(), + verifyinstruction_lookup_elements: interaction_elements + .verify_instruction + .clone(), + }, + interaction_claim.logup_sums, + ) + }) + .collect(); + let jump_f_t_components = claim + .jump_f_f_t + .iter() + .zip(interaction_claim.jump_f_f_t.iter()) + .map(|(&claim, &interaction_claim)| { + jump_opcode_is_rel_f_is_imm_f_is_double_deref_t::Component::new( + tree_span_provider, + jump_opcode_is_rel_f_is_imm_f_is_double_deref_t::Eval { + claim, + memoryaddresstoid_lookup_elements: interaction_elements + .memory_address_to_id + .clone(), + memoryidtobig_lookup_elements: interaction_elements + .memory_id_to_value + .clone(), + opcodes_lookup_elements: interaction_elements.opcodes.clone(), + verifyinstruction_lookup_elements: interaction_elements + .verify_instruction + .clone(), + }, + interaction_claim.logup_sums, + ) + }) + .collect(); + let jump_t_f_components = claim + .jump_t_f_f + .iter() + .zip(interaction_claim.jump_t_f_f.iter()) + .map(|(&claim, &interaction_claim)| { + jump_opcode_is_rel_t_is_imm_f_is_double_deref_f::Component::new( + tree_span_provider, + jump_opcode_is_rel_t_is_imm_f_is_double_deref_f::Eval { + claim, + memoryaddresstoid_lookup_elements: interaction_elements + .memory_address_to_id + .clone(), + memoryidtobig_lookup_elements: interaction_elements + .memory_id_to_value + .clone(), + opcodes_lookup_elements: interaction_elements.opcodes.clone(), + verifyinstruction_lookup_elements: interaction_elements + .verify_instruction + .clone(), + }, + interaction_claim.logup_sums, + ) + }) + .collect(); + let jump_t_t_components = claim + .jump_t_t_f + .iter() + .zip(interaction_claim.jump_t_t_f.iter()) + .map(|(&claim, &interaction_claim)| { + jump_opcode_is_rel_t_is_imm_t_is_double_deref_f::Component::new( + tree_span_provider, + jump_opcode_is_rel_t_is_imm_t_is_double_deref_f::Eval { + claim, + memoryaddresstoid_lookup_elements: interaction_elements + .memory_address_to_id + .clone(), + memoryidtobig_lookup_elements: interaction_elements + .memory_id_to_value + .clone(), + opcodes_lookup_elements: interaction_elements.opcodes.clone(), + verifyinstruction_lookup_elements: interaction_elements + .verify_instruction + .clone(), + }, + interaction_claim.logup_sums, + ) + }) + .collect(); let mul_f_f_components = claim .mul_f_f .iter() @@ -1544,6 +1876,10 @@ impl OpcodeComponents { jnz_f_t: jnz_f_t_components, jnz_t_f: jnz_t_f_components, jnz_t_t: jnz_t_t_components, + jump_f_f_f: jump_f_f_components, + jump_f_f_t: jump_f_t_components, + jump_t_f_f: jump_t_f_components, + jump_t_t_f: jump_t_t_components, mul_f_f: mul_f_f_components, mul_f_t: mul_f_t_components, ret: ret_components, @@ -1627,6 +1963,26 @@ impl OpcodeComponents { .iter() .map(|component| component as &dyn ComponentProver), ); + vec.extend( + self.jump_f_f_f + .iter() + .map(|component| component as &dyn ComponentProver), + ); + vec.extend( + self.jump_f_f_t + .iter() + .map(|component| component as &dyn ComponentProver), + ); + vec.extend( + self.jump_t_f_f + .iter() + .map(|component| component as &dyn ComponentProver), + ); + vec.extend( + self.jump_t_t_f + .iter() + .map(|component| component as &dyn ComponentProver), + ); vec.extend( self.mul_f_f .iter() diff --git a/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_f_is_imm_f_is_double_deref_f/component.rs b/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_f_is_imm_f_is_double_deref_f/component.rs new file mode 100644 index 00000000..66523983 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_f_is_imm_f_is_double_deref_f/component.rs @@ -0,0 +1,174 @@ +#![allow(non_camel_case_types)] +#![allow(unused_imports)] +use num_traits::{One, Zero}; +use serde::{Deserialize, Serialize}; +use stwo_prover::constraint_framework::logup::{LogupAtRow, LogupSums, LookupElements}; +use stwo_prover::constraint_framework::{ + EvalAtRow, FrameworkComponent, FrameworkEval, RelationEntry, +}; +use stwo_prover::core::backend::simd::m31::LOG_N_LANES; +use stwo_prover::core::channel::Channel; +use stwo_prover::core::fields::m31::M31; +use stwo_prover::core::fields::qm31::SecureField; +use stwo_prover::core::fields::secure_column::SECURE_EXTENSION_DEGREE; +use stwo_prover::core::pcs::TreeVec; + +use crate::relations; + +pub struct Eval { + pub claim: Claim, + pub memoryaddresstoid_lookup_elements: relations::MemoryAddressToId, + pub memoryidtobig_lookup_elements: relations::MemoryIdToBig, + pub opcodes_lookup_elements: relations::Opcodes, + pub verifyinstruction_lookup_elements: relations::VerifyInstruction, +} + +#[derive(Copy, Clone, Serialize, Deserialize)] +pub struct Claim { + pub n_calls: usize, +} +impl Claim { + pub fn log_sizes(&self) -> TreeVec> { + let log_size = std::cmp::max(self.n_calls.next_power_of_two().ilog2(), LOG_N_LANES); + let trace_log_sizes = vec![log_size; 11]; + let interaction_log_sizes = vec![log_size; SECURE_EXTENSION_DEGREE * 5]; + let preprocessed_log_sizes = vec![log_size]; + TreeVec::new(vec![ + preprocessed_log_sizes, + trace_log_sizes, + interaction_log_sizes, + ]) + } + + pub fn mix_into(&self, channel: &mut impl Channel) { + channel.mix_u64(self.n_calls as u64); + } +} + +#[derive(Copy, Clone, Serialize, Deserialize)] +pub struct InteractionClaim { + pub logup_sums: LogupSums, +} +impl InteractionClaim { + pub fn mix_into(&self, channel: &mut impl Channel) { + let (total_sum, claimed_sum) = self.logup_sums; + channel.mix_felts(&[total_sum]); + if let Some(claimed_sum) = claimed_sum { + channel.mix_felts(&[claimed_sum.0]); + channel.mix_u64(claimed_sum.1 as u64); + } + } +} + +pub type Component = FrameworkComponent; + +impl FrameworkEval for Eval { + fn log_size(&self) -> u32 { + std::cmp::max(self.claim.n_calls.next_power_of_two().ilog2(), LOG_N_LANES) + } + + fn max_constraint_log_degree_bound(&self) -> u32 { + self.log_size() + 1 + } + + #[allow(unused_parens)] + #[allow(clippy::double_parens)] + #[allow(non_snake_case)] + fn evaluate(&self, mut eval: E) -> E { + let M31_0 = E::F::from(M31::from(0)); + let M31_1 = E::F::from(M31::from(1)); + let M31_262144 = E::F::from(M31::from(262144)); + let M31_32767 = E::F::from(M31::from(32767)); + let M31_32768 = E::F::from(M31::from(32768)); + let M31_512 = E::F::from(M31::from(512)); + let input_pc_col0 = eval.next_trace_mask(); + let input_ap_col1 = eval.next_trace_mask(); + let input_fp_col2 = eval.next_trace_mask(); + let offset2_col3 = eval.next_trace_mask(); + let op1_base_fp_col4 = eval.next_trace_mask(); + let op1_base_ap_col5 = eval.next_trace_mask(); + let ap_update_add_1_col6 = eval.next_trace_mask(); + let next_pc_id_col7 = eval.next_trace_mask(); + let next_pc_limb_0_col8 = eval.next_trace_mask(); + let next_pc_limb_1_col9 = eval.next_trace_mask(); + let next_pc_limb_2_col10 = eval.next_trace_mask(); + + // decode_instruction_ff344370bb4f7f54. + + eval.add_to_relation(&[RelationEntry::new( + &self.verifyinstruction_lookup_elements, + E::EF::one(), + &[ + input_pc_col0.clone(), + M31_32767.clone(), + M31_32767.clone(), + offset2_col3.clone(), + M31_1.clone(), + M31_1.clone(), + M31_0.clone(), + op1_base_fp_col4.clone(), + op1_base_ap_col5.clone(), + M31_0.clone(), + M31_0.clone(), + M31_1.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + ap_update_add_1_col6.clone(), + ], + )]); + + // Either flag op1_base_fp is on or flag op1_base_ap is on. + eval.add_constraint( + ((op1_base_fp_col4.clone() + op1_base_ap_col5.clone()) - M31_1.clone()), + ); + + // read_positive_num_bits_27. + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryaddresstoid_lookup_elements, + E::EF::one(), + &[ + (((op1_base_fp_col4.clone() * input_fp_col2.clone()) + + (op1_base_ap_col5.clone() * input_ap_col1.clone())) + + (offset2_col3.clone() - M31_32768.clone())), + next_pc_id_col7.clone(), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryidtobig_lookup_elements, + E::EF::one(), + &[ + next_pc_id_col7.clone(), + next_pc_limb_0_col8.clone(), + next_pc_limb_1_col9.clone(), + next_pc_limb_2_col10.clone(), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.opcodes_lookup_elements, + E::EF::one(), + &[ + input_pc_col0.clone(), + input_ap_col1.clone(), + input_fp_col2.clone(), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.opcodes_lookup_elements, + -E::EF::one(), + &[ + ((next_pc_limb_0_col8.clone() + (next_pc_limb_1_col9.clone() * M31_512.clone())) + + (next_pc_limb_2_col10.clone() * M31_262144.clone())), + (input_ap_col1.clone() + ap_update_add_1_col6.clone()), + input_fp_col2.clone(), + ], + )]); + + eval.finalize_logup(); + eval + } +} diff --git a/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_f_is_imm_f_is_double_deref_f/mod.rs b/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_f_is_imm_f_is_double_deref_f/mod.rs new file mode 100644 index 00000000..3f7a8d74 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_f_is_imm_f_is_double_deref_f/mod.rs @@ -0,0 +1,5 @@ +pub mod component; +pub mod prover; + +pub use component::{Claim, Component, Eval, InteractionClaim}; +pub use prover::{ClaimGenerator, InputType, InteractionClaimGenerator}; diff --git a/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_f_is_imm_f_is_double_deref_f/prover.rs b/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_f_is_imm_f_is_double_deref_f/prover.rs new file mode 100644 index 00000000..7a9406b6 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_f_is_imm_f_is_double_deref_f/prover.rs @@ -0,0 +1,442 @@ +#![allow(unused_parens)] +#![allow(unused_imports)] +use itertools::{chain, zip_eq, Itertools}; +use num_traits::{One, Zero}; +use prover_types::cpu::*; +use prover_types::simd::*; +use stwo_prover::constraint_framework::logup::LogupTraceGenerator; +use stwo_prover::constraint_framework::Relation; +use stwo_prover::core::air::Component; +use stwo_prover::core::backend::simd::column::BaseColumn; +use stwo_prover::core::backend::simd::conversion::Unpack; +use stwo_prover::core::backend::simd::m31::{PackedM31, LOG_N_LANES, N_LANES}; +use stwo_prover::core::backend::simd::qm31::PackedQM31; +use stwo_prover::core::backend::simd::SimdBackend; +use stwo_prover::core::backend::{Col, Column}; +use stwo_prover::core::fields::m31::M31; +use stwo_prover::core::pcs::TreeBuilder; +use stwo_prover::core::poly::circle::{CanonicCoset, CircleEvaluation}; +use stwo_prover::core::poly::BitReversedOrder; +use stwo_prover::core::utils::bit_reverse_coset_to_circle_domain_order; +use stwo_prover::core::vcs::blake2_merkle::{Blake2sMerkleChannel, Blake2sMerkleHasher}; + +use super::component::{Claim, InteractionClaim}; +use crate::components::{memory_address_to_id, memory_id_to_big, pack_values, verify_instruction}; +use crate::relations; + +pub type InputType = CasmState; +pub type PackedInputType = PackedCasmState; +const N_TRACE_COLUMNS: usize = 11; + +#[derive(Default)] +pub struct ClaimGenerator { + pub inputs: Vec, +} +impl ClaimGenerator { + pub fn new(inputs: Vec) -> Self { + Self { inputs } + } + + pub fn write_trace( + mut self, + tree_builder: &mut TreeBuilder<'_, '_, SimdBackend, Blake2sMerkleChannel>, + memory_address_to_id_state: &mut memory_address_to_id::ClaimGenerator, + memory_id_to_big_state: &mut memory_id_to_big::ClaimGenerator, + verify_instruction_state: &mut verify_instruction::ClaimGenerator, + ) -> (Claim, InteractionClaimGenerator) { + let n_calls = self.inputs.len(); + assert_ne!(n_calls, 0); + let size = std::cmp::max(n_calls.next_power_of_two(), N_LANES); + let need_padding = n_calls != size; + + if need_padding { + self.inputs.resize(size, *self.inputs.first().unwrap()); + bit_reverse_coset_to_circle_domain_order(&mut self.inputs); + } + + let packed_inputs = pack_values(&self.inputs); + let (trace, mut sub_components_inputs, lookup_data) = write_trace_simd( + packed_inputs, + memory_address_to_id_state, + memory_id_to_big_state, + ); + + if need_padding { + sub_components_inputs.bit_reverse_coset_to_circle_domain_order(); + } + sub_components_inputs + .memory_address_to_id_inputs + .iter() + .for_each(|inputs| { + memory_address_to_id_state.add_inputs(&inputs[..n_calls]); + }); + sub_components_inputs + .memory_id_to_big_inputs + .iter() + .for_each(|inputs| { + memory_id_to_big_state.add_inputs(&inputs[..n_calls]); + }); + sub_components_inputs + .verify_instruction_inputs + .iter() + .for_each(|inputs| { + verify_instruction_state.add_inputs(&inputs[..n_calls]); + }); + + tree_builder.extend_evals( + trace + .into_iter() + .map(|eval| { + let domain = CanonicCoset::new( + eval.len() + .checked_ilog2() + .expect("Input is not a power of 2!"), + ) + .circle_domain(); + CircleEvaluation::::new(domain, eval) + }) + .collect_vec(), + ); + + ( + Claim { n_calls }, + InteractionClaimGenerator { + n_calls, + lookup_data, + }, + ) + } + + pub fn add_inputs(&mut self, inputs: &[InputType]) { + self.inputs.extend(inputs); + } +} + +pub struct SubComponentInputs { + pub memory_address_to_id_inputs: [Vec; 1], + pub memory_id_to_big_inputs: [Vec; 1], + pub verify_instruction_inputs: [Vec; 1], +} +impl SubComponentInputs { + #[allow(unused_variables)] + fn with_capacity(capacity: usize) -> Self { + Self { + memory_address_to_id_inputs: [Vec::with_capacity(capacity)], + memory_id_to_big_inputs: [Vec::with_capacity(capacity)], + verify_instruction_inputs: [Vec::with_capacity(capacity)], + } + } + + fn bit_reverse_coset_to_circle_domain_order(&mut self) { + self.memory_address_to_id_inputs + .iter_mut() + .for_each(|vec| bit_reverse_coset_to_circle_domain_order(vec)); + self.memory_id_to_big_inputs + .iter_mut() + .for_each(|vec| bit_reverse_coset_to_circle_domain_order(vec)); + self.verify_instruction_inputs + .iter_mut() + .for_each(|vec| bit_reverse_coset_to_circle_domain_order(vec)); + } +} + +#[allow(clippy::useless_conversion)] +#[allow(unused_variables)] +#[allow(clippy::double_parens)] +#[allow(non_snake_case)] +pub fn write_trace_simd( + inputs: Vec, + memory_address_to_id_state: &mut memory_address_to_id::ClaimGenerator, + memory_id_to_big_state: &mut memory_id_to_big::ClaimGenerator, +) -> ( + [BaseColumn; N_TRACE_COLUMNS], + SubComponentInputs, + LookupData, +) { + const N_TRACE_COLUMNS: usize = 11; + let mut trace: [_; N_TRACE_COLUMNS] = + std::array::from_fn(|_| Col::::zeros(inputs.len() * N_LANES)); + + let mut lookup_data = LookupData::with_capacity(inputs.len()); + #[allow(unused_mut)] + let mut sub_components_inputs = SubComponentInputs::with_capacity(inputs.len()); + + let M31_0 = PackedM31::broadcast(M31::from(0)); + let M31_1 = PackedM31::broadcast(M31::from(1)); + let M31_262144 = PackedM31::broadcast(M31::from(262144)); + let M31_32767 = PackedM31::broadcast(M31::from(32767)); + let M31_32768 = PackedM31::broadcast(M31::from(32768)); + let M31_512 = PackedM31::broadcast(M31::from(512)); + let UInt16_1 = PackedUInt16::broadcast(UInt16::from(1)); + let UInt16_11 = PackedUInt16::broadcast(UInt16::from(11)); + let UInt16_13 = PackedUInt16::broadcast(UInt16::from(13)); + let UInt16_3 = PackedUInt16::broadcast(UInt16::from(3)); + let UInt16_4 = PackedUInt16::broadcast(UInt16::from(4)); + let UInt16_5 = PackedUInt16::broadcast(UInt16::from(5)); + let UInt16_6 = PackedUInt16::broadcast(UInt16::from(6)); + let UInt16_7 = PackedUInt16::broadcast(UInt16::from(7)); + + inputs.into_iter().enumerate().for_each( + |(row_index, jump_opcode_is_rel_f_is_imm_f_is_double_deref_f_input)| { + let input_tmp_1315 = jump_opcode_is_rel_f_is_imm_f_is_double_deref_f_input; + let input_pc_col0 = input_tmp_1315.pc; + trace[0].data[row_index] = input_pc_col0; + let input_ap_col1 = input_tmp_1315.ap; + trace[1].data[row_index] = input_ap_col1; + let input_fp_col2 = input_tmp_1315.fp; + trace[2].data[row_index] = input_fp_col2; + + // decode_instruction_ff344370bb4f7f54. + + let memory_address_to_id_value_tmp_1323 = + memory_address_to_id_state.deduce_output(input_pc_col0); + let memory_id_to_big_value_tmp_1324 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1323); + let offset2_tmp_1325 = + ((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1324.get_m31(3))) + >> (UInt16_5)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1324.get_m31(4))) + << (UInt16_4))) + + (((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1324.get_m31(5))) + & (UInt16_7)) + << (UInt16_13))); + let offset2_col3 = offset2_tmp_1325.as_m31(); + trace[3].data[row_index] = offset2_col3; + let op1_base_fp_tmp_1326 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1324.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1324.get_m31(6))) + << (UInt16_6))) + >> (UInt16_3)) + & (UInt16_1)); + let op1_base_fp_col4 = op1_base_fp_tmp_1326.as_m31(); + trace[4].data[row_index] = op1_base_fp_col4; + let op1_base_ap_tmp_1327 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1324.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1324.get_m31(6))) + << (UInt16_6))) + >> (UInt16_4)) + & (UInt16_1)); + let op1_base_ap_col5 = op1_base_ap_tmp_1327.as_m31(); + trace[5].data[row_index] = op1_base_ap_col5; + let ap_update_add_1_tmp_1328 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1324.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1324.get_m31(6))) + << (UInt16_6))) + >> (UInt16_11)) + & (UInt16_1)); + let ap_update_add_1_col6 = ap_update_add_1_tmp_1328.as_m31(); + trace[6].data[row_index] = ap_update_add_1_col6; + + sub_components_inputs.verify_instruction_inputs[0].extend( + ( + input_pc_col0, + [M31_32767, M31_32767, offset2_col3], + [ + M31_1, + M31_1, + M31_0, + op1_base_fp_col4, + op1_base_ap_col5, + M31_0, + M31_0, + M31_1, + M31_0, + M31_0, + M31_0, + ap_update_add_1_col6, + M31_0, + M31_0, + M31_0, + ], + ) + .unpack(), + ); + + lookup_data.verifyinstruction[0].push([ + input_pc_col0, + M31_32767, + M31_32767, + offset2_col3, + M31_1, + M31_1, + M31_0, + op1_base_fp_col4, + op1_base_ap_col5, + M31_0, + M31_0, + M31_1, + M31_0, + M31_0, + M31_0, + ap_update_add_1_col6, + M31_0, + M31_0, + M31_0, + ]); + + // read_positive_num_bits_27. + + let memory_address_to_id_value_tmp_1330 = memory_address_to_id_state.deduce_output( + ((((op1_base_fp_col4) * (input_fp_col2)) + ((op1_base_ap_col5) * (input_ap_col1))) + + ((offset2_col3) - (M31_32768))), + ); + let memory_id_to_big_value_tmp_1331 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1330); + let next_pc_id_col7 = memory_address_to_id_value_tmp_1330; + trace[7].data[row_index] = next_pc_id_col7; + sub_components_inputs.memory_address_to_id_inputs[0].extend( + ((((op1_base_fp_col4) * (input_fp_col2)) + ((op1_base_ap_col5) * (input_ap_col1))) + + ((offset2_col3) - (M31_32768))) + .unpack(), + ); + + lookup_data.memoryaddresstoid[0].push([ + ((((op1_base_fp_col4) * (input_fp_col2)) + ((op1_base_ap_col5) * (input_ap_col1))) + + ((offset2_col3) - (M31_32768))), + next_pc_id_col7, + ]); + let next_pc_limb_0_col8 = memory_id_to_big_value_tmp_1331.get_m31(0); + trace[8].data[row_index] = next_pc_limb_0_col8; + let next_pc_limb_1_col9 = memory_id_to_big_value_tmp_1331.get_m31(1); + trace[9].data[row_index] = next_pc_limb_1_col9; + let next_pc_limb_2_col10 = memory_id_to_big_value_tmp_1331.get_m31(2); + trace[10].data[row_index] = next_pc_limb_2_col10; + sub_components_inputs.memory_id_to_big_inputs[0].extend(next_pc_id_col7.unpack()); + + lookup_data.memoryidtobig[0].push([ + next_pc_id_col7, + next_pc_limb_0_col8, + next_pc_limb_1_col9, + next_pc_limb_2_col10, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + ]); + + lookup_data.opcodes[0].push([input_pc_col0, input_ap_col1, input_fp_col2]); + lookup_data.opcodes[1].push([ + (((next_pc_limb_0_col8) + ((next_pc_limb_1_col9) * (M31_512))) + + ((next_pc_limb_2_col10) * (M31_262144))), + ((input_ap_col1) + (ap_update_add_1_col6)), + input_fp_col2, + ]); + }, + ); + + (trace, sub_components_inputs, lookup_data) +} + +pub struct LookupData { + pub memoryaddresstoid: [Vec<[PackedM31; 2]>; 1], + pub memoryidtobig: [Vec<[PackedM31; 29]>; 1], + pub opcodes: [Vec<[PackedM31; 3]>; 2], + pub verifyinstruction: [Vec<[PackedM31; 19]>; 1], +} +impl LookupData { + #[allow(unused_variables)] + fn with_capacity(capacity: usize) -> Self { + Self { + memoryaddresstoid: [Vec::with_capacity(capacity)], + memoryidtobig: [Vec::with_capacity(capacity)], + opcodes: [Vec::with_capacity(capacity), Vec::with_capacity(capacity)], + verifyinstruction: [Vec::with_capacity(capacity)], + } + } +} + +pub struct InteractionClaimGenerator { + pub n_calls: usize, + pub lookup_data: LookupData, +} +impl InteractionClaimGenerator { + pub fn write_interaction_trace( + self, + tree_builder: &mut TreeBuilder<'_, '_, SimdBackend, Blake2sMerkleChannel>, + memoryaddresstoid_lookup_elements: &relations::MemoryAddressToId, + memoryidtobig_lookup_elements: &relations::MemoryIdToBig, + opcodes_lookup_elements: &relations::Opcodes, + verifyinstruction_lookup_elements: &relations::VerifyInstruction, + ) -> InteractionClaim { + let log_size = std::cmp::max(self.n_calls.next_power_of_two().ilog2(), LOG_N_LANES); + let mut logup_gen = LogupTraceGenerator::new(log_size); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.verifyinstruction[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = verifyinstruction_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.memoryaddresstoid[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = memoryaddresstoid_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.memoryidtobig[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = memoryidtobig_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.opcodes[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = opcodes_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.opcodes[1]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = opcodes_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, -PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let (trace, total_sum, claimed_sum) = if self.n_calls == 1 << log_size { + let (trace, claimed_sum) = logup_gen.finalize_last(); + (trace, claimed_sum, None) + } else { + let (trace, [total_sum, claimed_sum]) = + logup_gen.finalize_at([(1 << log_size) - 1, self.n_calls - 1]); + (trace, total_sum, Some((claimed_sum, self.n_calls - 1))) + }; + tree_builder.extend_evals(trace); + + InteractionClaim { + logup_sums: (total_sum, claimed_sum), + } + } +} diff --git a/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_f_is_imm_f_is_double_deref_t/component.rs b/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_f_is_imm_f_is_double_deref_t/component.rs new file mode 100644 index 00000000..66325edd --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_f_is_imm_f_is_double_deref_t/component.rs @@ -0,0 +1,198 @@ +#![allow(non_camel_case_types)] +#![allow(unused_imports)] +use num_traits::{One, Zero}; +use serde::{Deserialize, Serialize}; +use stwo_prover::constraint_framework::logup::{LogupAtRow, LogupSums, LookupElements}; +use stwo_prover::constraint_framework::{ + EvalAtRow, FrameworkComponent, FrameworkEval, RelationEntry, +}; +use stwo_prover::core::backend::simd::m31::LOG_N_LANES; +use stwo_prover::core::channel::Channel; +use stwo_prover::core::fields::m31::M31; +use stwo_prover::core::fields::qm31::SecureField; +use stwo_prover::core::fields::secure_column::SECURE_EXTENSION_DEGREE; +use stwo_prover::core::pcs::TreeVec; + +use crate::relations; + +pub struct Eval { + pub claim: Claim, + pub memoryaddresstoid_lookup_elements: relations::MemoryAddressToId, + pub memoryidtobig_lookup_elements: relations::MemoryIdToBig, + pub opcodes_lookup_elements: relations::Opcodes, + pub verifyinstruction_lookup_elements: relations::VerifyInstruction, +} + +#[derive(Copy, Clone, Serialize, Deserialize)] +pub struct Claim { + pub n_calls: usize, +} +impl Claim { + pub fn log_sizes(&self) -> TreeVec> { + let log_size = std::cmp::max(self.n_calls.next_power_of_two().ilog2(), LOG_N_LANES); + let trace_log_sizes = vec![log_size; 15]; + let interaction_log_sizes = vec![log_size; SECURE_EXTENSION_DEGREE * 7]; + let preprocessed_log_sizes = vec![log_size]; + TreeVec::new(vec![ + preprocessed_log_sizes, + trace_log_sizes, + interaction_log_sizes, + ]) + } + + pub fn mix_into(&self, channel: &mut impl Channel) { + channel.mix_u64(self.n_calls as u64); + } +} + +#[derive(Copy, Clone, Serialize, Deserialize)] +pub struct InteractionClaim { + pub logup_sums: LogupSums, +} +impl InteractionClaim { + pub fn mix_into(&self, channel: &mut impl Channel) { + let (total_sum, claimed_sum) = self.logup_sums; + channel.mix_felts(&[total_sum]); + if let Some(claimed_sum) = claimed_sum { + channel.mix_felts(&[claimed_sum.0]); + channel.mix_u64(claimed_sum.1 as u64); + } + } +} + +pub type Component = FrameworkComponent; + +impl FrameworkEval for Eval { + fn log_size(&self) -> u32 { + std::cmp::max(self.claim.n_calls.next_power_of_two().ilog2(), LOG_N_LANES) + } + + fn max_constraint_log_degree_bound(&self) -> u32 { + self.log_size() + 1 + } + + #[allow(unused_parens)] + #[allow(clippy::double_parens)] + #[allow(non_snake_case)] + fn evaluate(&self, mut eval: E) -> E { + let M31_0 = E::F::from(M31::from(0)); + let M31_1 = E::F::from(M31::from(1)); + let M31_262144 = E::F::from(M31::from(262144)); + let M31_32767 = E::F::from(M31::from(32767)); + let M31_32768 = E::F::from(M31::from(32768)); + let M31_512 = E::F::from(M31::from(512)); + let input_pc_col0 = eval.next_trace_mask(); + let input_ap_col1 = eval.next_trace_mask(); + let input_fp_col2 = eval.next_trace_mask(); + let offset1_col3 = eval.next_trace_mask(); + let offset2_col4 = eval.next_trace_mask(); + let op0_base_fp_col5 = eval.next_trace_mask(); + let ap_update_add_1_col6 = eval.next_trace_mask(); + let mem1_base_id_col7 = eval.next_trace_mask(); + let mem1_base_limb_0_col8 = eval.next_trace_mask(); + let mem1_base_limb_1_col9 = eval.next_trace_mask(); + let mem1_base_limb_2_col10 = eval.next_trace_mask(); + let next_pc_id_col11 = eval.next_trace_mask(); + let next_pc_limb_0_col12 = eval.next_trace_mask(); + let next_pc_limb_1_col13 = eval.next_trace_mask(); + let next_pc_limb_2_col14 = eval.next_trace_mask(); + + // decode_instruction_d5cc27a6f788af1d. + + eval.add_to_relation(&[RelationEntry::new( + &self.verifyinstruction_lookup_elements, + E::EF::one(), + &[ + input_pc_col0.clone(), + M31_32767.clone(), + offset1_col3.clone(), + offset2_col4.clone(), + M31_1.clone(), + op0_base_fp_col5.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_1.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + ap_update_add_1_col6.clone(), + ], + )]); + + // read_positive_num_bits_27. + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryaddresstoid_lookup_elements, + E::EF::one(), + &[ + (((op0_base_fp_col5.clone() * input_fp_col2.clone()) + + ((M31_1.clone() - op0_base_fp_col5.clone()) * input_ap_col1.clone())) + + (offset1_col3.clone() - M31_32768.clone())), + mem1_base_id_col7.clone(), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryidtobig_lookup_elements, + E::EF::one(), + &[ + mem1_base_id_col7.clone(), + mem1_base_limb_0_col8.clone(), + mem1_base_limb_1_col9.clone(), + mem1_base_limb_2_col10.clone(), + ], + )]); + + // read_positive_num_bits_27. + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryaddresstoid_lookup_elements, + E::EF::one(), + &[ + (((mem1_base_limb_0_col8.clone() + + (mem1_base_limb_1_col9.clone() * M31_512.clone())) + + (mem1_base_limb_2_col10.clone() * M31_262144.clone())) + + (offset2_col4.clone() - M31_32768.clone())), + next_pc_id_col11.clone(), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryidtobig_lookup_elements, + E::EF::one(), + &[ + next_pc_id_col11.clone(), + next_pc_limb_0_col12.clone(), + next_pc_limb_1_col13.clone(), + next_pc_limb_2_col14.clone(), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.opcodes_lookup_elements, + E::EF::one(), + &[ + input_pc_col0.clone(), + input_ap_col1.clone(), + input_fp_col2.clone(), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.opcodes_lookup_elements, + -E::EF::one(), + &[ + ((next_pc_limb_0_col12.clone() + (next_pc_limb_1_col13.clone() * M31_512.clone())) + + (next_pc_limb_2_col14.clone() * M31_262144.clone())), + (input_ap_col1.clone() + ap_update_add_1_col6.clone()), + input_fp_col2.clone(), + ], + )]); + + eval.finalize_logup(); + eval + } +} diff --git a/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_f_is_imm_f_is_double_deref_t/mod.rs b/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_f_is_imm_f_is_double_deref_t/mod.rs new file mode 100644 index 00000000..3f7a8d74 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_f_is_imm_f_is_double_deref_t/mod.rs @@ -0,0 +1,5 @@ +pub mod component; +pub mod prover; + +pub use component::{Claim, Component, Eval, InteractionClaim}; +pub use prover::{ClaimGenerator, InputType, InteractionClaimGenerator}; diff --git a/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_f_is_imm_f_is_double_deref_t/prover.rs b/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_f_is_imm_f_is_double_deref_t/prover.rs new file mode 100644 index 00000000..05e3bcb4 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_f_is_imm_f_is_double_deref_t/prover.rs @@ -0,0 +1,531 @@ +#![allow(unused_parens)] +#![allow(unused_imports)] +use itertools::{chain, zip_eq, Itertools}; +use num_traits::{One, Zero}; +use prover_types::cpu::*; +use prover_types::simd::*; +use stwo_prover::constraint_framework::logup::LogupTraceGenerator; +use stwo_prover::constraint_framework::Relation; +use stwo_prover::core::air::Component; +use stwo_prover::core::backend::simd::column::BaseColumn; +use stwo_prover::core::backend::simd::conversion::Unpack; +use stwo_prover::core::backend::simd::m31::{PackedM31, LOG_N_LANES, N_LANES}; +use stwo_prover::core::backend::simd::qm31::PackedQM31; +use stwo_prover::core::backend::simd::SimdBackend; +use stwo_prover::core::backend::{Col, Column}; +use stwo_prover::core::fields::m31::M31; +use stwo_prover::core::pcs::TreeBuilder; +use stwo_prover::core::poly::circle::{CanonicCoset, CircleEvaluation}; +use stwo_prover::core::poly::BitReversedOrder; +use stwo_prover::core::utils::bit_reverse_coset_to_circle_domain_order; +use stwo_prover::core::vcs::blake2_merkle::{Blake2sMerkleChannel, Blake2sMerkleHasher}; + +use super::component::{Claim, InteractionClaim}; +use crate::components::{memory_address_to_id, memory_id_to_big, pack_values, verify_instruction}; +use crate::relations; + +pub type InputType = CasmState; +pub type PackedInputType = PackedCasmState; +const N_TRACE_COLUMNS: usize = 15; + +#[derive(Default)] +pub struct ClaimGenerator { + pub inputs: Vec, +} +impl ClaimGenerator { + pub fn new(inputs: Vec) -> Self { + Self { inputs } + } + + pub fn write_trace( + mut self, + tree_builder: &mut TreeBuilder<'_, '_, SimdBackend, Blake2sMerkleChannel>, + memory_address_to_id_state: &mut memory_address_to_id::ClaimGenerator, + memory_id_to_big_state: &mut memory_id_to_big::ClaimGenerator, + verify_instruction_state: &mut verify_instruction::ClaimGenerator, + ) -> (Claim, InteractionClaimGenerator) { + let n_calls = self.inputs.len(); + assert_ne!(n_calls, 0); + let size = std::cmp::max(n_calls.next_power_of_two(), N_LANES); + let need_padding = n_calls != size; + + if need_padding { + self.inputs.resize(size, *self.inputs.first().unwrap()); + bit_reverse_coset_to_circle_domain_order(&mut self.inputs); + } + + let packed_inputs = pack_values(&self.inputs); + let (trace, mut sub_components_inputs, lookup_data) = write_trace_simd( + packed_inputs, + memory_address_to_id_state, + memory_id_to_big_state, + ); + + if need_padding { + sub_components_inputs.bit_reverse_coset_to_circle_domain_order(); + } + sub_components_inputs + .memory_address_to_id_inputs + .iter() + .for_each(|inputs| { + memory_address_to_id_state.add_inputs(&inputs[..n_calls]); + }); + sub_components_inputs + .memory_id_to_big_inputs + .iter() + .for_each(|inputs| { + memory_id_to_big_state.add_inputs(&inputs[..n_calls]); + }); + sub_components_inputs + .verify_instruction_inputs + .iter() + .for_each(|inputs| { + verify_instruction_state.add_inputs(&inputs[..n_calls]); + }); + + tree_builder.extend_evals( + trace + .into_iter() + .map(|eval| { + let domain = CanonicCoset::new( + eval.len() + .checked_ilog2() + .expect("Input is not a power of 2!"), + ) + .circle_domain(); + CircleEvaluation::::new(domain, eval) + }) + .collect_vec(), + ); + + ( + Claim { n_calls }, + InteractionClaimGenerator { + n_calls, + lookup_data, + }, + ) + } + + pub fn add_inputs(&mut self, inputs: &[InputType]) { + self.inputs.extend(inputs); + } +} + +pub struct SubComponentInputs { + pub memory_address_to_id_inputs: [Vec; 2], + pub memory_id_to_big_inputs: [Vec; 2], + pub verify_instruction_inputs: [Vec; 1], +} +impl SubComponentInputs { + #[allow(unused_variables)] + fn with_capacity(capacity: usize) -> Self { + Self { + memory_address_to_id_inputs: [ + Vec::with_capacity(capacity), + Vec::with_capacity(capacity), + ], + memory_id_to_big_inputs: [Vec::with_capacity(capacity), Vec::with_capacity(capacity)], + verify_instruction_inputs: [Vec::with_capacity(capacity)], + } + } + + fn bit_reverse_coset_to_circle_domain_order(&mut self) { + self.memory_address_to_id_inputs + .iter_mut() + .for_each(|vec| bit_reverse_coset_to_circle_domain_order(vec)); + self.memory_id_to_big_inputs + .iter_mut() + .for_each(|vec| bit_reverse_coset_to_circle_domain_order(vec)); + self.verify_instruction_inputs + .iter_mut() + .for_each(|vec| bit_reverse_coset_to_circle_domain_order(vec)); + } +} + +#[allow(clippy::useless_conversion)] +#[allow(unused_variables)] +#[allow(clippy::double_parens)] +#[allow(non_snake_case)] +pub fn write_trace_simd( + inputs: Vec, + memory_address_to_id_state: &mut memory_address_to_id::ClaimGenerator, + memory_id_to_big_state: &mut memory_id_to_big::ClaimGenerator, +) -> ( + [BaseColumn; N_TRACE_COLUMNS], + SubComponentInputs, + LookupData, +) { + const N_TRACE_COLUMNS: usize = 15; + let mut trace: [_; N_TRACE_COLUMNS] = + std::array::from_fn(|_| Col::::zeros(inputs.len() * N_LANES)); + + let mut lookup_data = LookupData::with_capacity(inputs.len()); + #[allow(unused_mut)] + let mut sub_components_inputs = SubComponentInputs::with_capacity(inputs.len()); + + let M31_0 = PackedM31::broadcast(M31::from(0)); + let M31_1 = PackedM31::broadcast(M31::from(1)); + let M31_262144 = PackedM31::broadcast(M31::from(262144)); + let M31_32767 = PackedM31::broadcast(M31::from(32767)); + let M31_32768 = PackedM31::broadcast(M31::from(32768)); + let M31_512 = PackedM31::broadcast(M31::from(512)); + let UInt16_1 = PackedUInt16::broadcast(UInt16::from(1)); + let UInt16_11 = PackedUInt16::broadcast(UInt16::from(11)); + let UInt16_13 = PackedUInt16::broadcast(UInt16::from(13)); + let UInt16_2 = PackedUInt16::broadcast(UInt16::from(2)); + let UInt16_3 = PackedUInt16::broadcast(UInt16::from(3)); + let UInt16_31 = PackedUInt16::broadcast(UInt16::from(31)); + let UInt16_4 = PackedUInt16::broadcast(UInt16::from(4)); + let UInt16_5 = PackedUInt16::broadcast(UInt16::from(5)); + let UInt16_6 = PackedUInt16::broadcast(UInt16::from(6)); + let UInt16_7 = PackedUInt16::broadcast(UInt16::from(7)); + + inputs.into_iter().enumerate().for_each( + |(row_index, jump_opcode_is_rel_f_is_imm_f_is_double_deref_t_input)| { + let input_tmp_1296 = jump_opcode_is_rel_f_is_imm_f_is_double_deref_t_input; + let input_pc_col0 = input_tmp_1296.pc; + trace[0].data[row_index] = input_pc_col0; + let input_ap_col1 = input_tmp_1296.ap; + trace[1].data[row_index] = input_ap_col1; + let input_fp_col2 = input_tmp_1296.fp; + trace[2].data[row_index] = input_fp_col2; + + // decode_instruction_d5cc27a6f788af1d. + + let memory_address_to_id_value_tmp_1304 = + memory_address_to_id_state.deduce_output(input_pc_col0); + let memory_id_to_big_value_tmp_1305 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1304); + let offset1_tmp_1306 = + ((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1305.get_m31(1))) + >> (UInt16_7)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1305.get_m31(2))) + << (UInt16_2))) + + (((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1305.get_m31(3))) + & (UInt16_31)) + << (UInt16_11))); + let offset1_col3 = offset1_tmp_1306.as_m31(); + trace[3].data[row_index] = offset1_col3; + let offset2_tmp_1307 = + ((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1305.get_m31(3))) + >> (UInt16_5)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1305.get_m31(4))) + << (UInt16_4))) + + (((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1305.get_m31(5))) + & (UInt16_7)) + << (UInt16_13))); + let offset2_col4 = offset2_tmp_1307.as_m31(); + trace[4].data[row_index] = offset2_col4; + let op0_base_fp_tmp_1308 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1305.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1305.get_m31(6))) + << (UInt16_6))) + >> (UInt16_1)) + & (UInt16_1)); + let op0_base_fp_col5 = op0_base_fp_tmp_1308.as_m31(); + trace[5].data[row_index] = op0_base_fp_col5; + let ap_update_add_1_tmp_1309 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1305.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1305.get_m31(6))) + << (UInt16_6))) + >> (UInt16_11)) + & (UInt16_1)); + let ap_update_add_1_col6 = ap_update_add_1_tmp_1309.as_m31(); + trace[6].data[row_index] = ap_update_add_1_col6; + + sub_components_inputs.verify_instruction_inputs[0].extend( + ( + input_pc_col0, + [M31_32767, offset1_col3, offset2_col4], + [ + M31_1, + op0_base_fp_col5, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_1, + M31_0, + M31_0, + M31_0, + ap_update_add_1_col6, + M31_0, + M31_0, + M31_0, + ], + ) + .unpack(), + ); + + lookup_data.verifyinstruction[0].push([ + input_pc_col0, + M31_32767, + offset1_col3, + offset2_col4, + M31_1, + op0_base_fp_col5, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_1, + M31_0, + M31_0, + M31_0, + ap_update_add_1_col6, + M31_0, + M31_0, + M31_0, + ]); + + // read_positive_num_bits_27. + + let memory_address_to_id_value_tmp_1311 = memory_address_to_id_state.deduce_output( + ((((op0_base_fp_col5) * (input_fp_col2)) + + (((M31_1) - (op0_base_fp_col5)) * (input_ap_col1))) + + ((offset1_col3) - (M31_32768))), + ); + let memory_id_to_big_value_tmp_1312 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1311); + let mem1_base_id_col7 = memory_address_to_id_value_tmp_1311; + trace[7].data[row_index] = mem1_base_id_col7; + sub_components_inputs.memory_address_to_id_inputs[0].extend( + ((((op0_base_fp_col5) * (input_fp_col2)) + + (((M31_1) - (op0_base_fp_col5)) * (input_ap_col1))) + + ((offset1_col3) - (M31_32768))) + .unpack(), + ); + + lookup_data.memoryaddresstoid[0].push([ + ((((op0_base_fp_col5) * (input_fp_col2)) + + (((M31_1) - (op0_base_fp_col5)) * (input_ap_col1))) + + ((offset1_col3) - (M31_32768))), + mem1_base_id_col7, + ]); + let mem1_base_limb_0_col8 = memory_id_to_big_value_tmp_1312.get_m31(0); + trace[8].data[row_index] = mem1_base_limb_0_col8; + let mem1_base_limb_1_col9 = memory_id_to_big_value_tmp_1312.get_m31(1); + trace[9].data[row_index] = mem1_base_limb_1_col9; + let mem1_base_limb_2_col10 = memory_id_to_big_value_tmp_1312.get_m31(2); + trace[10].data[row_index] = mem1_base_limb_2_col10; + sub_components_inputs.memory_id_to_big_inputs[0].extend(mem1_base_id_col7.unpack()); + + lookup_data.memoryidtobig[0].push([ + mem1_base_id_col7, + mem1_base_limb_0_col8, + mem1_base_limb_1_col9, + mem1_base_limb_2_col10, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + ]); + + // read_positive_num_bits_27. + + let memory_address_to_id_value_tmp_1313 = memory_address_to_id_state.deduce_output( + ((((mem1_base_limb_0_col8) + ((mem1_base_limb_1_col9) * (M31_512))) + + ((mem1_base_limb_2_col10) * (M31_262144))) + + ((offset2_col4) - (M31_32768))), + ); + let memory_id_to_big_value_tmp_1314 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1313); + let next_pc_id_col11 = memory_address_to_id_value_tmp_1313; + trace[11].data[row_index] = next_pc_id_col11; + sub_components_inputs.memory_address_to_id_inputs[1].extend( + ((((mem1_base_limb_0_col8) + ((mem1_base_limb_1_col9) * (M31_512))) + + ((mem1_base_limb_2_col10) * (M31_262144))) + + ((offset2_col4) - (M31_32768))) + .unpack(), + ); + + lookup_data.memoryaddresstoid[1].push([ + ((((mem1_base_limb_0_col8) + ((mem1_base_limb_1_col9) * (M31_512))) + + ((mem1_base_limb_2_col10) * (M31_262144))) + + ((offset2_col4) - (M31_32768))), + next_pc_id_col11, + ]); + let next_pc_limb_0_col12 = memory_id_to_big_value_tmp_1314.get_m31(0); + trace[12].data[row_index] = next_pc_limb_0_col12; + let next_pc_limb_1_col13 = memory_id_to_big_value_tmp_1314.get_m31(1); + trace[13].data[row_index] = next_pc_limb_1_col13; + let next_pc_limb_2_col14 = memory_id_to_big_value_tmp_1314.get_m31(2); + trace[14].data[row_index] = next_pc_limb_2_col14; + sub_components_inputs.memory_id_to_big_inputs[1].extend(next_pc_id_col11.unpack()); + + lookup_data.memoryidtobig[1].push([ + next_pc_id_col11, + next_pc_limb_0_col12, + next_pc_limb_1_col13, + next_pc_limb_2_col14, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + ]); + + lookup_data.opcodes[0].push([input_pc_col0, input_ap_col1, input_fp_col2]); + lookup_data.opcodes[1].push([ + (((next_pc_limb_0_col12) + ((next_pc_limb_1_col13) * (M31_512))) + + ((next_pc_limb_2_col14) * (M31_262144))), + ((input_ap_col1) + (ap_update_add_1_col6)), + input_fp_col2, + ]); + }, + ); + + (trace, sub_components_inputs, lookup_data) +} + +pub struct LookupData { + pub memoryaddresstoid: [Vec<[PackedM31; 2]>; 2], + pub memoryidtobig: [Vec<[PackedM31; 29]>; 2], + pub opcodes: [Vec<[PackedM31; 3]>; 2], + pub verifyinstruction: [Vec<[PackedM31; 19]>; 1], +} +impl LookupData { + #[allow(unused_variables)] + fn with_capacity(capacity: usize) -> Self { + Self { + memoryaddresstoid: [Vec::with_capacity(capacity), Vec::with_capacity(capacity)], + memoryidtobig: [Vec::with_capacity(capacity), Vec::with_capacity(capacity)], + opcodes: [Vec::with_capacity(capacity), Vec::with_capacity(capacity)], + verifyinstruction: [Vec::with_capacity(capacity)], + } + } +} + +pub struct InteractionClaimGenerator { + pub n_calls: usize, + pub lookup_data: LookupData, +} +impl InteractionClaimGenerator { + pub fn write_interaction_trace( + self, + tree_builder: &mut TreeBuilder<'_, '_, SimdBackend, Blake2sMerkleChannel>, + memoryaddresstoid_lookup_elements: &relations::MemoryAddressToId, + memoryidtobig_lookup_elements: &relations::MemoryIdToBig, + opcodes_lookup_elements: &relations::Opcodes, + verifyinstruction_lookup_elements: &relations::VerifyInstruction, + ) -> InteractionClaim { + let log_size = std::cmp::max(self.n_calls.next_power_of_two().ilog2(), LOG_N_LANES); + let mut logup_gen = LogupTraceGenerator::new(log_size); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.verifyinstruction[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = verifyinstruction_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.memoryaddresstoid[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = memoryaddresstoid_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.memoryidtobig[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = memoryidtobig_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.memoryaddresstoid[1]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = memoryaddresstoid_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.memoryidtobig[1]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = memoryidtobig_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.opcodes[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = opcodes_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.opcodes[1]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = opcodes_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, -PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let (trace, total_sum, claimed_sum) = if self.n_calls == 1 << log_size { + let (trace, claimed_sum) = logup_gen.finalize_last(); + (trace, claimed_sum, None) + } else { + let (trace, [total_sum, claimed_sum]) = + logup_gen.finalize_at([(1 << log_size) - 1, self.n_calls - 1]); + (trace, total_sum, Some((claimed_sum, self.n_calls - 1))) + }; + tree_builder.extend_evals(trace); + + InteractionClaim { + logup_sums: (total_sum, claimed_sum), + } + } +} diff --git a/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_t_is_imm_f_is_double_deref_f/component.rs b/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_t_is_imm_f_is_double_deref_f/component.rs new file mode 100644 index 00000000..5df263b9 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_t_is_imm_f_is_double_deref_f/component.rs @@ -0,0 +1,222 @@ +#![allow(non_camel_case_types)] +#![allow(unused_imports)] +use num_traits::{One, Zero}; +use serde::{Deserialize, Serialize}; +use stwo_prover::constraint_framework::logup::{LogupAtRow, LogupSums, LookupElements}; +use stwo_prover::constraint_framework::{ + EvalAtRow, FrameworkComponent, FrameworkEval, RelationEntry, +}; +use stwo_prover::core::backend::simd::m31::LOG_N_LANES; +use stwo_prover::core::channel::Channel; +use stwo_prover::core::fields::m31::M31; +use stwo_prover::core::fields::qm31::SecureField; +use stwo_prover::core::fields::secure_column::SECURE_EXTENSION_DEGREE; +use stwo_prover::core::pcs::TreeVec; + +use crate::relations; + +pub struct Eval { + pub claim: Claim, + pub memoryaddresstoid_lookup_elements: relations::MemoryAddressToId, + pub memoryidtobig_lookup_elements: relations::MemoryIdToBig, + pub opcodes_lookup_elements: relations::Opcodes, + pub verifyinstruction_lookup_elements: relations::VerifyInstruction, +} + +#[derive(Copy, Clone, Serialize, Deserialize)] +pub struct Claim { + pub n_calls: usize, +} +impl Claim { + pub fn log_sizes(&self) -> TreeVec> { + let log_size = std::cmp::max(self.n_calls.next_power_of_two().ilog2(), LOG_N_LANES); + let trace_log_sizes = vec![log_size; 13]; + let interaction_log_sizes = vec![log_size; SECURE_EXTENSION_DEGREE * 5]; + let preprocessed_log_sizes = vec![log_size]; + TreeVec::new(vec![ + preprocessed_log_sizes, + trace_log_sizes, + interaction_log_sizes, + ]) + } + + pub fn mix_into(&self, channel: &mut impl Channel) { + channel.mix_u64(self.n_calls as u64); + } +} + +#[derive(Copy, Clone, Serialize, Deserialize)] +pub struct InteractionClaim { + pub logup_sums: LogupSums, +} +impl InteractionClaim { + pub fn mix_into(&self, channel: &mut impl Channel) { + let (total_sum, claimed_sum) = self.logup_sums; + channel.mix_felts(&[total_sum]); + if let Some(claimed_sum) = claimed_sum { + channel.mix_felts(&[claimed_sum.0]); + channel.mix_u64(claimed_sum.1 as u64); + } + } +} + +pub type Component = FrameworkComponent; + +impl FrameworkEval for Eval { + fn log_size(&self) -> u32 { + std::cmp::max(self.claim.n_calls.next_power_of_two().ilog2(), LOG_N_LANES) + } + + fn max_constraint_log_degree_bound(&self) -> u32 { + self.log_size() + 1 + } + + #[allow(unused_parens)] + #[allow(clippy::double_parens)] + #[allow(non_snake_case)] + fn evaluate(&self, mut eval: E) -> E { + let M31_0 = E::F::from(M31::from(0)); + let M31_1 = E::F::from(M31::from(1)); + let M31_134217728 = E::F::from(M31::from(134217728)); + let M31_136 = E::F::from(M31::from(136)); + let M31_256 = E::F::from(M31::from(256)); + let M31_262144 = E::F::from(M31::from(262144)); + let M31_32767 = E::F::from(M31::from(32767)); + let M31_32768 = E::F::from(M31::from(32768)); + let M31_511 = E::F::from(M31::from(511)); + let M31_512 = E::F::from(M31::from(512)); + let input_pc_col0 = eval.next_trace_mask(); + let input_ap_col1 = eval.next_trace_mask(); + let input_fp_col2 = eval.next_trace_mask(); + let offset2_col3 = eval.next_trace_mask(); + let op1_base_fp_col4 = eval.next_trace_mask(); + let op1_base_ap_col5 = eval.next_trace_mask(); + let ap_update_add_1_col6 = eval.next_trace_mask(); + let next_pc_id_col7 = eval.next_trace_mask(); + let msb_col8 = eval.next_trace_mask(); + let mid_limbs_set_col9 = eval.next_trace_mask(); + let next_pc_limb_0_col10 = eval.next_trace_mask(); + let next_pc_limb_1_col11 = eval.next_trace_mask(); + let next_pc_limb_2_col12 = eval.next_trace_mask(); + + // decode_instruction_2cd1887fb89e83e3. + + eval.add_to_relation(&[RelationEntry::new( + &self.verifyinstruction_lookup_elements, + E::EF::one(), + &[ + input_pc_col0.clone(), + M31_32767.clone(), + M31_32767.clone(), + offset2_col3.clone(), + M31_1.clone(), + M31_1.clone(), + M31_0.clone(), + op1_base_fp_col4.clone(), + op1_base_ap_col5.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_1.clone(), + M31_0.clone(), + M31_0.clone(), + ap_update_add_1_col6.clone(), + ], + )]); + + // Either flag op1_base_fp is on or flag op1_base_ap is on. + eval.add_constraint( + ((op1_base_fp_col4.clone() + op1_base_ap_col5.clone()) - M31_1.clone()), + ); + + // read_small. + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryaddresstoid_lookup_elements, + E::EF::one(), + &[ + (((op1_base_fp_col4.clone() * input_fp_col2.clone()) + + (op1_base_ap_col5.clone() * input_ap_col1.clone())) + + (offset2_col3.clone() - M31_32768.clone())), + next_pc_id_col7.clone(), + ], + )]); + + // cond_decode_small_sign. + + // msb is a bit. + eval.add_constraint((msb_col8.clone() * (msb_col8.clone() - M31_1.clone()))); + // mid_limbs_set is a bit. + eval.add_constraint( + (mid_limbs_set_col9.clone() * (mid_limbs_set_col9.clone() - M31_1.clone())), + ); + // Cannot have msb equals 0 and mid_limbs_set equals 1. + eval.add_constraint( + ((M31_1.clone() * mid_limbs_set_col9.clone()) * (msb_col8.clone() - M31_1.clone())), + ); + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryidtobig_lookup_elements, + E::EF::one(), + &[ + next_pc_id_col7.clone(), + next_pc_limb_0_col10.clone(), + next_pc_limb_1_col11.clone(), + next_pc_limb_2_col12.clone(), + (mid_limbs_set_col9.clone() * M31_511.clone()), + (mid_limbs_set_col9.clone() * M31_511.clone()), + (mid_limbs_set_col9.clone() * M31_511.clone()), + (mid_limbs_set_col9.clone() * M31_511.clone()), + (mid_limbs_set_col9.clone() * M31_511.clone()), + (mid_limbs_set_col9.clone() * M31_511.clone()), + (mid_limbs_set_col9.clone() * M31_511.clone()), + (mid_limbs_set_col9.clone() * M31_511.clone()), + (mid_limbs_set_col9.clone() * M31_511.clone()), + (mid_limbs_set_col9.clone() * M31_511.clone()), + (mid_limbs_set_col9.clone() * M31_511.clone()), + (mid_limbs_set_col9.clone() * M31_511.clone()), + (mid_limbs_set_col9.clone() * M31_511.clone()), + (mid_limbs_set_col9.clone() * M31_511.clone()), + (mid_limbs_set_col9.clone() * M31_511.clone()), + (mid_limbs_set_col9.clone() * M31_511.clone()), + (mid_limbs_set_col9.clone() * M31_511.clone()), + (mid_limbs_set_col9.clone() * M31_511.clone()), + ((M31_136.clone() * msb_col8.clone()) - mid_limbs_set_col9.clone()), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + (msb_col8.clone() * M31_256.clone()), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.opcodes_lookup_elements, + E::EF::one(), + &[ + input_pc_col0.clone(), + input_ap_col1.clone(), + input_fp_col2.clone(), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.opcodes_lookup_elements, + -E::EF::one(), + &[ + (input_pc_col0.clone() + + ((((next_pc_limb_0_col10.clone() + + (next_pc_limb_1_col11.clone() * M31_512.clone())) + + (next_pc_limb_2_col12.clone() * M31_262144.clone())) + - msb_col8.clone()) + - (M31_134217728.clone() * mid_limbs_set_col9.clone()))), + (input_ap_col1.clone() + ap_update_add_1_col6.clone()), + input_fp_col2.clone(), + ], + )]); + + eval.finalize_logup(); + eval + } +} diff --git a/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_t_is_imm_f_is_double_deref_f/mod.rs b/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_t_is_imm_f_is_double_deref_f/mod.rs new file mode 100644 index 00000000..3f7a8d74 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_t_is_imm_f_is_double_deref_f/mod.rs @@ -0,0 +1,5 @@ +pub mod component; +pub mod prover; + +pub use component::{Claim, Component, Eval, InteractionClaim}; +pub use prover::{ClaimGenerator, InputType, InteractionClaimGenerator}; diff --git a/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_t_is_imm_f_is_double_deref_f/prover.rs b/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_t_is_imm_f_is_double_deref_f/prover.rs new file mode 100644 index 00000000..efe09d6f --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_t_is_imm_f_is_double_deref_f/prover.rs @@ -0,0 +1,459 @@ +#![allow(unused_parens)] +#![allow(unused_imports)] +use itertools::{chain, zip_eq, Itertools}; +use num_traits::{One, Zero}; +use prover_types::cpu::*; +use prover_types::simd::*; +use stwo_prover::constraint_framework::logup::LogupTraceGenerator; +use stwo_prover::constraint_framework::Relation; +use stwo_prover::core::air::Component; +use stwo_prover::core::backend::simd::column::BaseColumn; +use stwo_prover::core::backend::simd::conversion::Unpack; +use stwo_prover::core::backend::simd::m31::{PackedM31, LOG_N_LANES, N_LANES}; +use stwo_prover::core::backend::simd::qm31::PackedQM31; +use stwo_prover::core::backend::simd::SimdBackend; +use stwo_prover::core::backend::{Col, Column}; +use stwo_prover::core::fields::m31::M31; +use stwo_prover::core::pcs::TreeBuilder; +use stwo_prover::core::poly::circle::{CanonicCoset, CircleEvaluation}; +use stwo_prover::core::poly::BitReversedOrder; +use stwo_prover::core::utils::bit_reverse_coset_to_circle_domain_order; +use stwo_prover::core::vcs::blake2_merkle::{Blake2sMerkleChannel, Blake2sMerkleHasher}; + +use super::component::{Claim, InteractionClaim}; +use crate::components::{memory_address_to_id, memory_id_to_big, pack_values, verify_instruction}; +use crate::relations; + +pub type InputType = CasmState; +pub type PackedInputType = PackedCasmState; +const N_TRACE_COLUMNS: usize = 13; + +#[derive(Default)] +pub struct ClaimGenerator { + pub inputs: Vec, +} +impl ClaimGenerator { + pub fn new(inputs: Vec) -> Self { + Self { inputs } + } + + pub fn write_trace( + mut self, + tree_builder: &mut TreeBuilder<'_, '_, SimdBackend, Blake2sMerkleChannel>, + memory_address_to_id_state: &mut memory_address_to_id::ClaimGenerator, + memory_id_to_big_state: &mut memory_id_to_big::ClaimGenerator, + verify_instruction_state: &mut verify_instruction::ClaimGenerator, + ) -> (Claim, InteractionClaimGenerator) { + let n_calls = self.inputs.len(); + assert_ne!(n_calls, 0); + let size = std::cmp::max(n_calls.next_power_of_two(), N_LANES); + let need_padding = n_calls != size; + + if need_padding { + self.inputs.resize(size, *self.inputs.first().unwrap()); + bit_reverse_coset_to_circle_domain_order(&mut self.inputs); + } + + let packed_inputs = pack_values(&self.inputs); + let (trace, mut sub_components_inputs, lookup_data) = write_trace_simd( + packed_inputs, + memory_address_to_id_state, + memory_id_to_big_state, + ); + + if need_padding { + sub_components_inputs.bit_reverse_coset_to_circle_domain_order(); + } + sub_components_inputs + .memory_address_to_id_inputs + .iter() + .for_each(|inputs| { + memory_address_to_id_state.add_inputs(&inputs[..n_calls]); + }); + sub_components_inputs + .memory_id_to_big_inputs + .iter() + .for_each(|inputs| { + memory_id_to_big_state.add_inputs(&inputs[..n_calls]); + }); + sub_components_inputs + .verify_instruction_inputs + .iter() + .for_each(|inputs| { + verify_instruction_state.add_inputs(&inputs[..n_calls]); + }); + + tree_builder.extend_evals( + trace + .into_iter() + .map(|eval| { + let domain = CanonicCoset::new( + eval.len() + .checked_ilog2() + .expect("Input is not a power of 2!"), + ) + .circle_domain(); + CircleEvaluation::::new(domain, eval) + }) + .collect_vec(), + ); + + ( + Claim { n_calls }, + InteractionClaimGenerator { + n_calls, + lookup_data, + }, + ) + } + + pub fn add_inputs(&mut self, inputs: &[InputType]) { + self.inputs.extend(inputs); + } +} + +pub struct SubComponentInputs { + pub memory_address_to_id_inputs: [Vec; 1], + pub memory_id_to_big_inputs: [Vec; 1], + pub verify_instruction_inputs: [Vec; 1], +} +impl SubComponentInputs { + #[allow(unused_variables)] + fn with_capacity(capacity: usize) -> Self { + Self { + memory_address_to_id_inputs: [Vec::with_capacity(capacity)], + memory_id_to_big_inputs: [Vec::with_capacity(capacity)], + verify_instruction_inputs: [Vec::with_capacity(capacity)], + } + } + + fn bit_reverse_coset_to_circle_domain_order(&mut self) { + self.memory_address_to_id_inputs + .iter_mut() + .for_each(|vec| bit_reverse_coset_to_circle_domain_order(vec)); + self.memory_id_to_big_inputs + .iter_mut() + .for_each(|vec| bit_reverse_coset_to_circle_domain_order(vec)); + self.verify_instruction_inputs + .iter_mut() + .for_each(|vec| bit_reverse_coset_to_circle_domain_order(vec)); + } +} + +#[allow(clippy::useless_conversion)] +#[allow(unused_variables)] +#[allow(clippy::double_parens)] +#[allow(non_snake_case)] +pub fn write_trace_simd( + inputs: Vec, + memory_address_to_id_state: &mut memory_address_to_id::ClaimGenerator, + memory_id_to_big_state: &mut memory_id_to_big::ClaimGenerator, +) -> ( + [BaseColumn; N_TRACE_COLUMNS], + SubComponentInputs, + LookupData, +) { + const N_TRACE_COLUMNS: usize = 13; + let mut trace: [_; N_TRACE_COLUMNS] = + std::array::from_fn(|_| Col::::zeros(inputs.len() * N_LANES)); + + let mut lookup_data = LookupData::with_capacity(inputs.len()); + #[allow(unused_mut)] + let mut sub_components_inputs = SubComponentInputs::with_capacity(inputs.len()); + + let M31_0 = PackedM31::broadcast(M31::from(0)); + let M31_1 = PackedM31::broadcast(M31::from(1)); + let M31_134217728 = PackedM31::broadcast(M31::from(134217728)); + let M31_136 = PackedM31::broadcast(M31::from(136)); + let M31_256 = PackedM31::broadcast(M31::from(256)); + let M31_262144 = PackedM31::broadcast(M31::from(262144)); + let M31_32767 = PackedM31::broadcast(M31::from(32767)); + let M31_32768 = PackedM31::broadcast(M31::from(32768)); + let M31_511 = PackedM31::broadcast(M31::from(511)); + let M31_512 = PackedM31::broadcast(M31::from(512)); + let UInt16_1 = PackedUInt16::broadcast(UInt16::from(1)); + let UInt16_11 = PackedUInt16::broadcast(UInt16::from(11)); + let UInt16_13 = PackedUInt16::broadcast(UInt16::from(13)); + let UInt16_3 = PackedUInt16::broadcast(UInt16::from(3)); + let UInt16_4 = PackedUInt16::broadcast(UInt16::from(4)); + let UInt16_5 = PackedUInt16::broadcast(UInt16::from(5)); + let UInt16_6 = PackedUInt16::broadcast(UInt16::from(6)); + let UInt16_7 = PackedUInt16::broadcast(UInt16::from(7)); + + inputs.into_iter().enumerate().for_each( + |(row_index, jump_opcode_is_rel_t_is_imm_f_is_double_deref_f_input)| { + let input_tmp_1277 = jump_opcode_is_rel_t_is_imm_f_is_double_deref_f_input; + let input_pc_col0 = input_tmp_1277.pc; + trace[0].data[row_index] = input_pc_col0; + let input_ap_col1 = input_tmp_1277.ap; + trace[1].data[row_index] = input_ap_col1; + let input_fp_col2 = input_tmp_1277.fp; + trace[2].data[row_index] = input_fp_col2; + + // decode_instruction_2cd1887fb89e83e3. + + let memory_address_to_id_value_tmp_1285 = + memory_address_to_id_state.deduce_output(input_pc_col0); + let memory_id_to_big_value_tmp_1286 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1285); + let offset2_tmp_1287 = + ((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1286.get_m31(3))) + >> (UInt16_5)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1286.get_m31(4))) + << (UInt16_4))) + + (((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1286.get_m31(5))) + & (UInt16_7)) + << (UInt16_13))); + let offset2_col3 = offset2_tmp_1287.as_m31(); + trace[3].data[row_index] = offset2_col3; + let op1_base_fp_tmp_1288 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1286.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1286.get_m31(6))) + << (UInt16_6))) + >> (UInt16_3)) + & (UInt16_1)); + let op1_base_fp_col4 = op1_base_fp_tmp_1288.as_m31(); + trace[4].data[row_index] = op1_base_fp_col4; + let op1_base_ap_tmp_1289 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1286.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1286.get_m31(6))) + << (UInt16_6))) + >> (UInt16_4)) + & (UInt16_1)); + let op1_base_ap_col5 = op1_base_ap_tmp_1289.as_m31(); + trace[5].data[row_index] = op1_base_ap_col5; + let ap_update_add_1_tmp_1290 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1286.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1286.get_m31(6))) + << (UInt16_6))) + >> (UInt16_11)) + & (UInt16_1)); + let ap_update_add_1_col6 = ap_update_add_1_tmp_1290.as_m31(); + trace[6].data[row_index] = ap_update_add_1_col6; + + sub_components_inputs.verify_instruction_inputs[0].extend( + ( + input_pc_col0, + [M31_32767, M31_32767, offset2_col3], + [ + M31_1, + M31_1, + M31_0, + op1_base_fp_col4, + op1_base_ap_col5, + M31_0, + M31_0, + M31_0, + M31_1, + M31_0, + M31_0, + ap_update_add_1_col6, + M31_0, + M31_0, + M31_0, + ], + ) + .unpack(), + ); + + lookup_data.verifyinstruction[0].push([ + input_pc_col0, + M31_32767, + M31_32767, + offset2_col3, + M31_1, + M31_1, + M31_0, + op1_base_fp_col4, + op1_base_ap_col5, + M31_0, + M31_0, + M31_0, + M31_1, + M31_0, + M31_0, + ap_update_add_1_col6, + M31_0, + M31_0, + M31_0, + ]); + + // read_small. + + let memory_address_to_id_value_tmp_1292 = memory_address_to_id_state.deduce_output( + ((((op1_base_fp_col4) * (input_fp_col2)) + ((op1_base_ap_col5) * (input_ap_col1))) + + ((offset2_col3) - (M31_32768))), + ); + let memory_id_to_big_value_tmp_1293 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1292); + let next_pc_id_col7 = memory_address_to_id_value_tmp_1292; + trace[7].data[row_index] = next_pc_id_col7; + sub_components_inputs.memory_address_to_id_inputs[0].extend( + ((((op1_base_fp_col4) * (input_fp_col2)) + ((op1_base_ap_col5) * (input_ap_col1))) + + ((offset2_col3) - (M31_32768))) + .unpack(), + ); + + lookup_data.memoryaddresstoid[0].push([ + ((((op1_base_fp_col4) * (input_fp_col2)) + ((op1_base_ap_col5) * (input_ap_col1))) + + ((offset2_col3) - (M31_32768))), + next_pc_id_col7, + ]); + + // cond_decode_small_sign. + + let msb_tmp_1294 = memory_id_to_big_value_tmp_1293.get_m31(27).eq(M31_256); + let msb_col8 = msb_tmp_1294.as_m31(); + trace[8].data[row_index] = msb_col8; + let mid_limbs_set_tmp_1295 = memory_id_to_big_value_tmp_1293.get_m31(20).eq(M31_511); + let mid_limbs_set_col9 = mid_limbs_set_tmp_1295.as_m31(); + trace[9].data[row_index] = mid_limbs_set_col9; + + let next_pc_limb_0_col10 = memory_id_to_big_value_tmp_1293.get_m31(0); + trace[10].data[row_index] = next_pc_limb_0_col10; + let next_pc_limb_1_col11 = memory_id_to_big_value_tmp_1293.get_m31(1); + trace[11].data[row_index] = next_pc_limb_1_col11; + let next_pc_limb_2_col12 = memory_id_to_big_value_tmp_1293.get_m31(2); + trace[12].data[row_index] = next_pc_limb_2_col12; + sub_components_inputs.memory_id_to_big_inputs[0].extend(next_pc_id_col7.unpack()); + + lookup_data.memoryidtobig[0].push([ + next_pc_id_col7, + next_pc_limb_0_col10, + next_pc_limb_1_col11, + next_pc_limb_2_col12, + ((mid_limbs_set_col9) * (M31_511)), + ((mid_limbs_set_col9) * (M31_511)), + ((mid_limbs_set_col9) * (M31_511)), + ((mid_limbs_set_col9) * (M31_511)), + ((mid_limbs_set_col9) * (M31_511)), + ((mid_limbs_set_col9) * (M31_511)), + ((mid_limbs_set_col9) * (M31_511)), + ((mid_limbs_set_col9) * (M31_511)), + ((mid_limbs_set_col9) * (M31_511)), + ((mid_limbs_set_col9) * (M31_511)), + ((mid_limbs_set_col9) * (M31_511)), + ((mid_limbs_set_col9) * (M31_511)), + ((mid_limbs_set_col9) * (M31_511)), + ((mid_limbs_set_col9) * (M31_511)), + ((mid_limbs_set_col9) * (M31_511)), + ((mid_limbs_set_col9) * (M31_511)), + ((mid_limbs_set_col9) * (M31_511)), + ((mid_limbs_set_col9) * (M31_511)), + (((M31_136) * (msb_col8)) - (mid_limbs_set_col9)), + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + ((msb_col8) * (M31_256)), + ]); + + lookup_data.opcodes[0].push([input_pc_col0, input_ap_col1, input_fp_col2]); + lookup_data.opcodes[1].push([ + ((input_pc_col0) + + (((((next_pc_limb_0_col10) + ((next_pc_limb_1_col11) * (M31_512))) + + ((next_pc_limb_2_col12) * (M31_262144))) + - (msb_col8)) + - ((M31_134217728) * (mid_limbs_set_col9)))), + ((input_ap_col1) + (ap_update_add_1_col6)), + input_fp_col2, + ]); + }, + ); + + (trace, sub_components_inputs, lookup_data) +} + +pub struct LookupData { + pub memoryaddresstoid: [Vec<[PackedM31; 2]>; 1], + pub memoryidtobig: [Vec<[PackedM31; 29]>; 1], + pub opcodes: [Vec<[PackedM31; 3]>; 2], + pub verifyinstruction: [Vec<[PackedM31; 19]>; 1], +} +impl LookupData { + #[allow(unused_variables)] + fn with_capacity(capacity: usize) -> Self { + Self { + memoryaddresstoid: [Vec::with_capacity(capacity)], + memoryidtobig: [Vec::with_capacity(capacity)], + opcodes: [Vec::with_capacity(capacity), Vec::with_capacity(capacity)], + verifyinstruction: [Vec::with_capacity(capacity)], + } + } +} + +pub struct InteractionClaimGenerator { + pub n_calls: usize, + pub lookup_data: LookupData, +} +impl InteractionClaimGenerator { + pub fn write_interaction_trace( + self, + tree_builder: &mut TreeBuilder<'_, '_, SimdBackend, Blake2sMerkleChannel>, + memoryaddresstoid_lookup_elements: &relations::MemoryAddressToId, + memoryidtobig_lookup_elements: &relations::MemoryIdToBig, + opcodes_lookup_elements: &relations::Opcodes, + verifyinstruction_lookup_elements: &relations::VerifyInstruction, + ) -> InteractionClaim { + let log_size = std::cmp::max(self.n_calls.next_power_of_two().ilog2(), LOG_N_LANES); + let mut logup_gen = LogupTraceGenerator::new(log_size); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.verifyinstruction[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = verifyinstruction_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.memoryaddresstoid[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = memoryaddresstoid_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.memoryidtobig[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = memoryidtobig_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.opcodes[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = opcodes_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.opcodes[1]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = opcodes_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, -PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let (trace, total_sum, claimed_sum) = if self.n_calls == 1 << log_size { + let (trace, claimed_sum) = logup_gen.finalize_last(); + (trace, claimed_sum, None) + } else { + let (trace, [total_sum, claimed_sum]) = + logup_gen.finalize_at([(1 << log_size) - 1, self.n_calls - 1]); + (trace, total_sum, Some((claimed_sum, self.n_calls - 1))) + }; + tree_builder.extend_evals(trace); + + InteractionClaim { + logup_sums: (total_sum, claimed_sum), + } + } +} diff --git a/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_t_is_imm_t_is_double_deref_f/component.rs b/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_t_is_imm_t_is_double_deref_f/component.rs new file mode 100644 index 00000000..0f443ab4 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_t_is_imm_t_is_double_deref_f/component.rs @@ -0,0 +1,212 @@ +#![allow(non_camel_case_types)] +#![allow(unused_imports)] +use num_traits::{One, Zero}; +use serde::{Deserialize, Serialize}; +use stwo_prover::constraint_framework::logup::{LogupAtRow, LogupSums, LookupElements}; +use stwo_prover::constraint_framework::{ + EvalAtRow, FrameworkComponent, FrameworkEval, RelationEntry, +}; +use stwo_prover::core::backend::simd::m31::LOG_N_LANES; +use stwo_prover::core::channel::Channel; +use stwo_prover::core::fields::m31::M31; +use stwo_prover::core::fields::qm31::SecureField; +use stwo_prover::core::fields::secure_column::SECURE_EXTENSION_DEGREE; +use stwo_prover::core::pcs::TreeVec; + +use crate::relations; + +pub struct Eval { + pub claim: Claim, + pub memoryaddresstoid_lookup_elements: relations::MemoryAddressToId, + pub memoryidtobig_lookup_elements: relations::MemoryIdToBig, + pub opcodes_lookup_elements: relations::Opcodes, + pub verifyinstruction_lookup_elements: relations::VerifyInstruction, +} + +#[derive(Copy, Clone, Serialize, Deserialize)] +pub struct Claim { + pub n_calls: usize, +} +impl Claim { + pub fn log_sizes(&self) -> TreeVec> { + let log_size = std::cmp::max(self.n_calls.next_power_of_two().ilog2(), LOG_N_LANES); + let trace_log_sizes = vec![log_size; 10]; + let interaction_log_sizes = vec![log_size; SECURE_EXTENSION_DEGREE * 5]; + let preprocessed_log_sizes = vec![log_size]; + TreeVec::new(vec![ + preprocessed_log_sizes, + trace_log_sizes, + interaction_log_sizes, + ]) + } + + pub fn mix_into(&self, channel: &mut impl Channel) { + channel.mix_u64(self.n_calls as u64); + } +} + +#[derive(Copy, Clone, Serialize, Deserialize)] +pub struct InteractionClaim { + pub logup_sums: LogupSums, +} +impl InteractionClaim { + pub fn mix_into(&self, channel: &mut impl Channel) { + let (total_sum, claimed_sum) = self.logup_sums; + channel.mix_felts(&[total_sum]); + if let Some(claimed_sum) = claimed_sum { + channel.mix_felts(&[claimed_sum.0]); + channel.mix_u64(claimed_sum.1 as u64); + } + } +} + +pub type Component = FrameworkComponent; + +impl FrameworkEval for Eval { + fn log_size(&self) -> u32 { + std::cmp::max(self.claim.n_calls.next_power_of_two().ilog2(), LOG_N_LANES) + } + + fn max_constraint_log_degree_bound(&self) -> u32 { + self.log_size() + 1 + } + + #[allow(unused_parens)] + #[allow(clippy::double_parens)] + #[allow(non_snake_case)] + fn evaluate(&self, mut eval: E) -> E { + let M31_0 = E::F::from(M31::from(0)); + let M31_1 = E::F::from(M31::from(1)); + let M31_134217728 = E::F::from(M31::from(134217728)); + let M31_136 = E::F::from(M31::from(136)); + let M31_256 = E::F::from(M31::from(256)); + let M31_262144 = E::F::from(M31::from(262144)); + let M31_32767 = E::F::from(M31::from(32767)); + let M31_32769 = E::F::from(M31::from(32769)); + let M31_511 = E::F::from(M31::from(511)); + let M31_512 = E::F::from(M31::from(512)); + let input_pc_col0 = eval.next_trace_mask(); + let input_ap_col1 = eval.next_trace_mask(); + let input_fp_col2 = eval.next_trace_mask(); + let ap_update_add_1_col3 = eval.next_trace_mask(); + let next_pc_id_col4 = eval.next_trace_mask(); + let msb_col5 = eval.next_trace_mask(); + let mid_limbs_set_col6 = eval.next_trace_mask(); + let next_pc_limb_0_col7 = eval.next_trace_mask(); + let next_pc_limb_1_col8 = eval.next_trace_mask(); + let next_pc_limb_2_col9 = eval.next_trace_mask(); + + // decode_instruction_ccd4c4cd993af638. + + eval.add_to_relation(&[RelationEntry::new( + &self.verifyinstruction_lookup_elements, + E::EF::one(), + &[ + input_pc_col0.clone(), + M31_32767.clone(), + M31_32767.clone(), + M31_32769.clone(), + M31_1.clone(), + M31_1.clone(), + M31_1.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_1.clone(), + M31_0.clone(), + M31_0.clone(), + ap_update_add_1_col3.clone(), + ], + )]); + + // read_small. + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryaddresstoid_lookup_elements, + E::EF::one(), + &[ + (input_pc_col0.clone() + M31_1.clone()), + next_pc_id_col4.clone(), + ], + )]); + + // cond_decode_small_sign. + + // msb is a bit. + eval.add_constraint((msb_col5.clone() * (msb_col5.clone() - M31_1.clone()))); + // mid_limbs_set is a bit. + eval.add_constraint( + (mid_limbs_set_col6.clone() * (mid_limbs_set_col6.clone() - M31_1.clone())), + ); + // Cannot have msb equals 0 and mid_limbs_set equals 1. + eval.add_constraint( + ((M31_1.clone() * mid_limbs_set_col6.clone()) * (msb_col5.clone() - M31_1.clone())), + ); + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryidtobig_lookup_elements, + E::EF::one(), + &[ + next_pc_id_col4.clone(), + next_pc_limb_0_col7.clone(), + next_pc_limb_1_col8.clone(), + next_pc_limb_2_col9.clone(), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + ((M31_136.clone() * msb_col5.clone()) - mid_limbs_set_col6.clone()), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + (msb_col5.clone() * M31_256.clone()), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.opcodes_lookup_elements, + E::EF::one(), + &[ + input_pc_col0.clone(), + input_ap_col1.clone(), + input_fp_col2.clone(), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.opcodes_lookup_elements, + -E::EF::one(), + &[ + (input_pc_col0.clone() + + ((((next_pc_limb_0_col7.clone() + + (next_pc_limb_1_col8.clone() * M31_512.clone())) + + (next_pc_limb_2_col9.clone() * M31_262144.clone())) + - msb_col5.clone()) + - (M31_134217728.clone() * mid_limbs_set_col6.clone()))), + (input_ap_col1.clone() + ap_update_add_1_col3.clone()), + input_fp_col2.clone(), + ], + )]); + + eval.finalize_logup(); + eval + } +} diff --git a/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_t_is_imm_t_is_double_deref_f/mod.rs b/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_t_is_imm_t_is_double_deref_f/mod.rs new file mode 100644 index 00000000..3f7a8d74 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_t_is_imm_t_is_double_deref_f/mod.rs @@ -0,0 +1,5 @@ +pub mod component; +pub mod prover; + +pub use component::{Claim, Component, Eval, InteractionClaim}; +pub use prover::{ClaimGenerator, InputType, InteractionClaimGenerator}; diff --git a/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_t_is_imm_t_is_double_deref_f/prover.rs b/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_t_is_imm_t_is_double_deref_f/prover.rs new file mode 100644 index 00000000..20ff97e4 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/jump_opcode_is_rel_t_is_imm_t_is_double_deref_f/prover.rs @@ -0,0 +1,418 @@ +#![allow(unused_parens)] +#![allow(unused_imports)] +use itertools::{chain, zip_eq, Itertools}; +use num_traits::{One, Zero}; +use prover_types::cpu::*; +use prover_types::simd::*; +use stwo_prover::constraint_framework::logup::LogupTraceGenerator; +use stwo_prover::constraint_framework::Relation; +use stwo_prover::core::air::Component; +use stwo_prover::core::backend::simd::column::BaseColumn; +use stwo_prover::core::backend::simd::conversion::Unpack; +use stwo_prover::core::backend::simd::m31::{PackedM31, LOG_N_LANES, N_LANES}; +use stwo_prover::core::backend::simd::qm31::PackedQM31; +use stwo_prover::core::backend::simd::SimdBackend; +use stwo_prover::core::backend::{Col, Column}; +use stwo_prover::core::fields::m31::M31; +use stwo_prover::core::pcs::TreeBuilder; +use stwo_prover::core::poly::circle::{CanonicCoset, CircleEvaluation}; +use stwo_prover::core::poly::BitReversedOrder; +use stwo_prover::core::utils::bit_reverse_coset_to_circle_domain_order; +use stwo_prover::core::vcs::blake2_merkle::{Blake2sMerkleChannel, Blake2sMerkleHasher}; + +use super::component::{Claim, InteractionClaim}; +use crate::components::{memory_address_to_id, memory_id_to_big, pack_values, verify_instruction}; +use crate::relations; + +pub type InputType = CasmState; +pub type PackedInputType = PackedCasmState; +const N_TRACE_COLUMNS: usize = 10; + +#[derive(Default)] +pub struct ClaimGenerator { + pub inputs: Vec, +} +impl ClaimGenerator { + pub fn new(inputs: Vec) -> Self { + Self { inputs } + } + + pub fn write_trace( + mut self, + tree_builder: &mut TreeBuilder<'_, '_, SimdBackend, Blake2sMerkleChannel>, + memory_address_to_id_state: &mut memory_address_to_id::ClaimGenerator, + memory_id_to_big_state: &mut memory_id_to_big::ClaimGenerator, + verify_instruction_state: &mut verify_instruction::ClaimGenerator, + ) -> (Claim, InteractionClaimGenerator) { + let n_calls = self.inputs.len(); + assert_ne!(n_calls, 0); + let size = std::cmp::max(n_calls.next_power_of_two(), N_LANES); + let need_padding = n_calls != size; + + if need_padding { + self.inputs.resize(size, *self.inputs.first().unwrap()); + bit_reverse_coset_to_circle_domain_order(&mut self.inputs); + } + + let packed_inputs = pack_values(&self.inputs); + let (trace, mut sub_components_inputs, lookup_data) = write_trace_simd( + packed_inputs, + memory_address_to_id_state, + memory_id_to_big_state, + ); + + if need_padding { + sub_components_inputs.bit_reverse_coset_to_circle_domain_order(); + } + sub_components_inputs + .memory_address_to_id_inputs + .iter() + .for_each(|inputs| { + memory_address_to_id_state.add_inputs(&inputs[..n_calls]); + }); + sub_components_inputs + .memory_id_to_big_inputs + .iter() + .for_each(|inputs| { + memory_id_to_big_state.add_inputs(&inputs[..n_calls]); + }); + sub_components_inputs + .verify_instruction_inputs + .iter() + .for_each(|inputs| { + verify_instruction_state.add_inputs(&inputs[..n_calls]); + }); + + tree_builder.extend_evals( + trace + .into_iter() + .map(|eval| { + let domain = CanonicCoset::new( + eval.len() + .checked_ilog2() + .expect("Input is not a power of 2!"), + ) + .circle_domain(); + CircleEvaluation::::new(domain, eval) + }) + .collect_vec(), + ); + + ( + Claim { n_calls }, + InteractionClaimGenerator { + n_calls, + lookup_data, + }, + ) + } + + pub fn add_inputs(&mut self, inputs: &[InputType]) { + self.inputs.extend(inputs); + } +} + +pub struct SubComponentInputs { + pub memory_address_to_id_inputs: [Vec; 1], + pub memory_id_to_big_inputs: [Vec; 1], + pub verify_instruction_inputs: [Vec; 1], +} +impl SubComponentInputs { + #[allow(unused_variables)] + fn with_capacity(capacity: usize) -> Self { + Self { + memory_address_to_id_inputs: [Vec::with_capacity(capacity)], + memory_id_to_big_inputs: [Vec::with_capacity(capacity)], + verify_instruction_inputs: [Vec::with_capacity(capacity)], + } + } + + fn bit_reverse_coset_to_circle_domain_order(&mut self) { + self.memory_address_to_id_inputs + .iter_mut() + .for_each(|vec| bit_reverse_coset_to_circle_domain_order(vec)); + self.memory_id_to_big_inputs + .iter_mut() + .for_each(|vec| bit_reverse_coset_to_circle_domain_order(vec)); + self.verify_instruction_inputs + .iter_mut() + .for_each(|vec| bit_reverse_coset_to_circle_domain_order(vec)); + } +} + +#[allow(clippy::useless_conversion)] +#[allow(unused_variables)] +#[allow(clippy::double_parens)] +#[allow(non_snake_case)] +pub fn write_trace_simd( + inputs: Vec, + memory_address_to_id_state: &mut memory_address_to_id::ClaimGenerator, + memory_id_to_big_state: &mut memory_id_to_big::ClaimGenerator, +) -> ( + [BaseColumn; N_TRACE_COLUMNS], + SubComponentInputs, + LookupData, +) { + const N_TRACE_COLUMNS: usize = 10; + let mut trace: [_; N_TRACE_COLUMNS] = + std::array::from_fn(|_| Col::::zeros(inputs.len() * N_LANES)); + + let mut lookup_data = LookupData::with_capacity(inputs.len()); + #[allow(unused_mut)] + let mut sub_components_inputs = SubComponentInputs::with_capacity(inputs.len()); + + let M31_0 = PackedM31::broadcast(M31::from(0)); + let M31_1 = PackedM31::broadcast(M31::from(1)); + let M31_134217728 = PackedM31::broadcast(M31::from(134217728)); + let M31_136 = PackedM31::broadcast(M31::from(136)); + let M31_256 = PackedM31::broadcast(M31::from(256)); + let M31_262144 = PackedM31::broadcast(M31::from(262144)); + let M31_32767 = PackedM31::broadcast(M31::from(32767)); + let M31_32769 = PackedM31::broadcast(M31::from(32769)); + let M31_511 = PackedM31::broadcast(M31::from(511)); + let M31_512 = PackedM31::broadcast(M31::from(512)); + let UInt16_1 = PackedUInt16::broadcast(UInt16::from(1)); + let UInt16_11 = PackedUInt16::broadcast(UInt16::from(11)); + let UInt16_3 = PackedUInt16::broadcast(UInt16::from(3)); + let UInt16_6 = PackedUInt16::broadcast(UInt16::from(6)); + + inputs.into_iter().enumerate().for_each( + |(row_index, jump_opcode_is_rel_t_is_imm_t_is_double_deref_f_input)| { + let input_tmp_1264 = jump_opcode_is_rel_t_is_imm_t_is_double_deref_f_input; + let input_pc_col0 = input_tmp_1264.pc; + trace[0].data[row_index] = input_pc_col0; + let input_ap_col1 = input_tmp_1264.ap; + trace[1].data[row_index] = input_ap_col1; + let input_fp_col2 = input_tmp_1264.fp; + trace[2].data[row_index] = input_fp_col2; + + // decode_instruction_ccd4c4cd993af638. + + let memory_address_to_id_value_tmp_1269 = + memory_address_to_id_state.deduce_output(input_pc_col0); + let memory_id_to_big_value_tmp_1270 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1269); + let ap_update_add_1_tmp_1271 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1270.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1270.get_m31(6))) + << (UInt16_6))) + >> (UInt16_11)) + & (UInt16_1)); + let ap_update_add_1_col3 = ap_update_add_1_tmp_1271.as_m31(); + trace[3].data[row_index] = ap_update_add_1_col3; + + sub_components_inputs.verify_instruction_inputs[0].extend( + ( + input_pc_col0, + [M31_32767, M31_32767, M31_32769], + [ + M31_1, + M31_1, + M31_1, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_1, + M31_0, + M31_0, + ap_update_add_1_col3, + M31_0, + M31_0, + M31_0, + ], + ) + .unpack(), + ); + + lookup_data.verifyinstruction[0].push([ + input_pc_col0, + M31_32767, + M31_32767, + M31_32769, + M31_1, + M31_1, + M31_1, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_1, + M31_0, + M31_0, + ap_update_add_1_col3, + M31_0, + M31_0, + M31_0, + ]); + + // read_small. + + let memory_address_to_id_value_tmp_1273 = + memory_address_to_id_state.deduce_output(((input_pc_col0) + (M31_1))); + let memory_id_to_big_value_tmp_1274 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1273); + let next_pc_id_col4 = memory_address_to_id_value_tmp_1273; + trace[4].data[row_index] = next_pc_id_col4; + sub_components_inputs.memory_address_to_id_inputs[0] + .extend(((input_pc_col0) + (M31_1)).unpack()); + + lookup_data.memoryaddresstoid[0].push([((input_pc_col0) + (M31_1)), next_pc_id_col4]); + + // cond_decode_small_sign. + + let msb_tmp_1275 = memory_id_to_big_value_tmp_1274.get_m31(27).eq(M31_256); + let msb_col5 = msb_tmp_1275.as_m31(); + trace[5].data[row_index] = msb_col5; + let mid_limbs_set_tmp_1276 = memory_id_to_big_value_tmp_1274.get_m31(20).eq(M31_511); + let mid_limbs_set_col6 = mid_limbs_set_tmp_1276.as_m31(); + trace[6].data[row_index] = mid_limbs_set_col6; + + let next_pc_limb_0_col7 = memory_id_to_big_value_tmp_1274.get_m31(0); + trace[7].data[row_index] = next_pc_limb_0_col7; + let next_pc_limb_1_col8 = memory_id_to_big_value_tmp_1274.get_m31(1); + trace[8].data[row_index] = next_pc_limb_1_col8; + let next_pc_limb_2_col9 = memory_id_to_big_value_tmp_1274.get_m31(2); + trace[9].data[row_index] = next_pc_limb_2_col9; + sub_components_inputs.memory_id_to_big_inputs[0].extend(next_pc_id_col4.unpack()); + + lookup_data.memoryidtobig[0].push([ + next_pc_id_col4, + next_pc_limb_0_col7, + next_pc_limb_1_col8, + next_pc_limb_2_col9, + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + (((M31_136) * (msb_col5)) - (mid_limbs_set_col6)), + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + ((msb_col5) * (M31_256)), + ]); + + lookup_data.opcodes[0].push([input_pc_col0, input_ap_col1, input_fp_col2]); + lookup_data.opcodes[1].push([ + ((input_pc_col0) + + (((((next_pc_limb_0_col7) + ((next_pc_limb_1_col8) * (M31_512))) + + ((next_pc_limb_2_col9) * (M31_262144))) + - (msb_col5)) + - ((M31_134217728) * (mid_limbs_set_col6)))), + ((input_ap_col1) + (ap_update_add_1_col3)), + input_fp_col2, + ]); + }, + ); + + (trace, sub_components_inputs, lookup_data) +} + +pub struct LookupData { + pub memoryaddresstoid: [Vec<[PackedM31; 2]>; 1], + pub memoryidtobig: [Vec<[PackedM31; 29]>; 1], + pub opcodes: [Vec<[PackedM31; 3]>; 2], + pub verifyinstruction: [Vec<[PackedM31; 19]>; 1], +} +impl LookupData { + #[allow(unused_variables)] + fn with_capacity(capacity: usize) -> Self { + Self { + memoryaddresstoid: [Vec::with_capacity(capacity)], + memoryidtobig: [Vec::with_capacity(capacity)], + opcodes: [Vec::with_capacity(capacity), Vec::with_capacity(capacity)], + verifyinstruction: [Vec::with_capacity(capacity)], + } + } +} + +pub struct InteractionClaimGenerator { + pub n_calls: usize, + pub lookup_data: LookupData, +} +impl InteractionClaimGenerator { + pub fn write_interaction_trace( + self, + tree_builder: &mut TreeBuilder<'_, '_, SimdBackend, Blake2sMerkleChannel>, + memoryaddresstoid_lookup_elements: &relations::MemoryAddressToId, + memoryidtobig_lookup_elements: &relations::MemoryIdToBig, + opcodes_lookup_elements: &relations::Opcodes, + verifyinstruction_lookup_elements: &relations::VerifyInstruction, + ) -> InteractionClaim { + let log_size = std::cmp::max(self.n_calls.next_power_of_two().ilog2(), LOG_N_LANES); + let mut logup_gen = LogupTraceGenerator::new(log_size); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.verifyinstruction[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = verifyinstruction_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.memoryaddresstoid[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = memoryaddresstoid_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.memoryidtobig[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = memoryidtobig_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.opcodes[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = opcodes_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.opcodes[1]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = opcodes_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, -PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let (trace, total_sum, claimed_sum) = if self.n_calls == 1 << log_size { + let (trace, claimed_sum) = logup_gen.finalize_last(); + (trace, claimed_sum, None) + } else { + let (trace, [total_sum, claimed_sum]) = + logup_gen.finalize_at([(1 << log_size) - 1, self.n_calls - 1]); + (trace, total_sum, Some((claimed_sum, self.n_calls - 1))) + }; + tree_builder.extend_evals(trace); + + InteractionClaim { + logup_sums: (total_sum, claimed_sum), + } + } +} diff --git a/stwo_cairo_prover/crates/prover/src/components/mod.rs b/stwo_cairo_prover/crates/prover/src/components/mod.rs index ab0a1d2a..068a6fc9 100644 --- a/stwo_cairo_prover/crates/prover/src/components/mod.rs +++ b/stwo_cairo_prover/crates/prover/src/components/mod.rs @@ -16,6 +16,10 @@ pub mod jnz_opcode_is_taken_f_dst_base_fp_f; pub mod jnz_opcode_is_taken_f_dst_base_fp_t; pub mod jnz_opcode_is_taken_t_dst_base_fp_f; pub mod jnz_opcode_is_taken_t_dst_base_fp_t; +pub mod jump_opcode_is_rel_f_is_imm_f_is_double_deref_f; +pub mod jump_opcode_is_rel_f_is_imm_f_is_double_deref_t; +pub mod jump_opcode_is_rel_t_is_imm_f_is_double_deref_f; +pub mod jump_opcode_is_rel_t_is_imm_t_is_double_deref_f; pub mod memory; pub mod range_check_vector; pub mod ret_opcode; diff --git a/stwo_cairo_prover/crates/prover/src/input/state_transitions.rs b/stwo_cairo_prover/crates/prover/src/input/state_transitions.rs index 3ff34700..0b12d039 100644 --- a/stwo_cairo_prover/crates/prover/src/input/state_transitions.rs +++ b/stwo_cairo_prover/crates/prover/src/input/state_transitions.rs @@ -289,7 +289,7 @@ impl StateTransitions { opcode_call: false, opcode_ret: false, opcode_assert_eq: false, - } if !dev_mode => { + } => { if op1_imm { // jump rel imm. assert!(