kimchi_msm/test/test_circuit/
interpreter.rs

1use crate::{
2    circuit_design::{ColAccessCap, ColWriteCap, DirectWitnessCap, LookupCap},
3    serialization::interpreter::limb_decompose_ff,
4    test::test_circuit::{
5        columns::{TestColumn, N_FSEL_TEST},
6        lookups::LookupTable,
7    },
8    LIMB_BITSIZE, N_LIMBS,
9};
10use ark_ff::{Field, PrimeField, Zero};
11
12fn fill_limbs_a_b<
13    F: PrimeField,
14    Ff: PrimeField,
15    Env: ColAccessCap<F, TestColumn> + ColWriteCap<F, TestColumn>,
16>(
17    env: &mut Env,
18    a: Ff,
19    b: Ff,
20) -> ([Env::Variable; N_LIMBS], [Env::Variable; N_LIMBS]) {
21    let a_limbs: [Env::Variable; N_LIMBS] =
22        limb_decompose_ff::<F, Ff, LIMB_BITSIZE, N_LIMBS>(&a).map(Env::constant);
23    let b_limbs: [Env::Variable; N_LIMBS] =
24        limb_decompose_ff::<F, Ff, LIMB_BITSIZE, N_LIMBS>(&b).map(Env::constant);
25    a_limbs.iter().enumerate().for_each(|(i, var)| {
26        env.write_column(TestColumn::A(i), var);
27    });
28    b_limbs.iter().enumerate().for_each(|(i, var)| {
29        env.write_column(TestColumn::B(i), var);
30    });
31    (a_limbs, b_limbs)
32}
33
34/// A constraint function for A + B - C that reads values from limbs A
35/// and B, and additionally returns resulting value in C.
36pub fn constrain_addition<F: PrimeField, Env: ColAccessCap<F, TestColumn>>(env: &mut Env) {
37    let a_limbs: [Env::Variable; N_LIMBS] =
38        core::array::from_fn(|i| Env::read_column(env, TestColumn::A(i)));
39    let b_limbs: [Env::Variable; N_LIMBS] =
40        core::array::from_fn(|i| Env::read_column(env, TestColumn::B(i)));
41    // fix cloning
42    let c_limbs: [Env::Variable; N_LIMBS] =
43        core::array::from_fn(|i| Env::read_column(env, TestColumn::C(i)));
44    let equation: [Env::Variable; N_LIMBS] =
45        core::array::from_fn(|i| a_limbs[i].clone() * b_limbs[i].clone() - c_limbs[i].clone());
46    equation.iter().for_each(|var| {
47        env.assert_zero(var.clone());
48    });
49}
50
51/// Circuit generator function for A + B - C, with D = 0.
52pub fn test_addition<
53    F: PrimeField,
54    Ff: PrimeField,
55    Env: ColAccessCap<F, TestColumn> + ColWriteCap<F, TestColumn>,
56>(
57    env: &mut Env,
58    a: Ff,
59    b: Ff,
60) {
61    let (a_limbs, b_limbs) = fill_limbs_a_b(env, a, b);
62
63    (0..N_LIMBS).for_each(|i| {
64        env.write_column(TestColumn::C(i), &(a_limbs[i].clone() + b_limbs[i].clone()));
65        env.write_column(TestColumn::D(i), &Env::constant(Zero::zero()));
66    });
67
68    constrain_addition(env);
69}
70
71/// A constraint function for A * B - D that reads values from limbs A
72/// and B, and multiplicationally returns resulting value in D.
73pub fn constrain_multiplication<F: PrimeField, Env: ColAccessCap<F, TestColumn>>(env: &mut Env) {
74    let a_limbs: [Env::Variable; N_LIMBS] =
75        core::array::from_fn(|i| Env::read_column(env, TestColumn::A(i)));
76    let b_limbs: [Env::Variable; N_LIMBS] =
77        core::array::from_fn(|i| Env::read_column(env, TestColumn::B(i)));
78    // fix cloning
79    let d_limbs: [Env::Variable; N_LIMBS] =
80        core::array::from_fn(|i| Env::read_column(env, TestColumn::D(i)));
81    let equation: [Env::Variable; N_LIMBS] =
82        core::array::from_fn(|i| a_limbs[i].clone() * b_limbs[i].clone() - d_limbs[i].clone());
83    equation.iter().for_each(|var| {
84        env.assert_zero(var.clone());
85    });
86}
87
88/// Circuit generator function for A * B - C, with D = 0.
89pub fn test_multiplication<
90    F: PrimeField,
91    Ff: PrimeField,
92    Env: ColAccessCap<F, TestColumn> + ColWriteCap<F, TestColumn>,
93>(
94    env: &mut Env,
95    a: Ff,
96    b: Ff,
97) {
98    let (a_limbs, b_limbs) = fill_limbs_a_b(env, a, b);
99
100    (0..N_LIMBS).for_each(|i| {
101        env.write_column(TestColumn::D(i), &(a_limbs[i].clone() * b_limbs[i].clone()));
102        env.write_column(TestColumn::C(i), &Env::constant(Zero::zero()));
103    });
104
105    constrain_multiplication(env);
106}
107
108/// A constraint function for A * B - D that reads values from limbs A
109/// and B, and multiplication_constally returns resulting value in D.
110pub fn constrain_test_const<F: PrimeField, Env: ColAccessCap<F, TestColumn>>(
111    env: &mut Env,
112    constant: F,
113) {
114    let a0 = Env::read_column(env, TestColumn::A(0));
115    let b0 = Env::read_column(env, TestColumn::B(0));
116    let equation = a0.clone() * b0.clone() - Env::constant(constant);
117    env.assert_zero(equation.clone());
118}
119
120/// Circuit generator function for A_0 * B_0 - const, with every other column = 0
121pub fn test_const<F: PrimeField, Env: ColAccessCap<F, TestColumn> + ColWriteCap<F, TestColumn>>(
122    env: &mut Env,
123    a: F,
124    b: F,
125    constant: F,
126) {
127    env.write_column(TestColumn::A(0), &Env::constant(a));
128    env.write_column(TestColumn::B(0), &Env::constant(b));
129
130    constrain_test_const(env, constant);
131}
132
133/// A constraint function for A_0 + B_0 - FIXED_SEL_1
134pub fn constrain_test_fixed_sel<F: PrimeField, Env: ColAccessCap<F, TestColumn>>(env: &mut Env) {
135    let a0 = Env::read_column(env, TestColumn::A(0));
136    let b0 = Env::read_column(env, TestColumn::B(0));
137    let fixed_e = Env::read_column(env, TestColumn::FixedSel1);
138    let equation = a0.clone() + b0.clone() - fixed_e;
139    env.assert_zero(equation.clone());
140}
141
142/// A constraint function for A_0^7 + B_0 - FIXED_SEL_1
143pub fn constrain_test_fixed_sel_degree_7<F: PrimeField, Env: ColAccessCap<F, TestColumn>>(
144    env: &mut Env,
145) {
146    let a0 = Env::read_column(env, TestColumn::A(0));
147    let b0 = Env::read_column(env, TestColumn::B(0));
148    let fixed_e = Env::read_column(env, TestColumn::FixedSel1);
149    let a0_2 = a0.clone() * a0.clone();
150    let a0_4 = a0_2.clone() * a0_2.clone();
151    let a0_6 = a0_4.clone() * a0_2.clone();
152    let a0_7 = a0_6.clone() * a0.clone();
153    let equation = a0_7.clone() + b0.clone() - fixed_e;
154    env.assert_zero(equation.clone());
155}
156
157/// A constraint function for 3 * A_0^7 + 42 * B_0 - FIXED_SEL_1
158pub fn constrain_test_fixed_sel_degree_7_with_constants<
159    F: PrimeField,
160    Env: ColAccessCap<F, TestColumn>,
161>(
162    env: &mut Env,
163) {
164    let a0 = Env::read_column(env, TestColumn::A(0));
165    let forty_two = Env::constant(F::from(42u32));
166    let three = Env::constant(F::from(3u32));
167    let b0 = Env::read_column(env, TestColumn::B(0));
168    let fixed_e = Env::read_column(env, TestColumn::FixedSel1);
169    let a0_2 = a0.clone() * a0.clone();
170    let a0_4 = a0_2.clone() * a0_2.clone();
171    let a0_6 = a0_4.clone() * a0_2.clone();
172    let a0_7 = a0_6.clone() * a0.clone();
173    let equation = three * a0_7.clone() + forty_two * b0.clone() - fixed_e;
174    env.assert_zero(equation.clone());
175}
176
177// NB: Assumes non-standard selectors
178/// A constraint function for 3 * A_0^7 + B_0 * FIXED_SEL_3
179pub fn constrain_test_fixed_sel_degree_7_mul_witness<
180    F: PrimeField,
181    Env: ColAccessCap<F, TestColumn>,
182>(
183    env: &mut Env,
184) {
185    let a0 = Env::read_column(env, TestColumn::A(0));
186    let three = Env::constant(F::from(3u32));
187    let b0 = Env::read_column(env, TestColumn::B(0));
188    let fixed_e = Env::read_column(env, TestColumn::FixedSel3);
189    let a0_2 = a0.clone() * a0.clone();
190    let a0_4 = a0_2.clone() * a0_2.clone();
191    let a0_6 = a0_4.clone() * a0_2.clone();
192    let a0_7 = a0_6.clone() * a0.clone();
193    let equation = three * a0_7.clone() + b0.clone() * fixed_e;
194    env.assert_zero(equation.clone());
195}
196
197/// Circuit generator function for A_0 + B_0 - FIXED_SEL_1.
198pub fn test_fixed_sel<
199    F: PrimeField,
200    Env: ColAccessCap<F, TestColumn> + ColWriteCap<F, TestColumn>,
201>(
202    env: &mut Env,
203    a: F,
204) {
205    env.write_column(TestColumn::A(0), &Env::constant(a));
206    let fixed_e = env.read_column(TestColumn::FixedSel1);
207    env.write_column(TestColumn::B(0), &(fixed_e - Env::constant(a)));
208
209    constrain_test_fixed_sel(env);
210}
211
212/// Circuit generator function for A_0^7 + B_0 - FIXED_SEL_1.
213pub fn test_fixed_sel_degree_7<
214    F: PrimeField,
215    Env: ColAccessCap<F, TestColumn> + ColWriteCap<F, TestColumn>,
216>(
217    env: &mut Env,
218    a: F,
219) {
220    env.write_column(TestColumn::A(0), &Env::constant(a));
221    let a_2 = a * a;
222    let a_4 = a_2 * a_2;
223    let a_6 = a_4 * a_2;
224    let a_7 = a_6 * a;
225    let fixed_e = env.read_column(TestColumn::FixedSel1);
226    env.write_column(TestColumn::B(0), &(fixed_e - Env::constant(a_7)));
227    constrain_test_fixed_sel_degree_7(env);
228}
229
230/// Circuit generator function for 3 * A_0^7 + 42 * B_0 - FIXED_SEL_1.
231pub fn test_fixed_sel_degree_7_with_constants<
232    F: PrimeField,
233    Env: ColAccessCap<F, TestColumn> + ColWriteCap<F, TestColumn>,
234>(
235    env: &mut Env,
236    a: F,
237) {
238    env.write_column(TestColumn::A(0), &Env::constant(a));
239    let a_2 = a * a;
240    let a_4 = a_2 * a_2;
241    let a_6 = a_4 * a_2;
242    let a_7 = a_6 * a;
243    let fixed_e = env.read_column(TestColumn::FixedSel1);
244    let inv_42 = F::from(42u32).inverse().unwrap();
245    let three = F::from(3u32);
246    env.write_column(
247        TestColumn::B(0),
248        &((fixed_e - Env::constant(three) * Env::constant(a_7)) * Env::constant(inv_42)),
249    );
250    constrain_test_fixed_sel_degree_7_with_constants(env);
251}
252
253// NB: Assumes non-standard selectors
254/// Circuit generator function for 3 * A_0^7 + B_0 * FIXED_SEL_3.
255pub fn test_fixed_sel_degree_7_mul_witness<
256    F: PrimeField,
257    Env: ColAccessCap<F, TestColumn> + ColWriteCap<F, TestColumn> + DirectWitnessCap<F, TestColumn>,
258>(
259    env: &mut Env,
260    a: F,
261) {
262    env.write_column(TestColumn::A(0), &Env::constant(a));
263    let a_2 = a * a;
264    let a_4 = a_2 * a_2;
265    let a_6 = a_4 * a_2;
266    let a_7 = a_6 * a;
267    let fixed_e = env.read_column(TestColumn::FixedSel3);
268    let three = F::from(3u32);
269    let val_fixed_e: F = Env::variable_to_field(fixed_e);
270    let inv_fixed_e: F = val_fixed_e.inverse().unwrap();
271    let res = -three * a_7 * inv_fixed_e;
272    let res_var = Env::constant(res);
273    env.write_column(TestColumn::B(0), &res_var);
274    constrain_test_fixed_sel_degree_7_mul_witness(env);
275}
276
277pub fn constrain_lookups<
278    F: PrimeField,
279    Env: ColAccessCap<F, TestColumn> + LookupCap<F, TestColumn, LookupTable>,
280>(
281    env: &mut Env,
282) {
283    let a0 = Env::read_column(env, TestColumn::A(0));
284    let a1 = Env::read_column(env, TestColumn::A(1));
285
286    env.lookup(LookupTable::RangeCheck15, vec![a0.clone()]);
287    env.lookup(LookupTable::RangeCheck15, vec![a1.clone()]);
288
289    let cur_index = Env::read_column(env, TestColumn::FixedSel1);
290    let prev_index = Env::read_column(env, TestColumn::FixedSel2);
291    let next_index = Env::read_column(env, TestColumn::FixedSel3);
292
293    env.lookup(
294        LookupTable::RuntimeTable1,
295        vec![
296            cur_index.clone(),
297            prev_index.clone(),
298            next_index.clone(),
299            Env::constant(F::from(4u64)),
300        ],
301    );
302
303    // For now we only allow one read per runtime table with runtime_create_column = true.
304    //env.lookup(LookupTable::RuntimeTable1, vec![a0.clone(), a1.clone()]);
305
306    env.lookup_runtime_write(
307        LookupTable::RuntimeTable2,
308        vec![
309            Env::constant(F::from(1u64 << 26)),
310            Env::constant(F::from(5u64)),
311        ],
312    );
313    env.lookup_runtime_write(
314        LookupTable::RuntimeTable2,
315        vec![cur_index, Env::constant(F::from(5u64))],
316    );
317    env.lookup(
318        LookupTable::RuntimeTable2,
319        vec![
320            Env::constant(F::from(1u64 << 26)),
321            Env::constant(F::from(5u64)),
322        ],
323    );
324    env.lookup(
325        LookupTable::RuntimeTable2,
326        vec![prev_index, Env::constant(F::from(5u64))],
327    );
328}
329
330pub fn lookups_circuit<
331    F: PrimeField,
332    Env: ColAccessCap<F, TestColumn>
333        + ColWriteCap<F, TestColumn>
334        + DirectWitnessCap<F, TestColumn>
335        + LookupCap<F, TestColumn, LookupTable>,
336>(
337    env: &mut Env,
338    domain_size: usize,
339) {
340    for row_i in 0..domain_size {
341        env.write_column(TestColumn::A(0), &Env::constant(F::from(11u64)));
342        env.write_column(TestColumn::A(1), &Env::constant(F::from(17u64)));
343
344        constrain_lookups(env);
345
346        if row_i < domain_size - 1 {
347            env.next_row();
348        }
349    }
350}
351
352/// Fixed selectors for the test circuit.
353pub fn build_fixed_selectors<F: Field>(domain_size: usize) -> Box<[Vec<F>; N_FSEL_TEST]> {
354    // 0 1 2 3 4 ...
355    let sel1 = (0..domain_size).map(|i| F::from(i as u64)).collect();
356    // 0 0 1 2 3 4 ...
357    let sel2 = (0..domain_size)
358        .map(|i| {
359            if i == 0 {
360                F::zero()
361            } else {
362                F::from((i as u64) - 1)
363            }
364        })
365        .collect();
366    // 1 2 3 4 5 ...
367    let sel3 = (0..domain_size).map(|i| F::from((i + 1) as u64)).collect();
368
369    Box::new([sel1, sel2, sel3])
370}
kimchi_msm/test/test_circuit/interpreter.rs

kimchi_msm/test/test_circuit/
interpreter.rs
