Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

add_ap components #215

Merged
merged 1 commit into from
Dec 3, 2024
+2,133 −39
Merged

add_ap components #215

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
268 changes: 266 additions & 2 deletions stwo_cairo_prover/crates/prover/src/cairo_air/air.rs
View file
Open in desktop

Large diffs are not rendered by default.

211 changes: 211 additions & 0 deletions ...iro_prover/crates/prover/src/components/add_ap_opcode_is_imm_f_op1_base_fp_f/component.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,211 @@
#![allow(non_camel_case_types)]
#![allow(unused_imports)]
use num_traits::{One, Zero};
use serde::{Deserialize, Serialize};
use stwo_prover::constraint_framework::logup::{LogupAtRow, LogupSums, LookupElements};
use stwo_prover::constraint_framework::{
EvalAtRow, FrameworkComponent, FrameworkEval, RelationEntry,
};
use stwo_prover::core::backend::simd::m31::LOG_N_LANES;
use stwo_prover::core::channel::Channel;
use stwo_prover::core::fields::m31::M31;
use stwo_prover::core::fields::qm31::SecureField;
use stwo_prover::core::fields::secure_column::SECURE_EXTENSION_DEGREE;
use stwo_prover::core::pcs::TreeVec;

use crate::relations;

pub struct Eval {
pub claim: Claim,
pub memoryaddresstoid_lookup_elements: relations::MemoryAddressToId,
pub memoryidtobig_lookup_elements: relations::MemoryIdToBig,
pub opcodes_lookup_elements: relations::Opcodes,
pub verifyinstruction_lookup_elements: relations::VerifyInstruction,
}

#[derive(Copy, Clone, Serialize, Deserialize)]
pub struct Claim {
pub n_calls: usize,
}
impl Claim {
pub fn log_sizes(&self) -> TreeVec<Vec<u32>> {
let log_size = std::cmp::max(self.n_calls.next_power_of_two().ilog2(), LOG_N_LANES);
let trace_log_sizes = vec![log_size; 10];
let interaction_log_sizes = vec![log_size; SECURE_EXTENSION_DEGREE * 5];
let preprocessed_log_sizes = vec![log_size];
TreeVec::new(vec![
preprocessed_log_sizes,
trace_log_sizes,
interaction_log_sizes,
])
}

pub fn mix_into(&self, channel: &mut impl Channel) {
channel.mix_u64(self.n_calls as u64);
}
}

#[derive(Copy, Clone, Serialize, Deserialize)]
pub struct InteractionClaim {
pub logup_sums: LogupSums,
}
impl InteractionClaim {
pub fn mix_into(&self, channel: &mut impl Channel) {
let (total_sum, claimed_sum) = self.logup_sums;
channel.mix_felts(&[total_sum]);
if let Some(claimed_sum) = claimed_sum {
channel.mix_felts(&[claimed_sum.0]);
channel.mix_u64(claimed_sum.1 as u64);
}
}
}

