Skip to main content

midnight_circuits/vec/
vector_gadget.rs

1// This file is part of MIDNIGHT-ZK.
2// Copyright (C) 2025 Midnight Foundation
3// SPDX-License-Identifier: Apache-2.0
4// Licensed under the Apache License, Version 2.0 (the "License");
5// You may not use this file except in compliance with the License.
6// You may obtain a copy of the License at
7// http://www.apache.org/licenses/LICENSE-2.0
8// Unless required by applicable law or agreed to in writing, software
9// distributed under the License is distributed on an "AS IS" BASIS,
10// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11// See the License for the specific language governing permissions and
12// limitations under the License.
13
14use ff::PrimeField;
15use midnight_proofs::{
16    circuit::{Layouter, Value},
17    plonk::Error,
18};
19use num_bigint::BigUint;
20
21use crate::{
22    field::{
23        decomposition::chip::P2RDecompositionChip, AssignedBounded, AssignedNative, NativeChip,
24        NativeGadget,
25    },
26    instructions::{
27        division::DivisionInstructions, vector::VectorInstructions, ArithInstructions,
28        AssertionInstructions, AssignmentInstructions, BinaryInstructions, ComparisonInstructions,
29        ControlFlowInstructions, EqualityInstructions, RangeCheckInstructions,
30    },
31    types::{AssignedBit, AssignedVector, InnerValue, Vectorizable},
32    vec::get_lims,
33};
34
35type NG<F> = NativeGadget<F, P2RDecompositionChip<F>, NativeChip<F>>;
36
37#[derive(Clone, Debug)]
38/// A gadget for vector operations of elements that are or fit within a native
39/// field element:
40pub struct VectorGadget<F: PrimeField> {
41    native_gadget: NG<F>,
42}
43
44impl<F> VectorGadget<F>
45where
46    F: PrimeField,
47{
48    /// Create a new vector gadgets.
49    pub fn new(native_gadget: &NG<F>) -> Self {
50        Self {
51            native_gadget: native_gadget.clone(),
52        }
53    }
54}
55
56impl<F, T, const M: usize, const A: usize> VectorInstructions<F, T, M, A> for VectorGadget<F>
57where
58    F: PrimeField,
59    T: Vectorizable,
60    T::Element: Copy,
61    NG<F>: RangeCheckInstructions<F, AssignedNative<F>>
62        + AssignmentInstructions<F, T>
63        + AssignmentInstructions<F, AssignedNative<F>>
64        + AssignmentInstructions<F, AssignedBit<F>>
65        + EqualityInstructions<F, AssignedNative<F>>
66        + BinaryInstructions<F>
67        + ControlFlowInstructions<F, AssignedNative<F>>
68        + ControlFlowInstructions<F, T>
69        + DivisionInstructions<F, AssignedNative<F>>
70        + AssertionInstructions<F, AssignedBit<F>>
71        + ArithInstructions<F, AssignedNative<F>>,
72{
73    fn resize<const L: usize>(
74        &self,
75        layouter: &mut impl Layouter<F>,
76        input: AssignedVector<F, T, M, A>,
77    ) -> Result<AssignedVector<F, T, L, A>, Error> {
78        assert_eq!(L % A, 0);
79        assert!(L > M);
80
81        let extra_pad = self
82            .native_gadget
83            .assign_many(layouter, &vec![Value::known(T::FILLER); L - M])?;
84
85        let buffer: [T; L] =
86            [extra_pad.as_slice(), input.buffer.as_slice()].concat().try_into().unwrap();
87
88        Ok(AssignedVector {
89            buffer,
90            len: input.len.clone(),
91        })
92    }
93
94    fn assign_with_filler(
95        &self,
96        layouter: &mut impl Layouter<F>,
97        value: Value<Vec<T::Element>>,
98        filler: Option<T::Element>,
99    ) -> Result<AssignedVector<F, T, M, A>, Error> {
100        let ng = &self.native_gadget;
101        let filler = filler.unwrap_or(T::FILLER);
102        let (data_val, len_val) = value
103            .map(|v| {
104                assert!(v.len() <= M);
105                let len = F::from(v.len() as u64);
106                let mut buffer = [filler; M];
107                buffer[get_lims::<M, A>(v.len())].copy_from_slice(v.as_slice());
108                (buffer, len)
109            })
110            .unzip();
111
112        let data = ng
113            .assign_many(layouter, &data_val.transpose_array())?
114            .try_into()
115            .expect("Length mismatch in AssignedVector.");
116        let len = ng.assign_lower_than_fixed(layouter, len_val, &(M + 1).into())?;
117        Ok(AssignedVector { buffer: data, len })
118    }
119
120    fn padding_flag(
121        &self,
122        layouter: &mut impl Layouter<F>,
123        input: &AssignedVector<F, T, M, A>,
124    ) -> Result<[AssignedBit<F>; M], Error> {
125        let ng = &self.native_gadget;
126        let (start, end) = self.get_limits(layouter, input)?;
127        let mut is_data: AssignedBit<F> = ng.assign_fixed(layouter, true)?;
128
129        let result = (0..M - A)
130            .map(|i| {
131                let is_start = ng.is_equal_to_fixed(layouter, &start, F::from(i as u64))?;
132                is_data = ng.xor(layouter, &[is_data.clone(), is_start])?;
133                Ok(is_data.clone())
134            })
135            .collect::<Result<Vec<_>, Error>>()?;
136
137        let last_chunk = (M - A..M)
138            .map(|i| {
139                let is_end = ng.is_equal_to_fixed(layouter, &end, F::from(i as u64))?;
140                is_data = ng.xor(layouter, &[is_data.clone(), is_end])?;
141                Ok(is_data.clone())
142            })
143            .collect::<Result<Vec<_>, Error>>()?;
144
145        Ok([result, last_chunk].concat().try_into().expect("Mismatch in vector lengths"))
146    }
147
148    fn get_limits(
149        &self,
150        layouter: &mut impl Layouter<F>,
151        input: &AssignedVector<F, T, M, A>,
152    ) -> Result<(AssignedNative<F>, AssignedNative<F>), Error> {
153        let ng = &self.native_gadget;
154        let end: AssignedNative<F> = {
155            // The last data position within the last chunk. Value in [0, A);
156            // 0 means the last chunk is full, all its positions are data.
157            let offset = ng.rem(layouter, &input.len, A.into(), Some(M.into()))?;
158
159            // if offset != 0.  End = M - (A - offset).
160            let end1 = ng.add_constant(layouter, &offset, F::from(M as u64 - A as u64))?;
161            // if offset == 0.  End = M - (A - offset) + A = M.
162            let end2 = ng.add_constant(layouter, &end1, F::from(A as u64))?;
163            let is_zero = ng.is_equal_to_fixed(layouter, &offset, F::ZERO)?;
164            ng.select(layouter, &is_zero, &end2, &end1)
165        }?;
166
167        // The index where the data starts.
168        let start: AssignedNative<F> = ng.sub(layouter, &end, &input.len)?;
169
170        Ok((start, end))
171    }
172
173    fn trim_beginning(
174        &self,
175        layouter: &mut impl Layouter<F>,
176        input: &AssignedVector<F, T, M, A>,
177        n_elems: usize,
178    ) -> Result<AssignedVector<F, T, M, A>, Error> {
179        let ng = &self.native_gadget;
180        let a_max_bits = (usize::BITS - A.leading_zeros()) as usize;
181
182        // Assert input.len >= n_elems.
183        let len_complement =
184            ng.linear_combination(layouter, &[(-F::ONE, input.len.clone())], F::from(M as u64))?;
185        ng.assert_lower_than_fixed(layouter, &len_complement, &BigUint::from(M + 1 - n_elems))?;
186
187        // We divide the number of elements to be trimmed in 2 parts.
188        // The A-sized whole chunks, one last <A sized piece.
189        // (1) The A-sized chunks won't modify the alignment, so modifying the value
190        // the vector length is enough to have them trimmed. They will remain
191        // in the buffer but they will be considered padding.
192        // (2) Trimming this last piece may require some realignment of the vector
193        // that ensures the padding at the end remains in [0, A).
194
195        let last_trim = n_elems % A;
196
197        // Length of last chunk ( or 0 if it is full ).
198        let last_len = ng.rem(layouter, &input.len, A.into(), Some(M.into()))?;
199
200        // `modulus` already ensures last_len is in [0, A), so unsafe conversion can be
201        // used here.
202        let bounded_last_len =
203            AssignedBounded::to_assigned_bounded_unsafe(&last_len, a_max_bits as u32);
204
205        // We need to shift right by A if the padding at the end after the left shift is
206        // >= A.
207        let needs_adjust = {
208            let leq_shift = ng.leq_fixed(layouter, &bounded_last_len, F::from(last_trim as u64))?;
209            let full_last = ng.is_equal_to_fixed(layouter, &last_len, F::ZERO)?;
210
211            // Since full_last = 1 => leq_shift = 1:
212            //     let not_full_last = ng.not(layouter, &full_last)?;
213            //     ng.and(layouter, &[not_full_last, leq_shift])
214            // A XOR operation is equivalent to the commented code above.
215            ng.xor(layouter, &[full_last, leq_shift])
216        }?;
217
218        // Shift the original buffer `last_trim` positions to the left.
219        // Then, add A filler elements to the left, in case we need to shift A to the
220        // right to adjust the padding at the end.
221        let buffer = {
222            let filler = ng.assign_many_fixed(layouter, &vec![T::FILLER; A + last_trim])?;
223            [&filler[..A], &input.buffer[last_trim..], &filler[A..]].concat()
224        };
225        debug_assert_eq!(buffer.len(), M + A);
226
227        let buffer: [_; M] = (0..M)
228            .map(|i| ng.select(layouter, &needs_adjust, &buffer[i], &buffer[A + i]))
229            .collect::<Result<Vec<_>, Error>>()?
230            .try_into()
231            .unwrap();
232
233        // Compute final length.
234        let len = ng.add_constant(layouter, &input.len, -F::from(n_elems as u64))?;
235
236        Ok(AssignedVector { buffer, len })
237    }
238}
239
240impl<F, const M: usize, T, const A: usize> AssignmentInstructions<F, AssignedVector<F, T, M, A>>
241    for VectorGadget<F>
242where
243    F: PrimeField,
244    T: Vectorizable,
245    T::Element: Copy,
246    Self: VectorInstructions<F, T, M, A>,
247{
248    fn assign_fixed(
249        &self,
250        _layouter: &mut impl Layouter<F>,
251        _constant: <AssignedVector<F, T, M, A> as InnerValue>::Element,
252    ) -> Result<AssignedVector<F, T, M, A>, Error> {
253        unimplemented!("You should not be assigining a fixed `AssignedVector`")
254    }
255
256    fn assign(
257        &self,
258        layouter: &mut impl Layouter<F>,
259        value: Value<<AssignedVector<F, T, M, A> as InnerValue>::Element>,
260    ) -> Result<AssignedVector<F, T, M, A>, Error> {
261        self.assign_with_filler(layouter, value, None)
262    }
263}
264
265impl<F, const M: usize, T, const A: usize> EqualityInstructions<F, AssignedVector<F, T, M, A>>
266    for VectorGadget<F>
267where
268    F: PrimeField,
269    T: Vectorizable,
270    T::Element: Copy,
271    Self: VectorInstructions<F, T, M, A>,
272    NG<F>: ArithInstructions<F, AssignedNative<F>>
273        + EqualityInstructions<F, T>
274        + EqualityInstructions<F, AssignedNative<F>>
275        + BinaryInstructions<F>,
276{
277    fn is_equal(
278        &self,
279        layouter: &mut impl Layouter<F>,
280        x: &AssignedVector<F, T, M, A>,
281        y: &AssignedVector<F, T, M, A>,
282    ) -> Result<AssignedBit<F>, Error> {
283        let ng = &self.native_gadget;
284        // Check all data values are equal.
285        let val_checks = self
286            .padding_flag(layouter, x)?
287            .into_iter()
288            .zip(x.buffer.iter().zip(y.buffer.iter()))
289            .map(|(is_padding, (a, b))| {
290                let a_eq_b = ng.is_equal(layouter, a, b)?;
291                ng.or(layouter, &[is_padding, a_eq_b])
292            })
293            .collect::<Result<Vec<_>, Error>>()?;
294
295        // Check lengths are equal.
296        let len_check = ng.is_equal(layouter, &x.len, &y.len)?;
297
298        ng.and(layouter, &[val_checks.as_slice(), &[len_check]].concat())
299    }
300
301    fn is_not_equal(
302        &self,
303        layouter: &mut impl Layouter<F>,
304        x: &AssignedVector<F, T, M, A>,
305        y: &AssignedVector<F, T, M, A>,
306    ) -> Result<AssignedBit<F>, Error> {
307        let b = self.is_equal(layouter, x, y)?;
308        self.native_gadget.not(layouter, &b)
309    }
310
311    fn is_equal_to_fixed(
312        &self,
313        layouter: &mut impl Layouter<F>,
314        x: &AssignedVector<F, T, M, A>,
315        constant: Vec<T::Element>,
316    ) -> Result<AssignedBit<F>, Error> {
317        let ng = &self.native_gadget;
318        let ct_len = constant.len();
319
320        let eq_len = ng.is_equal_to_fixed(layouter, &x.len, F::from(ct_len as u64))?;
321
322        let mut element_checks = x.buffer[get_lims::<M, A>(ct_len)]
323            .iter()
324            .zip(constant.iter())
325            .map(|(a, c)| ng.is_equal_to_fixed(layouter, a, *c))
326            .collect::<Result<Vec<_>, Error>>()?;
327        element_checks.push(eq_len);
328
329        ng.and(layouter, &element_checks)
330    }
331
332    fn is_not_equal_to_fixed(
333        &self,
334        layouter: &mut impl Layouter<F>,
335        x: &AssignedVector<F, T, M, A>,
336        constant: Vec<T::Element>,
337    ) -> Result<AssignedBit<F>, Error> {
338        let b = self.is_equal_to_fixed(layouter, x, constant)?;
339        self.native_gadget.not(layouter, &b)
340    }
341}
342
343impl<F, T, const M: usize, const A: usize> AssertionInstructions<F, AssignedVector<F, T, M, A>>
344    for VectorGadget<F>
345where
346    F: PrimeField,
347    T: Vectorizable,
348    T::Element: Copy,
349    Self: VectorInstructions<F, T, M, A> + EqualityInstructions<F, AssignedVector<F, T, M, A>>,
350    NG<F>: ArithInstructions<F, AssignedNative<F>>
351        + EqualityInstructions<F, T>
352        + EqualityInstructions<F, AssignedNative<F>>
353        + AssertionInstructions<F, AssignedBit<F>>
354        + AssertionInstructions<F, T>
355        + BinaryInstructions<F>,
356{
357    fn assert_equal(
358        &self,
359        layouter: &mut impl Layouter<F>,
360        x: &AssignedVector<F, T, M, A>,
361        y: &AssignedVector<F, T, M, A>,
362    ) -> Result<(), Error> {
363        let is_equal = self.is_equal(layouter, x, y)?;
364        self.native_gadget.assert_equal_to_fixed(layouter, &is_equal, true)
365    }
366
367    fn assert_not_equal(
368        &self,
369        layouter: &mut impl Layouter<F>,
370        x: &AssignedVector<F, T, M, A>,
371        y: &AssignedVector<F, T, M, A>,
372    ) -> Result<(), Error> {
373        let x_eq_y = self.is_equal(layouter, x, y)?;
374        self.native_gadget.assert_equal_to_fixed(layouter, &x_eq_y, false)
375    }
376
377    fn assert_equal_to_fixed(
378        &self,
379        layouter: &mut impl Layouter<F>,
380        x: &AssignedVector<F, T, M, A>,
381        constant: <AssignedVector<F, T, M, A> as InnerValue>::Element,
382    ) -> Result<(), Error> {
383        let ng = &self.native_gadget;
384        let ct_len = constant.len();
385        ng.assert_equal_to_fixed(layouter, &x.len, F::from(ct_len as u64))?;
386
387        x.buffer[get_lims::<M, A>(ct_len)]
388            .iter()
389            .zip(constant.iter())
390            .map(|(a, c)| ng.assert_equal_to_fixed(layouter, a, *c))
391            .collect::<Result<Vec<()>, Error>>()?;
392        Ok(())
393    }
394
395    fn assert_not_equal_to_fixed(
396        &self,
397        layouter: &mut impl Layouter<F>,
398        x: &AssignedVector<F, T, M, A>,
399        constant: <AssignedVector<F, T, M, A> as InnerValue>::Element,
400    ) -> Result<(), Error> {
401        let is_equal = self.is_equal_to_fixed(layouter, x, constant)?;
402        self.native_gadget.assert_equal_to_fixed(layouter, &is_equal, false)
403    }
404}
405
406#[cfg(any(test, feature = "testing"))]
407use midnight_proofs::plonk::{Column, ConstraintSystem, Instance};
408
409#[cfg(any(test, feature = "testing"))]
410use crate::testing_utils::FromScratch;
411
412#[cfg(any(test, feature = "testing"))]
413impl<F: PrimeField> FromScratch<F> for VectorGadget<F> {
414    type Config = <NG<F> as FromScratch<F>>::Config;
415
416    fn new_from_scratch(config: &Self::Config) -> Self {
417        Self {
418            native_gadget: <NG<F> as FromScratch<F>>::new_from_scratch(config),
419        }
420    }
421
422    fn configure_from_scratch(
423        meta: &mut ConstraintSystem<F>,
424        instance_columns: &[Column<Instance>; 2],
425    ) -> Self::Config {
426        <NG<F>>::configure_from_scratch(meta, instance_columns)
427    }
428
429    fn load_from_scratch(&self, layouter: &mut impl Layouter<F>) -> Result<(), Error> {
430        self.native_gadget.load_from_scratch(layouter)
431    }
432}
433
434#[cfg(test)]
435mod tests {
436    use ff::{Field, FromUniformBytes, PrimeField};
437    use midnight_proofs::{
438        circuit::{Layouter, SimpleFloorPlanner, Value},
439        dev::MockProver,
440        plonk::{Circuit, ConstraintSystem},
441    };
442    use rand_chacha::{rand_core::SeedableRng, ChaCha12Rng};
443
444    use super::*;
445    use crate::{
446        field::{
447            decomposition::chip::{P2RDecompositionChip, P2RDecompositionConfig},
448            AssignedNative, NativeChip, NativeGadget,
449        },
450        testing_utils::FromScratch,
451        utils::{circuit_modeling::circuit_to_json, util::fe_to_big},
452    };
453
454    struct TestCircuit<F: PrimeField, const M: usize, const A: usize> {
455        input_1: Value<Vec<F>>,
456        input_2: Vec<F>, // We don't use value here in order to easily mutate the padding.
457        opts: TestOpts,
458    }
459
460    enum TestOpts {
461        // Tests vector equality.
462        Eq { mutate_padding: bool, equal: bool },
463        // Test data limit (indices) on a vector.
464        Limits,
465        // Test padding_flag instruction.
466        Padding,
467        // Test trim.
468        Trim { trim_size: usize },
469    }
470
471    type NG<F> = NativeGadget<F, P2RDecompositionChip<F>, NativeChip<F>>;
472
473    impl<F: PrimeField, const M: usize, const A: usize> Circuit<F> for TestCircuit<F, M, A> {
474        type Config = P2RDecompositionConfig;
475
476        type FloorPlanner = SimpleFloorPlanner;
477
478        type Params = ();
479
480        fn without_witnesses(&self) -> Self {
481            unreachable!();
482        }
483
484        fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
485            let comm_ic = meta.instance_column();
486            let instance_column = meta.instance_column();
487            NativeGadget::configure_from_scratch(meta, &[comm_ic, instance_column])
488        }
489
490        fn synthesize(
491            &self,
492            config: Self::Config,
493            mut layouter: impl Layouter<F>,
494        ) -> Result<(), Error> {
495            let ng = NG::<F>::new_from_scratch(&config);
496            let vg = VectorGadget::new(&ng);
497
498            match self.opts {
499                TestOpts::Eq {
500                    mutate_padding,
501                    equal,
502                } => {
503                    let vec_1: AssignedVector<F, AssignedNative<F>, M, A> =
504                        vg.assign(&mut layouter, self.input_1.clone())?;
505
506                    let mut vec_2: AssignedVector<F, AssignedNative<F>, M, A> =
507                        vg.assign(&mut layouter, Value::known(self.input_2.clone()))?;
508
509                    // Mutate padding
510                    if mutate_padding {
511                        let range = get_lims::<M, A>(self.input_2.len());
512                        for i in 0..range.start {
513                            vec_2.buffer[i] =
514                                ng.add_constant(&mut layouter, &vec_2.buffer[i], F::ONE)?;
515                        }
516                        for i in range.end..M {
517                            vec_2.buffer[i] =
518                                ng.add_constant(&mut layouter, &vec_2.buffer[i], F::ONE)?;
519                        }
520                    }
521
522                    let check = vg.is_equal(&mut layouter, &vec_1, &vec_2)?;
523
524                    ng.assert_equal_to_fixed(&mut layouter, &check, equal)?;
525                }
526                TestOpts::Limits => {
527                    let vec_1: AssignedVector<F, AssignedNative<F>, M, A> =
528                        vg.assign(&mut layouter, self.input_1.clone())?;
529
530                    let limits = vg.get_limits(&mut layouter, &vec_1)?;
531                    let (start, end) = vec_1
532                        .len
533                        .value()
534                        .map(|l| {
535                            let len: usize = fe_to_big(*l).try_into().unwrap();
536                            let range = get_lims::<M, A>(len);
537                            (F::from(range.start as u64), F::from(range.end as u64))
538                        })
539                        .unzip();
540                    let start = ng.assign(&mut layouter, start)?;
541                    let end = ng.assign(&mut layouter, end)?;
542                    ng.assert_equal(&mut layouter, &limits.0, &start)?;
543                    ng.assert_equal(&mut layouter, &limits.1, &end)?;
544                }
545
546                TestOpts::Padding => {
547                    let vec_1: AssignedVector<F, AssignedNative<F>, M, A> =
548                        vg.assign(&mut layouter, self.input_1.clone())?;
549
550                    let expected: [Value<bool>; M] = vec_1
551                        .len
552                        .value()
553                        .map(|l| {
554                            let len: usize = fe_to_big(*l).try_into().unwrap();
555                            let range = get_lims::<M, A>(len);
556                            let mut result = vec![true; M];
557                            result[range].iter_mut().for_each(|r| {
558                                *r = false;
559                            });
560                            result.try_into().unwrap()
561                        })
562                        .transpose_array();
563
564                    let result = vg.padding_flag(&mut layouter, &vec_1)?;
565
566                    for (r, e) in result.iter().zip(expected.iter()) {
567                        let e: AssignedBit<F> = ng.assign(&mut layouter, *e)?;
568                        ng.assert_equal(&mut layouter, &e, r)?;
569                    }
570                }
571
572                TestOpts::Trim { trim_size: n_elems } => {
573                    let vec_1: AssignedVector<F, AssignedNative<F>, M, A> =
574                        vg.assign(&mut layouter, self.input_1.clone())?;
575
576                    let result = vg.trim_beginning(&mut layouter, &vec_1, n_elems)?;
577
578                    vg.assert_equal_to_fixed(&mut layouter, &result, self.input_2.clone())?;
579                }
580            }
581
582            ng.load_from_scratch(&mut layouter)
583        }
584    }
585
586    fn run_eq_vec_test<F, const M: usize, const A: usize>(
587        input_1: &[F],
588        input_2: &[F],
589        equal: bool,
590        mutate_padding: bool,
591        cost_model: bool,
592    ) where
593        F: PrimeField + FromUniformBytes<64> + Ord,
594    {
595        let circuit = TestCircuit::<F, M, A> {
596            input_1: Value::known(input_1.to_vec()),
597            input_2: input_2.to_vec(),
598            opts: TestOpts::Eq {
599                equal,
600                mutate_padding,
601            },
602        };
603
604        let k = 14;
605
606        MockProver::run(k, &circuit, vec![vec![], vec![]]).unwrap().assert_satisfied();
607
608        if cost_model {
609            circuit_to_json(
610                "Vector equality",
611                format!("Vector equality check with M={M}").as_str(),
612                circuit,
613            );
614        }
615    }
616
617    fn run_limit_vec_test<F, const M: usize, const A: usize>(input_1: &[F], cost_model: bool)
618    where
619        F: PrimeField + FromUniformBytes<64> + Ord,
620    {
621        let circuit = TestCircuit::<F, M, A> {
622            input_1: Value::known(input_1.to_vec()),
623            input_2: vec![],
624            opts: TestOpts::Limits,
625        };
626
627        let k = 14;
628
629        MockProver::run(k, &circuit, vec![vec![], vec![]]).unwrap().assert_satisfied();
630
631        if cost_model {
632            circuit_to_json(
633                "Vector limits check",
634                format!("Vector limit check with M={M}").as_str(),
635                circuit,
636            );
637        }
638    }
639
640    fn run_padding_flags_test<F, const M: usize, const A: usize>(input_1: &[F], cost_model: bool)
641    where
642        F: PrimeField + FromUniformBytes<64> + Ord,
643    {
644        let circuit = TestCircuit::<F, M, A> {
645            input_1: Value::known(input_1.to_vec()),
646            input_2: vec![],
647            opts: TestOpts::Padding,
648        };
649
650        let k = 14;
651
652        MockProver::run(k, &circuit, vec![vec![], vec![]]).unwrap().assert_satisfied();
653
654        if cost_model {
655            circuit_to_json(
656                "Vector padding flags.",
657                format!("Vector padding flags with M={M}").as_str(),
658                circuit,
659            );
660        }
661    }
662
663    fn run_trim_vec_test<F, const M: usize, const A: usize>(
664        input_1: &[F],
665        trim_size: usize,
666        cost_model: bool,
667    ) where
668        F: PrimeField + FromUniformBytes<64> + Ord,
669    {
670        let input = input_1.to_vec();
671        assert!(trim_size <= input.len());
672        let circuit = TestCircuit::<F, M, A> {
673            input_1: Value::known(input.clone()),
674            input_2: input[trim_size..].to_vec(),
675            opts: TestOpts::Trim { trim_size },
676        };
677
678        let k = 14;
679
680        MockProver::run(k, &circuit, vec![vec![], vec![]]).unwrap().assert_satisfied();
681
682        if cost_model {
683            circuit_to_json(
684                "Vector trim beginning.",
685                format!("Vector trim_beginning with M={M}").as_str(),
686                circuit,
687            );
688        }
689    }
690
691    #[test]
692    fn vector_eq() {
693        type F = midnight_curves::Fq;
694
695        // Create a random number generator
696        let mut rng = ChaCha12Rng::seed_from_u64(0xdeadcafe);
697        let inputs = (0..100).map(|_| F::random(&mut rng)).collect::<Vec<_>>();
698
699        // Equal vectors, different padding.
700        run_eq_vec_test::<_, 128, 2>(&inputs, &inputs, true, true, true);
701        run_eq_vec_test::<_, 128, 3>(&inputs, &inputs, true, true, false);
702
703        // Equal vectors, equal padding.
704        run_eq_vec_test::<_, 128, 2>(&inputs, &inputs, true, false, false);
705
706        // Equal data, different length.
707        run_eq_vec_test::<_, 128, 2>(&inputs[..80], &inputs[..81], false, false, false);
708
709        // Different data.
710        run_eq_vec_test::<_, 128, 2>(
711            &[&[F::ZERO], &inputs[..80]].concat(),
712            &[&[F::ONE], &inputs[..80]].concat(),
713            false,
714            false,
715            false,
716        );
717    }
718
719    #[test]
720    fn vector_limits() {
721        type F = midnight_curves::Fq;
722
723        // Create a random number generator
724        let mut rng = ChaCha12Rng::seed_from_u64(0xdeadcafe);
725        let inputs = (0..100).map(|_| F::random(&mut rng)).collect::<Vec<_>>();
726
727        // Test different alignments.
728        run_limit_vec_test::<_, 128, 1>(&inputs, true);
729        run_limit_vec_test::<_, 128, 2>(&inputs, false);
730        run_limit_vec_test::<_, 128, 3>(&inputs, false);
731        run_limit_vec_test::<_, 128, 4>(&inputs, false);
732        run_limit_vec_test::<_, 128, 5>(&inputs, false);
733
734        // Test edge cases.
735        run_limit_vec_test::<_, 64, 2>(&inputs[..64], false);
736        run_limit_vec_test::<F, 64, 2>(&[], false);
737    }
738
739    #[test]
740    fn vector_padding_flags() {
741        type F = midnight_curves::Fq;
742
743        // Create a random number generator
744        let mut rng = ChaCha12Rng::seed_from_u64(0xdeadcafe);
745        let inputs = (0..100).map(|_| F::random(&mut rng)).collect::<Vec<_>>();
746
747        run_padding_flags_test::<_, 128, 1>(&inputs, true);
748        run_padding_flags_test::<_, 128, 2>(&inputs, false);
749        run_padding_flags_test::<_, 128, 3>(&inputs, false);
750        run_padding_flags_test::<_, 128, 64>(&inputs, false);
751        run_padding_flags_test::<F, 128, 64>(&[], false);
752        run_padding_flags_test::<F, 64, 16>(&inputs[..64], false);
753    }
754
755    #[test]
756    fn vector_trim_beginning() {
757        type F = midnight_curves::Fq;
758
759        // Create a random number generator
760        let mut rng = ChaCha12Rng::seed_from_u64(0xdeadcafe);
761        let inputs = (0..100).map(|_| F::random(&mut rng)).collect::<Vec<_>>();
762
763        // Test different alignments (under A).
764        run_trim_vec_test::<_, 128, 64>(&[F::ONE, F::ONE], 1, true);
765        run_trim_vec_test::<_, 128, 32>(&inputs, 0, false);
766        run_trim_vec_test::<_, 128, 32>(&inputs, 1, false);
767        run_trim_vec_test::<_, 128, 32>(&inputs, 2, false);
768        run_trim_vec_test::<_, 128, 32>(&inputs, 3, false);
769        run_trim_vec_test::<_, 128, 32>(&inputs, 4, false);
770        run_trim_vec_test::<_, 128, 32>(&inputs, 5, false);
771        run_trim_vec_test::<_, 128, 32>(&inputs, 30, false);
772        run_trim_vec_test::<_, 128, 32>(&inputs, 31, false);
773
774        // Above or equal to A.
775        run_trim_vec_test::<_, 128, 3>(&inputs, 3, false);
776        run_trim_vec_test::<_, 128, 3>(&inputs, 4, false);
777        run_trim_vec_test::<_, 128, 3>(&inputs, 5, false);
778        run_trim_vec_test::<_, 128, 3>(&inputs, 6, false);
779        run_trim_vec_test::<_, 128, 3>(&inputs, 10, false);
780        run_trim_vec_test::<_, 128, 3>(&inputs, 20, false);
781        run_trim_vec_test::<_, 128, 3>(&inputs, 30, false);
782        run_trim_vec_test::<_, 128, 3>(&inputs, 40, false);
783
784        // Edge case: offset of original vector = 0;
785        run_trim_vec_test::<_, 128, 32>(&inputs[..96], 23, false);
786
787        // Edge case: full vector;
788        run_trim_vec_test::<_, 64, 32>(&inputs[..64], 20, false);
789
790        // Edge case: full vector, trim all elements.
791        run_trim_vec_test::<_, 64, 32>(&inputs[..64], 64, false);
792
793        // The particular case of the credentials:
794        run_trim_vec_test::<_, 128, 64>(&inputs, 39, false);
795    }
796}