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 b3d4c7e2..d26159ca 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 @@ -12,9 +12,11 @@ use stwo_prover::core::vcs::blake2_merkle::Blake2sMerkleChannel; use super::air::CairoInteractionElements; use crate::components::{ add_ap_opcode_is_imm_f_op1_base_fp_f, add_ap_opcode_is_imm_f_op1_base_fp_t, - add_ap_opcode_is_imm_t_op1_base_fp_f, 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, + add_ap_opcode_is_imm_t_op1_base_fp_f, add_opcode_is_small_f_is_imm_f, + add_opcode_is_small_f_is_imm_t, add_opcode_is_small_t_is_imm_f, add_opcode_is_small_t_is_imm_t, + 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, @@ -23,6 +25,10 @@ use crate::input::state_transitions::StateTransitions; #[derive(Serialize, Deserialize)] pub struct OpcodeClaim { + add_f_f: Vec, + add_f_t: Vec, + add_t_f: Vec, + add_t_t: Vec, add_ap_f_f: Vec, add_ap_f_t: Vec, add_ap_t_f: Vec, @@ -40,6 +46,10 @@ pub struct OpcodeClaim { } impl OpcodeClaim { pub fn mix_into(&self, channel: &mut impl Channel) { + self.add_f_f.iter().for_each(|c| c.mix_into(channel)); + self.add_f_t.iter().for_each(|c| c.mix_into(channel)); + self.add_t_f.iter().for_each(|c| c.mix_into(channel)); + self.add_t_t.iter().for_each(|c| c.mix_into(channel)); self.add_ap_f_f.iter().for_each(|c| c.mix_into(channel)); self.add_ap_f_t.iter().for_each(|c| c.mix_into(channel)); self.add_ap_t_f.iter().for_each(|c| c.mix_into(channel)); @@ -58,6 +68,10 @@ impl OpcodeClaim { pub fn log_sizes(&self) -> TreeVec> { TreeVec::concat_cols(chain!( + self.add_f_f.iter().map(|c| c.log_sizes()), + self.add_f_t.iter().map(|c| c.log_sizes()), + self.add_t_f.iter().map(|c| c.log_sizes()), + self.add_t_t.iter().map(|c| c.log_sizes()), self.add_ap_f_f.iter().map(|c| c.log_sizes()), self.add_ap_f_t.iter().map(|c| c.log_sizes()), self.add_ap_t_f.iter().map(|c| c.log_sizes()), @@ -77,6 +91,10 @@ impl OpcodeClaim { } pub struct OpcodesClaimGenerator { + add_f_f: Vec, + add_f_t: Vec, + add_t_f: Vec, + add_t_t: Vec, add_ap_f_f: Vec, add_ap_f_t: Vec, add_ap_t_f: Vec, @@ -95,6 +113,10 @@ pub struct OpcodesClaimGenerator { impl OpcodesClaimGenerator { pub fn new(input: StateTransitions) -> Self { // TODO(Ohad): decide split sizes for opcode traces. + let mut add_f_f = vec![]; + let mut add_f_t = vec![]; + let mut add_t_f = vec![]; + let mut add_t_t = vec![]; let mut add_ap_f_f = vec![]; let mut add_ap_f_t = vec![]; let mut add_ap_t_f = vec![]; @@ -109,6 +131,42 @@ impl OpcodesClaimGenerator { let mut mul_f_f = vec![]; let mut mul_f_t = vec![]; let mut ret = vec![]; + if !input + .casm_states_by_opcode + .add_opcode_is_small_f_is_imm_f + .is_empty() + { + add_f_f.push(add_opcode_is_small_f_is_imm_f::ClaimGenerator::new( + input.casm_states_by_opcode.add_opcode_is_small_f_is_imm_f, + )); + } + if !input + .casm_states_by_opcode + .add_opcode_is_small_f_is_imm_t + .is_empty() + { + add_f_t.push(add_opcode_is_small_f_is_imm_t::ClaimGenerator::new( + input.casm_states_by_opcode.add_opcode_is_small_f_is_imm_t, + )); + } + if !input + .casm_states_by_opcode + .add_opcode_is_small_t_is_imm_f + .is_empty() + { + add_t_f.push(add_opcode_is_small_t_is_imm_f::ClaimGenerator::new( + input.casm_states_by_opcode.add_opcode_is_small_t_is_imm_f, + )); + } + if !input + .casm_states_by_opcode + .add_opcode_is_small_t_is_imm_t + .is_empty() + { + add_t_t.push(add_opcode_is_small_t_is_imm_t::ClaimGenerator::new( + input.casm_states_by_opcode.add_opcode_is_small_t_is_imm_t, + )); + } if !input .casm_states_by_opcode .add_ap_opcode_is_imm_f_op1_base_fp_f @@ -256,6 +314,10 @@ impl OpcodesClaimGenerator { )); } Self { + add_f_f, + add_f_t, + add_t_f, + add_t_t, add_ap_f_f, add_ap_f_t, add_ap_t_f, @@ -282,6 +344,54 @@ impl OpcodesClaimGenerator { range_check_9_9_trace_generator: &mut range_check_9_9::ClaimGenerator, verify_instruction_trace_generator: &mut verify_instruction::ClaimGenerator, ) -> (OpcodeClaim, OpcodesInteractionClaimGenerator) { + let (add_f_f_claims, add_f_f_interaction_gens) = self + .add_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 (add_f_t_claims, add_f_t_interaction_gens) = self + .add_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 (add_t_f_claims, add_t_f_interaction_gens) = self + .add_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 (add_t_t_claims, add_t_t_interaction_gens) = self + .add_t_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 (add_ap_f_f_claims, add_ap_f_f_interaction_gens) = self .add_ap_f_f .into_iter() @@ -456,6 +566,10 @@ impl OpcodesClaimGenerator { .unzip(); ( OpcodeClaim { + add_f_f: add_f_f_claims, + add_f_t: add_f_t_claims, + add_t_f: add_t_f_claims, + add_t_t: add_t_t_claims, add_ap_f_f: add_ap_f_f_claims, add_ap_f_t: add_ap_f_t_claims, add_ap_t_f: add_ap_t_f_claims, @@ -472,6 +586,10 @@ impl OpcodesClaimGenerator { ret: ret_claims, }, OpcodesInteractionClaimGenerator { + add_f_f: add_f_f_interaction_gens, + add_f_t: add_f_t_interaction_gens, + add_t_f: add_t_f_interaction_gens, + add_t_t: add_t_t_interaction_gens, add_ap_f_f: add_ap_f_f_interaction_gens, add_ap_f_t: add_ap_f_t_interaction_gens, add_ap_t_f: add_ap_t_f_interaction_gens, @@ -493,6 +611,10 @@ impl OpcodesClaimGenerator { #[derive(Serialize, Deserialize)] pub struct OpcodeInteractionClaim { + add_f_f: Vec, + add_f_t: Vec, + add_t_f: Vec, + add_t_t: Vec, add_ap_f_f: Vec, add_ap_f_t: Vec, add_ap_t_f: Vec, @@ -510,6 +632,10 @@ pub struct OpcodeInteractionClaim { } impl OpcodeInteractionClaim { pub fn mix_into(&self, channel: &mut impl Channel) { + self.add_f_f.iter().for_each(|c| c.mix_into(channel)); + self.add_f_t.iter().for_each(|c| c.mix_into(channel)); + self.add_t_f.iter().for_each(|c| c.mix_into(channel)); + self.add_t_t.iter().for_each(|c| c.mix_into(channel)); self.add_ap_f_f.iter().for_each(|c| c.mix_into(channel)); self.add_ap_f_t.iter().for_each(|c| c.mix_into(channel)); self.add_ap_t_f.iter().for_each(|c| c.mix_into(channel)); @@ -528,6 +654,34 @@ impl OpcodeInteractionClaim { pub fn sum(&self) -> SecureField { let mut sum = QM31::zero(); + for interaction_claim in &self.add_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.add_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.add_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.add_t_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.add_ap_f_f { let (total_sum, claimed_sum) = interaction_claim.logup_sums; sum += match claimed_sum { @@ -631,6 +785,10 @@ impl OpcodeInteractionClaim { } pub struct OpcodesInteractionClaimGenerator { + add_f_f: Vec, + add_f_t: Vec, + add_t_f: Vec, + add_t_t: Vec, add_ap_f_f: Vec, add_ap_f_t: Vec, add_ap_t_f: Vec, @@ -652,6 +810,58 @@ impl OpcodesInteractionClaimGenerator { tree_builder: &mut TreeBuilder<'_, '_, SimdBackend, Blake2sMerkleChannel>, interaction_elements: &CairoInteractionElements, ) -> OpcodeInteractionClaim { + let add_f_f_interaction_claims = self + .add_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 add_f_t_interaction_claims = self + .add_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 add_t_f_interaction_claims = self + .add_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 add_t_t_interaction_claims = self + .add_t_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 add_ap_f_f_interaction_claims = self .add_ap_f_f .into_iter() @@ -837,6 +1047,10 @@ impl OpcodesInteractionClaimGenerator { }) .collect(); OpcodeInteractionClaim { + add_f_f: add_f_f_interaction_claims, + add_f_t: add_f_t_interaction_claims, + add_t_f: add_t_f_interaction_claims, + add_t_t: add_t_t_interaction_claims, add_ap_f_f: add_ap_f_f_interaction_claims, add_ap_f_t: add_ap_f_t_interaction_claims, add_ap_t_f: add_ap_t_f_interaction_claims, @@ -856,6 +1070,10 @@ impl OpcodesInteractionClaimGenerator { } pub struct OpcodeComponents { + add_f_f: Vec, + add_f_t: Vec, + add_t_f: Vec, + add_t_t: Vec, add_ap_f_f: Vec, add_ap_f_t: Vec, add_ap_t_f: Vec, @@ -878,6 +1096,102 @@ impl OpcodeComponents { interaction_elements: &CairoInteractionElements, interaction_claim: &OpcodeInteractionClaim, ) -> Self { + let add_f_f_components = claim + .add_f_f + .iter() + .zip(interaction_claim.add_f_f.iter()) + .map(|(&claim, &interaction_claim)| { + add_opcode_is_small_f_is_imm_f::Component::new( + tree_span_provider, + add_opcode_is_small_f_is_imm_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_vec(); + let add_f_t_components = claim + .add_f_t + .iter() + .zip(interaction_claim.add_f_t.iter()) + .map(|(&claim, &interaction_claim)| { + add_opcode_is_small_f_is_imm_t::Component::new( + tree_span_provider, + add_opcode_is_small_f_is_imm_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_vec(); + let add_t_f_components = claim + .add_t_f + .iter() + .zip(interaction_claim.add_t_f.iter()) + .map(|(&claim, &interaction_claim)| { + add_opcode_is_small_t_is_imm_f::Component::new( + tree_span_provider, + add_opcode_is_small_t_is_imm_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_vec(); + let add_t_t_components = claim + .add_t_t + .iter() + .zip(interaction_claim.add_t_t.iter()) + .map(|(&claim, &interaction_claim)| { + add_opcode_is_small_t_is_imm_t::Component::new( + tree_span_provider, + add_opcode_is_small_t_is_imm_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_vec(); let add_ap_f_f_components = claim .add_ap_f_f .iter() @@ -1215,6 +1529,10 @@ impl OpcodeComponents { }) .collect_vec(); Self { + add_f_f: add_f_f_components, + add_f_t: add_f_t_components, + add_t_f: add_t_f_components, + add_t_t: add_t_t_components, add_ap_f_f: add_ap_f_f_components, add_ap_f_t: add_ap_f_t_components, add_ap_t_f: add_ap_t_f_components, @@ -1234,6 +1552,26 @@ impl OpcodeComponents { pub fn provers(&self) -> Vec<&dyn ComponentProver> { let mut vec: Vec<&dyn ComponentProver> = vec![]; + vec.extend( + self.add_f_f + .iter() + .map(|component| component as &dyn ComponentProver), + ); + vec.extend( + self.add_f_t + .iter() + .map(|component| component as &dyn ComponentProver), + ); + vec.extend( + self.add_t_f + .iter() + .map(|component| component as &dyn ComponentProver), + ); + vec.extend( + self.add_t_t + .iter() + .map(|component| component as &dyn ComponentProver), + ); vec.extend( self.add_ap_f_f .iter() diff --git a/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_f_is_imm_f/component.rs b/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_f_is_imm_f/component.rs new file mode 100644 index 00000000..669bbc88 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_f_is_imm_f/component.rs @@ -0,0 +1,640 @@ +#![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; 99]; + let interaction_log_sizes = vec![log_size; SECURE_EXTENSION_DEGREE * 9]; + 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_136 = E::F::from(M31::from(136)); + let M31_256 = E::F::from(M31::from(256)); + let M31_32768 = E::F::from(M31::from(32768)); + let M31_4194304 = E::F::from(M31::from(4194304)); + 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 offset0_col3 = eval.next_trace_mask(); + let offset1_col4 = eval.next_trace_mask(); + let offset2_col5 = eval.next_trace_mask(); + let dst_base_fp_col6 = eval.next_trace_mask(); + let op0_base_fp_col7 = eval.next_trace_mask(); + let op1_base_fp_col8 = eval.next_trace_mask(); + let op1_base_ap_col9 = eval.next_trace_mask(); + let ap_update_add_1_col10 = eval.next_trace_mask(); + let dst_id_col11 = eval.next_trace_mask(); + let dst_limb_0_col12 = eval.next_trace_mask(); + let dst_limb_1_col13 = eval.next_trace_mask(); + let dst_limb_2_col14 = eval.next_trace_mask(); + let dst_limb_3_col15 = eval.next_trace_mask(); + let dst_limb_4_col16 = eval.next_trace_mask(); + let dst_limb_5_col17 = eval.next_trace_mask(); + let dst_limb_6_col18 = eval.next_trace_mask(); + let dst_limb_7_col19 = eval.next_trace_mask(); + let dst_limb_8_col20 = eval.next_trace_mask(); + let dst_limb_9_col21 = eval.next_trace_mask(); + let dst_limb_10_col22 = eval.next_trace_mask(); + let dst_limb_11_col23 = eval.next_trace_mask(); + let dst_limb_12_col24 = eval.next_trace_mask(); + let dst_limb_13_col25 = eval.next_trace_mask(); + let dst_limb_14_col26 = eval.next_trace_mask(); + let dst_limb_15_col27 = eval.next_trace_mask(); + let dst_limb_16_col28 = eval.next_trace_mask(); + let dst_limb_17_col29 = eval.next_trace_mask(); + let dst_limb_18_col30 = eval.next_trace_mask(); + let dst_limb_19_col31 = eval.next_trace_mask(); + let dst_limb_20_col32 = eval.next_trace_mask(); + let dst_limb_21_col33 = eval.next_trace_mask(); + let dst_limb_22_col34 = eval.next_trace_mask(); + let dst_limb_23_col35 = eval.next_trace_mask(); + let dst_limb_24_col36 = eval.next_trace_mask(); + let dst_limb_25_col37 = eval.next_trace_mask(); + let dst_limb_26_col38 = eval.next_trace_mask(); + let dst_limb_27_col39 = eval.next_trace_mask(); + let op0_id_col40 = eval.next_trace_mask(); + let op0_limb_0_col41 = eval.next_trace_mask(); + let op0_limb_1_col42 = eval.next_trace_mask(); + let op0_limb_2_col43 = eval.next_trace_mask(); + let op0_limb_3_col44 = eval.next_trace_mask(); + let op0_limb_4_col45 = eval.next_trace_mask(); + let op0_limb_5_col46 = eval.next_trace_mask(); + let op0_limb_6_col47 = eval.next_trace_mask(); + let op0_limb_7_col48 = eval.next_trace_mask(); + let op0_limb_8_col49 = eval.next_trace_mask(); + let op0_limb_9_col50 = eval.next_trace_mask(); + let op0_limb_10_col51 = eval.next_trace_mask(); + let op0_limb_11_col52 = eval.next_trace_mask(); + let op0_limb_12_col53 = eval.next_trace_mask(); + let op0_limb_13_col54 = eval.next_trace_mask(); + let op0_limb_14_col55 = eval.next_trace_mask(); + let op0_limb_15_col56 = eval.next_trace_mask(); + let op0_limb_16_col57 = eval.next_trace_mask(); + let op0_limb_17_col58 = eval.next_trace_mask(); + let op0_limb_18_col59 = eval.next_trace_mask(); + let op0_limb_19_col60 = eval.next_trace_mask(); + let op0_limb_20_col61 = eval.next_trace_mask(); + let op0_limb_21_col62 = eval.next_trace_mask(); + let op0_limb_22_col63 = eval.next_trace_mask(); + let op0_limb_23_col64 = eval.next_trace_mask(); + let op0_limb_24_col65 = eval.next_trace_mask(); + let op0_limb_25_col66 = eval.next_trace_mask(); + let op0_limb_26_col67 = eval.next_trace_mask(); + let op0_limb_27_col68 = eval.next_trace_mask(); + let op1_id_col69 = eval.next_trace_mask(); + let op1_limb_0_col70 = eval.next_trace_mask(); + let op1_limb_1_col71 = eval.next_trace_mask(); + let op1_limb_2_col72 = eval.next_trace_mask(); + let op1_limb_3_col73 = eval.next_trace_mask(); + let op1_limb_4_col74 = eval.next_trace_mask(); + let op1_limb_5_col75 = eval.next_trace_mask(); + let op1_limb_6_col76 = eval.next_trace_mask(); + let op1_limb_7_col77 = eval.next_trace_mask(); + let op1_limb_8_col78 = eval.next_trace_mask(); + let op1_limb_9_col79 = eval.next_trace_mask(); + let op1_limb_10_col80 = eval.next_trace_mask(); + let op1_limb_11_col81 = eval.next_trace_mask(); + let op1_limb_12_col82 = eval.next_trace_mask(); + let op1_limb_13_col83 = eval.next_trace_mask(); + let op1_limb_14_col84 = eval.next_trace_mask(); + let op1_limb_15_col85 = eval.next_trace_mask(); + let op1_limb_16_col86 = eval.next_trace_mask(); + let op1_limb_17_col87 = eval.next_trace_mask(); + let op1_limb_18_col88 = eval.next_trace_mask(); + let op1_limb_19_col89 = eval.next_trace_mask(); + let op1_limb_20_col90 = eval.next_trace_mask(); + let op1_limb_21_col91 = eval.next_trace_mask(); + let op1_limb_22_col92 = eval.next_trace_mask(); + let op1_limb_23_col93 = eval.next_trace_mask(); + let op1_limb_24_col94 = eval.next_trace_mask(); + let op1_limb_25_col95 = eval.next_trace_mask(); + let op1_limb_26_col96 = eval.next_trace_mask(); + let op1_limb_27_col97 = eval.next_trace_mask(); + let sub_p_bit_col98 = eval.next_trace_mask(); + + // decode_instruction_52ce7a4a3d9be19a. + + eval.add_to_relation(&[RelationEntry::new( + &self.verifyinstruction_lookup_elements, + E::EF::one(), + &[ + input_pc_col0.clone(), + offset0_col3.clone(), + offset1_col4.clone(), + offset2_col5.clone(), + dst_base_fp_col6.clone(), + op0_base_fp_col7.clone(), + M31_0.clone(), + op1_base_fp_col8.clone(), + op1_base_ap_col9.clone(), + M31_1.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + ap_update_add_1_col10.clone(), + M31_0.clone(), + M31_0.clone(), + M31_1.clone(), + ], + )]); + + // Either flag op1_base_fp is on or flag op1_base_ap is on. + eval.add_constraint( + ((op1_base_fp_col8.clone() + op1_base_ap_col9.clone()) - M31_1.clone()), + ); + + // read_positive_num_bits_252. + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryaddresstoid_lookup_elements, + E::EF::one(), + &[ + (((dst_base_fp_col6.clone() * input_fp_col2.clone()) + + ((M31_1.clone() - dst_base_fp_col6.clone()) * input_ap_col1.clone())) + + (offset0_col3.clone() - M31_32768.clone())), + dst_id_col11.clone(), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryidtobig_lookup_elements, + E::EF::one(), + &[ + dst_id_col11.clone(), + dst_limb_0_col12.clone(), + dst_limb_1_col13.clone(), + dst_limb_2_col14.clone(), + dst_limb_3_col15.clone(), + dst_limb_4_col16.clone(), + dst_limb_5_col17.clone(), + dst_limb_6_col18.clone(), + dst_limb_7_col19.clone(), + dst_limb_8_col20.clone(), + dst_limb_9_col21.clone(), + dst_limb_10_col22.clone(), + dst_limb_11_col23.clone(), + dst_limb_12_col24.clone(), + dst_limb_13_col25.clone(), + dst_limb_14_col26.clone(), + dst_limb_15_col27.clone(), + dst_limb_16_col28.clone(), + dst_limb_17_col29.clone(), + dst_limb_18_col30.clone(), + dst_limb_19_col31.clone(), + dst_limb_20_col32.clone(), + dst_limb_21_col33.clone(), + dst_limb_22_col34.clone(), + dst_limb_23_col35.clone(), + dst_limb_24_col36.clone(), + dst_limb_25_col37.clone(), + dst_limb_26_col38.clone(), + dst_limb_27_col39.clone(), + ], + )]); + + // read_positive_num_bits_252. + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryaddresstoid_lookup_elements, + E::EF::one(), + &[ + (((op0_base_fp_col7.clone() * input_fp_col2.clone()) + + ((M31_1.clone() - op0_base_fp_col7.clone()) * input_ap_col1.clone())) + + (offset1_col4.clone() - M31_32768.clone())), + op0_id_col40.clone(), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryidtobig_lookup_elements, + E::EF::one(), + &[ + op0_id_col40.clone(), + op0_limb_0_col41.clone(), + op0_limb_1_col42.clone(), + op0_limb_2_col43.clone(), + op0_limb_3_col44.clone(), + op0_limb_4_col45.clone(), + op0_limb_5_col46.clone(), + op0_limb_6_col47.clone(), + op0_limb_7_col48.clone(), + op0_limb_8_col49.clone(), + op0_limb_9_col50.clone(), + op0_limb_10_col51.clone(), + op0_limb_11_col52.clone(), + op0_limb_12_col53.clone(), + op0_limb_13_col54.clone(), + op0_limb_14_col55.clone(), + op0_limb_15_col56.clone(), + op0_limb_16_col57.clone(), + op0_limb_17_col58.clone(), + op0_limb_18_col59.clone(), + op0_limb_19_col60.clone(), + op0_limb_20_col61.clone(), + op0_limb_21_col62.clone(), + op0_limb_22_col63.clone(), + op0_limb_23_col64.clone(), + op0_limb_24_col65.clone(), + op0_limb_25_col66.clone(), + op0_limb_26_col67.clone(), + op0_limb_27_col68.clone(), + ], + )]); + + // read_positive_num_bits_252. + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryaddresstoid_lookup_elements, + E::EF::one(), + &[ + (((op1_base_fp_col8.clone() * input_fp_col2.clone()) + + (op1_base_ap_col9.clone() * input_ap_col1.clone())) + + (offset2_col5.clone() - M31_32768.clone())), + op1_id_col69.clone(), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryidtobig_lookup_elements, + E::EF::one(), + &[ + op1_id_col69.clone(), + op1_limb_0_col70.clone(), + op1_limb_1_col71.clone(), + op1_limb_2_col72.clone(), + op1_limb_3_col73.clone(), + op1_limb_4_col74.clone(), + op1_limb_5_col75.clone(), + op1_limb_6_col76.clone(), + op1_limb_7_col77.clone(), + op1_limb_8_col78.clone(), + op1_limb_9_col79.clone(), + op1_limb_10_col80.clone(), + op1_limb_11_col81.clone(), + op1_limb_12_col82.clone(), + op1_limb_13_col83.clone(), + op1_limb_14_col84.clone(), + op1_limb_15_col85.clone(), + op1_limb_16_col86.clone(), + op1_limb_17_col87.clone(), + op1_limb_18_col88.clone(), + op1_limb_19_col89.clone(), + op1_limb_20_col90.clone(), + op1_limb_21_col91.clone(), + op1_limb_22_col92.clone(), + op1_limb_23_col93.clone(), + op1_limb_24_col94.clone(), + op1_limb_25_col95.clone(), + op1_limb_26_col96.clone(), + op1_limb_27_col97.clone(), + ], + )]); + + // verify_add252. + + // sub_p_bit is a bit. + eval.add_constraint((sub_p_bit_col98.clone() * (sub_p_bit_col98.clone() - M31_1.clone()))); + let carry_tmp_1016 = (((((op0_limb_0_col41.clone() + op1_limb_0_col70.clone()) + + M31_0.clone()) + - dst_limb_0_col12.clone()) + - (M31_1.clone() * sub_p_bit_col98.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1016.clone() + * ((carry_tmp_1016.clone() * carry_tmp_1016.clone()) - M31_1.clone())), + ); + let carry_tmp_1017 = (((((op0_limb_1_col42.clone() + op1_limb_1_col71.clone()) + + carry_tmp_1016.clone()) + - dst_limb_1_col13.clone()) + - (M31_0.clone() * sub_p_bit_col98.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1017.clone() + * ((carry_tmp_1017.clone() * carry_tmp_1017.clone()) - M31_1.clone())), + ); + let carry_tmp_1018 = (((((op0_limb_2_col43.clone() + op1_limb_2_col72.clone()) + + carry_tmp_1017.clone()) + - dst_limb_2_col14.clone()) + - (M31_0.clone() * sub_p_bit_col98.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1018.clone() + * ((carry_tmp_1018.clone() * carry_tmp_1018.clone()) - M31_1.clone())), + ); + let carry_tmp_1019 = (((((op0_limb_3_col44.clone() + op1_limb_3_col73.clone()) + + carry_tmp_1018.clone()) + - dst_limb_3_col15.clone()) + - (M31_0.clone() * sub_p_bit_col98.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1019.clone() + * ((carry_tmp_1019.clone() * carry_tmp_1019.clone()) - M31_1.clone())), + ); + let carry_tmp_1020 = (((((op0_limb_4_col45.clone() + op1_limb_4_col74.clone()) + + carry_tmp_1019.clone()) + - dst_limb_4_col16.clone()) + - (M31_0.clone() * sub_p_bit_col98.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1020.clone() + * ((carry_tmp_1020.clone() * carry_tmp_1020.clone()) - M31_1.clone())), + ); + let carry_tmp_1021 = (((((op0_limb_5_col46.clone() + op1_limb_5_col75.clone()) + + carry_tmp_1020.clone()) + - dst_limb_5_col17.clone()) + - (M31_0.clone() * sub_p_bit_col98.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1021.clone() + * ((carry_tmp_1021.clone() * carry_tmp_1021.clone()) - M31_1.clone())), + ); + let carry_tmp_1022 = (((((op0_limb_6_col47.clone() + op1_limb_6_col76.clone()) + + carry_tmp_1021.clone()) + - dst_limb_6_col18.clone()) + - (M31_0.clone() * sub_p_bit_col98.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1022.clone() + * ((carry_tmp_1022.clone() * carry_tmp_1022.clone()) - M31_1.clone())), + ); + let carry_tmp_1023 = (((((op0_limb_7_col48.clone() + op1_limb_7_col77.clone()) + + carry_tmp_1022.clone()) + - dst_limb_7_col19.clone()) + - (M31_0.clone() * sub_p_bit_col98.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1023.clone() + * ((carry_tmp_1023.clone() * carry_tmp_1023.clone()) - M31_1.clone())), + ); + let carry_tmp_1024 = (((((op0_limb_8_col49.clone() + op1_limb_8_col78.clone()) + + carry_tmp_1023.clone()) + - dst_limb_8_col20.clone()) + - (M31_0.clone() * sub_p_bit_col98.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1024.clone() + * ((carry_tmp_1024.clone() * carry_tmp_1024.clone()) - M31_1.clone())), + ); + let carry_tmp_1025 = (((((op0_limb_9_col50.clone() + op1_limb_9_col79.clone()) + + carry_tmp_1024.clone()) + - dst_limb_9_col21.clone()) + - (M31_0.clone() * sub_p_bit_col98.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1025.clone() + * ((carry_tmp_1025.clone() * carry_tmp_1025.clone()) - M31_1.clone())), + ); + let carry_tmp_1026 = (((((op0_limb_10_col51.clone() + op1_limb_10_col80.clone()) + + carry_tmp_1025.clone()) + - dst_limb_10_col22.clone()) + - (M31_0.clone() * sub_p_bit_col98.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1026.clone() + * ((carry_tmp_1026.clone() * carry_tmp_1026.clone()) - M31_1.clone())), + ); + let carry_tmp_1027 = (((((op0_limb_11_col52.clone() + op1_limb_11_col81.clone()) + + carry_tmp_1026.clone()) + - dst_limb_11_col23.clone()) + - (M31_0.clone() * sub_p_bit_col98.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1027.clone() + * ((carry_tmp_1027.clone() * carry_tmp_1027.clone()) - M31_1.clone())), + ); + let carry_tmp_1028 = (((((op0_limb_12_col53.clone() + op1_limb_12_col82.clone()) + + carry_tmp_1027.clone()) + - dst_limb_12_col24.clone()) + - (M31_0.clone() * sub_p_bit_col98.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1028.clone() + * ((carry_tmp_1028.clone() * carry_tmp_1028.clone()) - M31_1.clone())), + ); + let carry_tmp_1029 = (((((op0_limb_13_col54.clone() + op1_limb_13_col83.clone()) + + carry_tmp_1028.clone()) + - dst_limb_13_col25.clone()) + - (M31_0.clone() * sub_p_bit_col98.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1029.clone() + * ((carry_tmp_1029.clone() * carry_tmp_1029.clone()) - M31_1.clone())), + ); + let carry_tmp_1030 = (((((op0_limb_14_col55.clone() + op1_limb_14_col84.clone()) + + carry_tmp_1029.clone()) + - dst_limb_14_col26.clone()) + - (M31_0.clone() * sub_p_bit_col98.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1030.clone() + * ((carry_tmp_1030.clone() * carry_tmp_1030.clone()) - M31_1.clone())), + ); + let carry_tmp_1031 = (((((op0_limb_15_col56.clone() + op1_limb_15_col85.clone()) + + carry_tmp_1030.clone()) + - dst_limb_15_col27.clone()) + - (M31_0.clone() * sub_p_bit_col98.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1031.clone() + * ((carry_tmp_1031.clone() * carry_tmp_1031.clone()) - M31_1.clone())), + ); + let carry_tmp_1032 = (((((op0_limb_16_col57.clone() + op1_limb_16_col86.clone()) + + carry_tmp_1031.clone()) + - dst_limb_16_col28.clone()) + - (M31_0.clone() * sub_p_bit_col98.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1032.clone() + * ((carry_tmp_1032.clone() * carry_tmp_1032.clone()) - M31_1.clone())), + ); + let carry_tmp_1033 = (((((op0_limb_17_col58.clone() + op1_limb_17_col87.clone()) + + carry_tmp_1032.clone()) + - dst_limb_17_col29.clone()) + - (M31_0.clone() * sub_p_bit_col98.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1033.clone() + * ((carry_tmp_1033.clone() * carry_tmp_1033.clone()) - M31_1.clone())), + ); + let carry_tmp_1034 = (((((op0_limb_18_col59.clone() + op1_limb_18_col88.clone()) + + carry_tmp_1033.clone()) + - dst_limb_18_col30.clone()) + - (M31_0.clone() * sub_p_bit_col98.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1034.clone() + * ((carry_tmp_1034.clone() * carry_tmp_1034.clone()) - M31_1.clone())), + ); + let carry_tmp_1035 = (((((op0_limb_19_col60.clone() + op1_limb_19_col89.clone()) + + carry_tmp_1034.clone()) + - dst_limb_19_col31.clone()) + - (M31_0.clone() * sub_p_bit_col98.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1035.clone() + * ((carry_tmp_1035.clone() * carry_tmp_1035.clone()) - M31_1.clone())), + ); + let carry_tmp_1036 = (((((op0_limb_20_col61.clone() + op1_limb_20_col90.clone()) + + carry_tmp_1035.clone()) + - dst_limb_20_col32.clone()) + - (M31_0.clone() * sub_p_bit_col98.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1036.clone() + * ((carry_tmp_1036.clone() * carry_tmp_1036.clone()) - M31_1.clone())), + ); + let carry_tmp_1037 = (((((op0_limb_21_col62.clone() + op1_limb_21_col91.clone()) + + carry_tmp_1036.clone()) + - dst_limb_21_col33.clone()) + - (M31_136.clone() * sub_p_bit_col98.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1037.clone() + * ((carry_tmp_1037.clone() * carry_tmp_1037.clone()) - M31_1.clone())), + ); + let carry_tmp_1038 = (((((op0_limb_22_col63.clone() + op1_limb_22_col92.clone()) + + carry_tmp_1037.clone()) + - dst_limb_22_col34.clone()) + - (M31_0.clone() * sub_p_bit_col98.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1038.clone() + * ((carry_tmp_1038.clone() * carry_tmp_1038.clone()) - M31_1.clone())), + ); + let carry_tmp_1039 = (((((op0_limb_23_col64.clone() + op1_limb_23_col93.clone()) + + carry_tmp_1038.clone()) + - dst_limb_23_col35.clone()) + - (M31_0.clone() * sub_p_bit_col98.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1039.clone() + * ((carry_tmp_1039.clone() * carry_tmp_1039.clone()) - M31_1.clone())), + ); + let carry_tmp_1040 = (((((op0_limb_24_col65.clone() + op1_limb_24_col94.clone()) + + carry_tmp_1039.clone()) + - dst_limb_24_col36.clone()) + - (M31_0.clone() * sub_p_bit_col98.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1040.clone() + * ((carry_tmp_1040.clone() * carry_tmp_1040.clone()) - M31_1.clone())), + ); + let carry_tmp_1041 = (((((op0_limb_25_col66.clone() + op1_limb_25_col95.clone()) + + carry_tmp_1040.clone()) + - dst_limb_25_col37.clone()) + - (M31_0.clone() * sub_p_bit_col98.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1041.clone() + * ((carry_tmp_1041.clone() * carry_tmp_1041.clone()) - M31_1.clone())), + ); + let carry_tmp_1042 = (((((op0_limb_26_col67.clone() + op1_limb_26_col96.clone()) + + carry_tmp_1041.clone()) + - dst_limb_26_col38.clone()) + - (M31_0.clone() * sub_p_bit_col98.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1042.clone() + * ((carry_tmp_1042.clone() * carry_tmp_1042.clone()) - M31_1.clone())), + ); + eval.add_constraint( + ((((op0_limb_27_col68.clone() + op1_limb_27_col97.clone()) + carry_tmp_1042.clone()) + - dst_limb_27_col39.clone()) + - (M31_256.clone() * sub_p_bit_col98.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() + M31_1.clone()), + (input_ap_col1.clone() + ap_update_add_1_col10.clone()), + input_fp_col2.clone(), + ], + )]); + + eval.finalize_logup(); + eval + } +} diff --git a/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_f_is_imm_f/mod.rs b/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_f_is_imm_f/mod.rs new file mode 100644 index 00000000..3f7a8d74 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_f_is_imm_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/add_opcode_is_small_f_is_imm_f/prover.rs b/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_f_is_imm_f/prover.rs new file mode 100644 index 00000000..e0562af2 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_f_is_imm_f/prover.rs @@ -0,0 +1,814 @@ +#![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 = 99; + +#[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; 3], + pub memory_id_to_big_inputs: [Vec; 3], + 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), + Vec::with_capacity(capacity), + ], + memory_id_to_big_inputs: [ + Vec::with_capacity(capacity), + 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 = 99; + 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_32768 = PackedM31::broadcast(M31::from(32768)); + let UInt16_0 = PackedUInt16::broadcast(UInt16::from(0)); + let UInt16_1 = PackedUInt16::broadcast(UInt16::from(1)); + let UInt16_11 = PackedUInt16::broadcast(UInt16::from(11)); + let UInt16_127 = PackedUInt16::broadcast(UInt16::from(127)); + 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)); + let UInt16_9 = PackedUInt16::broadcast(UInt16::from(9)); + + inputs + .into_iter() + .enumerate() + .for_each(|(row_index, add_opcode_is_small_f_is_imm_f_input)| { + let input_tmp_986 = add_opcode_is_small_f_is_imm_f_input; + let input_pc_col0 = input_tmp_986.pc; + trace[0].data[row_index] = input_pc_col0; + let input_ap_col1 = input_tmp_986.ap; + trace[1].data[row_index] = input_ap_col1; + let input_fp_col2 = input_tmp_986.fp; + trace[2].data[row_index] = input_fp_col2; + + // decode_instruction_52ce7a4a3d9be19a. + + let memory_address_to_id_value_tmp_998 = + memory_address_to_id_state.deduce_output(input_pc_col0); + let memory_id_to_big_value_tmp_999 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_998); + let offset0_tmp_1000 = + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_999.get_m31(0))) + + (((PackedUInt16::from_m31(memory_id_to_big_value_tmp_999.get_m31(1))) + & (UInt16_127)) + << (UInt16_9))); + let offset0_col3 = offset0_tmp_1000.as_m31(); + trace[3].data[row_index] = offset0_col3; + let offset1_tmp_1001 = + ((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_999.get_m31(1))) + >> (UInt16_7)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_999.get_m31(2))) + << (UInt16_2))) + + (((PackedUInt16::from_m31(memory_id_to_big_value_tmp_999.get_m31(3))) + & (UInt16_31)) + << (UInt16_11))); + let offset1_col4 = offset1_tmp_1001.as_m31(); + trace[4].data[row_index] = offset1_col4; + let offset2_tmp_1002 = + ((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_999.get_m31(3))) + >> (UInt16_5)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_999.get_m31(4))) + << (UInt16_4))) + + (((PackedUInt16::from_m31(memory_id_to_big_value_tmp_999.get_m31(5))) + & (UInt16_7)) + << (UInt16_13))); + let offset2_col5 = offset2_tmp_1002.as_m31(); + trace[5].data[row_index] = offset2_col5; + let dst_base_fp_tmp_1003 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_999.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_999.get_m31(6))) + << (UInt16_6))) + >> (UInt16_0)) + & (UInt16_1)); + let dst_base_fp_col6 = dst_base_fp_tmp_1003.as_m31(); + trace[6].data[row_index] = dst_base_fp_col6; + let op0_base_fp_tmp_1004 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_999.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_999.get_m31(6))) + << (UInt16_6))) + >> (UInt16_1)) + & (UInt16_1)); + let op0_base_fp_col7 = op0_base_fp_tmp_1004.as_m31(); + trace[7].data[row_index] = op0_base_fp_col7; + let op1_base_fp_tmp_1005 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_999.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_999.get_m31(6))) + << (UInt16_6))) + >> (UInt16_3)) + & (UInt16_1)); + let op1_base_fp_col8 = op1_base_fp_tmp_1005.as_m31(); + trace[8].data[row_index] = op1_base_fp_col8; + let op1_base_ap_tmp_1006 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_999.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_999.get_m31(6))) + << (UInt16_6))) + >> (UInt16_4)) + & (UInt16_1)); + let op1_base_ap_col9 = op1_base_ap_tmp_1006.as_m31(); + trace[9].data[row_index] = op1_base_ap_col9; + let ap_update_add_1_tmp_1007 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_999.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_999.get_m31(6))) + << (UInt16_6))) + >> (UInt16_11)) + & (UInt16_1)); + let ap_update_add_1_col10 = ap_update_add_1_tmp_1007.as_m31(); + trace[10].data[row_index] = ap_update_add_1_col10; + + sub_components_inputs.verify_instruction_inputs[0].extend( + ( + input_pc_col0, + [offset0_col3, offset1_col4, offset2_col5], + [ + dst_base_fp_col6, + op0_base_fp_col7, + M31_0, + op1_base_fp_col8, + op1_base_ap_col9, + M31_1, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + ap_update_add_1_col10, + M31_0, + M31_0, + M31_1, + ], + ) + .unpack(), + ); + + lookup_data.verifyinstruction[0].push([ + input_pc_col0, + offset0_col3, + offset1_col4, + offset2_col5, + dst_base_fp_col6, + op0_base_fp_col7, + M31_0, + op1_base_fp_col8, + op1_base_ap_col9, + M31_1, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + ap_update_add_1_col10, + M31_0, + M31_0, + M31_1, + ]); + + // read_positive_num_bits_252. + + let memory_address_to_id_value_tmp_1009 = memory_address_to_id_state.deduce_output( + ((((dst_base_fp_col6) * (input_fp_col2)) + + (((M31_1) - (dst_base_fp_col6)) * (input_ap_col1))) + + ((offset0_col3) - (M31_32768))), + ); + let memory_id_to_big_value_tmp_1010 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1009); + let dst_id_col11 = memory_address_to_id_value_tmp_1009; + trace[11].data[row_index] = dst_id_col11; + sub_components_inputs.memory_address_to_id_inputs[0].extend( + ((((dst_base_fp_col6) * (input_fp_col2)) + + (((M31_1) - (dst_base_fp_col6)) * (input_ap_col1))) + + ((offset0_col3) - (M31_32768))) + .unpack(), + ); + + lookup_data.memoryaddresstoid[0].push([ + ((((dst_base_fp_col6) * (input_fp_col2)) + + (((M31_1) - (dst_base_fp_col6)) * (input_ap_col1))) + + ((offset0_col3) - (M31_32768))), + dst_id_col11, + ]); + let dst_limb_0_col12 = memory_id_to_big_value_tmp_1010.get_m31(0); + trace[12].data[row_index] = dst_limb_0_col12; + let dst_limb_1_col13 = memory_id_to_big_value_tmp_1010.get_m31(1); + trace[13].data[row_index] = dst_limb_1_col13; + let dst_limb_2_col14 = memory_id_to_big_value_tmp_1010.get_m31(2); + trace[14].data[row_index] = dst_limb_2_col14; + let dst_limb_3_col15 = memory_id_to_big_value_tmp_1010.get_m31(3); + trace[15].data[row_index] = dst_limb_3_col15; + let dst_limb_4_col16 = memory_id_to_big_value_tmp_1010.get_m31(4); + trace[16].data[row_index] = dst_limb_4_col16; + let dst_limb_5_col17 = memory_id_to_big_value_tmp_1010.get_m31(5); + trace[17].data[row_index] = dst_limb_5_col17; + let dst_limb_6_col18 = memory_id_to_big_value_tmp_1010.get_m31(6); + trace[18].data[row_index] = dst_limb_6_col18; + let dst_limb_7_col19 = memory_id_to_big_value_tmp_1010.get_m31(7); + trace[19].data[row_index] = dst_limb_7_col19; + let dst_limb_8_col20 = memory_id_to_big_value_tmp_1010.get_m31(8); + trace[20].data[row_index] = dst_limb_8_col20; + let dst_limb_9_col21 = memory_id_to_big_value_tmp_1010.get_m31(9); + trace[21].data[row_index] = dst_limb_9_col21; + let dst_limb_10_col22 = memory_id_to_big_value_tmp_1010.get_m31(10); + trace[22].data[row_index] = dst_limb_10_col22; + let dst_limb_11_col23 = memory_id_to_big_value_tmp_1010.get_m31(11); + trace[23].data[row_index] = dst_limb_11_col23; + let dst_limb_12_col24 = memory_id_to_big_value_tmp_1010.get_m31(12); + trace[24].data[row_index] = dst_limb_12_col24; + let dst_limb_13_col25 = memory_id_to_big_value_tmp_1010.get_m31(13); + trace[25].data[row_index] = dst_limb_13_col25; + let dst_limb_14_col26 = memory_id_to_big_value_tmp_1010.get_m31(14); + trace[26].data[row_index] = dst_limb_14_col26; + let dst_limb_15_col27 = memory_id_to_big_value_tmp_1010.get_m31(15); + trace[27].data[row_index] = dst_limb_15_col27; + let dst_limb_16_col28 = memory_id_to_big_value_tmp_1010.get_m31(16); + trace[28].data[row_index] = dst_limb_16_col28; + let dst_limb_17_col29 = memory_id_to_big_value_tmp_1010.get_m31(17); + trace[29].data[row_index] = dst_limb_17_col29; + let dst_limb_18_col30 = memory_id_to_big_value_tmp_1010.get_m31(18); + trace[30].data[row_index] = dst_limb_18_col30; + let dst_limb_19_col31 = memory_id_to_big_value_tmp_1010.get_m31(19); + trace[31].data[row_index] = dst_limb_19_col31; + let dst_limb_20_col32 = memory_id_to_big_value_tmp_1010.get_m31(20); + trace[32].data[row_index] = dst_limb_20_col32; + let dst_limb_21_col33 = memory_id_to_big_value_tmp_1010.get_m31(21); + trace[33].data[row_index] = dst_limb_21_col33; + let dst_limb_22_col34 = memory_id_to_big_value_tmp_1010.get_m31(22); + trace[34].data[row_index] = dst_limb_22_col34; + let dst_limb_23_col35 = memory_id_to_big_value_tmp_1010.get_m31(23); + trace[35].data[row_index] = dst_limb_23_col35; + let dst_limb_24_col36 = memory_id_to_big_value_tmp_1010.get_m31(24); + trace[36].data[row_index] = dst_limb_24_col36; + let dst_limb_25_col37 = memory_id_to_big_value_tmp_1010.get_m31(25); + trace[37].data[row_index] = dst_limb_25_col37; + let dst_limb_26_col38 = memory_id_to_big_value_tmp_1010.get_m31(26); + trace[38].data[row_index] = dst_limb_26_col38; + let dst_limb_27_col39 = memory_id_to_big_value_tmp_1010.get_m31(27); + trace[39].data[row_index] = dst_limb_27_col39; + sub_components_inputs.memory_id_to_big_inputs[0].extend(dst_id_col11.unpack()); + + lookup_data.memoryidtobig[0].push([ + dst_id_col11, + dst_limb_0_col12, + dst_limb_1_col13, + dst_limb_2_col14, + dst_limb_3_col15, + dst_limb_4_col16, + dst_limb_5_col17, + dst_limb_6_col18, + dst_limb_7_col19, + dst_limb_8_col20, + dst_limb_9_col21, + dst_limb_10_col22, + dst_limb_11_col23, + dst_limb_12_col24, + dst_limb_13_col25, + dst_limb_14_col26, + dst_limb_15_col27, + dst_limb_16_col28, + dst_limb_17_col29, + dst_limb_18_col30, + dst_limb_19_col31, + dst_limb_20_col32, + dst_limb_21_col33, + dst_limb_22_col34, + dst_limb_23_col35, + dst_limb_24_col36, + dst_limb_25_col37, + dst_limb_26_col38, + dst_limb_27_col39, + ]); + + // read_positive_num_bits_252. + + let memory_address_to_id_value_tmp_1011 = memory_address_to_id_state.deduce_output( + ((((op0_base_fp_col7) * (input_fp_col2)) + + (((M31_1) - (op0_base_fp_col7)) * (input_ap_col1))) + + ((offset1_col4) - (M31_32768))), + ); + let memory_id_to_big_value_tmp_1012 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1011); + let op0_id_col40 = memory_address_to_id_value_tmp_1011; + trace[40].data[row_index] = op0_id_col40; + sub_components_inputs.memory_address_to_id_inputs[1].extend( + ((((op0_base_fp_col7) * (input_fp_col2)) + + (((M31_1) - (op0_base_fp_col7)) * (input_ap_col1))) + + ((offset1_col4) - (M31_32768))) + .unpack(), + ); + + lookup_data.memoryaddresstoid[1].push([ + ((((op0_base_fp_col7) * (input_fp_col2)) + + (((M31_1) - (op0_base_fp_col7)) * (input_ap_col1))) + + ((offset1_col4) - (M31_32768))), + op0_id_col40, + ]); + let op0_limb_0_col41 = memory_id_to_big_value_tmp_1012.get_m31(0); + trace[41].data[row_index] = op0_limb_0_col41; + let op0_limb_1_col42 = memory_id_to_big_value_tmp_1012.get_m31(1); + trace[42].data[row_index] = op0_limb_1_col42; + let op0_limb_2_col43 = memory_id_to_big_value_tmp_1012.get_m31(2); + trace[43].data[row_index] = op0_limb_2_col43; + let op0_limb_3_col44 = memory_id_to_big_value_tmp_1012.get_m31(3); + trace[44].data[row_index] = op0_limb_3_col44; + let op0_limb_4_col45 = memory_id_to_big_value_tmp_1012.get_m31(4); + trace[45].data[row_index] = op0_limb_4_col45; + let op0_limb_5_col46 = memory_id_to_big_value_tmp_1012.get_m31(5); + trace[46].data[row_index] = op0_limb_5_col46; + let op0_limb_6_col47 = memory_id_to_big_value_tmp_1012.get_m31(6); + trace[47].data[row_index] = op0_limb_6_col47; + let op0_limb_7_col48 = memory_id_to_big_value_tmp_1012.get_m31(7); + trace[48].data[row_index] = op0_limb_7_col48; + let op0_limb_8_col49 = memory_id_to_big_value_tmp_1012.get_m31(8); + trace[49].data[row_index] = op0_limb_8_col49; + let op0_limb_9_col50 = memory_id_to_big_value_tmp_1012.get_m31(9); + trace[50].data[row_index] = op0_limb_9_col50; + let op0_limb_10_col51 = memory_id_to_big_value_tmp_1012.get_m31(10); + trace[51].data[row_index] = op0_limb_10_col51; + let op0_limb_11_col52 = memory_id_to_big_value_tmp_1012.get_m31(11); + trace[52].data[row_index] = op0_limb_11_col52; + let op0_limb_12_col53 = memory_id_to_big_value_tmp_1012.get_m31(12); + trace[53].data[row_index] = op0_limb_12_col53; + let op0_limb_13_col54 = memory_id_to_big_value_tmp_1012.get_m31(13); + trace[54].data[row_index] = op0_limb_13_col54; + let op0_limb_14_col55 = memory_id_to_big_value_tmp_1012.get_m31(14); + trace[55].data[row_index] = op0_limb_14_col55; + let op0_limb_15_col56 = memory_id_to_big_value_tmp_1012.get_m31(15); + trace[56].data[row_index] = op0_limb_15_col56; + let op0_limb_16_col57 = memory_id_to_big_value_tmp_1012.get_m31(16); + trace[57].data[row_index] = op0_limb_16_col57; + let op0_limb_17_col58 = memory_id_to_big_value_tmp_1012.get_m31(17); + trace[58].data[row_index] = op0_limb_17_col58; + let op0_limb_18_col59 = memory_id_to_big_value_tmp_1012.get_m31(18); + trace[59].data[row_index] = op0_limb_18_col59; + let op0_limb_19_col60 = memory_id_to_big_value_tmp_1012.get_m31(19); + trace[60].data[row_index] = op0_limb_19_col60; + let op0_limb_20_col61 = memory_id_to_big_value_tmp_1012.get_m31(20); + trace[61].data[row_index] = op0_limb_20_col61; + let op0_limb_21_col62 = memory_id_to_big_value_tmp_1012.get_m31(21); + trace[62].data[row_index] = op0_limb_21_col62; + let op0_limb_22_col63 = memory_id_to_big_value_tmp_1012.get_m31(22); + trace[63].data[row_index] = op0_limb_22_col63; + let op0_limb_23_col64 = memory_id_to_big_value_tmp_1012.get_m31(23); + trace[64].data[row_index] = op0_limb_23_col64; + let op0_limb_24_col65 = memory_id_to_big_value_tmp_1012.get_m31(24); + trace[65].data[row_index] = op0_limb_24_col65; + let op0_limb_25_col66 = memory_id_to_big_value_tmp_1012.get_m31(25); + trace[66].data[row_index] = op0_limb_25_col66; + let op0_limb_26_col67 = memory_id_to_big_value_tmp_1012.get_m31(26); + trace[67].data[row_index] = op0_limb_26_col67; + let op0_limb_27_col68 = memory_id_to_big_value_tmp_1012.get_m31(27); + trace[68].data[row_index] = op0_limb_27_col68; + sub_components_inputs.memory_id_to_big_inputs[1].extend(op0_id_col40.unpack()); + + lookup_data.memoryidtobig[1].push([ + op0_id_col40, + op0_limb_0_col41, + op0_limb_1_col42, + op0_limb_2_col43, + op0_limb_3_col44, + op0_limb_4_col45, + op0_limb_5_col46, + op0_limb_6_col47, + op0_limb_7_col48, + op0_limb_8_col49, + op0_limb_9_col50, + op0_limb_10_col51, + op0_limb_11_col52, + op0_limb_12_col53, + op0_limb_13_col54, + op0_limb_14_col55, + op0_limb_15_col56, + op0_limb_16_col57, + op0_limb_17_col58, + op0_limb_18_col59, + op0_limb_19_col60, + op0_limb_20_col61, + op0_limb_21_col62, + op0_limb_22_col63, + op0_limb_23_col64, + op0_limb_24_col65, + op0_limb_25_col66, + op0_limb_26_col67, + op0_limb_27_col68, + ]); + + // read_positive_num_bits_252. + + let memory_address_to_id_value_tmp_1013 = memory_address_to_id_state.deduce_output( + ((((op1_base_fp_col8) * (input_fp_col2)) + ((op1_base_ap_col9) * (input_ap_col1))) + + ((offset2_col5) - (M31_32768))), + ); + let memory_id_to_big_value_tmp_1014 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1013); + let op1_id_col69 = memory_address_to_id_value_tmp_1013; + trace[69].data[row_index] = op1_id_col69; + sub_components_inputs.memory_address_to_id_inputs[2].extend( + ((((op1_base_fp_col8) * (input_fp_col2)) + ((op1_base_ap_col9) * (input_ap_col1))) + + ((offset2_col5) - (M31_32768))) + .unpack(), + ); + + lookup_data.memoryaddresstoid[2].push([ + ((((op1_base_fp_col8) * (input_fp_col2)) + ((op1_base_ap_col9) * (input_ap_col1))) + + ((offset2_col5) - (M31_32768))), + op1_id_col69, + ]); + let op1_limb_0_col70 = memory_id_to_big_value_tmp_1014.get_m31(0); + trace[70].data[row_index] = op1_limb_0_col70; + let op1_limb_1_col71 = memory_id_to_big_value_tmp_1014.get_m31(1); + trace[71].data[row_index] = op1_limb_1_col71; + let op1_limb_2_col72 = memory_id_to_big_value_tmp_1014.get_m31(2); + trace[72].data[row_index] = op1_limb_2_col72; + let op1_limb_3_col73 = memory_id_to_big_value_tmp_1014.get_m31(3); + trace[73].data[row_index] = op1_limb_3_col73; + let op1_limb_4_col74 = memory_id_to_big_value_tmp_1014.get_m31(4); + trace[74].data[row_index] = op1_limb_4_col74; + let op1_limb_5_col75 = memory_id_to_big_value_tmp_1014.get_m31(5); + trace[75].data[row_index] = op1_limb_5_col75; + let op1_limb_6_col76 = memory_id_to_big_value_tmp_1014.get_m31(6); + trace[76].data[row_index] = op1_limb_6_col76; + let op1_limb_7_col77 = memory_id_to_big_value_tmp_1014.get_m31(7); + trace[77].data[row_index] = op1_limb_7_col77; + let op1_limb_8_col78 = memory_id_to_big_value_tmp_1014.get_m31(8); + trace[78].data[row_index] = op1_limb_8_col78; + let op1_limb_9_col79 = memory_id_to_big_value_tmp_1014.get_m31(9); + trace[79].data[row_index] = op1_limb_9_col79; + let op1_limb_10_col80 = memory_id_to_big_value_tmp_1014.get_m31(10); + trace[80].data[row_index] = op1_limb_10_col80; + let op1_limb_11_col81 = memory_id_to_big_value_tmp_1014.get_m31(11); + trace[81].data[row_index] = op1_limb_11_col81; + let op1_limb_12_col82 = memory_id_to_big_value_tmp_1014.get_m31(12); + trace[82].data[row_index] = op1_limb_12_col82; + let op1_limb_13_col83 = memory_id_to_big_value_tmp_1014.get_m31(13); + trace[83].data[row_index] = op1_limb_13_col83; + let op1_limb_14_col84 = memory_id_to_big_value_tmp_1014.get_m31(14); + trace[84].data[row_index] = op1_limb_14_col84; + let op1_limb_15_col85 = memory_id_to_big_value_tmp_1014.get_m31(15); + trace[85].data[row_index] = op1_limb_15_col85; + let op1_limb_16_col86 = memory_id_to_big_value_tmp_1014.get_m31(16); + trace[86].data[row_index] = op1_limb_16_col86; + let op1_limb_17_col87 = memory_id_to_big_value_tmp_1014.get_m31(17); + trace[87].data[row_index] = op1_limb_17_col87; + let op1_limb_18_col88 = memory_id_to_big_value_tmp_1014.get_m31(18); + trace[88].data[row_index] = op1_limb_18_col88; + let op1_limb_19_col89 = memory_id_to_big_value_tmp_1014.get_m31(19); + trace[89].data[row_index] = op1_limb_19_col89; + let op1_limb_20_col90 = memory_id_to_big_value_tmp_1014.get_m31(20); + trace[90].data[row_index] = op1_limb_20_col90; + let op1_limb_21_col91 = memory_id_to_big_value_tmp_1014.get_m31(21); + trace[91].data[row_index] = op1_limb_21_col91; + let op1_limb_22_col92 = memory_id_to_big_value_tmp_1014.get_m31(22); + trace[92].data[row_index] = op1_limb_22_col92; + let op1_limb_23_col93 = memory_id_to_big_value_tmp_1014.get_m31(23); + trace[93].data[row_index] = op1_limb_23_col93; + let op1_limb_24_col94 = memory_id_to_big_value_tmp_1014.get_m31(24); + trace[94].data[row_index] = op1_limb_24_col94; + let op1_limb_25_col95 = memory_id_to_big_value_tmp_1014.get_m31(25); + trace[95].data[row_index] = op1_limb_25_col95; + let op1_limb_26_col96 = memory_id_to_big_value_tmp_1014.get_m31(26); + trace[96].data[row_index] = op1_limb_26_col96; + let op1_limb_27_col97 = memory_id_to_big_value_tmp_1014.get_m31(27); + trace[97].data[row_index] = op1_limb_27_col97; + sub_components_inputs.memory_id_to_big_inputs[2].extend(op1_id_col69.unpack()); + + lookup_data.memoryidtobig[2].push([ + op1_id_col69, + op1_limb_0_col70, + op1_limb_1_col71, + op1_limb_2_col72, + op1_limb_3_col73, + op1_limb_4_col74, + op1_limb_5_col75, + op1_limb_6_col76, + op1_limb_7_col77, + op1_limb_8_col78, + op1_limb_9_col79, + op1_limb_10_col80, + op1_limb_11_col81, + op1_limb_12_col82, + op1_limb_13_col83, + op1_limb_14_col84, + op1_limb_15_col85, + op1_limb_16_col86, + op1_limb_17_col87, + op1_limb_18_col88, + op1_limb_19_col89, + op1_limb_20_col90, + op1_limb_21_col91, + op1_limb_22_col92, + op1_limb_23_col93, + op1_limb_24_col94, + op1_limb_25_col95, + op1_limb_26_col96, + op1_limb_27_col97, + ]); + + // verify_add252. + + let sub_p_bit_tmp_1015 = ((UInt16_1) + & (((PackedUInt16::from_m31(op0_limb_0_col41)) + ^ (PackedUInt16::from_m31(op1_limb_0_col70))) + ^ (PackedUInt16::from_m31(dst_limb_0_col12)))); + let sub_p_bit_col98 = sub_p_bit_tmp_1015.as_m31(); + trace[98].data[row_index] = sub_p_bit_col98; + + lookup_data.opcodes[0].push([input_pc_col0, input_ap_col1, input_fp_col2]); + lookup_data.opcodes[1].push([ + ((input_pc_col0) + (M31_1)), + ((input_ap_col1) + (ap_update_add_1_col10)), + input_fp_col2, + ]); + }); + + (trace, sub_components_inputs, lookup_data) +} + +pub struct LookupData { + pub memoryaddresstoid: [Vec<[PackedM31; 2]>; 3], + pub memoryidtobig: [Vec<[PackedM31; 29]>; 3], + 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), + Vec::with_capacity(capacity), + ], + memoryidtobig: [ + Vec::with_capacity(capacity), + 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.memoryaddresstoid[2]; + 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[2]; + 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/add_opcode_is_small_f_is_imm_t/component.rs b/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_f_is_imm_t/component.rs new file mode 100644 index 00000000..af331975 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_f_is_imm_t/component.rs @@ -0,0 +1,632 @@ +#![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; 96]; + let interaction_log_sizes = vec![log_size; SECURE_EXTENSION_DEGREE * 9]; + 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_136 = E::F::from(M31::from(136)); + let M31_2 = E::F::from(M31::from(2)); + let M31_256 = E::F::from(M31::from(256)); + let M31_32768 = E::F::from(M31::from(32768)); + let M31_32769 = E::F::from(M31::from(32769)); + let M31_4194304 = E::F::from(M31::from(4194304)); + 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 offset0_col3 = eval.next_trace_mask(); + let offset1_col4 = eval.next_trace_mask(); + let dst_base_fp_col5 = eval.next_trace_mask(); + let op0_base_fp_col6 = eval.next_trace_mask(); + let ap_update_add_1_col7 = eval.next_trace_mask(); + let dst_id_col8 = eval.next_trace_mask(); + let dst_limb_0_col9 = eval.next_trace_mask(); + let dst_limb_1_col10 = eval.next_trace_mask(); + let dst_limb_2_col11 = eval.next_trace_mask(); + let dst_limb_3_col12 = eval.next_trace_mask(); + let dst_limb_4_col13 = eval.next_trace_mask(); + let dst_limb_5_col14 = eval.next_trace_mask(); + let dst_limb_6_col15 = eval.next_trace_mask(); + let dst_limb_7_col16 = eval.next_trace_mask(); + let dst_limb_8_col17 = eval.next_trace_mask(); + let dst_limb_9_col18 = eval.next_trace_mask(); + let dst_limb_10_col19 = eval.next_trace_mask(); + let dst_limb_11_col20 = eval.next_trace_mask(); + let dst_limb_12_col21 = eval.next_trace_mask(); + let dst_limb_13_col22 = eval.next_trace_mask(); + let dst_limb_14_col23 = eval.next_trace_mask(); + let dst_limb_15_col24 = eval.next_trace_mask(); + let dst_limb_16_col25 = eval.next_trace_mask(); + let dst_limb_17_col26 = eval.next_trace_mask(); + let dst_limb_18_col27 = eval.next_trace_mask(); + let dst_limb_19_col28 = eval.next_trace_mask(); + let dst_limb_20_col29 = eval.next_trace_mask(); + let dst_limb_21_col30 = eval.next_trace_mask(); + let dst_limb_22_col31 = eval.next_trace_mask(); + let dst_limb_23_col32 = eval.next_trace_mask(); + let dst_limb_24_col33 = eval.next_trace_mask(); + let dst_limb_25_col34 = eval.next_trace_mask(); + let dst_limb_26_col35 = eval.next_trace_mask(); + let dst_limb_27_col36 = eval.next_trace_mask(); + let op0_id_col37 = eval.next_trace_mask(); + let op0_limb_0_col38 = eval.next_trace_mask(); + let op0_limb_1_col39 = eval.next_trace_mask(); + let op0_limb_2_col40 = eval.next_trace_mask(); + let op0_limb_3_col41 = eval.next_trace_mask(); + let op0_limb_4_col42 = eval.next_trace_mask(); + let op0_limb_5_col43 = eval.next_trace_mask(); + let op0_limb_6_col44 = eval.next_trace_mask(); + let op0_limb_7_col45 = eval.next_trace_mask(); + let op0_limb_8_col46 = eval.next_trace_mask(); + let op0_limb_9_col47 = eval.next_trace_mask(); + let op0_limb_10_col48 = eval.next_trace_mask(); + let op0_limb_11_col49 = eval.next_trace_mask(); + let op0_limb_12_col50 = eval.next_trace_mask(); + let op0_limb_13_col51 = eval.next_trace_mask(); + let op0_limb_14_col52 = eval.next_trace_mask(); + let op0_limb_15_col53 = eval.next_trace_mask(); + let op0_limb_16_col54 = eval.next_trace_mask(); + let op0_limb_17_col55 = eval.next_trace_mask(); + let op0_limb_18_col56 = eval.next_trace_mask(); + let op0_limb_19_col57 = eval.next_trace_mask(); + let op0_limb_20_col58 = eval.next_trace_mask(); + let op0_limb_21_col59 = eval.next_trace_mask(); + let op0_limb_22_col60 = eval.next_trace_mask(); + let op0_limb_23_col61 = eval.next_trace_mask(); + let op0_limb_24_col62 = eval.next_trace_mask(); + let op0_limb_25_col63 = eval.next_trace_mask(); + let op0_limb_26_col64 = eval.next_trace_mask(); + let op0_limb_27_col65 = eval.next_trace_mask(); + let op1_id_col66 = eval.next_trace_mask(); + let op1_limb_0_col67 = eval.next_trace_mask(); + let op1_limb_1_col68 = eval.next_trace_mask(); + let op1_limb_2_col69 = eval.next_trace_mask(); + let op1_limb_3_col70 = eval.next_trace_mask(); + let op1_limb_4_col71 = eval.next_trace_mask(); + let op1_limb_5_col72 = eval.next_trace_mask(); + let op1_limb_6_col73 = eval.next_trace_mask(); + let op1_limb_7_col74 = eval.next_trace_mask(); + let op1_limb_8_col75 = eval.next_trace_mask(); + let op1_limb_9_col76 = eval.next_trace_mask(); + let op1_limb_10_col77 = eval.next_trace_mask(); + let op1_limb_11_col78 = eval.next_trace_mask(); + let op1_limb_12_col79 = eval.next_trace_mask(); + let op1_limb_13_col80 = eval.next_trace_mask(); + let op1_limb_14_col81 = eval.next_trace_mask(); + let op1_limb_15_col82 = eval.next_trace_mask(); + let op1_limb_16_col83 = eval.next_trace_mask(); + let op1_limb_17_col84 = eval.next_trace_mask(); + let op1_limb_18_col85 = eval.next_trace_mask(); + let op1_limb_19_col86 = eval.next_trace_mask(); + let op1_limb_20_col87 = eval.next_trace_mask(); + let op1_limb_21_col88 = eval.next_trace_mask(); + let op1_limb_22_col89 = eval.next_trace_mask(); + let op1_limb_23_col90 = eval.next_trace_mask(); + let op1_limb_24_col91 = eval.next_trace_mask(); + let op1_limb_25_col92 = eval.next_trace_mask(); + let op1_limb_26_col93 = eval.next_trace_mask(); + let op1_limb_27_col94 = eval.next_trace_mask(); + let sub_p_bit_col95 = eval.next_trace_mask(); + + // decode_instruction_9aed6a790187299c. + + eval.add_to_relation(&[RelationEntry::new( + &self.verifyinstruction_lookup_elements, + E::EF::one(), + &[ + input_pc_col0.clone(), + offset0_col3.clone(), + offset1_col4.clone(), + M31_32769.clone(), + dst_base_fp_col5.clone(), + op0_base_fp_col6.clone(), + M31_1.clone(), + M31_0.clone(), + M31_0.clone(), + M31_1.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + ap_update_add_1_col7.clone(), + M31_0.clone(), + M31_0.clone(), + M31_1.clone(), + ], + )]); + + // read_positive_num_bits_252. + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryaddresstoid_lookup_elements, + E::EF::one(), + &[ + (((dst_base_fp_col5.clone() * input_fp_col2.clone()) + + ((M31_1.clone() - dst_base_fp_col5.clone()) * input_ap_col1.clone())) + + (offset0_col3.clone() - M31_32768.clone())), + dst_id_col8.clone(), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryidtobig_lookup_elements, + E::EF::one(), + &[ + dst_id_col8.clone(), + dst_limb_0_col9.clone(), + dst_limb_1_col10.clone(), + dst_limb_2_col11.clone(), + dst_limb_3_col12.clone(), + dst_limb_4_col13.clone(), + dst_limb_5_col14.clone(), + dst_limb_6_col15.clone(), + dst_limb_7_col16.clone(), + dst_limb_8_col17.clone(), + dst_limb_9_col18.clone(), + dst_limb_10_col19.clone(), + dst_limb_11_col20.clone(), + dst_limb_12_col21.clone(), + dst_limb_13_col22.clone(), + dst_limb_14_col23.clone(), + dst_limb_15_col24.clone(), + dst_limb_16_col25.clone(), + dst_limb_17_col26.clone(), + dst_limb_18_col27.clone(), + dst_limb_19_col28.clone(), + dst_limb_20_col29.clone(), + dst_limb_21_col30.clone(), + dst_limb_22_col31.clone(), + dst_limb_23_col32.clone(), + dst_limb_24_col33.clone(), + dst_limb_25_col34.clone(), + dst_limb_26_col35.clone(), + dst_limb_27_col36.clone(), + ], + )]); + + // read_positive_num_bits_252. + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryaddresstoid_lookup_elements, + E::EF::one(), + &[ + (((op0_base_fp_col6.clone() * input_fp_col2.clone()) + + ((M31_1.clone() - op0_base_fp_col6.clone()) * input_ap_col1.clone())) + + (offset1_col4.clone() - M31_32768.clone())), + op0_id_col37.clone(), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryidtobig_lookup_elements, + E::EF::one(), + &[ + op0_id_col37.clone(), + op0_limb_0_col38.clone(), + op0_limb_1_col39.clone(), + op0_limb_2_col40.clone(), + op0_limb_3_col41.clone(), + op0_limb_4_col42.clone(), + op0_limb_5_col43.clone(), + op0_limb_6_col44.clone(), + op0_limb_7_col45.clone(), + op0_limb_8_col46.clone(), + op0_limb_9_col47.clone(), + op0_limb_10_col48.clone(), + op0_limb_11_col49.clone(), + op0_limb_12_col50.clone(), + op0_limb_13_col51.clone(), + op0_limb_14_col52.clone(), + op0_limb_15_col53.clone(), + op0_limb_16_col54.clone(), + op0_limb_17_col55.clone(), + op0_limb_18_col56.clone(), + op0_limb_19_col57.clone(), + op0_limb_20_col58.clone(), + op0_limb_21_col59.clone(), + op0_limb_22_col60.clone(), + op0_limb_23_col61.clone(), + op0_limb_24_col62.clone(), + op0_limb_25_col63.clone(), + op0_limb_26_col64.clone(), + op0_limb_27_col65.clone(), + ], + )]); + + // read_positive_num_bits_252. + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryaddresstoid_lookup_elements, + E::EF::one(), + &[ + (input_pc_col0.clone() + M31_1.clone()), + op1_id_col66.clone(), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryidtobig_lookup_elements, + E::EF::one(), + &[ + op1_id_col66.clone(), + op1_limb_0_col67.clone(), + op1_limb_1_col68.clone(), + op1_limb_2_col69.clone(), + op1_limb_3_col70.clone(), + op1_limb_4_col71.clone(), + op1_limb_5_col72.clone(), + op1_limb_6_col73.clone(), + op1_limb_7_col74.clone(), + op1_limb_8_col75.clone(), + op1_limb_9_col76.clone(), + op1_limb_10_col77.clone(), + op1_limb_11_col78.clone(), + op1_limb_12_col79.clone(), + op1_limb_13_col80.clone(), + op1_limb_14_col81.clone(), + op1_limb_15_col82.clone(), + op1_limb_16_col83.clone(), + op1_limb_17_col84.clone(), + op1_limb_18_col85.clone(), + op1_limb_19_col86.clone(), + op1_limb_20_col87.clone(), + op1_limb_21_col88.clone(), + op1_limb_22_col89.clone(), + op1_limb_23_col90.clone(), + op1_limb_24_col91.clone(), + op1_limb_25_col92.clone(), + op1_limb_26_col93.clone(), + op1_limb_27_col94.clone(), + ], + )]); + + // verify_add252. + + // sub_p_bit is a bit. + eval.add_constraint((sub_p_bit_col95.clone() * (sub_p_bit_col95.clone() - M31_1.clone()))); + let carry_tmp_1083 = (((((op0_limb_0_col38.clone() + op1_limb_0_col67.clone()) + + M31_0.clone()) + - dst_limb_0_col9.clone()) + - (M31_1.clone() * sub_p_bit_col95.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1083.clone() + * ((carry_tmp_1083.clone() * carry_tmp_1083.clone()) - M31_1.clone())), + ); + let carry_tmp_1084 = (((((op0_limb_1_col39.clone() + op1_limb_1_col68.clone()) + + carry_tmp_1083.clone()) + - dst_limb_1_col10.clone()) + - (M31_0.clone() * sub_p_bit_col95.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1084.clone() + * ((carry_tmp_1084.clone() * carry_tmp_1084.clone()) - M31_1.clone())), + ); + let carry_tmp_1085 = (((((op0_limb_2_col40.clone() + op1_limb_2_col69.clone()) + + carry_tmp_1084.clone()) + - dst_limb_2_col11.clone()) + - (M31_0.clone() * sub_p_bit_col95.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1085.clone() + * ((carry_tmp_1085.clone() * carry_tmp_1085.clone()) - M31_1.clone())), + ); + let carry_tmp_1086 = (((((op0_limb_3_col41.clone() + op1_limb_3_col70.clone()) + + carry_tmp_1085.clone()) + - dst_limb_3_col12.clone()) + - (M31_0.clone() * sub_p_bit_col95.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1086.clone() + * ((carry_tmp_1086.clone() * carry_tmp_1086.clone()) - M31_1.clone())), + ); + let carry_tmp_1087 = (((((op0_limb_4_col42.clone() + op1_limb_4_col71.clone()) + + carry_tmp_1086.clone()) + - dst_limb_4_col13.clone()) + - (M31_0.clone() * sub_p_bit_col95.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1087.clone() + * ((carry_tmp_1087.clone() * carry_tmp_1087.clone()) - M31_1.clone())), + ); + let carry_tmp_1088 = (((((op0_limb_5_col43.clone() + op1_limb_5_col72.clone()) + + carry_tmp_1087.clone()) + - dst_limb_5_col14.clone()) + - (M31_0.clone() * sub_p_bit_col95.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1088.clone() + * ((carry_tmp_1088.clone() * carry_tmp_1088.clone()) - M31_1.clone())), + ); + let carry_tmp_1089 = (((((op0_limb_6_col44.clone() + op1_limb_6_col73.clone()) + + carry_tmp_1088.clone()) + - dst_limb_6_col15.clone()) + - (M31_0.clone() * sub_p_bit_col95.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1089.clone() + * ((carry_tmp_1089.clone() * carry_tmp_1089.clone()) - M31_1.clone())), + ); + let carry_tmp_1090 = (((((op0_limb_7_col45.clone() + op1_limb_7_col74.clone()) + + carry_tmp_1089.clone()) + - dst_limb_7_col16.clone()) + - (M31_0.clone() * sub_p_bit_col95.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1090.clone() + * ((carry_tmp_1090.clone() * carry_tmp_1090.clone()) - M31_1.clone())), + ); + let carry_tmp_1091 = (((((op0_limb_8_col46.clone() + op1_limb_8_col75.clone()) + + carry_tmp_1090.clone()) + - dst_limb_8_col17.clone()) + - (M31_0.clone() * sub_p_bit_col95.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1091.clone() + * ((carry_tmp_1091.clone() * carry_tmp_1091.clone()) - M31_1.clone())), + ); + let carry_tmp_1092 = (((((op0_limb_9_col47.clone() + op1_limb_9_col76.clone()) + + carry_tmp_1091.clone()) + - dst_limb_9_col18.clone()) + - (M31_0.clone() * sub_p_bit_col95.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1092.clone() + * ((carry_tmp_1092.clone() * carry_tmp_1092.clone()) - M31_1.clone())), + ); + let carry_tmp_1093 = (((((op0_limb_10_col48.clone() + op1_limb_10_col77.clone()) + + carry_tmp_1092.clone()) + - dst_limb_10_col19.clone()) + - (M31_0.clone() * sub_p_bit_col95.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1093.clone() + * ((carry_tmp_1093.clone() * carry_tmp_1093.clone()) - M31_1.clone())), + ); + let carry_tmp_1094 = (((((op0_limb_11_col49.clone() + op1_limb_11_col78.clone()) + + carry_tmp_1093.clone()) + - dst_limb_11_col20.clone()) + - (M31_0.clone() * sub_p_bit_col95.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1094.clone() + * ((carry_tmp_1094.clone() * carry_tmp_1094.clone()) - M31_1.clone())), + ); + let carry_tmp_1095 = (((((op0_limb_12_col50.clone() + op1_limb_12_col79.clone()) + + carry_tmp_1094.clone()) + - dst_limb_12_col21.clone()) + - (M31_0.clone() * sub_p_bit_col95.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1095.clone() + * ((carry_tmp_1095.clone() * carry_tmp_1095.clone()) - M31_1.clone())), + ); + let carry_tmp_1096 = (((((op0_limb_13_col51.clone() + op1_limb_13_col80.clone()) + + carry_tmp_1095.clone()) + - dst_limb_13_col22.clone()) + - (M31_0.clone() * sub_p_bit_col95.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1096.clone() + * ((carry_tmp_1096.clone() * carry_tmp_1096.clone()) - M31_1.clone())), + ); + let carry_tmp_1097 = (((((op0_limb_14_col52.clone() + op1_limb_14_col81.clone()) + + carry_tmp_1096.clone()) + - dst_limb_14_col23.clone()) + - (M31_0.clone() * sub_p_bit_col95.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1097.clone() + * ((carry_tmp_1097.clone() * carry_tmp_1097.clone()) - M31_1.clone())), + ); + let carry_tmp_1098 = (((((op0_limb_15_col53.clone() + op1_limb_15_col82.clone()) + + carry_tmp_1097.clone()) + - dst_limb_15_col24.clone()) + - (M31_0.clone() * sub_p_bit_col95.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1098.clone() + * ((carry_tmp_1098.clone() * carry_tmp_1098.clone()) - M31_1.clone())), + ); + let carry_tmp_1099 = (((((op0_limb_16_col54.clone() + op1_limb_16_col83.clone()) + + carry_tmp_1098.clone()) + - dst_limb_16_col25.clone()) + - (M31_0.clone() * sub_p_bit_col95.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1099.clone() + * ((carry_tmp_1099.clone() * carry_tmp_1099.clone()) - M31_1.clone())), + ); + let carry_tmp_1100 = (((((op0_limb_17_col55.clone() + op1_limb_17_col84.clone()) + + carry_tmp_1099.clone()) + - dst_limb_17_col26.clone()) + - (M31_0.clone() * sub_p_bit_col95.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1100.clone() + * ((carry_tmp_1100.clone() * carry_tmp_1100.clone()) - M31_1.clone())), + ); + let carry_tmp_1101 = (((((op0_limb_18_col56.clone() + op1_limb_18_col85.clone()) + + carry_tmp_1100.clone()) + - dst_limb_18_col27.clone()) + - (M31_0.clone() * sub_p_bit_col95.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1101.clone() + * ((carry_tmp_1101.clone() * carry_tmp_1101.clone()) - M31_1.clone())), + ); + let carry_tmp_1102 = (((((op0_limb_19_col57.clone() + op1_limb_19_col86.clone()) + + carry_tmp_1101.clone()) + - dst_limb_19_col28.clone()) + - (M31_0.clone() * sub_p_bit_col95.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1102.clone() + * ((carry_tmp_1102.clone() * carry_tmp_1102.clone()) - M31_1.clone())), + ); + let carry_tmp_1103 = (((((op0_limb_20_col58.clone() + op1_limb_20_col87.clone()) + + carry_tmp_1102.clone()) + - dst_limb_20_col29.clone()) + - (M31_0.clone() * sub_p_bit_col95.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1103.clone() + * ((carry_tmp_1103.clone() * carry_tmp_1103.clone()) - M31_1.clone())), + ); + let carry_tmp_1104 = (((((op0_limb_21_col59.clone() + op1_limb_21_col88.clone()) + + carry_tmp_1103.clone()) + - dst_limb_21_col30.clone()) + - (M31_136.clone() * sub_p_bit_col95.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1104.clone() + * ((carry_tmp_1104.clone() * carry_tmp_1104.clone()) - M31_1.clone())), + ); + let carry_tmp_1105 = (((((op0_limb_22_col60.clone() + op1_limb_22_col89.clone()) + + carry_tmp_1104.clone()) + - dst_limb_22_col31.clone()) + - (M31_0.clone() * sub_p_bit_col95.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1105.clone() + * ((carry_tmp_1105.clone() * carry_tmp_1105.clone()) - M31_1.clone())), + ); + let carry_tmp_1106 = (((((op0_limb_23_col61.clone() + op1_limb_23_col90.clone()) + + carry_tmp_1105.clone()) + - dst_limb_23_col32.clone()) + - (M31_0.clone() * sub_p_bit_col95.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1106.clone() + * ((carry_tmp_1106.clone() * carry_tmp_1106.clone()) - M31_1.clone())), + ); + let carry_tmp_1107 = (((((op0_limb_24_col62.clone() + op1_limb_24_col91.clone()) + + carry_tmp_1106.clone()) + - dst_limb_24_col33.clone()) + - (M31_0.clone() * sub_p_bit_col95.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1107.clone() + * ((carry_tmp_1107.clone() * carry_tmp_1107.clone()) - M31_1.clone())), + ); + let carry_tmp_1108 = (((((op0_limb_25_col63.clone() + op1_limb_25_col92.clone()) + + carry_tmp_1107.clone()) + - dst_limb_25_col34.clone()) + - (M31_0.clone() * sub_p_bit_col95.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1108.clone() + * ((carry_tmp_1108.clone() * carry_tmp_1108.clone()) - M31_1.clone())), + ); + let carry_tmp_1109 = (((((op0_limb_26_col64.clone() + op1_limb_26_col93.clone()) + + carry_tmp_1108.clone()) + - dst_limb_26_col35.clone()) + - (M31_0.clone() * sub_p_bit_col95.clone())) + * M31_4194304.clone()); + eval.add_constraint( + (carry_tmp_1109.clone() + * ((carry_tmp_1109.clone() * carry_tmp_1109.clone()) - M31_1.clone())), + ); + eval.add_constraint( + ((((op0_limb_27_col65.clone() + op1_limb_27_col94.clone()) + carry_tmp_1109.clone()) + - dst_limb_27_col36.clone()) + - (M31_256.clone() * sub_p_bit_col95.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() + M31_2.clone()), + (input_ap_col1.clone() + ap_update_add_1_col7.clone()), + input_fp_col2.clone(), + ], + )]); + + eval.finalize_logup(); + eval + } +} diff --git a/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_f_is_imm_t/mod.rs b/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_f_is_imm_t/mod.rs new file mode 100644 index 00000000..3f7a8d74 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_f_is_imm_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/add_opcode_is_small_f_is_imm_t/prover.rs b/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_f_is_imm_t/prover.rs new file mode 100644 index 00000000..82f254eb --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_f_is_imm_t/prover.rs @@ -0,0 +1,776 @@ +#![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 = 96; + +#[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; 3], + pub memory_id_to_big_inputs: [Vec; 3], + 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), + Vec::with_capacity(capacity), + ], + memory_id_to_big_inputs: [ + Vec::with_capacity(capacity), + 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 = 96; + 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_2 = PackedM31::broadcast(M31::from(2)); + let M31_32768 = PackedM31::broadcast(M31::from(32768)); + let M31_32769 = PackedM31::broadcast(M31::from(32769)); + let UInt16_0 = PackedUInt16::broadcast(UInt16::from(0)); + let UInt16_1 = PackedUInt16::broadcast(UInt16::from(1)); + let UInt16_11 = PackedUInt16::broadcast(UInt16::from(11)); + let UInt16_127 = PackedUInt16::broadcast(UInt16::from(127)); + 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_6 = PackedUInt16::broadcast(UInt16::from(6)); + let UInt16_7 = PackedUInt16::broadcast(UInt16::from(7)); + let UInt16_9 = PackedUInt16::broadcast(UInt16::from(9)); + + inputs + .into_iter() + .enumerate() + .for_each(|(row_index, add_opcode_is_small_f_is_imm_t_input)| { + let input_tmp_1067 = add_opcode_is_small_f_is_imm_t_input; + let input_pc_col0 = input_tmp_1067.pc; + trace[0].data[row_index] = input_pc_col0; + let input_ap_col1 = input_tmp_1067.ap; + trace[1].data[row_index] = input_ap_col1; + let input_fp_col2 = input_tmp_1067.fp; + trace[2].data[row_index] = input_fp_col2; + + // decode_instruction_9aed6a790187299c. + + let memory_address_to_id_value_tmp_1068 = + memory_address_to_id_state.deduce_output(input_pc_col0); + let memory_id_to_big_value_tmp_1069 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1068); + let offset0_tmp_1070 = + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1069.get_m31(0))) + + (((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1069.get_m31(1))) + & (UInt16_127)) + << (UInt16_9))); + let offset0_col3 = offset0_tmp_1070.as_m31(); + trace[3].data[row_index] = offset0_col3; + let offset1_tmp_1071 = + ((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1069.get_m31(1))) + >> (UInt16_7)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1069.get_m31(2))) + << (UInt16_2))) + + (((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1069.get_m31(3))) + & (UInt16_31)) + << (UInt16_11))); + let offset1_col4 = offset1_tmp_1071.as_m31(); + trace[4].data[row_index] = offset1_col4; + let dst_base_fp_tmp_1072 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1069.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1069.get_m31(6))) + << (UInt16_6))) + >> (UInt16_0)) + & (UInt16_1)); + let dst_base_fp_col5 = dst_base_fp_tmp_1072.as_m31(); + trace[5].data[row_index] = dst_base_fp_col5; + let op0_base_fp_tmp_1073 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1069.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1069.get_m31(6))) + << (UInt16_6))) + >> (UInt16_1)) + & (UInt16_1)); + let op0_base_fp_col6 = op0_base_fp_tmp_1073.as_m31(); + trace[6].data[row_index] = op0_base_fp_col6; + let ap_update_add_1_tmp_1074 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1069.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1069.get_m31(6))) + << (UInt16_6))) + >> (UInt16_11)) + & (UInt16_1)); + let ap_update_add_1_col7 = ap_update_add_1_tmp_1074.as_m31(); + trace[7].data[row_index] = ap_update_add_1_col7; + + sub_components_inputs.verify_instruction_inputs[0].extend( + ( + input_pc_col0, + [offset0_col3, offset1_col4, M31_32769], + [ + dst_base_fp_col5, + op0_base_fp_col6, + M31_1, + M31_0, + M31_0, + M31_1, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + ap_update_add_1_col7, + M31_0, + M31_0, + M31_1, + ], + ) + .unpack(), + ); + + lookup_data.verifyinstruction[0].push([ + input_pc_col0, + offset0_col3, + offset1_col4, + M31_32769, + dst_base_fp_col5, + op0_base_fp_col6, + M31_1, + M31_0, + M31_0, + M31_1, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + ap_update_add_1_col7, + M31_0, + M31_0, + M31_1, + ]); + + // read_positive_num_bits_252. + + let memory_address_to_id_value_tmp_1076 = memory_address_to_id_state.deduce_output( + ((((dst_base_fp_col5) * (input_fp_col2)) + + (((M31_1) - (dst_base_fp_col5)) * (input_ap_col1))) + + ((offset0_col3) - (M31_32768))), + ); + let memory_id_to_big_value_tmp_1077 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1076); + let dst_id_col8 = memory_address_to_id_value_tmp_1076; + trace[8].data[row_index] = dst_id_col8; + sub_components_inputs.memory_address_to_id_inputs[0].extend( + ((((dst_base_fp_col5) * (input_fp_col2)) + + (((M31_1) - (dst_base_fp_col5)) * (input_ap_col1))) + + ((offset0_col3) - (M31_32768))) + .unpack(), + ); + + lookup_data.memoryaddresstoid[0].push([ + ((((dst_base_fp_col5) * (input_fp_col2)) + + (((M31_1) - (dst_base_fp_col5)) * (input_ap_col1))) + + ((offset0_col3) - (M31_32768))), + dst_id_col8, + ]); + let dst_limb_0_col9 = memory_id_to_big_value_tmp_1077.get_m31(0); + trace[9].data[row_index] = dst_limb_0_col9; + let dst_limb_1_col10 = memory_id_to_big_value_tmp_1077.get_m31(1); + trace[10].data[row_index] = dst_limb_1_col10; + let dst_limb_2_col11 = memory_id_to_big_value_tmp_1077.get_m31(2); + trace[11].data[row_index] = dst_limb_2_col11; + let dst_limb_3_col12 = memory_id_to_big_value_tmp_1077.get_m31(3); + trace[12].data[row_index] = dst_limb_3_col12; + let dst_limb_4_col13 = memory_id_to_big_value_tmp_1077.get_m31(4); + trace[13].data[row_index] = dst_limb_4_col13; + let dst_limb_5_col14 = memory_id_to_big_value_tmp_1077.get_m31(5); + trace[14].data[row_index] = dst_limb_5_col14; + let dst_limb_6_col15 = memory_id_to_big_value_tmp_1077.get_m31(6); + trace[15].data[row_index] = dst_limb_6_col15; + let dst_limb_7_col16 = memory_id_to_big_value_tmp_1077.get_m31(7); + trace[16].data[row_index] = dst_limb_7_col16; + let dst_limb_8_col17 = memory_id_to_big_value_tmp_1077.get_m31(8); + trace[17].data[row_index] = dst_limb_8_col17; + let dst_limb_9_col18 = memory_id_to_big_value_tmp_1077.get_m31(9); + trace[18].data[row_index] = dst_limb_9_col18; + let dst_limb_10_col19 = memory_id_to_big_value_tmp_1077.get_m31(10); + trace[19].data[row_index] = dst_limb_10_col19; + let dst_limb_11_col20 = memory_id_to_big_value_tmp_1077.get_m31(11); + trace[20].data[row_index] = dst_limb_11_col20; + let dst_limb_12_col21 = memory_id_to_big_value_tmp_1077.get_m31(12); + trace[21].data[row_index] = dst_limb_12_col21; + let dst_limb_13_col22 = memory_id_to_big_value_tmp_1077.get_m31(13); + trace[22].data[row_index] = dst_limb_13_col22; + let dst_limb_14_col23 = memory_id_to_big_value_tmp_1077.get_m31(14); + trace[23].data[row_index] = dst_limb_14_col23; + let dst_limb_15_col24 = memory_id_to_big_value_tmp_1077.get_m31(15); + trace[24].data[row_index] = dst_limb_15_col24; + let dst_limb_16_col25 = memory_id_to_big_value_tmp_1077.get_m31(16); + trace[25].data[row_index] = dst_limb_16_col25; + let dst_limb_17_col26 = memory_id_to_big_value_tmp_1077.get_m31(17); + trace[26].data[row_index] = dst_limb_17_col26; + let dst_limb_18_col27 = memory_id_to_big_value_tmp_1077.get_m31(18); + trace[27].data[row_index] = dst_limb_18_col27; + let dst_limb_19_col28 = memory_id_to_big_value_tmp_1077.get_m31(19); + trace[28].data[row_index] = dst_limb_19_col28; + let dst_limb_20_col29 = memory_id_to_big_value_tmp_1077.get_m31(20); + trace[29].data[row_index] = dst_limb_20_col29; + let dst_limb_21_col30 = memory_id_to_big_value_tmp_1077.get_m31(21); + trace[30].data[row_index] = dst_limb_21_col30; + let dst_limb_22_col31 = memory_id_to_big_value_tmp_1077.get_m31(22); + trace[31].data[row_index] = dst_limb_22_col31; + let dst_limb_23_col32 = memory_id_to_big_value_tmp_1077.get_m31(23); + trace[32].data[row_index] = dst_limb_23_col32; + let dst_limb_24_col33 = memory_id_to_big_value_tmp_1077.get_m31(24); + trace[33].data[row_index] = dst_limb_24_col33; + let dst_limb_25_col34 = memory_id_to_big_value_tmp_1077.get_m31(25); + trace[34].data[row_index] = dst_limb_25_col34; + let dst_limb_26_col35 = memory_id_to_big_value_tmp_1077.get_m31(26); + trace[35].data[row_index] = dst_limb_26_col35; + let dst_limb_27_col36 = memory_id_to_big_value_tmp_1077.get_m31(27); + trace[36].data[row_index] = dst_limb_27_col36; + sub_components_inputs.memory_id_to_big_inputs[0].extend(dst_id_col8.unpack()); + + lookup_data.memoryidtobig[0].push([ + dst_id_col8, + dst_limb_0_col9, + dst_limb_1_col10, + dst_limb_2_col11, + dst_limb_3_col12, + dst_limb_4_col13, + dst_limb_5_col14, + dst_limb_6_col15, + dst_limb_7_col16, + dst_limb_8_col17, + dst_limb_9_col18, + dst_limb_10_col19, + dst_limb_11_col20, + dst_limb_12_col21, + dst_limb_13_col22, + dst_limb_14_col23, + dst_limb_15_col24, + dst_limb_16_col25, + dst_limb_17_col26, + dst_limb_18_col27, + dst_limb_19_col28, + dst_limb_20_col29, + dst_limb_21_col30, + dst_limb_22_col31, + dst_limb_23_col32, + dst_limb_24_col33, + dst_limb_25_col34, + dst_limb_26_col35, + dst_limb_27_col36, + ]); + + // read_positive_num_bits_252. + + let memory_address_to_id_value_tmp_1078 = memory_address_to_id_state.deduce_output( + ((((op0_base_fp_col6) * (input_fp_col2)) + + (((M31_1) - (op0_base_fp_col6)) * (input_ap_col1))) + + ((offset1_col4) - (M31_32768))), + ); + let memory_id_to_big_value_tmp_1079 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1078); + let op0_id_col37 = memory_address_to_id_value_tmp_1078; + trace[37].data[row_index] = op0_id_col37; + sub_components_inputs.memory_address_to_id_inputs[1].extend( + ((((op0_base_fp_col6) * (input_fp_col2)) + + (((M31_1) - (op0_base_fp_col6)) * (input_ap_col1))) + + ((offset1_col4) - (M31_32768))) + .unpack(), + ); + + lookup_data.memoryaddresstoid[1].push([ + ((((op0_base_fp_col6) * (input_fp_col2)) + + (((M31_1) - (op0_base_fp_col6)) * (input_ap_col1))) + + ((offset1_col4) - (M31_32768))), + op0_id_col37, + ]); + let op0_limb_0_col38 = memory_id_to_big_value_tmp_1079.get_m31(0); + trace[38].data[row_index] = op0_limb_0_col38; + let op0_limb_1_col39 = memory_id_to_big_value_tmp_1079.get_m31(1); + trace[39].data[row_index] = op0_limb_1_col39; + let op0_limb_2_col40 = memory_id_to_big_value_tmp_1079.get_m31(2); + trace[40].data[row_index] = op0_limb_2_col40; + let op0_limb_3_col41 = memory_id_to_big_value_tmp_1079.get_m31(3); + trace[41].data[row_index] = op0_limb_3_col41; + let op0_limb_4_col42 = memory_id_to_big_value_tmp_1079.get_m31(4); + trace[42].data[row_index] = op0_limb_4_col42; + let op0_limb_5_col43 = memory_id_to_big_value_tmp_1079.get_m31(5); + trace[43].data[row_index] = op0_limb_5_col43; + let op0_limb_6_col44 = memory_id_to_big_value_tmp_1079.get_m31(6); + trace[44].data[row_index] = op0_limb_6_col44; + let op0_limb_7_col45 = memory_id_to_big_value_tmp_1079.get_m31(7); + trace[45].data[row_index] = op0_limb_7_col45; + let op0_limb_8_col46 = memory_id_to_big_value_tmp_1079.get_m31(8); + trace[46].data[row_index] = op0_limb_8_col46; + let op0_limb_9_col47 = memory_id_to_big_value_tmp_1079.get_m31(9); + trace[47].data[row_index] = op0_limb_9_col47; + let op0_limb_10_col48 = memory_id_to_big_value_tmp_1079.get_m31(10); + trace[48].data[row_index] = op0_limb_10_col48; + let op0_limb_11_col49 = memory_id_to_big_value_tmp_1079.get_m31(11); + trace[49].data[row_index] = op0_limb_11_col49; + let op0_limb_12_col50 = memory_id_to_big_value_tmp_1079.get_m31(12); + trace[50].data[row_index] = op0_limb_12_col50; + let op0_limb_13_col51 = memory_id_to_big_value_tmp_1079.get_m31(13); + trace[51].data[row_index] = op0_limb_13_col51; + let op0_limb_14_col52 = memory_id_to_big_value_tmp_1079.get_m31(14); + trace[52].data[row_index] = op0_limb_14_col52; + let op0_limb_15_col53 = memory_id_to_big_value_tmp_1079.get_m31(15); + trace[53].data[row_index] = op0_limb_15_col53; + let op0_limb_16_col54 = memory_id_to_big_value_tmp_1079.get_m31(16); + trace[54].data[row_index] = op0_limb_16_col54; + let op0_limb_17_col55 = memory_id_to_big_value_tmp_1079.get_m31(17); + trace[55].data[row_index] = op0_limb_17_col55; + let op0_limb_18_col56 = memory_id_to_big_value_tmp_1079.get_m31(18); + trace[56].data[row_index] = op0_limb_18_col56; + let op0_limb_19_col57 = memory_id_to_big_value_tmp_1079.get_m31(19); + trace[57].data[row_index] = op0_limb_19_col57; + let op0_limb_20_col58 = memory_id_to_big_value_tmp_1079.get_m31(20); + trace[58].data[row_index] = op0_limb_20_col58; + let op0_limb_21_col59 = memory_id_to_big_value_tmp_1079.get_m31(21); + trace[59].data[row_index] = op0_limb_21_col59; + let op0_limb_22_col60 = memory_id_to_big_value_tmp_1079.get_m31(22); + trace[60].data[row_index] = op0_limb_22_col60; + let op0_limb_23_col61 = memory_id_to_big_value_tmp_1079.get_m31(23); + trace[61].data[row_index] = op0_limb_23_col61; + let op0_limb_24_col62 = memory_id_to_big_value_tmp_1079.get_m31(24); + trace[62].data[row_index] = op0_limb_24_col62; + let op0_limb_25_col63 = memory_id_to_big_value_tmp_1079.get_m31(25); + trace[63].data[row_index] = op0_limb_25_col63; + let op0_limb_26_col64 = memory_id_to_big_value_tmp_1079.get_m31(26); + trace[64].data[row_index] = op0_limb_26_col64; + let op0_limb_27_col65 = memory_id_to_big_value_tmp_1079.get_m31(27); + trace[65].data[row_index] = op0_limb_27_col65; + sub_components_inputs.memory_id_to_big_inputs[1].extend(op0_id_col37.unpack()); + + lookup_data.memoryidtobig[1].push([ + op0_id_col37, + op0_limb_0_col38, + op0_limb_1_col39, + op0_limb_2_col40, + op0_limb_3_col41, + op0_limb_4_col42, + op0_limb_5_col43, + op0_limb_6_col44, + op0_limb_7_col45, + op0_limb_8_col46, + op0_limb_9_col47, + op0_limb_10_col48, + op0_limb_11_col49, + op0_limb_12_col50, + op0_limb_13_col51, + op0_limb_14_col52, + op0_limb_15_col53, + op0_limb_16_col54, + op0_limb_17_col55, + op0_limb_18_col56, + op0_limb_19_col57, + op0_limb_20_col58, + op0_limb_21_col59, + op0_limb_22_col60, + op0_limb_23_col61, + op0_limb_24_col62, + op0_limb_25_col63, + op0_limb_26_col64, + op0_limb_27_col65, + ]); + + // read_positive_num_bits_252. + + let memory_address_to_id_value_tmp_1080 = + memory_address_to_id_state.deduce_output(((input_pc_col0) + (M31_1))); + let memory_id_to_big_value_tmp_1081 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1080); + let op1_id_col66 = memory_address_to_id_value_tmp_1080; + trace[66].data[row_index] = op1_id_col66; + sub_components_inputs.memory_address_to_id_inputs[2] + .extend(((input_pc_col0) + (M31_1)).unpack()); + + lookup_data.memoryaddresstoid[2].push([((input_pc_col0) + (M31_1)), op1_id_col66]); + let op1_limb_0_col67 = memory_id_to_big_value_tmp_1081.get_m31(0); + trace[67].data[row_index] = op1_limb_0_col67; + let op1_limb_1_col68 = memory_id_to_big_value_tmp_1081.get_m31(1); + trace[68].data[row_index] = op1_limb_1_col68; + let op1_limb_2_col69 = memory_id_to_big_value_tmp_1081.get_m31(2); + trace[69].data[row_index] = op1_limb_2_col69; + let op1_limb_3_col70 = memory_id_to_big_value_tmp_1081.get_m31(3); + trace[70].data[row_index] = op1_limb_3_col70; + let op1_limb_4_col71 = memory_id_to_big_value_tmp_1081.get_m31(4); + trace[71].data[row_index] = op1_limb_4_col71; + let op1_limb_5_col72 = memory_id_to_big_value_tmp_1081.get_m31(5); + trace[72].data[row_index] = op1_limb_5_col72; + let op1_limb_6_col73 = memory_id_to_big_value_tmp_1081.get_m31(6); + trace[73].data[row_index] = op1_limb_6_col73; + let op1_limb_7_col74 = memory_id_to_big_value_tmp_1081.get_m31(7); + trace[74].data[row_index] = op1_limb_7_col74; + let op1_limb_8_col75 = memory_id_to_big_value_tmp_1081.get_m31(8); + trace[75].data[row_index] = op1_limb_8_col75; + let op1_limb_9_col76 = memory_id_to_big_value_tmp_1081.get_m31(9); + trace[76].data[row_index] = op1_limb_9_col76; + let op1_limb_10_col77 = memory_id_to_big_value_tmp_1081.get_m31(10); + trace[77].data[row_index] = op1_limb_10_col77; + let op1_limb_11_col78 = memory_id_to_big_value_tmp_1081.get_m31(11); + trace[78].data[row_index] = op1_limb_11_col78; + let op1_limb_12_col79 = memory_id_to_big_value_tmp_1081.get_m31(12); + trace[79].data[row_index] = op1_limb_12_col79; + let op1_limb_13_col80 = memory_id_to_big_value_tmp_1081.get_m31(13); + trace[80].data[row_index] = op1_limb_13_col80; + let op1_limb_14_col81 = memory_id_to_big_value_tmp_1081.get_m31(14); + trace[81].data[row_index] = op1_limb_14_col81; + let op1_limb_15_col82 = memory_id_to_big_value_tmp_1081.get_m31(15); + trace[82].data[row_index] = op1_limb_15_col82; + let op1_limb_16_col83 = memory_id_to_big_value_tmp_1081.get_m31(16); + trace[83].data[row_index] = op1_limb_16_col83; + let op1_limb_17_col84 = memory_id_to_big_value_tmp_1081.get_m31(17); + trace[84].data[row_index] = op1_limb_17_col84; + let op1_limb_18_col85 = memory_id_to_big_value_tmp_1081.get_m31(18); + trace[85].data[row_index] = op1_limb_18_col85; + let op1_limb_19_col86 = memory_id_to_big_value_tmp_1081.get_m31(19); + trace[86].data[row_index] = op1_limb_19_col86; + let op1_limb_20_col87 = memory_id_to_big_value_tmp_1081.get_m31(20); + trace[87].data[row_index] = op1_limb_20_col87; + let op1_limb_21_col88 = memory_id_to_big_value_tmp_1081.get_m31(21); + trace[88].data[row_index] = op1_limb_21_col88; + let op1_limb_22_col89 = memory_id_to_big_value_tmp_1081.get_m31(22); + trace[89].data[row_index] = op1_limb_22_col89; + let op1_limb_23_col90 = memory_id_to_big_value_tmp_1081.get_m31(23); + trace[90].data[row_index] = op1_limb_23_col90; + let op1_limb_24_col91 = memory_id_to_big_value_tmp_1081.get_m31(24); + trace[91].data[row_index] = op1_limb_24_col91; + let op1_limb_25_col92 = memory_id_to_big_value_tmp_1081.get_m31(25); + trace[92].data[row_index] = op1_limb_25_col92; + let op1_limb_26_col93 = memory_id_to_big_value_tmp_1081.get_m31(26); + trace[93].data[row_index] = op1_limb_26_col93; + let op1_limb_27_col94 = memory_id_to_big_value_tmp_1081.get_m31(27); + trace[94].data[row_index] = op1_limb_27_col94; + sub_components_inputs.memory_id_to_big_inputs[2].extend(op1_id_col66.unpack()); + + lookup_data.memoryidtobig[2].push([ + op1_id_col66, + op1_limb_0_col67, + op1_limb_1_col68, + op1_limb_2_col69, + op1_limb_3_col70, + op1_limb_4_col71, + op1_limb_5_col72, + op1_limb_6_col73, + op1_limb_7_col74, + op1_limb_8_col75, + op1_limb_9_col76, + op1_limb_10_col77, + op1_limb_11_col78, + op1_limb_12_col79, + op1_limb_13_col80, + op1_limb_14_col81, + op1_limb_15_col82, + op1_limb_16_col83, + op1_limb_17_col84, + op1_limb_18_col85, + op1_limb_19_col86, + op1_limb_20_col87, + op1_limb_21_col88, + op1_limb_22_col89, + op1_limb_23_col90, + op1_limb_24_col91, + op1_limb_25_col92, + op1_limb_26_col93, + op1_limb_27_col94, + ]); + + // verify_add252. + + let sub_p_bit_tmp_1082 = ((UInt16_1) + & (((PackedUInt16::from_m31(op0_limb_0_col38)) + ^ (PackedUInt16::from_m31(op1_limb_0_col67))) + ^ (PackedUInt16::from_m31(dst_limb_0_col9)))); + let sub_p_bit_col95 = sub_p_bit_tmp_1082.as_m31(); + trace[95].data[row_index] = sub_p_bit_col95; + + lookup_data.opcodes[0].push([input_pc_col0, input_ap_col1, input_fp_col2]); + lookup_data.opcodes[1].push([ + ((input_pc_col0) + (M31_2)), + ((input_ap_col1) + (ap_update_add_1_col7)), + input_fp_col2, + ]); + }); + + (trace, sub_components_inputs, lookup_data) +} + +pub struct LookupData { + pub memoryaddresstoid: [Vec<[PackedM31; 2]>; 3], + pub memoryidtobig: [Vec<[PackedM31; 29]>; 3], + 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), + Vec::with_capacity(capacity), + ], + memoryidtobig: [ + Vec::with_capacity(capacity), + 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.memoryaddresstoid[2]; + 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[2]; + 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/add_opcode_is_small_t_is_imm_f/component.rs b/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_t_is_imm_f/component.rs new file mode 100644 index 00000000..f9314c05 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_t_is_imm_f/component.rs @@ -0,0 +1,376 @@ +#![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; 29]; + let interaction_log_sizes = vec![log_size; SECURE_EXTENSION_DEGREE * 9]; + 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_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 offset0_col3 = eval.next_trace_mask(); + let offset1_col4 = eval.next_trace_mask(); + let offset2_col5 = eval.next_trace_mask(); + let dst_base_fp_col6 = eval.next_trace_mask(); + let op0_base_fp_col7 = eval.next_trace_mask(); + let op1_base_fp_col8 = eval.next_trace_mask(); + let op1_base_ap_col9 = eval.next_trace_mask(); + let ap_update_add_1_col10 = eval.next_trace_mask(); + let dst_id_col11 = eval.next_trace_mask(); + let msb_col12 = eval.next_trace_mask(); + let mid_limbs_set_col13 = eval.next_trace_mask(); + let dst_limb_0_col14 = eval.next_trace_mask(); + let dst_limb_1_col15 = eval.next_trace_mask(); + let dst_limb_2_col16 = eval.next_trace_mask(); + let op0_id_col17 = eval.next_trace_mask(); + let msb_col18 = eval.next_trace_mask(); + let mid_limbs_set_col19 = eval.next_trace_mask(); + let op0_limb_0_col20 = eval.next_trace_mask(); + let op0_limb_1_col21 = eval.next_trace_mask(); + let op0_limb_2_col22 = eval.next_trace_mask(); + let op1_id_col23 = eval.next_trace_mask(); + let msb_col24 = eval.next_trace_mask(); + let mid_limbs_set_col25 = eval.next_trace_mask(); + let op1_limb_0_col26 = eval.next_trace_mask(); + let op1_limb_1_col27 = eval.next_trace_mask(); + let op1_limb_2_col28 = eval.next_trace_mask(); + + // decode_instruction_52ce7a4a3d9be19a. + + eval.add_to_relation(&[RelationEntry::new( + &self.verifyinstruction_lookup_elements, + E::EF::one(), + &[ + input_pc_col0.clone(), + offset0_col3.clone(), + offset1_col4.clone(), + offset2_col5.clone(), + dst_base_fp_col6.clone(), + op0_base_fp_col7.clone(), + M31_0.clone(), + op1_base_fp_col8.clone(), + op1_base_ap_col9.clone(), + M31_1.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + ap_update_add_1_col10.clone(), + M31_0.clone(), + M31_0.clone(), + M31_1.clone(), + ], + )]); + + // Either flag op1_base_fp is on or flag op1_base_ap is on. + eval.add_constraint( + ((op1_base_fp_col8.clone() + op1_base_ap_col9.clone()) - M31_1.clone()), + ); + + // read_small. + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryaddresstoid_lookup_elements, + E::EF::one(), + &[ + (((dst_base_fp_col6.clone() * input_fp_col2.clone()) + + ((M31_1.clone() - dst_base_fp_col6.clone()) * input_ap_col1.clone())) + + (offset0_col3.clone() - M31_32768.clone())), + dst_id_col11.clone(), + ], + )]); + + // cond_decode_small_sign. + + // msb is a bit. + eval.add_constraint((msb_col12.clone() * (msb_col12.clone() - M31_1.clone()))); + // mid_limbs_set is a bit. + eval.add_constraint( + (mid_limbs_set_col13.clone() * (mid_limbs_set_col13.clone() - M31_1.clone())), + ); + // Cannot have msb equals 0 and mid_limbs_set equals 1. + eval.add_constraint( + ((M31_1.clone() * mid_limbs_set_col13.clone()) * (msb_col12.clone() - M31_1.clone())), + ); + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryidtobig_lookup_elements, + E::EF::one(), + &[ + dst_id_col11.clone(), + dst_limb_0_col14.clone(), + dst_limb_1_col15.clone(), + dst_limb_2_col16.clone(), + (mid_limbs_set_col13.clone() * M31_511.clone()), + (mid_limbs_set_col13.clone() * M31_511.clone()), + (mid_limbs_set_col13.clone() * M31_511.clone()), + (mid_limbs_set_col13.clone() * M31_511.clone()), + (mid_limbs_set_col13.clone() * M31_511.clone()), + (mid_limbs_set_col13.clone() * M31_511.clone()), + (mid_limbs_set_col13.clone() * M31_511.clone()), + (mid_limbs_set_col13.clone() * M31_511.clone()), + (mid_limbs_set_col13.clone() * M31_511.clone()), + (mid_limbs_set_col13.clone() * M31_511.clone()), + (mid_limbs_set_col13.clone() * M31_511.clone()), + (mid_limbs_set_col13.clone() * M31_511.clone()), + (mid_limbs_set_col13.clone() * M31_511.clone()), + (mid_limbs_set_col13.clone() * M31_511.clone()), + (mid_limbs_set_col13.clone() * M31_511.clone()), + (mid_limbs_set_col13.clone() * M31_511.clone()), + (mid_limbs_set_col13.clone() * M31_511.clone()), + (mid_limbs_set_col13.clone() * M31_511.clone()), + ((M31_136.clone() * msb_col12.clone()) - mid_limbs_set_col13.clone()), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + (msb_col12.clone() * M31_256.clone()), + ], + )]); + + // read_small. + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryaddresstoid_lookup_elements, + E::EF::one(), + &[ + (((op0_base_fp_col7.clone() * input_fp_col2.clone()) + + ((M31_1.clone() - op0_base_fp_col7.clone()) * input_ap_col1.clone())) + + (offset1_col4.clone() - M31_32768.clone())), + op0_id_col17.clone(), + ], + )]); + + // cond_decode_small_sign. + + // msb is a bit. + eval.add_constraint((msb_col18.clone() * (msb_col18.clone() - M31_1.clone()))); + // mid_limbs_set is a bit. + eval.add_constraint( + (mid_limbs_set_col19.clone() * (mid_limbs_set_col19.clone() - M31_1.clone())), + ); + // Cannot have msb equals 0 and mid_limbs_set equals 1. + eval.add_constraint( + ((M31_1.clone() * mid_limbs_set_col19.clone()) * (msb_col18.clone() - M31_1.clone())), + ); + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryidtobig_lookup_elements, + E::EF::one(), + &[ + op0_id_col17.clone(), + op0_limb_0_col20.clone(), + op0_limb_1_col21.clone(), + op0_limb_2_col22.clone(), + (mid_limbs_set_col19.clone() * M31_511.clone()), + (mid_limbs_set_col19.clone() * M31_511.clone()), + (mid_limbs_set_col19.clone() * M31_511.clone()), + (mid_limbs_set_col19.clone() * M31_511.clone()), + (mid_limbs_set_col19.clone() * M31_511.clone()), + (mid_limbs_set_col19.clone() * M31_511.clone()), + (mid_limbs_set_col19.clone() * M31_511.clone()), + (mid_limbs_set_col19.clone() * M31_511.clone()), + (mid_limbs_set_col19.clone() * M31_511.clone()), + (mid_limbs_set_col19.clone() * M31_511.clone()), + (mid_limbs_set_col19.clone() * M31_511.clone()), + (mid_limbs_set_col19.clone() * M31_511.clone()), + (mid_limbs_set_col19.clone() * M31_511.clone()), + (mid_limbs_set_col19.clone() * M31_511.clone()), + (mid_limbs_set_col19.clone() * M31_511.clone()), + (mid_limbs_set_col19.clone() * M31_511.clone()), + (mid_limbs_set_col19.clone() * M31_511.clone()), + (mid_limbs_set_col19.clone() * M31_511.clone()), + ((M31_136.clone() * msb_col18.clone()) - mid_limbs_set_col19.clone()), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + (msb_col18.clone() * M31_256.clone()), + ], + )]); + + // read_small. + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryaddresstoid_lookup_elements, + E::EF::one(), + &[ + (((op1_base_fp_col8.clone() * input_fp_col2.clone()) + + (op1_base_ap_col9.clone() * input_ap_col1.clone())) + + (offset2_col5.clone() - M31_32768.clone())), + op1_id_col23.clone(), + ], + )]); + + // cond_decode_small_sign. + + // msb is a bit. + eval.add_constraint((msb_col24.clone() * (msb_col24.clone() - M31_1.clone()))); + // mid_limbs_set is a bit. + eval.add_constraint( + (mid_limbs_set_col25.clone() * (mid_limbs_set_col25.clone() - M31_1.clone())), + ); + // Cannot have msb equals 0 and mid_limbs_set equals 1. + eval.add_constraint( + ((M31_1.clone() * mid_limbs_set_col25.clone()) * (msb_col24.clone() - M31_1.clone())), + ); + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryidtobig_lookup_elements, + E::EF::one(), + &[ + op1_id_col23.clone(), + op1_limb_0_col26.clone(), + op1_limb_1_col27.clone(), + op1_limb_2_col28.clone(), + (mid_limbs_set_col25.clone() * M31_511.clone()), + (mid_limbs_set_col25.clone() * M31_511.clone()), + (mid_limbs_set_col25.clone() * M31_511.clone()), + (mid_limbs_set_col25.clone() * M31_511.clone()), + (mid_limbs_set_col25.clone() * M31_511.clone()), + (mid_limbs_set_col25.clone() * M31_511.clone()), + (mid_limbs_set_col25.clone() * M31_511.clone()), + (mid_limbs_set_col25.clone() * M31_511.clone()), + (mid_limbs_set_col25.clone() * M31_511.clone()), + (mid_limbs_set_col25.clone() * M31_511.clone()), + (mid_limbs_set_col25.clone() * M31_511.clone()), + (mid_limbs_set_col25.clone() * M31_511.clone()), + (mid_limbs_set_col25.clone() * M31_511.clone()), + (mid_limbs_set_col25.clone() * M31_511.clone()), + (mid_limbs_set_col25.clone() * M31_511.clone()), + (mid_limbs_set_col25.clone() * M31_511.clone()), + (mid_limbs_set_col25.clone() * M31_511.clone()), + (mid_limbs_set_col25.clone() * M31_511.clone()), + ((M31_136.clone() * msb_col24.clone()) - mid_limbs_set_col25.clone()), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + (msb_col24.clone() * M31_256.clone()), + ], + )]); + + // dst equals op0 + op1. + eval.add_constraint( + (((((dst_limb_0_col14.clone() + (dst_limb_1_col15.clone() * M31_512.clone())) + + (dst_limb_2_col16.clone() * M31_262144.clone())) + - msb_col12.clone()) + - (M31_134217728.clone() * mid_limbs_set_col13.clone())) + - (((((op0_limb_0_col20.clone() + + (op0_limb_1_col21.clone() * M31_512.clone())) + + (op0_limb_2_col22.clone() * M31_262144.clone())) + - msb_col18.clone()) + - (M31_134217728.clone() * mid_limbs_set_col19.clone())) + + ((((op1_limb_0_col26.clone() + + (op1_limb_1_col27.clone() * M31_512.clone())) + + (op1_limb_2_col28.clone() * M31_262144.clone())) + - msb_col24.clone()) + - (M31_134217728.clone() * mid_limbs_set_col25.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() + M31_1.clone()), + (input_ap_col1.clone() + ap_update_add_1_col10.clone()), + input_fp_col2.clone(), + ], + )]); + + eval.finalize_logup(); + eval + } +} diff --git a/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_t_is_imm_f/mod.rs b/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_t_is_imm_f/mod.rs new file mode 100644 index 00000000..3f7a8d74 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_t_is_imm_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/add_opcode_is_small_t_is_imm_f/prover.rs b/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_t_is_imm_f/prover.rs new file mode 100644 index 00000000..6ddad0d6 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_t_is_imm_f/prover.rs @@ -0,0 +1,688 @@ +#![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 = 29; + +#[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; 3], + pub memory_id_to_big_inputs: [Vec; 3], + 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), + Vec::with_capacity(capacity), + ], + memory_id_to_big_inputs: [ + Vec::with_capacity(capacity), + 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 = 29; + 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_136 = PackedM31::broadcast(M31::from(136)); + let M31_256 = PackedM31::broadcast(M31::from(256)); + let M31_32768 = PackedM31::broadcast(M31::from(32768)); + let M31_511 = PackedM31::broadcast(M31::from(511)); + let UInt16_0 = PackedUInt16::broadcast(UInt16::from(0)); + let UInt16_1 = PackedUInt16::broadcast(UInt16::from(1)); + let UInt16_11 = PackedUInt16::broadcast(UInt16::from(11)); + let UInt16_127 = PackedUInt16::broadcast(UInt16::from(127)); + 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)); + let UInt16_9 = PackedUInt16::broadcast(UInt16::from(9)); + + inputs + .into_iter() + .enumerate() + .for_each(|(row_index, add_opcode_is_small_t_is_imm_f_input)| { + let input_tmp_1043 = add_opcode_is_small_t_is_imm_f_input; + let input_pc_col0 = input_tmp_1043.pc; + trace[0].data[row_index] = input_pc_col0; + let input_ap_col1 = input_tmp_1043.ap; + trace[1].data[row_index] = input_ap_col1; + let input_fp_col2 = input_tmp_1043.fp; + trace[2].data[row_index] = input_fp_col2; + + // decode_instruction_52ce7a4a3d9be19a. + + let memory_address_to_id_value_tmp_1044 = + memory_address_to_id_state.deduce_output(input_pc_col0); + let memory_id_to_big_value_tmp_1045 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1044); + let offset0_tmp_1046 = + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1045.get_m31(0))) + + (((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1045.get_m31(1))) + & (UInt16_127)) + << (UInt16_9))); + let offset0_col3 = offset0_tmp_1046.as_m31(); + trace[3].data[row_index] = offset0_col3; + let offset1_tmp_1047 = + ((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1045.get_m31(1))) + >> (UInt16_7)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1045.get_m31(2))) + << (UInt16_2))) + + (((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1045.get_m31(3))) + & (UInt16_31)) + << (UInt16_11))); + let offset1_col4 = offset1_tmp_1047.as_m31(); + trace[4].data[row_index] = offset1_col4; + let offset2_tmp_1048 = + ((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1045.get_m31(3))) + >> (UInt16_5)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1045.get_m31(4))) + << (UInt16_4))) + + (((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1045.get_m31(5))) + & (UInt16_7)) + << (UInt16_13))); + let offset2_col5 = offset2_tmp_1048.as_m31(); + trace[5].data[row_index] = offset2_col5; + let dst_base_fp_tmp_1049 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1045.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1045.get_m31(6))) + << (UInt16_6))) + >> (UInt16_0)) + & (UInt16_1)); + let dst_base_fp_col6 = dst_base_fp_tmp_1049.as_m31(); + trace[6].data[row_index] = dst_base_fp_col6; + let op0_base_fp_tmp_1050 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1045.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1045.get_m31(6))) + << (UInt16_6))) + >> (UInt16_1)) + & (UInt16_1)); + let op0_base_fp_col7 = op0_base_fp_tmp_1050.as_m31(); + trace[7].data[row_index] = op0_base_fp_col7; + let op1_base_fp_tmp_1051 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1045.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1045.get_m31(6))) + << (UInt16_6))) + >> (UInt16_3)) + & (UInt16_1)); + let op1_base_fp_col8 = op1_base_fp_tmp_1051.as_m31(); + trace[8].data[row_index] = op1_base_fp_col8; + let op1_base_ap_tmp_1052 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1045.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1045.get_m31(6))) + << (UInt16_6))) + >> (UInt16_4)) + & (UInt16_1)); + let op1_base_ap_col9 = op1_base_ap_tmp_1052.as_m31(); + trace[9].data[row_index] = op1_base_ap_col9; + let ap_update_add_1_tmp_1053 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1045.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1045.get_m31(6))) + << (UInt16_6))) + >> (UInt16_11)) + & (UInt16_1)); + let ap_update_add_1_col10 = ap_update_add_1_tmp_1053.as_m31(); + trace[10].data[row_index] = ap_update_add_1_col10; + + sub_components_inputs.verify_instruction_inputs[0].extend( + ( + input_pc_col0, + [offset0_col3, offset1_col4, offset2_col5], + [ + dst_base_fp_col6, + op0_base_fp_col7, + M31_0, + op1_base_fp_col8, + op1_base_ap_col9, + M31_1, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + ap_update_add_1_col10, + M31_0, + M31_0, + M31_1, + ], + ) + .unpack(), + ); + + lookup_data.verifyinstruction[0].push([ + input_pc_col0, + offset0_col3, + offset1_col4, + offset2_col5, + dst_base_fp_col6, + op0_base_fp_col7, + M31_0, + op1_base_fp_col8, + op1_base_ap_col9, + M31_1, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + ap_update_add_1_col10, + M31_0, + M31_0, + M31_1, + ]); + + // read_small. + + let memory_address_to_id_value_tmp_1055 = memory_address_to_id_state.deduce_output( + ((((dst_base_fp_col6) * (input_fp_col2)) + + (((M31_1) - (dst_base_fp_col6)) * (input_ap_col1))) + + ((offset0_col3) - (M31_32768))), + ); + let memory_id_to_big_value_tmp_1056 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1055); + let dst_id_col11 = memory_address_to_id_value_tmp_1055; + trace[11].data[row_index] = dst_id_col11; + sub_components_inputs.memory_address_to_id_inputs[0].extend( + ((((dst_base_fp_col6) * (input_fp_col2)) + + (((M31_1) - (dst_base_fp_col6)) * (input_ap_col1))) + + ((offset0_col3) - (M31_32768))) + .unpack(), + ); + + lookup_data.memoryaddresstoid[0].push([ + ((((dst_base_fp_col6) * (input_fp_col2)) + + (((M31_1) - (dst_base_fp_col6)) * (input_ap_col1))) + + ((offset0_col3) - (M31_32768))), + dst_id_col11, + ]); + + // cond_decode_small_sign. + + let msb_tmp_1057 = memory_id_to_big_value_tmp_1056.get_m31(27).eq(M31_256); + let msb_col12 = msb_tmp_1057.as_m31(); + trace[12].data[row_index] = msb_col12; + let mid_limbs_set_tmp_1058 = memory_id_to_big_value_tmp_1056.get_m31(20).eq(M31_511); + let mid_limbs_set_col13 = mid_limbs_set_tmp_1058.as_m31(); + trace[13].data[row_index] = mid_limbs_set_col13; + + let dst_limb_0_col14 = memory_id_to_big_value_tmp_1056.get_m31(0); + trace[14].data[row_index] = dst_limb_0_col14; + let dst_limb_1_col15 = memory_id_to_big_value_tmp_1056.get_m31(1); + trace[15].data[row_index] = dst_limb_1_col15; + let dst_limb_2_col16 = memory_id_to_big_value_tmp_1056.get_m31(2); + trace[16].data[row_index] = dst_limb_2_col16; + sub_components_inputs.memory_id_to_big_inputs[0].extend(dst_id_col11.unpack()); + + lookup_data.memoryidtobig[0].push([ + dst_id_col11, + dst_limb_0_col14, + dst_limb_1_col15, + dst_limb_2_col16, + ((mid_limbs_set_col13) * (M31_511)), + ((mid_limbs_set_col13) * (M31_511)), + ((mid_limbs_set_col13) * (M31_511)), + ((mid_limbs_set_col13) * (M31_511)), + ((mid_limbs_set_col13) * (M31_511)), + ((mid_limbs_set_col13) * (M31_511)), + ((mid_limbs_set_col13) * (M31_511)), + ((mid_limbs_set_col13) * (M31_511)), + ((mid_limbs_set_col13) * (M31_511)), + ((mid_limbs_set_col13) * (M31_511)), + ((mid_limbs_set_col13) * (M31_511)), + ((mid_limbs_set_col13) * (M31_511)), + ((mid_limbs_set_col13) * (M31_511)), + ((mid_limbs_set_col13) * (M31_511)), + ((mid_limbs_set_col13) * (M31_511)), + ((mid_limbs_set_col13) * (M31_511)), + ((mid_limbs_set_col13) * (M31_511)), + ((mid_limbs_set_col13) * (M31_511)), + (((M31_136) * (msb_col12)) - (mid_limbs_set_col13)), + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + ((msb_col12) * (M31_256)), + ]); + + // read_small. + + let memory_address_to_id_value_tmp_1059 = memory_address_to_id_state.deduce_output( + ((((op0_base_fp_col7) * (input_fp_col2)) + + (((M31_1) - (op0_base_fp_col7)) * (input_ap_col1))) + + ((offset1_col4) - (M31_32768))), + ); + let memory_id_to_big_value_tmp_1060 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1059); + let op0_id_col17 = memory_address_to_id_value_tmp_1059; + trace[17].data[row_index] = op0_id_col17; + sub_components_inputs.memory_address_to_id_inputs[1].extend( + ((((op0_base_fp_col7) * (input_fp_col2)) + + (((M31_1) - (op0_base_fp_col7)) * (input_ap_col1))) + + ((offset1_col4) - (M31_32768))) + .unpack(), + ); + + lookup_data.memoryaddresstoid[1].push([ + ((((op0_base_fp_col7) * (input_fp_col2)) + + (((M31_1) - (op0_base_fp_col7)) * (input_ap_col1))) + + ((offset1_col4) - (M31_32768))), + op0_id_col17, + ]); + + // cond_decode_small_sign. + + let msb_tmp_1061 = memory_id_to_big_value_tmp_1060.get_m31(27).eq(M31_256); + let msb_col18 = msb_tmp_1061.as_m31(); + trace[18].data[row_index] = msb_col18; + let mid_limbs_set_tmp_1062 = memory_id_to_big_value_tmp_1060.get_m31(20).eq(M31_511); + let mid_limbs_set_col19 = mid_limbs_set_tmp_1062.as_m31(); + trace[19].data[row_index] = mid_limbs_set_col19; + + let op0_limb_0_col20 = memory_id_to_big_value_tmp_1060.get_m31(0); + trace[20].data[row_index] = op0_limb_0_col20; + let op0_limb_1_col21 = memory_id_to_big_value_tmp_1060.get_m31(1); + trace[21].data[row_index] = op0_limb_1_col21; + let op0_limb_2_col22 = memory_id_to_big_value_tmp_1060.get_m31(2); + trace[22].data[row_index] = op0_limb_2_col22; + sub_components_inputs.memory_id_to_big_inputs[1].extend(op0_id_col17.unpack()); + + lookup_data.memoryidtobig[1].push([ + op0_id_col17, + op0_limb_0_col20, + op0_limb_1_col21, + op0_limb_2_col22, + ((mid_limbs_set_col19) * (M31_511)), + ((mid_limbs_set_col19) * (M31_511)), + ((mid_limbs_set_col19) * (M31_511)), + ((mid_limbs_set_col19) * (M31_511)), + ((mid_limbs_set_col19) * (M31_511)), + ((mid_limbs_set_col19) * (M31_511)), + ((mid_limbs_set_col19) * (M31_511)), + ((mid_limbs_set_col19) * (M31_511)), + ((mid_limbs_set_col19) * (M31_511)), + ((mid_limbs_set_col19) * (M31_511)), + ((mid_limbs_set_col19) * (M31_511)), + ((mid_limbs_set_col19) * (M31_511)), + ((mid_limbs_set_col19) * (M31_511)), + ((mid_limbs_set_col19) * (M31_511)), + ((mid_limbs_set_col19) * (M31_511)), + ((mid_limbs_set_col19) * (M31_511)), + ((mid_limbs_set_col19) * (M31_511)), + ((mid_limbs_set_col19) * (M31_511)), + (((M31_136) * (msb_col18)) - (mid_limbs_set_col19)), + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + ((msb_col18) * (M31_256)), + ]); + + // read_small. + + let memory_address_to_id_value_tmp_1063 = memory_address_to_id_state.deduce_output( + ((((op1_base_fp_col8) * (input_fp_col2)) + ((op1_base_ap_col9) * (input_ap_col1))) + + ((offset2_col5) - (M31_32768))), + ); + let memory_id_to_big_value_tmp_1064 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1063); + let op1_id_col23 = memory_address_to_id_value_tmp_1063; + trace[23].data[row_index] = op1_id_col23; + sub_components_inputs.memory_address_to_id_inputs[2].extend( + ((((op1_base_fp_col8) * (input_fp_col2)) + ((op1_base_ap_col9) * (input_ap_col1))) + + ((offset2_col5) - (M31_32768))) + .unpack(), + ); + + lookup_data.memoryaddresstoid[2].push([ + ((((op1_base_fp_col8) * (input_fp_col2)) + ((op1_base_ap_col9) * (input_ap_col1))) + + ((offset2_col5) - (M31_32768))), + op1_id_col23, + ]); + + // cond_decode_small_sign. + + let msb_tmp_1065 = memory_id_to_big_value_tmp_1064.get_m31(27).eq(M31_256); + let msb_col24 = msb_tmp_1065.as_m31(); + trace[24].data[row_index] = msb_col24; + let mid_limbs_set_tmp_1066 = memory_id_to_big_value_tmp_1064.get_m31(20).eq(M31_511); + let mid_limbs_set_col25 = mid_limbs_set_tmp_1066.as_m31(); + trace[25].data[row_index] = mid_limbs_set_col25; + + let op1_limb_0_col26 = memory_id_to_big_value_tmp_1064.get_m31(0); + trace[26].data[row_index] = op1_limb_0_col26; + let op1_limb_1_col27 = memory_id_to_big_value_tmp_1064.get_m31(1); + trace[27].data[row_index] = op1_limb_1_col27; + let op1_limb_2_col28 = memory_id_to_big_value_tmp_1064.get_m31(2); + trace[28].data[row_index] = op1_limb_2_col28; + sub_components_inputs.memory_id_to_big_inputs[2].extend(op1_id_col23.unpack()); + + lookup_data.memoryidtobig[2].push([ + op1_id_col23, + op1_limb_0_col26, + op1_limb_1_col27, + op1_limb_2_col28, + ((mid_limbs_set_col25) * (M31_511)), + ((mid_limbs_set_col25) * (M31_511)), + ((mid_limbs_set_col25) * (M31_511)), + ((mid_limbs_set_col25) * (M31_511)), + ((mid_limbs_set_col25) * (M31_511)), + ((mid_limbs_set_col25) * (M31_511)), + ((mid_limbs_set_col25) * (M31_511)), + ((mid_limbs_set_col25) * (M31_511)), + ((mid_limbs_set_col25) * (M31_511)), + ((mid_limbs_set_col25) * (M31_511)), + ((mid_limbs_set_col25) * (M31_511)), + ((mid_limbs_set_col25) * (M31_511)), + ((mid_limbs_set_col25) * (M31_511)), + ((mid_limbs_set_col25) * (M31_511)), + ((mid_limbs_set_col25) * (M31_511)), + ((mid_limbs_set_col25) * (M31_511)), + ((mid_limbs_set_col25) * (M31_511)), + ((mid_limbs_set_col25) * (M31_511)), + (((M31_136) * (msb_col24)) - (mid_limbs_set_col25)), + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + ((msb_col24) * (M31_256)), + ]); + + lookup_data.opcodes[0].push([input_pc_col0, input_ap_col1, input_fp_col2]); + lookup_data.opcodes[1].push([ + ((input_pc_col0) + (M31_1)), + ((input_ap_col1) + (ap_update_add_1_col10)), + input_fp_col2, + ]); + }); + + (trace, sub_components_inputs, lookup_data) +} + +pub struct LookupData { + pub memoryaddresstoid: [Vec<[PackedM31; 2]>; 3], + pub memoryidtobig: [Vec<[PackedM31; 29]>; 3], + 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), + Vec::with_capacity(capacity), + ], + memoryidtobig: [ + Vec::with_capacity(capacity), + 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.memoryaddresstoid[2]; + 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[2]; + 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/add_opcode_is_small_t_is_imm_t/component.rs b/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_t_is_imm_t/component.rs new file mode 100644 index 00000000..8bd25371 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_t_is_imm_t/component.rs @@ -0,0 +1,368 @@ +#![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; 26]; + let interaction_log_sizes = vec![log_size; SECURE_EXTENSION_DEGREE * 9]; + 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_2 = E::F::from(M31::from(2)); + let M31_256 = E::F::from(M31::from(256)); + let M31_262144 = E::F::from(M31::from(262144)); + let M31_32768 = E::F::from(M31::from(32768)); + 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 offset0_col3 = eval.next_trace_mask(); + let offset1_col4 = eval.next_trace_mask(); + let dst_base_fp_col5 = eval.next_trace_mask(); + let op0_base_fp_col6 = eval.next_trace_mask(); + let ap_update_add_1_col7 = eval.next_trace_mask(); + let dst_id_col8 = eval.next_trace_mask(); + let msb_col9 = eval.next_trace_mask(); + let mid_limbs_set_col10 = eval.next_trace_mask(); + let dst_limb_0_col11 = eval.next_trace_mask(); + let dst_limb_1_col12 = eval.next_trace_mask(); + let dst_limb_2_col13 = eval.next_trace_mask(); + let op0_id_col14 = eval.next_trace_mask(); + let msb_col15 = eval.next_trace_mask(); + let mid_limbs_set_col16 = eval.next_trace_mask(); + let op0_limb_0_col17 = eval.next_trace_mask(); + let op0_limb_1_col18 = eval.next_trace_mask(); + let op0_limb_2_col19 = eval.next_trace_mask(); + let op1_id_col20 = eval.next_trace_mask(); + let msb_col21 = eval.next_trace_mask(); + let mid_limbs_set_col22 = eval.next_trace_mask(); + let op1_limb_0_col23 = eval.next_trace_mask(); + let op1_limb_1_col24 = eval.next_trace_mask(); + let op1_limb_2_col25 = eval.next_trace_mask(); + + // decode_instruction_9aed6a790187299c. + + eval.add_to_relation(&[RelationEntry::new( + &self.verifyinstruction_lookup_elements, + E::EF::one(), + &[ + input_pc_col0.clone(), + offset0_col3.clone(), + offset1_col4.clone(), + M31_32769.clone(), + dst_base_fp_col5.clone(), + op0_base_fp_col6.clone(), + M31_1.clone(), + M31_0.clone(), + M31_0.clone(), + M31_1.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + ap_update_add_1_col7.clone(), + M31_0.clone(), + M31_0.clone(), + M31_1.clone(), + ], + )]); + + // read_small. + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryaddresstoid_lookup_elements, + E::EF::one(), + &[ + (((dst_base_fp_col5.clone() * input_fp_col2.clone()) + + ((M31_1.clone() - dst_base_fp_col5.clone()) * input_ap_col1.clone())) + + (offset0_col3.clone() - M31_32768.clone())), + dst_id_col8.clone(), + ], + )]); + + // cond_decode_small_sign. + + // msb is a bit. + eval.add_constraint((msb_col9.clone() * (msb_col9.clone() - M31_1.clone()))); + // mid_limbs_set is a bit. + eval.add_constraint( + (mid_limbs_set_col10.clone() * (mid_limbs_set_col10.clone() - M31_1.clone())), + ); + // Cannot have msb equals 0 and mid_limbs_set equals 1. + eval.add_constraint( + ((M31_1.clone() * mid_limbs_set_col10.clone()) * (msb_col9.clone() - M31_1.clone())), + ); + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryidtobig_lookup_elements, + E::EF::one(), + &[ + dst_id_col8.clone(), + dst_limb_0_col11.clone(), + dst_limb_1_col12.clone(), + dst_limb_2_col13.clone(), + (mid_limbs_set_col10.clone() * M31_511.clone()), + (mid_limbs_set_col10.clone() * M31_511.clone()), + (mid_limbs_set_col10.clone() * M31_511.clone()), + (mid_limbs_set_col10.clone() * M31_511.clone()), + (mid_limbs_set_col10.clone() * M31_511.clone()), + (mid_limbs_set_col10.clone() * M31_511.clone()), + (mid_limbs_set_col10.clone() * M31_511.clone()), + (mid_limbs_set_col10.clone() * M31_511.clone()), + (mid_limbs_set_col10.clone() * M31_511.clone()), + (mid_limbs_set_col10.clone() * M31_511.clone()), + (mid_limbs_set_col10.clone() * M31_511.clone()), + (mid_limbs_set_col10.clone() * M31_511.clone()), + (mid_limbs_set_col10.clone() * M31_511.clone()), + (mid_limbs_set_col10.clone() * M31_511.clone()), + (mid_limbs_set_col10.clone() * M31_511.clone()), + (mid_limbs_set_col10.clone() * M31_511.clone()), + (mid_limbs_set_col10.clone() * M31_511.clone()), + (mid_limbs_set_col10.clone() * M31_511.clone()), + ((M31_136.clone() * msb_col9.clone()) - mid_limbs_set_col10.clone()), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + (msb_col9.clone() * M31_256.clone()), + ], + )]); + + // read_small. + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryaddresstoid_lookup_elements, + E::EF::one(), + &[ + (((op0_base_fp_col6.clone() * input_fp_col2.clone()) + + ((M31_1.clone() - op0_base_fp_col6.clone()) * input_ap_col1.clone())) + + (offset1_col4.clone() - M31_32768.clone())), + op0_id_col14.clone(), + ], + )]); + + // cond_decode_small_sign. + + // msb is a bit. + eval.add_constraint((msb_col15.clone() * (msb_col15.clone() - M31_1.clone()))); + // mid_limbs_set is a bit. + eval.add_constraint( + (mid_limbs_set_col16.clone() * (mid_limbs_set_col16.clone() - M31_1.clone())), + ); + // Cannot have msb equals 0 and mid_limbs_set equals 1. + eval.add_constraint( + ((M31_1.clone() * mid_limbs_set_col16.clone()) * (msb_col15.clone() - M31_1.clone())), + ); + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryidtobig_lookup_elements, + E::EF::one(), + &[ + op0_id_col14.clone(), + op0_limb_0_col17.clone(), + op0_limb_1_col18.clone(), + op0_limb_2_col19.clone(), + (mid_limbs_set_col16.clone() * M31_511.clone()), + (mid_limbs_set_col16.clone() * M31_511.clone()), + (mid_limbs_set_col16.clone() * M31_511.clone()), + (mid_limbs_set_col16.clone() * M31_511.clone()), + (mid_limbs_set_col16.clone() * M31_511.clone()), + (mid_limbs_set_col16.clone() * M31_511.clone()), + (mid_limbs_set_col16.clone() * M31_511.clone()), + (mid_limbs_set_col16.clone() * M31_511.clone()), + (mid_limbs_set_col16.clone() * M31_511.clone()), + (mid_limbs_set_col16.clone() * M31_511.clone()), + (mid_limbs_set_col16.clone() * M31_511.clone()), + (mid_limbs_set_col16.clone() * M31_511.clone()), + (mid_limbs_set_col16.clone() * M31_511.clone()), + (mid_limbs_set_col16.clone() * M31_511.clone()), + (mid_limbs_set_col16.clone() * M31_511.clone()), + (mid_limbs_set_col16.clone() * M31_511.clone()), + (mid_limbs_set_col16.clone() * M31_511.clone()), + (mid_limbs_set_col16.clone() * M31_511.clone()), + ((M31_136.clone() * msb_col15.clone()) - mid_limbs_set_col16.clone()), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + (msb_col15.clone() * M31_256.clone()), + ], + )]); + + // read_small. + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryaddresstoid_lookup_elements, + E::EF::one(), + &[ + (input_pc_col0.clone() + M31_1.clone()), + op1_id_col20.clone(), + ], + )]); + + // cond_decode_small_sign. + + // msb is a bit. + eval.add_constraint((msb_col21.clone() * (msb_col21.clone() - M31_1.clone()))); + // mid_limbs_set is a bit. + eval.add_constraint( + (mid_limbs_set_col22.clone() * (mid_limbs_set_col22.clone() - M31_1.clone())), + ); + // Cannot have msb equals 0 and mid_limbs_set equals 1. + eval.add_constraint( + ((M31_1.clone() * mid_limbs_set_col22.clone()) * (msb_col21.clone() - M31_1.clone())), + ); + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryidtobig_lookup_elements, + E::EF::one(), + &[ + op1_id_col20.clone(), + op1_limb_0_col23.clone(), + op1_limb_1_col24.clone(), + op1_limb_2_col25.clone(), + (mid_limbs_set_col22.clone() * M31_511.clone()), + (mid_limbs_set_col22.clone() * M31_511.clone()), + (mid_limbs_set_col22.clone() * M31_511.clone()), + (mid_limbs_set_col22.clone() * M31_511.clone()), + (mid_limbs_set_col22.clone() * M31_511.clone()), + (mid_limbs_set_col22.clone() * M31_511.clone()), + (mid_limbs_set_col22.clone() * M31_511.clone()), + (mid_limbs_set_col22.clone() * M31_511.clone()), + (mid_limbs_set_col22.clone() * M31_511.clone()), + (mid_limbs_set_col22.clone() * M31_511.clone()), + (mid_limbs_set_col22.clone() * M31_511.clone()), + (mid_limbs_set_col22.clone() * M31_511.clone()), + (mid_limbs_set_col22.clone() * M31_511.clone()), + (mid_limbs_set_col22.clone() * M31_511.clone()), + (mid_limbs_set_col22.clone() * M31_511.clone()), + (mid_limbs_set_col22.clone() * M31_511.clone()), + (mid_limbs_set_col22.clone() * M31_511.clone()), + (mid_limbs_set_col22.clone() * M31_511.clone()), + ((M31_136.clone() * msb_col21.clone()) - mid_limbs_set_col22.clone()), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + (msb_col21.clone() * M31_256.clone()), + ], + )]); + + // dst equals op0 + op1. + eval.add_constraint( + (((((dst_limb_0_col11.clone() + (dst_limb_1_col12.clone() * M31_512.clone())) + + (dst_limb_2_col13.clone() * M31_262144.clone())) + - msb_col9.clone()) + - (M31_134217728.clone() * mid_limbs_set_col10.clone())) + - (((((op0_limb_0_col17.clone() + + (op0_limb_1_col18.clone() * M31_512.clone())) + + (op0_limb_2_col19.clone() * M31_262144.clone())) + - msb_col15.clone()) + - (M31_134217728.clone() * mid_limbs_set_col16.clone())) + + ((((op1_limb_0_col23.clone() + + (op1_limb_1_col24.clone() * M31_512.clone())) + + (op1_limb_2_col25.clone() * M31_262144.clone())) + - msb_col21.clone()) + - (M31_134217728.clone() * mid_limbs_set_col22.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() + M31_2.clone()), + (input_ap_col1.clone() + ap_update_add_1_col7.clone()), + input_fp_col2.clone(), + ], + )]); + + eval.finalize_logup(); + eval + } +} diff --git a/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_t_is_imm_t/mod.rs b/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_t_is_imm_t/mod.rs new file mode 100644 index 00000000..3f7a8d74 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_t_is_imm_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/add_opcode_is_small_t_is_imm_t/prover.rs b/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_t_is_imm_t/prover.rs new file mode 100644 index 00000000..f7139de7 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/add_opcode_is_small_t_is_imm_t/prover.rs @@ -0,0 +1,650 @@ +#![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 = 26; + +#[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; 3], + pub memory_id_to_big_inputs: [Vec; 3], + 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), + Vec::with_capacity(capacity), + ], + memory_id_to_big_inputs: [ + Vec::with_capacity(capacity), + 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 = 26; + 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_136 = PackedM31::broadcast(M31::from(136)); + let M31_2 = PackedM31::broadcast(M31::from(2)); + let M31_256 = PackedM31::broadcast(M31::from(256)); + let M31_32768 = PackedM31::broadcast(M31::from(32768)); + let M31_32769 = PackedM31::broadcast(M31::from(32769)); + let M31_511 = PackedM31::broadcast(M31::from(511)); + let UInt16_0 = PackedUInt16::broadcast(UInt16::from(0)); + let UInt16_1 = PackedUInt16::broadcast(UInt16::from(1)); + let UInt16_11 = PackedUInt16::broadcast(UInt16::from(11)); + let UInt16_127 = PackedUInt16::broadcast(UInt16::from(127)); + 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_6 = PackedUInt16::broadcast(UInt16::from(6)); + let UInt16_7 = PackedUInt16::broadcast(UInt16::from(7)); + let UInt16_9 = PackedUInt16::broadcast(UInt16::from(9)); + + inputs + .into_iter() + .enumerate() + .for_each(|(row_index, add_opcode_is_small_t_is_imm_t_input)| { + let input_tmp_957 = add_opcode_is_small_t_is_imm_t_input; + let input_pc_col0 = input_tmp_957.pc; + trace[0].data[row_index] = input_pc_col0; + let input_ap_col1 = input_tmp_957.ap; + trace[1].data[row_index] = input_ap_col1; + let input_fp_col2 = input_tmp_957.fp; + trace[2].data[row_index] = input_fp_col2; + + // decode_instruction_9aed6a790187299c. + + let memory_address_to_id_value_tmp_966 = + memory_address_to_id_state.deduce_output(input_pc_col0); + let memory_id_to_big_value_tmp_967 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_966); + let offset0_tmp_968 = + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_967.get_m31(0))) + + (((PackedUInt16::from_m31(memory_id_to_big_value_tmp_967.get_m31(1))) + & (UInt16_127)) + << (UInt16_9))); + let offset0_col3 = offset0_tmp_968.as_m31(); + trace[3].data[row_index] = offset0_col3; + let offset1_tmp_969 = + ((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_967.get_m31(1))) + >> (UInt16_7)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_967.get_m31(2))) + << (UInt16_2))) + + (((PackedUInt16::from_m31(memory_id_to_big_value_tmp_967.get_m31(3))) + & (UInt16_31)) + << (UInt16_11))); + let offset1_col4 = offset1_tmp_969.as_m31(); + trace[4].data[row_index] = offset1_col4; + let dst_base_fp_tmp_970 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_967.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_967.get_m31(6))) + << (UInt16_6))) + >> (UInt16_0)) + & (UInt16_1)); + let dst_base_fp_col5 = dst_base_fp_tmp_970.as_m31(); + trace[5].data[row_index] = dst_base_fp_col5; + let op0_base_fp_tmp_971 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_967.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_967.get_m31(6))) + << (UInt16_6))) + >> (UInt16_1)) + & (UInt16_1)); + let op0_base_fp_col6 = op0_base_fp_tmp_971.as_m31(); + trace[6].data[row_index] = op0_base_fp_col6; + let ap_update_add_1_tmp_972 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_967.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_967.get_m31(6))) + << (UInt16_6))) + >> (UInt16_11)) + & (UInt16_1)); + let ap_update_add_1_col7 = ap_update_add_1_tmp_972.as_m31(); + trace[7].data[row_index] = ap_update_add_1_col7; + + sub_components_inputs.verify_instruction_inputs[0].extend( + ( + input_pc_col0, + [offset0_col3, offset1_col4, M31_32769], + [ + dst_base_fp_col5, + op0_base_fp_col6, + M31_1, + M31_0, + M31_0, + M31_1, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + ap_update_add_1_col7, + M31_0, + M31_0, + M31_1, + ], + ) + .unpack(), + ); + + lookup_data.verifyinstruction[0].push([ + input_pc_col0, + offset0_col3, + offset1_col4, + M31_32769, + dst_base_fp_col5, + op0_base_fp_col6, + M31_1, + M31_0, + M31_0, + M31_1, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + ap_update_add_1_col7, + M31_0, + M31_0, + M31_1, + ]); + + // read_small. + + let memory_address_to_id_value_tmp_974 = memory_address_to_id_state.deduce_output( + ((((dst_base_fp_col5) * (input_fp_col2)) + + (((M31_1) - (dst_base_fp_col5)) * (input_ap_col1))) + + ((offset0_col3) - (M31_32768))), + ); + let memory_id_to_big_value_tmp_975 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_974); + let dst_id_col8 = memory_address_to_id_value_tmp_974; + trace[8].data[row_index] = dst_id_col8; + sub_components_inputs.memory_address_to_id_inputs[0].extend( + ((((dst_base_fp_col5) * (input_fp_col2)) + + (((M31_1) - (dst_base_fp_col5)) * (input_ap_col1))) + + ((offset0_col3) - (M31_32768))) + .unpack(), + ); + + lookup_data.memoryaddresstoid[0].push([ + ((((dst_base_fp_col5) * (input_fp_col2)) + + (((M31_1) - (dst_base_fp_col5)) * (input_ap_col1))) + + ((offset0_col3) - (M31_32768))), + dst_id_col8, + ]); + + // cond_decode_small_sign. + + let msb_tmp_976 = memory_id_to_big_value_tmp_975.get_m31(27).eq(M31_256); + let msb_col9 = msb_tmp_976.as_m31(); + trace[9].data[row_index] = msb_col9; + let mid_limbs_set_tmp_977 = memory_id_to_big_value_tmp_975.get_m31(20).eq(M31_511); + let mid_limbs_set_col10 = mid_limbs_set_tmp_977.as_m31(); + trace[10].data[row_index] = mid_limbs_set_col10; + + let dst_limb_0_col11 = memory_id_to_big_value_tmp_975.get_m31(0); + trace[11].data[row_index] = dst_limb_0_col11; + let dst_limb_1_col12 = memory_id_to_big_value_tmp_975.get_m31(1); + trace[12].data[row_index] = dst_limb_1_col12; + let dst_limb_2_col13 = memory_id_to_big_value_tmp_975.get_m31(2); + trace[13].data[row_index] = dst_limb_2_col13; + sub_components_inputs.memory_id_to_big_inputs[0].extend(dst_id_col8.unpack()); + + lookup_data.memoryidtobig[0].push([ + dst_id_col8, + dst_limb_0_col11, + dst_limb_1_col12, + dst_limb_2_col13, + ((mid_limbs_set_col10) * (M31_511)), + ((mid_limbs_set_col10) * (M31_511)), + ((mid_limbs_set_col10) * (M31_511)), + ((mid_limbs_set_col10) * (M31_511)), + ((mid_limbs_set_col10) * (M31_511)), + ((mid_limbs_set_col10) * (M31_511)), + ((mid_limbs_set_col10) * (M31_511)), + ((mid_limbs_set_col10) * (M31_511)), + ((mid_limbs_set_col10) * (M31_511)), + ((mid_limbs_set_col10) * (M31_511)), + ((mid_limbs_set_col10) * (M31_511)), + ((mid_limbs_set_col10) * (M31_511)), + ((mid_limbs_set_col10) * (M31_511)), + ((mid_limbs_set_col10) * (M31_511)), + ((mid_limbs_set_col10) * (M31_511)), + ((mid_limbs_set_col10) * (M31_511)), + ((mid_limbs_set_col10) * (M31_511)), + ((mid_limbs_set_col10) * (M31_511)), + (((M31_136) * (msb_col9)) - (mid_limbs_set_col10)), + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + ((msb_col9) * (M31_256)), + ]); + + // read_small. + + let memory_address_to_id_value_tmp_978 = memory_address_to_id_state.deduce_output( + ((((op0_base_fp_col6) * (input_fp_col2)) + + (((M31_1) - (op0_base_fp_col6)) * (input_ap_col1))) + + ((offset1_col4) - (M31_32768))), + ); + let memory_id_to_big_value_tmp_979 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_978); + let op0_id_col14 = memory_address_to_id_value_tmp_978; + trace[14].data[row_index] = op0_id_col14; + sub_components_inputs.memory_address_to_id_inputs[1].extend( + ((((op0_base_fp_col6) * (input_fp_col2)) + + (((M31_1) - (op0_base_fp_col6)) * (input_ap_col1))) + + ((offset1_col4) - (M31_32768))) + .unpack(), + ); + + lookup_data.memoryaddresstoid[1].push([ + ((((op0_base_fp_col6) * (input_fp_col2)) + + (((M31_1) - (op0_base_fp_col6)) * (input_ap_col1))) + + ((offset1_col4) - (M31_32768))), + op0_id_col14, + ]); + + // cond_decode_small_sign. + + let msb_tmp_980 = memory_id_to_big_value_tmp_979.get_m31(27).eq(M31_256); + let msb_col15 = msb_tmp_980.as_m31(); + trace[15].data[row_index] = msb_col15; + let mid_limbs_set_tmp_981 = memory_id_to_big_value_tmp_979.get_m31(20).eq(M31_511); + let mid_limbs_set_col16 = mid_limbs_set_tmp_981.as_m31(); + trace[16].data[row_index] = mid_limbs_set_col16; + + let op0_limb_0_col17 = memory_id_to_big_value_tmp_979.get_m31(0); + trace[17].data[row_index] = op0_limb_0_col17; + let op0_limb_1_col18 = memory_id_to_big_value_tmp_979.get_m31(1); + trace[18].data[row_index] = op0_limb_1_col18; + let op0_limb_2_col19 = memory_id_to_big_value_tmp_979.get_m31(2); + trace[19].data[row_index] = op0_limb_2_col19; + sub_components_inputs.memory_id_to_big_inputs[1].extend(op0_id_col14.unpack()); + + lookup_data.memoryidtobig[1].push([ + op0_id_col14, + op0_limb_0_col17, + op0_limb_1_col18, + op0_limb_2_col19, + ((mid_limbs_set_col16) * (M31_511)), + ((mid_limbs_set_col16) * (M31_511)), + ((mid_limbs_set_col16) * (M31_511)), + ((mid_limbs_set_col16) * (M31_511)), + ((mid_limbs_set_col16) * (M31_511)), + ((mid_limbs_set_col16) * (M31_511)), + ((mid_limbs_set_col16) * (M31_511)), + ((mid_limbs_set_col16) * (M31_511)), + ((mid_limbs_set_col16) * (M31_511)), + ((mid_limbs_set_col16) * (M31_511)), + ((mid_limbs_set_col16) * (M31_511)), + ((mid_limbs_set_col16) * (M31_511)), + ((mid_limbs_set_col16) * (M31_511)), + ((mid_limbs_set_col16) * (M31_511)), + ((mid_limbs_set_col16) * (M31_511)), + ((mid_limbs_set_col16) * (M31_511)), + ((mid_limbs_set_col16) * (M31_511)), + ((mid_limbs_set_col16) * (M31_511)), + (((M31_136) * (msb_col15)) - (mid_limbs_set_col16)), + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + ((msb_col15) * (M31_256)), + ]); + + // read_small. + + let memory_address_to_id_value_tmp_982 = + memory_address_to_id_state.deduce_output(((input_pc_col0) + (M31_1))); + let memory_id_to_big_value_tmp_983 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_982); + let op1_id_col20 = memory_address_to_id_value_tmp_982; + trace[20].data[row_index] = op1_id_col20; + sub_components_inputs.memory_address_to_id_inputs[2] + .extend(((input_pc_col0) + (M31_1)).unpack()); + + lookup_data.memoryaddresstoid[2].push([((input_pc_col0) + (M31_1)), op1_id_col20]); + + // cond_decode_small_sign. + + let msb_tmp_984 = memory_id_to_big_value_tmp_983.get_m31(27).eq(M31_256); + let msb_col21 = msb_tmp_984.as_m31(); + trace[21].data[row_index] = msb_col21; + let mid_limbs_set_tmp_985 = memory_id_to_big_value_tmp_983.get_m31(20).eq(M31_511); + let mid_limbs_set_col22 = mid_limbs_set_tmp_985.as_m31(); + trace[22].data[row_index] = mid_limbs_set_col22; + + let op1_limb_0_col23 = memory_id_to_big_value_tmp_983.get_m31(0); + trace[23].data[row_index] = op1_limb_0_col23; + let op1_limb_1_col24 = memory_id_to_big_value_tmp_983.get_m31(1); + trace[24].data[row_index] = op1_limb_1_col24; + let op1_limb_2_col25 = memory_id_to_big_value_tmp_983.get_m31(2); + trace[25].data[row_index] = op1_limb_2_col25; + sub_components_inputs.memory_id_to_big_inputs[2].extend(op1_id_col20.unpack()); + + lookup_data.memoryidtobig[2].push([ + op1_id_col20, + op1_limb_0_col23, + op1_limb_1_col24, + op1_limb_2_col25, + ((mid_limbs_set_col22) * (M31_511)), + ((mid_limbs_set_col22) * (M31_511)), + ((mid_limbs_set_col22) * (M31_511)), + ((mid_limbs_set_col22) * (M31_511)), + ((mid_limbs_set_col22) * (M31_511)), + ((mid_limbs_set_col22) * (M31_511)), + ((mid_limbs_set_col22) * (M31_511)), + ((mid_limbs_set_col22) * (M31_511)), + ((mid_limbs_set_col22) * (M31_511)), + ((mid_limbs_set_col22) * (M31_511)), + ((mid_limbs_set_col22) * (M31_511)), + ((mid_limbs_set_col22) * (M31_511)), + ((mid_limbs_set_col22) * (M31_511)), + ((mid_limbs_set_col22) * (M31_511)), + ((mid_limbs_set_col22) * (M31_511)), + ((mid_limbs_set_col22) * (M31_511)), + ((mid_limbs_set_col22) * (M31_511)), + ((mid_limbs_set_col22) * (M31_511)), + (((M31_136) * (msb_col21)) - (mid_limbs_set_col22)), + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + ((msb_col21) * (M31_256)), + ]); + + lookup_data.opcodes[0].push([input_pc_col0, input_ap_col1, input_fp_col2]); + lookup_data.opcodes[1].push([ + ((input_pc_col0) + (M31_2)), + ((input_ap_col1) + (ap_update_add_1_col7)), + input_fp_col2, + ]); + }); + + (trace, sub_components_inputs, lookup_data) +} + +pub struct LookupData { + pub memoryaddresstoid: [Vec<[PackedM31; 2]>; 3], + pub memoryidtobig: [Vec<[PackedM31; 29]>; 3], + 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), + Vec::with_capacity(capacity), + ], + memoryidtobig: [ + Vec::with_capacity(capacity), + 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.memoryaddresstoid[2]; + 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[2]; + 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 85c1a11d..9d5d625a 100644 --- a/stwo_cairo_prover/crates/prover/src/components/mod.rs +++ b/stwo_cairo_prover/crates/prover/src/components/mod.rs @@ -4,6 +4,10 @@ use stwo_prover::core::backend::simd::conversion::Pack; pub mod add_ap_opcode_is_imm_f_op1_base_fp_f; pub mod add_ap_opcode_is_imm_f_op1_base_fp_t; pub mod add_ap_opcode_is_imm_t_op1_base_fp_f; +pub mod add_opcode_is_small_f_is_imm_f; +pub mod add_opcode_is_small_f_is_imm_t; +pub mod add_opcode_is_small_t_is_imm_f; +pub mod add_opcode_is_small_t_is_imm_t; pub mod assert_eq_opcode_is_double_deref_f_is_imm_f; pub mod assert_eq_opcode_is_double_deref_f_is_imm_t; pub mod assert_eq_opcode_is_double_deref_t_is_imm_f; 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 742afa19..3db450e7 100644 --- a/stwo_cairo_prover/crates/prover/src/input/state_transitions.rs +++ b/stwo_cairo_prover/crates/prover/src/input/state_transitions.rs @@ -555,7 +555,7 @@ impl StateTransitions { opcode_call: false, opcode_ret: false, opcode_assert_eq: true, - } if !dev_mode => { + } => { let op1_addr = if op0_base_fp { fp } else { ap }; let op1 = mem.get(op1_addr.0.checked_add_signed(offset0 as i32).unwrap()); if op1_imm {