midnight_circuits/instructions/
vector.rs

1// This file is part of MIDNIGHT-ZK.
2// Copyright (C) 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 midnight_proofs::{
21    circuit::{Layouter, Value},
22    plonk::Error,
23};
24
25use crate::{
26    field::AssignedNative,
27    types::AssignedBit,
28    vec::{AssignedVector, Vectorizable},
29    CircuitField,
30};
31
32/// Indicator of the number of filler elements at the beginning and end of an
33/// assigned vector's buffer, as returned by `get_limits`.
34pub type VectorBounds<F> = (AssignedNative<F>, AssignedNative<F>);
35
36/// Instructions for Vector manipulation..
37pub trait VectorInstructions<F, T, const M: usize, const A: usize>
38where
39    F: CircuitField,
40    T: Vectorizable,
41    T::Element: Copy,
42{
43    /// Changes the size of an AssignedVector from M to L.
44    ///
45    /// # Panics
46    ///
47    /// If `L <= M` or `A` does not divide `L`.
48    fn resize<const L: usize>(
49        &self,
50        layouter: &mut impl Layouter<F>,
51        input: AssignedVector<F, T, M, A>,
52    ) -> Result<AssignedVector<F, T, L, A>, Error>;
53
54    /// Assigns vector with a chosen filler value.
55    ///
56    /// # Panics
57    ///
58    /// If |value| > M.
59    fn assign_with_filler(
60        &self,
61        layouter: &mut impl Layouter<F>,
62        value: Value<Vec<T::Element>>,
63        filler: Option<T::Element>,
64    ) -> Result<AssignedVector<F, T, M, A>, Error>;
65
66    /// Trims `n_elems` elements from the beginning of the vector.
67    /// The trimmed elements will not be changed by filler elements,
68    /// they will remain in the buffer but not as part of the effective payload.
69    ///
70    /// # Unsatisfiable Circuit
71    ///
72    /// If the vector length < `n_elems`.
73    fn trim_beginning(
74        &self,
75        layouter: &mut impl Layouter<F>,
76        input: &AssignedVector<F, T, M, A>,
77        n_elems: usize,
78    ) -> Result<AssignedVector<F, T, M, A>, Error>;
79
80    /// Returns a vector of AssignedBits signaling the cells that represent
81    /// padding with a 1, and the ones that represent payload data with a 0.
82    /// Also returns the (start, end) limits of the data in the buffer, since
83    /// they are computed internally.
84    #[allow(clippy::type_complexity)]
85    fn padding_flag(
86        &self,
87        layouter: &mut impl Layouter<F>,
88        input: &AssignedVector<F, T, M, A>,
89    ) -> Result<(Box<[AssignedBit<F>; M]>, VectorBounds<F>), Error>;
90
91    /// Returns the first and last positions of data in the buffer.
92    fn get_limits(
93        &self,
94        layouter: &mut impl Layouter<F>,
95        input: &AssignedVector<F, T, M, A>,
96    ) -> Result<VectorBounds<F>, Error>;
97}
midnight_circuits/instructions/vector.rs

midnight_circuits/instructions/
vector.rs
