From a0797396b348918c053676bc0008bd24c6650d2f Mon Sep 17 00:00:00 2001 From: Ohad Agadi Date: Sun, 1 Dec 2024 12:39:04 +0200 Subject: [PATCH] add_ap components --- .../crates/prover/src/cairo_air/air.rs | 268 +++++++++++- .../component.rs | 211 +++++++++ .../mod.rs | 5 + .../prover.rs | 409 ++++++++++++++++++ .../component.rs | 211 +++++++++ .../mod.rs | 5 + .../prover.rs | 409 ++++++++++++++++++ .../component.rs | 208 +++++++++ .../mod.rs | 5 + .../prover.rs | 393 +++++++++++++++++ .../src/components/generic_opcode/prover.rs | 4 +- .../crates/prover/src/components/mod.rs | 3 + .../prover/src/input/state_transitions.rs | 41 +- 13 files changed, 2133 insertions(+), 39 deletions(-) create mode 100644 stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_f_op1_base_fp_f/component.rs create mode 100644 stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_f_op1_base_fp_f/mod.rs create mode 100644 stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_f_op1_base_fp_f/prover.rs create mode 100644 stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_f_op1_base_fp_t/component.rs create mode 100644 stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_f_op1_base_fp_t/mod.rs create mode 100644 stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_f_op1_base_fp_t/prover.rs create mode 100644 stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_t_op1_base_fp_f/component.rs create mode 100644 stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_t_op1_base_fp_f/mod.rs create mode 100644 stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_t_op1_base_fp_f/prover.rs diff --git a/stwo_cairo_prover/crates/prover/src/cairo_air/air.rs b/stwo_cairo_prover/crates/prover/src/cairo_air/air.rs index 7cd8e5aa..722c7f8b 100644 --- a/stwo_cairo_prover/crates/prover/src/cairo_air/air.rs +++ b/stwo_cairo_prover/crates/prover/src/cairo_air/air.rs @@ -20,7 +20,10 @@ use crate::components::memory::{memory_address_to_id, memory_id_to_big}; use crate::components::range_check_vector::{ range_check_19, range_check_4_3, range_check_7_2_5, range_check_9_9, }; -use crate::components::{generic_opcode, ret_opcode, verify_instruction}; +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, generic_opcode, ret_opcode, verify_instruction, +}; use crate::felt::split_f252; use crate::input::state_transitions::StateTransitions; use crate::input::CairoInput; @@ -38,17 +41,26 @@ pub type PublicMemory = Vec<(u32, u32, [u32; 8])>; #[derive(Serialize, Deserialize)] pub struct OpcodeClaim { + add_ap_f_f: Vec, + add_ap_f_t: Vec, + add_ap_t_f: Vec, ret: Vec, generic: Vec, } impl OpcodeClaim { pub fn mix_into(&self, channel: &mut impl 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)); self.ret.iter().for_each(|c| c.mix_into(channel)); self.generic.iter().for_each(|c| c.mix_into(channel)); } pub fn log_sizes(&self) -> TreeVec> { TreeVec::concat_cols(chain!( + 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()), self.generic.iter().map(|c| c.log_sizes()), self.ret.iter().map(|c| c.log_sizes()), )) @@ -147,14 +159,53 @@ impl PublicData { } pub struct OpcodesClaimGenerator { + add_ap_f_f: Vec, + add_ap_f_t: Vec, + add_ap_t_f: Vec, generic: Vec, ret: Vec, } impl OpcodesClaimGenerator { pub fn new(input: StateTransitions) -> Self { // TODO(Ohad): decide split sizes for opcode traces. + let mut add_ap_f_f = vec![]; + let mut add_ap_f_t = vec![]; + let mut add_ap_t_f = vec![]; let mut generic = vec![]; let mut ret = vec![]; + if !input + .casm_states_by_opcode + .add_ap_opcode_is_imm_f_op1_base_fp_f + .is_empty() + { + add_ap_f_f.push(add_ap_opcode_is_imm_f_op1_base_fp_f::ClaimGenerator::new( + input + .casm_states_by_opcode + .add_ap_opcode_is_imm_f_op1_base_fp_f, + )); + } + if !input + .casm_states_by_opcode + .add_ap_opcode_is_imm_f_op1_base_fp_t + .is_empty() + { + add_ap_f_t.push(add_ap_opcode_is_imm_f_op1_base_fp_t::ClaimGenerator::new( + input + .casm_states_by_opcode + .add_ap_opcode_is_imm_f_op1_base_fp_t, + )); + } + if !input + .casm_states_by_opcode + .add_ap_opcode_is_imm_t_op1_base_fp_f + .is_empty() + { + add_ap_t_f.push(add_ap_opcode_is_imm_t_op1_base_fp_f::ClaimGenerator::new( + input + .casm_states_by_opcode + .add_ap_opcode_is_imm_t_op1_base_fp_f, + )); + } if !input.casm_states_by_opcode.generic_opcode.is_empty() { generic.push(generic_opcode::ClaimGenerator::new( input.casm_states_by_opcode.generic_opcode, @@ -165,7 +216,13 @@ impl OpcodesClaimGenerator { input.casm_states_by_opcode.ret_opcode, )); } - Self { ret, generic } + Self { + add_ap_f_f, + add_ap_f_t, + add_ap_t_f, + ret, + generic, + } } pub fn write_trace( @@ -177,6 +234,42 @@ 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_ap_f_f_claims, add_ap_f_f_interaction_gens) = self + .add_ap_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_ap_f_t_claims, add_ap_f_t_interaction_gens) = self + .add_ap_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_ap_t_f_claims, add_ap_t_f_interaction_gens) = self + .add_ap_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 (generic_opcode_claims, generic_opcode_interaction_gens) = self .generic .into_iter() @@ -205,10 +298,16 @@ impl OpcodesClaimGenerator { .unzip(); ( OpcodeClaim { + 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, generic: generic_opcode_claims, ret: ret_claims, }, OpcodesInteractionClaimGenerator { + 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, generic_opcode_interaction_gens, ret_interaction_gens, }, @@ -218,17 +317,44 @@ impl OpcodesClaimGenerator { #[derive(Serialize, Deserialize)] pub struct OpcodeInteractionClaim { + add_ap_f_f: Vec, + add_ap_f_t: Vec, + add_ap_t_f: Vec, generic: Vec, ret: Vec, } impl OpcodeInteractionClaim { pub fn mix_into(&self, channel: &mut impl 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)); self.generic.iter().for_each(|c| c.mix_into(channel)); self.ret.iter().for_each(|c| c.mix_into(channel)); } pub fn sum(&self) -> SecureField { let mut sum = QM31::zero(); + for interaction_claim in &self.add_ap_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_ap_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_ap_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.generic { let (total_sum, claimed_sum) = interaction_claim.logup_sums; sum += match claimed_sum { @@ -248,6 +374,9 @@ impl OpcodeInteractionClaim { } pub struct OpcodesInteractionClaimGenerator { + add_ap_f_f: Vec, + add_ap_f_t: Vec, + add_ap_t_f: Vec, generic_opcode_interaction_gens: Vec, ret_interaction_gens: Vec, } @@ -257,6 +386,45 @@ impl OpcodesInteractionClaimGenerator { tree_builder: &mut TreeBuilder<'_, '_, SimdBackend, Blake2sMerkleChannel>, interaction_elements: &CairoInteractionElements, ) -> OpcodeInteractionClaim { + let add_ap_f_f_interaction_claims = self + .add_ap_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_ap_f_t_interaction_claims = self + .add_ap_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_ap_t_f_interaction_claims = self + .add_ap_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 generic_opcode_interaction_claims = self .generic_opcode_interaction_gens .into_iter() @@ -286,6 +454,9 @@ impl OpcodesInteractionClaimGenerator { }) .collect(); OpcodeInteractionClaim { + 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, generic: generic_opcode_interaction_claims, ret: ret_interaction_claims, } @@ -560,6 +731,9 @@ pub fn lookup_sum( } pub struct OpcodeComponents { + add_ap_f_f: Vec, + add_ap_f_t: Vec, + add_ap_t_f: Vec, generic: Vec, ret: Vec, } @@ -570,6 +744,78 @@ impl OpcodeComponents { interaction_elements: &CairoInteractionElements, interaction_claim: &OpcodeInteractionClaim, ) -> Self { + let add_ap_f_f_components = claim + .add_ap_f_f + .iter() + .zip(interaction_claim.add_ap_f_f.iter()) + .map(|(&claim, &interaction_claim)| { + add_ap_opcode_is_imm_f_op1_base_fp_f::Component::new( + tree_span_provider, + add_ap_opcode_is_imm_f_op1_base_fp_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_ap_f_t_components = claim + .add_ap_f_t + .iter() + .zip(interaction_claim.add_ap_f_t.iter()) + .map(|(&claim, &interaction_claim)| { + add_ap_opcode_is_imm_f_op1_base_fp_t::Component::new( + tree_span_provider, + add_ap_opcode_is_imm_f_op1_base_fp_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_t_f_components = claim + .add_ap_t_f + .iter() + .zip(interaction_claim.add_ap_t_f.iter()) + .map(|(&claim, &interaction_claim)| { + add_ap_opcode_is_imm_t_op1_base_fp_f::Component::new( + tree_span_provider, + add_ap_opcode_is_imm_t_op1_base_fp_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 generic_components = claim .generic .iter() @@ -623,6 +869,9 @@ impl OpcodeComponents { }) .collect_vec(); Self { + 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, generic: generic_components, ret: ret_components, } @@ -630,6 +879,21 @@ impl OpcodeComponents { pub fn provers(&self) -> Vec<&dyn ComponentProver> { let mut vec: Vec<&dyn ComponentProver> = vec![]; + vec.extend( + self.add_ap_f_f + .iter() + .map(|component| component as &dyn ComponentProver), + ); + vec.extend( + self.add_ap_f_t + .iter() + .map(|component| component as &dyn ComponentProver), + ); + vec.extend( + self.add_ap_t_f + .iter() + .map(|component| component as &dyn ComponentProver), + ); vec.extend( self.generic .iter() diff --git a/stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_f_op1_base_fp_f/component.rs b/stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_f_op1_base_fp_f/component.rs new file mode 100644 index 00000000..e2c6b5d9 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_f_op1_base_fp_f/component.rs @@ -0,0 +1,211 @@ +#![allow(non_camel_case_types)] +#![allow(unused_imports)] +use num_traits::{One, Zero}; +use serde::{Deserialize, Serialize}; +use stwo_prover::constraint_framework::logup::{LogupAtRow, LogupSums, LookupElements}; +use stwo_prover::constraint_framework::{ + EvalAtRow, FrameworkComponent, FrameworkEval, RelationEntry, +}; +use stwo_prover::core::backend::simd::m31::LOG_N_LANES; +use stwo_prover::core::channel::Channel; +use stwo_prover::core::fields::m31::M31; +use stwo_prover::core::fields::qm31::SecureField; +use stwo_prover::core::fields::secure_column::SECURE_EXTENSION_DEGREE; +use stwo_prover::core::pcs::TreeVec; + +use crate::relations; + +pub struct Eval { + pub claim: Claim, + pub memoryaddresstoid_lookup_elements: relations::MemoryAddressToId, + pub memoryidtobig_lookup_elements: relations::MemoryIdToBig, + pub opcodes_lookup_elements: relations::Opcodes, + pub verifyinstruction_lookup_elements: relations::VerifyInstruction, +} + +#[derive(Copy, Clone, Serialize, Deserialize)] +pub struct Claim { + pub n_calls: usize, +} +impl Claim { + pub fn log_sizes(&self) -> TreeVec> { + let log_size = std::cmp::max(self.n_calls.next_power_of_two().ilog2(), LOG_N_LANES); + let trace_log_sizes = vec![log_size; 10]; + let interaction_log_sizes = vec![log_size; SECURE_EXTENSION_DEGREE * 5]; + let preprocessed_log_sizes = vec![log_size]; + TreeVec::new(vec![ + preprocessed_log_sizes, + trace_log_sizes, + interaction_log_sizes, + ]) + } + + pub fn mix_into(&self, channel: &mut impl Channel) { + channel.mix_u64(self.n_calls as u64); + } +} + +#[derive(Copy, Clone, Serialize, Deserialize)] +pub struct InteractionClaim { + pub logup_sums: LogupSums, +} +impl InteractionClaim { + pub fn mix_into(&self, channel: &mut impl Channel) { + let (total_sum, claimed_sum) = self.logup_sums; + channel.mix_felts(&[total_sum]); + if let Some(claimed_sum) = claimed_sum { + channel.mix_felts(&[claimed_sum.0]); + channel.mix_u64(claimed_sum.1 as u64); + } + } +} + +pub type Component = FrameworkComponent; + +impl FrameworkEval for Eval { + fn log_size(&self) -> u32 { + std::cmp::max(self.claim.n_calls.next_power_of_two().ilog2(), LOG_N_LANES) + } + + fn max_constraint_log_degree_bound(&self) -> u32 { + self.log_size() + 1 + } + + #[allow(unused_parens)] + #[allow(clippy::double_parens)] + #[allow(non_snake_case)] + fn evaluate(&self, mut eval: E) -> E { + let M31_0 = E::F::from(M31::from(0)); + let M31_1 = E::F::from(M31::from(1)); + let M31_134217728 = E::F::from(M31::from(134217728)); + let M31_136 = E::F::from(M31::from(136)); + let M31_256 = E::F::from(M31::from(256)); + let M31_262144 = E::F::from(M31::from(262144)); + let M31_32767 = E::F::from(M31::from(32767)); + let M31_32768 = E::F::from(M31::from(32768)); + let M31_511 = E::F::from(M31::from(511)); + let M31_512 = E::F::from(M31::from(512)); + let input_pc_col0 = eval.next_trace_mask(); + let input_ap_col1 = eval.next_trace_mask(); + let input_fp_col2 = eval.next_trace_mask(); + let offset2_col3 = eval.next_trace_mask(); + let op1_id_col4 = eval.next_trace_mask(); + let msb_col5 = eval.next_trace_mask(); + let mid_limbs_set_col6 = eval.next_trace_mask(); + let op1_limb_0_col7 = eval.next_trace_mask(); + let op1_limb_1_col8 = eval.next_trace_mask(); + let op1_limb_2_col9 = eval.next_trace_mask(); + + // decode_instruction_95ed11aea2bb2eff. + + eval.add_to_relation(&[RelationEntry::new( + &self.verifyinstruction_lookup_elements, + E::EF::one(), + &[ + input_pc_col0.clone(), + M31_32767.clone(), + M31_32767.clone(), + offset2_col3.clone(), + M31_1.clone(), + M31_1.clone(), + M31_0.clone(), + M31_0.clone(), + M31_1.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.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(), + &[ + (input_ap_col1.clone() + (offset2_col3.clone() - M31_32768.clone())), + op1_id_col4.clone(), + ], + )]); + + // cond_decode_small_sign. + + // msb is a bit. + eval.add_constraint((msb_col5.clone() * (msb_col5.clone() - M31_1.clone()))); + // mid_limbs_set is a bit. + eval.add_constraint( + (mid_limbs_set_col6.clone() * (mid_limbs_set_col6.clone() - M31_1.clone())), + ); + // Cannot have msb equals 0 and mid_limbs_set equals 1. + eval.add_constraint( + ((M31_1.clone() * mid_limbs_set_col6.clone()) * (msb_col5.clone() - M31_1.clone())), + ); + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryidtobig_lookup_elements, + E::EF::one(), + &[ + op1_id_col4.clone(), + op1_limb_0_col7.clone(), + op1_limb_1_col8.clone(), + op1_limb_2_col9.clone(), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + ((M31_136.clone() * msb_col5.clone()) - mid_limbs_set_col6.clone()), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + (msb_col5.clone() * M31_256.clone()), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.opcodes_lookup_elements, + E::EF::one(), + &[ + input_pc_col0.clone(), + input_ap_col1.clone(), + input_fp_col2.clone(), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.opcodes_lookup_elements, + -E::EF::one(), + &[ + (input_pc_col0.clone() + M31_1.clone()), + (input_ap_col1.clone() + + ((((op1_limb_0_col7.clone() + + (op1_limb_1_col8.clone() * M31_512.clone())) + + (op1_limb_2_col9.clone() * M31_262144.clone())) + - msb_col5.clone()) + - (M31_134217728.clone() * mid_limbs_set_col6.clone()))), + input_fp_col2.clone(), + ], + )]); + + eval.finalize_logup(); + eval + } +} diff --git a/stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_f_op1_base_fp_f/mod.rs b/stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_f_op1_base_fp_f/mod.rs new file mode 100644 index 00000000..3f7a8d74 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_f_op1_base_fp_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_ap_opcode_is_imm_f_op1_base_fp_f/prover.rs b/stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_f_op1_base_fp_f/prover.rs new file mode 100644 index 00000000..8b9ba632 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_f_op1_base_fp_f/prover.rs @@ -0,0 +1,409 @@ +#![allow(unused_parens)] +#![allow(unused_imports)] +use itertools::{chain, zip_eq, Itertools}; +use num_traits::{One, Zero}; +use prover_types::cpu::*; +use prover_types::simd::*; +use stwo_prover::constraint_framework::logup::LogupTraceGenerator; +use stwo_prover::constraint_framework::Relation; +use stwo_prover::core::air::Component; +use stwo_prover::core::backend::simd::column::BaseColumn; +use stwo_prover::core::backend::simd::conversion::Unpack; +use stwo_prover::core::backend::simd::m31::{PackedM31, LOG_N_LANES, N_LANES}; +use stwo_prover::core::backend::simd::qm31::PackedQM31; +use stwo_prover::core::backend::simd::SimdBackend; +use stwo_prover::core::backend::{Col, Column}; +use stwo_prover::core::fields::m31::M31; +use stwo_prover::core::pcs::TreeBuilder; +use stwo_prover::core::poly::circle::{CanonicCoset, CircleEvaluation}; +use stwo_prover::core::poly::BitReversedOrder; +use stwo_prover::core::utils::bit_reverse_coset_to_circle_domain_order; +use stwo_prover::core::vcs::blake2_merkle::{Blake2sMerkleChannel, Blake2sMerkleHasher}; + +use super::component::{Claim, InteractionClaim}; +use crate::components::{memory_address_to_id, memory_id_to_big, pack_values, verify_instruction}; +use crate::relations; + +pub type InputType = CasmState; +pub type PackedInputType = PackedCasmState; +const N_TRACE_COLUMNS: usize = 10; + +#[derive(Default)] +pub struct ClaimGenerator { + pub inputs: Vec, +} +impl ClaimGenerator { + pub fn new(inputs: Vec) -> Self { + Self { inputs } + } + + pub fn write_trace( + mut self, + tree_builder: &mut TreeBuilder<'_, '_, SimdBackend, Blake2sMerkleChannel>, + memory_address_to_id_state: &mut memory_address_to_id::ClaimGenerator, + memory_id_to_big_state: &mut memory_id_to_big::ClaimGenerator, + verify_instruction_state: &mut verify_instruction::ClaimGenerator, + ) -> (Claim, InteractionClaimGenerator) { + let n_calls = self.inputs.len(); + assert_ne!(n_calls, 0); + let size = std::cmp::max(n_calls.next_power_of_two(), N_LANES); + let need_padding = n_calls != size; + + if need_padding { + self.inputs.resize(size, *self.inputs.first().unwrap()); + bit_reverse_coset_to_circle_domain_order(&mut self.inputs); + } + + let packed_inputs = pack_values(&self.inputs); + let (trace, mut sub_components_inputs, lookup_data) = write_trace_simd( + packed_inputs, + memory_address_to_id_state, + memory_id_to_big_state, + ); + + if need_padding { + sub_components_inputs.bit_reverse_coset_to_circle_domain_order(); + } + sub_components_inputs + .memory_address_to_id_inputs + .iter() + .for_each(|inputs| { + memory_address_to_id_state.add_inputs(&inputs[..n_calls]); + }); + sub_components_inputs + .memory_id_to_big_inputs + .iter() + .for_each(|inputs| { + memory_id_to_big_state.add_inputs(&inputs[..n_calls]); + }); + sub_components_inputs + .verify_instruction_inputs + .iter() + .for_each(|inputs| { + verify_instruction_state.add_inputs(&inputs[..n_calls]); + }); + + tree_builder.extend_evals( + trace + .into_iter() + .map(|eval| { + let domain = CanonicCoset::new( + eval.len() + .checked_ilog2() + .expect("Input is not a power of 2!"), + ) + .circle_domain(); + CircleEvaluation::::new(domain, eval) + }) + .collect_vec(), + ); + + ( + Claim { n_calls }, + InteractionClaimGenerator { + n_calls, + lookup_data, + }, + ) + } + + pub fn add_inputs(&mut self, inputs: &[InputType]) { + self.inputs.extend(inputs); + } +} + +pub struct SubComponentInputs { + pub memory_address_to_id_inputs: [Vec; 1], + pub memory_id_to_big_inputs: [Vec; 1], + pub verify_instruction_inputs: [Vec; 1], +} +impl SubComponentInputs { + #[allow(unused_variables)] + fn with_capacity(capacity: usize) -> Self { + Self { + memory_address_to_id_inputs: [Vec::with_capacity(capacity)], + memory_id_to_big_inputs: [Vec::with_capacity(capacity)], + verify_instruction_inputs: [Vec::with_capacity(capacity)], + } + } + + fn bit_reverse_coset_to_circle_domain_order(&mut self) { + self.memory_address_to_id_inputs + .iter_mut() + .for_each(|vec| bit_reverse_coset_to_circle_domain_order(vec)); + self.memory_id_to_big_inputs + .iter_mut() + .for_each(|vec| bit_reverse_coset_to_circle_domain_order(vec)); + self.verify_instruction_inputs + .iter_mut() + .for_each(|vec| bit_reverse_coset_to_circle_domain_order(vec)); + } +} + +#[allow(clippy::useless_conversion)] +#[allow(unused_variables)] +#[allow(clippy::double_parens)] +#[allow(non_snake_case)] +pub fn write_trace_simd( + inputs: Vec, + memory_address_to_id_state: &mut memory_address_to_id::ClaimGenerator, + memory_id_to_big_state: &mut memory_id_to_big::ClaimGenerator, +) -> ( + [BaseColumn; N_TRACE_COLUMNS], + SubComponentInputs, + LookupData, +) { + const N_TRACE_COLUMNS: usize = 10; + let mut trace: [_; N_TRACE_COLUMNS] = + std::array::from_fn(|_| Col::::zeros(inputs.len() * N_LANES)); + + let mut lookup_data = LookupData::with_capacity(inputs.len()); + #[allow(unused_mut)] + let mut sub_components_inputs = SubComponentInputs::with_capacity(inputs.len()); + + let M31_0 = PackedM31::broadcast(M31::from(0)); + let M31_1 = PackedM31::broadcast(M31::from(1)); + let M31_134217728 = PackedM31::broadcast(M31::from(134217728)); + let M31_136 = PackedM31::broadcast(M31::from(136)); + let M31_256 = PackedM31::broadcast(M31::from(256)); + let M31_262144 = PackedM31::broadcast(M31::from(262144)); + let M31_32767 = PackedM31::broadcast(M31::from(32767)); + let M31_32768 = PackedM31::broadcast(M31::from(32768)); + let M31_511 = PackedM31::broadcast(M31::from(511)); + let M31_512 = PackedM31::broadcast(M31::from(512)); + let UInt16_13 = PackedUInt16::broadcast(UInt16::from(13)); + let UInt16_4 = PackedUInt16::broadcast(UInt16::from(4)); + let UInt16_5 = PackedUInt16::broadcast(UInt16::from(5)); + let UInt16_7 = PackedUInt16::broadcast(UInt16::from(7)); + + inputs.into_iter().enumerate().for_each( + |(row_index, add_ap_opcode_is_imm_f_op1_base_fp_f_input)| { + let input_tmp_916 = add_ap_opcode_is_imm_f_op1_base_fp_f_input; + let input_pc_col0 = input_tmp_916.pc; + trace[0].data[row_index] = input_pc_col0; + let input_ap_col1 = input_tmp_916.ap; + trace[1].data[row_index] = input_ap_col1; + let input_fp_col2 = input_tmp_916.fp; + trace[2].data[row_index] = input_fp_col2; + + // decode_instruction_95ed11aea2bb2eff. + + let memory_address_to_id_value_tmp_921 = + memory_address_to_id_state.deduce_output(input_pc_col0); + let memory_id_to_big_value_tmp_922 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_921); + let offset2_tmp_923 = + ((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_922.get_m31(3))) + >> (UInt16_5)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_922.get_m31(4))) + << (UInt16_4))) + + (((PackedUInt16::from_m31(memory_id_to_big_value_tmp_922.get_m31(5))) + & (UInt16_7)) + << (UInt16_13))); + let offset2_col3 = offset2_tmp_923.as_m31(); + trace[3].data[row_index] = offset2_col3; + + sub_components_inputs.verify_instruction_inputs[0].extend( + ( + input_pc_col0, + [M31_32767, M31_32767, offset2_col3], + [ + M31_1, M31_1, M31_0, M31_0, M31_1, M31_0, M31_0, M31_0, M31_0, M31_0, + M31_1, M31_0, M31_0, M31_0, M31_0, + ], + ) + .unpack(), + ); + + lookup_data.verifyinstruction[0].push([ + input_pc_col0, + M31_32767, + M31_32767, + offset2_col3, + M31_1, + M31_1, + M31_0, + M31_0, + M31_1, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_1, + M31_0, + M31_0, + M31_0, + M31_0, + ]); + + // read_small. + + let memory_address_to_id_value_tmp_929 = memory_address_to_id_state + .deduce_output(((input_ap_col1) + ((offset2_col3) - (M31_32768)))); + let memory_id_to_big_value_tmp_930 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_929); + let op1_id_col4 = memory_address_to_id_value_tmp_929; + trace[4].data[row_index] = op1_id_col4; + sub_components_inputs.memory_address_to_id_inputs[0] + .extend(((input_ap_col1) + ((offset2_col3) - (M31_32768))).unpack()); + + lookup_data.memoryaddresstoid[0].push([ + ((input_ap_col1) + ((offset2_col3) - (M31_32768))), + op1_id_col4, + ]); + + // cond_decode_small_sign. + + let msb_tmp_931 = memory_id_to_big_value_tmp_930.get_m31(27).eq(M31_256); + let msb_col5 = msb_tmp_931.as_m31(); + trace[5].data[row_index] = msb_col5; + let mid_limbs_set_tmp_932 = memory_id_to_big_value_tmp_930.get_m31(20).eq(M31_511); + let mid_limbs_set_col6 = mid_limbs_set_tmp_932.as_m31(); + trace[6].data[row_index] = mid_limbs_set_col6; + + let op1_limb_0_col7 = memory_id_to_big_value_tmp_930.get_m31(0); + trace[7].data[row_index] = op1_limb_0_col7; + let op1_limb_1_col8 = memory_id_to_big_value_tmp_930.get_m31(1); + trace[8].data[row_index] = op1_limb_1_col8; + let op1_limb_2_col9 = memory_id_to_big_value_tmp_930.get_m31(2); + trace[9].data[row_index] = op1_limb_2_col9; + sub_components_inputs.memory_id_to_big_inputs[0].extend(op1_id_col4.unpack()); + + lookup_data.memoryidtobig[0].push([ + op1_id_col4, + op1_limb_0_col7, + op1_limb_1_col8, + op1_limb_2_col9, + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + (((M31_136) * (msb_col5)) - (mid_limbs_set_col6)), + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + ((msb_col5) * (M31_256)), + ]); + + lookup_data.opcodes[0].push([input_pc_col0, input_ap_col1, input_fp_col2]); + lookup_data.opcodes[1].push([ + ((input_pc_col0) + (M31_1)), + ((input_ap_col1) + + (((((op1_limb_0_col7) + ((op1_limb_1_col8) * (M31_512))) + + ((op1_limb_2_col9) * (M31_262144))) + - (msb_col5)) + - ((M31_134217728) * (mid_limbs_set_col6)))), + input_fp_col2, + ]); + }, + ); + + (trace, sub_components_inputs, lookup_data) +} + +pub struct LookupData { + pub memoryaddresstoid: [Vec<[PackedM31; 2]>; 1], + pub memoryidtobig: [Vec<[PackedM31; 29]>; 1], + pub opcodes: [Vec<[PackedM31; 3]>; 2], + pub verifyinstruction: [Vec<[PackedM31; 19]>; 1], +} +impl LookupData { + #[allow(unused_variables)] + fn with_capacity(capacity: usize) -> Self { + Self { + memoryaddresstoid: [Vec::with_capacity(capacity)], + memoryidtobig: [Vec::with_capacity(capacity)], + opcodes: [Vec::with_capacity(capacity), Vec::with_capacity(capacity)], + verifyinstruction: [Vec::with_capacity(capacity)], + } + } +} + +pub struct InteractionClaimGenerator { + pub n_calls: usize, + pub lookup_data: LookupData, +} +impl InteractionClaimGenerator { + pub fn write_interaction_trace( + self, + tree_builder: &mut TreeBuilder<'_, '_, SimdBackend, Blake2sMerkleChannel>, + memoryaddresstoid_lookup_elements: &relations::MemoryAddressToId, + memoryidtobig_lookup_elements: &relations::MemoryIdToBig, + opcodes_lookup_elements: &relations::Opcodes, + verifyinstruction_lookup_elements: &relations::VerifyInstruction, + ) -> InteractionClaim { + let log_size = std::cmp::max(self.n_calls.next_power_of_two().ilog2(), LOG_N_LANES); + let mut logup_gen = LogupTraceGenerator::new(log_size); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.verifyinstruction[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = verifyinstruction_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.memoryaddresstoid[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = memoryaddresstoid_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.memoryidtobig[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = memoryidtobig_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.opcodes[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = opcodes_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.opcodes[1]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = opcodes_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, -PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let (trace, total_sum, claimed_sum) = if self.n_calls == 1 << log_size { + let (trace, claimed_sum) = logup_gen.finalize_last(); + (trace, claimed_sum, None) + } else { + let (trace, [total_sum, claimed_sum]) = + logup_gen.finalize_at([(1 << log_size) - 1, self.n_calls - 1]); + (trace, total_sum, Some((claimed_sum, self.n_calls - 1))) + }; + tree_builder.extend_evals(trace); + + InteractionClaim { + logup_sums: (total_sum, claimed_sum), + } + } +} diff --git a/stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_f_op1_base_fp_t/component.rs b/stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_f_op1_base_fp_t/component.rs new file mode 100644 index 00000000..1d5ea340 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_f_op1_base_fp_t/component.rs @@ -0,0 +1,211 @@ +#![allow(non_camel_case_types)] +#![allow(unused_imports)] +use num_traits::{One, Zero}; +use serde::{Deserialize, Serialize}; +use stwo_prover::constraint_framework::logup::{LogupAtRow, LogupSums, LookupElements}; +use stwo_prover::constraint_framework::{ + EvalAtRow, FrameworkComponent, FrameworkEval, RelationEntry, +}; +use stwo_prover::core::backend::simd::m31::LOG_N_LANES; +use stwo_prover::core::channel::Channel; +use stwo_prover::core::fields::m31::M31; +use stwo_prover::core::fields::qm31::SecureField; +use stwo_prover::core::fields::secure_column::SECURE_EXTENSION_DEGREE; +use stwo_prover::core::pcs::TreeVec; + +use crate::relations; + +pub struct Eval { + pub claim: Claim, + pub memoryaddresstoid_lookup_elements: relations::MemoryAddressToId, + pub memoryidtobig_lookup_elements: relations::MemoryIdToBig, + pub opcodes_lookup_elements: relations::Opcodes, + pub verifyinstruction_lookup_elements: relations::VerifyInstruction, +} + +#[derive(Copy, Clone, Serialize, Deserialize)] +pub struct Claim { + pub n_calls: usize, +} +impl Claim { + pub fn log_sizes(&self) -> TreeVec> { + let log_size = std::cmp::max(self.n_calls.next_power_of_two().ilog2(), LOG_N_LANES); + let trace_log_sizes = vec![log_size; 10]; + let interaction_log_sizes = vec![log_size; SECURE_EXTENSION_DEGREE * 5]; + let preprocessed_log_sizes = vec![log_size]; + TreeVec::new(vec![ + preprocessed_log_sizes, + trace_log_sizes, + interaction_log_sizes, + ]) + } + + pub fn mix_into(&self, channel: &mut impl Channel) { + channel.mix_u64(self.n_calls as u64); + } +} + +#[derive(Copy, Clone, Serialize, Deserialize)] +pub struct InteractionClaim { + pub logup_sums: LogupSums, +} +impl InteractionClaim { + pub fn mix_into(&self, channel: &mut impl Channel) { + let (total_sum, claimed_sum) = self.logup_sums; + channel.mix_felts(&[total_sum]); + if let Some(claimed_sum) = claimed_sum { + channel.mix_felts(&[claimed_sum.0]); + channel.mix_u64(claimed_sum.1 as u64); + } + } +} + +pub type Component = FrameworkComponent; + +impl FrameworkEval for Eval { + fn log_size(&self) -> u32 { + std::cmp::max(self.claim.n_calls.next_power_of_two().ilog2(), LOG_N_LANES) + } + + fn max_constraint_log_degree_bound(&self) -> u32 { + self.log_size() + 1 + } + + #[allow(unused_parens)] + #[allow(clippy::double_parens)] + #[allow(non_snake_case)] + fn evaluate(&self, mut eval: E) -> E { + let M31_0 = E::F::from(M31::from(0)); + let M31_1 = E::F::from(M31::from(1)); + let M31_134217728 = E::F::from(M31::from(134217728)); + let M31_136 = E::F::from(M31::from(136)); + let M31_256 = E::F::from(M31::from(256)); + let M31_262144 = E::F::from(M31::from(262144)); + let M31_32767 = E::F::from(M31::from(32767)); + let M31_32768 = E::F::from(M31::from(32768)); + let M31_511 = E::F::from(M31::from(511)); + let M31_512 = E::F::from(M31::from(512)); + let input_pc_col0 = eval.next_trace_mask(); + let input_ap_col1 = eval.next_trace_mask(); + let input_fp_col2 = eval.next_trace_mask(); + let offset2_col3 = eval.next_trace_mask(); + let op1_id_col4 = eval.next_trace_mask(); + let msb_col5 = eval.next_trace_mask(); + let mid_limbs_set_col6 = eval.next_trace_mask(); + let op1_limb_0_col7 = eval.next_trace_mask(); + let op1_limb_1_col8 = eval.next_trace_mask(); + let op1_limb_2_col9 = eval.next_trace_mask(); + + // decode_instruction_3a1aeaa2aac0bdcf. + + eval.add_to_relation(&[RelationEntry::new( + &self.verifyinstruction_lookup_elements, + E::EF::one(), + &[ + input_pc_col0.clone(), + M31_32767.clone(), + M31_32767.clone(), + offset2_col3.clone(), + M31_1.clone(), + M31_1.clone(), + M31_0.clone(), + M31_1.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.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(), + &[ + (input_fp_col2.clone() + (offset2_col3.clone() - M31_32768.clone())), + op1_id_col4.clone(), + ], + )]); + + // cond_decode_small_sign. + + // msb is a bit. + eval.add_constraint((msb_col5.clone() * (msb_col5.clone() - M31_1.clone()))); + // mid_limbs_set is a bit. + eval.add_constraint( + (mid_limbs_set_col6.clone() * (mid_limbs_set_col6.clone() - M31_1.clone())), + ); + // Cannot have msb equals 0 and mid_limbs_set equals 1. + eval.add_constraint( + ((M31_1.clone() * mid_limbs_set_col6.clone()) * (msb_col5.clone() - M31_1.clone())), + ); + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryidtobig_lookup_elements, + E::EF::one(), + &[ + op1_id_col4.clone(), + op1_limb_0_col7.clone(), + op1_limb_1_col8.clone(), + op1_limb_2_col9.clone(), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + (mid_limbs_set_col6.clone() * M31_511.clone()), + ((M31_136.clone() * msb_col5.clone()) - mid_limbs_set_col6.clone()), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + (msb_col5.clone() * M31_256.clone()), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.opcodes_lookup_elements, + E::EF::one(), + &[ + input_pc_col0.clone(), + input_ap_col1.clone(), + input_fp_col2.clone(), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.opcodes_lookup_elements, + -E::EF::one(), + &[ + (input_pc_col0.clone() + M31_1.clone()), + (input_ap_col1.clone() + + ((((op1_limb_0_col7.clone() + + (op1_limb_1_col8.clone() * M31_512.clone())) + + (op1_limb_2_col9.clone() * M31_262144.clone())) + - msb_col5.clone()) + - (M31_134217728.clone() * mid_limbs_set_col6.clone()))), + input_fp_col2.clone(), + ], + )]); + + eval.finalize_logup(); + eval + } +} diff --git a/stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_f_op1_base_fp_t/mod.rs b/stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_f_op1_base_fp_t/mod.rs new file mode 100644 index 00000000..3f7a8d74 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_f_op1_base_fp_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_ap_opcode_is_imm_f_op1_base_fp_t/prover.rs b/stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_f_op1_base_fp_t/prover.rs new file mode 100644 index 00000000..ff59b6b8 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_f_op1_base_fp_t/prover.rs @@ -0,0 +1,409 @@ +#![allow(unused_parens)] +#![allow(unused_imports)] +use itertools::{chain, zip_eq, Itertools}; +use num_traits::{One, Zero}; +use prover_types::cpu::*; +use prover_types::simd::*; +use stwo_prover::constraint_framework::logup::LogupTraceGenerator; +use stwo_prover::constraint_framework::Relation; +use stwo_prover::core::air::Component; +use stwo_prover::core::backend::simd::column::BaseColumn; +use stwo_prover::core::backend::simd::conversion::Unpack; +use stwo_prover::core::backend::simd::m31::{PackedM31, LOG_N_LANES, N_LANES}; +use stwo_prover::core::backend::simd::qm31::PackedQM31; +use stwo_prover::core::backend::simd::SimdBackend; +use stwo_prover::core::backend::{Col, Column}; +use stwo_prover::core::fields::m31::M31; +use stwo_prover::core::pcs::TreeBuilder; +use stwo_prover::core::poly::circle::{CanonicCoset, CircleEvaluation}; +use stwo_prover::core::poly::BitReversedOrder; +use stwo_prover::core::utils::bit_reverse_coset_to_circle_domain_order; +use stwo_prover::core::vcs::blake2_merkle::{Blake2sMerkleChannel, Blake2sMerkleHasher}; + +use super::component::{Claim, InteractionClaim}; +use crate::components::{memory_address_to_id, memory_id_to_big, pack_values, verify_instruction}; +use crate::relations; + +pub type InputType = CasmState; +pub type PackedInputType = PackedCasmState; +const N_TRACE_COLUMNS: usize = 10; + +#[derive(Default)] +pub struct ClaimGenerator { + pub inputs: Vec, +} +impl ClaimGenerator { + pub fn new(inputs: Vec) -> Self { + Self { inputs } + } + + pub fn write_trace( + mut self, + tree_builder: &mut TreeBuilder<'_, '_, SimdBackend, Blake2sMerkleChannel>, + memory_address_to_id_state: &mut memory_address_to_id::ClaimGenerator, + memory_id_to_big_state: &mut memory_id_to_big::ClaimGenerator, + verify_instruction_state: &mut verify_instruction::ClaimGenerator, + ) -> (Claim, InteractionClaimGenerator) { + let n_calls = self.inputs.len(); + assert_ne!(n_calls, 0); + let size = std::cmp::max(n_calls.next_power_of_two(), N_LANES); + let need_padding = n_calls != size; + + if need_padding { + self.inputs.resize(size, *self.inputs.first().unwrap()); + bit_reverse_coset_to_circle_domain_order(&mut self.inputs); + } + + let packed_inputs = pack_values(&self.inputs); + let (trace, mut sub_components_inputs, lookup_data) = write_trace_simd( + packed_inputs, + memory_address_to_id_state, + memory_id_to_big_state, + ); + + if need_padding { + sub_components_inputs.bit_reverse_coset_to_circle_domain_order(); + } + sub_components_inputs + .memory_address_to_id_inputs + .iter() + .for_each(|inputs| { + memory_address_to_id_state.add_inputs(&inputs[..n_calls]); + }); + sub_components_inputs + .memory_id_to_big_inputs + .iter() + .for_each(|inputs| { + memory_id_to_big_state.add_inputs(&inputs[..n_calls]); + }); + sub_components_inputs + .verify_instruction_inputs + .iter() + .for_each(|inputs| { + verify_instruction_state.add_inputs(&inputs[..n_calls]); + }); + + tree_builder.extend_evals( + trace + .into_iter() + .map(|eval| { + let domain = CanonicCoset::new( + eval.len() + .checked_ilog2() + .expect("Input is not a power of 2!"), + ) + .circle_domain(); + CircleEvaluation::::new(domain, eval) + }) + .collect_vec(), + ); + + ( + Claim { n_calls }, + InteractionClaimGenerator { + n_calls, + lookup_data, + }, + ) + } + + pub fn add_inputs(&mut self, inputs: &[InputType]) { + self.inputs.extend(inputs); + } +} + +pub struct SubComponentInputs { + pub memory_address_to_id_inputs: [Vec; 1], + pub memory_id_to_big_inputs: [Vec; 1], + pub verify_instruction_inputs: [Vec; 1], +} +impl SubComponentInputs { + #[allow(unused_variables)] + fn with_capacity(capacity: usize) -> Self { + Self { + memory_address_to_id_inputs: [Vec::with_capacity(capacity)], + memory_id_to_big_inputs: [Vec::with_capacity(capacity)], + verify_instruction_inputs: [Vec::with_capacity(capacity)], + } + } + + fn bit_reverse_coset_to_circle_domain_order(&mut self) { + self.memory_address_to_id_inputs + .iter_mut() + .for_each(|vec| bit_reverse_coset_to_circle_domain_order(vec)); + self.memory_id_to_big_inputs + .iter_mut() + .for_each(|vec| bit_reverse_coset_to_circle_domain_order(vec)); + self.verify_instruction_inputs + .iter_mut() + .for_each(|vec| bit_reverse_coset_to_circle_domain_order(vec)); + } +} + +#[allow(clippy::useless_conversion)] +#[allow(unused_variables)] +#[allow(clippy::double_parens)] +#[allow(non_snake_case)] +pub fn write_trace_simd( + inputs: Vec, + memory_address_to_id_state: &mut memory_address_to_id::ClaimGenerator, + memory_id_to_big_state: &mut memory_id_to_big::ClaimGenerator, +) -> ( + [BaseColumn; N_TRACE_COLUMNS], + SubComponentInputs, + LookupData, +) { + const N_TRACE_COLUMNS: usize = 10; + let mut trace: [_; N_TRACE_COLUMNS] = + std::array::from_fn(|_| Col::::zeros(inputs.len() * N_LANES)); + + let mut lookup_data = LookupData::with_capacity(inputs.len()); + #[allow(unused_mut)] + let mut sub_components_inputs = SubComponentInputs::with_capacity(inputs.len()); + + let M31_0 = PackedM31::broadcast(M31::from(0)); + let M31_1 = PackedM31::broadcast(M31::from(1)); + let M31_134217728 = PackedM31::broadcast(M31::from(134217728)); + let M31_136 = PackedM31::broadcast(M31::from(136)); + let M31_256 = PackedM31::broadcast(M31::from(256)); + let M31_262144 = PackedM31::broadcast(M31::from(262144)); + let M31_32767 = PackedM31::broadcast(M31::from(32767)); + let M31_32768 = PackedM31::broadcast(M31::from(32768)); + let M31_511 = PackedM31::broadcast(M31::from(511)); + let M31_512 = PackedM31::broadcast(M31::from(512)); + let UInt16_13 = PackedUInt16::broadcast(UInt16::from(13)); + let UInt16_4 = PackedUInt16::broadcast(UInt16::from(4)); + let UInt16_5 = PackedUInt16::broadcast(UInt16::from(5)); + let UInt16_7 = PackedUInt16::broadcast(UInt16::from(7)); + + inputs.into_iter().enumerate().for_each( + |(row_index, add_ap_opcode_is_imm_f_op1_base_fp_t_input)| { + let input_tmp_944 = add_ap_opcode_is_imm_f_op1_base_fp_t_input; + let input_pc_col0 = input_tmp_944.pc; + trace[0].data[row_index] = input_pc_col0; + let input_ap_col1 = input_tmp_944.ap; + trace[1].data[row_index] = input_ap_col1; + let input_fp_col2 = input_tmp_944.fp; + trace[2].data[row_index] = input_fp_col2; + + // decode_instruction_3a1aeaa2aac0bdcf. + + let memory_address_to_id_value_tmp_949 = + memory_address_to_id_state.deduce_output(input_pc_col0); + let memory_id_to_big_value_tmp_950 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_949); + let offset2_tmp_951 = + ((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_950.get_m31(3))) + >> (UInt16_5)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_950.get_m31(4))) + << (UInt16_4))) + + (((PackedUInt16::from_m31(memory_id_to_big_value_tmp_950.get_m31(5))) + & (UInt16_7)) + << (UInt16_13))); + let offset2_col3 = offset2_tmp_951.as_m31(); + trace[3].data[row_index] = offset2_col3; + + sub_components_inputs.verify_instruction_inputs[0].extend( + ( + input_pc_col0, + [M31_32767, M31_32767, offset2_col3], + [ + M31_1, M31_1, M31_0, M31_1, M31_0, M31_0, M31_0, M31_0, M31_0, M31_0, + M31_1, M31_0, M31_0, M31_0, M31_0, + ], + ) + .unpack(), + ); + + lookup_data.verifyinstruction[0].push([ + input_pc_col0, + M31_32767, + M31_32767, + offset2_col3, + M31_1, + M31_1, + M31_0, + M31_1, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_1, + M31_0, + M31_0, + M31_0, + M31_0, + ]); + + // read_small. + + let memory_address_to_id_value_tmp_953 = memory_address_to_id_state + .deduce_output(((input_fp_col2) + ((offset2_col3) - (M31_32768)))); + let memory_id_to_big_value_tmp_954 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_953); + let op1_id_col4 = memory_address_to_id_value_tmp_953; + trace[4].data[row_index] = op1_id_col4; + sub_components_inputs.memory_address_to_id_inputs[0] + .extend(((input_fp_col2) + ((offset2_col3) - (M31_32768))).unpack()); + + lookup_data.memoryaddresstoid[0].push([ + ((input_fp_col2) + ((offset2_col3) - (M31_32768))), + op1_id_col4, + ]); + + // cond_decode_small_sign. + + let msb_tmp_955 = memory_id_to_big_value_tmp_954.get_m31(27).eq(M31_256); + let msb_col5 = msb_tmp_955.as_m31(); + trace[5].data[row_index] = msb_col5; + let mid_limbs_set_tmp_956 = memory_id_to_big_value_tmp_954.get_m31(20).eq(M31_511); + let mid_limbs_set_col6 = mid_limbs_set_tmp_956.as_m31(); + trace[6].data[row_index] = mid_limbs_set_col6; + + let op1_limb_0_col7 = memory_id_to_big_value_tmp_954.get_m31(0); + trace[7].data[row_index] = op1_limb_0_col7; + let op1_limb_1_col8 = memory_id_to_big_value_tmp_954.get_m31(1); + trace[8].data[row_index] = op1_limb_1_col8; + let op1_limb_2_col9 = memory_id_to_big_value_tmp_954.get_m31(2); + trace[9].data[row_index] = op1_limb_2_col9; + sub_components_inputs.memory_id_to_big_inputs[0].extend(op1_id_col4.unpack()); + + lookup_data.memoryidtobig[0].push([ + op1_id_col4, + op1_limb_0_col7, + op1_limb_1_col8, + op1_limb_2_col9, + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + ((mid_limbs_set_col6) * (M31_511)), + (((M31_136) * (msb_col5)) - (mid_limbs_set_col6)), + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + ((msb_col5) * (M31_256)), + ]); + + lookup_data.opcodes[0].push([input_pc_col0, input_ap_col1, input_fp_col2]); + lookup_data.opcodes[1].push([ + ((input_pc_col0) + (M31_1)), + ((input_ap_col1) + + (((((op1_limb_0_col7) + ((op1_limb_1_col8) * (M31_512))) + + ((op1_limb_2_col9) * (M31_262144))) + - (msb_col5)) + - ((M31_134217728) * (mid_limbs_set_col6)))), + input_fp_col2, + ]); + }, + ); + + (trace, sub_components_inputs, lookup_data) +} + +pub struct LookupData { + pub memoryaddresstoid: [Vec<[PackedM31; 2]>; 1], + pub memoryidtobig: [Vec<[PackedM31; 29]>; 1], + pub opcodes: [Vec<[PackedM31; 3]>; 2], + pub verifyinstruction: [Vec<[PackedM31; 19]>; 1], +} +impl LookupData { + #[allow(unused_variables)] + fn with_capacity(capacity: usize) -> Self { + Self { + memoryaddresstoid: [Vec::with_capacity(capacity)], + memoryidtobig: [Vec::with_capacity(capacity)], + opcodes: [Vec::with_capacity(capacity), Vec::with_capacity(capacity)], + verifyinstruction: [Vec::with_capacity(capacity)], + } + } +} + +pub struct InteractionClaimGenerator { + pub n_calls: usize, + pub lookup_data: LookupData, +} +impl InteractionClaimGenerator { + pub fn write_interaction_trace( + self, + tree_builder: &mut TreeBuilder<'_, '_, SimdBackend, Blake2sMerkleChannel>, + memoryaddresstoid_lookup_elements: &relations::MemoryAddressToId, + memoryidtobig_lookup_elements: &relations::MemoryIdToBig, + opcodes_lookup_elements: &relations::Opcodes, + verifyinstruction_lookup_elements: &relations::VerifyInstruction, + ) -> InteractionClaim { + let log_size = std::cmp::max(self.n_calls.next_power_of_two().ilog2(), LOG_N_LANES); + let mut logup_gen = LogupTraceGenerator::new(log_size); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.verifyinstruction[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = verifyinstruction_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.memoryaddresstoid[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = memoryaddresstoid_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.memoryidtobig[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = memoryidtobig_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.opcodes[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = opcodes_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.opcodes[1]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = opcodes_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, -PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let (trace, total_sum, claimed_sum) = if self.n_calls == 1 << log_size { + let (trace, claimed_sum) = logup_gen.finalize_last(); + (trace, claimed_sum, None) + } else { + let (trace, [total_sum, claimed_sum]) = + logup_gen.finalize_at([(1 << log_size) - 1, self.n_calls - 1]); + (trace, total_sum, Some((claimed_sum, self.n_calls - 1))) + }; + tree_builder.extend_evals(trace); + + InteractionClaim { + logup_sums: (total_sum, claimed_sum), + } + } +} diff --git a/stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_t_op1_base_fp_f/component.rs b/stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_t_op1_base_fp_f/component.rs new file mode 100644 index 00000000..2be7334f --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_t_op1_base_fp_f/component.rs @@ -0,0 +1,208 @@ +#![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; 9]; + let interaction_log_sizes = vec![log_size; SECURE_EXTENSION_DEGREE * 5]; + let preprocessed_log_sizes = vec![log_size]; + TreeVec::new(vec![ + preprocessed_log_sizes, + trace_log_sizes, + interaction_log_sizes, + ]) + } + + pub fn mix_into(&self, channel: &mut impl Channel) { + channel.mix_u64(self.n_calls as u64); + } +} + +#[derive(Copy, Clone, Serialize, Deserialize)] +pub struct InteractionClaim { + pub logup_sums: LogupSums, +} +impl InteractionClaim { + pub fn mix_into(&self, channel: &mut impl Channel) { + let (total_sum, claimed_sum) = self.logup_sums; + channel.mix_felts(&[total_sum]); + if let Some(claimed_sum) = claimed_sum { + channel.mix_felts(&[claimed_sum.0]); + channel.mix_u64(claimed_sum.1 as u64); + } + } +} + +pub type Component = FrameworkComponent; + +impl FrameworkEval for Eval { + fn log_size(&self) -> u32 { + std::cmp::max(self.claim.n_calls.next_power_of_two().ilog2(), LOG_N_LANES) + } + + fn max_constraint_log_degree_bound(&self) -> u32 { + self.log_size() + 1 + } + + #[allow(unused_parens)] + #[allow(clippy::double_parens)] + #[allow(non_snake_case)] + fn evaluate(&self, mut eval: E) -> E { + let M31_0 = E::F::from(M31::from(0)); + let M31_1 = E::F::from(M31::from(1)); + let M31_134217728 = E::F::from(M31::from(134217728)); + let M31_136 = E::F::from(M31::from(136)); + let M31_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_32767 = E::F::from(M31::from(32767)); + let M31_32769 = E::F::from(M31::from(32769)); + let M31_511 = E::F::from(M31::from(511)); + let M31_512 = E::F::from(M31::from(512)); + let input_pc_col0 = eval.next_trace_mask(); + let input_ap_col1 = eval.next_trace_mask(); + let input_fp_col2 = eval.next_trace_mask(); + let op1_id_col3 = eval.next_trace_mask(); + let msb_col4 = eval.next_trace_mask(); + let mid_limbs_set_col5 = eval.next_trace_mask(); + let op1_limb_0_col6 = eval.next_trace_mask(); + let op1_limb_1_col7 = eval.next_trace_mask(); + let op1_limb_2_col8 = eval.next_trace_mask(); + + // decode_instruction_a14b71db698d77c8. + + eval.add_to_relation(&[RelationEntry::new( + &self.verifyinstruction_lookup_elements, + E::EF::one(), + &[ + input_pc_col0.clone(), + M31_32767.clone(), + M31_32767.clone(), + M31_32769.clone(), + M31_1.clone(), + M31_1.clone(), + M31_1.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_1.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_col3.clone()], + )]); + + // cond_decode_small_sign. + + // msb is a bit. + eval.add_constraint((msb_col4.clone() * (msb_col4.clone() - M31_1.clone()))); + // mid_limbs_set is a bit. + eval.add_constraint( + (mid_limbs_set_col5.clone() * (mid_limbs_set_col5.clone() - M31_1.clone())), + ); + // Cannot have msb equals 0 and mid_limbs_set equals 1. + eval.add_constraint( + ((M31_1.clone() * mid_limbs_set_col5.clone()) * (msb_col4.clone() - M31_1.clone())), + ); + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryidtobig_lookup_elements, + E::EF::one(), + &[ + op1_id_col3.clone(), + op1_limb_0_col6.clone(), + op1_limb_1_col7.clone(), + op1_limb_2_col8.clone(), + (mid_limbs_set_col5.clone() * M31_511.clone()), + (mid_limbs_set_col5.clone() * M31_511.clone()), + (mid_limbs_set_col5.clone() * M31_511.clone()), + (mid_limbs_set_col5.clone() * M31_511.clone()), + (mid_limbs_set_col5.clone() * M31_511.clone()), + (mid_limbs_set_col5.clone() * M31_511.clone()), + (mid_limbs_set_col5.clone() * M31_511.clone()), + (mid_limbs_set_col5.clone() * M31_511.clone()), + (mid_limbs_set_col5.clone() * M31_511.clone()), + (mid_limbs_set_col5.clone() * M31_511.clone()), + (mid_limbs_set_col5.clone() * M31_511.clone()), + (mid_limbs_set_col5.clone() * M31_511.clone()), + (mid_limbs_set_col5.clone() * M31_511.clone()), + (mid_limbs_set_col5.clone() * M31_511.clone()), + (mid_limbs_set_col5.clone() * M31_511.clone()), + (mid_limbs_set_col5.clone() * M31_511.clone()), + (mid_limbs_set_col5.clone() * M31_511.clone()), + (mid_limbs_set_col5.clone() * M31_511.clone()), + ((M31_136.clone() * msb_col4.clone()) - mid_limbs_set_col5.clone()), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + (msb_col4.clone() * M31_256.clone()), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.opcodes_lookup_elements, + E::EF::one(), + &[ + input_pc_col0.clone(), + input_ap_col1.clone(), + input_fp_col2.clone(), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.opcodes_lookup_elements, + -E::EF::one(), + &[ + (input_pc_col0.clone() + M31_2.clone()), + (input_ap_col1.clone() + + ((((op1_limb_0_col6.clone() + + (op1_limb_1_col7.clone() * M31_512.clone())) + + (op1_limb_2_col8.clone() * M31_262144.clone())) + - msb_col4.clone()) + - (M31_134217728.clone() * mid_limbs_set_col5.clone()))), + input_fp_col2.clone(), + ], + )]); + + eval.finalize_logup(); + eval + } +} diff --git a/stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_t_op1_base_fp_f/mod.rs b/stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_t_op1_base_fp_f/mod.rs new file mode 100644 index 00000000..3f7a8d74 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_t_op1_base_fp_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_ap_opcode_is_imm_t_op1_base_fp_f/prover.rs b/stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_t_op1_base_fp_f/prover.rs new file mode 100644 index 00000000..b20dc6c8 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_t_op1_base_fp_f/prover.rs @@ -0,0 +1,393 @@ +#![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 = 9; + +#[derive(Default)] +pub struct ClaimGenerator { + pub inputs: Vec, +} +impl ClaimGenerator { + pub fn new(inputs: Vec) -> Self { + Self { inputs } + } + + pub fn write_trace( + mut self, + tree_builder: &mut TreeBuilder<'_, '_, SimdBackend, Blake2sMerkleChannel>, + memory_address_to_id_state: &mut memory_address_to_id::ClaimGenerator, + memory_id_to_big_state: &mut memory_id_to_big::ClaimGenerator, + verify_instruction_state: &mut verify_instruction::ClaimGenerator, + ) -> (Claim, InteractionClaimGenerator) { + let n_calls = self.inputs.len(); + assert_ne!(n_calls, 0); + let size = std::cmp::max(n_calls.next_power_of_two(), N_LANES); + let need_padding = n_calls != size; + + if need_padding { + self.inputs.resize(size, *self.inputs.first().unwrap()); + bit_reverse_coset_to_circle_domain_order(&mut self.inputs); + } + + let packed_inputs = pack_values(&self.inputs); + let (trace, mut sub_components_inputs, lookup_data) = write_trace_simd( + packed_inputs, + memory_address_to_id_state, + memory_id_to_big_state, + ); + + if need_padding { + sub_components_inputs.bit_reverse_coset_to_circle_domain_order(); + } + sub_components_inputs + .memory_address_to_id_inputs + .iter() + .for_each(|inputs| { + memory_address_to_id_state.add_inputs(&inputs[..n_calls]); + }); + sub_components_inputs + .memory_id_to_big_inputs + .iter() + .for_each(|inputs| { + memory_id_to_big_state.add_inputs(&inputs[..n_calls]); + }); + sub_components_inputs + .verify_instruction_inputs + .iter() + .for_each(|inputs| { + verify_instruction_state.add_inputs(&inputs[..n_calls]); + }); + + tree_builder.extend_evals( + trace + .into_iter() + .map(|eval| { + let domain = CanonicCoset::new( + eval.len() + .checked_ilog2() + .expect("Input is not a power of 2!"), + ) + .circle_domain(); + CircleEvaluation::::new(domain, eval) + }) + .collect_vec(), + ); + + ( + Claim { n_calls }, + InteractionClaimGenerator { + n_calls, + lookup_data, + }, + ) + } + + pub fn add_inputs(&mut self, inputs: &[InputType]) { + self.inputs.extend(inputs); + } +} + +pub struct SubComponentInputs { + pub memory_address_to_id_inputs: [Vec; 1], + pub memory_id_to_big_inputs: [Vec; 1], + pub verify_instruction_inputs: [Vec; 1], +} +impl SubComponentInputs { + #[allow(unused_variables)] + fn with_capacity(capacity: usize) -> Self { + Self { + memory_address_to_id_inputs: [Vec::with_capacity(capacity)], + memory_id_to_big_inputs: [Vec::with_capacity(capacity)], + verify_instruction_inputs: [Vec::with_capacity(capacity)], + } + } + + fn bit_reverse_coset_to_circle_domain_order(&mut self) { + self.memory_address_to_id_inputs + .iter_mut() + .for_each(|vec| bit_reverse_coset_to_circle_domain_order(vec)); + self.memory_id_to_big_inputs + .iter_mut() + .for_each(|vec| bit_reverse_coset_to_circle_domain_order(vec)); + self.verify_instruction_inputs + .iter_mut() + .for_each(|vec| bit_reverse_coset_to_circle_domain_order(vec)); + } +} + +#[allow(clippy::useless_conversion)] +#[allow(unused_variables)] +#[allow(clippy::double_parens)] +#[allow(non_snake_case)] +pub fn write_trace_simd( + inputs: Vec, + memory_address_to_id_state: &mut memory_address_to_id::ClaimGenerator, + memory_id_to_big_state: &mut memory_id_to_big::ClaimGenerator, +) -> ( + [BaseColumn; N_TRACE_COLUMNS], + SubComponentInputs, + LookupData, +) { + const N_TRACE_COLUMNS: usize = 9; + let mut trace: [_; N_TRACE_COLUMNS] = + std::array::from_fn(|_| Col::::zeros(inputs.len() * N_LANES)); + + let mut lookup_data = LookupData::with_capacity(inputs.len()); + #[allow(unused_mut)] + let mut sub_components_inputs = SubComponentInputs::with_capacity(inputs.len()); + + let M31_0 = PackedM31::broadcast(M31::from(0)); + let M31_1 = PackedM31::broadcast(M31::from(1)); + let M31_134217728 = PackedM31::broadcast(M31::from(134217728)); + let M31_136 = PackedM31::broadcast(M31::from(136)); + let M31_2 = PackedM31::broadcast(M31::from(2)); + let M31_256 = PackedM31::broadcast(M31::from(256)); + let M31_262144 = PackedM31::broadcast(M31::from(262144)); + let M31_32767 = PackedM31::broadcast(M31::from(32767)); + let M31_32769 = PackedM31::broadcast(M31::from(32769)); + let M31_511 = PackedM31::broadcast(M31::from(511)); + let M31_512 = PackedM31::broadcast(M31::from(512)); + + inputs.into_iter().enumerate().for_each( + |(row_index, add_ap_opcode_is_imm_t_op1_base_fp_f_input)| { + let input_tmp_933 = add_ap_opcode_is_imm_t_op1_base_fp_f_input; + let input_pc_col0 = input_tmp_933.pc; + trace[0].data[row_index] = input_pc_col0; + let input_ap_col1 = input_tmp_933.ap; + trace[1].data[row_index] = input_ap_col1; + let input_fp_col2 = input_tmp_933.fp; + trace[2].data[row_index] = input_fp_col2; + + // decode_instruction_a14b71db698d77c8. + + let memory_address_to_id_value_tmp_937 = + memory_address_to_id_state.deduce_output(input_pc_col0); + let memory_id_to_big_value_tmp_938 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_937); + + sub_components_inputs.verify_instruction_inputs[0].extend( + ( + input_pc_col0, + [M31_32767, M31_32767, M31_32769], + [ + M31_1, M31_1, M31_1, M31_0, M31_0, M31_0, M31_0, M31_0, M31_0, M31_0, + M31_1, M31_0, M31_0, M31_0, M31_0, + ], + ) + .unpack(), + ); + + lookup_data.verifyinstruction[0].push([ + input_pc_col0, + M31_32767, + M31_32767, + M31_32769, + M31_1, + M31_1, + M31_1, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_1, + M31_0, + M31_0, + M31_0, + M31_0, + ]); + + // read_small. + + let memory_address_to_id_value_tmp_940 = + memory_address_to_id_state.deduce_output(((input_pc_col0) + (M31_1))); + let memory_id_to_big_value_tmp_941 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_940); + let op1_id_col3 = memory_address_to_id_value_tmp_940; + trace[3].data[row_index] = op1_id_col3; + sub_components_inputs.memory_address_to_id_inputs[0] + .extend(((input_pc_col0) + (M31_1)).unpack()); + + lookup_data.memoryaddresstoid[0].push([((input_pc_col0) + (M31_1)), op1_id_col3]); + + // cond_decode_small_sign. + + let msb_tmp_942 = memory_id_to_big_value_tmp_941.get_m31(27).eq(M31_256); + let msb_col4 = msb_tmp_942.as_m31(); + trace[4].data[row_index] = msb_col4; + let mid_limbs_set_tmp_943 = memory_id_to_big_value_tmp_941.get_m31(20).eq(M31_511); + let mid_limbs_set_col5 = mid_limbs_set_tmp_943.as_m31(); + trace[5].data[row_index] = mid_limbs_set_col5; + + let op1_limb_0_col6 = memory_id_to_big_value_tmp_941.get_m31(0); + trace[6].data[row_index] = op1_limb_0_col6; + let op1_limb_1_col7 = memory_id_to_big_value_tmp_941.get_m31(1); + trace[7].data[row_index] = op1_limb_1_col7; + let op1_limb_2_col8 = memory_id_to_big_value_tmp_941.get_m31(2); + trace[8].data[row_index] = op1_limb_2_col8; + sub_components_inputs.memory_id_to_big_inputs[0].extend(op1_id_col3.unpack()); + + lookup_data.memoryidtobig[0].push([ + op1_id_col3, + op1_limb_0_col6, + op1_limb_1_col7, + op1_limb_2_col8, + ((mid_limbs_set_col5) * (M31_511)), + ((mid_limbs_set_col5) * (M31_511)), + ((mid_limbs_set_col5) * (M31_511)), + ((mid_limbs_set_col5) * (M31_511)), + ((mid_limbs_set_col5) * (M31_511)), + ((mid_limbs_set_col5) * (M31_511)), + ((mid_limbs_set_col5) * (M31_511)), + ((mid_limbs_set_col5) * (M31_511)), + ((mid_limbs_set_col5) * (M31_511)), + ((mid_limbs_set_col5) * (M31_511)), + ((mid_limbs_set_col5) * (M31_511)), + ((mid_limbs_set_col5) * (M31_511)), + ((mid_limbs_set_col5) * (M31_511)), + ((mid_limbs_set_col5) * (M31_511)), + ((mid_limbs_set_col5) * (M31_511)), + ((mid_limbs_set_col5) * (M31_511)), + ((mid_limbs_set_col5) * (M31_511)), + ((mid_limbs_set_col5) * (M31_511)), + (((M31_136) * (msb_col4)) - (mid_limbs_set_col5)), + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + ((msb_col4) * (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) + + (((((op1_limb_0_col6) + ((op1_limb_1_col7) * (M31_512))) + + ((op1_limb_2_col8) * (M31_262144))) + - (msb_col4)) + - ((M31_134217728) * (mid_limbs_set_col5)))), + input_fp_col2, + ]); + }, + ); + + (trace, sub_components_inputs, lookup_data) +} + +pub struct LookupData { + pub memoryaddresstoid: [Vec<[PackedM31; 2]>; 1], + pub memoryidtobig: [Vec<[PackedM31; 29]>; 1], + pub opcodes: [Vec<[PackedM31; 3]>; 2], + pub verifyinstruction: [Vec<[PackedM31; 19]>; 1], +} +impl LookupData { + #[allow(unused_variables)] + fn with_capacity(capacity: usize) -> Self { + Self { + memoryaddresstoid: [Vec::with_capacity(capacity)], + memoryidtobig: [Vec::with_capacity(capacity)], + opcodes: [Vec::with_capacity(capacity), Vec::with_capacity(capacity)], + verifyinstruction: [Vec::with_capacity(capacity)], + } + } +} + +pub struct InteractionClaimGenerator { + pub n_calls: usize, + pub lookup_data: LookupData, +} +impl InteractionClaimGenerator { + pub fn write_interaction_trace( + self, + tree_builder: &mut TreeBuilder<'_, '_, SimdBackend, Blake2sMerkleChannel>, + memoryaddresstoid_lookup_elements: &relations::MemoryAddressToId, + memoryidtobig_lookup_elements: &relations::MemoryIdToBig, + opcodes_lookup_elements: &relations::Opcodes, + verifyinstruction_lookup_elements: &relations::VerifyInstruction, + ) -> InteractionClaim { + let log_size = std::cmp::max(self.n_calls.next_power_of_two().ilog2(), LOG_N_LANES); + let mut logup_gen = LogupTraceGenerator::new(log_size); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.verifyinstruction[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = verifyinstruction_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.memoryaddresstoid[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = memoryaddresstoid_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.memoryidtobig[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = memoryidtobig_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.opcodes[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = opcodes_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.opcodes[1]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = opcodes_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, -PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let (trace, total_sum, claimed_sum) = if self.n_calls == 1 << log_size { + let (trace, claimed_sum) = logup_gen.finalize_last(); + (trace, claimed_sum, None) + } else { + let (trace, [total_sum, claimed_sum]) = + logup_gen.finalize_at([(1 << log_size) - 1, self.n_calls - 1]); + (trace, total_sum, Some((claimed_sum, self.n_calls - 1))) + }; + tree_builder.extend_evals(trace); + + InteractionClaim { + logup_sums: (total_sum, claimed_sum), + } + } +} diff --git a/stwo_cairo_prover/crates/prover/src/components/generic_opcode/prover.rs b/stwo_cairo_prover/crates/prover/src/components/generic_opcode/prover.rs index a2de5857..7c1a9e78 100644 --- a/stwo_cairo_prover/crates/prover/src/components/generic_opcode/prover.rs +++ b/stwo_cairo_prover/crates/prover/src/components/generic_opcode/prover.rs @@ -1351,7 +1351,7 @@ impl InteractionClaimGenerator { &relations::RangeCheck_19, rangecheck_9_9_lookup_elements: &relations::RangeCheck_9_9, - verifyinstruction_lookup_elements: + verify_instruction_lookup_elements: &relations::VerifyInstruction, ) -> InteractionClaim { let log_size = std::cmp::max(self.n_calls.next_power_of_two().ilog2(), LOG_N_LANES); @@ -1362,7 +1362,7 @@ impl InteractionClaimGenerator { .verifyinstruction[0]; for (i, lookup_values) in lookup_row.iter().enumerate() { let denom = - verifyinstruction_lookup_elements.combine(lookup_values); + verify_instruction_lookup_elements.combine(lookup_values); col_gen.write_frac(i, PackedQM31::one(), denom); } col_gen.finalize_col(); diff --git a/stwo_cairo_prover/crates/prover/src/components/mod.rs b/stwo_cairo_prover/crates/prover/src/components/mod.rs index a3378b2e..f327a788 100644 --- a/stwo_cairo_prover/crates/prover/src/components/mod.rs +++ b/stwo_cairo_prover/crates/prover/src/components/mod.rs @@ -1,6 +1,9 @@ use prover_types::simd::N_LANES; 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 generic_opcode; pub mod memory; pub mod range_check_vector; 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 8ae23133..53cf1039 100644 --- a/stwo_cairo_prover/crates/prover/src/input/state_transitions.rs +++ b/stwo_cairo_prover/crates/prover/src/input/state_transitions.rs @@ -200,35 +200,6 @@ impl StateTransitions { let CasmState { ap, fp, pc } = state; let instruction = mem.get_inst(pc.0); let instruction = Instruction::decode(instruction); - if dev_mode { - if let Instruction { - offset0: -2, - offset1: -1, - offset2: -1, - dst_base_fp: true, - op0_base_fp: true, - op1_imm: false, - op1_base_fp: true, - op1_base_ap: false, - res_add: false, - res_mul: false, - pc_update_jump: true, - pc_update_jump_rel: false, - pc_update_jnz: false, - ap_update_add: false, - ap_update_add_1: false, - opcode_call: false, - opcode_ret: true, - opcode_assert_eq: false, - } = instruction - { - self.casm_states_by_opcode.ret_opcode.push(state); - } else { - self.casm_states_by_opcode.generic_opcode.push(state); - } - - return; - } match instruction { // ret. @@ -314,7 +285,7 @@ impl StateTransitions { opcode_call: false, opcode_ret: false, opcode_assert_eq: false, - } => { + } if !dev_mode => { if op1_imm { // jump rel imm. assert!( @@ -380,7 +351,7 @@ impl StateTransitions { opcode_call: true, opcode_ret: false, opcode_assert_eq: false, - } => { + } if !dev_mode => { if pc_update_jump_rel { // call rel imm. assert!( @@ -424,7 +395,7 @@ impl StateTransitions { opcode_call: false, opcode_ret: false, opcode_assert_eq: false, - } => { + } if !dev_mode => { let dst_addr = if dst_base_fp { fp } else { ap }; let dst = mem.get(dst_addr.0.checked_add_signed(offset0 as i32).unwrap()); let taken = dst != MemoryValue::Small(0); @@ -473,7 +444,7 @@ impl StateTransitions { opcode_call: false, opcode_ret: false, opcode_assert_eq: true, - } => { + } if !dev_mode => { if op1_imm { // [ap/fp + offset0] = imm. assert!( @@ -520,7 +491,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 { @@ -576,7 +547,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 {