diff --git a/provers/cairo/src/air.rs b/provers/cairo/src/air.rs index 4ce45d130..f5e22c85b 100644 --- a/provers/cairo/src/air.rs +++ b/provers/cairo/src/air.rs @@ -124,34 +124,34 @@ pub const EXTRA_VAL: usize = 34; pub const RC_HOLES: usize = 35; // Auxiliary range check columns -pub const RANGE_CHECK_COL_1: usize = 36; -pub const RANGE_CHECK_COL_2: usize = 37; -pub const RANGE_CHECK_COL_3: usize = 38; -pub const RANGE_CHECK_COL_4: usize = 39; +pub const RANGE_CHECK_COL_1: usize = 0; +pub const RANGE_CHECK_COL_2: usize = 1; +pub const RANGE_CHECK_COL_3: usize = 2; +pub const RANGE_CHECK_COL_4: usize = 3; // Auxiliary memory columns -pub const MEMORY_ADDR_SORTED_0: usize = 40; -pub const MEMORY_ADDR_SORTED_1: usize = 41; -pub const MEMORY_ADDR_SORTED_2: usize = 42; -pub const MEMORY_ADDR_SORTED_3: usize = 43; -pub const MEMORY_ADDR_SORTED_4: usize = 44; - -pub const MEMORY_VALUES_SORTED_0: usize = 45; -pub const MEMORY_VALUES_SORTED_1: usize = 46; -pub const MEMORY_VALUES_SORTED_2: usize = 47; -pub const MEMORY_VALUES_SORTED_3: usize = 48; -pub const MEMORY_VALUES_SORTED_4: usize = 49; - -pub const PERMUTATION_ARGUMENT_COL_0: usize = 50; -pub const PERMUTATION_ARGUMENT_COL_1: usize = 51; -pub const PERMUTATION_ARGUMENT_COL_2: usize = 52; -pub const PERMUTATION_ARGUMENT_COL_3: usize = 53; -pub const PERMUTATION_ARGUMENT_COL_4: usize = 54; - -pub const PERMUTATION_ARGUMENT_RANGE_CHECK_COL_1: usize = 55; -pub const PERMUTATION_ARGUMENT_RANGE_CHECK_COL_2: usize = 56; -pub const PERMUTATION_ARGUMENT_RANGE_CHECK_COL_3: usize = 57; -pub const PERMUTATION_ARGUMENT_RANGE_CHECK_COL_4: usize = 58; +pub const MEMORY_ADDR_SORTED_0: usize = 4; +pub const MEMORY_ADDR_SORTED_1: usize = 5; +pub const MEMORY_ADDR_SORTED_2: usize = 6; +pub const MEMORY_ADDR_SORTED_3: usize = 7; +pub const MEMORY_ADDR_SORTED_4: usize = 8; + +pub const MEMORY_VALUES_SORTED_0: usize = 9; +pub const MEMORY_VALUES_SORTED_1: usize = 10; +pub const MEMORY_VALUES_SORTED_2: usize = 11; +pub const MEMORY_VALUES_SORTED_3: usize = 12; +pub const MEMORY_VALUES_SORTED_4: usize = 13; + +pub const PERMUTATION_ARGUMENT_COL_0: usize = 14; +pub const PERMUTATION_ARGUMENT_COL_1: usize = 15; +pub const PERMUTATION_ARGUMENT_COL_2: usize = 16; +pub const PERMUTATION_ARGUMENT_COL_3: usize = 17; +pub const PERMUTATION_ARGUMENT_COL_4: usize = 18; + +pub const PERMUTATION_ARGUMENT_RANGE_CHECK_COL_1: usize = 19; +pub const PERMUTATION_ARGUMENT_RANGE_CHECK_COL_2: usize = 20; +pub const PERMUTATION_ARGUMENT_RANGE_CHECK_COL_3: usize = 21; +pub const PERMUTATION_ARGUMENT_RANGE_CHECK_COL_4: usize = 22; // Trace layout pub const MEM_P_TRACE_OFFSET: usize = 17; @@ -787,9 +787,9 @@ impl AIR for CairoAIR { 23 } - fn compute_transition( + fn compute_transition_prover( &self, - frame: &Frame, + frame: &Frame, _periodic_values: &[FieldElement], rap_challenges: &Self::RAPChallenges, ) -> Vec> { @@ -819,15 +819,17 @@ impl AIR for CairoAIR { &self, rap_challenges: &Self::RAPChallenges, ) -> BoundaryConstraints { - let initial_pc = BoundaryConstraint::new(MEM_A_TRACE_OFFSET, 0, self.pub_inputs.pc_init); - let initial_ap = BoundaryConstraint::new(MEM_P_TRACE_OFFSET, 0, self.pub_inputs.ap_init); + let initial_pc = + BoundaryConstraint::new_main(MEM_A_TRACE_OFFSET, 0, self.pub_inputs.pc_init); + let initial_ap = + BoundaryConstraint::new_main(MEM_P_TRACE_OFFSET, 0, self.pub_inputs.ap_init); - let final_pc = BoundaryConstraint::new( + let final_pc = BoundaryConstraint::new_main( MEM_A_TRACE_OFFSET, self.pub_inputs.num_steps - 1, self.pub_inputs.pc_final, ); - let final_ap = BoundaryConstraint::new( + let final_ap = BoundaryConstraint::new_main( MEM_P_TRACE_OFFSET, self.pub_inputs.num_steps - 1, self.pub_inputs.ap_final, @@ -853,19 +855,19 @@ impl AIR for CairoAIR { * cumulative_product; let permutation_final_constraint = - BoundaryConstraint::new(PERMUTATION_ARGUMENT_COL_4, final_index, permutation_final); + BoundaryConstraint::new_aux(PERMUTATION_ARGUMENT_COL_4, final_index, permutation_final); let one: FieldElement = FieldElement::one(); let range_check_final_constraint = - BoundaryConstraint::new(PERMUTATION_ARGUMENT_RANGE_CHECK_COL_4, final_index, one); + BoundaryConstraint::new_aux(PERMUTATION_ARGUMENT_RANGE_CHECK_COL_4, final_index, one); - let range_check_min = BoundaryConstraint::new( + let range_check_min = BoundaryConstraint::new_aux( RANGE_CHECK_COL_1, 0, FieldElement::from(self.pub_inputs.range_check_min.unwrap() as u64), ); - let range_check_max = BoundaryConstraint::new( + let range_check_max = BoundaryConstraint::new_aux( RANGE_CHECK_COL_4, final_index, FieldElement::from(self.pub_inputs.range_check_max.unwrap() as u64), @@ -900,17 +902,29 @@ impl AIR for CairoAIR { fn pub_inputs(&self) -> &Self::PublicInputs { &self.pub_inputs } + + fn compute_transition_verifier( + &self, + frame: &Frame, + periodic_values: &[FieldElement], + rap_challenges: &Self::RAPChallenges, + ) -> Vec> { + self.compute_transition_prover(frame, periodic_values, rap_challenges) + } } /// From the Cairo whitepaper, section 9.10 -fn compute_instr_constraints(constraints: &mut [Felt252], frame: &Frame) { +fn compute_instr_constraints( + constraints: &mut [Felt252], + frame: &Frame, +) { // These constraints are only applied over elements of the same row. let curr = frame.get_evaluation_step(0); // Bit-prefixes constraints. // See section 9.4 of Cairo whitepaper https://eprint.iacr.org/2021/1063.pdf. let flags: Vec<&Felt252> = (0..16) - .map(|col_idx| curr.get_evaluation_element(0, col_idx)) + .map(|col_idx| curr.get_main_evaluation_element(0, col_idx)) .collect(); let one = Felt252::one(); @@ -965,10 +979,10 @@ fn compute_instr_constraints(constraints: &mut [Felt252], frame: &Frame) { +fn compute_operand_constraints( + constraints: &mut [Felt252], + frame: &Frame, +) { // These constraints are only applied over elements of the same row. let curr = frame.get_evaluation_step(0); - let ap = curr.get_evaluation_element(0, FRAME_AP); - let fp = curr.get_evaluation_element(0, FRAME_FP); - let pc = curr.get_evaluation_element(0, FRAME_PC); + let ap = curr.get_main_evaluation_element(0, FRAME_AP); + let fp = curr.get_main_evaluation_element(0, FRAME_FP); + let pc = curr.get_main_evaluation_element(0, FRAME_PC); let dst_fp = into_bit_flag(curr, F_DST_FP); - let off_dst = curr.get_evaluation_element(0, OFF_DST); - let dst_addr = curr.get_evaluation_element(0, FRAME_DST_ADDR); + let off_dst = curr.get_main_evaluation_element(0, OFF_DST); + let dst_addr = curr.get_main_evaluation_element(0, FRAME_DST_ADDR); let op0_fp = into_bit_flag(curr, F_OP_0_FP); - let off_op0 = curr.get_evaluation_element(0, OFF_OP0); - let op0_addr = curr.get_evaluation_element(0, FRAME_OP0_ADDR); + let off_op0 = curr.get_main_evaluation_element(0, OFF_OP0); + let op0_addr = curr.get_main_evaluation_element(0, FRAME_OP0_ADDR); let op1_val = into_bit_flag(curr, F_OP_1_VAL); let op1_ap = into_bit_flag(curr, F_OP_1_AP); let op1_fp = into_bit_flag(curr, F_OP_1_FP); - let op0 = curr.get_evaluation_element(0, FRAME_OP0); - let off_op1 = curr.get_evaluation_element(0, OFF_OP1); - let op1_addr = curr.get_evaluation_element(0, FRAME_OP1_ADDR); + let op0 = curr.get_main_evaluation_element(0, FRAME_OP0); + let off_op1 = curr.get_main_evaluation_element(0, OFF_OP1); + let op1_addr = curr.get_main_evaluation_element(0, FRAME_OP1_ADDR); let one = Felt252::one(); let b15 = Felt252::from(2).pow(15u32); @@ -1030,37 +1047,43 @@ fn compute_operand_constraints(constraints: &mut [Felt252], frame: &Frame, element_idx: usize) -> Felt252 { - step.get_evaluation_element(0, element_idx) - - Felt252::from(2) * step.get_evaluation_element(0, element_idx + 1) +fn into_bit_flag( + step: &StepView, + element_idx: usize, +) -> Felt252 { + step.get_main_evaluation_element(0, element_idx) + - Felt252::from(2) * step.get_main_evaluation_element(0, element_idx + 1) } -fn compute_register_constraints(constraints: &mut [Felt252], frame: &Frame) { +fn compute_register_constraints( + constraints: &mut [Felt252], + frame: &Frame, +) { let curr = frame.get_evaluation_step(0); let next = frame.get_evaluation_step(1); let one = Felt252::one(); let two = Felt252::from(2); - let ap = curr.get_evaluation_element(0, FRAME_AP); - let next_ap = next.get_evaluation_element(0, FRAME_AP); + let ap = curr.get_main_evaluation_element(0, FRAME_AP); + let next_ap = next.get_main_evaluation_element(0, FRAME_AP); let ap_add = into_bit_flag(curr, F_AP_ADD); - let res = curr.get_evaluation_element(0, FRAME_RES); + let res = curr.get_main_evaluation_element(0, FRAME_RES); let ap_one = into_bit_flag(curr, F_AP_ONE); let opc_ret = into_bit_flag(curr, F_OPC_RET); let opc_call = into_bit_flag(curr, F_OPC_CALL); - let dst = curr.get_evaluation_element(0, FRAME_DST); - let fp = curr.get_evaluation_element(0, FRAME_FP); - let next_fp = next.get_evaluation_element(0, FRAME_FP); + let dst = curr.get_main_evaluation_element(0, FRAME_DST); + let fp = curr.get_main_evaluation_element(0, FRAME_FP); + let next_fp = next.get_main_evaluation_element(0, FRAME_FP); - let t1 = curr.get_evaluation_element(0, FRAME_T1); + let t1 = curr.get_main_evaluation_element(0, FRAME_T1); let pc_jnz = into_bit_flag(curr, F_PC_JNZ); - let pc = curr.get_evaluation_element(0, FRAME_PC); - let next_pc = next.get_evaluation_element(0, FRAME_PC); + let pc = curr.get_main_evaluation_element(0, FRAME_PC); + let next_pc = next.get_main_evaluation_element(0, FRAME_PC); - let t0 = curr.get_evaluation_element(0, FRAME_T0); - let op1 = curr.get_evaluation_element(0, FRAME_OP1); + let t0 = curr.get_main_evaluation_element(0, FRAME_T0); + let op1 = curr.get_main_evaluation_element(0, FRAME_OP1); let pc_abs = into_bit_flag(curr, F_PC_ABS); let pc_rel = into_bit_flag(curr, F_PC_REL); @@ -1082,23 +1105,26 @@ fn compute_register_constraints(constraints: &mut [Felt252], frame: &Frame) { +fn compute_opcode_constraints( + constraints: &mut [Felt252], + frame: &Frame, +) { let curr = frame.get_evaluation_step(0); let one = Felt252::one(); - let mul = curr.get_evaluation_element(0, FRAME_MUL); - let op0 = curr.get_evaluation_element(0, FRAME_OP0); - let op1 = curr.get_evaluation_element(0, FRAME_OP1); + let mul = curr.get_main_evaluation_element(0, FRAME_MUL); + let op0 = curr.get_main_evaluation_element(0, FRAME_OP0); + let op1 = curr.get_main_evaluation_element(0, FRAME_OP1); let res_add = into_bit_flag(curr, F_RES_ADD); let res_mul = into_bit_flag(curr, F_RES_MUL); let pc_jnz = into_bit_flag(curr, F_PC_JNZ); - let res = curr.get_evaluation_element(0, FRAME_RES); + let res = curr.get_main_evaluation_element(0, FRAME_RES); let opc_call = into_bit_flag(curr, F_OPC_CALL); - let dst = curr.get_evaluation_element(0, FRAME_DST); - let fp = curr.get_evaluation_element(0, FRAME_FP); - let pc = curr.get_evaluation_element(0, FRAME_PC); + let dst = curr.get_main_evaluation_element(0, FRAME_DST); + let fp = curr.get_main_evaluation_element(0, FRAME_FP); + let pc = curr.get_main_evaluation_element(0, FRAME_PC); let opc_aeq = into_bit_flag(curr, F_OPC_AEQ); @@ -1115,24 +1141,27 @@ fn compute_opcode_constraints(constraints: &mut [Felt252], frame: &Frame) { +fn memory_is_increasing( + constraints: &mut [Felt252], + frame: &Frame, +) { let curr = frame.get_evaluation_step(0); let next = frame.get_evaluation_step(1); let one = FieldElement::one(); - let mem_addr_sorted_0 = curr.get_evaluation_element(0, MEMORY_ADDR_SORTED_0); - let mem_addr_sorted_1 = curr.get_evaluation_element(0, MEMORY_ADDR_SORTED_1); - let mem_addr_sorted_2 = curr.get_evaluation_element(0, MEMORY_ADDR_SORTED_2); - let mem_addr_sorted_3 = curr.get_evaluation_element(0, MEMORY_ADDR_SORTED_3); - let mem_addr_sorted_4 = curr.get_evaluation_element(0, MEMORY_ADDR_SORTED_4); - let next_mem_addr_sorted_0 = next.get_evaluation_element(0, MEMORY_ADDR_SORTED_0); + let mem_addr_sorted_0 = curr.get_aux_evaluation_element(0, MEMORY_ADDR_SORTED_0); + let mem_addr_sorted_1 = curr.get_aux_evaluation_element(0, MEMORY_ADDR_SORTED_1); + let mem_addr_sorted_2 = curr.get_aux_evaluation_element(0, MEMORY_ADDR_SORTED_2); + let mem_addr_sorted_3 = curr.get_aux_evaluation_element(0, MEMORY_ADDR_SORTED_3); + let mem_addr_sorted_4 = curr.get_aux_evaluation_element(0, MEMORY_ADDR_SORTED_4); + let next_mem_addr_sorted_0 = next.get_aux_evaluation_element(0, MEMORY_ADDR_SORTED_0); - let mem_val_sorted_0 = curr.get_evaluation_element(0, MEMORY_VALUES_SORTED_0); - let mem_val_sorted_1 = curr.get_evaluation_element(0, MEMORY_VALUES_SORTED_1); - let mem_val_sorted_2 = curr.get_evaluation_element(0, MEMORY_VALUES_SORTED_2); - let mem_val_sorted_3 = curr.get_evaluation_element(0, MEMORY_VALUES_SORTED_3); - let mem_val_sorted_4 = curr.get_evaluation_element(0, MEMORY_VALUES_SORTED_4); - let next_mem_val_sorted_0 = next.get_evaluation_element(0, MEMORY_VALUES_SORTED_0); + let mem_val_sorted_0 = curr.get_aux_evaluation_element(0, MEMORY_VALUES_SORTED_0); + let mem_val_sorted_1 = curr.get_aux_evaluation_element(0, MEMORY_VALUES_SORTED_1); + let mem_val_sorted_2 = curr.get_aux_evaluation_element(0, MEMORY_VALUES_SORTED_2); + let mem_val_sorted_3 = curr.get_aux_evaluation_element(0, MEMORY_VALUES_SORTED_3); + let mem_val_sorted_4 = curr.get_aux_evaluation_element(0, MEMORY_VALUES_SORTED_4); + let next_mem_val_sorted_0 = next.get_aux_evaluation_element(0, MEMORY_VALUES_SORTED_0); constraints[MEMORY_INCREASING_0] = (mem_addr_sorted_0 - mem_addr_sorted_1) * (mem_addr_sorted_1 - mem_addr_sorted_0 - one); @@ -1167,7 +1196,7 @@ fn memory_is_increasing(constraints: &mut [Felt252], frame: &Frame, + frame: &Frame, rap_challenges: &CairoRAPChallenges, ) { let curr = frame.get_evaluation_step(0); @@ -1176,36 +1205,36 @@ fn permutation_argument( let z = &rap_challenges.z_memory; let alpha = &rap_challenges.alpha_memory; - let p0 = curr.get_evaluation_element(0, PERMUTATION_ARGUMENT_COL_0); - let next_p0 = next.get_evaluation_element(0, PERMUTATION_ARGUMENT_COL_0); - let p1 = curr.get_evaluation_element(0, PERMUTATION_ARGUMENT_COL_1); - let p2 = curr.get_evaluation_element(0, PERMUTATION_ARGUMENT_COL_2); - let p3 = curr.get_evaluation_element(0, PERMUTATION_ARGUMENT_COL_3); - let p4 = curr.get_evaluation_element(0, PERMUTATION_ARGUMENT_COL_4); - - let next_ap0 = next.get_evaluation_element(0, MEMORY_ADDR_SORTED_0); - let ap1 = curr.get_evaluation_element(0, MEMORY_ADDR_SORTED_1); - let ap2 = curr.get_evaluation_element(0, MEMORY_ADDR_SORTED_2); - let ap3 = curr.get_evaluation_element(0, MEMORY_ADDR_SORTED_3); - let ap4 = curr.get_evaluation_element(0, MEMORY_ADDR_SORTED_4); - - let next_vp0 = next.get_evaluation_element(0, MEMORY_VALUES_SORTED_0); - let vp1 = curr.get_evaluation_element(0, MEMORY_VALUES_SORTED_1); - let vp2 = curr.get_evaluation_element(0, MEMORY_VALUES_SORTED_2); - let vp3 = curr.get_evaluation_element(0, MEMORY_VALUES_SORTED_3); - let vp4 = curr.get_evaluation_element(0, MEMORY_VALUES_SORTED_4); - - let next_a0 = next.get_evaluation_element(0, FRAME_PC); - let a1 = curr.get_evaluation_element(0, FRAME_DST_ADDR); - let a2 = curr.get_evaluation_element(0, FRAME_OP0_ADDR); - let a3 = curr.get_evaluation_element(0, FRAME_OP1_ADDR); - let a4 = curr.get_evaluation_element(0, EXTRA_ADDR); - - let next_v0 = next.get_evaluation_element(0, FRAME_INST); - let v1 = curr.get_evaluation_element(0, FRAME_DST); - let v2 = curr.get_evaluation_element(0, FRAME_OP0); - let v3 = curr.get_evaluation_element(0, FRAME_OP1); - let v4 = curr.get_evaluation_element(0, EXTRA_VAL); + let p0 = curr.get_aux_evaluation_element(0, PERMUTATION_ARGUMENT_COL_0); + let next_p0 = next.get_aux_evaluation_element(0, PERMUTATION_ARGUMENT_COL_0); + let p1 = curr.get_aux_evaluation_element(0, PERMUTATION_ARGUMENT_COL_1); + let p2 = curr.get_aux_evaluation_element(0, PERMUTATION_ARGUMENT_COL_2); + let p3 = curr.get_aux_evaluation_element(0, PERMUTATION_ARGUMENT_COL_3); + let p4 = curr.get_aux_evaluation_element(0, PERMUTATION_ARGUMENT_COL_4); + + let next_ap0 = next.get_aux_evaluation_element(0, MEMORY_ADDR_SORTED_0); + let ap1 = curr.get_aux_evaluation_element(0, MEMORY_ADDR_SORTED_1); + let ap2 = curr.get_aux_evaluation_element(0, MEMORY_ADDR_SORTED_2); + let ap3 = curr.get_aux_evaluation_element(0, MEMORY_ADDR_SORTED_3); + let ap4 = curr.get_aux_evaluation_element(0, MEMORY_ADDR_SORTED_4); + + let next_vp0 = next.get_aux_evaluation_element(0, MEMORY_VALUES_SORTED_0); + let vp1 = curr.get_aux_evaluation_element(0, MEMORY_VALUES_SORTED_1); + let vp2 = curr.get_aux_evaluation_element(0, MEMORY_VALUES_SORTED_2); + let vp3 = curr.get_aux_evaluation_element(0, MEMORY_VALUES_SORTED_3); + let vp4 = curr.get_aux_evaluation_element(0, MEMORY_VALUES_SORTED_4); + + let next_a0 = next.get_main_evaluation_element(0, FRAME_PC); + let a1 = curr.get_main_evaluation_element(0, FRAME_DST_ADDR); + let a2 = curr.get_main_evaluation_element(0, FRAME_OP0_ADDR); + let a3 = curr.get_main_evaluation_element(0, FRAME_OP1_ADDR); + let a4 = curr.get_main_evaluation_element(0, EXTRA_ADDR); + + let next_v0 = next.get_main_evaluation_element(0, FRAME_INST); + let v1 = curr.get_main_evaluation_element(0, FRAME_DST); + let v2 = curr.get_main_evaluation_element(0, FRAME_OP0); + let v3 = curr.get_main_evaluation_element(0, FRAME_OP1); + let v4 = curr.get_main_evaluation_element(0, EXTRA_VAL); constraints[PERMUTATION_ARGUMENT_0] = (z - (ap1 + alpha * vp1)) * p1 - (z - (a1 + alpha * v1)) * p0; @@ -1221,7 +1250,7 @@ fn permutation_argument( fn permutation_argument_range_check( constraints: &mut [Felt252], - frame: &Frame, + frame: &Frame, rap_challenges: &CairoRAPChallenges, ) { let curr = frame.get_evaluation_step(0); @@ -1229,11 +1258,11 @@ fn permutation_argument_range_check( let one = FieldElement::one(); let z = &rap_challenges.z_range_check; - let rc_col_1 = curr.get_evaluation_element(0, RANGE_CHECK_COL_1); - let rc_col_2 = curr.get_evaluation_element(0, RANGE_CHECK_COL_2); - let rc_col_3 = curr.get_evaluation_element(0, RANGE_CHECK_COL_3); - let rc_col_4 = curr.get_evaluation_element(0, RANGE_CHECK_COL_4); - let next_rc_col_1 = next.get_evaluation_element(0, RANGE_CHECK_COL_1); + let rc_col_1 = curr.get_aux_evaluation_element(0, RANGE_CHECK_COL_1); + let rc_col_2 = curr.get_aux_evaluation_element(0, RANGE_CHECK_COL_2); + let rc_col_3 = curr.get_aux_evaluation_element(0, RANGE_CHECK_COL_3); + let rc_col_4 = curr.get_aux_evaluation_element(0, RANGE_CHECK_COL_4); + let next_rc_col_1 = next.get_aux_evaluation_element(0, RANGE_CHECK_COL_1); constraints[RANGE_CHECK_INCREASING_0] = (rc_col_1 - rc_col_2) * (rc_col_2 - rc_col_1 - one); constraints[RANGE_CHECK_INCREASING_1] = (rc_col_2 - rc_col_3) * (rc_col_3 - rc_col_2 - one); @@ -1241,21 +1270,21 @@ fn permutation_argument_range_check( constraints[RANGE_CHECK_INCREASING_3] = (rc_col_4 - next_rc_col_1) * (next_rc_col_1 - rc_col_4 - one); - let p0 = curr.get_evaluation_element(0, PERMUTATION_ARGUMENT_RANGE_CHECK_COL_1); - let next_p0 = next.get_evaluation_element(0, PERMUTATION_ARGUMENT_RANGE_CHECK_COL_1); - let p1 = curr.get_evaluation_element(0, PERMUTATION_ARGUMENT_RANGE_CHECK_COL_2); - let p2 = curr.get_evaluation_element(0, PERMUTATION_ARGUMENT_RANGE_CHECK_COL_3); - let p3 = curr.get_evaluation_element(0, PERMUTATION_ARGUMENT_RANGE_CHECK_COL_4); + let p0 = curr.get_aux_evaluation_element(0, PERMUTATION_ARGUMENT_RANGE_CHECK_COL_1); + let next_p0 = next.get_aux_evaluation_element(0, PERMUTATION_ARGUMENT_RANGE_CHECK_COL_1); + let p1 = curr.get_aux_evaluation_element(0, PERMUTATION_ARGUMENT_RANGE_CHECK_COL_2); + let p2 = curr.get_aux_evaluation_element(0, PERMUTATION_ARGUMENT_RANGE_CHECK_COL_3); + let p3 = curr.get_aux_evaluation_element(0, PERMUTATION_ARGUMENT_RANGE_CHECK_COL_4); - let next_ap0 = next.get_evaluation_element(0, RANGE_CHECK_COL_1); - let ap1 = curr.get_evaluation_element(0, RANGE_CHECK_COL_2); - let ap2 = curr.get_evaluation_element(0, RANGE_CHECK_COL_3); - let ap3 = curr.get_evaluation_element(0, RANGE_CHECK_COL_4); + let next_ap0 = next.get_aux_evaluation_element(0, RANGE_CHECK_COL_1); + let ap1 = curr.get_aux_evaluation_element(0, RANGE_CHECK_COL_2); + let ap2 = curr.get_aux_evaluation_element(0, RANGE_CHECK_COL_3); + let ap3 = curr.get_aux_evaluation_element(0, RANGE_CHECK_COL_4); - let a0_next = next.get_evaluation_element(0, OFF_DST); - let a1 = curr.get_evaluation_element(0, OFF_OP0); - let a2 = curr.get_evaluation_element(0, OFF_OP1); - let a3 = curr.get_evaluation_element(0, RC_HOLES); + let a0_next = next.get_main_evaluation_element(0, OFF_DST); + let a1 = curr.get_main_evaluation_element(0, OFF_OP0); + let a2 = curr.get_main_evaluation_element(0, OFF_OP1); + let a3 = curr.get_main_evaluation_element(0, RC_HOLES); constraints[RANGE_CHECK_0] = (z - ap1) * p1 - (z - a1) * p0; constraints[RANGE_CHECK_1] = (z - ap2) * p2 - (z - a2) * p1; @@ -1263,7 +1292,7 @@ fn permutation_argument_range_check( constraints[RANGE_CHECK_3] = (z - next_ap0) * next_p0 - (z - a0_next) * p3; } -fn frame_inst_size(step: &StepView) -> Felt252 { +fn frame_inst_size(step: &StepView) -> Felt252 { let op1_val = into_bit_flag(step, F_OP_1_VAL); op1_val + Felt252::one() } diff --git a/provers/cairo/src/tests/integration_tests.rs b/provers/cairo/src/tests/integration_tests.rs index 4c7a41046..79f051830 100644 --- a/provers/cairo/src/tests/integration_tests.rs +++ b/provers/cairo/src/tests/integration_tests.rs @@ -161,6 +161,7 @@ fn check_simple_cairo_trace_evaluates_to_zero() { assert!(validate_trace( &cairo_air, &trace_polys, + &aux_polys, &domain, &rap_challenges )); diff --git a/provers/cairo/tests/wasm.rs b/provers/cairo/tests/wasm.rs index 0eba68898..0fd44a5e9 100644 --- a/provers/cairo/tests/wasm.rs +++ b/provers/cairo/tests/wasm.rs @@ -19,103 +19,66 @@ fn test_prove_cairo1_program_wasm() { // Test case is fibo5, with default test options #[cfg(feature = "wasm")] -static PROOF: [u8; 25527] = [ - 189, 90, 0, 0, 64, 34, 150, 252, 123, 41, 36, 58, 219, 76, 25, 24, 145, 52, 128, 169, 121, 212, +static PROOF: [u8; 25531] = [ + 193, 90, 0, 0, 64, 34, 150, 252, 123, 41, 36, 58, 219, 76, 25, 24, 145, 52, 128, 169, 121, 212, 127, 31, 128, 230, 237, 60, 212, 165, 171, 81, 190, 191, 157, 241, 200, 1, 77, 31, 232, 212, 215, 170, 34, 124, 137, 195, 171, 208, 228, 24, 74, 34, 237, 107, 135, 106, 205, 168, 33, 72, - 193, 202, 8, 15, 250, 12, 38, 185, 118, 32, 4, 171, 46, 46, 72, 149, 150, 106, 253, 54, 138, - 21, 229, 36, 56, 120, 99, 238, 141, 157, 240, 156, 48, 237, 33, 19, 160, 95, 129, 156, 230, - 103, 32, 5, 92, 56, 221, 221, 174, 163, 72, 227, 62, 104, 105, 67, 88, 2, 1, 167, 128, 234, - 197, 5, 19, 84, 237, 187, 255, 26, 202, 199, 198, 212, 123, 32, 6, 179, 252, 250, 97, 234, 175, - 28, 235, 179, 10, 3, 105, 223, 144, 217, 123, 180, 69, 201, 228, 37, 168, 76, 160, 177, 251, - 61, 4, 188, 206, 150, 32, 4, 35, 76, 126, 184, 197, 8, 44, 216, 227, 61, 246, 83, 23, 174, 189, - 38, 10, 238, 119, 48, 144, 139, 151, 205, 240, 162, 170, 38, 69, 32, 218, 32, 0, 78, 185, 188, - 8, 218, 190, 3, 120, 130, 120, 175, 57, 130, 249, 75, 60, 8, 193, 5, 209, 215, 185, 84, 20, - 152, 161, 136, 29, 105, 202, 146, 32, 1, 32, 251, 95, 208, 37, 117, 134, 77, 38, 169, 174, 238, - 162, 116, 104, 140, 208, 75, 38, 112, 222, 177, 176, 95, 20, 91, 133, 96, 134, 241, 165, 32, 5, - 58, 73, 111, 62, 133, 211, 177, 161, 47, 249, 216, 236, 145, 223, 222, 0, 208, 194, 218, 24, - 115, 204, 219, 46, 122, 185, 109, 97, 142, 6, 157, 32, 6, 157, 36, 183, 159, 66, 233, 225, 80, - 151, 252, 236, 118, 72, 239, 239, 0, 104, 97, 109, 12, 57, 230, 109, 151, 61, 92, 182, 176, - 199, 3, 79, 32, 1, 112, 61, 72, 192, 28, 241, 170, 208, 254, 139, 231, 7, 209, 54, 27, 192, - 145, 224, 147, 87, 46, 129, 150, 250, 105, 17, 146, 120, 238, 160, 242, 32, 6, 171, 57, 209, - 156, 186, 18, 81, 248, 81, 70, 231, 108, 187, 34, 194, 209, 111, 66, 41, 165, 196, 44, 203, - 185, 199, 88, 119, 146, 115, 47, 134, 32, 3, 253, 112, 171, 215, 178, 72, 192, 87, 190, 133, - 240, 187, 7, 161, 188, 230, 12, 255, 184, 120, 26, 25, 36, 123, 72, 169, 168, 139, 153, 157, - 59, 32, 4, 66, 223, 179, 251, 173, 74, 78, 2, 84, 31, 166, 43, 236, 208, 150, 145, 194, 243, - 10, 118, 191, 206, 20, 156, 165, 1, 69, 115, 4, 199, 206, 32, 7, 139, 31, 61, 86, 188, 154, - 191, 165, 215, 226, 86, 162, 70, 214, 134, 187, 31, 125, 208, 216, 59, 183, 54, 16, 82, 52, - 237, 240, 126, 50, 223, 32, 7, 191, 175, 19, 56, 74, 241, 8, 88, 216, 27, 92, 136, 239, 219, - 106, 181, 155, 238, 129, 10, 129, 221, 197, 69, 118, 172, 159, 87, 101, 181, 40, 32, 6, 1, 130, - 118, 140, 160, 245, 70, 213, 30, 155, 31, 17, 36, 171, 217, 155, 43, 167, 29, 86, 82, 125, 66, - 209, 133, 185, 134, 204, 61, 249, 223, 32, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, - 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 32, 5, 5, 77, 210, 22, 240, 224, 140, 52, 197, - 169, 11, 160, 21, 13, 55, 239, 229, 66, 219, 125, 182, 6, 36, 172, 145, 58, 153, 209, 202, 52, - 114, 32, 0, 148, 26, 6, 89, 195, 227, 119, 6, 167, 12, 169, 231, 161, 188, 192, 231, 34, 181, - 72, 158, 226, 167, 181, 10, 160, 173, 188, 242, 236, 219, 152, 32, 0, 228, 51, 150, 138, 23, - 240, 58, 239, 11, 11, 49, 205, 232, 207, 77, 226, 183, 230, 217, 57, 64, 109, 196, 12, 39, 85, - 255, 237, 18, 85, 193, 32, 6, 85, 4, 87, 121, 137, 197, 38, 112, 136, 27, 230, 225, 169, 48, - 102, 5, 84, 136, 250, 71, 223, 219, 186, 104, 60, 135, 3, 128, 62, 106, 45, 32, 7, 56, 179, - 166, 236, 231, 225, 176, 54, 191, 5, 110, 209, 16, 229, 236, 73, 110, 41, 50, 90, 219, 209, - 125, 93, 79, 197, 186, 92, 170, 49, 219, 32, 3, 10, 93, 160, 62, 131, 106, 88, 66, 230, 41, - 206, 250, 29, 161, 133, 102, 106, 249, 221, 8, 97, 108, 255, 63, 67, 47, 168, 171, 220, 106, - 41, 32, 0, 139, 66, 37, 71, 31, 54, 72, 41, 206, 95, 73, 251, 212, 195, 255, 11, 100, 97, 24, - 153, 43, 0, 48, 38, 167, 83, 93, 94, 34, 210, 250, 32, 5, 109, 143, 37, 8, 2, 69, 20, 0, 152, - 119, 96, 22, 198, 72, 166, 96, 100, 110, 176, 22, 243, 142, 119, 221, 147, 218, 103, 40, 35, - 46, 125, 32, 4, 188, 184, 9, 251, 140, 5, 113, 122, 209, 130, 111, 194, 127, 208, 115, 60, 123, - 105, 88, 5, 7, 234, 212, 115, 83, 139, 114, 75, 218, 7, 70, 32, 1, 227, 195, 188, 203, 231, - 139, 5, 12, 254, 39, 124, 95, 116, 106, 12, 10, 179, 28, 165, 161, 182, 30, 11, 214, 138, 148, - 228, 179, 58, 162, 36, 32, 5, 62, 149, 75, 155, 0, 72, 204, 169, 3, 6, 65, 123, 194, 43, 245, - 19, 54, 172, 21, 95, 53, 55, 148, 127, 95, 27, 64, 184, 193, 216, 120, 32, 4, 27, 7, 54, 57, - 150, 199, 162, 106, 136, 171, 108, 35, 200, 0, 240, 225, 124, 114, 127, 192, 131, 131, 14, 216, - 142, 47, 58, 30, 65, 127, 55, 32, 1, 148, 91, 227, 154, 152, 80, 25, 52, 55, 158, 182, 187, 14, - 180, 170, 20, 138, 197, 24, 175, 230, 9, 219, 122, 144, 144, 61, 108, 215, 189, 250, 32, 7, - 114, 120, 91, 223, 13, 219, 241, 233, 217, 192, 111, 190, 224, 172, 246, 176, 182, 66, 142, - 136, 226, 43, 54, 172, 53, 15, 59, 142, 97, 211, 188, 32, 2, 132, 57, 150, 70, 49, 1, 8, 234, - 246, 45, 249, 78, 230, 149, 128, 150, 96, 213, 213, 11, 99, 63, 254, 93, 43, 187, 22, 231, 60, - 154, 36, 32, 3, 63, 223, 107, 43, 58, 72, 137, 1, 117, 86, 227, 189, 56, 81, 54, 68, 42, 58, - 135, 219, 191, 103, 9, 82, 207, 206, 34, 151, 38, 200, 153, 32, 1, 238, 242, 213, 113, 252, 6, - 128, 90, 154, 103, 235, 16, 227, 37, 91, 202, 212, 170, 172, 81, 1, 10, 69, 89, 136, 49, 193, - 130, 176, 239, 60, 32, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, - 0, 0, 0, 0, 0, 0, 0, 0, 32, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, - 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 32, 7, 255, 255, 255, 254, 239, 253, 240, 255, 255, 255, 255, - 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 239, 255, - 225, 32, 2, 91, 68, 30, 167, 149, 38, 118, 145, 95, 148, 62, 85, 145, 230, 53, 55, 130, 176, - 244, 48, 67, 173, 42, 214, 141, 102, 245, 187, 90, 230, 19, 32, 5, 34, 69, 70, 141, 13, 255, - 133, 225, 104, 55, 188, 22, 185, 42, 245, 181, 99, 180, 84, 29, 89, 106, 130, 235, 89, 220, 87, - 144, 176, 77, 60, 32, 5, 34, 69, 70, 141, 13, 255, 133, 225, 104, 55, 188, 22, 185, 42, 245, - 181, 99, 180, 84, 29, 89, 106, 130, 235, 89, 220, 87, 144, 176, 77, 60, 32, 5, 34, 69, 70, 141, - 13, 255, 133, 225, 104, 55, 188, 22, 185, 42, 245, 181, 99, 180, 84, 29, 89, 106, 130, 235, 89, - 220, 87, 144, 176, 77, 60, 32, 4, 172, 50, 234, 18, 80, 78, 10, 45, 122, 188, 84, 165, 217, - 106, 152, 186, 208, 180, 33, 157, 178, 199, 196, 247, 86, 102, 162, 254, 117, 30, 72, 32, 0, - 181, 233, 160, 243, 50, 209, 135, 128, 205, 250, 37, 164, 203, 220, 42, 145, 194, 139, 44, 213, - 121, 80, 254, 184, 153, 32, 79, 69, 57, 83, 216, 32, 6, 19, 23, 214, 231, 29, 95, 179, 150, - 132, 169, 32, 196, 217, 91, 169, 163, 124, 152, 184, 237, 143, 180, 231, 117, 152, 167, 123, - 83, 209, 158, 147, 32, 6, 53, 28, 103, 222, 115, 121, 45, 17, 1, 207, 189, 245, 123, 206, 196, - 83, 65, 169, 108, 164, 89, 160, 91, 82, 95, 127, 247, 39, 181, 34, 110, 32, 3, 31, 236, 182, - 13, 15, 107, 36, 19, 38, 250, 71, 179, 208, 136, 106, 154, 173, 227, 31, 17, 152, 79, 12, 144, - 63, 104, 61, 227, 164, 31, 228, 32, 1, 159, 112, 153, 196, 243, 158, 187, 254, 28, 60, 241, 46, - 105, 131, 157, 200, 26, 27, 122, 61, 228, 124, 189, 29, 242, 143, 79, 146, 139, 250, 153, 32, - 6, 193, 59, 12, 1, 213, 95, 240, 123, 204, 211, 89, 91, 2, 87, 245, 137, 143, 166, 33, 52, 104, - 219, 164, 137, 65, 209, 54, 190, 218, 216, 212, 32, 3, 229, 249, 197, 153, 170, 217, 112, 20, - 238, 233, 2, 174, 64, 10, 149, 156, 93, 238, 183, 26, 131, 97, 252, 235, 129, 71, 6, 23, 175, - 79, 173, 32, 6, 253, 237, 190, 189, 104, 8, 118, 156, 19, 217, 149, 238, 165, 120, 5, 142, 216, - 5, 93, 213, 251, 77, 5, 153, 131, 157, 90, 222, 105, 122, 120, 32, 2, 129, 96, 22, 155, 203, - 11, 182, 232, 185, 144, 137, 252, 51, 123, 36, 247, 87, 64, 32, 96, 251, 255, 208, 25, 98, 57, - 66, 175, 117, 176, 193, 32, 3, 193, 122, 195, 109, 117, 12, 99, 231, 45, 239, 98, 138, 155, 65, - 11, 130, 87, 253, 152, 152, 204, 121, 224, 34, 239, 131, 187, 169, 165, 80, 147, 32, 4, 246, - 117, 1, 253, 181, 210, 144, 241, 105, 62, 229, 159, 173, 99, 208, 146, 160, 204, 225, 177, 13, - 249, 172, 46, 189, 182, 61, 154, 161, 37, 214, 32, 7, 204, 121, 1, 160, 97, 61, 117, 31, 237, - 167, 240, 191, 56, 46, 150, 73, 122, 206, 192, 102, 9, 94, 103, 110, 233, 248, 26, 236, 255, - 132, 154, 32, 4, 137, 131, 56, 170, 8, 125, 216, 70, 207, 87, 130, 132, 70, 1, 125, 242, 43, - 121, 151, 176, 95, 112, 189, 214, 242, 170, 214, 129, 55, 154, 128, 32, 4, 201, 114, 110, 175, - 33, 250, 89, 22, 203, 194, 137, 227, 107, 31, 82, 20, 62, 160, 204, 121, 71, 65, 18, 220, 240, - 245, 105, 137, 65, 104, 186, 32, 5, 73, 163, 150, 210, 209, 44, 45, 88, 147, 177, 140, 73, 245, - 231, 52, 114, 8, 113, 216, 127, 88, 253, 134, 215, 221, 35, 183, 71, 99, 55, 163, 32, 4, 183, - 149, 133, 222, 16, 181, 158, 187, 26, 112, 160, 13, 165, 89, 191, 175, 117, 135, 204, 186, 117, - 164, 118, 218, 181, 24, 248, 8, 182, 165, 181, 32, 5, 180, 94, 217, 181, 61, 240, 200, 208, 79, - 68, 123, 238, 236, 167, 131, 241, 128, 31, 247, 36, 252, 212, 75, 196, 240, 89, 232, 91, 20, - 91, 209, 32, 4, 44, 50, 77, 67, 251, 45, 217, 70, 42, 101, 206, 195, 184, 161, 10, 85, 151, 59, - 51, 28, 208, 81, 78, 247, 241, 88, 37, 195, 149, 151, 228, 32, 5, 164, 73, 93, 67, 178, 117, + 193, 202, 8, 15, 250, 12, 38, 185, 72, 32, 4, 171, 46, 46, 72, 149, 150, 106, 253, 54, 138, 21, + 229, 36, 56, 120, 99, 238, 141, 157, 240, 156, 48, 237, 33, 19, 160, 95, 129, 156, 230, 103, + 32, 5, 92, 56, 221, 221, 174, 163, 72, 227, 62, 104, 105, 67, 88, 2, 1, 167, 128, 234, 197, 5, + 19, 84, 237, 187, 255, 26, 202, 199, 198, 212, 123, 32, 6, 179, 252, 250, 97, 234, 175, 28, + 235, 179, 10, 3, 105, 223, 144, 217, 123, 180, 69, 201, 228, 37, 168, 76, 160, 177, 251, 61, 4, + 188, 206, 150, 32, 4, 35, 76, 126, 184, 197, 8, 44, 216, 227, 61, 246, 83, 23, 174, 189, 38, + 10, 238, 119, 48, 144, 139, 151, 205, 240, 162, 170, 38, 69, 32, 218, 32, 0, 78, 185, 188, 8, + 218, 190, 3, 120, 130, 120, 175, 57, 130, 249, 75, 60, 8, 193, 5, 209, 215, 185, 84, 20, 152, + 161, 136, 29, 105, 202, 146, 32, 1, 32, 251, 95, 208, 37, 117, 134, 77, 38, 169, 174, 238, 162, + 116, 104, 140, 208, 75, 38, 112, 222, 177, 176, 95, 20, 91, 133, 96, 134, 241, 165, 32, 5, 58, + 73, 111, 62, 133, 211, 177, 161, 47, 249, 216, 236, 145, 223, 222, 0, 208, 194, 218, 24, 115, + 204, 219, 46, 122, 185, 109, 97, 142, 6, 157, 32, 6, 157, 36, 183, 159, 66, 233, 225, 80, 151, + 252, 236, 118, 72, 239, 239, 0, 104, 97, 109, 12, 57, 230, 109, 151, 61, 92, 182, 176, 199, 3, + 79, 32, 1, 112, 61, 72, 192, 28, 241, 170, 208, 254, 139, 231, 7, 209, 54, 27, 192, 145, 224, + 147, 87, 46, 129, 150, 250, 105, 17, 146, 120, 238, 160, 242, 32, 6, 171, 57, 209, 156, 186, + 18, 81, 248, 81, 70, 231, 108, 187, 34, 194, 209, 111, 66, 41, 165, 196, 44, 203, 185, 199, 88, + 119, 146, 115, 47, 134, 32, 3, 253, 112, 171, 215, 178, 72, 192, 87, 190, 133, 240, 187, 7, + 161, 188, 230, 12, 255, 184, 120, 26, 25, 36, 123, 72, 169, 168, 139, 153, 157, 59, 32, 4, 66, + 223, 179, 251, 173, 74, 78, 2, 84, 31, 166, 43, 236, 208, 150, 145, 194, 243, 10, 118, 191, + 206, 20, 156, 165, 1, 69, 115, 4, 199, 206, 32, 7, 139, 31, 61, 86, 188, 154, 191, 165, 215, + 226, 86, 162, 70, 214, 134, 187, 31, 125, 208, 216, 59, 183, 54, 16, 82, 52, 237, 240, 126, 50, + 223, 32, 7, 191, 175, 19, 56, 74, 241, 8, 88, 216, 27, 92, 136, 239, 219, 106, 181, 155, 238, + 129, 10, 129, 221, 197, 69, 118, 172, 159, 87, 101, 181, 40, 32, 6, 1, 130, 118, 140, 160, 245, + 70, 213, 30, 155, 31, 17, 36, 171, 217, 155, 43, 167, 29, 86, 82, 125, 66, 209, 133, 185, 134, + 204, 61, 249, 223, 32, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, + 0, 0, 0, 0, 0, 0, 0, 0, 32, 5, 5, 77, 210, 22, 240, 224, 140, 52, 197, 169, 11, 160, 21, 13, + 55, 239, 229, 66, 219, 125, 182, 6, 36, 172, 145, 58, 153, 209, 202, 52, 114, 32, 0, 148, 26, + 6, 89, 195, 227, 119, 6, 167, 12, 169, 231, 161, 188, 192, 231, 34, 181, 72, 158, 226, 167, + 181, 10, 160, 173, 188, 242, 236, 219, 152, 32, 0, 228, 51, 150, 138, 23, 240, 58, 239, 11, 11, + 49, 205, 232, 207, 77, 226, 183, 230, 217, 57, 64, 109, 196, 12, 39, 85, 255, 237, 18, 85, 193, + 32, 6, 85, 4, 87, 121, 137, 197, 38, 112, 136, 27, 230, 225, 169, 48, 102, 5, 84, 136, 250, 71, + 223, 219, 186, 104, 60, 135, 3, 128, 62, 106, 45, 32, 7, 56, 179, 166, 236, 231, 225, 176, 54, + 191, 5, 110, 209, 16, 229, 236, 73, 110, 41, 50, 90, 219, 209, 125, 93, 79, 197, 186, 92, 170, + 49, 219, 32, 3, 10, 93, 160, 62, 131, 106, 88, 66, 230, 41, 206, 250, 29, 161, 133, 102, 106, + 249, 221, 8, 97, 108, 255, 63, 67, 47, 168, 171, 220, 106, 41, 32, 0, 139, 66, 37, 71, 31, 54, + 72, 41, 206, 95, 73, 251, 212, 195, 255, 11, 100, 97, 24, 153, 43, 0, 48, 38, 167, 83, 93, 94, + 34, 210, 250, 32, 5, 109, 143, 37, 8, 2, 69, 20, 0, 152, 119, 96, 22, 198, 72, 166, 96, 100, + 110, 176, 22, 243, 142, 119, 221, 147, 218, 103, 40, 35, 46, 125, 32, 4, 188, 184, 9, 251, 140, + 5, 113, 122, 209, 130, 111, 194, 127, 208, 115, 60, 123, 105, 88, 5, 7, 234, 212, 115, 83, 139, + 114, 75, 218, 7, 70, 32, 1, 227, 195, 188, 203, 231, 139, 5, 12, 254, 39, 124, 95, 116, 106, + 12, 10, 179, 28, 165, 161, 182, 30, 11, 214, 138, 148, 228, 179, 58, 162, 36, 32, 5, 62, 149, + 75, 155, 0, 72, 204, 169, 3, 6, 65, 123, 194, 43, 245, 19, 54, 172, 21, 95, 53, 55, 148, 127, + 95, 27, 64, 184, 193, 216, 120, 32, 4, 27, 7, 54, 57, 150, 199, 162, 106, 136, 171, 108, 35, + 200, 0, 240, 225, 124, 114, 127, 192, 131, 131, 14, 216, 142, 47, 58, 30, 65, 127, 55, 32, 1, + 148, 91, 227, 154, 152, 80, 25, 52, 55, 158, 182, 187, 14, 180, 170, 20, 138, 197, 24, 175, + 230, 9, 219, 122, 144, 144, 61, 108, 215, 189, 250, 32, 7, 114, 120, 91, 223, 13, 219, 241, + 233, 217, 192, 111, 190, 224, 172, 246, 176, 182, 66, 142, 136, 226, 43, 54, 172, 53, 15, 59, + 142, 97, 211, 188, 32, 2, 132, 57, 150, 70, 49, 1, 8, 234, 246, 45, 249, 78, 230, 149, 128, + 150, 96, 213, 213, 11, 99, 63, 254, 93, 43, 187, 22, 231, 60, 154, 36, 32, 3, 63, 223, 107, 43, + 58, 72, 137, 1, 117, 86, 227, 189, 56, 81, 54, 68, 42, 58, 135, 219, 191, 103, 9, 82, 207, 206, + 34, 151, 38, 200, 153, 32, 1, 238, 242, 213, 113, 252, 6, 128, 90, 154, 103, 235, 16, 227, 37, + 91, 202, 212, 170, 172, 81, 1, 10, 69, 89, 136, 49, 193, 130, 176, 239, 60, 32, 0, 0, 0, 0, 0, + 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 32, 0, 0, 0, + 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 32, 7, + 255, 255, 255, 254, 239, 253, 240, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, + 255, 255, 255, 255, 255, 255, 255, 255, 255, 239, 255, 225, 32, 5, 164, 73, 93, 67, 178, 117, 132, 236, 197, 104, 163, 216, 184, 202, 92, 66, 199, 96, 214, 233, 218, 106, 44, 172, 235, 112, 136, 66, 249, 90, 126, 32, 3, 216, 209, 48, 53, 210, 164, 231, 47, 146, 117, 140, 11, 65, 169, 131, 250, 39, 109, 15, 216, 66, 25, 51, 242, 199, 136, 251, 208, 55, 7, 38, 32, 0, 28, 192, @@ -171,23 +134,60 @@ static PROOF: [u8; 25527] = [ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 32, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 32, 7, 255, 255, 255, 254, 239, 253, 240, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, - 255, 255, 255, 255, 255, 255, 255, 239, 255, 225, 32, 2, 97, 27, 155, 37, 146, 202, 43, 214, - 62, 62, 237, 12, 122, 139, 243, 242, 150, 242, 183, 49, 130, 122, 247, 48, 56, 106, 114, 143, - 235, 8, 79, 32, 2, 185, 124, 96, 183, 155, 14, 136, 208, 75, 114, 37, 245, 191, 178, 178, 63, - 111, 67, 60, 28, 27, 238, 221, 224, 240, 253, 47, 91, 239, 13, 179, 32, 2, 185, 124, 96, 183, - 155, 14, 136, 208, 75, 114, 37, 245, 191, 178, 178, 63, 111, 67, 60, 28, 27, 238, 221, 224, - 240, 253, 47, 91, 239, 13, 179, 32, 2, 185, 124, 96, 183, 155, 14, 136, 208, 75, 114, 37, 245, - 191, 178, 178, 63, 111, 67, 60, 28, 27, 238, 221, 224, 240, 253, 47, 91, 239, 13, 179, 32, 3, - 81, 15, 195, 103, 39, 66, 162, 136, 92, 92, 14, 153, 166, 21, 71, 131, 158, 181, 10, 33, 207, - 138, 191, 11, 61, 159, 8, 59, 196, 116, 206, 32, 6, 92, 174, 186, 3, 163, 232, 46, 142, 159, - 231, 236, 199, 52, 201, 253, 94, 196, 194, 27, 170, 65, 56, 3, 235, 54, 159, 71, 74, 224, 145, - 194, 32, 7, 37, 192, 191, 55, 232, 222, 163, 133, 119, 204, 154, 2, 252, 68, 204, 127, 35, 115, - 18, 255, 101, 92, 159, 113, 38, 148, 11, 88, 14, 188, 24, 32, 1, 185, 157, 208, 201, 232, 187, - 167, 69, 41, 191, 112, 20, 178, 90, 158, 106, 103, 187, 169, 152, 209, 138, 82, 222, 48, 151, - 43, 211, 122, 139, 62, 32, 0, 82, 151, 15, 254, 101, 72, 162, 180, 25, 122, 196, 91, 240, 198, - 230, 133, 210, 171, 61, 168, 31, 207, 166, 62, 126, 137, 58, 58, 215, 89, 196, 32, 7, 243, 45, - 235, 180, 10, 147, 108, 102, 148, 41, 190, 1, 4, 246, 173, 38, 149, 22, 241, 244, 63, 151, 200, - 36, 150, 99, 141, 148, 213, 170, 198, 32, 3, 127, 184, 40, 17, 194, 24, 186, 31, 167, 103, 162, + 255, 255, 255, 255, 255, 255, 255, 239, 255, 225, 36, 2, 46, 32, 2, 91, 68, 30, 167, 149, 38, + 118, 145, 95, 148, 62, 85, 145, 230, 53, 55, 130, 176, 244, 48, 67, 173, 42, 214, 141, 102, + 245, 187, 90, 230, 19, 32, 5, 34, 69, 70, 141, 13, 255, 133, 225, 104, 55, 188, 22, 185, 42, + 245, 181, 99, 180, 84, 29, 89, 106, 130, 235, 89, 220, 87, 144, 176, 77, 60, 32, 5, 34, 69, 70, + 141, 13, 255, 133, 225, 104, 55, 188, 22, 185, 42, 245, 181, 99, 180, 84, 29, 89, 106, 130, + 235, 89, 220, 87, 144, 176, 77, 60, 32, 5, 34, 69, 70, 141, 13, 255, 133, 225, 104, 55, 188, + 22, 185, 42, 245, 181, 99, 180, 84, 29, 89, 106, 130, 235, 89, 220, 87, 144, 176, 77, 60, 32, + 4, 172, 50, 234, 18, 80, 78, 10, 45, 122, 188, 84, 165, 217, 106, 152, 186, 208, 180, 33, 157, + 178, 199, 196, 247, 86, 102, 162, 254, 117, 30, 72, 32, 0, 181, 233, 160, 243, 50, 209, 135, + 128, 205, 250, 37, 164, 203, 220, 42, 145, 194, 139, 44, 213, 121, 80, 254, 184, 153, 32, 79, + 69, 57, 83, 216, 32, 6, 19, 23, 214, 231, 29, 95, 179, 150, 132, 169, 32, 196, 217, 91, 169, + 163, 124, 152, 184, 237, 143, 180, 231, 117, 152, 167, 123, 83, 209, 158, 147, 32, 6, 53, 28, + 103, 222, 115, 121, 45, 17, 1, 207, 189, 245, 123, 206, 196, 83, 65, 169, 108, 164, 89, 160, + 91, 82, 95, 127, 247, 39, 181, 34, 110, 32, 3, 31, 236, 182, 13, 15, 107, 36, 19, 38, 250, 71, + 179, 208, 136, 106, 154, 173, 227, 31, 17, 152, 79, 12, 144, 63, 104, 61, 227, 164, 31, 228, + 32, 1, 159, 112, 153, 196, 243, 158, 187, 254, 28, 60, 241, 46, 105, 131, 157, 200, 26, 27, + 122, 61, 228, 124, 189, 29, 242, 143, 79, 146, 139, 250, 153, 32, 6, 193, 59, 12, 1, 213, 95, + 240, 123, 204, 211, 89, 91, 2, 87, 245, 137, 143, 166, 33, 52, 104, 219, 164, 137, 65, 209, 54, + 190, 218, 216, 212, 32, 3, 229, 249, 197, 153, 170, 217, 112, 20, 238, 233, 2, 174, 64, 10, + 149, 156, 93, 238, 183, 26, 131, 97, 252, 235, 129, 71, 6, 23, 175, 79, 173, 32, 6, 253, 237, + 190, 189, 104, 8, 118, 156, 19, 217, 149, 238, 165, 120, 5, 142, 216, 5, 93, 213, 251, 77, 5, + 153, 131, 157, 90, 222, 105, 122, 120, 32, 2, 129, 96, 22, 155, 203, 11, 182, 232, 185, 144, + 137, 252, 51, 123, 36, 247, 87, 64, 32, 96, 251, 255, 208, 25, 98, 57, 66, 175, 117, 176, 193, + 32, 3, 193, 122, 195, 109, 117, 12, 99, 231, 45, 239, 98, 138, 155, 65, 11, 130, 87, 253, 152, + 152, 204, 121, 224, 34, 239, 131, 187, 169, 165, 80, 147, 32, 4, 246, 117, 1, 253, 181, 210, + 144, 241, 105, 62, 229, 159, 173, 99, 208, 146, 160, 204, 225, 177, 13, 249, 172, 46, 189, 182, + 61, 154, 161, 37, 214, 32, 7, 204, 121, 1, 160, 97, 61, 117, 31, 237, 167, 240, 191, 56, 46, + 150, 73, 122, 206, 192, 102, 9, 94, 103, 110, 233, 248, 26, 236, 255, 132, 154, 32, 4, 137, + 131, 56, 170, 8, 125, 216, 70, 207, 87, 130, 132, 70, 1, 125, 242, 43, 121, 151, 176, 95, 112, + 189, 214, 242, 170, 214, 129, 55, 154, 128, 32, 4, 201, 114, 110, 175, 33, 250, 89, 22, 203, + 194, 137, 227, 107, 31, 82, 20, 62, 160, 204, 121, 71, 65, 18, 220, 240, 245, 105, 137, 65, + 104, 186, 32, 5, 73, 163, 150, 210, 209, 44, 45, 88, 147, 177, 140, 73, 245, 231, 52, 114, 8, + 113, 216, 127, 88, 253, 134, 215, 221, 35, 183, 71, 99, 55, 163, 32, 4, 183, 149, 133, 222, 16, + 181, 158, 187, 26, 112, 160, 13, 165, 89, 191, 175, 117, 135, 204, 186, 117, 164, 118, 218, + 181, 24, 248, 8, 182, 165, 181, 32, 5, 180, 94, 217, 181, 61, 240, 200, 208, 79, 68, 123, 238, + 236, 167, 131, 241, 128, 31, 247, 36, 252, 212, 75, 196, 240, 89, 232, 91, 20, 91, 209, 32, 4, + 44, 50, 77, 67, 251, 45, 217, 70, 42, 101, 206, 195, 184, 161, 10, 85, 151, 59, 51, 28, 208, + 81, 78, 247, 241, 88, 37, 195, 149, 151, 228, 32, 2, 97, 27, 155, 37, 146, 202, 43, 214, 62, + 62, 237, 12, 122, 139, 243, 242, 150, 242, 183, 49, 130, 122, 247, 48, 56, 106, 114, 143, 235, + 8, 79, 32, 2, 185, 124, 96, 183, 155, 14, 136, 208, 75, 114, 37, 245, 191, 178, 178, 63, 111, + 67, 60, 28, 27, 238, 221, 224, 240, 253, 47, 91, 239, 13, 179, 32, 2, 185, 124, 96, 183, 155, + 14, 136, 208, 75, 114, 37, 245, 191, 178, 178, 63, 111, 67, 60, 28, 27, 238, 221, 224, 240, + 253, 47, 91, 239, 13, 179, 32, 2, 185, 124, 96, 183, 155, 14, 136, 208, 75, 114, 37, 245, 191, + 178, 178, 63, 111, 67, 60, 28, 27, 238, 221, 224, 240, 253, 47, 91, 239, 13, 179, 32, 3, 81, + 15, 195, 103, 39, 66, 162, 136, 92, 92, 14, 153, 166, 21, 71, 131, 158, 181, 10, 33, 207, 138, + 191, 11, 61, 159, 8, 59, 196, 116, 206, 32, 6, 92, 174, 186, 3, 163, 232, 46, 142, 159, 231, + 236, 199, 52, 201, 253, 94, 196, 194, 27, 170, 65, 56, 3, 235, 54, 159, 71, 74, 224, 145, 194, + 32, 7, 37, 192, 191, 55, 232, 222, 163, 133, 119, 204, 154, 2, 252, 68, 204, 127, 35, 115, 18, + 255, 101, 92, 159, 113, 38, 148, 11, 88, 14, 188, 24, 32, 1, 185, 157, 208, 201, 232, 187, 167, + 69, 41, 191, 112, 20, 178, 90, 158, 106, 103, 187, 169, 152, 209, 138, 82, 222, 48, 151, 43, + 211, 122, 139, 62, 32, 0, 82, 151, 15, 254, 101, 72, 162, 180, 25, 122, 196, 91, 240, 198, 230, + 133, 210, 171, 61, 168, 31, 207, 166, 62, 126, 137, 58, 58, 215, 89, 196, 32, 7, 243, 45, 235, + 180, 10, 147, 108, 102, 148, 41, 190, 1, 4, 246, 173, 38, 149, 22, 241, 244, 63, 151, 200, 36, + 150, 99, 141, 148, 213, 170, 198, 32, 3, 127, 184, 40, 17, 194, 24, 186, 31, 167, 103, 162, 171, 234, 52, 191, 197, 201, 175, 217, 230, 31, 216, 93, 227, 79, 185, 7, 14, 166, 193, 138, 32, 5, 198, 163, 129, 217, 40, 49, 109, 212, 20, 113, 205, 18, 187, 6, 2, 41, 105, 178, 32, 112, 127, 81, 84, 120, 159, 217, 95, 160, 16, 1, 38, 32, 0, 214, 196, 180, 99, 92, 89, 104, @@ -207,56 +207,95 @@ static PROOF: [u8; 25527] = [ 161, 129, 74, 133, 100, 113, 62, 104, 54, 249, 65, 156, 152, 203, 181, 174, 32, 7, 10, 198, 8, 71, 203, 123, 22, 215, 252, 95, 209, 228, 106, 1, 250, 148, 203, 149, 7, 35, 101, 250, 210, 186, 174, 64, 246, 179, 223, 66, 30, 32, 5, 242, 65, 116, 15, 209, 144, 160, 137, 244, 39, 200, - 223, 20, 127, 84, 108, 194, 233, 203, 81, 191, 36, 35, 67, 165, 197, 81, 185, 130, 37, 193, 59, - 2, 109, 191, 15, 222, 88, 251, 175, 15, 246, 130, 107, 105, 199, 118, 215, 241, 134, 76, 221, - 63, 47, 49, 81, 45, 0, 176, 60, 72, 117, 236, 249, 84, 2, 32, 3, 48, 127, 250, 48, 148, 100, - 159, 213, 218, 177, 58, 105, 139, 239, 218, 169, 185, 129, 164, 21, 88, 237, 88, 82, 191, 111, - 215, 137, 76, 223, 150, 32, 6, 16, 251, 113, 251, 35, 236, 142, 170, 88, 82, 203, 6, 0, 233, - 114, 105, 131, 238, 92, 207, 172, 58, 109, 219, 24, 246, 118, 55, 208, 230, 78, 5, 82, 112, - 121, 238, 185, 141, 1, 80, 168, 186, 34, 154, 225, 245, 139, 2, 123, 218, 190, 111, 15, 255, - 121, 41, 116, 227, 152, 42, 33, 168, 14, 1, 91, 35, 62, 84, 79, 132, 71, 170, 171, 23, 112, - 214, 190, 237, 191, 69, 250, 105, 10, 169, 108, 130, 87, 63, 201, 38, 178, 114, 139, 43, 91, - 113, 197, 141, 75, 213, 227, 174, 88, 250, 176, 106, 37, 76, 216, 107, 19, 138, 88, 156, 239, - 72, 27, 21, 218, 19, 60, 112, 156, 230, 158, 109, 190, 37, 168, 189, 205, 25, 14, 92, 102, 145, - 190, 239, 54, 179, 10, 15, 6, 103, 175, 66, 228, 134, 136, 118, 9, 64, 139, 92, 75, 55, 96, - 218, 229, 124, 227, 68, 31, 40, 194, 252, 219, 96, 27, 0, 152, 179, 217, 227, 210, 255, 77, 23, - 81, 166, 105, 218, 253, 13, 104, 220, 10, 192, 184, 18, 0, 193, 32, 1, 104, 12, 185, 205, 138, - 208, 244, 253, 33, 222, 248, 187, 128, 233, 27, 56, 12, 110, 239, 76, 137, 124, 240, 234, 232, - 103, 31, 240, 100, 98, 53, 3, 5, 6, 115, 121, 6, 85, 176, 150, 169, 85, 8, 57, 5, 144, 154, 23, - 153, 192, 202, 71, 43, 105, 225, 171, 19, 208, 87, 5, 6, 31, 239, 175, 229, 64, 33, 47, 206, 7, - 162, 188, 218, 42, 204, 87, 160, 251, 213, 62, 180, 7, 121, 99, 0, 211, 63, 30, 254, 106, 31, - 176, 41, 25, 175, 80, 100, 190, 111, 88, 75, 217, 188, 235, 191, 225, 117, 197, 67, 219, 63, - 231, 94, 69, 23, 155, 115, 39, 126, 66, 230, 232, 97, 65, 196, 47, 174, 63, 3, 102, 12, 170, - 97, 193, 165, 130, 39, 228, 52, 78, 243, 4, 108, 238, 148, 139, 4, 138, 220, 22, 151, 90, 245, - 199, 228, 126, 112, 63, 238, 140, 3, 100, 141, 244, 146, 128, 230, 70, 232, 217, 250, 154, 27, - 231, 23, 163, 61, 230, 124, 50, 221, 102, 196, 17, 93, 22, 222, 37, 204, 3, 54, 252, 116, 208, - 45, 93, 164, 82, 210, 92, 91, 63, 69, 76, 186, 185, 17, 78, 26, 238, 81, 20, 223, 109, 188, - 216, 28, 7, 139, 13, 241, 111, 119, 115, 3, 223, 5, 138, 86, 3, 251, 12, 37, 26, 26, 37, 229, - 31, 77, 213, 196, 29, 94, 132, 241, 23, 42, 110, 8, 144, 8, 241, 120, 250, 91, 227, 24, 59, - 118, 27, 166, 110, 151, 252, 42, 38, 13, 148, 178, 163, 7, 86, 243, 206, 99, 51, 45, 174, 176, - 2, 176, 222, 79, 185, 46, 239, 213, 231, 110, 203, 243, 231, 144, 68, 128, 118, 48, 62, 253, - 17, 89, 151, 143, 22, 34, 87, 213, 31, 37, 220, 227, 16, 247, 190, 214, 150, 187, 105, 125, - 102, 15, 145, 3, 159, 192, 79, 117, 81, 131, 127, 69, 145, 20, 160, 108, 209, 65, 86, 163, 214, - 220, 48, 231, 113, 225, 26, 192, 222, 215, 102, 154, 77, 26, 184, 181, 230, 178, 31, 28, 242, - 118, 216, 199, 237, 31, 119, 2, 113, 240, 112, 172, 197, 210, 98, 201, 91, 235, 196, 125, 20, - 119, 2, 25, 24, 146, 211, 241, 4, 74, 100, 162, 210, 220, 234, 124, 46, 120, 142, 236, 102, - 152, 212, 37, 114, 126, 89, 239, 119, 17, 248, 231, 171, 61, 108, 232, 175, 196, 62, 194, 69, - 13, 46, 84, 234, 17, 3, 21, 46, 232, 96, 9, 70, 128, 36, 230, 16, 165, 191, 254, 148, 41, 202, - 229, 89, 212, 233, 141, 168, 174, 229, 140, 224, 81, 97, 29, 1, 23, 2, 22, 151, 247, 233, 81, - 79, 170, 158, 249, 229, 199, 81, 89, 200, 216, 145, 38, 153, 216, 65, 34, 219, 99, 193, 248, - 36, 23, 36, 129, 51, 155, 81, 170, 123, 1, 59, 160, 203, 139, 28, 197, 58, 211, 230, 37, 31, - 85, 193, 140, 119, 108, 130, 78, 25, 191, 43, 91, 161, 3, 0, 250, 166, 193, 194, 161, 166, 73, - 214, 204, 218, 13, 80, 76, 118, 250, 79, 222, 128, 150, 252, 245, 253, 158, 102, 27, 172, 50, - 192, 131, 192, 147, 28, 23, 189, 214, 38, 116, 4, 248, 192, 87, 143, 63, 134, 25, 6, 201, 48, - 121, 23, 233, 211, 162, 185, 219, 176, 27, 21, 61, 121, 58, 228, 60, 47, 126, 131, 56, 51, 84, - 132, 13, 81, 124, 22, 98, 17, 50, 110, 109, 59, 181, 109, 154, 84, 88, 60, 188, 0, 191, 64, 46, - 229, 182, 32, 20, 2, 74, 42, 18, 235, 9, 249, 64, 116, 65, 54, 67, 1, 118, 34, 236, 213, 63, - 88, 202, 131, 114, 138, 154, 105, 29, 58, 106, 66, 201, 200, 74, 150, 27, 149, 159, 90, 213, - 12, 112, 252, 64, 244, 104, 220, 50, 128, 113, 201, 104, 20, 107, 144, 30, 58, 28, 189, 44, 89, - 107, 176, 167, 113, 52, 250, 5, 32, 2, 78, 97, 121, 127, 238, 47, 119, 199, 15, 200, 125, 16, - 150, 254, 168, 168, 59, 109, 247, 150, 38, 227, 91, 124, 212, 64, 194, 25, 127, 188, 125, 32, - 0, 113, 249, 249, 255, 228, 13, 136, 153, 122, 192, 187, 56, 42, 197, 101, 118, 59, 124, 61, - 95, 37, 92, 208, 123, 153, 43, 38, 94, 210, 169, 139, 32, 6, 167, 37, 185, 208, 123, 36, 223, + 223, 20, 127, 84, 108, 194, 233, 203, 81, 191, 36, 35, 67, 165, 197, 81, 185, 130, 37, 193, 23, + 2, 1, 109, 191, 15, 222, 88, 251, 175, 15, 246, 130, 107, 105, 199, 118, 215, 241, 134, 76, + 221, 63, 47, 49, 81, 45, 0, 176, 60, 72, 117, 236, 249, 84, 2, 32, 3, 48, 127, 250, 48, 148, + 100, 159, 213, 218, 177, 58, 105, 139, 239, 218, 169, 185, 129, 164, 21, 88, 237, 88, 82, 191, + 111, 215, 137, 76, 223, 150, 32, 6, 16, 251, 113, 251, 35, 236, 142, 170, 88, 82, 203, 6, 0, + 233, 114, 105, 131, 238, 92, 207, 172, 58, 109, 219, 24, 246, 118, 55, 208, 230, 78, 5, 82, + 112, 121, 238, 185, 141, 1, 80, 168, 186, 34, 154, 225, 245, 139, 2, 123, 218, 190, 111, 15, + 255, 121, 41, 116, 227, 152, 42, 33, 168, 14, 1, 91, 35, 62, 84, 79, 132, 71, 170, 171, 23, + 112, 214, 190, 237, 191, 69, 250, 105, 10, 169, 108, 130, 87, 63, 201, 38, 178, 114, 139, 43, + 91, 113, 197, 141, 75, 213, 227, 174, 88, 250, 176, 106, 37, 76, 216, 107, 19, 138, 88, 156, + 239, 72, 27, 21, 218, 19, 60, 112, 156, 230, 158, 109, 190, 37, 168, 189, 205, 25, 14, 92, 102, + 145, 190, 239, 54, 179, 10, 15, 6, 103, 175, 66, 228, 134, 136, 118, 9, 64, 139, 92, 75, 55, + 96, 218, 229, 124, 227, 68, 31, 40, 194, 252, 219, 96, 27, 0, 152, 179, 217, 227, 210, 255, 77, + 23, 81, 166, 105, 218, 253, 13, 104, 220, 10, 192, 184, 18, 0, 193, 32, 1, 104, 12, 185, 205, + 138, 208, 244, 253, 33, 222, 248, 187, 128, 233, 27, 56, 12, 110, 239, 76, 137, 124, 240, 234, + 232, 103, 31, 240, 100, 98, 53, 3, 5, 6, 115, 121, 6, 85, 176, 150, 169, 85, 8, 57, 5, 144, + 154, 23, 153, 192, 202, 71, 43, 105, 225, 171, 19, 208, 87, 5, 6, 31, 239, 175, 229, 64, 33, + 47, 206, 7, 162, 188, 218, 42, 204, 87, 160, 251, 213, 62, 180, 7, 121, 99, 0, 211, 63, 30, + 254, 106, 31, 176, 41, 25, 175, 80, 100, 190, 111, 88, 75, 217, 188, 235, 191, 225, 117, 197, + 67, 219, 63, 231, 94, 69, 23, 155, 115, 39, 126, 66, 230, 232, 97, 65, 196, 47, 174, 63, 3, + 102, 12, 170, 97, 193, 165, 130, 39, 228, 52, 78, 243, 4, 108, 238, 148, 139, 4, 138, 220, 22, + 151, 90, 245, 199, 228, 126, 112, 63, 238, 140, 3, 100, 141, 244, 146, 128, 230, 70, 232, 217, + 250, 154, 27, 231, 23, 163, 61, 230, 124, 50, 221, 102, 196, 17, 93, 22, 222, 37, 204, 3, 54, + 252, 116, 208, 45, 93, 164, 82, 210, 92, 91, 63, 69, 76, 186, 185, 17, 78, 26, 238, 81, 20, + 223, 109, 188, 216, 28, 7, 139, 13, 241, 111, 119, 115, 3, 223, 5, 138, 86, 3, 251, 12, 37, 26, + 26, 37, 229, 31, 77, 213, 196, 29, 94, 132, 241, 23, 42, 110, 8, 144, 8, 241, 120, 250, 91, + 227, 24, 59, 118, 27, 166, 110, 151, 252, 42, 38, 13, 148, 178, 163, 7, 86, 243, 206, 99, 51, + 45, 174, 176, 2, 176, 222, 79, 185, 46, 239, 213, 231, 110, 203, 243, 231, 144, 68, 128, 118, + 48, 62, 253, 17, 89, 151, 143, 22, 34, 87, 213, 31, 37, 220, 227, 16, 247, 190, 214, 150, 187, + 105, 125, 102, 15, 145, 3, 159, 192, 79, 117, 81, 131, 127, 69, 145, 20, 160, 108, 209, 65, 86, + 163, 214, 220, 48, 231, 113, 225, 26, 192, 222, 215, 102, 154, 77, 26, 184, 181, 230, 178, 31, + 28, 242, 118, 216, 199, 237, 31, 119, 2, 113, 240, 112, 172, 197, 210, 98, 201, 91, 235, 196, + 125, 20, 119, 2, 25, 24, 146, 211, 241, 4, 74, 100, 162, 210, 220, 234, 124, 46, 120, 142, 236, + 102, 152, 212, 37, 114, 126, 89, 239, 119, 17, 248, 231, 171, 61, 108, 232, 175, 196, 62, 194, + 69, 13, 46, 84, 234, 17, 3, 21, 46, 232, 96, 9, 70, 128, 36, 230, 16, 165, 191, 254, 148, 41, + 202, 229, 89, 212, 233, 141, 168, 174, 229, 140, 224, 81, 97, 29, 1, 23, 2, 22, 151, 247, 233, + 81, 79, 170, 158, 249, 229, 199, 81, 89, 200, 216, 145, 38, 153, 216, 65, 34, 219, 99, 193, + 248, 36, 23, 36, 129, 51, 155, 81, 170, 123, 1, 59, 160, 203, 139, 28, 197, 58, 211, 230, 37, + 31, 85, 193, 140, 119, 108, 130, 78, 25, 191, 43, 91, 161, 3, 0, 250, 166, 193, 194, 161, 166, + 73, 214, 204, 218, 13, 80, 76, 118, 250, 79, 222, 128, 150, 252, 245, 253, 158, 102, 27, 172, + 50, 192, 131, 192, 147, 28, 23, 189, 214, 38, 116, 4, 248, 192, 87, 143, 63, 134, 25, 6, 201, + 48, 121, 23, 233, 211, 162, 185, 219, 176, 27, 21, 61, 121, 58, 228, 60, 47, 126, 131, 56, 51, + 84, 132, 13, 81, 124, 22, 98, 17, 50, 110, 109, 59, 181, 109, 154, 84, 88, 60, 188, 0, 191, 64, + 46, 229, 182, 32, 20, 2, 74, 42, 18, 235, 9, 249, 64, 116, 65, 54, 67, 1, 118, 34, 236, 213, + 63, 88, 202, 131, 114, 138, 154, 105, 29, 58, 106, 66, 201, 200, 74, 150, 27, 149, 159, 90, + 213, 12, 112, 252, 64, 244, 104, 220, 50, 128, 113, 201, 104, 20, 107, 144, 30, 58, 28, 189, + 44, 89, 107, 176, 167, 113, 52, 250, 5, 32, 2, 78, 97, 121, 127, 238, 47, 119, 199, 15, 200, + 125, 16, 150, 254, 168, 168, 59, 109, 247, 150, 38, 227, 91, 124, 212, 64, 194, 25, 127, 188, + 125, 32, 0, 113, 249, 249, 255, 228, 13, 136, 153, 122, 192, 187, 56, 42, 197, 101, 118, 59, + 124, 61, 95, 37, 92, 208, 123, 153, 43, 38, 94, 210, 169, 139, 32, 6, 167, 37, 185, 208, 123, + 36, 223, 152, 196, 150, 147, 157, 29, 252, 246, 66, 97, 248, 67, 241, 28, 215, 27, 63, 0, 229, + 114, 99, 207, 95, 21, 32, 2, 112, 59, 63, 171, 54, 166, 178, 221, 202, 101, 39, 130, 200, 103, + 184, 44, 166, 220, 246, 108, 106, 76, 54, 33, 134, 47, 117, 48, 240, 255, 173, 32, 5, 196, 143, + 35, 233, 0, 32, 54, 82, 255, 118, 12, 30, 80, 201, 187, 151, 120, 176, 215, 146, 164, 12, 194, + 190, 166, 214, 43, 224, 224, 149, 217, 5, 6, 168, 38, 220, 25, 149, 71, 84, 129, 64, 73, 73, + 59, 140, 69, 111, 67, 195, 15, 178, 147, 177, 105, 84, 186, 79, 63, 194, 33, 85, 112, 1, 213, + 33, 47, 206, 7, 162, 188, 218, 42, 204, 87, 160, 251, 213, 62, 180, 7, 121, 99, 0, 211, 63, 30, + 254, 106, 31, 176, 41, 25, 175, 80, 100, 190, 111, 88, 75, 217, 188, 235, 191, 225, 117, 197, + 67, 219, 63, 231, 94, 69, 23, 155, 115, 39, 126, 66, 230, 232, 97, 65, 196, 47, 174, 63, 3, + 102, 12, 170, 97, 193, 165, 130, 39, 228, 52, 78, 243, 4, 108, 238, 148, 139, 4, 138, 220, 22, + 151, 90, 245, 199, 228, 126, 112, 63, 238, 140, 3, 100, 141, 244, 146, 128, 230, 70, 232, 217, + 250, 154, 27, 231, 23, 163, 61, 230, 124, 50, 221, 102, 196, 17, 93, 22, 222, 37, 204, 3, 54, + 252, 116, 208, 45, 93, 164, 82, 210, 92, 91, 63, 69, 76, 186, 185, 17, 78, 26, 238, 81, 20, + 223, 109, 188, 216, 28, 7, 139, 13, 241, 111, 119, 115, 3, 223, 5, 138, 86, 3, 251, 12, 37, 26, + 26, 37, 229, 31, 77, 213, 196, 29, 94, 132, 241, 23, 42, 110, 8, 144, 8, 241, 120, 250, 91, + 227, 24, 59, 118, 27, 166, 110, 151, 252, 42, 38, 13, 148, 178, 163, 7, 86, 243, 206, 99, 51, + 45, 174, 176, 2, 176, 222, 79, 185, 46, 239, 213, 231, 110, 203, 243, 231, 144, 68, 128, 118, + 48, 62, 253, 17, 89, 151, 143, 22, 34, 87, 213, 31, 37, 220, 227, 16, 247, 190, 214, 150, 187, + 105, 125, 102, 15, 145, 3, 159, 192, 79, 117, 81, 131, 127, 69, 145, 20, 160, 108, 209, 65, 86, + 163, 214, 220, 48, 231, 113, 225, 26, 192, 222, 215, 102, 154, 77, 26, 184, 181, 230, 178, 31, + 28, 242, 118, 216, 199, 237, 31, 119, 2, 113, 240, 112, 172, 197, 210, 98, 201, 91, 235, 196, + 125, 20, 119, 2, 25, 24, 146, 211, 241, 4, 74, 100, 162, 210, 220, 234, 124, 46, 120, 142, 236, + 102, 152, 212, 37, 114, 126, 89, 239, 119, 17, 248, 231, 171, 61, 108, 232, 175, 196, 62, 194, + 69, 13, 46, 84, 234, 17, 3, 21, 46, 232, 96, 9, 70, 128, 36, 230, 16, 165, 191, 254, 148, 41, + 202, 229, 89, 212, 233, 141, 168, 174, 229, 140, 224, 81, 97, 29, 1, 23, 2, 22, 151, 247, 233, + 81, 79, 170, 158, 249, 229, 199, 81, 89, 200, 216, 145, 38, 153, 216, 65, 34, 219, 99, 193, + 248, 36, 23, 36, 129, 51, 155, 81, 170, 123, 1, 59, 160, 203, 139, 28, 197, 58, 211, 230, 37, + 31, 85, 193, 140, 119, 108, 130, 78, 25, 191, 43, 91, 161, 3, 0, 250, 166, 193, 194, 161, 166, + 73, 214, 204, 218, 13, 80, 76, 118, 250, 79, 222, 128, 150, 252, 245, 253, 158, 102, 27, 172, + 50, 192, 131, 192, 147, 28, 23, 189, 214, 38, 116, 4, 248, 192, 87, 143, 63, 134, 25, 6, 201, + 48, 121, 23, 233, 211, 162, 185, 219, 176, 27, 21, 61, 121, 58, 228, 60, 47, 126, 131, 56, 51, + 84, 132, 13, 81, 124, 22, 98, 17, 50, 110, 109, 59, 181, 109, 154, 84, 88, 60, 188, 0, 191, 64, + 46, 229, 182, 32, 20, 2, 74, 42, 18, 235, 9, 249, 64, 116, 65, 54, 67, 1, 118, 34, 236, 213, + 63, 88, 202, 131, 114, 138, 154, 105, 29, 58, 106, 66, 201, 200, 74, 150, 27, 149, 159, 90, + 213, 12, 112, 252, 64, 244, 104, 220, 50, 128, 113, 201, 104, 20, 107, 144, 30, 58, 28, 189, + 44, 89, 107, 176, 167, 113, 52, 250, 5, 32, 4, 87, 105, 19, 100, 49, 206, 121, 89, 252, 243, + 252, 225, 44, 180, 118, 113, 8, 186, 165, 2, 200, 56, 154, 176, 142, 73, 83, 118, 20, 113, 72, + 32, 6, 136, 174, 25, 103, 129, 228, 236, 152, 40, 59, 146, 249, 150, 237, 20, 81, 215, 10, 200, + 139, 59, 35, 133, 200, 43, 47, 215, 22, 184, 229, 2, 32, 6, 167, 37, 185, 208, 123, 36, 223, 152, 196, 150, 147, 157, 29, 252, 246, 66, 97, 248, 67, 241, 28, 215, 27, 63, 0, 229, 114, 99, 207, 95, 21, 32, 2, 112, 59, 63, 171, 54, 166, 178, 221, 202, 101, 39, 130, 200, 103, 184, 44, 166, 220, 246, 108, 106, 76, 54, 33, 134, 47, 117, 48, 240, 255, 173, 32, 5, 196, 143, 35, 233, @@ -300,45 +339,6 @@ static PROOF: [u8; 25527] = [ 95, 21, 32, 2, 112, 59, 63, 171, 54, 166, 178, 221, 202, 101, 39, 130, 200, 103, 184, 44, 166, 220, 246, 108, 106, 76, 54, 33, 134, 47, 117, 48, 240, 255, 173, 32, 5, 196, 143, 35, 233, 0, 32, 54, 82, 255, 118, 12, 30, 80, 201, 187, 151, 120, 176, 215, 146, 164, 12, 194, 190, 166, - 214, 43, 224, 224, 149, 217, 5, 6, 168, 38, 220, 25, 149, 71, 84, 129, 64, 73, 73, 59, 140, 69, - 111, 67, 195, 15, 178, 147, 177, 105, 84, 186, 79, 63, 194, 33, 85, 112, 1, 213, 33, 47, 206, - 7, 162, 188, 218, 42, 204, 87, 160, 251, 213, 62, 180, 7, 121, 99, 0, 211, 63, 30, 254, 106, - 31, 176, 41, 25, 175, 80, 100, 190, 111, 88, 75, 217, 188, 235, 191, 225, 117, 197, 67, 219, - 63, 231, 94, 69, 23, 155, 115, 39, 126, 66, 230, 232, 97, 65, 196, 47, 174, 63, 3, 102, 12, - 170, 97, 193, 165, 130, 39, 228, 52, 78, 243, 4, 108, 238, 148, 139, 4, 138, 220, 22, 151, 90, - 245, 199, 228, 126, 112, 63, 238, 140, 3, 100, 141, 244, 146, 128, 230, 70, 232, 217, 250, 154, - 27, 231, 23, 163, 61, 230, 124, 50, 221, 102, 196, 17, 93, 22, 222, 37, 204, 3, 54, 252, 116, - 208, 45, 93, 164, 82, 210, 92, 91, 63, 69, 76, 186, 185, 17, 78, 26, 238, 81, 20, 223, 109, - 188, 216, 28, 7, 139, 13, 241, 111, 119, 115, 3, 223, 5, 138, 86, 3, 251, 12, 37, 26, 26, 37, - 229, 31, 77, 213, 196, 29, 94, 132, 241, 23, 42, 110, 8, 144, 8, 241, 120, 250, 91, 227, 24, - 59, 118, 27, 166, 110, 151, 252, 42, 38, 13, 148, 178, 163, 7, 86, 243, 206, 99, 51, 45, 174, - 176, 2, 176, 222, 79, 185, 46, 239, 213, 231, 110, 203, 243, 231, 144, 68, 128, 118, 48, 62, - 253, 17, 89, 151, 143, 22, 34, 87, 213, 31, 37, 220, 227, 16, 247, 190, 214, 150, 187, 105, - 125, 102, 15, 145, 3, 159, 192, 79, 117, 81, 131, 127, 69, 145, 20, 160, 108, 209, 65, 86, 163, - 214, 220, 48, 231, 113, 225, 26, 192, 222, 215, 102, 154, 77, 26, 184, 181, 230, 178, 31, 28, - 242, 118, 216, 199, 237, 31, 119, 2, 113, 240, 112, 172, 197, 210, 98, 201, 91, 235, 196, 125, - 20, 119, 2, 25, 24, 146, 211, 241, 4, 74, 100, 162, 210, 220, 234, 124, 46, 120, 142, 236, 102, - 152, 212, 37, 114, 126, 89, 239, 119, 17, 248, 231, 171, 61, 108, 232, 175, 196, 62, 194, 69, - 13, 46, 84, 234, 17, 3, 21, 46, 232, 96, 9, 70, 128, 36, 230, 16, 165, 191, 254, 148, 41, 202, - 229, 89, 212, 233, 141, 168, 174, 229, 140, 224, 81, 97, 29, 1, 23, 2, 22, 151, 247, 233, 81, - 79, 170, 158, 249, 229, 199, 81, 89, 200, 216, 145, 38, 153, 216, 65, 34, 219, 99, 193, 248, - 36, 23, 36, 129, 51, 155, 81, 170, 123, 1, 59, 160, 203, 139, 28, 197, 58, 211, 230, 37, 31, - 85, 193, 140, 119, 108, 130, 78, 25, 191, 43, 91, 161, 3, 0, 250, 166, 193, 194, 161, 166, 73, - 214, 204, 218, 13, 80, 76, 118, 250, 79, 222, 128, 150, 252, 245, 253, 158, 102, 27, 172, 50, - 192, 131, 192, 147, 28, 23, 189, 214, 38, 116, 4, 248, 192, 87, 143, 63, 134, 25, 6, 201, 48, - 121, 23, 233, 211, 162, 185, 219, 176, 27, 21, 61, 121, 58, 228, 60, 47, 126, 131, 56, 51, 84, - 132, 13, 81, 124, 22, 98, 17, 50, 110, 109, 59, 181, 109, 154, 84, 88, 60, 188, 0, 191, 64, 46, - 229, 182, 32, 20, 2, 74, 42, 18, 235, 9, 249, 64, 116, 65, 54, 67, 1, 118, 34, 236, 213, 63, - 88, 202, 131, 114, 138, 154, 105, 29, 58, 106, 66, 201, 200, 74, 150, 27, 149, 159, 90, 213, - 12, 112, 252, 64, 244, 104, 220, 50, 128, 113, 201, 104, 20, 107, 144, 30, 58, 28, 189, 44, 89, - 107, 176, 167, 113, 52, 250, 5, 32, 4, 87, 105, 19, 100, 49, 206, 121, 89, 252, 243, 252, 225, - 44, 180, 118, 113, 8, 186, 165, 2, 200, 56, 154, 176, 142, 73, 83, 118, 20, 113, 72, 32, 6, - 136, 174, 25, 103, 129, 228, 236, 152, 40, 59, 146, 249, 150, 237, 20, 81, 215, 10, 200, 139, - 59, 35, 133, 200, 43, 47, 215, 22, 184, 229, 2, 32, 6, 167, 37, 185, 208, 123, 36, 223, 152, - 196, 150, 147, 157, 29, 252, 246, 66, 97, 248, 67, 241, 28, 215, 27, 63, 0, 229, 114, 99, 207, - 95, 21, 32, 2, 112, 59, 63, 171, 54, 166, 178, 221, 202, 101, 39, 130, 200, 103, 184, 44, 166, - 220, 246, 108, 106, 76, 54, 33, 134, 47, 117, 48, 240, 255, 173, 32, 5, 196, 143, 35, 233, 0, - 32, 54, 82, 255, 118, 12, 30, 80, 201, 187, 151, 120, 176, 215, 146, 164, 12, 194, 190, 166, 214, 43, 224, 224, 149, 217, 3, 7, 126, 40, 243, 172, 167, 175, 234, 240, 174, 123, 250, 6, 48, 63, 188, 203, 225, 130, 112, 128, 54, 46, 62, 66, 37, 235, 178, 113, 16, 113, 73, 110, 112, 159, 196, 68, 95, 225, 214, 36, 29, 252, 221, 60, 143, 203, 240, 62, 161, 247, 182, 212, 232, diff --git a/provers/stark/src/constraints/boundary.rs b/provers/stark/src/constraints/boundary.rs index 6fc6e97c5..50a4bbb98 100644 --- a/provers/stark/src/constraints/boundary.rs +++ b/provers/stark/src/constraints/boundary.rs @@ -14,19 +14,45 @@ pub struct BoundaryConstraint { pub col: usize, pub step: usize, pub value: FieldElement, + pub is_aux: bool, } impl BoundaryConstraint { - pub fn new(col: usize, step: usize, value: FieldElement) -> Self { - Self { col, step, value } + pub fn new_main(col: usize, step: usize, value: FieldElement) -> Self { + Self { + col, + step, + value, + is_aux: false, + } + } + + pub fn new_aux(col: usize, step: usize, value: FieldElement) -> Self { + Self { + col, + step, + value, + is_aux: true, + } + } + + /// Used for creating boundary constraints for a trace with only one column + pub fn new_simple_main(step: usize, value: FieldElement) -> Self { + Self { + col: 0, + step, + value, + is_aux: false, + } } /// Used for creating boundary constraints for a trace with only one column - pub fn new_simple(step: usize, value: FieldElement) -> Self { + pub fn new_simple_aux(step: usize, value: FieldElement) -> Self { Self { col: 0, step, value, + is_aux: true, } } } @@ -150,9 +176,9 @@ mod test { // * a0 = 1 // * a1 = 1 // * a7 = 32 - let a0 = BoundaryConstraint::new_simple(0, one); - let a1 = BoundaryConstraint::new_simple(1, one); - let result = BoundaryConstraint::new_simple(7, FieldElement::::from(32)); + let a0 = BoundaryConstraint::new_simple_main(0, one); + let a1 = BoundaryConstraint::new_simple_main(1, one); + let result = BoundaryConstraint::new_simple_main(7, FieldElement::::from(32)); let constraints = BoundaryConstraints::from_constraints(vec![a0, a1, result]); diff --git a/provers/stark/src/constraints/evaluator.rs b/provers/stark/src/constraints/evaluator.rs index 6850f5314..1cc889b73 100644 --- a/provers/stark/src/constraints/evaluator.rs +++ b/provers/stark/src/constraints/evaluator.rs @@ -17,9 +17,8 @@ use rayon::prelude::{ use super::boundary::BoundaryConstraints; #[cfg(all(debug_assertions, not(feature = "parallel")))] use crate::debug::check_boundary_polys_divisibility; -use crate::domain::Domain; -use crate::trace::TraceTable; use crate::traits::AIR; +use crate::{domain::Domain, table::EvaluationTable}; use crate::{frame::Frame, prover::evaluate_polynomial_on_lde_domain}; pub struct ConstraintEvaluator { @@ -34,10 +33,10 @@ impl ConstraintEvaluator { } } - pub fn evaluate( + pub(crate) fn evaluate( &self, air: &A, - lde_trace: &TraceTable, + lde_table: &EvaluationTable, domain: &Domain, transition_coefficients: &[FieldElement], boundary_coefficients: &[FieldElement], @@ -83,27 +82,30 @@ impl ConstraintEvaluator { &domain.coset_offset, ) }) - .collect::>>, FFTError>>() + .collect::>>, FFTError>>() .unwrap(); - let n_col = lde_trace.n_cols(); - let n_elem = domain.lde_roots_of_unity_coset.len(); let boundary_polys_evaluations = boundary_constraints .constraints .iter() .map(|constraint| { - let col = constraint.col; - lde_trace - .table - .data - .iter() - .skip(col) - .step_by(n_col) - .take(n_elem) - .map(|v| -&constraint.value + v) - .collect::>>() + if constraint.is_aux { + (0..lde_table.n_rows()) + .map(|row| { + let v = lde_table.get_aux(row, constraint.col); + v - &constraint.value + }) + .collect() + } else { + (0..lde_table.n_rows()) + .map(|row| { + let v = lde_table.get_main(row, constraint.col); + v - &constraint.value + }) + .collect() + } }) - .collect::>>>(); + .collect::>>>(); #[cfg(feature = "parallel")] let boundary_eval_iter = (0..domain.lde_roots_of_unity_coset.len()).into_par_iter(); @@ -182,8 +184,8 @@ impl ConstraintEvaluator { .zip(&boundary_evaluation) .zip(zerofier_iter) .map(|((i, boundary), zerofier)| { - let frame = Frame::read_from_trace( - lde_trace, + let frame = Frame::::read_from_lde_table( + lde_table, i, blowup_factor, &air.context().transition_offsets, @@ -191,13 +193,13 @@ impl ConstraintEvaluator { let periodic_values: Vec<_> = lde_periodic_columns .iter() - .map(|col| col[i].clone().to_extension()) + .map(|col| col[i].clone()) .collect(); // Compute all the transition constraints at this // point of the LDE domain. let evaluations_transition = - air.compute_transition(&frame, &periodic_values, rap_challenges); + air.compute_transition_prover(&frame, &periodic_values, rap_challenges); #[cfg(all(debug_assertions, not(feature = "parallel")))] transition_evaluations.push(evaluations_transition.clone()); diff --git a/provers/stark/src/debug.rs b/provers/stark/src/debug.rs index f9d264298..85fc3a1af 100644 --- a/provers/stark/src/debug.rs +++ b/provers/stark/src/debug.rs @@ -1,5 +1,4 @@ -use crate::frame::Frame; -use crate::trace::TraceTable; +use crate::{frame::Frame, table::EvaluationTable}; use super::domain::Domain; use super::traits::AIR; @@ -15,14 +14,26 @@ use log::{error, info}; /// Validates that the trace is valid with respect to the supplied AIR constraints pub fn validate_trace( air: &A, - trace_polys: &[Polynomial>], + main_trace_polys: &[Polynomial>], + aux_trace_polys: &[Polynomial>], domain: &Domain, rap_challenges: &A::RAPChallenges, ) -> bool { info!("Starting constraints validation over trace..."); let mut ret = true; - let trace_columns: Vec<_> = trace_polys + let main_trace_columns: Vec<_> = main_trace_polys + .iter() + .map(|poly| { + Polynomial::>::evaluate_fft::( + poly, + 1, + Some(domain.interpolation_domain_size), + ) + .unwrap() + }) + .collect(); + let aux_trace_columns: Vec<_> = aux_trace_polys .iter() .map(|poly| { Polynomial::evaluate_fft::(poly, 1, Some(domain.interpolation_domain_size)) @@ -30,14 +41,19 @@ pub fn validate_trace( }) .collect(); - let trace = TraceTable::from_columns(trace_columns, A::STEP_SIZE); + let lde_table = + EvaluationTable::from_columns(main_trace_columns, aux_trace_columns, A::STEP_SIZE); let periodic_columns: Vec<_> = air .get_periodic_column_polynomials() .iter() .map(|poly| { - Polynomial::evaluate_fft::(poly, 1, Some(domain.interpolation_domain_size)) - .unwrap() + Polynomial::>::evaluate_fft::( + poly, + 1, + Some(domain.interpolation_domain_size), + ) + .unwrap() }) .collect(); @@ -49,9 +65,14 @@ pub fn validate_trace( let col = constraint.col; let step = constraint.step; let boundary_value = constraint.value.clone(); - let trace_value = trace.get(step, col); - if &boundary_value.clone().to_extension() != trace_value { + let trace_value = if !constraint.is_aux { + lde_table.get_main(step, col).clone().to_extension() + } else { + lde_table.get_aux(step, col).clone() + }; + + if boundary_value.clone().to_extension() != trace_value { ret = false; error!("Boundary constraint inconsistency - Expected value {:?} in step {} and column {}, found: {:?}", boundary_value, step, col, trace_value); } @@ -61,21 +82,22 @@ pub fn validate_trace( let n_transition_constraints = air.context().num_transition_constraints(); let transition_exemptions = &air.context().transition_exemptions; - let exemption_steps: Vec = vec![trace.n_rows(); n_transition_constraints] + let exemption_steps: Vec = vec![lde_table.n_rows(); n_transition_constraints] .iter() .zip(transition_exemptions) .map(|(trace_steps, exemptions)| trace_steps - exemptions) .collect(); // Iterate over trace and compute transitions - for step in 0..trace.num_steps() { - let frame = Frame::read_from_trace(&trace, step, 1, &air.context().transition_offsets); + for step in 0..lde_table.num_steps() { + let frame = + Frame::read_from_lde_table(&lde_table, step, 1, &air.context().transition_offsets); let periodic_values: Vec<_> = periodic_columns .iter() .map(|col| col[step].clone()) .collect(); - let evaluations = air.compute_transition(&frame, &periodic_values, rap_challenges); + let evaluations = air.compute_transition_prover(&frame, &periodic_values, rap_challenges); // Iterate over each transition evaluation. When the evaluated step is not from // the exemption steps corresponding to the transition, it should have zero as a diff --git a/provers/stark/src/examples/dummy_air.rs b/provers/stark/src/examples/dummy_air.rs index d27353331..b85c49e9c 100644 --- a/provers/stark/src/examples/dummy_air.rs +++ b/provers/stark/src/examples/dummy_air.rs @@ -59,20 +59,20 @@ impl AIR for DummyAIR { _transcript: &mut impl IsStarkTranscript, ) -> Self::RAPChallenges { } - fn compute_transition( + fn compute_transition_prover( &self, - frame: &Frame, + frame: &Frame, _periodic_values: &[FieldElement], _rap_challenges: &Self::RAPChallenges, - ) -> Vec> { + ) -> Vec> { let first_step = frame.get_evaluation_step(0); let second_step = frame.get_evaluation_step(1); let third_step = frame.get_evaluation_step(2); - let flag = first_step.get_evaluation_element(0, 0); - let a0 = first_step.get_evaluation_element(0, 1); - let a1 = second_step.get_evaluation_element(0, 1); - let a2 = third_step.get_evaluation_element(0, 1); + let flag = first_step.get_main_evaluation_element(0, 0); + let a0 = first_step.get_main_evaluation_element(0, 1); + let a1 = second_step.get_main_evaluation_element(0, 1); + let a2 = third_step.get_main_evaluation_element(0, 1); let f_constraint = flag * (flag - FieldElement::one()); @@ -85,8 +85,8 @@ impl AIR for DummyAIR { &self, _rap_challenges: &Self::RAPChallenges, ) -> BoundaryConstraints { - let a0 = BoundaryConstraint::new(1, 0, FieldElement::::one()); - let a1 = BoundaryConstraint::new(1, 1, FieldElement::::one()); + let a0 = BoundaryConstraint::new_main(1, 0, FieldElement::::one()); + let a1 = BoundaryConstraint::new_main(1, 1, FieldElement::::one()); BoundaryConstraints::from_constraints(vec![a0, a1]) } @@ -110,6 +110,15 @@ impl AIR for DummyAIR { fn pub_inputs(&self) -> &Self::PublicInputs { &() } + + fn compute_transition_verifier( + &self, + frame: &Frame, + periodic_values: &[FieldElement], + rap_challenges: &Self::RAPChallenges, + ) -> Vec> { + self.compute_transition_prover(frame, periodic_values, rap_challenges) + } } pub fn dummy_trace(trace_length: usize) -> TraceTable { diff --git a/provers/stark/src/examples/fibonacci_2_cols_shifted.rs b/provers/stark/src/examples/fibonacci_2_cols_shifted.rs index c50e6b937..d5c220d01 100644 --- a/provers/stark/src/examples/fibonacci_2_cols_shifted.rs +++ b/provers/stark/src/examples/fibonacci_2_cols_shifted.rs @@ -93,20 +93,20 @@ where ) -> Self::RAPChallenges { } - fn compute_transition( + fn compute_transition_prover( &self, - frame: &Frame, + frame: &Frame, _periodic_values: &[FieldElement], _rap_challenges: &Self::RAPChallenges, ) -> Vec> { let first_row = frame.get_evaluation_step(0); let second_row = frame.get_evaluation_step(1); - let a0_0 = first_row.get_evaluation_element(0, 0); - let a0_1 = first_row.get_evaluation_element(0, 1); + let a0_0 = first_row.get_main_evaluation_element(0, 0); + let a0_1 = first_row.get_main_evaluation_element(0, 1); - let a1_0 = second_row.get_evaluation_element(0, 0); - let a1_1 = second_row.get_evaluation_element(0, 1); + let a1_0 = second_row.get_main_evaluation_element(0, 0); + let a1_1 = second_row.get_main_evaluation_element(0, 1); let first_transition = a1_0 - a0_1; let second_transition = a1_1 - a0_0 - a0_1; @@ -122,8 +122,8 @@ where &self, _rap_challenges: &Self::RAPChallenges, ) -> BoundaryConstraints { - let initial_condition = BoundaryConstraint::new(0, 0, FieldElement::one()); - let claimed_value_constraint = BoundaryConstraint::new( + let initial_condition = BoundaryConstraint::new_main(0, 0, FieldElement::one()); + let claimed_value_constraint = BoundaryConstraint::new_main( 0, self.pub_inputs.claimed_index, self.pub_inputs.claimed_value.clone(), @@ -147,6 +147,15 @@ where fn pub_inputs(&self) -> &Self::PublicInputs { &self.pub_inputs } + + fn compute_transition_verifier( + &self, + frame: &Frame, + periodic_values: &[FieldElement], + rap_challenges: &Self::RAPChallenges, + ) -> Vec> { + self.compute_transition_prover(frame, periodic_values, rap_challenges) + } } pub fn compute_trace( diff --git a/provers/stark/src/examples/fibonacci_2_columns.rs b/provers/stark/src/examples/fibonacci_2_columns.rs index 0534feded..98c93b72b 100644 --- a/provers/stark/src/examples/fibonacci_2_columns.rs +++ b/provers/stark/src/examples/fibonacci_2_columns.rs @@ -69,9 +69,9 @@ where ) -> Self::RAPChallenges { } - fn compute_transition( + fn compute_transition_prover( &self, - frame: &Frame, + frame: &Frame, _periodic_values: &[FieldElement], _rap_challenges: &Self::RAPChallenges, ) -> Vec> { @@ -81,10 +81,10 @@ where // constraints of Fibonacci sequence (2 terms per step): // s_{0, i+1} = s_{0, i} + s_{1, i} // s_{1, i+1} = s_{1, i} + s_{0, i+1} - let s0_0 = first_step.get_evaluation_element(0, 0); - let s0_1 = first_step.get_evaluation_element(0, 1); - let s1_0 = second_step.get_evaluation_element(0, 0); - let s1_1 = second_step.get_evaluation_element(0, 1); + let s0_0 = first_step.get_main_evaluation_element(0, 0); + let s0_1 = first_step.get_main_evaluation_element(0, 1); + let s1_0 = second_step.get_main_evaluation_element(0, 0); + let s1_1 = second_step.get_main_evaluation_element(0, 1); let first_transition = s1_0 - s0_0 - s0_1; let second_transition = s1_1 - s0_1 - s1_0; @@ -100,8 +100,8 @@ where &self, _rap_challenges: &Self::RAPChallenges, ) -> BoundaryConstraints { - let a0 = BoundaryConstraint::new(0, 0, self.pub_inputs.a0.clone()); - let a1 = BoundaryConstraint::new(1, 0, self.pub_inputs.a1.clone()); + let a0 = BoundaryConstraint::new_main(0, 0, self.pub_inputs.a0.clone()); + let a1 = BoundaryConstraint::new_main(1, 0, self.pub_inputs.a1.clone()); BoundaryConstraints::from_constraints(vec![a0, a1]) } @@ -121,6 +121,15 @@ where fn pub_inputs(&self) -> &Self::PublicInputs { &self.pub_inputs } + + fn compute_transition_verifier( + &self, + frame: &Frame, + periodic_values: &[FieldElement], + rap_challenges: &Self::RAPChallenges, + ) -> Vec> { + self.compute_transition_prover(frame, periodic_values, rap_challenges) + } } pub fn compute_trace( diff --git a/provers/stark/src/examples/fibonacci_rap.rs b/provers/stark/src/examples/fibonacci_rap.rs index c2dbb6738..b960ae97c 100644 --- a/provers/stark/src/examples/fibonacci_rap.rs +++ b/provers/stark/src/examples/fibonacci_rap.rs @@ -107,9 +107,9 @@ where 1 } - fn compute_transition( + fn compute_transition_prover( &self, - frame: &Frame, + frame: &Frame, _periodic_values: &[FieldElement], gamma: &Self::RAPChallenges, ) -> Vec> { @@ -118,18 +118,18 @@ where let second_step = frame.get_evaluation_step(1); let third_step = frame.get_evaluation_step(2); - let a0 = first_step.get_evaluation_element(0, 0); - let a1 = second_step.get_evaluation_element(0, 0); - let a2 = third_step.get_evaluation_element(0, 0); + let a0 = first_step.get_main_evaluation_element(0, 0); + let a1 = second_step.get_main_evaluation_element(0, 0); + let a2 = third_step.get_main_evaluation_element(0, 0); let mut constraints = vec![a2 - a1 - a0]; // Auxiliary constraints - let z_i = first_step.get_evaluation_element(0, 2); - let z_i_plus_one = second_step.get_evaluation_element(0, 2); + let z_i = first_step.get_aux_evaluation_element(0, 0); + let z_i_plus_one = second_step.get_aux_evaluation_element(0, 0); - let a_i = first_step.get_evaluation_element(0, 0); - let b_i = first_step.get_evaluation_element(0, 1); + let a_i = first_step.get_main_evaluation_element(0, 0); + let b_i = first_step.get_main_evaluation_element(0, 1); let eval = z_i_plus_one * (b_i + gamma) - z_i * (a_i + gamma); @@ -142,11 +142,11 @@ where _rap_challenges: &Self::RAPChallenges, ) -> BoundaryConstraints { // Main boundary constraints - let a0 = BoundaryConstraint::new_simple(0, FieldElement::::one()); - let a1 = BoundaryConstraint::new_simple(1, FieldElement::::one()); + let a0 = BoundaryConstraint::new_simple_main(0, FieldElement::::one()); + let a1 = BoundaryConstraint::new_simple_main(1, FieldElement::::one()); // Auxiliary boundary constraints - let a0_aux = BoundaryConstraint::new(2, 0, FieldElement::::one()); + let a0_aux = BoundaryConstraint::new_aux(0, 0, FieldElement::::one()); BoundaryConstraints::from_constraints(vec![a0, a1, a0_aux]) } @@ -166,6 +166,15 @@ where fn pub_inputs(&self) -> &Self::PublicInputs { &self.pub_inputs } + + fn compute_transition_verifier( + &self, + frame: &Frame, + periodic_values: &[FieldElement], + rap_challenges: &Self::RAPChallenges, + ) -> Vec> { + self.compute_transition_prover(frame, periodic_values, rap_challenges) + } } pub fn fibonacci_rap_trace( diff --git a/provers/stark/src/examples/quadratic_air.rs b/provers/stark/src/examples/quadratic_air.rs index 5dff7bd58..ef7c29409 100644 --- a/provers/stark/src/examples/quadratic_air.rs +++ b/provers/stark/src/examples/quadratic_air.rs @@ -73,17 +73,17 @@ where ) -> Self::RAPChallenges { } - fn compute_transition( + fn compute_transition_prover( &self, - frame: &Frame, + frame: &Frame, _periodic_values: &[FieldElement], _rap_challenges: &Self::RAPChallenges, ) -> Vec> { let first_step = frame.get_evaluation_step(0); let second_step = frame.get_evaluation_step(1); - let x = first_step.get_evaluation_element(0, 0); - let x_squared = second_step.get_evaluation_element(0, 0); + let x = first_step.get_main_evaluation_element(0, 0); + let x_squared = second_step.get_main_evaluation_element(0, 0); vec![x_squared - x * x] } @@ -96,7 +96,7 @@ where &self, _rap_challenges: &Self::RAPChallenges, ) -> BoundaryConstraints { - let a0 = BoundaryConstraint::new_simple(0, self.pub_inputs.a0.clone()); + let a0 = BoundaryConstraint::new_simple_main(0, self.pub_inputs.a0.clone()); BoundaryConstraints::from_constraints(vec![a0]) } @@ -116,6 +116,15 @@ where fn pub_inputs(&self) -> &Self::PublicInputs { &self.pub_inputs } + + fn compute_transition_verifier( + &self, + frame: &Frame, + periodic_values: &[FieldElement], + rap_challenges: &Self::RAPChallenges, + ) -> Vec> { + self.compute_transition_prover(frame, periodic_values, rap_challenges) + } } pub fn quadratic_trace( diff --git a/provers/stark/src/examples/simple_fibonacci.rs b/provers/stark/src/examples/simple_fibonacci.rs index eb6bcde6a..b255ee318 100644 --- a/provers/stark/src/examples/simple_fibonacci.rs +++ b/provers/stark/src/examples/simple_fibonacci.rs @@ -78,9 +78,9 @@ where ) -> Self::RAPChallenges { } - fn compute_transition( + fn compute_transition_prover( &self, - frame: &Frame, + frame: &Frame, _periodic_values: &[FieldElement], _rap_challenges: &Self::RAPChallenges, ) -> Vec> { @@ -88,9 +88,9 @@ where let second_step = frame.get_evaluation_step(1); let third_step = frame.get_evaluation_step(2); - let a0 = first_step.get_evaluation_element(0, 0); - let a1 = second_step.get_evaluation_element(0, 0); - let a2 = third_step.get_evaluation_element(0, 0); + let a0 = first_step.get_main_evaluation_element(0, 0); + let a1 = second_step.get_main_evaluation_element(0, 0); + let a2 = third_step.get_main_evaluation_element(0, 0); vec![a2 - a1 - a0] } @@ -99,8 +99,8 @@ where &self, _rap_challenges: &Self::RAPChallenges, ) -> BoundaryConstraints { - let a0 = BoundaryConstraint::new_simple(0, self.pub_inputs.a0.clone()); - let a1 = BoundaryConstraint::new_simple(1, self.pub_inputs.a1.clone()); + let a0 = BoundaryConstraint::new_simple_main(0, self.pub_inputs.a0.clone()); + let a1 = BoundaryConstraint::new_simple_main(1, self.pub_inputs.a1.clone()); BoundaryConstraints::from_constraints(vec![a0, a1]) } @@ -120,6 +120,15 @@ where fn pub_inputs(&self) -> &Self::PublicInputs { &self.pub_inputs } + + fn compute_transition_verifier( + &self, + frame: &Frame, + periodic_values: &[FieldElement], + rap_challenges: &Self::RAPChallenges, + ) -> Vec> { + self.compute_transition_prover(frame, periodic_values, rap_challenges) + } } pub fn fibonacci_trace( diff --git a/provers/stark/src/examples/simple_periodic_cols.rs b/provers/stark/src/examples/simple_periodic_cols.rs index 5db81a6f1..3ca7b68b2 100644 --- a/provers/stark/src/examples/simple_periodic_cols.rs +++ b/provers/stark/src/examples/simple_periodic_cols.rs @@ -92,9 +92,9 @@ where ) -> Self::RAPChallenges { } - fn compute_transition( + fn compute_transition_prover( &self, - frame: &Frame, + frame: &Frame, periodic_values: &[FieldElement], _rap_challenges: &Self::RAPChallenges, ) -> Vec> { @@ -102,9 +102,9 @@ where let second_step = frame.get_evaluation_step(1); let third_step = frame.get_evaluation_step(2); - let a0 = first_step.get_evaluation_element(0, 0); - let a1 = second_step.get_evaluation_element(0, 0); - let a2 = third_step.get_evaluation_element(0, 0); + let a0 = first_step.get_main_evaluation_element(0, 0); + let a1 = second_step.get_main_evaluation_element(0, 0); + let a2 = third_step.get_main_evaluation_element(0, 0); let s = &periodic_values[0]; @@ -115,9 +115,11 @@ where &self, _rap_challenges: &Self::RAPChallenges, ) -> BoundaryConstraints { - let a0 = BoundaryConstraint::new_simple(0, self.pub_inputs.a0.clone()); - let a1 = - BoundaryConstraint::new_simple(self.trace_length() - 1, self.pub_inputs.a1.clone()); + let a0 = BoundaryConstraint::new_simple_main(0, self.pub_inputs.a0.clone()); + let a1 = BoundaryConstraint::new_simple_main( + self.trace_length() - 1, + self.pub_inputs.a1.clone(), + ); BoundaryConstraints::from_constraints(vec![a0, a1]) } @@ -141,6 +143,15 @@ where fn pub_inputs(&self) -> &Self::PublicInputs { &self.pub_inputs } + + fn compute_transition_verifier( + &self, + frame: &Frame, + periodic_values: &[FieldElement], + rap_challenges: &Self::RAPChallenges, + ) -> Vec> { + self.compute_transition_prover(frame, periodic_values, rap_challenges) + } } pub fn simple_periodic_trace(trace_length: usize) -> TraceTable { diff --git a/provers/stark/src/frame.rs b/provers/stark/src/frame.rs index cca79d044..51d24e395 100644 --- a/provers/stark/src/frame.rs +++ b/provers/stark/src/frame.rs @@ -1,41 +1,50 @@ -use super::trace::TraceTable; -use crate::trace::StepView; -use lambdaworks_math::field::traits::IsField; +use crate::{table::EvaluationTable, trace::StepView}; +use lambdaworks_math::field::traits::{IsField, IsSubFieldOf}; /// A frame represents a collection of trace steps. /// The collected steps are all the necessary steps for /// all transition costraints over a trace to be evaluated. #[derive(Clone, Debug, PartialEq)] -pub struct Frame<'t, F: IsField> { - steps: Vec>, +pub struct Frame<'t, F: IsSubFieldOf, E: IsField> { + steps: Vec>, } -impl<'t, F: IsField> Frame<'t, F> { - pub fn new(steps: Vec>) -> Self { +impl<'t, F: IsSubFieldOf, E: IsField> Frame<'t, F, E> { + pub fn new(steps: Vec>) -> Self { Self { steps } } - pub fn get_evaluation_step(&self, step: usize) -> &StepView { + pub fn get_evaluation_step(&self, step: usize) -> &StepView { &self.steps[step] } - pub fn read_from_trace( - trace: &'t TraceTable, + pub fn read_from_lde_table( + lde_table: &'t EvaluationTable, step: usize, blowup: u8, offsets: &[usize], ) -> Self { // Get trace length to apply module with it when getting elements of // the frame from the trace. - let trace_steps = trace.num_steps(); + let trace_steps = lde_table.num_steps(); let steps = offsets .iter() .map(|eval_offset| { - trace.step_view((step + (eval_offset * blowup as usize)) % trace_steps) + lde_table.step_view((step + (eval_offset * blowup as usize)) % trace_steps) }) .collect(); Self::new(steps) } } + +impl<'t, E: IsField> Frame<'t, E, E> { + pub fn read_from_ood_table(ood_table: &'t EvaluationTable, offsets: &[usize]) -> Self { + let steps: Vec<_> = offsets + .iter() + .map(|offset| ood_table.step_view(*offset)) + .collect(); + Self::new(steps) + } +} diff --git a/provers/stark/src/proof/stark.rs b/provers/stark/src/proof/stark.rs index cabb19323..893643537 100644 --- a/provers/stark/src/proof/stark.rs +++ b/provers/stark/src/proof/stark.rs @@ -14,7 +14,7 @@ use crate::{ config::Commitment, domain::Domain, fri::fri_decommit::FriDecommitment, - table::Table, + table::EvaluationTable, traits::AIR, transcript::StoneProverTranscript, verifier::{IsStarkVerifier, Verifier}, @@ -50,7 +50,7 @@ pub struct StarkProof, E: IsField> { // [tⱼ] pub lde_trace_aux_merkle_root: Option, // tⱼ(zgᵏ) - pub trace_ood_evaluations: Table, + pub trace_ood_evaluations: EvaluationTable, // Commitments to Hᵢ pub composition_poly_root: Commitment, // Hᵢ(z^N) @@ -131,9 +131,10 @@ impl StoneCompatibleSerializer { proof: &StarkProof, output: &mut Vec, ) { - for i in 0..proof.trace_ood_evaluations.width { - for j in 0..proof.trace_ood_evaluations.height { - output.extend_from_slice(&proof.trace_ood_evaluations.get_row(j)[i].serialize()); + for i in 0..proof.trace_ood_evaluations.n_cols() { + for j in 0..proof.trace_ood_evaluations.n_rows() { + output + .extend_from_slice(&proof.trace_ood_evaluations.get_row_main(j)[i].serialize()); } } diff --git a/provers/stark/src/prover.rs b/provers/stark/src/prover.rs index 7c68c01f7..77ee87d0f 100644 --- a/provers/stark/src/prover.rs +++ b/provers/stark/src/prover.rs @@ -20,7 +20,7 @@ use rayon::prelude::{IndexedParallelIterator, IntoParallelRefIterator, ParallelI use crate::debug::validate_trace; use crate::fri; use crate::proof::stark::{DeepPolynomialOpenings, PolynomialOpenings}; -use crate::table::Table; +use crate::table::{EvaluationTable, Table}; use crate::transcript::IsStarkTranscript; use super::config::{BatchedMerkleTree, Commitment}; @@ -50,7 +50,6 @@ where FieldElement: Serializable + Send + Sync, { pub(crate) trace_polys: Vec>>, - pub(crate) lde_trace: TraceTable, pub(crate) lde_trace_merkle_tree: BatchedMerkleTree, pub(crate) lde_trace_merkle_root: Commitment, } @@ -61,6 +60,7 @@ where FieldElement: Serializable + Sync + Send, FieldElement: Serializable + Sync + Send, { + pub(crate) lde_table: EvaluationTable, pub(crate) main: Round1CommitmentData, pub(crate) aux: Option>, pub(crate) rap_challenges: A::RAPChallenges, @@ -86,23 +86,6 @@ where } trace_polys } - - fn all_evaluations(&self) -> TraceTable { - let mut evaluations: Vec>> = self - .main - .lde_trace - .columns() - .clone() - .into_iter() - .map(|col| col.into_iter().map(|x| x.to_extension()).collect()) - .collect(); - - if let Some(aux) = &self.aux { - evaluations.extend_from_slice(&aux.lde_trace.columns()) - } - - TraceTable::from_columns(evaluations, A::STEP_SIZE) - } } pub struct Round2 where @@ -116,7 +99,7 @@ where } pub struct Round3 { - trace_ood_evaluations: Vec>>, + trace_ood_evaluations: EvaluationTable, composition_poly_parts_ood_evaluation: Vec>, } @@ -246,7 +229,6 @@ pub trait IsStarkProver { let main = Round1CommitmentData:: { trace_polys, - lde_trace: TraceTable::from_columns(evaluations, A::STEP_SIZE), lde_trace_merkle_tree: main_merkle_tree, lde_trace_merkle_root: main_merkle_root, }; @@ -254,21 +236,23 @@ pub trait IsStarkProver { let rap_challenges = air.build_rap_challenges(transcript); let aux_trace = air.build_auxiliary_trace(main_trace, &rap_challenges); - let aux = if !aux_trace.is_empty() { - // Check that this is valid for interpolation + let (aux, aux_evaluations) = if !aux_trace.is_empty() { let (aux_trace_polys, aux_trace_polys_evaluations, aux_merkle_tree, aux_merkle_root) = Self::interpolate_and_commit(&aux_trace, domain, transcript); - Some(Round1CommitmentData:: { + let aux_evaluations = aux_trace_polys_evaluations; + let aux = Some(Round1CommitmentData:: { trace_polys: aux_trace_polys, - lde_trace: TraceTable::from_columns(aux_trace_polys_evaluations, A::STEP_SIZE), lde_trace_merkle_tree: aux_merkle_tree, lde_trace_merkle_root: aux_merkle_root, - }) + }); + (aux, aux_evaluations) } else { - None + (None, Vec::new()) }; + let lde_table = EvaluationTable::from_columns(evaluations, aux_evaluations, A::STEP_SIZE); Ok(Round1 { + lde_table, main, aux, rap_challenges, @@ -317,19 +301,18 @@ pub trait IsStarkProver { FieldElement: Serializable + Send + Sync, FieldElement: Serializable + Send + Sync, { - // Create evaluation table + // Compute the evaluations of the composition polynomial on the LDE domain. let evaluator = ConstraintEvaluator::new(air, &round_1_result.rap_challenges); - let constraint_evaluations = evaluator.evaluate( air, - &round_1_result.all_evaluations(), + &round_1_result.lde_table, domain, transition_coefficients, boundary_coefficients, &round_1_result.rap_challenges, ); - // Get the composition poly H + // Get coefficients of the composition poly H let composition_poly = Polynomial::interpolate_offset_fft(&constraint_evaluations, &domain.coset_offset) .unwrap(); @@ -391,10 +374,16 @@ pub trait IsStarkProver { // polynomial and `g` is the primitive root of unity used when interpolating `t`. let trace_ood_evaluations = crate::trace::get_trace_evaluations( - &round_1_result.all_trace_polys(), + &round_1_result.main.trace_polys, + round_1_result + .aux + .as_ref() + .map(|aux| &aux.trace_polys) + .unwrap_or(&vec![]), z, &air.context().transition_offsets, &domain.trace_primitive_root, + A::STEP_SIZE, ); Round3 { @@ -542,7 +531,7 @@ pub trait IsStarkProver { // ∑ ⱼₖ [ 𝛾ₖ ( tⱼ − tⱼ(z) ) / ( X − zgᵏ )] // @@@ this could be const - let trace_frame_length = trace_frame_evaluations.len(); + let trace_frame_length = trace_frame_evaluations.n_rows(); #[cfg(feature = "parallel")] let trace_terms = trace_polys @@ -556,7 +545,7 @@ pub trait IsStarkProver { (i, t_j), trace_frame_length, trace_terms_gammas, - trace_frame_evaluations, + &trace_frame_evaluations.columns(), transition_offsets, (z, primitive_root), ) @@ -575,7 +564,7 @@ pub trait IsStarkProver { (i, t_j), trace_frame_length, trace_terms_gammas, - trace_frame_evaluations, + &trace_frame_evaluations.columns(), transition_offsets, (z, primitive_root), ) @@ -601,15 +590,13 @@ pub trait IsStarkProver { let iter_trace_gammas = trace_terms_gammas .iter() .skip(i_times_trace_frame_evaluation); - let trace_int = trace_frame_evaluations + let trace_int = trace_frame_evaluations[i] .iter() .zip(transition_offsets) .zip(iter_trace_gammas) .fold( Polynomial::zero(), - |trace_agg, ((eval, offset), trace_gamma)| { - // @@@ we can avoid this clone - let t_j_z = &eval[i]; + |trace_agg, ((t_j_z, offset), trace_gamma)| { // @@@ this can be pre-computed let z_shifted = primitive_root.pow(*offset) * z; let mut poly = t_j - t_j_z; @@ -663,7 +650,7 @@ pub trait IsStarkProver { fn open_trace_polys( domain: &Domain, tree: &BatchedMerkleTree, - lde_trace: &TraceTable, + lde_trace: &Table, challenge: usize, ) -> PolynomialOpenings where @@ -706,7 +693,7 @@ pub trait IsStarkProver { let main_trace_opening = Self::open_trace_polys::( domain, &round_1_result.main.lde_trace_merkle_tree, - &round_1_result.main.lde_trace, + &round_1_result.lde_table.main_table, *index, ); @@ -720,7 +707,7 @@ pub trait IsStarkProver { Self::open_trace_polys::( domain, &aux.lde_trace_merkle_tree, - &aux.lde_trace, + &round_1_result.lde_table.aux_table, *index, ) }); @@ -781,7 +768,12 @@ pub trait IsStarkProver { #[cfg(debug_assertions)] validate_trace( &air, - &round_1_result.all_trace_polys(), + &round_1_result.main.trace_polys, + round_1_result + .aux + .as_ref() + .map(|a| &a.trace_polys) + .unwrap_or(&vec![]), &domain, &round_1_result.rap_challenges, ); @@ -858,9 +850,10 @@ pub trait IsStarkProver { ); // >>>> Send values: tⱼ(zgᵏ) - for i in 0..round_3_result.trace_ood_evaluations[0].len() { - for j in 0..round_3_result.trace_ood_evaluations.len() { - transcript.append_field_element(&round_3_result.trace_ood_evaluations[j][i]); + let trace_ood_evaluations_columns = round_3_result.trace_ood_evaluations.columns(); + for col in trace_ood_evaluations_columns.iter() { + for elem in col.iter() { + transcript.append_field_element(elem); } } @@ -916,22 +909,13 @@ pub trait IsStarkProver { info!("End proof generation"); - let trace_ood_evaluations = Table::new( - round_3_result - .trace_ood_evaluations - .into_iter() - .flatten() - .collect(), - air.context().trace_columns, - ); - Ok(StarkProof:: { // [tⱼ] lde_trace_main_merkle_root: round_1_result.main.lde_trace_merkle_root, // [tⱼ] lde_trace_aux_merkle_root: round_1_result.aux.map(|x| x.lde_trace_merkle_root), // tⱼ(zgᵏ) - trace_ood_evaluations, + trace_ood_evaluations: round_3_result.trace_ood_evaluations, // [H₁] and [H₂] composition_poly_root: round_2_result.composition_poly_root, // Hᵢ(z^N) @@ -1193,25 +1177,25 @@ mod tests { let proof = stone_compatibility_case_1_proof(); assert_eq!( - proof.trace_ood_evaluations.get_row(0)[0], + proof.trace_ood_evaluations.get_row_main(0)[0], FieldElement::from_hex_unchecked( "70d8181785336cc7e0a0a1078a79ee6541ca0803ed3ff716de5a13c41684037", ) ); assert_eq!( - proof.trace_ood_evaluations.get_row(1)[0], + proof.trace_ood_evaluations.get_row_main(1)[0], FieldElement::from_hex_unchecked( "29808fc8b7480a69295e4b61600480ae574ca55f8d118100940501b789c1630", ) ); assert_eq!( - proof.trace_ood_evaluations.get_row(0)[1], + proof.trace_ood_evaluations.get_row_main(0)[1], FieldElement::from_hex_unchecked( "7d8110f21d1543324cc5e472ab82037eaad785707f8cae3d64c5b9034f0abd2", ) ); assert_eq!( - proof.trace_ood_evaluations.get_row(1)[1], + proof.trace_ood_evaluations.get_row_main(1)[1], FieldElement::from_hex_unchecked( "1b58470130218c122f71399bf1e04cf75a6e8556c4751629d5ce8c02cc4e62d", ) diff --git a/provers/stark/src/table.rs b/provers/stark/src/table.rs index ab9a102bc..87d3febc0 100644 --- a/provers/stark/src/table.rs +++ b/provers/stark/src/table.rs @@ -1,6 +1,9 @@ -use lambdaworks_math::field::{element::FieldElement, traits::IsField}; +use lambdaworks_math::field::{ + element::FieldElement, + traits::{IsField, IsSubFieldOf}, +}; -use crate::{frame::Frame, trace::StepView}; +use crate::trace::StepView; /// A two-dimensional Table holding field elements, arranged in a row-major order. /// This is the basic underlying data structure used for any two-dimensional component in the @@ -14,6 +17,25 @@ pub struct Table { pub height: usize, } +/// A view of a contiguos subset of rows of a table. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct TableView<'t, F: IsField> { + pub data: &'t [FieldElement], + pub table_row_idx: usize, + pub width: usize, + pub height: usize, +} + +/// A pair of tables corresponding to evaluations of the main and auxiliary traces. +/// It supports main and auxiliary tables taking values in different fields. +/// Both tables must have the same number of rows. +#[derive(Clone, Default, Debug, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct EvaluationTable, E: IsField> { + pub(crate) main_table: Table, + pub(crate) aux_table: Table, + pub(crate) step_size: usize, +} + impl<'t, F: IsField> Table { /// Crates a new Table instance from a one-dimensional array in row major order /// and the intended width of the table. @@ -122,30 +144,117 @@ impl<'t, F: IsField> Table { let idx = row * self.width + col; &self.data[idx] } +} - /// Given a step size, converts the given table into a `Frame`. - pub fn into_frame(&'t self, step_size: usize) -> Frame<'t, F> { - debug_assert!(self.height % step_size == 0); - let steps = (0..self.height) - .step_by(step_size) - .enumerate() - .map(|(step_idx, row_idx)| { - let table_view = self.table_view(row_idx, step_size); - StepView::new(table_view, step_idx) - }) - .collect(); +impl EvaluationTable { + /// Returns a single vector of elements with the concatenation of the corresponding rows + /// in the main and auxiliary tables. + pub fn get_row(&self, row_idx: usize) -> Vec> { + let mut row: Vec<_> = self.get_row_main(row_idx).to_vec(); + row.extend_from_slice(self.get_row_aux(row_idx)); + row + } - Frame::new(steps) + /// Returns the values of the tables as a single list of columns containing both main and + /// auxiliary tables. The first `self.n_main_cols()` are the columns of the main trace and the + /// rest are the auxiliary table columns. + pub fn columns(&self) -> Vec>> { + let mut columns = self.main_table.columns(); + let aux_columns = self.aux_table.columns(); + columns.extend(aux_columns); + columns } } -/// A view of a contiguos subset of rows of a table. -#[derive(Clone, Debug, PartialEq, Eq)] -pub struct TableView<'t, F: IsField> { - pub data: &'t [FieldElement], - pub table_row_idx: usize, - pub width: usize, - pub height: usize, +impl, E: IsField> EvaluationTable { + /// Creates an EvaluationTable instance from a vector of columns. + pub fn from_columns( + main_columns: Vec>>, + aux_columns: Vec>>, + step_size: usize, + ) -> Self { + let main_table = Table::from_columns(main_columns); + let aux_table = Table::from_columns(aux_columns); + debug_assert!(aux_table.height == 0 || (main_table.height == aux_table.height)); + Self { + main_table, + aux_table, + step_size, + } + } + + /// Returns the number of columns of the main table. + pub fn n_main_cols(&self) -> usize { + self.main_table.width + } + + /// Returns the number of columns of the auxiliary table. + pub fn n_aux_cols(&self) -> usize { + self.aux_table.width + } + + /// Returns the total number of columns in both tables. + pub fn n_cols(&self) -> usize { + self.n_main_cols() + self.n_aux_cols() + } + + /// Returns the total number of rows. + pub fn n_rows(&self) -> usize { + debug_assert!( + self.aux_table.height == 0 || (self.main_table.height == self.aux_table.height) + ); + self.main_table.height + } + + /// Returns the total number of steps. + pub fn num_steps(&self) -> usize { + debug_assert!((self.main_table.height % self.step_size) == 0); + debug_assert!( + self.aux_table.height == 0 || (self.main_table.height == self.aux_table.height) + ); + self.main_table.height / self.step_size + } + + /// Given a particular step of the computation represented on the trace, + /// returns the row of the underlying table. + pub fn step_to_row(&self, step: usize) -> usize { + self.step_size * step + } + + /// Given a step index, return the step view of the trace for that index + pub fn step_view(&self, step_idx: usize) -> StepView<'_, F, E> { + let row_idx = self.step_to_row(step_idx); + let main_table_view = self.main_table.table_view(row_idx, self.step_size); + let aux_table_view = self.aux_table.table_view(row_idx, self.step_size); + + StepView { + main_table_view, + aux_table_view, + step_idx, + } + } + + /// Given a row and a column index, gives stored value in that position + pub fn get_main(&self, row: usize, col: usize) -> &FieldElement { + self.main_table.get(row, col) + } + + /// Given a row and a column index, gives stored value in that position + pub fn get_aux(&self, row: usize, col: usize) -> &FieldElement { + self.aux_table.get(row, col) + } + + /// Given a row index, returns a reference to that row in the main table as a slice of field elements. + pub fn get_row_main(&self, row_idx: usize) -> &[FieldElement] { + let row_offset = row_idx * self.main_table.width; + &self.main_table.data[row_offset..row_offset + self.main_table.width] + } + + /// Given a row index, returns a reference to that row in the aux table as a slice of field elements. + pub fn get_row_aux(&self, row_idx: usize) -> &[FieldElement] { + let row_offset = row_idx * self.aux_table.width; + &self.aux_table.data[row_offset..row_offset + self.aux_table.width] + } } impl<'t, F: IsField> TableView<'t, F> { diff --git a/provers/stark/src/trace.rs b/provers/stark/src/trace.rs index a3cabafd0..e7ef297de 100644 --- a/provers/stark/src/trace.rs +++ b/provers/stark/src/trace.rs @@ -1,4 +1,4 @@ -use crate::table::{Table, TableView}; +use crate::table::{EvaluationTable, Table, TableView}; use lambdaworks_math::fft::errors::FFTError; use lambdaworks_math::field::traits::{IsField, IsSubFieldOf}; use lambdaworks_math::{ @@ -21,7 +21,7 @@ pub struct TraceTable { pub step_size: usize, } -impl<'t, F: IsField> TraceTable { +impl TraceTable { pub fn new(data: Vec>, n_columns: usize, step_size: usize) -> Self { let table = Table::new(data, n_columns); Self { table, step_size } @@ -55,17 +55,6 @@ impl<'t, F: IsField> TraceTable { self.step_size * step } - /// Given a step index, return the step view of the trace for that index - pub fn step_view(&'t self, step_idx: usize) -> StepView<'t, F> { - let row_idx = self.step_to_row(step_idx); - let table_view = self.table.table_view(row_idx, self.step_size); - - StepView { - table_view, - step_idx, - } - } - pub fn n_cols(&self) -> usize { self.table.width } @@ -106,11 +95,6 @@ impl<'t, F: IsField> TraceTable { data } - /// Given a row and a column index, gives stored value in that position - pub fn get(&self, row: usize, col: usize) -> &FieldElement { - self.table.get(row, col) - } - pub fn compute_trace_polys>( &self, ) -> Vec>> @@ -170,26 +154,41 @@ impl<'t, F: IsField> TraceTable { /// access the steps in a trace, in order to grab elements to calculate /// constraint evaluations. #[derive(Debug, Clone, PartialEq)] -pub struct StepView<'t, F: IsField> { - pub table_view: TableView<'t, F>, +pub struct StepView<'t, F: IsSubFieldOf, E: IsField> { + pub main_table_view: TableView<'t, F>, + pub aux_table_view: TableView<'t, E>, pub step_idx: usize, } -impl<'t, F: IsField> StepView<'t, F> { - pub fn new(table_view: TableView<'t, F>, step_idx: usize) -> Self { +impl<'t, F: IsSubFieldOf, E: IsField> StepView<'t, F, E> { + pub fn new( + main_table_view: TableView<'t, F>, + aux_table_view: TableView<'t, E>, + step_idx: usize, + ) -> Self { StepView { - table_view, + main_table_view, + aux_table_view, step_idx, } } - /// Gets the evaluation element specified by `row_idx` and `col_idx` of this step - pub fn get_evaluation_element(&self, row_idx: usize, col_idx: usize) -> &FieldElement { - self.table_view.get(row_idx, col_idx) + /// Gets the evaluation element of the main table specified by `row_idx` and `col_idx` of this step + pub fn get_main_evaluation_element(&self, row_idx: usize, col_idx: usize) -> &FieldElement { + self.main_table_view.get(row_idx, col_idx) } - pub fn get_row(&self, row_idx: usize) -> &[FieldElement] { - self.table_view.get_row(row_idx) + /// Gets the evaluation element of the aux table specified by `row_idx` and `col_idx` of this step + pub fn get_aux_evaluation_element(&self, row_idx: usize, col_idx: usize) -> &FieldElement { + self.aux_table_view.get(row_idx, col_idx) + } + + pub fn get_row_main(&self, row_idx: usize) -> &[FieldElement] { + self.main_table_view.get_row(row_idx) + } + + pub fn get_row_aux(&self, row_idx: usize) -> &[FieldElement] { + self.aux_table_view.get_row(row_idx) } } @@ -199,22 +198,38 @@ impl<'t, F: IsField> StepView<'t, F> { /// compute a transition. /// Example: For a simple Fibonacci computation, if t(x) is the trace polynomial of /// the computation, this will output evaluations t(x), t(g * x), t(g^2 * z). -pub fn get_trace_evaluations>( - trace_polys: &[Polynomial>], +pub(crate) fn get_trace_evaluations, E: IsField>( + main_trace_polys: &[Polynomial>], + aux_trace_polys: &[Polynomial>], x: &FieldElement, frame_offsets: &[usize], primitive_root: &FieldElement, -) -> Vec>> { - frame_offsets + step_size: usize, +) -> EvaluationTable { + let evaluation_points: Vec<_> = frame_offsets .iter() .map(|offset| primitive_root.pow(*offset) * x) - .map(|eval_point| { - trace_polys + .collect(); + let main_evaluations = main_trace_polys + .iter() + .map(|poly| { + evaluation_points .iter() - .map(|poly| poly.evaluate(&eval_point)) - .collect::>>() + .map(|eval_point| poly.evaluate(eval_point)) + .collect() }) - .collect() + .collect(); + let aux_evaluations = aux_trace_polys + .iter() + .map(|poly| { + evaluation_points + .iter() + .map(|eval_point| poly.evaluate(eval_point)) + .collect() + }) + .collect(); + + EvaluationTable::from_columns(main_evaluations, aux_evaluations, step_size) } #[cfg(test)] diff --git a/provers/stark/src/traits.rs b/provers/stark/src/traits.rs index 7099dd926..82efa6409 100644 --- a/provers/stark/src/traits.rs +++ b/provers/stark/src/traits.rs @@ -45,9 +45,25 @@ pub trait AIR { fn composition_poly_degree_bound(&self) -> usize; - fn compute_transition( + /// The method called by the prover to evaluate the transitions corresponding to an evaluation frame. + /// In the case of the prover, the main evaluation table of the frame takes values in + /// `Self::Field`, since they are the evaluations of the main trace at the LDE domain. + fn compute_transition_prover( &self, - frame: &Frame, + frame: &Frame, + periodic_values: &[FieldElement], + rap_challenges: &Self::RAPChallenges, + ) -> Vec>; + + /// The method called by the verifier to evaluate the transitions at the out of domain frame. + /// In the case of the verifier, both main and auxiliary tables of the evaluation frame take + /// values in `Self::FieldExtension`, since they are the evaluations of the trace polynomials + /// at the out of domain challenge. + /// In case `Self::Field` coincides with `Self::FieldExtension`, this method and + /// `compute_transition_prover` should return the same values. + fn compute_transition_verifier( + &self, + frame: &Frame, periodic_values: &[FieldElement], rap_challenges: &Self::RAPChallenges, ) -> Vec>; @@ -133,9 +149,7 @@ pub trait AIR { vec![] } - fn get_periodic_column_polynomials( - &self, - ) -> Vec>> { + fn get_periodic_column_polynomials(&self) -> Vec>> { let mut result = Vec::new(); for periodic_column in self.get_periodic_column_values() { let values: Vec<_> = periodic_column @@ -143,9 +157,10 @@ pub trait AIR { .cycle() .take(self.trace_length()) .cloned() - .map(|x| x.to_extension()) .collect(); - let poly = Polynomial::interpolate_fft::(&values).unwrap(); + let poly = + Polynomial::>::interpolate_fft::(&values) + .unwrap(); result.push(poly); } result diff --git a/provers/stark/src/verifier.rs b/provers/stark/src/verifier.rs index 7be6148ad..675566452 100644 --- a/provers/stark/src/verifier.rs +++ b/provers/stark/src/verifier.rs @@ -8,7 +8,8 @@ use lambdaworks_crypto::merkle_tree::proof::Proof; use log::error; use crate::{ - config::Commitment, proof::stark::DeepPolynomialOpening, transcript::IsStarkTranscript, + config::Commitment, frame::Frame, proof::stark::DeepPolynomialOpening, + transcript::IsStarkTranscript, }; use lambdaworks_math::{ fft::cpu::bit_reversing::reverse_index, @@ -118,9 +119,10 @@ pub trait IsStarkVerifier { ); // <<<< Receive values: tⱼ(zgᵏ) - for i in 0..proof.trace_ood_evaluations.width { - for j in 0..proof.trace_ood_evaluations.height { - transcript.append_field_element(&proof.trace_ood_evaluations.get_row(j)[i]); + let trace_ood_evaluations_columns = proof.trace_ood_evaluations.columns(); + for col in trace_ood_evaluations_columns.iter() { + for elem in col.iter() { + transcript.append_field_element(elem); } } // <<<< Receive value: Hᵢ(z^N) @@ -217,9 +219,14 @@ pub trait IsStarkVerifier { ) = (0..number_of_b_constraints) .map(|index| { let step = boundary_constraints.constraints[index].step; + let is_aux = boundary_constraints.constraints[index].is_aux; let point = &domain.trace_primitive_root.pow(step as u64); let trace_idx = boundary_constraints.constraints[index].col; - let trace_evaluation = &proof.trace_ood_evaluations.get_row(0)[trace_idx]; + let trace_evaluation = if is_aux { + &proof.trace_ood_evaluations.get_row_aux(0)[trace_idx] + } else { + &proof.trace_ood_evaluations.get_row_main(0)[trace_idx] + }; let boundary_zerofier_challenges_z_den = -point + &challenges.z; let boundary_quotient_ood_evaluation_num = @@ -250,8 +257,11 @@ pub trait IsStarkVerifier { .map(|poly| poly.evaluate(&challenges.z)) .collect::>>(); - let transition_ood_frame_evaluations = air.compute_transition( - &(proof.trace_ood_evaluations).into_frame(A::STEP_SIZE), + let transition_ood_frame_evaluations = air.compute_transition_verifier( + &Frame::read_from_ood_table( + &proof.trace_ood_evaluations, + &air.context().transition_offsets, + ), &periodic_values, &challenges.rap_challenges, ); @@ -642,23 +652,22 @@ pub trait IsStarkVerifier { lde_trace_evaluations: &[FieldElement], lde_composition_poly_parts_evaluation: &[FieldElement], ) -> FieldElement { - let mut denoms_trace = (0..proof.trace_ood_evaluations.height) + let mut denoms_trace = (0..proof.trace_ood_evaluations.n_rows()) .map(|row_idx| evaluation_point - primitive_root.pow(row_idx as u64) * &challenges.z) .collect::>>(); FieldElement::inplace_batch_inverse(&mut denoms_trace).unwrap(); - let trace_term = (0..proof.trace_ood_evaluations.width) + let trace_term = (0..proof.trace_ood_evaluations.n_cols()) .zip(&challenges.trace_term_coeffs) .fold(FieldElement::zero(), |trace_terms, (col_idx, coeff_row)| { - let trace_i = (0..proof.trace_ood_evaluations.height).zip(coeff_row).fold( - FieldElement::zero(), - |trace_t, (row_idx, coeff)| { + let trace_i = (0..proof.trace_ood_evaluations.n_rows()) + .zip(coeff_row) + .fold(FieldElement::zero(), |trace_t, (row_idx, coeff)| { let poly_evaluation = (lde_trace_evaluations[col_idx].clone() - proof.trace_ood_evaluations.get_row(row_idx)[col_idx].clone()) * &denoms_trace[row_idx]; trace_t + &poly_evaluation * coeff - }, - ); + }); trace_terms + trace_i }); diff --git a/winterfell_adapter/src/adapter/air.rs b/winterfell_adapter/src/adapter/air.rs index d539ed84d..256deedf8 100644 --- a/winterfell_adapter/src/adapter/air.rs +++ b/winterfell_adapter/src/adapter/air.rs @@ -190,26 +190,23 @@ where * self.trace_length() } - fn compute_transition( + fn compute_transition_prover( &self, - frame: &stark_platinum_prover::frame::Frame, - periodic_values: &[FieldElement], + frame: &stark_platinum_prover::frame::Frame, + periodic_values: &[FieldElement], rap_challenges: &Self::RAPChallenges, ) -> Vec> { - let num_aux_columns = self.number_auxiliary_rap_columns(); - let num_main_columns = self.context().trace_columns - num_aux_columns; - let first_step = frame.get_evaluation_step(0); let second_step = frame.get_evaluation_step(1); let main_frame = EvaluationFrame::from_rows( - vec_lambda2winter(&first_step.get_row(0)[..num_main_columns]), - vec_lambda2winter(&second_step.get_row(0)[..num_main_columns]), + vec_lambda2winter(first_step.get_row_main(0)), + vec_lambda2winter(second_step.get_row_main(0)), ); let periodic_values = vec_lambda2winter(periodic_values); - let mut main_result = vec![ + let main_result = vec![ FieldElement::zero(); self.winterfell_air .context() @@ -217,13 +214,16 @@ where ]; let mut main_result_winter = vec_lambda2winter(&main_result); - self.winterfell_air.evaluate_transition::( + self.winterfell_air.evaluate_transition::( &main_frame, &periodic_values, &mut main_result_winter, - ); // Periodic values not supported + ); - main_result = vec_winter2lambda(&main_result_winter); + let mut result: Vec<_> = vec_winter2lambda(&main_result_winter) + .into_iter() + .map(|element| element.to_extension()) + .collect(); if self.winterfell_air.trace_layout().num_aux_segments() == 1 { let mut rand_elements = AuxTraceRandElements::new(); @@ -233,8 +233,8 @@ where let second_step = frame.get_evaluation_step(1); let aux_frame = EvaluationFrame::from_rows( - vec_lambda2winter(&first_step.get_row(0)[num_main_columns..]), - vec_lambda2winter(&second_step.get_row(0)[num_main_columns..]), + vec_lambda2winter(first_step.get_row_aux(0)), + vec_lambda2winter(second_step.get_row_aux(0)), ); let mut aux_result = vec![ @@ -252,22 +252,19 @@ where &mut winter_aux_result, ); aux_result = vec_winter2lambda(&winter_aux_result); - main_result.extend_from_slice(&aux_result); + result.extend_from_slice(&aux_result); } - main_result + result } fn boundary_constraints( &self, rap_challenges: &Self::RAPChallenges, ) -> stark_platinum_prover::constraints::boundary::BoundaryConstraints { - let num_aux_columns = self.number_auxiliary_rap_columns(); - let num_main_columns = self.context().trace_columns - num_aux_columns; - let mut result = Vec::new(); for assertion in self.winterfell_air.get_assertions() { assert!(assertion.is_single()); - result.push(BoundaryConstraint::::new( + result.push(BoundaryConstraint::new_main( assertion.column(), assertion.first_step(), FieldElement::::const_from_raw(assertion.values()[0]).to_extension(), @@ -279,8 +276,8 @@ where for assertion in self.winterfell_air.get_aux_assertions(&rand_elements) { assert!(assertion.is_single()); - result.push(BoundaryConstraint::new( - assertion.column() + num_main_columns, + result.push(BoundaryConstraint::new_aux( + assertion.column(), assertion.first_step(), FieldElement::::const_from_raw(assertion.values()[0]), )); @@ -304,4 +301,68 @@ where fn get_periodic_column_values(&self) -> Vec>> { matrix_winter2lambda(&self.winterfell_air.get_periodic_column_values()) } + + fn compute_transition_verifier( + &self, + frame: &stark_platinum_prover::frame::Frame, + periodic_values: &[FieldElement], + rap_challenges: &Self::RAPChallenges, + ) -> Vec> { + let first_step = frame.get_evaluation_step(0); + let second_step = frame.get_evaluation_step(1); + + let main_frame = EvaluationFrame::from_rows( + vec_lambda2winter(first_step.get_row_main(0)), + vec_lambda2winter(second_step.get_row_main(0)), + ); + + let periodic_values = vec_lambda2winter(periodic_values); + + let main_result = vec![ + FieldElement::zero(); + self.winterfell_air + .context() + .num_main_transition_constraints() + ]; + + let mut main_result_winter = vec_lambda2winter(&main_result); + self.winterfell_air.evaluate_transition::( + &main_frame, + &periodic_values, + &mut main_result_winter, + ); + + let mut result: Vec> = vec_winter2lambda(&main_result_winter); + + if self.winterfell_air.trace_layout().num_aux_segments() == 1 { + let mut rand_elements = AuxTraceRandElements::new(); + rand_elements.add_segment_elements(rap_challenges.clone()); + + let first_step = frame.get_evaluation_step(0); + let second_step = frame.get_evaluation_step(1); + + let aux_frame = EvaluationFrame::from_rows( + vec_lambda2winter(first_step.get_row_aux(0)), + vec_lambda2winter(second_step.get_row_aux(0)), + ); + + let mut aux_result = vec![ + FieldElement::zero(); + self.winterfell_air + .context() + .num_aux_transition_constraints() + ]; + let mut winter_aux_result = vec_lambda2winter(&aux_result); + self.winterfell_air.evaluate_aux_transition( + &main_frame, + &aux_frame, + &periodic_values, + &rand_elements, + &mut winter_aux_result, + ); + aux_result = vec_winter2lambda(&winter_aux_result); + result.extend_from_slice(&aux_result); + } + result + } }