Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
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
7 changes: 3 additions & 4 deletions stwo_cairo_prover/crates/adapter/src/adapter.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
use anyhow::Result;
use cairo_vm::vm::runners::cairo_runner::CairoRunner;
use itertools::Itertools;
use stwo_cairo_common::preprocessed_columns::program::PROGRAM_LOG_LEN_BOUND;
use tracing::{info, span, Level};

use super::memory::{MemoryBuilder, MemoryConfig};
Expand Down Expand Up @@ -45,12 +46,10 @@ pub fn adapt(runner: &CairoRunner) -> Result<ProverInput> {
// Compute program segment.
let initial_pc = state_transitions.initial_state.pc.0;
let initial_ap = state_transitions.initial_state.ap.0;
// The verify_program builtin covers the program segment (initial_pc to initial_ap - 2).
// It is not a standard cairo_vm builtin, so we set it manually.
let program_length = (initial_ap - 2 - initial_pc) as usize;

builtin_segments.verify_program = Some(MemorySegmentAddresses {
begin_addr: initial_pc as usize,
stop_ptr: initial_pc as usize + program_length,
Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Missing validation that program fits within bound

Medium Severity

The old code dynamically sized the preprocessed column via data.len().next_power_of_two(), accommodating any program length. The new code hardcodes the column length to 1 << PROGRAM_LOG_LEN_BOUND (4096) but never validates that the actual program length (initial_ap - 2 - initial_pc) fits within this bound. If a program exceeds 4096 entries, ProgramColumn::new silently truncates the data while get_program_len() returns the full length, causing deduce_output to set cond=1 for indices beyond the preprocessed column — a mismatch that could lead to proof failures or incomplete program verification.

Additional Locations (1)
Fix in Cursor Fix in Web

stop_ptr: initial_pc as usize + (1 << PROGRAM_LOG_LEN_BOUND),
});

let program = (initial_pc..initial_ap - 2)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -136,6 +136,9 @@ impl FrameworkEval for Eval {
let curr_program_27 = eval.get_preprocessed_column(PreProcessedColumnId {
id: "curr_program_27".to_owned(),
});
let curr_program_28 = eval.get_preprocessed_column(PreProcessedColumnId {
id: "curr_program_28".to_owned(),
});
let multiplicity_0_col0 = eval.next_trace_mask();

eval.add_to_relation(RelationEntry::new(
Expand Down Expand Up @@ -172,6 +175,7 @@ impl FrameworkEval for Eval {
curr_program_25.clone(),
curr_program_26.clone(),
curr_program_27.clone(),
curr_program_28.clone(),
],
));

Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,241 @@
// This file was created by the AIR team.

use crate::components::prelude::*;
use crate::components::subroutines::read_positive_num_bits_252::ReadPositiveNumBits252;

#[derive(Copy, Clone, Serialize, Deserialize, CairoSerialize)]
pub struct MemVerifyCond {}

impl MemVerifyCond {
#[allow(unused_parens)]
#[allow(clippy::double_parens)]
#[allow(non_snake_case)]
#[allow(clippy::unused_unit)]
#[allow(unused_variables)]
#[allow(clippy::too_many_arguments)]
pub fn evaluate<E: EvalAtRow>(
[mem_verify_cond_input_address, mem_verify_cond_input_value_limb_0, mem_verify_cond_input_value_limb_1, mem_verify_cond_input_value_limb_2, mem_verify_cond_input_value_limb_3, mem_verify_cond_input_value_limb_4, mem_verify_cond_input_value_limb_5, mem_verify_cond_input_value_limb_6, mem_verify_cond_input_value_limb_7, mem_verify_cond_input_value_limb_8, mem_verify_cond_input_value_limb_9, mem_verify_cond_input_value_limb_10, mem_verify_cond_input_value_limb_11, mem_verify_cond_input_value_limb_12, mem_verify_cond_input_value_limb_13, mem_verify_cond_input_value_limb_14, mem_verify_cond_input_value_limb_15, mem_verify_cond_input_value_limb_16, mem_verify_cond_input_value_limb_17, mem_verify_cond_input_value_limb_18, mem_verify_cond_input_value_limb_19, mem_verify_cond_input_value_limb_20, mem_verify_cond_input_value_limb_21, mem_verify_cond_input_value_limb_22, mem_verify_cond_input_value_limb_23, mem_verify_cond_input_value_limb_24, mem_verify_cond_input_value_limb_25, mem_verify_cond_input_value_limb_26, mem_verify_cond_input_value_limb_27, mem_verify_cond_input_cond]: [E::F; 30],
cond_address_col0: E::F,
cond_address_id_col1: E::F,
cond_address_limb_0_col2: E::F,
cond_address_limb_1_col3: E::F,
cond_address_limb_2_col4: E::F,
cond_address_limb_3_col5: E::F,
cond_address_limb_4_col6: E::F,
cond_address_limb_5_col7: E::F,
cond_address_limb_6_col8: E::F,
cond_address_limb_7_col9: E::F,
cond_address_limb_8_col10: E::F,
cond_address_limb_9_col11: E::F,
cond_address_limb_10_col12: E::F,
cond_address_limb_11_col13: E::F,
cond_address_limb_12_col14: E::F,
cond_address_limb_13_col15: E::F,
cond_address_limb_14_col16: E::F,
cond_address_limb_15_col17: E::F,
cond_address_limb_16_col18: E::F,
cond_address_limb_17_col19: E::F,
cond_address_limb_18_col20: E::F,
cond_address_limb_19_col21: E::F,
cond_address_limb_20_col22: E::F,
cond_address_limb_21_col23: E::F,
cond_address_limb_22_col24: E::F,
cond_address_limb_23_col25: E::F,
cond_address_limb_24_col26: E::F,
cond_address_limb_25_col27: E::F,
cond_address_limb_26_col28: E::F,
cond_address_limb_27_col29: E::F,
common_lookup_elements: &relations::CommonLookupElements,
eval: &mut E,
) -> [E::F; 0] {
let M31_1 = E::F::from(M31::from(1));

// cond=0 or cond=1..
eval.add_constraint(
(mem_verify_cond_input_cond.clone()
* (M31_1.clone() - mem_verify_cond_input_cond.clone())),
);
// cond_address.
eval.add_constraint(
(cond_address_col0.clone()
- (((mem_verify_cond_input_address.clone() - M31_1.clone())
* mem_verify_cond_input_cond.clone())
+ M31_1.clone())),
);
ReadPositiveNumBits252::evaluate(
[cond_address_col0.clone()],
cond_address_id_col1.clone(),
cond_address_limb_0_col2.clone(),
cond_address_limb_1_col3.clone(),
cond_address_limb_2_col4.clone(),
cond_address_limb_3_col5.clone(),
cond_address_limb_4_col6.clone(),
cond_address_limb_5_col7.clone(),
cond_address_limb_6_col8.clone(),
cond_address_limb_7_col9.clone(),
cond_address_limb_8_col10.clone(),
cond_address_limb_9_col11.clone(),
cond_address_limb_10_col12.clone(),
cond_address_limb_11_col13.clone(),
cond_address_limb_12_col14.clone(),
cond_address_limb_13_col15.clone(),
cond_address_limb_14_col16.clone(),
cond_address_limb_15_col17.clone(),
cond_address_limb_16_col18.clone(),
cond_address_limb_17_col19.clone(),
cond_address_limb_18_col20.clone(),
cond_address_limb_19_col21.clone(),
cond_address_limb_20_col22.clone(),
cond_address_limb_21_col23.clone(),
cond_address_limb_22_col24.clone(),
cond_address_limb_23_col25.clone(),
cond_address_limb_24_col26.clone(),
cond_address_limb_25_col27.clone(),
cond_address_limb_26_col28.clone(),
cond_address_limb_27_col29.clone(),
common_lookup_elements,
eval,
);
// felt252 limb is zero.
eval.add_constraint(
((cond_address_limb_0_col2.clone() - mem_verify_cond_input_value_limb_0.clone())
* mem_verify_cond_input_cond.clone()),
);
// felt252 limb is zero.
eval.add_constraint(
((cond_address_limb_1_col3.clone() - mem_verify_cond_input_value_limb_1.clone())
* mem_verify_cond_input_cond.clone()),
);
// felt252 limb is zero.
eval.add_constraint(
((cond_address_limb_2_col4.clone() - mem_verify_cond_input_value_limb_2.clone())
* mem_verify_cond_input_cond.clone()),
);
// felt252 limb is zero.
eval.add_constraint(
((cond_address_limb_3_col5.clone() - mem_verify_cond_input_value_limb_3.clone())
* mem_verify_cond_input_cond.clone()),
);
// felt252 limb is zero.
eval.add_constraint(
((cond_address_limb_4_col6.clone() - mem_verify_cond_input_value_limb_4.clone())
* mem_verify_cond_input_cond.clone()),
);
// felt252 limb is zero.
eval.add_constraint(
((cond_address_limb_5_col7.clone() - mem_verify_cond_input_value_limb_5.clone())
* mem_verify_cond_input_cond.clone()),
);
// felt252 limb is zero.
eval.add_constraint(
((cond_address_limb_6_col8.clone() - mem_verify_cond_input_value_limb_6.clone())
* mem_verify_cond_input_cond.clone()),
);
// felt252 limb is zero.
eval.add_constraint(
((cond_address_limb_7_col9.clone() - mem_verify_cond_input_value_limb_7.clone())
* mem_verify_cond_input_cond.clone()),
);
// felt252 limb is zero.
eval.add_constraint(
((cond_address_limb_8_col10.clone() - mem_verify_cond_input_value_limb_8.clone())
* mem_verify_cond_input_cond.clone()),
);
// felt252 limb is zero.
eval.add_constraint(
((cond_address_limb_9_col11.clone() - mem_verify_cond_input_value_limb_9.clone())
* mem_verify_cond_input_cond.clone()),
);
// felt252 limb is zero.
eval.add_constraint(
((cond_address_limb_10_col12.clone() - mem_verify_cond_input_value_limb_10.clone())
* mem_verify_cond_input_cond.clone()),
);
// felt252 limb is zero.
eval.add_constraint(
((cond_address_limb_11_col13.clone() - mem_verify_cond_input_value_limb_11.clone())
* mem_verify_cond_input_cond.clone()),
);
// felt252 limb is zero.
eval.add_constraint(
((cond_address_limb_12_col14.clone() - mem_verify_cond_input_value_limb_12.clone())
* mem_verify_cond_input_cond.clone()),
);
// felt252 limb is zero.
eval.add_constraint(
((cond_address_limb_13_col15.clone() - mem_verify_cond_input_value_limb_13.clone())
* mem_verify_cond_input_cond.clone()),
);
// felt252 limb is zero.
eval.add_constraint(
((cond_address_limb_14_col16.clone() - mem_verify_cond_input_value_limb_14.clone())
* mem_verify_cond_input_cond.clone()),
);
// felt252 limb is zero.
eval.add_constraint(
((cond_address_limb_15_col17.clone() - mem_verify_cond_input_value_limb_15.clone())
* mem_verify_cond_input_cond.clone()),
);
// felt252 limb is zero.
eval.add_constraint(
((cond_address_limb_16_col18.clone() - mem_verify_cond_input_value_limb_16.clone())
* mem_verify_cond_input_cond.clone()),
);
// felt252 limb is zero.
eval.add_constraint(
((cond_address_limb_17_col19.clone() - mem_verify_cond_input_value_limb_17.clone())
* mem_verify_cond_input_cond.clone()),
);
// felt252 limb is zero.
eval.add_constraint(
((cond_address_limb_18_col20.clone() - mem_verify_cond_input_value_limb_18.clone())
* mem_verify_cond_input_cond.clone()),
);
// felt252 limb is zero.
eval.add_constraint(
((cond_address_limb_19_col21.clone() - mem_verify_cond_input_value_limb_19.clone())
* mem_verify_cond_input_cond.clone()),
);
// felt252 limb is zero.
eval.add_constraint(
((cond_address_limb_20_col22.clone() - mem_verify_cond_input_value_limb_20.clone())
* mem_verify_cond_input_cond.clone()),
);
// felt252 limb is zero.
eval.add_constraint(
((cond_address_limb_21_col23.clone() - mem_verify_cond_input_value_limb_21.clone())
* mem_verify_cond_input_cond.clone()),
);
// felt252 limb is zero.
eval.add_constraint(
((cond_address_limb_22_col24.clone() - mem_verify_cond_input_value_limb_22.clone())
* mem_verify_cond_input_cond.clone()),
);
// felt252 limb is zero.
eval.add_constraint(
((cond_address_limb_23_col25.clone() - mem_verify_cond_input_value_limb_23.clone())
* mem_verify_cond_input_cond.clone()),
);
// felt252 limb is zero.
eval.add_constraint(
((cond_address_limb_24_col26.clone() - mem_verify_cond_input_value_limb_24.clone())
* mem_verify_cond_input_cond.clone()),
);
// felt252 limb is zero.
eval.add_constraint(
((cond_address_limb_25_col27.clone() - mem_verify_cond_input_value_limb_25.clone())
* mem_verify_cond_input_cond.clone()),
);
// felt252 limb is zero.
eval.add_constraint(
((cond_address_limb_26_col28.clone() - mem_verify_cond_input_value_limb_26.clone())
* mem_verify_cond_input_cond.clone()),
);
// felt252 limb is zero.
eval.add_constraint(
((cond_address_limb_27_col29.clone() - mem_verify_cond_input_value_limb_27.clone())
* mem_verify_cond_input_cond.clone()),
);
[]
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,7 @@ pub mod linear_combination_n_4_coefs_4_2_m2_1;
pub mod linear_combination_n_6_coefs_4_2_3_1_m1_1;
pub mod mem_cond_verify_equal_known_id;
pub mod mem_verify;
pub mod mem_verify_cond;
pub mod mem_verify_equal;
pub mod mod_utils;
pub mod mod_words_to_12_bit_array;
Expand Down
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
// This file was created by the AIR team.

use crate::components::prelude::*;
use crate::components::subroutines::mem_verify::MemVerify;
use crate::components::subroutines::mem_verify_cond::MemVerifyCond;

pub const N_TRACE_COLUMNS: usize = 29;
pub const N_TRACE_COLUMNS: usize = 59;
pub const RELATION_USES_PER_ROW: [RelationUse; 3] = [
RelationUse {
relation_id: "MemoryAddressToId",
Expand Down Expand Up @@ -98,7 +98,37 @@ impl FrameworkEval for Eval {
let program_component_output_limb_25_col25 = eval.next_trace_mask();
let program_component_output_limb_26_col26 = eval.next_trace_mask();
let program_component_output_limb_27_col27 = eval.next_trace_mask();
let address_id_col28 = eval.next_trace_mask();
let program_component_output_limb_28_col28 = eval.next_trace_mask();
let cond_address_col29 = eval.next_trace_mask();
let cond_address_id_col30 = eval.next_trace_mask();
let cond_address_limb_0_col31 = eval.next_trace_mask();
let cond_address_limb_1_col32 = eval.next_trace_mask();
let cond_address_limb_2_col33 = eval.next_trace_mask();
let cond_address_limb_3_col34 = eval.next_trace_mask();
let cond_address_limb_4_col35 = eval.next_trace_mask();
let cond_address_limb_5_col36 = eval.next_trace_mask();
let cond_address_limb_6_col37 = eval.next_trace_mask();
let cond_address_limb_7_col38 = eval.next_trace_mask();
let cond_address_limb_8_col39 = eval.next_trace_mask();
let cond_address_limb_9_col40 = eval.next_trace_mask();
let cond_address_limb_10_col41 = eval.next_trace_mask();
let cond_address_limb_11_col42 = eval.next_trace_mask();
let cond_address_limb_12_col43 = eval.next_trace_mask();
let cond_address_limb_13_col44 = eval.next_trace_mask();
let cond_address_limb_14_col45 = eval.next_trace_mask();
let cond_address_limb_15_col46 = eval.next_trace_mask();
let cond_address_limb_16_col47 = eval.next_trace_mask();
let cond_address_limb_17_col48 = eval.next_trace_mask();
let cond_address_limb_18_col49 = eval.next_trace_mask();
let cond_address_limb_19_col50 = eval.next_trace_mask();
let cond_address_limb_20_col51 = eval.next_trace_mask();
let cond_address_limb_21_col52 = eval.next_trace_mask();
let cond_address_limb_22_col53 = eval.next_trace_mask();
let cond_address_limb_23_col54 = eval.next_trace_mask();
let cond_address_limb_24_col55 = eval.next_trace_mask();
let cond_address_limb_25_col56 = eval.next_trace_mask();
let cond_address_limb_26_col57 = eval.next_trace_mask();
let cond_address_limb_27_col58 = eval.next_trace_mask();
Comment thread
cursor[bot] marked this conversation as resolved.

eval.add_to_relation(RelationEntry::new(
&self.common_lookup_elements,
Expand Down Expand Up @@ -134,10 +164,11 @@ impl FrameworkEval for Eval {
program_component_output_limb_25_col25.clone(),
program_component_output_limb_26_col26.clone(),
program_component_output_limb_27_col27.clone(),
program_component_output_limb_28_col28.clone(),
],
));

MemVerify::evaluate(
MemVerifyCond::evaluate(
[
(E::F::from(M31::from(self.claim.verify_program_segment_start)) + seq.clone()),
program_component_output_limb_0_col0.clone(),
Expand Down Expand Up @@ -168,8 +199,38 @@ impl FrameworkEval for Eval {
program_component_output_limb_25_col25.clone(),
program_component_output_limb_26_col26.clone(),
program_component_output_limb_27_col27.clone(),
program_component_output_limb_28_col28.clone(),
],
address_id_col28.clone(),
cond_address_col29.clone(),
cond_address_id_col30.clone(),
cond_address_limb_0_col31.clone(),
cond_address_limb_1_col32.clone(),
cond_address_limb_2_col33.clone(),
cond_address_limb_3_col34.clone(),
cond_address_limb_4_col35.clone(),
cond_address_limb_5_col36.clone(),
cond_address_limb_6_col37.clone(),
cond_address_limb_7_col38.clone(),
cond_address_limb_8_col39.clone(),
cond_address_limb_9_col40.clone(),
cond_address_limb_10_col41.clone(),
cond_address_limb_11_col42.clone(),
cond_address_limb_12_col43.clone(),
cond_address_limb_13_col44.clone(),
cond_address_limb_14_col45.clone(),
cond_address_limb_15_col46.clone(),
cond_address_limb_16_col47.clone(),
cond_address_limb_17_col48.clone(),
cond_address_limb_18_col49.clone(),
cond_address_limb_19_col50.clone(),
cond_address_limb_20_col51.clone(),
cond_address_limb_21_col52.clone(),
cond_address_limb_22_col53.clone(),
cond_address_limb_23_col54.clone(),
cond_address_limb_24_col55.clone(),
cond_address_limb_25_col56.clone(),
cond_address_limb_26_col57.clone(),
cond_address_limb_27_col58.clone(),
&self.common_lookup_elements,
&mut eval,
);
Expand Down
Loading
Loading