triton_air/table/
op_stack.rs

1use constraint_circuit::ConstraintCircuitBuilder;
2use constraint_circuit::ConstraintCircuitMonad;
3use constraint_circuit::DualRowIndicator;
4use constraint_circuit::DualRowIndicator::CurrentAux;
5use constraint_circuit::DualRowIndicator::CurrentMain;
6use constraint_circuit::DualRowIndicator::NextAux;
7use constraint_circuit::DualRowIndicator::NextMain;
8use constraint_circuit::SingleRowIndicator;
9use constraint_circuit::SingleRowIndicator::Aux;
10use constraint_circuit::SingleRowIndicator::Main;
11use isa::op_stack::OpStackElement;
12use strum::EnumCount;
13use twenty_first::prelude::*;
14
15use crate::AIR;
16use crate::challenge_id::ChallengeId;
17use crate::cross_table_argument::CrossTableArg;
18use crate::cross_table_argument::LookupArg;
19use crate::cross_table_argument::PermArg;
20use crate::table_column::MasterAuxColumn;
21use crate::table_column::MasterMainColumn;
22
23/// The value indicating a padding row in the op stack table. Stored in the
24/// `ib1_shrink_stack` column.
25pub const PADDING_VALUE: BFieldElement = BFieldElement::new(2);
26
27#[derive(Debug, Copy, Clone, Eq, PartialEq)]
28pub struct OpStackTable;
29
30impl crate::private::Seal for OpStackTable {}
31
32impl AIR for OpStackTable {
33    type MainColumn = crate::table_column::OpStackMainColumn;
34    type AuxColumn = crate::table_column::OpStackAuxColumn;
35
36    fn initial_constraints(
37        circuit_builder: &ConstraintCircuitBuilder<SingleRowIndicator>,
38    ) -> Vec<ConstraintCircuitMonad<SingleRowIndicator>> {
39        let challenge = |c| circuit_builder.challenge(c);
40        let constant = |c| circuit_builder.b_constant(c);
41        let x_constant = |c| circuit_builder.x_constant(c);
42        let main_row =
43            |column: Self::MainColumn| circuit_builder.input(Main(column.master_main_index()));
44        let aux_row =
45            |column: Self::AuxColumn| circuit_builder.input(Aux(column.master_aux_index()));
46
47        let initial_stack_length = u32::try_from(OpStackElement::COUNT).unwrap();
48        let initial_stack_length = constant(initial_stack_length.into());
49        let padding_indicator = constant(PADDING_VALUE);
50
51        let stack_pointer_is_16 =
52            main_row(Self::MainColumn::StackPointer) - initial_stack_length.clone();
53
54        let compressed_row = challenge(ChallengeId::OpStackClkWeight)
55            * main_row(Self::MainColumn::CLK)
56            + challenge(ChallengeId::OpStackIb1Weight) * main_row(Self::MainColumn::IB1ShrinkStack)
57            + challenge(ChallengeId::OpStackPointerWeight) * initial_stack_length
58            + challenge(ChallengeId::OpStackFirstUnderflowElementWeight)
59                * main_row(Self::MainColumn::FirstUnderflowElement);
60        let rppa_initial = challenge(ChallengeId::OpStackIndeterminate) - compressed_row;
61        let rppa_has_accumulated_first_row =
62            aux_row(Self::AuxColumn::RunningProductPermArg) - rppa_initial;
63
64        let rppa_is_default_initial = aux_row(Self::AuxColumn::RunningProductPermArg)
65            - x_constant(PermArg::default_initial());
66
67        let first_row_is_padding_row =
68            main_row(Self::MainColumn::IB1ShrinkStack) - padding_indicator;
69        let first_row_is_not_padding_row = main_row(Self::MainColumn::IB1ShrinkStack)
70            * (main_row(Self::MainColumn::IB1ShrinkStack) - constant(bfe!(1)));
71
72        let rppa_starts_correctly = rppa_has_accumulated_first_row * first_row_is_padding_row
73            + rppa_is_default_initial * first_row_is_not_padding_row;
74
75        let lookup_argument_initial = x_constant(LookupArg::default_initial());
76        let clock_jump_diff_log_derivative_is_initialized_correctly =
77            aux_row(Self::AuxColumn::ClockJumpDifferenceLookupClientLogDerivative)
78                - lookup_argument_initial;
79
80        vec![
81            stack_pointer_is_16,
82            rppa_starts_correctly,
83            clock_jump_diff_log_derivative_is_initialized_correctly,
84        ]
85    }
86
87    fn consistency_constraints(
88        _circuit_builder: &ConstraintCircuitBuilder<SingleRowIndicator>,
89    ) -> Vec<ConstraintCircuitMonad<SingleRowIndicator>> {
90        // no further constraints
91        vec![]
92    }
93
94    fn transition_constraints(
95        circuit_builder: &ConstraintCircuitBuilder<DualRowIndicator>,
96    ) -> Vec<ConstraintCircuitMonad<DualRowIndicator>> {
97        let constant = |c| circuit_builder.b_constant(c);
98        let challenge = |c| circuit_builder.challenge(c);
99        let current_main_row = |column: Self::MainColumn| {
100            circuit_builder.input(CurrentMain(column.master_main_index()))
101        };
102        let current_aux_row =
103            |column: Self::AuxColumn| circuit_builder.input(CurrentAux(column.master_aux_index()));
104        let next_main_row =
105            |column: Self::MainColumn| circuit_builder.input(NextMain(column.master_main_index()));
106        let next_aux_row =
107            |column: Self::AuxColumn| circuit_builder.input(NextAux(column.master_aux_index()));
108
109        let one = constant(1_u32.into());
110        let padding_indicator = constant(PADDING_VALUE);
111
112        let clk = current_main_row(Self::MainColumn::CLK);
113        let ib1_shrink_stack = current_main_row(Self::MainColumn::IB1ShrinkStack);
114        let stack_pointer = current_main_row(Self::MainColumn::StackPointer);
115        let first_underflow_element = current_main_row(Self::MainColumn::FirstUnderflowElement);
116        let rppa = current_aux_row(Self::AuxColumn::RunningProductPermArg);
117        let clock_jump_diff_log_derivative =
118            current_aux_row(Self::AuxColumn::ClockJumpDifferenceLookupClientLogDerivative);
119
120        let clk_next = next_main_row(Self::MainColumn::CLK);
121        let ib1_shrink_stack_next = next_main_row(Self::MainColumn::IB1ShrinkStack);
122        let stack_pointer_next = next_main_row(Self::MainColumn::StackPointer);
123        let first_underflow_element_next = next_main_row(Self::MainColumn::FirstUnderflowElement);
124        let rppa_next = next_aux_row(Self::AuxColumn::RunningProductPermArg);
125        let clock_jump_diff_log_derivative_next =
126            next_aux_row(Self::AuxColumn::ClockJumpDifferenceLookupClientLogDerivative);
127
128        let stack_pointer_increases_by_1_or_does_not_change =
129            (stack_pointer_next.clone() - stack_pointer.clone() - one.clone())
130                * (stack_pointer_next.clone() - stack_pointer.clone());
131
132        let stack_pointer_inc_by_1_or_underflow_element_doesnt_change_or_next_ci_grows_stack =
133            (stack_pointer_next.clone() - stack_pointer.clone() - one.clone())
134                * (first_underflow_element_next.clone() - first_underflow_element.clone())
135                * ib1_shrink_stack_next.clone();
136
137        let next_row_is_padding_row = ib1_shrink_stack_next.clone() - padding_indicator.clone();
138        let if_current_row_is_padding_row_then_next_row_is_padding_row = ib1_shrink_stack.clone()
139            * (ib1_shrink_stack - one.clone())
140            * next_row_is_padding_row.clone();
141
142        // The running product for the permutation argument `rppa` is updated
143        // correctly.
144        let compressed_row = circuit_builder.challenge(ChallengeId::OpStackClkWeight)
145            * clk_next.clone()
146            + circuit_builder.challenge(ChallengeId::OpStackIb1Weight)
147                * ib1_shrink_stack_next.clone()
148            + circuit_builder.challenge(ChallengeId::OpStackPointerWeight)
149                * stack_pointer_next.clone()
150            + circuit_builder.challenge(ChallengeId::OpStackFirstUnderflowElementWeight)
151                * first_underflow_element_next;
152
153        let rppa_updates = rppa_next.clone()
154            - rppa.clone() * (challenge(ChallengeId::OpStackIndeterminate) - compressed_row);
155
156        let next_row_is_not_padding_row =
157            ib1_shrink_stack_next.clone() * (ib1_shrink_stack_next.clone() - one.clone());
158        let rppa_remains = rppa_next - rppa;
159
160        let rppa_updates_correctly = rppa_updates * next_row_is_padding_row.clone()
161            + rppa_remains * next_row_is_not_padding_row.clone();
162
163        let clk_diff = clk_next - clk;
164        let log_derivative_accumulates = (clock_jump_diff_log_derivative_next.clone()
165            - clock_jump_diff_log_derivative.clone())
166            * (challenge(ChallengeId::ClockJumpDifferenceLookupIndeterminate) - clk_diff)
167            - one.clone();
168        let log_derivative_remains =
169            clock_jump_diff_log_derivative_next.clone() - clock_jump_diff_log_derivative.clone();
170
171        let log_derivative_accumulates_or_stack_pointer_changes_or_next_row_is_padding_row =
172            log_derivative_accumulates
173                * (stack_pointer_next.clone() - stack_pointer.clone() - one.clone())
174                * next_row_is_padding_row;
175        let log_derivative_remains_or_stack_pointer_doesnt_change =
176            log_derivative_remains.clone() * (stack_pointer_next.clone() - stack_pointer.clone());
177        let log_derivatve_remains_or_next_row_is_not_padding_row =
178            log_derivative_remains * next_row_is_not_padding_row;
179
180        let log_derivative_updates_correctly =
181            log_derivative_accumulates_or_stack_pointer_changes_or_next_row_is_padding_row
182                + log_derivative_remains_or_stack_pointer_doesnt_change
183                + log_derivatve_remains_or_next_row_is_not_padding_row;
184
185        vec![
186            stack_pointer_increases_by_1_or_does_not_change,
187            stack_pointer_inc_by_1_or_underflow_element_doesnt_change_or_next_ci_grows_stack,
188            if_current_row_is_padding_row_then_next_row_is_padding_row,
189            rppa_updates_correctly,
190            log_derivative_updates_correctly,
191        ]
192    }
193
194    fn terminal_constraints(
195        _circuit_builder: &ConstraintCircuitBuilder<SingleRowIndicator>,
196    ) -> Vec<ConstraintCircuitMonad<SingleRowIndicator>> {
197        // no further constraints
198        vec![]
199    }
200}
triton_air/table/op_stack.rs

triton_air/table/
op_stack.rs
