Skip to content

Commit cdac7c2

Browse files
author
Gilad Chase
committed
add addap
1 parent 3fae126 commit cdac7c2

File tree

5 files changed

+160
-2
lines changed

5 files changed

+160
-2
lines changed
Lines changed: 154 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,154 @@
1+
use num_traits::One;
2+
use serde::{Deserialize, Serialize};
3+
use stwo_prover::constraint_framework::logup::LogupSums;
4+
use stwo_prover::constraint_framework::{
5+
EvalAtRow, FrameworkComponent, FrameworkEval, RelationEntry,
6+
};
7+
use stwo_prover::core::backend::simd::m31::LOG_N_LANES;
8+
use stwo_prover::core::channel::Channel;
9+
use stwo_prover::core::fields::m31::{BaseField, M31};
10+
use stwo_prover::core::fields::secure_column::SECURE_EXTENSION_DEGREE;
11+
use stwo_prover::core::pcs::TreeVec;
12+
13+
use crate::relations::{MemoryRelation, StateRelation};
14+
use crate::utils::component::decode_opcode;
15+
use crate::utils::{Selector, SelectorTrait};
16+
17+
pub const ADD_AP_N_TRACE_CELLS: usize = 7;
18+
// TODO: organize opcodes so that deduce_opcode will actually work with this.
19+
// Opcode base should be: `addap_imm = K`
20+
// such that:
21+
// ```
22+
// jmp_abs_imm = K + 1
23+
// jmp_rel_imm = K + 2
24+
// ```
25+
pub const INSTRUCTION_BASE: M31 = M31::from_u32_unchecked(0);
26+
27+
pub type Component = FrameworkComponent<Eval>;
28+
29+
pub struct Eval {
30+
pub claim: Claim,
31+
pub memory_lookup: MemoryRelation,
32+
pub state_lookup: StateRelation,
33+
}
34+
35+
impl FrameworkEval for Eval {
36+
fn log_size(&self) -> u32 {
37+
std::cmp::max(self.claim.n_rows.next_power_of_two().ilog2(), LOG_N_LANES)
38+
}
39+
40+
fn max_constraint_log_degree_bound(&self) -> u32 {
41+
self.log_size() + 1
42+
}
43+
44+
fn evaluate<E: EvalAtRow>(&self, mut eval: E) -> E {
45+
let state = std::array::from_fn(|_| eval.next_trace_mask());
46+
// Use initial state.
47+
eval.add_to_relation(RelationEntry::new(&self.state_lookup, E::EF::one(), &state));
48+
let [pc, ap, fp] = state;
49+
50+
// Assert flag is in range.
51+
let opcode_type = eval.next_trace_mask();
52+
const ONE: BaseField = BaseField::from_u32_unchecked(1);
53+
const TWO: BaseField = BaseField::from_u32_unchecked(2);
54+
const THREE: BaseField = BaseField::from_u32_unchecked(3);
55+
// assert is_trit.
56+
eval.add_constraint(
57+
opcode_type.clone() * opcode_type.clone() * opcode_type.clone()
58+
- E::F::from(THREE) * opcode_type.clone() * opcode_type.clone()
59+
+ E::F::from(TWO) * opcode_type.clone(),
60+
);
61+
62+
// Check instruction.
63+
let opcode = decode_opcode(
64+
INSTRUCTION_BASE.into(),
65+
&[
66+
(opcode_type.clone(), 3), // [addap, jmp_abs, jmp_rel]
67+
],
68+
);
69+
70+
let imm = eval.next_trace_mask();
71+
72+
eval.add_to_relation(RelationEntry::new(
73+
&self.memory_lookup,
74+
E::EF::one(),
75+
&[pc.clone(), opcode.clone()],
76+
));
77+
78+
// Compute new pc and new ap.
79+
// NEW_PC = { addap: pc + 1, jmp_imm: imm, jmp_rel: pc + imm }[opcode_type]
80+
let new_pc = Selector::select(
81+
&opcode_type,
82+
[
83+
&(pc.clone() + E::F::one()),
84+
&imm,
85+
&(pc.clone() + imm.clone()),
86+
],
87+
);
88+
let new_pc_value = eval.next_trace_mask();
89+
eval.add_to_relation(RelationEntry::new(
90+
&self.memory_lookup,
91+
E::EF::one(),
92+
&[new_pc.clone(), new_pc_value.clone()],
93+
));
94+
95+
// NEW_AP = { addap: ap+imm, jmp_*: ap}[opcode_type]
96+
let new_ap = Selector::select(&opcode_type, [&(ap.clone() + imm.clone()), &ap, &ap]);
97+
let new_ap_value = eval.next_trace_mask();
98+
eval.add_to_relation(RelationEntry::new(
99+
&self.memory_lookup,
100+
E::EF::one(),
101+
&[new_ap.clone(), new_ap_value.clone()],
102+
));
103+
104+
// Yield final state.
105+
let new_state = [new_pc, new_ap, fp];
106+
eval.add_to_relation(RelationEntry::new(
107+
&self.state_lookup,
108+
-E::EF::one(),
109+
&new_state,
110+
));
111+
112+
eval.finalize_logup_in_pairs();
113+
eval
114+
}
115+
}
116+
117+
#[derive(Copy, Clone, Serialize, Deserialize)]
118+
pub struct Claim {
119+
pub n_rows: usize,
120+
}
121+
122+
impl Claim {
123+
pub fn log_sizes(&self) -> TreeVec<Vec<u32>> {
124+
let log_size = std::cmp::max(self.n_rows.next_power_of_two().ilog2(), LOG_N_LANES);
125+
let preprocessed_log_sizes = vec![log_size];
126+
let trace_log_sizes = vec![log_size; ADD_AP_N_TRACE_CELLS];
127+
let interaction_log_sizes = vec![log_size; SECURE_EXTENSION_DEGREE * 3];
128+
TreeVec::new(vec![
129+
preprocessed_log_sizes,
130+
trace_log_sizes,
131+
interaction_log_sizes,
132+
])
133+
}
134+
135+
pub fn mix_into(&self, channel: &mut impl Channel) {
136+
channel.mix_u64(self.n_rows as u64);
137+
}
138+
}
139+
140+
#[derive(Clone, Serialize, Deserialize)]
141+
pub struct InteractionClaim {
142+
pub log_size: u32,
143+
pub logup_sums: LogupSums,
144+
}
145+
impl InteractionClaim {
146+
pub fn mix_into(&self, channel: &mut impl Channel) {
147+
let (total_sum, claimed_sum) = self.logup_sums;
148+
channel.mix_felts(&[total_sum]);
149+
if let Some(claimed_sum) = claimed_sum {
150+
channel.mix_felts(&[claimed_sum.0]);
151+
channel.mix_u64(claimed_sum.1 as u64);
152+
}
153+
}
154+
}
Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
pub mod component;
2+
pub use component::{Claim, Component, Eval, InteractionClaim};

