midnight_circuits/instructions/vector.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
14//! Vector manipulation instructions interface.
15//!
16//! The trait is parameterized by the type `T` of elements contained in the
17//! vector, as well as 2 constants: its maximum size `M` and its chunk alignment
18//! value `A`.
19
20use ff::PrimeField;
21use midnight_proofs::{
22 circuit::{Layouter, Value},
23 plonk::Error,
24};
25
26use crate::{
27 field::AssignedNative,
28 types::AssignedBit,
29 vec::{AssignedVector, Vectorizable},
30};
31
32/// Instructions for Vector manipulation..
33pub trait VectorInstructions<F, T, const M: usize, const A: usize>
34where
35 F: PrimeField,
36 T: Vectorizable,
37 T::Element: Copy,
38{
39 /// Changes the size of an AssignedVector from M to L.
40 ///
41 /// # Panics
42 ///
43 /// If `L <= M` or `A` does not divide `L`.
44 fn resize<const L: usize>(
45 &self,
46 layouter: &mut impl Layouter<F>,
47 input: AssignedVector<F, T, M, A>,
48 ) -> Result<AssignedVector<F, T, L, A>, Error>;
49
50 /// Assigns vector with a chosen filler value.
51 ///
52 /// # Panics
53 ///
54 /// If |value| > M.
55 fn assign_with_filler(
56 &self,
57 layouter: &mut impl Layouter<F>,
58 value: Value<Vec<T::Element>>,
59 filler: Option<T::Element>,
60 ) -> Result<AssignedVector<F, T, M, A>, Error>;
61
62 /// Trims `n_elems` elements from the beginning of the vector.
63 /// The trimmed elements will not be changed by filler elements,
64 /// they will remain in the buffer but not as part of the effective payload.
65 ///
66 /// # Unsatisfiable Circuit
67 ///
68 /// If the vector length < `n_elems`.
69 fn trim_beginning(
70 &self,
71 layouter: &mut impl Layouter<F>,
72 input: &AssignedVector<F, T, M, A>,
73 n_elems: usize,
74 ) -> Result<AssignedVector<F, T, M, A>, Error>;
75
76 /// Returns a vector of AssignedBits signaling the cells that represent
77 /// padding with a 1, and the ones that represent payload data with a 0.
78 fn padding_flag(
79 &self,
80 layouter: &mut impl Layouter<F>,
81 input: &AssignedVector<F, T, M, A>,
82 ) -> Result<[AssignedBit<F>; M], Error>;
83
84 /// Returns the first and last positions of data in the buffer.
85 fn get_limits(
86 &self,
87 layouter: &mut impl Layouter<F>,
88 input: &AssignedVector<F, T, M, A>,
89 ) -> Result<(AssignedNative<F>, AssignedNative<F>), Error>;
90}