pub type Component = FrameworkComponent<Eval>;

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<E: EvalAtRow>(&self, mut eval: E) -> E {
let M31_0 = E::F::from(M31::from(0));
let M31_1 = E::F::from(M31::from(1));
let M31_134217728 = E::F::from(M31::from(134217728));
let M31_136 = E::F::from(M31::from(136));
let M31_256 = E::F::from(M31::from(256));
let M31_262144 = E::F::from(M31::from(262144));
let M31_32767 = E::F::from(M31::from(32767));
let M31_32768 = E::F::from(M31::from(32768));
let M31_511 = E::F::from(M31::from(511));
let M31_512 = E::F::from(M31::from(512));
let input_pc_col0 = eval.next_trace_mask();
let input_ap_col1 = eval.next_trace_mask();
let input_fp_col2 = eval.next_trace_mask();
let offset2_col3 = eval.next_trace_mask();
let op1_id_col4 = eval.next_trace_mask();
let msb_col5 = eval.next_trace_mask();
let mid_limbs_set_col6 = eval.next_trace_mask();
let op1_limb_0_col7 = eval.next_trace_mask();
let op1_limb_1_col8 = eval.next_trace_mask();
let op1_limb_2_col9 = eval.next_trace_mask();

// decode_instruction_95ed11aea2bb2eff.

eval.add_to_relation(&[RelationEntry::new(
&self.verifyinstruction_lookup_elements,
E::EF::one(),
&[
input_pc_col0.clone(),
M31_32767.clone(),
M31_32767.clone(),
offset2_col3.clone(),
M31_1.clone(),
M31_1.clone(),
M31_0.clone(),
M31_0.clone(),
M31_1.clone(),
M31_0.clone(),
M31_0.clone(),
M31_0.clone(),
M31_0.clone(),
M31_0.clone(),
M31_1.clone(),
],
)]);

// read_small.

eval.add_to_relation(&[RelationEntry::new(
&self.memoryaddresstoid_lookup_elements,
E::EF::one(),
&[
(input_ap_col1.clone() + (offset2_col3.clone() - M31_32768.clone())),
op1_id_col4.clone(),
],
)]);

// cond_decode_small_sign.

// msb is a bit.
eval.add_constraint((msb_col5.clone() * (msb_col5.clone() - M31_1.clone())));
// mid_limbs_set is a bit.
eval.add_constraint(
(mid_limbs_set_col6.clone() * (mid_limbs_set_col6.clone() - M31_1.clone())),
);
// Cannot have msb equals 0 and mid_limbs_set equals 1.
eval.add_constraint(
((M31_1.clone() * mid_limbs_set_col6.clone()) * (msb_col5.clone() - M31_1.clone())),
);

eval.add_to_relation(&[RelationEntry::new(
&self.memoryidtobig_lookup_elements,
E::EF::one(),
&[
op1_id_col4.clone(),
op1_limb_0_col7.clone(),
op1_limb_1_col8.clone(),
op1_limb_2_col9.clone(),
(mid_limbs_set_col6.clone() * M31_511.clone()),
(mid_limbs_set_col6.clone() * M31_511.clone()),
(mid_limbs_set_col6.clone() * M31_511.clone()),
(mid_limbs_set_col6.clone() * M31_511.clone()),
(mid_limbs_set_col6.clone() * M31_511.clone()),
(mid_limbs_set_col6.clone() * M31_511.clone()),
(mid_limbs_set_col6.clone() * M31_511.clone()),
(mid_limbs_set_col6.clone() * M31_511.clone()),
(mid_limbs_set_col6.clone() * M31_511.clone()),
(mid_limbs_set_col6.clone() * M31_511.clone()),
(mid_limbs_set_col6.clone() * M31_511.clone()),
(mid_limbs_set_col6.clone() * M31_511.clone()),
(mid_limbs_set_col6.clone() * M31_511.clone()),
(mid_limbs_set_col6.clone() * M31_511.clone()),
(mid_limbs_set_col6.clone() * M31_511.clone()),
(mid_limbs_set_col6.clone() * M31_511.clone()),
(mid_limbs_set_col6.clone() * M31_511.clone()),
(mid_limbs_set_col6.clone() * M31_511.clone()),
((M31_136.clone() * msb_col5.clone()) - mid_limbs_set_col6.clone()),
M31_0.clone(),
M31_0.clone(),
M31_0.clone(),
M31_0.clone(),
M31_0.clone(),
(msb_col5.clone() * M31_256.clone()),
],
)]);

eval.add_to_relation(&[RelationEntry::new(
&self.opcodes_lookup_elements,
E::EF::one(),
&[
input_pc_col0.clone(),
input_ap_col1.clone(),
input_fp_col2.clone(),
],
)]);

eval.add_to_relation(&[RelationEntry::new(
&self.opcodes_lookup_elements,
-E::EF::one(),
&[
(input_pc_col0.clone() + M31_1.clone()),
(input_ap_col1.clone()
+ ((((op1_limb_0_col7.clone()
+ (op1_limb_1_col8.clone() * M31_512.clone()))
+ (op1_limb_2_col9.clone() * M31_262144.clone()))
- msb_col5.clone())
- (M31_134217728.clone() * mid_limbs_set_col6.clone()))),
input_fp_col2.clone(),
],
)]);

eval.finalize_logup();
eval
}
}
5 changes: 5 additions & 0 deletions stwo_cairo_prover/crates/prover/src/components/add_ap_opcode_is_imm_f_op1_base_fp_f/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
pub mod component;
pub mod prover;

pub use component::{Claim, Component, Eval, InteractionClaim};
pub use prover::{ClaimGenerator, InputType, InteractionClaimGenerator};
Loading
Loading