|
| 1 | +// This file was created by the AIR team. |
| 2 | + |
| 3 | +use super::prelude::*; |
| 4 | + |
| 5 | +pub const N_TRACE_COLUMNS: usize = 4; |
| 6 | +pub const N_INTERACTION_COLUMNS: usize = 12; |
| 7 | + |
| 8 | +pub const RELATION_USES_PER_ROW: [RelationUse; 2] = [ |
| 9 | + RelationUse { relation_id: "Gate", uses: 1 }, |
| 10 | + RelationUse { relation_id: "RangeCheck_16", uses: 3 }, |
| 11 | +]; |
| 12 | + |
| 13 | +#[allow(unused_variables)] |
| 14 | +pub fn accumulate_constraints<Value: IValue>( |
| 15 | + input: &[Var], |
| 16 | + context: &mut Context<Value>, |
| 17 | + component_data: &dyn ComponentDataTrait<Value>, |
| 18 | + acc: &mut CompositionConstraintAccumulator, |
| 19 | +) { |
| 20 | + let [input_m31_col0, input_u32_limb_0_col1, input_u32_limb_1_col2, inv_or_one_col3] = |
| 21 | + input.try_into().unwrap(); |
| 22 | + let m31_to_u32_input_addr = acc |
| 23 | + .get_preprocessed_column(&PreProcessedColumnId { id: "m31_to_u32_input_addr".to_owned() }); |
| 24 | + let m31_to_u32_multiplicity = acc.get_preprocessed_column(&PreProcessedColumnId { |
| 25 | + id: "m31_to_u32_multiplicity".to_owned(), |
| 26 | + }); |
| 27 | + let m31_to_u32_output_addr = acc |
| 28 | + .get_preprocessed_column(&PreProcessedColumnId { id: "m31_to_u32_output_addr".to_owned() }); |
| 29 | + |
| 30 | + // Use RangeCheck_16. |
| 31 | + let tuple_0 = &[eval!(context, 1008385708), eval!(context, input_u32_limb_0_col1)]; |
| 32 | + let numerator_0 = eval!(context, 1); |
| 33 | + acc.add_to_relation(context, numerator_0, tuple_0); |
| 34 | + |
| 35 | + // Use RangeCheck_16. |
| 36 | + let tuple_1 = &[eval!(context, 1008385708), eval!(context, input_u32_limb_1_col2)]; |
| 37 | + let numerator_1 = eval!(context, 1); |
| 38 | + acc.add_to_relation(context, numerator_1, tuple_1); |
| 39 | + |
| 40 | + // Use RangeCheck_16. |
| 41 | + let tuple_2 = &[eval!(context, 1008385708), eval!(context, (32767) - (input_u32_limb_1_col2))]; |
| 42 | + let numerator_2 = eval!(context, 1); |
| 43 | + acc.add_to_relation(context, numerator_2, tuple_2); |
| 44 | + |
| 45 | + //input is zero then limb_low is zero. |
| 46 | + let constraint_3_value = |
| 47 | + eval!(context, (((input_m31_col0) * (inv_or_one_col3)) - (1)) * (input_u32_limb_0_col1)); |
| 48 | + acc.add_constraint(context, constraint_3_value); |
| 49 | + |
| 50 | + //input reconstruction. |
| 51 | + let constraint_4_value = eval!( |
| 52 | + context, |
| 53 | + (input_m31_col0) - ((input_u32_limb_0_col1) + ((input_u32_limb_1_col2) * (65536))) |
| 54 | + ); |
| 55 | + acc.add_constraint(context, constraint_4_value); |
| 56 | + |
| 57 | + // Use Gate. |
| 58 | + let tuple_5 = &[ |
| 59 | + eval!(context, 378353459), |
| 60 | + eval!(context, m31_to_u32_input_addr), |
| 61 | + eval!(context, input_m31_col0), |
| 62 | + ]; |
| 63 | + let numerator_5 = eval!(context, 1); |
| 64 | + acc.add_to_relation(context, numerator_5, tuple_5); |
| 65 | + |
| 66 | + // Yield Gate. |
| 67 | + let tuple_6 = &[ |
| 68 | + eval!(context, 378353459), |
| 69 | + eval!(context, m31_to_u32_output_addr), |
| 70 | + eval!(context, input_u32_limb_0_col1), |
| 71 | + eval!(context, input_u32_limb_1_col2), |
| 72 | + ]; |
| 73 | + let numerator_6 = eval!(context, -(m31_to_u32_multiplicity)); |
| 74 | + acc.add_to_relation(context, numerator_6, tuple_6); |
| 75 | +} |
| 76 | + |
| 77 | +pub struct Component {} |
| 78 | +impl<Value: IValue> CircuitEval<Value> for Component { |
| 79 | + fn name(&self) -> String { |
| 80 | + "m_31_to_u_32".to_string() |
| 81 | + } |
| 82 | + |
| 83 | + fn evaluate( |
| 84 | + &self, |
| 85 | + context: &mut Context<Value>, |
| 86 | + component_data: &dyn ComponentDataTrait<Value>, |
| 87 | + acc: &mut CompositionConstraintAccumulator, |
| 88 | + ) { |
| 89 | + accumulate_constraints(component_data.trace_columns(), context, component_data, acc); |
| 90 | + } |
| 91 | + |
| 92 | + fn trace_columns(&self) -> usize { |
| 93 | + N_TRACE_COLUMNS |
| 94 | + } |
| 95 | + |
| 96 | + fn interaction_columns(&self) -> usize { |
| 97 | + N_INTERACTION_COLUMNS |
| 98 | + } |
| 99 | + |
| 100 | + fn relation_uses_per_row(&self) -> &[RelationUse] { |
| 101 | + &RELATION_USES_PER_ROW |
| 102 | + } |
| 103 | +} |
| 104 | +#[cfg(test)] |
| 105 | +mod tests { |
| 106 | + use std::collections::HashMap; |
| 107 | + use stwo::core::fields::qm31::QM31; |
| 108 | + |
| 109 | + #[allow(unused_imports)] |
| 110 | + use crate::components::prelude::PreProcessedColumnId; |
| 111 | + use crate::sample_evaluations::*; |
| 112 | + use circuits::context::Context; |
| 113 | + use circuits::ivalue::qm31_from_u32s; |
| 114 | + use circuits_stark_verifier::constraint_eval::*; |
| 115 | + use circuits_stark_verifier::test_utils::TestComponentData; |
| 116 | + |
| 117 | + use super::Component; |
| 118 | + |
| 119 | + #[test] |
| 120 | + fn test_evaluation_result() { |
| 121 | + let component = Component {}; |
| 122 | + let mut context: Context<QM31> = Default::default(); |
| 123 | + context.enable_assert_eq_on_eval(); |
| 124 | + let trace_columns = [ |
| 125 | + qm31_from_u32s(1659099300, 905558730, 651199673, 1375009625), |
| 126 | + qm31_from_u32s(1591990121, 771341002, 584090809, 1375009625), |
| 127 | + qm31_from_u32s(1793317658, 1173994186, 785417401, 1375009625), |
| 128 | + qm31_from_u32s(1726208479, 1039776458, 718308537, 1375009625), |
| 129 | + ]; |
| 130 | + let interaction_columns = [ |
| 131 | + qm31_from_u32s(1005168032, 79980996, 1847888101, 1941984119), |
| 132 | + qm31_from_u32s(1072277211, 214198724, 1914996965, 1941984119), |
| 133 | + qm31_from_u32s(1139386390, 348416452, 1982105829, 1941984119), |
| 134 | + ]; |
| 135 | + let component_data = TestComponentData::from_values( |
| 136 | + &mut context, |
| 137 | + &trace_columns, |
| 138 | + &interaction_columns, |
| 139 | + qm31_from_u32s(1115374022, 1127856551, 489657863, 643630026), |
| 140 | + 32768, |
| 141 | + ); |
| 142 | + let random_coeff = |
| 143 | + context.new_var(qm31_from_u32s(474642921, 876336632, 1911695779, 974600512)); |
| 144 | + let interaction_elements = [ |
| 145 | + context.new_var(qm31_from_u32s(445623802, 202571636, 1360224996, 131355117)), |
| 146 | + context.new_var(qm31_from_u32s(476823935, 939223384, 62486082, 122423602)), |
| 147 | + ]; |
| 148 | + let preprocessed_columns = HashMap::from([ |
| 149 | + ( |
| 150 | + PreProcessedColumnId { id: "m31_to_u32_input_addr".to_owned() }, |
| 151 | + context.constant(qm31_from_u32s(15668215, 1851966168, 874056991, 2075313468)), |
| 152 | + ), |
| 153 | + ( |
| 154 | + PreProcessedColumnId { id: "m31_to_u32_output_addr".to_owned() }, |
| 155 | + context.constant(qm31_from_u32s(701904311, 1125291129, 1904795215, 38357025)), |
| 156 | + ), |
| 157 | + ( |
| 158 | + PreProcessedColumnId { id: "m31_to_u32_multiplicity".to_owned() }, |
| 159 | + context.constant(qm31_from_u32s(1979029033, 1524573277, 1930122227, 1490762084)), |
| 160 | + ), |
| 161 | + ]); |
| 162 | + let public_params = HashMap::from([]); |
| 163 | + let mut accumulator = CompositionConstraintAccumulator::new( |
| 164 | + &mut context, |
| 165 | + preprocessed_columns, |
| 166 | + public_params, |
| 167 | + random_coeff, |
| 168 | + interaction_elements, |
| 169 | + ); |
| 170 | + component.evaluate(&mut context, &component_data, &mut accumulator); |
| 171 | + let claimed_sum = |
| 172 | + context.new_var(qm31_from_u32s(1398335417, 314974026, 1722107152, 821933968)); |
| 173 | + accumulator.finalize_logup_in_pairs( |
| 174 | + &mut context, |
| 175 | + <TestComponentData as ComponentDataTrait<QM31>>::interaction_columns(&component_data), |
| 176 | + &component_data, |
| 177 | + claimed_sum, |
| 178 | + ); |
| 179 | + |
| 180 | + let result = accumulator.finalize(); |
| 181 | + let result_value = context.get(result); |
| 182 | + assert_eq!(result_value, M_31_TO_U_32_SAMPLE_EVAL_RESULT) |
| 183 | + } |
| 184 | +} |
0 commit comments