crates/prover/src/components/add_mul_opcode/component.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -161,7 +161,7 @@ impl Claim {
161161
}
162162

163163
pub fn log_sizes(&self) -> TreeVec<Vec<u32>> {
164-
let log_size = self.n_rows.next_power_of_two().ilog2();
164+
let log_size = std::cmp::max(self.n_rows.next_power_of_two().ilog2(), LOG_N_LANES);
165165
let preprocessed_log_sizes = vec![log_size];
166166
let interaction_1_log_sizes = vec![log_size; N_TRACE_COLUMNS];
167167
let interaction_2_log_sizes = vec![log_size; SECURE_EXTENSION_DEGREE * 3];

crates/prover/src/components/mod.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
pub mod add_ap_opcode;
12
pub mod add_mul_opcode;
23
pub mod memory;
34
pub mod ret_opcode;

crates/prover/src/components/ret_opcode/component.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ use serde::{Deserialize, Serialize};
33
use stwo_prover::constraint_framework::{
44
EvalAtRow, FrameworkComponent, FrameworkEval, RelationEntry,
55
};
6+
use stwo_prover::core::backend::simd::m31::LOG_N_LANES;
67
use stwo_prover::core::channel::Channel;
78
use stwo_prover::core::fields::m31::M31;
89
use stwo_prover::core::fields::qm31::SecureField;
@@ -91,7 +92,7 @@ impl Claim {
9192
}
9293

9394
pub fn log_sizes(&self) -> TreeVec<Vec<u32>> {
94-
let log_size = self.n_rows.next_power_of_two().ilog2();
95+
let log_size = std::cmp::max(self.n_rows.next_power_of_two().ilog2(), LOG_N_LANES);
9596
let interaction_0_log_sizes = vec![log_size; RET_N_TRACE_CELLS];
9697
let interaction_1_log_sizes = vec![log_size; SECURE_EXTENSION_DEGREE * 3];
9798
let fixed_log_sizes = vec![log_size];

0 commit comments

Comments
 (0)