From a01a3a8bb53d086a419e04841c80dae11a38cb10 Mon Sep 17 00:00:00 2001 From: Ohad Agadi Date: Sun, 1 Dec 2024 12:39:04 +0200 Subject: [PATCH] jnz gen --- .../prover/src/cairo_air/opcodes_air.rs | 357 +++++++++- .../component.rs | 246 +++++++ .../mod.rs | 5 + .../prover.rs | 462 +++++++++++++ .../component.rs | 246 +++++++ .../mod.rs | 5 + .../prover.rs | 462 +++++++++++++ .../component.rs | 365 +++++++++++ .../mod.rs | 5 + .../prover.rs | 619 ++++++++++++++++++ .../component.rs | 365 +++++++++++ .../mod.rs | 5 + .../prover.rs | 619 ++++++++++++++++++ .../crates/prover/src/components/mod.rs | 4 + .../prover/src/input/state_transitions.rs | 2 +- 15 files changed, 3761 insertions(+), 6 deletions(-) create mode 100644 stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_f_dst_base_fp_f/component.rs create mode 100644 stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_f_dst_base_fp_f/mod.rs create mode 100644 stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_f_dst_base_fp_f/prover.rs create mode 100644 stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_f_dst_base_fp_t/component.rs create mode 100644 stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_f_dst_base_fp_t/mod.rs create mode 100644 stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_f_dst_base_fp_t/prover.rs create mode 100644 stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_t_dst_base_fp_f/component.rs create mode 100644 stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_t_dst_base_fp_f/mod.rs create mode 100644 stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_t_dst_base_fp_f/prover.rs create mode 100644 stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_t_dst_base_fp_t/component.rs create mode 100644 stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_t_dst_base_fp_t/mod.rs create mode 100644 stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_t_dst_base_fp_t/prover.rs 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 09dab0d2..9136b569 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,8 +12,10 @@ 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, generic_opcode, memory_address_to_id, memory_id_to_big, - range_check_19, range_check_9_9, ret_opcode, verify_instruction, + add_ap_opcode_is_imm_t_op1_base_fp_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, range_check_19, + range_check_9_9, ret_opcode, verify_instruction, }; use crate::input::state_transitions::StateTransitions; @@ -22,16 +24,24 @@ pub struct OpcodeClaim { add_ap_f_f: Vec, add_ap_f_t: Vec, add_ap_t_f: Vec, - ret: Vec, generic: Vec, + jnz_f_f: Vec, + jnz_f_t: Vec, + jnz_t_f: Vec, + jnz_t_t: Vec, + ret: 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)); + self.jnz_f_f.iter().for_each(|c| c.mix_into(channel)); + self.jnz_f_t.iter().for_each(|c| c.mix_into(channel)); + self.jnz_t_f.iter().for_each(|c| c.mix_into(channel)); + self.jnz_t_t.iter().for_each(|c| c.mix_into(channel)); + self.ret.iter().for_each(|c| c.mix_into(channel)); } pub fn log_sizes(&self) -> TreeVec> { @@ -40,6 +50,10 @@ impl OpcodeClaim { 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.jnz_f_f.iter().map(|c| c.log_sizes()), + self.jnz_f_t.iter().map(|c| c.log_sizes()), + self.jnz_t_f.iter().map(|c| c.log_sizes()), + self.jnz_t_t.iter().map(|c| c.log_sizes()), self.ret.iter().map(|c| c.log_sizes()), )) } @@ -50,6 +64,10 @@ pub struct OpcodesClaimGenerator { add_ap_f_t: Vec, add_ap_t_f: Vec, generic: Vec, + jnz_f_f: Vec, + jnz_f_t: Vec, + jnz_t_f: Vec, + jnz_t_t: Vec, ret: Vec, } impl OpcodesClaimGenerator { @@ -59,6 +77,10 @@ impl OpcodesClaimGenerator { let mut add_ap_f_t = vec![]; let mut add_ap_t_f = vec![]; let mut generic = vec![]; + let mut jnz_f_f = vec![]; + let mut jnz_f_t = vec![]; + let mut jnz_t_f = vec![]; + let mut jnz_t_t = vec![]; let mut ret = vec![]; if !input .casm_states_by_opcode @@ -93,6 +115,50 @@ impl OpcodesClaimGenerator { .add_ap_opcode_is_imm_t_op1_base_fp_f, )); } + if !input + .casm_states_by_opcode + .jnz_opcode_is_taken_f_dst_base_fp_f + .is_empty() + { + jnz_f_f.push(jnz_opcode_is_taken_f_dst_base_fp_f::ClaimGenerator::new( + input + .casm_states_by_opcode + .jnz_opcode_is_taken_f_dst_base_fp_f, + )); + } + if !input + .casm_states_by_opcode + .jnz_opcode_is_taken_f_dst_base_fp_t + .is_empty() + { + jnz_f_t.push(jnz_opcode_is_taken_f_dst_base_fp_t::ClaimGenerator::new( + input + .casm_states_by_opcode + .jnz_opcode_is_taken_f_dst_base_fp_t, + )); + } + if !input + .casm_states_by_opcode + .jnz_opcode_is_taken_t_dst_base_fp_f + .is_empty() + { + jnz_t_f.push(jnz_opcode_is_taken_t_dst_base_fp_f::ClaimGenerator::new( + input + .casm_states_by_opcode + .jnz_opcode_is_taken_t_dst_base_fp_f, + )); + } + if !input + .casm_states_by_opcode + .jnz_opcode_is_taken_t_dst_base_fp_t + .is_empty() + { + jnz_t_t.push(jnz_opcode_is_taken_t_dst_base_fp_t::ClaimGenerator::new( + input + .casm_states_by_opcode + .jnz_opcode_is_taken_t_dst_base_fp_t, + )); + } if !input.casm_states_by_opcode.generic_opcode.is_empty() { generic.push(generic_opcode::ClaimGenerator::new( input.casm_states_by_opcode.generic_opcode, @@ -107,8 +173,12 @@ impl OpcodesClaimGenerator { add_ap_f_f, add_ap_f_t, add_ap_t_f, - ret, generic, + jnz_f_f, + jnz_f_t, + jnz_t_f, + jnz_t_t, + ret, } } @@ -171,6 +241,55 @@ impl OpcodesClaimGenerator { ) }) .unzip(); + let (jnz_f_f_claims, jnz_f_f_interaction_gens) = self + .jnz_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 (jnz_f_t_claims, jnz_f_t_interaction_gens) = self + .jnz_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 (jnz_t_f_claims, jnz_t_f_interaction_gens) = self + .jnz_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 (jnz_t_t_claims, jnz_t_t_interaction_gens) = self + .jnz_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 (ret_claims, ret_interaction_gens) = self .ret .into_iter() @@ -189,6 +308,10 @@ impl OpcodesClaimGenerator { add_ap_f_t: add_ap_f_t_claims, add_ap_t_f: add_ap_t_f_claims, generic: generic_opcode_claims, + jnz_f_f: jnz_f_f_claims, + jnz_f_t: jnz_f_t_claims, + jnz_t_f: jnz_t_f_claims, + jnz_t_t: jnz_t_t_claims, ret: ret_claims, }, OpcodesInteractionClaimGenerator { @@ -196,6 +319,10 @@ impl OpcodesClaimGenerator { add_ap_f_t: add_ap_f_t_interaction_gens, add_ap_t_f: add_ap_t_f_interaction_gens, generic_opcode_interaction_gens, + jnz_f_f: jnz_f_f_interaction_gens, + jnz_f_t: jnz_f_t_interaction_gens, + jnz_t_f: jnz_t_f_interaction_gens, + jnz_t_t: jnz_t_t_interaction_gens, ret_interaction_gens, }, ) @@ -208,6 +335,10 @@ pub struct OpcodeInteractionClaim { add_ap_f_t: Vec, add_ap_t_f: Vec, generic: Vec, + jnz_f_f: Vec, + jnz_f_t: Vec, + jnz_t_f: Vec, + jnz_t_t: Vec, ret: Vec, } impl OpcodeInteractionClaim { @@ -216,6 +347,10 @@ impl OpcodeInteractionClaim { 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.jnz_f_f.iter().for_each(|c| c.mix_into(channel)); + self.jnz_f_t.iter().for_each(|c| c.mix_into(channel)); + self.jnz_t_f.iter().for_each(|c| c.mix_into(channel)); + self.jnz_t_t.iter().for_each(|c| c.mix_into(channel)); self.ret.iter().for_each(|c| c.mix_into(channel)); } @@ -249,6 +384,34 @@ impl OpcodeInteractionClaim { None => total_sum, }; } + for interaction_claim in &self.jnz_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.jnz_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.jnz_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.jnz_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.ret { let (total_sum, claimed_sum) = interaction_claim.logup_sums; sum += match claimed_sum { @@ -265,6 +428,10 @@ pub struct OpcodesInteractionClaimGenerator { add_ap_f_t: Vec, add_ap_t_f: Vec, generic_opcode_interaction_gens: Vec, + jnz_f_f: Vec, + jnz_f_t: Vec, + jnz_t_f: Vec, + jnz_t_t: Vec, ret_interaction_gens: Vec, } impl OpcodesInteractionClaimGenerator { @@ -327,6 +494,58 @@ impl OpcodesInteractionClaimGenerator { ) }) .collect(); + let jnz_f_f_interaction_claims = self + .jnz_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 jnz_f_t_interaction_claims = self + .jnz_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 jnz_t_f_interaction_claims = self + .jnz_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 jnz_t_t_interaction_claims = self + .jnz_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 ret_interaction_claims = self .ret_interaction_gens .into_iter() @@ -345,6 +564,10 @@ impl OpcodesInteractionClaimGenerator { 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, + jnz_f_f: jnz_f_f_interaction_claims, + jnz_f_t: jnz_f_t_interaction_claims, + jnz_t_f: jnz_t_f_interaction_claims, + jnz_t_t: jnz_t_t_interaction_claims, ret: ret_interaction_claims, } } @@ -355,6 +578,10 @@ pub struct OpcodeComponents { add_ap_f_t: Vec, add_ap_t_f: Vec, generic: Vec, + jnz_f_f: Vec, + jnz_f_t: Vec, + jnz_t_f: Vec, + jnz_t_t: Vec, ret: Vec, } impl OpcodeComponents { @@ -464,6 +691,102 @@ impl OpcodeComponents { ) }) .collect_vec(); + let jnz_f_f_components = claim + .jnz_f_f + .iter() + .zip(interaction_claim.jnz_f_f.iter()) + .map(|(&claim, &interaction_claim)| { + jnz_opcode_is_taken_f_dst_base_fp_f::Component::new( + tree_span_provider, + jnz_opcode_is_taken_f_dst_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 jnz_f_t_components = claim + .jnz_f_t + .iter() + .zip(interaction_claim.jnz_f_t.iter()) + .map(|(&claim, &interaction_claim)| { + jnz_opcode_is_taken_f_dst_base_fp_t::Component::new( + tree_span_provider, + jnz_opcode_is_taken_f_dst_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 jnz_t_f_components = claim + .jnz_t_f + .iter() + .zip(interaction_claim.jnz_t_f.iter()) + .map(|(&claim, &interaction_claim)| { + jnz_opcode_is_taken_t_dst_base_fp_f::Component::new( + tree_span_provider, + jnz_opcode_is_taken_t_dst_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 jnz_t_t_components = claim + .jnz_t_t + .iter() + .zip(interaction_claim.jnz_t_t.iter()) + .map(|(&claim, &interaction_claim)| { + jnz_opcode_is_taken_t_dst_base_fp_t::Component::new( + tree_span_provider, + jnz_opcode_is_taken_t_dst_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 ret_components = claim .ret .iter() @@ -493,6 +816,10 @@ impl OpcodeComponents { add_ap_f_t: add_ap_f_t_components, add_ap_t_f: add_ap_t_f_components, generic: generic_components, + jnz_f_f: jnz_f_f_components, + jnz_f_t: jnz_f_t_components, + jnz_t_f: jnz_t_f_components, + jnz_t_t: jnz_t_t_components, ret: ret_components, } } @@ -519,6 +846,26 @@ impl OpcodeComponents { .iter() .map(|component| component as &dyn ComponentProver), ); + vec.extend( + self.jnz_f_f + .iter() + .map(|component| component as &dyn ComponentProver), + ); + vec.extend( + self.jnz_f_t + .iter() + .map(|component| component as &dyn ComponentProver), + ); + vec.extend( + self.jnz_t_f + .iter() + .map(|component| component as &dyn ComponentProver), + ); + vec.extend( + self.jnz_t_t + .iter() + .map(|component| component as &dyn ComponentProver), + ); vec.extend( self.ret .iter() diff --git a/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_f_dst_base_fp_f/component.rs b/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_f_dst_base_fp_f/component.rs new file mode 100644 index 00000000..cd2e4291 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_f_dst_base_fp_f/component.rs @@ -0,0 +1,246 @@ +#![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; 34]; + 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_2 = E::F::from(M31::from(2)); + let M31_32767 = E::F::from(M31::from(32767)); + let M31_32768 = E::F::from(M31::from(32768)); + let M31_32769 = E::F::from(M31::from(32769)); + 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 ap_update_add_1_col4 = eval.next_trace_mask(); + let dst_id_col5 = eval.next_trace_mask(); + let dst_limb_0_col6 = eval.next_trace_mask(); + let dst_limb_1_col7 = eval.next_trace_mask(); + let dst_limb_2_col8 = eval.next_trace_mask(); + let dst_limb_3_col9 = eval.next_trace_mask(); + let dst_limb_4_col10 = eval.next_trace_mask(); + let dst_limb_5_col11 = eval.next_trace_mask(); + let dst_limb_6_col12 = eval.next_trace_mask(); + let dst_limb_7_col13 = eval.next_trace_mask(); + let dst_limb_8_col14 = eval.next_trace_mask(); + let dst_limb_9_col15 = eval.next_trace_mask(); + let dst_limb_10_col16 = eval.next_trace_mask(); + let dst_limb_11_col17 = eval.next_trace_mask(); + let dst_limb_12_col18 = eval.next_trace_mask(); + let dst_limb_13_col19 = eval.next_trace_mask(); + let dst_limb_14_col20 = eval.next_trace_mask(); + let dst_limb_15_col21 = eval.next_trace_mask(); + let dst_limb_16_col22 = eval.next_trace_mask(); + let dst_limb_17_col23 = eval.next_trace_mask(); + let dst_limb_18_col24 = eval.next_trace_mask(); + let dst_limb_19_col25 = eval.next_trace_mask(); + let dst_limb_20_col26 = eval.next_trace_mask(); + let dst_limb_21_col27 = eval.next_trace_mask(); + let dst_limb_22_col28 = eval.next_trace_mask(); + let dst_limb_23_col29 = eval.next_trace_mask(); + let dst_limb_24_col30 = eval.next_trace_mask(); + let dst_limb_25_col31 = eval.next_trace_mask(); + let dst_limb_26_col32 = eval.next_trace_mask(); + let dst_limb_27_col33 = eval.next_trace_mask(); + + // decode_instruction_d2b4cd588a3e2a7b. + + eval.add_to_relation(&[RelationEntry::new( + &self.verifyinstruction_lookup_elements, + E::EF::one(), + &[ + input_pc_col0.clone(), + offset0_col3.clone(), + M31_32767.clone(), + M31_32769.clone(), + M31_0.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_1.clone(), + M31_0.clone(), + ap_update_add_1_col4.clone(), + ], + )]); + + // read_positive_num_bits_252. + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryaddresstoid_lookup_elements, + E::EF::one(), + &[ + (input_ap_col1.clone() + (offset0_col3.clone() - M31_32768.clone())), + dst_id_col5.clone(), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryidtobig_lookup_elements, + E::EF::one(), + &[ + dst_id_col5.clone(), + dst_limb_0_col6.clone(), + dst_limb_1_col7.clone(), + dst_limb_2_col8.clone(), + dst_limb_3_col9.clone(), + dst_limb_4_col10.clone(), + dst_limb_5_col11.clone(), + dst_limb_6_col12.clone(), + dst_limb_7_col13.clone(), + dst_limb_8_col14.clone(), + dst_limb_9_col15.clone(), + dst_limb_10_col16.clone(), + dst_limb_11_col17.clone(), + dst_limb_12_col18.clone(), + dst_limb_13_col19.clone(), + dst_limb_14_col20.clone(), + dst_limb_15_col21.clone(), + dst_limb_16_col22.clone(), + dst_limb_17_col23.clone(), + dst_limb_18_col24.clone(), + dst_limb_19_col25.clone(), + dst_limb_20_col26.clone(), + dst_limb_21_col27.clone(), + dst_limb_22_col28.clone(), + dst_limb_23_col29.clone(), + dst_limb_24_col30.clone(), + dst_limb_25_col31.clone(), + dst_limb_26_col32.clone(), + dst_limb_27_col33.clone(), + ], + )]); + + // dst equals 0. + eval.add_constraint( + ((((((((((((((((((((((((((((M31_0.clone() + + dst_limb_0_col6.clone()) + + dst_limb_1_col7.clone()) + + dst_limb_2_col8.clone()) + + dst_limb_3_col9.clone()) + + dst_limb_4_col10.clone()) + + dst_limb_5_col11.clone()) + + dst_limb_6_col12.clone()) + + dst_limb_7_col13.clone()) + + dst_limb_8_col14.clone()) + + dst_limb_9_col15.clone()) + + dst_limb_10_col16.clone()) + + dst_limb_11_col17.clone()) + + dst_limb_12_col18.clone()) + + dst_limb_13_col19.clone()) + + dst_limb_14_col20.clone()) + + dst_limb_15_col21.clone()) + + dst_limb_16_col22.clone()) + + dst_limb_17_col23.clone()) + + dst_limb_18_col24.clone()) + + dst_limb_19_col25.clone()) + + dst_limb_20_col26.clone()) + + dst_limb_21_col27.clone()) + + dst_limb_22_col28.clone()) + + dst_limb_23_col29.clone()) + + dst_limb_24_col30.clone()) + + dst_limb_25_col31.clone()) + + dst_limb_26_col32.clone()) + + dst_limb_27_col33.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_col4.clone()), + input_fp_col2.clone(), + ], + )]); + + eval.finalize_logup(); + eval + } +} diff --git a/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_f_dst_base_fp_f/mod.rs b/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_f_dst_base_fp_f/mod.rs new file mode 100644 index 00000000..3f7a8d74 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_f_dst_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/jnz_opcode_is_taken_f_dst_base_fp_f/prover.rs b/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_f_dst_base_fp_f/prover.rs new file mode 100644 index 00000000..58cad706 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_f_dst_base_fp_f/prover.rs @@ -0,0 +1,462 @@ +#![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 = 34; + +#[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 = 34; + 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_32767 = PackedM31::broadcast(M31::from(32767)); + let M31_32768 = PackedM31::broadcast(M31::from(32768)); + let M31_32769 = PackedM31::broadcast(M31::from(32769)); + 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_3 = PackedUInt16::broadcast(UInt16::from(3)); + let UInt16_6 = PackedUInt16::broadcast(UInt16::from(6)); + let UInt16_9 = PackedUInt16::broadcast(UInt16::from(9)); + + inputs.into_iter().enumerate().for_each( + |(row_index, jnz_opcode_is_taken_f_dst_base_fp_f_input)| { + let input_tmp_1228 = jnz_opcode_is_taken_f_dst_base_fp_f_input; + let input_pc_col0 = input_tmp_1228.pc; + trace[0].data[row_index] = input_pc_col0; + let input_ap_col1 = input_tmp_1228.ap; + trace[1].data[row_index] = input_ap_col1; + let input_fp_col2 = input_tmp_1228.fp; + trace[2].data[row_index] = input_fp_col2; + + // decode_instruction_d2b4cd588a3e2a7b. + + let memory_address_to_id_value_tmp_1234 = + memory_address_to_id_state.deduce_output(input_pc_col0); + let memory_id_to_big_value_tmp_1235 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1234); + let offset0_tmp_1236 = + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1235.get_m31(0))) + + (((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1235.get_m31(1))) + & (UInt16_127)) + << (UInt16_9))); + let offset0_col3 = offset0_tmp_1236.as_m31(); + trace[3].data[row_index] = offset0_col3; + let ap_update_add_1_tmp_1237 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1235.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1235.get_m31(6))) + << (UInt16_6))) + >> (UInt16_11)) + & (UInt16_1)); + let ap_update_add_1_col4 = ap_update_add_1_tmp_1237.as_m31(); + trace[4].data[row_index] = ap_update_add_1_col4; + + sub_components_inputs.verify_instruction_inputs[0].extend( + ( + input_pc_col0, + [offset0_col3, M31_32767, M31_32769], + [ + M31_0, + M31_1, + M31_1, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_1, + M31_0, + ap_update_add_1_col4, + M31_0, + M31_0, + M31_0, + ], + ) + .unpack(), + ); + + lookup_data.verifyinstruction[0].push([ + input_pc_col0, + offset0_col3, + M31_32767, + M31_32769, + M31_0, + M31_1, + M31_1, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_1, + M31_0, + ap_update_add_1_col4, + M31_0, + M31_0, + M31_0, + ]); + + // read_positive_num_bits_252. + + let memory_address_to_id_value_tmp_1239 = memory_address_to_id_state + .deduce_output(((input_ap_col1) + ((offset0_col3) - (M31_32768)))); + let memory_id_to_big_value_tmp_1240 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1239); + let dst_id_col5 = memory_address_to_id_value_tmp_1239; + trace[5].data[row_index] = dst_id_col5; + sub_components_inputs.memory_address_to_id_inputs[0] + .extend(((input_ap_col1) + ((offset0_col3) - (M31_32768))).unpack()); + + lookup_data.memoryaddresstoid[0].push([ + ((input_ap_col1) + ((offset0_col3) - (M31_32768))), + dst_id_col5, + ]); + let dst_limb_0_col6 = memory_id_to_big_value_tmp_1240.get_m31(0); + trace[6].data[row_index] = dst_limb_0_col6; + let dst_limb_1_col7 = memory_id_to_big_value_tmp_1240.get_m31(1); + trace[7].data[row_index] = dst_limb_1_col7; + let dst_limb_2_col8 = memory_id_to_big_value_tmp_1240.get_m31(2); + trace[8].data[row_index] = dst_limb_2_col8; + let dst_limb_3_col9 = memory_id_to_big_value_tmp_1240.get_m31(3); + trace[9].data[row_index] = dst_limb_3_col9; + let dst_limb_4_col10 = memory_id_to_big_value_tmp_1240.get_m31(4); + trace[10].data[row_index] = dst_limb_4_col10; + let dst_limb_5_col11 = memory_id_to_big_value_tmp_1240.get_m31(5); + trace[11].data[row_index] = dst_limb_5_col11; + let dst_limb_6_col12 = memory_id_to_big_value_tmp_1240.get_m31(6); + trace[12].data[row_index] = dst_limb_6_col12; + let dst_limb_7_col13 = memory_id_to_big_value_tmp_1240.get_m31(7); + trace[13].data[row_index] = dst_limb_7_col13; + let dst_limb_8_col14 = memory_id_to_big_value_tmp_1240.get_m31(8); + trace[14].data[row_index] = dst_limb_8_col14; + let dst_limb_9_col15 = memory_id_to_big_value_tmp_1240.get_m31(9); + trace[15].data[row_index] = dst_limb_9_col15; + let dst_limb_10_col16 = memory_id_to_big_value_tmp_1240.get_m31(10); + trace[16].data[row_index] = dst_limb_10_col16; + let dst_limb_11_col17 = memory_id_to_big_value_tmp_1240.get_m31(11); + trace[17].data[row_index] = dst_limb_11_col17; + let dst_limb_12_col18 = memory_id_to_big_value_tmp_1240.get_m31(12); + trace[18].data[row_index] = dst_limb_12_col18; + let dst_limb_13_col19 = memory_id_to_big_value_tmp_1240.get_m31(13); + trace[19].data[row_index] = dst_limb_13_col19; + let dst_limb_14_col20 = memory_id_to_big_value_tmp_1240.get_m31(14); + trace[20].data[row_index] = dst_limb_14_col20; + let dst_limb_15_col21 = memory_id_to_big_value_tmp_1240.get_m31(15); + trace[21].data[row_index] = dst_limb_15_col21; + let dst_limb_16_col22 = memory_id_to_big_value_tmp_1240.get_m31(16); + trace[22].data[row_index] = dst_limb_16_col22; + let dst_limb_17_col23 = memory_id_to_big_value_tmp_1240.get_m31(17); + trace[23].data[row_index] = dst_limb_17_col23; + let dst_limb_18_col24 = memory_id_to_big_value_tmp_1240.get_m31(18); + trace[24].data[row_index] = dst_limb_18_col24; + let dst_limb_19_col25 = memory_id_to_big_value_tmp_1240.get_m31(19); + trace[25].data[row_index] = dst_limb_19_col25; + let dst_limb_20_col26 = memory_id_to_big_value_tmp_1240.get_m31(20); + trace[26].data[row_index] = dst_limb_20_col26; + let dst_limb_21_col27 = memory_id_to_big_value_tmp_1240.get_m31(21); + trace[27].data[row_index] = dst_limb_21_col27; + let dst_limb_22_col28 = memory_id_to_big_value_tmp_1240.get_m31(22); + trace[28].data[row_index] = dst_limb_22_col28; + let dst_limb_23_col29 = memory_id_to_big_value_tmp_1240.get_m31(23); + trace[29].data[row_index] = dst_limb_23_col29; + let dst_limb_24_col30 = memory_id_to_big_value_tmp_1240.get_m31(24); + trace[30].data[row_index] = dst_limb_24_col30; + let dst_limb_25_col31 = memory_id_to_big_value_tmp_1240.get_m31(25); + trace[31].data[row_index] = dst_limb_25_col31; + let dst_limb_26_col32 = memory_id_to_big_value_tmp_1240.get_m31(26); + trace[32].data[row_index] = dst_limb_26_col32; + let dst_limb_27_col33 = memory_id_to_big_value_tmp_1240.get_m31(27); + trace[33].data[row_index] = dst_limb_27_col33; + sub_components_inputs.memory_id_to_big_inputs[0].extend(dst_id_col5.unpack()); + + lookup_data.memoryidtobig[0].push([ + dst_id_col5, + dst_limb_0_col6, + dst_limb_1_col7, + dst_limb_2_col8, + dst_limb_3_col9, + dst_limb_4_col10, + dst_limb_5_col11, + dst_limb_6_col12, + dst_limb_7_col13, + dst_limb_8_col14, + dst_limb_9_col15, + dst_limb_10_col16, + dst_limb_11_col17, + dst_limb_12_col18, + dst_limb_13_col19, + dst_limb_14_col20, + dst_limb_15_col21, + dst_limb_16_col22, + dst_limb_17_col23, + dst_limb_18_col24, + dst_limb_19_col25, + dst_limb_20_col26, + dst_limb_21_col27, + dst_limb_22_col28, + dst_limb_23_col29, + dst_limb_24_col30, + dst_limb_25_col31, + dst_limb_26_col32, + dst_limb_27_col33, + ]); + + 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_col4)), + 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/jnz_opcode_is_taken_f_dst_base_fp_t/component.rs b/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_f_dst_base_fp_t/component.rs new file mode 100644 index 00000000..1507e81a --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_f_dst_base_fp_t/component.rs @@ -0,0 +1,246 @@ +#![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; 34]; + 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_2 = E::F::from(M31::from(2)); + let M31_32767 = E::F::from(M31::from(32767)); + let M31_32768 = E::F::from(M31::from(32768)); + let M31_32769 = E::F::from(M31::from(32769)); + 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 ap_update_add_1_col4 = eval.next_trace_mask(); + let dst_id_col5 = eval.next_trace_mask(); + let dst_limb_0_col6 = eval.next_trace_mask(); + let dst_limb_1_col7 = eval.next_trace_mask(); + let dst_limb_2_col8 = eval.next_trace_mask(); + let dst_limb_3_col9 = eval.next_trace_mask(); + let dst_limb_4_col10 = eval.next_trace_mask(); + let dst_limb_5_col11 = eval.next_trace_mask(); + let dst_limb_6_col12 = eval.next_trace_mask(); + let dst_limb_7_col13 = eval.next_trace_mask(); + let dst_limb_8_col14 = eval.next_trace_mask(); + let dst_limb_9_col15 = eval.next_trace_mask(); + let dst_limb_10_col16 = eval.next_trace_mask(); + let dst_limb_11_col17 = eval.next_trace_mask(); + let dst_limb_12_col18 = eval.next_trace_mask(); + let dst_limb_13_col19 = eval.next_trace_mask(); + let dst_limb_14_col20 = eval.next_trace_mask(); + let dst_limb_15_col21 = eval.next_trace_mask(); + let dst_limb_16_col22 = eval.next_trace_mask(); + let dst_limb_17_col23 = eval.next_trace_mask(); + let dst_limb_18_col24 = eval.next_trace_mask(); + let dst_limb_19_col25 = eval.next_trace_mask(); + let dst_limb_20_col26 = eval.next_trace_mask(); + let dst_limb_21_col27 = eval.next_trace_mask(); + let dst_limb_22_col28 = eval.next_trace_mask(); + let dst_limb_23_col29 = eval.next_trace_mask(); + let dst_limb_24_col30 = eval.next_trace_mask(); + let dst_limb_25_col31 = eval.next_trace_mask(); + let dst_limb_26_col32 = eval.next_trace_mask(); + let dst_limb_27_col33 = eval.next_trace_mask(); + + // decode_instruction_113648125c3c3f56. + + eval.add_to_relation(&[RelationEntry::new( + &self.verifyinstruction_lookup_elements, + E::EF::one(), + &[ + input_pc_col0.clone(), + offset0_col3.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_1.clone(), + M31_0.clone(), + ap_update_add_1_col4.clone(), + ], + )]); + + // read_positive_num_bits_252. + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryaddresstoid_lookup_elements, + E::EF::one(), + &[ + (input_fp_col2.clone() + (offset0_col3.clone() - M31_32768.clone())), + dst_id_col5.clone(), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryidtobig_lookup_elements, + E::EF::one(), + &[ + dst_id_col5.clone(), + dst_limb_0_col6.clone(), + dst_limb_1_col7.clone(), + dst_limb_2_col8.clone(), + dst_limb_3_col9.clone(), + dst_limb_4_col10.clone(), + dst_limb_5_col11.clone(), + dst_limb_6_col12.clone(), + dst_limb_7_col13.clone(), + dst_limb_8_col14.clone(), + dst_limb_9_col15.clone(), + dst_limb_10_col16.clone(), + dst_limb_11_col17.clone(), + dst_limb_12_col18.clone(), + dst_limb_13_col19.clone(), + dst_limb_14_col20.clone(), + dst_limb_15_col21.clone(), + dst_limb_16_col22.clone(), + dst_limb_17_col23.clone(), + dst_limb_18_col24.clone(), + dst_limb_19_col25.clone(), + dst_limb_20_col26.clone(), + dst_limb_21_col27.clone(), + dst_limb_22_col28.clone(), + dst_limb_23_col29.clone(), + dst_limb_24_col30.clone(), + dst_limb_25_col31.clone(), + dst_limb_26_col32.clone(), + dst_limb_27_col33.clone(), + ], + )]); + + // dst equals 0. + eval.add_constraint( + ((((((((((((((((((((((((((((M31_0.clone() + + dst_limb_0_col6.clone()) + + dst_limb_1_col7.clone()) + + dst_limb_2_col8.clone()) + + dst_limb_3_col9.clone()) + + dst_limb_4_col10.clone()) + + dst_limb_5_col11.clone()) + + dst_limb_6_col12.clone()) + + dst_limb_7_col13.clone()) + + dst_limb_8_col14.clone()) + + dst_limb_9_col15.clone()) + + dst_limb_10_col16.clone()) + + dst_limb_11_col17.clone()) + + dst_limb_12_col18.clone()) + + dst_limb_13_col19.clone()) + + dst_limb_14_col20.clone()) + + dst_limb_15_col21.clone()) + + dst_limb_16_col22.clone()) + + dst_limb_17_col23.clone()) + + dst_limb_18_col24.clone()) + + dst_limb_19_col25.clone()) + + dst_limb_20_col26.clone()) + + dst_limb_21_col27.clone()) + + dst_limb_22_col28.clone()) + + dst_limb_23_col29.clone()) + + dst_limb_24_col30.clone()) + + dst_limb_25_col31.clone()) + + dst_limb_26_col32.clone()) + + dst_limb_27_col33.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_col4.clone()), + input_fp_col2.clone(), + ], + )]); + + eval.finalize_logup(); + eval + } +} diff --git a/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_f_dst_base_fp_t/mod.rs b/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_f_dst_base_fp_t/mod.rs new file mode 100644 index 00000000..3f7a8d74 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_f_dst_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/jnz_opcode_is_taken_f_dst_base_fp_t/prover.rs b/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_f_dst_base_fp_t/prover.rs new file mode 100644 index 00000000..d85ab070 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_f_dst_base_fp_t/prover.rs @@ -0,0 +1,462 @@ +#![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 = 34; + +#[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 = 34; + 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_32767 = PackedM31::broadcast(M31::from(32767)); + let M31_32768 = PackedM31::broadcast(M31::from(32768)); + let M31_32769 = PackedM31::broadcast(M31::from(32769)); + 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_3 = PackedUInt16::broadcast(UInt16::from(3)); + let UInt16_6 = PackedUInt16::broadcast(UInt16::from(6)); + let UInt16_9 = PackedUInt16::broadcast(UInt16::from(9)); + + inputs.into_iter().enumerate().for_each( + |(row_index, jnz_opcode_is_taken_f_dst_base_fp_t_input)| { + let input_tmp_1256 = jnz_opcode_is_taken_f_dst_base_fp_t_input; + let input_pc_col0 = input_tmp_1256.pc; + trace[0].data[row_index] = input_pc_col0; + let input_ap_col1 = input_tmp_1256.ap; + trace[1].data[row_index] = input_ap_col1; + let input_fp_col2 = input_tmp_1256.fp; + trace[2].data[row_index] = input_fp_col2; + + // decode_instruction_113648125c3c3f56. + + let memory_address_to_id_value_tmp_1257 = + memory_address_to_id_state.deduce_output(input_pc_col0); + let memory_id_to_big_value_tmp_1258 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1257); + let offset0_tmp_1259 = + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1258.get_m31(0))) + + (((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1258.get_m31(1))) + & (UInt16_127)) + << (UInt16_9))); + let offset0_col3 = offset0_tmp_1259.as_m31(); + trace[3].data[row_index] = offset0_col3; + let ap_update_add_1_tmp_1260 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1258.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1258.get_m31(6))) + << (UInt16_6))) + >> (UInt16_11)) + & (UInt16_1)); + let ap_update_add_1_col4 = ap_update_add_1_tmp_1260.as_m31(); + trace[4].data[row_index] = ap_update_add_1_col4; + + sub_components_inputs.verify_instruction_inputs[0].extend( + ( + input_pc_col0, + [offset0_col3, M31_32767, M31_32769], + [ + M31_1, + M31_1, + M31_1, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_1, + M31_0, + ap_update_add_1_col4, + M31_0, + M31_0, + M31_0, + ], + ) + .unpack(), + ); + + lookup_data.verifyinstruction[0].push([ + input_pc_col0, + offset0_col3, + M31_32767, + M31_32769, + M31_1, + M31_1, + M31_1, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_1, + M31_0, + ap_update_add_1_col4, + M31_0, + M31_0, + M31_0, + ]); + + // read_positive_num_bits_252. + + let memory_address_to_id_value_tmp_1262 = memory_address_to_id_state + .deduce_output(((input_fp_col2) + ((offset0_col3) - (M31_32768)))); + let memory_id_to_big_value_tmp_1263 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1262); + let dst_id_col5 = memory_address_to_id_value_tmp_1262; + trace[5].data[row_index] = dst_id_col5; + sub_components_inputs.memory_address_to_id_inputs[0] + .extend(((input_fp_col2) + ((offset0_col3) - (M31_32768))).unpack()); + + lookup_data.memoryaddresstoid[0].push([ + ((input_fp_col2) + ((offset0_col3) - (M31_32768))), + dst_id_col5, + ]); + let dst_limb_0_col6 = memory_id_to_big_value_tmp_1263.get_m31(0); + trace[6].data[row_index] = dst_limb_0_col6; + let dst_limb_1_col7 = memory_id_to_big_value_tmp_1263.get_m31(1); + trace[7].data[row_index] = dst_limb_1_col7; + let dst_limb_2_col8 = memory_id_to_big_value_tmp_1263.get_m31(2); + trace[8].data[row_index] = dst_limb_2_col8; + let dst_limb_3_col9 = memory_id_to_big_value_tmp_1263.get_m31(3); + trace[9].data[row_index] = dst_limb_3_col9; + let dst_limb_4_col10 = memory_id_to_big_value_tmp_1263.get_m31(4); + trace[10].data[row_index] = dst_limb_4_col10; + let dst_limb_5_col11 = memory_id_to_big_value_tmp_1263.get_m31(5); + trace[11].data[row_index] = dst_limb_5_col11; + let dst_limb_6_col12 = memory_id_to_big_value_tmp_1263.get_m31(6); + trace[12].data[row_index] = dst_limb_6_col12; + let dst_limb_7_col13 = memory_id_to_big_value_tmp_1263.get_m31(7); + trace[13].data[row_index] = dst_limb_7_col13; + let dst_limb_8_col14 = memory_id_to_big_value_tmp_1263.get_m31(8); + trace[14].data[row_index] = dst_limb_8_col14; + let dst_limb_9_col15 = memory_id_to_big_value_tmp_1263.get_m31(9); + trace[15].data[row_index] = dst_limb_9_col15; + let dst_limb_10_col16 = memory_id_to_big_value_tmp_1263.get_m31(10); + trace[16].data[row_index] = dst_limb_10_col16; + let dst_limb_11_col17 = memory_id_to_big_value_tmp_1263.get_m31(11); + trace[17].data[row_index] = dst_limb_11_col17; + let dst_limb_12_col18 = memory_id_to_big_value_tmp_1263.get_m31(12); + trace[18].data[row_index] = dst_limb_12_col18; + let dst_limb_13_col19 = memory_id_to_big_value_tmp_1263.get_m31(13); + trace[19].data[row_index] = dst_limb_13_col19; + let dst_limb_14_col20 = memory_id_to_big_value_tmp_1263.get_m31(14); + trace[20].data[row_index] = dst_limb_14_col20; + let dst_limb_15_col21 = memory_id_to_big_value_tmp_1263.get_m31(15); + trace[21].data[row_index] = dst_limb_15_col21; + let dst_limb_16_col22 = memory_id_to_big_value_tmp_1263.get_m31(16); + trace[22].data[row_index] = dst_limb_16_col22; + let dst_limb_17_col23 = memory_id_to_big_value_tmp_1263.get_m31(17); + trace[23].data[row_index] = dst_limb_17_col23; + let dst_limb_18_col24 = memory_id_to_big_value_tmp_1263.get_m31(18); + trace[24].data[row_index] = dst_limb_18_col24; + let dst_limb_19_col25 = memory_id_to_big_value_tmp_1263.get_m31(19); + trace[25].data[row_index] = dst_limb_19_col25; + let dst_limb_20_col26 = memory_id_to_big_value_tmp_1263.get_m31(20); + trace[26].data[row_index] = dst_limb_20_col26; + let dst_limb_21_col27 = memory_id_to_big_value_tmp_1263.get_m31(21); + trace[27].data[row_index] = dst_limb_21_col27; + let dst_limb_22_col28 = memory_id_to_big_value_tmp_1263.get_m31(22); + trace[28].data[row_index] = dst_limb_22_col28; + let dst_limb_23_col29 = memory_id_to_big_value_tmp_1263.get_m31(23); + trace[29].data[row_index] = dst_limb_23_col29; + let dst_limb_24_col30 = memory_id_to_big_value_tmp_1263.get_m31(24); + trace[30].data[row_index] = dst_limb_24_col30; + let dst_limb_25_col31 = memory_id_to_big_value_tmp_1263.get_m31(25); + trace[31].data[row_index] = dst_limb_25_col31; + let dst_limb_26_col32 = memory_id_to_big_value_tmp_1263.get_m31(26); + trace[32].data[row_index] = dst_limb_26_col32; + let dst_limb_27_col33 = memory_id_to_big_value_tmp_1263.get_m31(27); + trace[33].data[row_index] = dst_limb_27_col33; + sub_components_inputs.memory_id_to_big_inputs[0].extend(dst_id_col5.unpack()); + + lookup_data.memoryidtobig[0].push([ + dst_id_col5, + dst_limb_0_col6, + dst_limb_1_col7, + dst_limb_2_col8, + dst_limb_3_col9, + dst_limb_4_col10, + dst_limb_5_col11, + dst_limb_6_col12, + dst_limb_7_col13, + dst_limb_8_col14, + dst_limb_9_col15, + dst_limb_10_col16, + dst_limb_11_col17, + dst_limb_12_col18, + dst_limb_13_col19, + dst_limb_14_col20, + dst_limb_15_col21, + dst_limb_16_col22, + dst_limb_17_col23, + dst_limb_18_col24, + dst_limb_19_col25, + dst_limb_20_col26, + dst_limb_21_col27, + dst_limb_22_col28, + dst_limb_23_col29, + dst_limb_24_col30, + dst_limb_25_col31, + dst_limb_26_col32, + dst_limb_27_col33, + ]); + + 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_col4)), + 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/jnz_opcode_is_taken_t_dst_base_fp_f/component.rs b/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_t_dst_base_fp_f/component.rs new file mode 100644 index 00000000..3999f0fb --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_t_dst_base_fp_f/component.rs @@ -0,0 +1,365 @@ +#![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; 42]; + let interaction_log_sizes = vec![log_size; SECURE_EXTENSION_DEGREE * 7]; + let preprocessed_log_sizes = vec![log_size]; + TreeVec::new(vec![ + preprocessed_log_sizes, + trace_log_sizes, + interaction_log_sizes, + ]) + } + + pub fn mix_into(&self, channel: &mut impl Channel) { + channel.mix_u64(self.n_calls as u64); + } +} + +#[derive(Copy, Clone, Serialize, Deserialize)] +pub struct InteractionClaim { + pub logup_sums: LogupSums, +} +impl InteractionClaim { + pub fn mix_into(&self, channel: &mut impl Channel) { + let (total_sum, claimed_sum) = self.logup_sums; + channel.mix_felts(&[total_sum]); + if let Some(claimed_sum) = claimed_sum { + channel.mix_felts(&[claimed_sum.0]); + channel.mix_u64(claimed_sum.1 as u64); + } + } +} + +pub type Component = FrameworkComponent; + +impl FrameworkEval for Eval { + fn log_size(&self) -> u32 { + std::cmp::max(self.claim.n_calls.next_power_of_two().ilog2(), LOG_N_LANES) + } + + fn max_constraint_log_degree_bound(&self) -> u32 { + self.log_size() + 1 + } + + #[allow(unused_parens)] + #[allow(clippy::double_parens)] + #[allow(non_snake_case)] + fn evaluate(&self, mut eval: E) -> E { + let M31_0 = E::F::from(M31::from(0)); + let M31_1 = E::F::from(M31::from(1)); + let M31_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_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 ap_update_add_1_col4 = eval.next_trace_mask(); + let dst_id_col5 = eval.next_trace_mask(); + let dst_limb_0_col6 = eval.next_trace_mask(); + let dst_limb_1_col7 = eval.next_trace_mask(); + let dst_limb_2_col8 = eval.next_trace_mask(); + let dst_limb_3_col9 = eval.next_trace_mask(); + let dst_limb_4_col10 = eval.next_trace_mask(); + let dst_limb_5_col11 = eval.next_trace_mask(); + let dst_limb_6_col12 = eval.next_trace_mask(); + let dst_limb_7_col13 = eval.next_trace_mask(); + let dst_limb_8_col14 = eval.next_trace_mask(); + let dst_limb_9_col15 = eval.next_trace_mask(); + let dst_limb_10_col16 = eval.next_trace_mask(); + let dst_limb_11_col17 = eval.next_trace_mask(); + let dst_limb_12_col18 = eval.next_trace_mask(); + let dst_limb_13_col19 = eval.next_trace_mask(); + let dst_limb_14_col20 = eval.next_trace_mask(); + let dst_limb_15_col21 = eval.next_trace_mask(); + let dst_limb_16_col22 = eval.next_trace_mask(); + let dst_limb_17_col23 = eval.next_trace_mask(); + let dst_limb_18_col24 = eval.next_trace_mask(); + let dst_limb_19_col25 = eval.next_trace_mask(); + let dst_limb_20_col26 = eval.next_trace_mask(); + let dst_limb_21_col27 = eval.next_trace_mask(); + let dst_limb_22_col28 = eval.next_trace_mask(); + let dst_limb_23_col29 = eval.next_trace_mask(); + let dst_limb_24_col30 = eval.next_trace_mask(); + let dst_limb_25_col31 = eval.next_trace_mask(); + let dst_limb_26_col32 = eval.next_trace_mask(); + let dst_limb_27_col33 = eval.next_trace_mask(); + let res_col34 = eval.next_trace_mask(); + let res_squares_col35 = eval.next_trace_mask(); + let next_pc_id_col36 = eval.next_trace_mask(); + let msb_col37 = eval.next_trace_mask(); + let mid_limbs_set_col38 = eval.next_trace_mask(); + let next_pc_limb_0_col39 = eval.next_trace_mask(); + let next_pc_limb_1_col40 = eval.next_trace_mask(); + let next_pc_limb_2_col41 = eval.next_trace_mask(); + + // decode_instruction_d2b4cd588a3e2a7b. + + eval.add_to_relation(&[RelationEntry::new( + &self.verifyinstruction_lookup_elements, + E::EF::one(), + &[ + input_pc_col0.clone(), + offset0_col3.clone(), + M31_32767.clone(), + M31_32769.clone(), + M31_0.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_1.clone(), + M31_0.clone(), + ap_update_add_1_col4.clone(), + ], + )]); + + // read_positive_num_bits_252. + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryaddresstoid_lookup_elements, + E::EF::one(), + &[ + (input_ap_col1.clone() + (offset0_col3.clone() - M31_32768.clone())), + dst_id_col5.clone(), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryidtobig_lookup_elements, + E::EF::one(), + &[ + dst_id_col5.clone(), + dst_limb_0_col6.clone(), + dst_limb_1_col7.clone(), + dst_limb_2_col8.clone(), + dst_limb_3_col9.clone(), + dst_limb_4_col10.clone(), + dst_limb_5_col11.clone(), + dst_limb_6_col12.clone(), + dst_limb_7_col13.clone(), + dst_limb_8_col14.clone(), + dst_limb_9_col15.clone(), + dst_limb_10_col16.clone(), + dst_limb_11_col17.clone(), + dst_limb_12_col18.clone(), + dst_limb_13_col19.clone(), + dst_limb_14_col20.clone(), + dst_limb_15_col21.clone(), + dst_limb_16_col22.clone(), + dst_limb_17_col23.clone(), + dst_limb_18_col24.clone(), + dst_limb_19_col25.clone(), + dst_limb_20_col26.clone(), + dst_limb_21_col27.clone(), + dst_limb_22_col28.clone(), + dst_limb_23_col29.clone(), + dst_limb_24_col30.clone(), + dst_limb_25_col31.clone(), + dst_limb_26_col32.clone(), + dst_limb_27_col33.clone(), + ], + )]); + + // dst doesn't equal 0. + eval.add_constraint( + ((((((((((((((((((((((((((((((M31_0.clone() + + dst_limb_0_col6.clone()) + + dst_limb_1_col7.clone()) + + dst_limb_2_col8.clone()) + + dst_limb_3_col9.clone()) + + dst_limb_4_col10.clone()) + + dst_limb_5_col11.clone()) + + dst_limb_6_col12.clone()) + + dst_limb_7_col13.clone()) + + dst_limb_8_col14.clone()) + + dst_limb_9_col15.clone()) + + dst_limb_10_col16.clone()) + + dst_limb_11_col17.clone()) + + dst_limb_12_col18.clone()) + + dst_limb_13_col19.clone()) + + dst_limb_14_col20.clone()) + + dst_limb_15_col21.clone()) + + dst_limb_16_col22.clone()) + + dst_limb_17_col23.clone()) + + dst_limb_18_col24.clone()) + + dst_limb_19_col25.clone()) + + dst_limb_20_col26.clone()) + + dst_limb_21_col27.clone()) + + dst_limb_22_col28.clone()) + + dst_limb_23_col29.clone()) + + dst_limb_24_col30.clone()) + + dst_limb_25_col31.clone()) + + dst_limb_26_col32.clone()) + + dst_limb_27_col33.clone()) + * res_col34.clone()) + - M31_1.clone()), + ); + let diff_from_p_tmp_1249 = (dst_limb_0_col6.clone() - M31_1.clone()); + let diff_from_p_tmp_1250 = (dst_limb_21_col27.clone() - M31_136.clone()); + let diff_from_p_tmp_1251 = (dst_limb_27_col33.clone() - M31_256.clone()); + // dst doesn't equal P. + eval.add_constraint( + ((((((((((((((((((((((((((((((M31_0.clone() + + (diff_from_p_tmp_1249.clone() + * diff_from_p_tmp_1249.clone())) + + dst_limb_1_col7.clone()) + + dst_limb_2_col8.clone()) + + dst_limb_3_col9.clone()) + + dst_limb_4_col10.clone()) + + dst_limb_5_col11.clone()) + + dst_limb_6_col12.clone()) + + dst_limb_7_col13.clone()) + + dst_limb_8_col14.clone()) + + dst_limb_9_col15.clone()) + + dst_limb_10_col16.clone()) + + dst_limb_11_col17.clone()) + + dst_limb_12_col18.clone()) + + dst_limb_13_col19.clone()) + + dst_limb_14_col20.clone()) + + dst_limb_15_col21.clone()) + + dst_limb_16_col22.clone()) + + dst_limb_17_col23.clone()) + + dst_limb_18_col24.clone()) + + dst_limb_19_col25.clone()) + + dst_limb_20_col26.clone()) + + (diff_from_p_tmp_1250.clone() * diff_from_p_tmp_1250.clone())) + + dst_limb_22_col28.clone()) + + dst_limb_23_col29.clone()) + + dst_limb_24_col30.clone()) + + dst_limb_25_col31.clone()) + + dst_limb_26_col32.clone()) + + (diff_from_p_tmp_1251.clone() * diff_from_p_tmp_1251.clone())) + * res_squares_col35.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()), + next_pc_id_col36.clone(), + ], + )]); + + // cond_decode_small_sign. + + // msb is a bit. + eval.add_constraint((msb_col37.clone() * (msb_col37.clone() - M31_1.clone()))); + // mid_limbs_set is a bit. + eval.add_constraint( + (mid_limbs_set_col38.clone() * (mid_limbs_set_col38.clone() - M31_1.clone())), + ); + // Cannot have msb equals 0 and mid_limbs_set equals 1. + eval.add_constraint( + ((M31_1.clone() * mid_limbs_set_col38.clone()) * (msb_col37.clone() - M31_1.clone())), + ); + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryidtobig_lookup_elements, + E::EF::one(), + &[ + next_pc_id_col36.clone(), + next_pc_limb_0_col39.clone(), + next_pc_limb_1_col40.clone(), + next_pc_limb_2_col41.clone(), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + ((M31_136.clone() * msb_col37.clone()) - mid_limbs_set_col38.clone()), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + (msb_col37.clone() * M31_256.clone()), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.opcodes_lookup_elements, + E::EF::one(), + &[ + input_pc_col0.clone(), + input_ap_col1.clone(), + input_fp_col2.clone(), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.opcodes_lookup_elements, + -E::EF::one(), + &[ + (input_pc_col0.clone() + + ((((next_pc_limb_0_col39.clone() + + (next_pc_limb_1_col40.clone() * M31_512.clone())) + + (next_pc_limb_2_col41.clone() * M31_262144.clone())) + - msb_col37.clone()) + - (M31_134217728.clone() * mid_limbs_set_col38.clone()))), + (input_ap_col1.clone() + ap_update_add_1_col4.clone()), + input_fp_col2.clone(), + ], + )]); + + eval.finalize_logup(); + eval + } +} diff --git a/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_t_dst_base_fp_f/mod.rs b/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_t_dst_base_fp_f/mod.rs new file mode 100644 index 00000000..3f7a8d74 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_t_dst_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/jnz_opcode_is_taken_t_dst_base_fp_f/prover.rs b/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_t_dst_base_fp_f/prover.rs new file mode 100644 index 00000000..6fa732d0 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_t_dst_base_fp_f/prover.rs @@ -0,0 +1,619 @@ +#![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 = 42; + +#[derive(Default)] +pub struct ClaimGenerator { + pub inputs: Vec, +} +impl ClaimGenerator { + pub fn new(inputs: Vec) -> Self { + Self { inputs } + } + + pub fn write_trace( + mut self, + tree_builder: &mut TreeBuilder<'_, '_, SimdBackend, Blake2sMerkleChannel>, + memory_address_to_id_state: &mut memory_address_to_id::ClaimGenerator, + memory_id_to_big_state: &mut memory_id_to_big::ClaimGenerator, + verify_instruction_state: &mut verify_instruction::ClaimGenerator, + ) -> (Claim, InteractionClaimGenerator) { + let n_calls = self.inputs.len(); + assert_ne!(n_calls, 0); + let size = std::cmp::max(n_calls.next_power_of_two(), N_LANES); + let need_padding = n_calls != size; + + if need_padding { + self.inputs.resize(size, *self.inputs.first().unwrap()); + bit_reverse_coset_to_circle_domain_order(&mut self.inputs); + } + + let packed_inputs = pack_values(&self.inputs); + let (trace, mut sub_components_inputs, lookup_data) = write_trace_simd( + packed_inputs, + memory_address_to_id_state, + memory_id_to_big_state, + ); + + if need_padding { + sub_components_inputs.bit_reverse_coset_to_circle_domain_order(); + } + sub_components_inputs + .memory_address_to_id_inputs + .iter() + .for_each(|inputs| { + memory_address_to_id_state.add_inputs(&inputs[..n_calls]); + }); + sub_components_inputs + .memory_id_to_big_inputs + .iter() + .for_each(|inputs| { + memory_id_to_big_state.add_inputs(&inputs[..n_calls]); + }); + sub_components_inputs + .verify_instruction_inputs + .iter() + .for_each(|inputs| { + verify_instruction_state.add_inputs(&inputs[..n_calls]); + }); + + tree_builder.extend_evals( + trace + .into_iter() + .map(|eval| { + let domain = CanonicCoset::new( + eval.len() + .checked_ilog2() + .expect("Input is not a power of 2!"), + ) + .circle_domain(); + CircleEvaluation::::new(domain, eval) + }) + .collect_vec(), + ); + + ( + Claim { n_calls }, + InteractionClaimGenerator { + n_calls, + lookup_data, + }, + ) + } + + pub fn add_inputs(&mut self, inputs: &[InputType]) { + self.inputs.extend(inputs); + } +} + +pub struct SubComponentInputs { + pub memory_address_to_id_inputs: [Vec; 2], + pub memory_id_to_big_inputs: [Vec; 2], + pub verify_instruction_inputs: [Vec; 1], +} +impl SubComponentInputs { + #[allow(unused_variables)] + fn with_capacity(capacity: usize) -> Self { + Self { + memory_address_to_id_inputs: [ + Vec::with_capacity(capacity), + Vec::with_capacity(capacity), + ], + memory_id_to_big_inputs: [Vec::with_capacity(capacity), Vec::with_capacity(capacity)], + verify_instruction_inputs: [Vec::with_capacity(capacity)], + } + } + + fn bit_reverse_coset_to_circle_domain_order(&mut self) { + self.memory_address_to_id_inputs + .iter_mut() + .for_each(|vec| bit_reverse_coset_to_circle_domain_order(vec)); + self.memory_id_to_big_inputs + .iter_mut() + .for_each(|vec| bit_reverse_coset_to_circle_domain_order(vec)); + self.verify_instruction_inputs + .iter_mut() + .for_each(|vec| bit_reverse_coset_to_circle_domain_order(vec)); + } +} + +#[allow(clippy::useless_conversion)] +#[allow(unused_variables)] +#[allow(clippy::double_parens)] +#[allow(non_snake_case)] +pub fn write_trace_simd( + inputs: Vec, + memory_address_to_id_state: &mut memory_address_to_id::ClaimGenerator, + memory_id_to_big_state: &mut memory_id_to_big::ClaimGenerator, +) -> ( + [BaseColumn; N_TRACE_COLUMNS], + SubComponentInputs, + LookupData, +) { + const N_TRACE_COLUMNS: usize = 42; + 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_32769 = PackedM31::broadcast(M31::from(32769)); + let M31_511 = PackedM31::broadcast(M31::from(511)); + let M31_512 = PackedM31::broadcast(M31::from(512)); + let UInt16_1 = PackedUInt16::broadcast(UInt16::from(1)); + let UInt16_11 = PackedUInt16::broadcast(UInt16::from(11)); + let UInt16_127 = PackedUInt16::broadcast(UInt16::from(127)); + let UInt16_3 = PackedUInt16::broadcast(UInt16::from(3)); + let UInt16_6 = PackedUInt16::broadcast(UInt16::from(6)); + let UInt16_9 = PackedUInt16::broadcast(UInt16::from(9)); + + inputs.into_iter().enumerate().for_each( + |(row_index, jnz_opcode_is_taken_t_dst_base_fp_f_input)| { + let input_tmp_1241 = jnz_opcode_is_taken_t_dst_base_fp_f_input; + let input_pc_col0 = input_tmp_1241.pc; + trace[0].data[row_index] = input_pc_col0; + let input_ap_col1 = input_tmp_1241.ap; + trace[1].data[row_index] = input_ap_col1; + let input_fp_col2 = input_tmp_1241.fp; + trace[2].data[row_index] = input_fp_col2; + + // decode_instruction_d2b4cd588a3e2a7b. + + let memory_address_to_id_value_tmp_1242 = + memory_address_to_id_state.deduce_output(input_pc_col0); + let memory_id_to_big_value_tmp_1243 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1242); + let offset0_tmp_1244 = + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1243.get_m31(0))) + + (((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1243.get_m31(1))) + & (UInt16_127)) + << (UInt16_9))); + let offset0_col3 = offset0_tmp_1244.as_m31(); + trace[3].data[row_index] = offset0_col3; + let ap_update_add_1_tmp_1245 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1243.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1243.get_m31(6))) + << (UInt16_6))) + >> (UInt16_11)) + & (UInt16_1)); + let ap_update_add_1_col4 = ap_update_add_1_tmp_1245.as_m31(); + trace[4].data[row_index] = ap_update_add_1_col4; + + sub_components_inputs.verify_instruction_inputs[0].extend( + ( + input_pc_col0, + [offset0_col3, M31_32767, M31_32769], + [ + M31_0, + M31_1, + M31_1, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_1, + M31_0, + ap_update_add_1_col4, + M31_0, + M31_0, + M31_0, + ], + ) + .unpack(), + ); + + lookup_data.verifyinstruction[0].push([ + input_pc_col0, + offset0_col3, + M31_32767, + M31_32769, + M31_0, + M31_1, + M31_1, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_1, + M31_0, + ap_update_add_1_col4, + M31_0, + M31_0, + M31_0, + ]); + + // read_positive_num_bits_252. + + let memory_address_to_id_value_tmp_1247 = memory_address_to_id_state + .deduce_output(((input_ap_col1) + ((offset0_col3) - (M31_32768)))); + let memory_id_to_big_value_tmp_1248 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1247); + let dst_id_col5 = memory_address_to_id_value_tmp_1247; + trace[5].data[row_index] = dst_id_col5; + sub_components_inputs.memory_address_to_id_inputs[0] + .extend(((input_ap_col1) + ((offset0_col3) - (M31_32768))).unpack()); + + lookup_data.memoryaddresstoid[0].push([ + ((input_ap_col1) + ((offset0_col3) - (M31_32768))), + dst_id_col5, + ]); + let dst_limb_0_col6 = memory_id_to_big_value_tmp_1248.get_m31(0); + trace[6].data[row_index] = dst_limb_0_col6; + let dst_limb_1_col7 = memory_id_to_big_value_tmp_1248.get_m31(1); + trace[7].data[row_index] = dst_limb_1_col7; + let dst_limb_2_col8 = memory_id_to_big_value_tmp_1248.get_m31(2); + trace[8].data[row_index] = dst_limb_2_col8; + let dst_limb_3_col9 = memory_id_to_big_value_tmp_1248.get_m31(3); + trace[9].data[row_index] = dst_limb_3_col9; + let dst_limb_4_col10 = memory_id_to_big_value_tmp_1248.get_m31(4); + trace[10].data[row_index] = dst_limb_4_col10; + let dst_limb_5_col11 = memory_id_to_big_value_tmp_1248.get_m31(5); + trace[11].data[row_index] = dst_limb_5_col11; + let dst_limb_6_col12 = memory_id_to_big_value_tmp_1248.get_m31(6); + trace[12].data[row_index] = dst_limb_6_col12; + let dst_limb_7_col13 = memory_id_to_big_value_tmp_1248.get_m31(7); + trace[13].data[row_index] = dst_limb_7_col13; + let dst_limb_8_col14 = memory_id_to_big_value_tmp_1248.get_m31(8); + trace[14].data[row_index] = dst_limb_8_col14; + let dst_limb_9_col15 = memory_id_to_big_value_tmp_1248.get_m31(9); + trace[15].data[row_index] = dst_limb_9_col15; + let dst_limb_10_col16 = memory_id_to_big_value_tmp_1248.get_m31(10); + trace[16].data[row_index] = dst_limb_10_col16; + let dst_limb_11_col17 = memory_id_to_big_value_tmp_1248.get_m31(11); + trace[17].data[row_index] = dst_limb_11_col17; + let dst_limb_12_col18 = memory_id_to_big_value_tmp_1248.get_m31(12); + trace[18].data[row_index] = dst_limb_12_col18; + let dst_limb_13_col19 = memory_id_to_big_value_tmp_1248.get_m31(13); + trace[19].data[row_index] = dst_limb_13_col19; + let dst_limb_14_col20 = memory_id_to_big_value_tmp_1248.get_m31(14); + trace[20].data[row_index] = dst_limb_14_col20; + let dst_limb_15_col21 = memory_id_to_big_value_tmp_1248.get_m31(15); + trace[21].data[row_index] = dst_limb_15_col21; + let dst_limb_16_col22 = memory_id_to_big_value_tmp_1248.get_m31(16); + trace[22].data[row_index] = dst_limb_16_col22; + let dst_limb_17_col23 = memory_id_to_big_value_tmp_1248.get_m31(17); + trace[23].data[row_index] = dst_limb_17_col23; + let dst_limb_18_col24 = memory_id_to_big_value_tmp_1248.get_m31(18); + trace[24].data[row_index] = dst_limb_18_col24; + let dst_limb_19_col25 = memory_id_to_big_value_tmp_1248.get_m31(19); + trace[25].data[row_index] = dst_limb_19_col25; + let dst_limb_20_col26 = memory_id_to_big_value_tmp_1248.get_m31(20); + trace[26].data[row_index] = dst_limb_20_col26; + let dst_limb_21_col27 = memory_id_to_big_value_tmp_1248.get_m31(21); + trace[27].data[row_index] = dst_limb_21_col27; + let dst_limb_22_col28 = memory_id_to_big_value_tmp_1248.get_m31(22); + trace[28].data[row_index] = dst_limb_22_col28; + let dst_limb_23_col29 = memory_id_to_big_value_tmp_1248.get_m31(23); + trace[29].data[row_index] = dst_limb_23_col29; + let dst_limb_24_col30 = memory_id_to_big_value_tmp_1248.get_m31(24); + trace[30].data[row_index] = dst_limb_24_col30; + let dst_limb_25_col31 = memory_id_to_big_value_tmp_1248.get_m31(25); + trace[31].data[row_index] = dst_limb_25_col31; + let dst_limb_26_col32 = memory_id_to_big_value_tmp_1248.get_m31(26); + trace[32].data[row_index] = dst_limb_26_col32; + let dst_limb_27_col33 = memory_id_to_big_value_tmp_1248.get_m31(27); + trace[33].data[row_index] = dst_limb_27_col33; + sub_components_inputs.memory_id_to_big_inputs[0].extend(dst_id_col5.unpack()); + + lookup_data.memoryidtobig[0].push([ + dst_id_col5, + dst_limb_0_col6, + dst_limb_1_col7, + dst_limb_2_col8, + dst_limb_3_col9, + dst_limb_4_col10, + dst_limb_5_col11, + dst_limb_6_col12, + dst_limb_7_col13, + dst_limb_8_col14, + dst_limb_9_col15, + dst_limb_10_col16, + dst_limb_11_col17, + dst_limb_12_col18, + dst_limb_13_col19, + dst_limb_14_col20, + dst_limb_15_col21, + dst_limb_16_col22, + dst_limb_17_col23, + dst_limb_18_col24, + dst_limb_19_col25, + dst_limb_20_col26, + dst_limb_21_col27, + dst_limb_22_col28, + dst_limb_23_col29, + dst_limb_24_col30, + dst_limb_25_col31, + dst_limb_26_col32, + dst_limb_27_col33, + ]); + + let res_col34 = ((M31_1).div( + (((((((((((((((((((((((((((((M31_0) + (dst_limb_0_col6)) + + (dst_limb_1_col7)) + + (dst_limb_2_col8)) + + (dst_limb_3_col9)) + + (dst_limb_4_col10)) + + (dst_limb_5_col11)) + + (dst_limb_6_col12)) + + (dst_limb_7_col13)) + + (dst_limb_8_col14)) + + (dst_limb_9_col15)) + + (dst_limb_10_col16)) + + (dst_limb_11_col17)) + + (dst_limb_12_col18)) + + (dst_limb_13_col19)) + + (dst_limb_14_col20)) + + (dst_limb_15_col21)) + + (dst_limb_16_col22)) + + (dst_limb_17_col23)) + + (dst_limb_18_col24)) + + (dst_limb_19_col25)) + + (dst_limb_20_col26)) + + (dst_limb_21_col27)) + + (dst_limb_22_col28)) + + (dst_limb_23_col29)) + + (dst_limb_24_col30)) + + (dst_limb_25_col31)) + + (dst_limb_26_col32)) + + (dst_limb_27_col33)), + )); + trace[34].data[row_index] = res_col34; + let diff_from_p_tmp_1249 = ((dst_limb_0_col6) - (M31_1)); + let diff_from_p_tmp_1250 = ((dst_limb_21_col27) - (M31_136)); + let diff_from_p_tmp_1251 = ((dst_limb_27_col33) - (M31_256)); + let res_squares_col35 = ((M31_1).div( + (((((((((((((((((((((((((((((M31_0) + + ((diff_from_p_tmp_1249) * (diff_from_p_tmp_1249))) + + (dst_limb_1_col7)) + + (dst_limb_2_col8)) + + (dst_limb_3_col9)) + + (dst_limb_4_col10)) + + (dst_limb_5_col11)) + + (dst_limb_6_col12)) + + (dst_limb_7_col13)) + + (dst_limb_8_col14)) + + (dst_limb_9_col15)) + + (dst_limb_10_col16)) + + (dst_limb_11_col17)) + + (dst_limb_12_col18)) + + (dst_limb_13_col19)) + + (dst_limb_14_col20)) + + (dst_limb_15_col21)) + + (dst_limb_16_col22)) + + (dst_limb_17_col23)) + + (dst_limb_18_col24)) + + (dst_limb_19_col25)) + + (dst_limb_20_col26)) + + ((diff_from_p_tmp_1250) * (diff_from_p_tmp_1250))) + + (dst_limb_22_col28)) + + (dst_limb_23_col29)) + + (dst_limb_24_col30)) + + (dst_limb_25_col31)) + + (dst_limb_26_col32)) + + ((diff_from_p_tmp_1251) * (diff_from_p_tmp_1251))), + )); + trace[35].data[row_index] = res_squares_col35; + + // read_small. + + let memory_address_to_id_value_tmp_1252 = + memory_address_to_id_state.deduce_output(((input_pc_col0) + (M31_1))); + let memory_id_to_big_value_tmp_1253 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1252); + let next_pc_id_col36 = memory_address_to_id_value_tmp_1252; + trace[36].data[row_index] = next_pc_id_col36; + sub_components_inputs.memory_address_to_id_inputs[1] + .extend(((input_pc_col0) + (M31_1)).unpack()); + + lookup_data.memoryaddresstoid[1].push([((input_pc_col0) + (M31_1)), next_pc_id_col36]); + + // cond_decode_small_sign. + + let msb_tmp_1254 = memory_id_to_big_value_tmp_1253.get_m31(27).eq(M31_256); + let msb_col37 = msb_tmp_1254.as_m31(); + trace[37].data[row_index] = msb_col37; + let mid_limbs_set_tmp_1255 = memory_id_to_big_value_tmp_1253.get_m31(20).eq(M31_511); + let mid_limbs_set_col38 = mid_limbs_set_tmp_1255.as_m31(); + trace[38].data[row_index] = mid_limbs_set_col38; + + let next_pc_limb_0_col39 = memory_id_to_big_value_tmp_1253.get_m31(0); + trace[39].data[row_index] = next_pc_limb_0_col39; + let next_pc_limb_1_col40 = memory_id_to_big_value_tmp_1253.get_m31(1); + trace[40].data[row_index] = next_pc_limb_1_col40; + let next_pc_limb_2_col41 = memory_id_to_big_value_tmp_1253.get_m31(2); + trace[41].data[row_index] = next_pc_limb_2_col41; + sub_components_inputs.memory_id_to_big_inputs[1].extend(next_pc_id_col36.unpack()); + + lookup_data.memoryidtobig[1].push([ + next_pc_id_col36, + next_pc_limb_0_col39, + next_pc_limb_1_col40, + next_pc_limb_2_col41, + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + (((M31_136) * (msb_col37)) - (mid_limbs_set_col38)), + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + ((msb_col37) * (M31_256)), + ]); + + lookup_data.opcodes[0].push([input_pc_col0, input_ap_col1, input_fp_col2]); + lookup_data.opcodes[1].push([ + ((input_pc_col0) + + (((((next_pc_limb_0_col39) + ((next_pc_limb_1_col40) * (M31_512))) + + ((next_pc_limb_2_col41) * (M31_262144))) + - (msb_col37)) + - ((M31_134217728) * (mid_limbs_set_col38)))), + ((input_ap_col1) + (ap_update_add_1_col4)), + input_fp_col2, + ]); + }, + ); + + (trace, sub_components_inputs, lookup_data) +} + +pub struct LookupData { + pub memoryaddresstoid: [Vec<[PackedM31; 2]>; 2], + pub memoryidtobig: [Vec<[PackedM31; 29]>; 2], + pub opcodes: [Vec<[PackedM31; 3]>; 2], + pub verifyinstruction: [Vec<[PackedM31; 19]>; 1], +} +impl LookupData { + #[allow(unused_variables)] + fn with_capacity(capacity: usize) -> Self { + Self { + memoryaddresstoid: [Vec::with_capacity(capacity), Vec::with_capacity(capacity)], + memoryidtobig: [Vec::with_capacity(capacity), Vec::with_capacity(capacity)], + opcodes: [Vec::with_capacity(capacity), Vec::with_capacity(capacity)], + verifyinstruction: [Vec::with_capacity(capacity)], + } + } +} + +pub struct InteractionClaimGenerator { + pub n_calls: usize, + pub lookup_data: LookupData, +} +impl InteractionClaimGenerator { + pub fn write_interaction_trace( + self, + tree_builder: &mut TreeBuilder<'_, '_, SimdBackend, Blake2sMerkleChannel>, + memoryaddresstoid_lookup_elements: &relations::MemoryAddressToId, + memoryidtobig_lookup_elements: &relations::MemoryIdToBig, + opcodes_lookup_elements: &relations::Opcodes, + verifyinstruction_lookup_elements: &relations::VerifyInstruction, + ) -> InteractionClaim { + let log_size = std::cmp::max(self.n_calls.next_power_of_two().ilog2(), LOG_N_LANES); + let mut logup_gen = LogupTraceGenerator::new(log_size); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.verifyinstruction[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = verifyinstruction_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.memoryaddresstoid[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = memoryaddresstoid_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.memoryidtobig[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = memoryidtobig_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.memoryaddresstoid[1]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = memoryaddresstoid_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.memoryidtobig[1]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = memoryidtobig_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.opcodes[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = opcodes_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.opcodes[1]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = opcodes_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, -PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let (trace, total_sum, claimed_sum) = if self.n_calls == 1 << log_size { + let (trace, claimed_sum) = logup_gen.finalize_last(); + (trace, claimed_sum, None) + } else { + let (trace, [total_sum, claimed_sum]) = + logup_gen.finalize_at([(1 << log_size) - 1, self.n_calls - 1]); + (trace, total_sum, Some((claimed_sum, self.n_calls - 1))) + }; + tree_builder.extend_evals(trace); + + InteractionClaim { + logup_sums: (total_sum, claimed_sum), + } + } +} diff --git a/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_t_dst_base_fp_t/component.rs b/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_t_dst_base_fp_t/component.rs new file mode 100644 index 00000000..80e75b05 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_t_dst_base_fp_t/component.rs @@ -0,0 +1,365 @@ +#![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; 42]; + let interaction_log_sizes = vec![log_size; SECURE_EXTENSION_DEGREE * 7]; + let preprocessed_log_sizes = vec![log_size]; + TreeVec::new(vec![ + preprocessed_log_sizes, + trace_log_sizes, + interaction_log_sizes, + ]) + } + + pub fn mix_into(&self, channel: &mut impl Channel) { + channel.mix_u64(self.n_calls as u64); + } +} + +#[derive(Copy, Clone, Serialize, Deserialize)] +pub struct InteractionClaim { + pub logup_sums: LogupSums, +} +impl InteractionClaim { + pub fn mix_into(&self, channel: &mut impl Channel) { + let (total_sum, claimed_sum) = self.logup_sums; + channel.mix_felts(&[total_sum]); + if let Some(claimed_sum) = claimed_sum { + channel.mix_felts(&[claimed_sum.0]); + channel.mix_u64(claimed_sum.1 as u64); + } + } +} + +pub type Component = FrameworkComponent; + +impl FrameworkEval for Eval { + fn log_size(&self) -> u32 { + std::cmp::max(self.claim.n_calls.next_power_of_two().ilog2(), LOG_N_LANES) + } + + fn max_constraint_log_degree_bound(&self) -> u32 { + self.log_size() + 1 + } + + #[allow(unused_parens)] + #[allow(clippy::double_parens)] + #[allow(non_snake_case)] + fn evaluate(&self, mut eval: E) -> E { + let M31_0 = E::F::from(M31::from(0)); + let M31_1 = E::F::from(M31::from(1)); + let M31_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_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 ap_update_add_1_col4 = eval.next_trace_mask(); + let dst_id_col5 = eval.next_trace_mask(); + let dst_limb_0_col6 = eval.next_trace_mask(); + let dst_limb_1_col7 = eval.next_trace_mask(); + let dst_limb_2_col8 = eval.next_trace_mask(); + let dst_limb_3_col9 = eval.next_trace_mask(); + let dst_limb_4_col10 = eval.next_trace_mask(); + let dst_limb_5_col11 = eval.next_trace_mask(); + let dst_limb_6_col12 = eval.next_trace_mask(); + let dst_limb_7_col13 = eval.next_trace_mask(); + let dst_limb_8_col14 = eval.next_trace_mask(); + let dst_limb_9_col15 = eval.next_trace_mask(); + let dst_limb_10_col16 = eval.next_trace_mask(); + let dst_limb_11_col17 = eval.next_trace_mask(); + let dst_limb_12_col18 = eval.next_trace_mask(); + let dst_limb_13_col19 = eval.next_trace_mask(); + let dst_limb_14_col20 = eval.next_trace_mask(); + let dst_limb_15_col21 = eval.next_trace_mask(); + let dst_limb_16_col22 = eval.next_trace_mask(); + let dst_limb_17_col23 = eval.next_trace_mask(); + let dst_limb_18_col24 = eval.next_trace_mask(); + let dst_limb_19_col25 = eval.next_trace_mask(); + let dst_limb_20_col26 = eval.next_trace_mask(); + let dst_limb_21_col27 = eval.next_trace_mask(); + let dst_limb_22_col28 = eval.next_trace_mask(); + let dst_limb_23_col29 = eval.next_trace_mask(); + let dst_limb_24_col30 = eval.next_trace_mask(); + let dst_limb_25_col31 = eval.next_trace_mask(); + let dst_limb_26_col32 = eval.next_trace_mask(); + let dst_limb_27_col33 = eval.next_trace_mask(); + let res_col34 = eval.next_trace_mask(); + let res_squares_col35 = eval.next_trace_mask(); + let next_pc_id_col36 = eval.next_trace_mask(); + let msb_col37 = eval.next_trace_mask(); + let mid_limbs_set_col38 = eval.next_trace_mask(); + let next_pc_limb_0_col39 = eval.next_trace_mask(); + let next_pc_limb_1_col40 = eval.next_trace_mask(); + let next_pc_limb_2_col41 = eval.next_trace_mask(); + + // decode_instruction_113648125c3c3f56. + + eval.add_to_relation(&[RelationEntry::new( + &self.verifyinstruction_lookup_elements, + E::EF::one(), + &[ + input_pc_col0.clone(), + offset0_col3.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_1.clone(), + M31_0.clone(), + ap_update_add_1_col4.clone(), + ], + )]); + + // read_positive_num_bits_252. + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryaddresstoid_lookup_elements, + E::EF::one(), + &[ + (input_fp_col2.clone() + (offset0_col3.clone() - M31_32768.clone())), + dst_id_col5.clone(), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryidtobig_lookup_elements, + E::EF::one(), + &[ + dst_id_col5.clone(), + dst_limb_0_col6.clone(), + dst_limb_1_col7.clone(), + dst_limb_2_col8.clone(), + dst_limb_3_col9.clone(), + dst_limb_4_col10.clone(), + dst_limb_5_col11.clone(), + dst_limb_6_col12.clone(), + dst_limb_7_col13.clone(), + dst_limb_8_col14.clone(), + dst_limb_9_col15.clone(), + dst_limb_10_col16.clone(), + dst_limb_11_col17.clone(), + dst_limb_12_col18.clone(), + dst_limb_13_col19.clone(), + dst_limb_14_col20.clone(), + dst_limb_15_col21.clone(), + dst_limb_16_col22.clone(), + dst_limb_17_col23.clone(), + dst_limb_18_col24.clone(), + dst_limb_19_col25.clone(), + dst_limb_20_col26.clone(), + dst_limb_21_col27.clone(), + dst_limb_22_col28.clone(), + dst_limb_23_col29.clone(), + dst_limb_24_col30.clone(), + dst_limb_25_col31.clone(), + dst_limb_26_col32.clone(), + dst_limb_27_col33.clone(), + ], + )]); + + // dst doesn't equal 0. + eval.add_constraint( + ((((((((((((((((((((((((((((((M31_0.clone() + + dst_limb_0_col6.clone()) + + dst_limb_1_col7.clone()) + + dst_limb_2_col8.clone()) + + dst_limb_3_col9.clone()) + + dst_limb_4_col10.clone()) + + dst_limb_5_col11.clone()) + + dst_limb_6_col12.clone()) + + dst_limb_7_col13.clone()) + + dst_limb_8_col14.clone()) + + dst_limb_9_col15.clone()) + + dst_limb_10_col16.clone()) + + dst_limb_11_col17.clone()) + + dst_limb_12_col18.clone()) + + dst_limb_13_col19.clone()) + + dst_limb_14_col20.clone()) + + dst_limb_15_col21.clone()) + + dst_limb_16_col22.clone()) + + dst_limb_17_col23.clone()) + + dst_limb_18_col24.clone()) + + dst_limb_19_col25.clone()) + + dst_limb_20_col26.clone()) + + dst_limb_21_col27.clone()) + + dst_limb_22_col28.clone()) + + dst_limb_23_col29.clone()) + + dst_limb_24_col30.clone()) + + dst_limb_25_col31.clone()) + + dst_limb_26_col32.clone()) + + dst_limb_27_col33.clone()) + * res_col34.clone()) + - M31_1.clone()), + ); + let diff_from_p_tmp_1221 = (dst_limb_0_col6.clone() - M31_1.clone()); + let diff_from_p_tmp_1222 = (dst_limb_21_col27.clone() - M31_136.clone()); + let diff_from_p_tmp_1223 = (dst_limb_27_col33.clone() - M31_256.clone()); + // dst doesn't equal P. + eval.add_constraint( + ((((((((((((((((((((((((((((((M31_0.clone() + + (diff_from_p_tmp_1221.clone() + * diff_from_p_tmp_1221.clone())) + + dst_limb_1_col7.clone()) + + dst_limb_2_col8.clone()) + + dst_limb_3_col9.clone()) + + dst_limb_4_col10.clone()) + + dst_limb_5_col11.clone()) + + dst_limb_6_col12.clone()) + + dst_limb_7_col13.clone()) + + dst_limb_8_col14.clone()) + + dst_limb_9_col15.clone()) + + dst_limb_10_col16.clone()) + + dst_limb_11_col17.clone()) + + dst_limb_12_col18.clone()) + + dst_limb_13_col19.clone()) + + dst_limb_14_col20.clone()) + + dst_limb_15_col21.clone()) + + dst_limb_16_col22.clone()) + + dst_limb_17_col23.clone()) + + dst_limb_18_col24.clone()) + + dst_limb_19_col25.clone()) + + dst_limb_20_col26.clone()) + + (diff_from_p_tmp_1222.clone() * diff_from_p_tmp_1222.clone())) + + dst_limb_22_col28.clone()) + + dst_limb_23_col29.clone()) + + dst_limb_24_col30.clone()) + + dst_limb_25_col31.clone()) + + dst_limb_26_col32.clone()) + + (diff_from_p_tmp_1223.clone() * diff_from_p_tmp_1223.clone())) + * res_squares_col35.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()), + next_pc_id_col36.clone(), + ], + )]); + + // cond_decode_small_sign. + + // msb is a bit. + eval.add_constraint((msb_col37.clone() * (msb_col37.clone() - M31_1.clone()))); + // mid_limbs_set is a bit. + eval.add_constraint( + (mid_limbs_set_col38.clone() * (mid_limbs_set_col38.clone() - M31_1.clone())), + ); + // Cannot have msb equals 0 and mid_limbs_set equals 1. + eval.add_constraint( + ((M31_1.clone() * mid_limbs_set_col38.clone()) * (msb_col37.clone() - M31_1.clone())), + ); + + eval.add_to_relation(&[RelationEntry::new( + &self.memoryidtobig_lookup_elements, + E::EF::one(), + &[ + next_pc_id_col36.clone(), + next_pc_limb_0_col39.clone(), + next_pc_limb_1_col40.clone(), + next_pc_limb_2_col41.clone(), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + (mid_limbs_set_col38.clone() * M31_511.clone()), + ((M31_136.clone() * msb_col37.clone()) - mid_limbs_set_col38.clone()), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + M31_0.clone(), + (msb_col37.clone() * M31_256.clone()), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.opcodes_lookup_elements, + E::EF::one(), + &[ + input_pc_col0.clone(), + input_ap_col1.clone(), + input_fp_col2.clone(), + ], + )]); + + eval.add_to_relation(&[RelationEntry::new( + &self.opcodes_lookup_elements, + -E::EF::one(), + &[ + (input_pc_col0.clone() + + ((((next_pc_limb_0_col39.clone() + + (next_pc_limb_1_col40.clone() * M31_512.clone())) + + (next_pc_limb_2_col41.clone() * M31_262144.clone())) + - msb_col37.clone()) + - (M31_134217728.clone() * mid_limbs_set_col38.clone()))), + (input_ap_col1.clone() + ap_update_add_1_col4.clone()), + input_fp_col2.clone(), + ], + )]); + + eval.finalize_logup(); + eval + } +} diff --git a/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_t_dst_base_fp_t/mod.rs b/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_t_dst_base_fp_t/mod.rs new file mode 100644 index 00000000..3f7a8d74 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_t_dst_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/jnz_opcode_is_taken_t_dst_base_fp_t/prover.rs b/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_t_dst_base_fp_t/prover.rs new file mode 100644 index 00000000..0d3ea0c8 --- /dev/null +++ b/stwo_cairo_prover/crates/prover/src/components/jnz_opcode_is_taken_t_dst_base_fp_t/prover.rs @@ -0,0 +1,619 @@ +#![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 = 42; + +#[derive(Default)] +pub struct ClaimGenerator { + pub inputs: Vec, +} +impl ClaimGenerator { + pub fn new(inputs: Vec) -> Self { + Self { inputs } + } + + pub fn write_trace( + mut self, + tree_builder: &mut TreeBuilder<'_, '_, SimdBackend, Blake2sMerkleChannel>, + memory_address_to_id_state: &mut memory_address_to_id::ClaimGenerator, + memory_id_to_big_state: &mut memory_id_to_big::ClaimGenerator, + verify_instruction_state: &mut verify_instruction::ClaimGenerator, + ) -> (Claim, InteractionClaimGenerator) { + let n_calls = self.inputs.len(); + assert_ne!(n_calls, 0); + let size = std::cmp::max(n_calls.next_power_of_two(), N_LANES); + let need_padding = n_calls != size; + + if need_padding { + self.inputs.resize(size, *self.inputs.first().unwrap()); + bit_reverse_coset_to_circle_domain_order(&mut self.inputs); + } + + let packed_inputs = pack_values(&self.inputs); + let (trace, mut sub_components_inputs, lookup_data) = write_trace_simd( + packed_inputs, + memory_address_to_id_state, + memory_id_to_big_state, + ); + + if need_padding { + sub_components_inputs.bit_reverse_coset_to_circle_domain_order(); + } + sub_components_inputs + .memory_address_to_id_inputs + .iter() + .for_each(|inputs| { + memory_address_to_id_state.add_inputs(&inputs[..n_calls]); + }); + sub_components_inputs + .memory_id_to_big_inputs + .iter() + .for_each(|inputs| { + memory_id_to_big_state.add_inputs(&inputs[..n_calls]); + }); + sub_components_inputs + .verify_instruction_inputs + .iter() + .for_each(|inputs| { + verify_instruction_state.add_inputs(&inputs[..n_calls]); + }); + + tree_builder.extend_evals( + trace + .into_iter() + .map(|eval| { + let domain = CanonicCoset::new( + eval.len() + .checked_ilog2() + .expect("Input is not a power of 2!"), + ) + .circle_domain(); + CircleEvaluation::::new(domain, eval) + }) + .collect_vec(), + ); + + ( + Claim { n_calls }, + InteractionClaimGenerator { + n_calls, + lookup_data, + }, + ) + } + + pub fn add_inputs(&mut self, inputs: &[InputType]) { + self.inputs.extend(inputs); + } +} + +pub struct SubComponentInputs { + pub memory_address_to_id_inputs: [Vec; 2], + pub memory_id_to_big_inputs: [Vec; 2], + pub verify_instruction_inputs: [Vec; 1], +} +impl SubComponentInputs { + #[allow(unused_variables)] + fn with_capacity(capacity: usize) -> Self { + Self { + memory_address_to_id_inputs: [ + Vec::with_capacity(capacity), + Vec::with_capacity(capacity), + ], + memory_id_to_big_inputs: [Vec::with_capacity(capacity), Vec::with_capacity(capacity)], + verify_instruction_inputs: [Vec::with_capacity(capacity)], + } + } + + fn bit_reverse_coset_to_circle_domain_order(&mut self) { + self.memory_address_to_id_inputs + .iter_mut() + .for_each(|vec| bit_reverse_coset_to_circle_domain_order(vec)); + self.memory_id_to_big_inputs + .iter_mut() + .for_each(|vec| bit_reverse_coset_to_circle_domain_order(vec)); + self.verify_instruction_inputs + .iter_mut() + .for_each(|vec| bit_reverse_coset_to_circle_domain_order(vec)); + } +} + +#[allow(clippy::useless_conversion)] +#[allow(unused_variables)] +#[allow(clippy::double_parens)] +#[allow(non_snake_case)] +pub fn write_trace_simd( + inputs: Vec, + memory_address_to_id_state: &mut memory_address_to_id::ClaimGenerator, + memory_id_to_big_state: &mut memory_id_to_big::ClaimGenerator, +) -> ( + [BaseColumn; N_TRACE_COLUMNS], + SubComponentInputs, + LookupData, +) { + const N_TRACE_COLUMNS: usize = 42; + 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_32769 = PackedM31::broadcast(M31::from(32769)); + let M31_511 = PackedM31::broadcast(M31::from(511)); + let M31_512 = PackedM31::broadcast(M31::from(512)); + let UInt16_1 = PackedUInt16::broadcast(UInt16::from(1)); + let UInt16_11 = PackedUInt16::broadcast(UInt16::from(11)); + let UInt16_127 = PackedUInt16::broadcast(UInt16::from(127)); + let UInt16_3 = PackedUInt16::broadcast(UInt16::from(3)); + let UInt16_6 = PackedUInt16::broadcast(UInt16::from(6)); + let UInt16_9 = PackedUInt16::broadcast(UInt16::from(9)); + + inputs.into_iter().enumerate().for_each( + |(row_index, jnz_opcode_is_taken_t_dst_base_fp_t_input)| { + let input_tmp_1208 = jnz_opcode_is_taken_t_dst_base_fp_t_input; + let input_pc_col0 = input_tmp_1208.pc; + trace[0].data[row_index] = input_pc_col0; + let input_ap_col1 = input_tmp_1208.ap; + trace[1].data[row_index] = input_ap_col1; + let input_fp_col2 = input_tmp_1208.fp; + trace[2].data[row_index] = input_fp_col2; + + // decode_instruction_113648125c3c3f56. + + let memory_address_to_id_value_tmp_1214 = + memory_address_to_id_state.deduce_output(input_pc_col0); + let memory_id_to_big_value_tmp_1215 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1214); + let offset0_tmp_1216 = + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1215.get_m31(0))) + + (((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1215.get_m31(1))) + & (UInt16_127)) + << (UInt16_9))); + let offset0_col3 = offset0_tmp_1216.as_m31(); + trace[3].data[row_index] = offset0_col3; + let ap_update_add_1_tmp_1217 = + (((((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1215.get_m31(5))) + >> (UInt16_3)) + + ((PackedUInt16::from_m31(memory_id_to_big_value_tmp_1215.get_m31(6))) + << (UInt16_6))) + >> (UInt16_11)) + & (UInt16_1)); + let ap_update_add_1_col4 = ap_update_add_1_tmp_1217.as_m31(); + trace[4].data[row_index] = ap_update_add_1_col4; + + sub_components_inputs.verify_instruction_inputs[0].extend( + ( + input_pc_col0, + [offset0_col3, M31_32767, M31_32769], + [ + M31_1, + M31_1, + M31_1, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_1, + M31_0, + ap_update_add_1_col4, + M31_0, + M31_0, + M31_0, + ], + ) + .unpack(), + ); + + lookup_data.verifyinstruction[0].push([ + input_pc_col0, + offset0_col3, + M31_32767, + M31_32769, + M31_1, + M31_1, + M31_1, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + M31_1, + M31_0, + ap_update_add_1_col4, + M31_0, + M31_0, + M31_0, + ]); + + // read_positive_num_bits_252. + + let memory_address_to_id_value_tmp_1219 = memory_address_to_id_state + .deduce_output(((input_fp_col2) + ((offset0_col3) - (M31_32768)))); + let memory_id_to_big_value_tmp_1220 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1219); + let dst_id_col5 = memory_address_to_id_value_tmp_1219; + trace[5].data[row_index] = dst_id_col5; + sub_components_inputs.memory_address_to_id_inputs[0] + .extend(((input_fp_col2) + ((offset0_col3) - (M31_32768))).unpack()); + + lookup_data.memoryaddresstoid[0].push([ + ((input_fp_col2) + ((offset0_col3) - (M31_32768))), + dst_id_col5, + ]); + let dst_limb_0_col6 = memory_id_to_big_value_tmp_1220.get_m31(0); + trace[6].data[row_index] = dst_limb_0_col6; + let dst_limb_1_col7 = memory_id_to_big_value_tmp_1220.get_m31(1); + trace[7].data[row_index] = dst_limb_1_col7; + let dst_limb_2_col8 = memory_id_to_big_value_tmp_1220.get_m31(2); + trace[8].data[row_index] = dst_limb_2_col8; + let dst_limb_3_col9 = memory_id_to_big_value_tmp_1220.get_m31(3); + trace[9].data[row_index] = dst_limb_3_col9; + let dst_limb_4_col10 = memory_id_to_big_value_tmp_1220.get_m31(4); + trace[10].data[row_index] = dst_limb_4_col10; + let dst_limb_5_col11 = memory_id_to_big_value_tmp_1220.get_m31(5); + trace[11].data[row_index] = dst_limb_5_col11; + let dst_limb_6_col12 = memory_id_to_big_value_tmp_1220.get_m31(6); + trace[12].data[row_index] = dst_limb_6_col12; + let dst_limb_7_col13 = memory_id_to_big_value_tmp_1220.get_m31(7); + trace[13].data[row_index] = dst_limb_7_col13; + let dst_limb_8_col14 = memory_id_to_big_value_tmp_1220.get_m31(8); + trace[14].data[row_index] = dst_limb_8_col14; + let dst_limb_9_col15 = memory_id_to_big_value_tmp_1220.get_m31(9); + trace[15].data[row_index] = dst_limb_9_col15; + let dst_limb_10_col16 = memory_id_to_big_value_tmp_1220.get_m31(10); + trace[16].data[row_index] = dst_limb_10_col16; + let dst_limb_11_col17 = memory_id_to_big_value_tmp_1220.get_m31(11); + trace[17].data[row_index] = dst_limb_11_col17; + let dst_limb_12_col18 = memory_id_to_big_value_tmp_1220.get_m31(12); + trace[18].data[row_index] = dst_limb_12_col18; + let dst_limb_13_col19 = memory_id_to_big_value_tmp_1220.get_m31(13); + trace[19].data[row_index] = dst_limb_13_col19; + let dst_limb_14_col20 = memory_id_to_big_value_tmp_1220.get_m31(14); + trace[20].data[row_index] = dst_limb_14_col20; + let dst_limb_15_col21 = memory_id_to_big_value_tmp_1220.get_m31(15); + trace[21].data[row_index] = dst_limb_15_col21; + let dst_limb_16_col22 = memory_id_to_big_value_tmp_1220.get_m31(16); + trace[22].data[row_index] = dst_limb_16_col22; + let dst_limb_17_col23 = memory_id_to_big_value_tmp_1220.get_m31(17); + trace[23].data[row_index] = dst_limb_17_col23; + let dst_limb_18_col24 = memory_id_to_big_value_tmp_1220.get_m31(18); + trace[24].data[row_index] = dst_limb_18_col24; + let dst_limb_19_col25 = memory_id_to_big_value_tmp_1220.get_m31(19); + trace[25].data[row_index] = dst_limb_19_col25; + let dst_limb_20_col26 = memory_id_to_big_value_tmp_1220.get_m31(20); + trace[26].data[row_index] = dst_limb_20_col26; + let dst_limb_21_col27 = memory_id_to_big_value_tmp_1220.get_m31(21); + trace[27].data[row_index] = dst_limb_21_col27; + let dst_limb_22_col28 = memory_id_to_big_value_tmp_1220.get_m31(22); + trace[28].data[row_index] = dst_limb_22_col28; + let dst_limb_23_col29 = memory_id_to_big_value_tmp_1220.get_m31(23); + trace[29].data[row_index] = dst_limb_23_col29; + let dst_limb_24_col30 = memory_id_to_big_value_tmp_1220.get_m31(24); + trace[30].data[row_index] = dst_limb_24_col30; + let dst_limb_25_col31 = memory_id_to_big_value_tmp_1220.get_m31(25); + trace[31].data[row_index] = dst_limb_25_col31; + let dst_limb_26_col32 = memory_id_to_big_value_tmp_1220.get_m31(26); + trace[32].data[row_index] = dst_limb_26_col32; + let dst_limb_27_col33 = memory_id_to_big_value_tmp_1220.get_m31(27); + trace[33].data[row_index] = dst_limb_27_col33; + sub_components_inputs.memory_id_to_big_inputs[0].extend(dst_id_col5.unpack()); + + lookup_data.memoryidtobig[0].push([ + dst_id_col5, + dst_limb_0_col6, + dst_limb_1_col7, + dst_limb_2_col8, + dst_limb_3_col9, + dst_limb_4_col10, + dst_limb_5_col11, + dst_limb_6_col12, + dst_limb_7_col13, + dst_limb_8_col14, + dst_limb_9_col15, + dst_limb_10_col16, + dst_limb_11_col17, + dst_limb_12_col18, + dst_limb_13_col19, + dst_limb_14_col20, + dst_limb_15_col21, + dst_limb_16_col22, + dst_limb_17_col23, + dst_limb_18_col24, + dst_limb_19_col25, + dst_limb_20_col26, + dst_limb_21_col27, + dst_limb_22_col28, + dst_limb_23_col29, + dst_limb_24_col30, + dst_limb_25_col31, + dst_limb_26_col32, + dst_limb_27_col33, + ]); + + let res_col34 = ((M31_1).div( + (((((((((((((((((((((((((((((M31_0) + (dst_limb_0_col6)) + + (dst_limb_1_col7)) + + (dst_limb_2_col8)) + + (dst_limb_3_col9)) + + (dst_limb_4_col10)) + + (dst_limb_5_col11)) + + (dst_limb_6_col12)) + + (dst_limb_7_col13)) + + (dst_limb_8_col14)) + + (dst_limb_9_col15)) + + (dst_limb_10_col16)) + + (dst_limb_11_col17)) + + (dst_limb_12_col18)) + + (dst_limb_13_col19)) + + (dst_limb_14_col20)) + + (dst_limb_15_col21)) + + (dst_limb_16_col22)) + + (dst_limb_17_col23)) + + (dst_limb_18_col24)) + + (dst_limb_19_col25)) + + (dst_limb_20_col26)) + + (dst_limb_21_col27)) + + (dst_limb_22_col28)) + + (dst_limb_23_col29)) + + (dst_limb_24_col30)) + + (dst_limb_25_col31)) + + (dst_limb_26_col32)) + + (dst_limb_27_col33)), + )); + trace[34].data[row_index] = res_col34; + let diff_from_p_tmp_1221 = ((dst_limb_0_col6) - (M31_1)); + let diff_from_p_tmp_1222 = ((dst_limb_21_col27) - (M31_136)); + let diff_from_p_tmp_1223 = ((dst_limb_27_col33) - (M31_256)); + let res_squares_col35 = ((M31_1).div( + (((((((((((((((((((((((((((((M31_0) + + ((diff_from_p_tmp_1221) * (diff_from_p_tmp_1221))) + + (dst_limb_1_col7)) + + (dst_limb_2_col8)) + + (dst_limb_3_col9)) + + (dst_limb_4_col10)) + + (dst_limb_5_col11)) + + (dst_limb_6_col12)) + + (dst_limb_7_col13)) + + (dst_limb_8_col14)) + + (dst_limb_9_col15)) + + (dst_limb_10_col16)) + + (dst_limb_11_col17)) + + (dst_limb_12_col18)) + + (dst_limb_13_col19)) + + (dst_limb_14_col20)) + + (dst_limb_15_col21)) + + (dst_limb_16_col22)) + + (dst_limb_17_col23)) + + (dst_limb_18_col24)) + + (dst_limb_19_col25)) + + (dst_limb_20_col26)) + + ((diff_from_p_tmp_1222) * (diff_from_p_tmp_1222))) + + (dst_limb_22_col28)) + + (dst_limb_23_col29)) + + (dst_limb_24_col30)) + + (dst_limb_25_col31)) + + (dst_limb_26_col32)) + + ((diff_from_p_tmp_1223) * (diff_from_p_tmp_1223))), + )); + trace[35].data[row_index] = res_squares_col35; + + // read_small. + + let memory_address_to_id_value_tmp_1224 = + memory_address_to_id_state.deduce_output(((input_pc_col0) + (M31_1))); + let memory_id_to_big_value_tmp_1225 = + memory_id_to_big_state.deduce_output(memory_address_to_id_value_tmp_1224); + let next_pc_id_col36 = memory_address_to_id_value_tmp_1224; + trace[36].data[row_index] = next_pc_id_col36; + sub_components_inputs.memory_address_to_id_inputs[1] + .extend(((input_pc_col0) + (M31_1)).unpack()); + + lookup_data.memoryaddresstoid[1].push([((input_pc_col0) + (M31_1)), next_pc_id_col36]); + + // cond_decode_small_sign. + + let msb_tmp_1226 = memory_id_to_big_value_tmp_1225.get_m31(27).eq(M31_256); + let msb_col37 = msb_tmp_1226.as_m31(); + trace[37].data[row_index] = msb_col37; + let mid_limbs_set_tmp_1227 = memory_id_to_big_value_tmp_1225.get_m31(20).eq(M31_511); + let mid_limbs_set_col38 = mid_limbs_set_tmp_1227.as_m31(); + trace[38].data[row_index] = mid_limbs_set_col38; + + let next_pc_limb_0_col39 = memory_id_to_big_value_tmp_1225.get_m31(0); + trace[39].data[row_index] = next_pc_limb_0_col39; + let next_pc_limb_1_col40 = memory_id_to_big_value_tmp_1225.get_m31(1); + trace[40].data[row_index] = next_pc_limb_1_col40; + let next_pc_limb_2_col41 = memory_id_to_big_value_tmp_1225.get_m31(2); + trace[41].data[row_index] = next_pc_limb_2_col41; + sub_components_inputs.memory_id_to_big_inputs[1].extend(next_pc_id_col36.unpack()); + + lookup_data.memoryidtobig[1].push([ + next_pc_id_col36, + next_pc_limb_0_col39, + next_pc_limb_1_col40, + next_pc_limb_2_col41, + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + ((mid_limbs_set_col38) * (M31_511)), + (((M31_136) * (msb_col37)) - (mid_limbs_set_col38)), + M31_0, + M31_0, + M31_0, + M31_0, + M31_0, + ((msb_col37) * (M31_256)), + ]); + + lookup_data.opcodes[0].push([input_pc_col0, input_ap_col1, input_fp_col2]); + lookup_data.opcodes[1].push([ + ((input_pc_col0) + + (((((next_pc_limb_0_col39) + ((next_pc_limb_1_col40) * (M31_512))) + + ((next_pc_limb_2_col41) * (M31_262144))) + - (msb_col37)) + - ((M31_134217728) * (mid_limbs_set_col38)))), + ((input_ap_col1) + (ap_update_add_1_col4)), + input_fp_col2, + ]); + }, + ); + + (trace, sub_components_inputs, lookup_data) +} + +pub struct LookupData { + pub memoryaddresstoid: [Vec<[PackedM31; 2]>; 2], + pub memoryidtobig: [Vec<[PackedM31; 29]>; 2], + pub opcodes: [Vec<[PackedM31; 3]>; 2], + pub verifyinstruction: [Vec<[PackedM31; 19]>; 1], +} +impl LookupData { + #[allow(unused_variables)] + fn with_capacity(capacity: usize) -> Self { + Self { + memoryaddresstoid: [Vec::with_capacity(capacity), Vec::with_capacity(capacity)], + memoryidtobig: [Vec::with_capacity(capacity), Vec::with_capacity(capacity)], + opcodes: [Vec::with_capacity(capacity), Vec::with_capacity(capacity)], + verifyinstruction: [Vec::with_capacity(capacity)], + } + } +} + +pub struct InteractionClaimGenerator { + pub n_calls: usize, + pub lookup_data: LookupData, +} +impl InteractionClaimGenerator { + pub fn write_interaction_trace( + self, + tree_builder: &mut TreeBuilder<'_, '_, SimdBackend, Blake2sMerkleChannel>, + memoryaddresstoid_lookup_elements: &relations::MemoryAddressToId, + memoryidtobig_lookup_elements: &relations::MemoryIdToBig, + opcodes_lookup_elements: &relations::Opcodes, + verifyinstruction_lookup_elements: &relations::VerifyInstruction, + ) -> InteractionClaim { + let log_size = std::cmp::max(self.n_calls.next_power_of_two().ilog2(), LOG_N_LANES); + let mut logup_gen = LogupTraceGenerator::new(log_size); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.verifyinstruction[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = verifyinstruction_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.memoryaddresstoid[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = memoryaddresstoid_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.memoryidtobig[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = memoryidtobig_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.memoryaddresstoid[1]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = memoryaddresstoid_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.memoryidtobig[1]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = memoryidtobig_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.opcodes[0]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = opcodes_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let mut col_gen = logup_gen.new_col(); + let lookup_row = &self.lookup_data.opcodes[1]; + for (i, lookup_values) in lookup_row.iter().enumerate() { + let denom = opcodes_lookup_elements.combine(lookup_values); + col_gen.write_frac(i, -PackedQM31::one(), denom); + } + col_gen.finalize_col(); + + let (trace, total_sum, claimed_sum) = if self.n_calls == 1 << log_size { + let (trace, claimed_sum) = logup_gen.finalize_last(); + (trace, claimed_sum, None) + } else { + let (trace, [total_sum, claimed_sum]) = + logup_gen.finalize_at([(1 << log_size) - 1, self.n_calls - 1]); + (trace, total_sum, Some((claimed_sum, self.n_calls - 1))) + }; + tree_builder.extend_evals(trace); + + InteractionClaim { + logup_sums: (total_sum, claimed_sum), + } + } +} diff --git a/stwo_cairo_prover/crates/prover/src/components/mod.rs b/stwo_cairo_prover/crates/prover/src/components/mod.rs index 043c15bb..492299f7 100644 --- a/stwo_cairo_prover/crates/prover/src/components/mod.rs +++ b/stwo_cairo_prover/crates/prover/src/components/mod.rs @@ -5,6 +5,10 @@ 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 jnz_opcode_is_taken_f_dst_base_fp_f; +pub mod jnz_opcode_is_taken_f_dst_base_fp_t; +pub mod jnz_opcode_is_taken_t_dst_base_fp_f; +pub mod jnz_opcode_is_taken_t_dst_base_fp_t; pub mod memory; pub mod range_check_vector; pub mod ret_opcode; diff --git a/stwo_cairo_prover/crates/prover/src/input/state_transitions.rs b/stwo_cairo_prover/crates/prover/src/input/state_transitions.rs index 53cf1039..af038d74 100644 --- a/stwo_cairo_prover/crates/prover/src/input/state_transitions.rs +++ b/stwo_cairo_prover/crates/prover/src/input/state_transitions.rs @@ -395,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);