triton_air/table/
program.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 twenty_first::prelude::*;
12
13use crate::AIR;
14use crate::challenge_id::ChallengeId;
15use crate::cross_table_argument::CrossTableArg;
16use crate::cross_table_argument::EvalArg;
17use crate::cross_table_argument::LookupArg;
18use crate::table_column::MasterAuxColumn;
19use crate::table_column::MasterMainColumn;
20
21#[derive(Debug, Copy, Clone, Eq, PartialEq)]
22pub struct ProgramTable;
23
24impl crate::private::Seal for ProgramTable {}
25
26impl AIR for ProgramTable {
27    type MainColumn = crate::table_column::ProgramMainColumn;
28    type AuxColumn = crate::table_column::ProgramAuxColumn;
29
30    fn initial_constraints(
31        circuit_builder: &ConstraintCircuitBuilder<SingleRowIndicator>,
32    ) -> Vec<ConstraintCircuitMonad<SingleRowIndicator>> {
33        let challenge = |c| circuit_builder.challenge(c);
34        let x_constant = |xfe| circuit_builder.x_constant(xfe);
35        let main_row = |col: Self::MainColumn| circuit_builder.input(Main(col.master_main_index()));
36        let aux_row = |col: Self::AuxColumn| circuit_builder.input(Aux(col.master_aux_index()));
37
38        let address = main_row(Self::MainColumn::Address);
39        let instruction = main_row(Self::MainColumn::Instruction);
40        let index_in_chunk = main_row(Self::MainColumn::IndexInChunk);
41        let is_hash_input_padding = main_row(Self::MainColumn::IsHashInputPadding);
42        let instruction_lookup_log_derivative =
43            aux_row(Self::AuxColumn::InstructionLookupServerLogDerivative);
44        let prepare_chunk_running_evaluation =
45            aux_row(Self::AuxColumn::PrepareChunkRunningEvaluation);
46        let send_chunk_running_evaluation = aux_row(Self::AuxColumn::SendChunkRunningEvaluation);
47
48        let lookup_arg_initial = x_constant(LookupArg::default_initial());
49        let eval_arg_initial = x_constant(EvalArg::default_initial());
50
51        let program_attestation_prepare_chunk_indeterminate =
52            challenge(ChallengeId::ProgramAttestationPrepareChunkIndeterminate);
53
54        let first_address_is_zero = address;
55        let index_in_chunk_is_zero = index_in_chunk;
56        let hash_input_padding_indicator_is_zero = is_hash_input_padding;
57
58        let instruction_lookup_log_derivative_is_initialized_correctly =
59            instruction_lookup_log_derivative - lookup_arg_initial;
60
61        let prepare_chunk_running_evaluation_has_absorbed_first_instruction =
62            prepare_chunk_running_evaluation
63                - eval_arg_initial.clone() * program_attestation_prepare_chunk_indeterminate
64                - instruction;
65
66        let send_chunk_running_evaluation_is_default_initial =
67            send_chunk_running_evaluation - eval_arg_initial;
68
69        vec![
70            first_address_is_zero,
71            index_in_chunk_is_zero,
72            hash_input_padding_indicator_is_zero,
73            instruction_lookup_log_derivative_is_initialized_correctly,
74            prepare_chunk_running_evaluation_has_absorbed_first_instruction,
75            send_chunk_running_evaluation_is_default_initial,
76        ]
77    }
78
79    fn consistency_constraints(
80        circuit_builder: &ConstraintCircuitBuilder<SingleRowIndicator>,
81    ) -> Vec<ConstraintCircuitMonad<SingleRowIndicator>> {
82        let constant = |c: u32| circuit_builder.b_constant(c);
83        let main_row = |col: Self::MainColumn| circuit_builder.input(Main(col.master_main_index()));
84
85        let one = constant(1);
86        let max_index_in_chunk = constant((Tip5::RATE - 1).try_into().unwrap());
87
88        let index_in_chunk = main_row(Self::MainColumn::IndexInChunk);
89        let max_minus_index_in_chunk_inv = main_row(Self::MainColumn::MaxMinusIndexInChunkInv);
90        let is_hash_input_padding = main_row(Self::MainColumn::IsHashInputPadding);
91        let is_table_padding = main_row(Self::MainColumn::IsTablePadding);
92
93        let max_minus_index_in_chunk = max_index_in_chunk - index_in_chunk;
94        let max_minus_index_in_chunk_inv_is_zero_or_the_inverse_of_max_minus_index_in_chunk =
95            (one.clone() - max_minus_index_in_chunk.clone() * max_minus_index_in_chunk_inv.clone())
96                * max_minus_index_in_chunk_inv.clone();
97        let max_minus_index_in_chunk_is_zero_or_the_inverse_of_max_minus_index_in_chunk_inv =
98            (one.clone() - max_minus_index_in_chunk.clone() * max_minus_index_in_chunk_inv)
99                * max_minus_index_in_chunk;
100
101        let is_hash_input_padding_is_bit =
102            is_hash_input_padding.clone() * (is_hash_input_padding - one.clone());
103        let is_table_padding_is_bit = is_table_padding.clone() * (is_table_padding - one);
104
105        vec![
106            max_minus_index_in_chunk_inv_is_zero_or_the_inverse_of_max_minus_index_in_chunk,
107            max_minus_index_in_chunk_is_zero_or_the_inverse_of_max_minus_index_in_chunk_inv,
108            is_hash_input_padding_is_bit,
109            is_table_padding_is_bit,
110        ]
111    }
112
113    fn transition_constraints(
114        circuit_builder: &ConstraintCircuitBuilder<DualRowIndicator>,
115    ) -> Vec<ConstraintCircuitMonad<DualRowIndicator>> {
116        let challenge = |c| circuit_builder.challenge(c);
117        let constant = |c: u64| circuit_builder.b_constant(c);
118
119        let current_main_row =
120            |col: Self::MainColumn| circuit_builder.input(CurrentMain(col.master_main_index()));
121        let next_main_row =
122            |col: Self::MainColumn| circuit_builder.input(NextMain(col.master_main_index()));
123        let current_aux_row =
124            |col: Self::AuxColumn| circuit_builder.input(CurrentAux(col.master_aux_index()));
125        let next_aux_row =
126            |col: Self::AuxColumn| circuit_builder.input(NextAux(col.master_aux_index()));
127
128        let one = constant(1);
129        let rate_minus_one = constant(u64::try_from(Tip5::RATE).unwrap() - 1);
130
131        let prepare_chunk_indeterminate =
132            challenge(ChallengeId::ProgramAttestationPrepareChunkIndeterminate);
133        let send_chunk_indeterminate =
134            challenge(ChallengeId::ProgramAttestationSendChunkIndeterminate);
135
136        let address = current_main_row(Self::MainColumn::Address);
137        let instruction = current_main_row(Self::MainColumn::Instruction);
138        let lookup_multiplicity = current_main_row(Self::MainColumn::LookupMultiplicity);
139        let index_in_chunk = current_main_row(Self::MainColumn::IndexInChunk);
140        let max_minus_index_in_chunk_inv =
141            current_main_row(Self::MainColumn::MaxMinusIndexInChunkInv);
142        let is_hash_input_padding = current_main_row(Self::MainColumn::IsHashInputPadding);
143        let is_table_padding = current_main_row(Self::MainColumn::IsTablePadding);
144        let log_derivative = current_aux_row(Self::AuxColumn::InstructionLookupServerLogDerivative);
145        let prepare_chunk_running_evaluation =
146            current_aux_row(Self::AuxColumn::PrepareChunkRunningEvaluation);
147        let send_chunk_running_evaluation =
148            current_aux_row(Self::AuxColumn::SendChunkRunningEvaluation);
149
150        let address_next = next_main_row(Self::MainColumn::Address);
151        let instruction_next = next_main_row(Self::MainColumn::Instruction);
152        let index_in_chunk_next = next_main_row(Self::MainColumn::IndexInChunk);
153        let max_minus_index_in_chunk_inv_next =
154            next_main_row(Self::MainColumn::MaxMinusIndexInChunkInv);
155        let is_hash_input_padding_next = next_main_row(Self::MainColumn::IsHashInputPadding);
156        let is_table_padding_next = next_main_row(Self::MainColumn::IsTablePadding);
157        let log_derivative_next =
158            next_aux_row(Self::AuxColumn::InstructionLookupServerLogDerivative);
159        let prepare_chunk_running_evaluation_next =
160            next_aux_row(Self::AuxColumn::PrepareChunkRunningEvaluation);
161        let send_chunk_running_evaluation_next =
162            next_aux_row(Self::AuxColumn::SendChunkRunningEvaluation);
163
164        let address_increases_by_one = address_next - (address.clone() + one.clone());
165        let is_table_padding_is_0_or_remains_unchanged =
166            is_table_padding.clone() * (is_table_padding_next.clone() - is_table_padding);
167
168        let index_in_chunk_cycles_correctly = (one.clone()
169            - max_minus_index_in_chunk_inv.clone()
170                * (rate_minus_one.clone() - index_in_chunk.clone()))
171            * index_in_chunk_next.clone()
172            + max_minus_index_in_chunk_inv.clone()
173                * (index_in_chunk_next.clone() - index_in_chunk.clone() - one.clone());
174
175        let hash_input_indicator_is_0_or_remains_unchanged =
176            is_hash_input_padding.clone() * (is_hash_input_padding_next.clone() - one.clone());
177
178        let first_hash_input_padding_is_1 = (is_hash_input_padding.clone() - one.clone())
179            * is_hash_input_padding_next
180            * (instruction_next.clone() - one.clone());
181
182        let hash_input_padding_is_0_after_the_first_1 =
183            is_hash_input_padding.clone() * instruction_next.clone();
184
185        let next_row_is_table_padding_row = is_table_padding_next.clone() - one.clone();
186        let table_padding_starts_when_hash_input_padding_is_active_and_index_in_chunk_is_zero =
187            is_hash_input_padding.clone()
188                * (one.clone()
189                    - max_minus_index_in_chunk_inv.clone()
190                        * (rate_minus_one.clone() - index_in_chunk.clone()))
191                * next_row_is_table_padding_row.clone();
192
193        let log_derivative_remains = log_derivative_next.clone() - log_derivative.clone();
194        let compressed_row = challenge(ChallengeId::ProgramAddressWeight) * address
195            + challenge(ChallengeId::ProgramInstructionWeight) * instruction
196            + challenge(ChallengeId::ProgramNextInstructionWeight) * instruction_next.clone();
197
198        let indeterminate = challenge(ChallengeId::InstructionLookupIndeterminate);
199        let log_derivative_updates = (log_derivative_next - log_derivative)
200            * (indeterminate - compressed_row)
201            - lookup_multiplicity;
202        let log_derivative_updates_if_and_only_if_not_a_padding_row =
203            (one.clone() - is_hash_input_padding.clone()) * log_derivative_updates
204                + is_hash_input_padding * log_derivative_remains;
205
206        let prepare_chunk_running_evaluation_absorbs_next_instruction =
207            prepare_chunk_running_evaluation_next.clone()
208                - prepare_chunk_indeterminate.clone() * prepare_chunk_running_evaluation
209                - instruction_next.clone();
210        let prepare_chunk_running_evaluation_resets_and_absorbs_next_instruction =
211            prepare_chunk_running_evaluation_next.clone()
212                - prepare_chunk_indeterminate
213                - instruction_next;
214        let index_in_chunk_is_max = rate_minus_one.clone() - index_in_chunk.clone();
215        let index_in_chunk_is_not_max =
216            one.clone() - max_minus_index_in_chunk_inv * (rate_minus_one.clone() - index_in_chunk);
217        let prepare_chunk_running_evaluation_resets_every_rate_rows_and_absorbs_next_instruction =
218            index_in_chunk_is_max * prepare_chunk_running_evaluation_absorbs_next_instruction
219                + index_in_chunk_is_not_max
220                    * prepare_chunk_running_evaluation_resets_and_absorbs_next_instruction;
221
222        let send_chunk_running_evaluation_absorbs_next_chunk = send_chunk_running_evaluation_next
223            .clone()
224            - send_chunk_indeterminate * send_chunk_running_evaluation.clone()
225            - prepare_chunk_running_evaluation_next;
226        let send_chunk_running_evaluation_does_not_change =
227            send_chunk_running_evaluation_next - send_chunk_running_evaluation;
228        let index_in_chunk_next_is_max = rate_minus_one - index_in_chunk_next;
229        let index_in_chunk_next_is_not_max =
230            one - max_minus_index_in_chunk_inv_next * index_in_chunk_next_is_max.clone();
231
232        let send_chunk_running_eval_absorbs_chunk_iff_index_in_chunk_next_is_max_and_not_padding =
233            send_chunk_running_evaluation_absorbs_next_chunk
234                * next_row_is_table_padding_row
235                * index_in_chunk_next_is_not_max
236                + send_chunk_running_evaluation_does_not_change.clone() * is_table_padding_next
237                + send_chunk_running_evaluation_does_not_change * index_in_chunk_next_is_max;
238
239        vec![
240            address_increases_by_one,
241            is_table_padding_is_0_or_remains_unchanged,
242            index_in_chunk_cycles_correctly,
243            hash_input_indicator_is_0_or_remains_unchanged,
244            first_hash_input_padding_is_1,
245            hash_input_padding_is_0_after_the_first_1,
246            table_padding_starts_when_hash_input_padding_is_active_and_index_in_chunk_is_zero,
247            log_derivative_updates_if_and_only_if_not_a_padding_row,
248            prepare_chunk_running_evaluation_resets_every_rate_rows_and_absorbs_next_instruction,
249            send_chunk_running_eval_absorbs_chunk_iff_index_in_chunk_next_is_max_and_not_padding,
250        ]
251    }
252
253    fn terminal_constraints(
254        circuit_builder: &ConstraintCircuitBuilder<SingleRowIndicator>,
255    ) -> Vec<ConstraintCircuitMonad<SingleRowIndicator>> {
256        let constant = |c: u64| circuit_builder.b_constant(c);
257        let main_row = |col: Self::MainColumn| circuit_builder.input(Main(col.master_main_index()));
258
259        let index_in_chunk = main_row(Self::MainColumn::IndexInChunk);
260        let is_hash_input_padding = main_row(Self::MainColumn::IsHashInputPadding);
261        let is_table_padding = main_row(Self::MainColumn::IsTablePadding);
262
263        let hash_input_padding_is_one = is_hash_input_padding - constant(1);
264
265        let max_index_in_chunk = Tip5::RATE as u64 - 1;
266        let index_in_chunk_is_max_or_row_is_padding_row =
267            (index_in_chunk - constant(max_index_in_chunk)) * (is_table_padding - constant(1));
268
269        vec![
270            hash_input_padding_is_one,
271            index_in_chunk_is_max_or_row_is_padding_row,
272        ]
273    }
274}
triton_air/table/program.rs

triton_air/table/
program.rs
