Skip to main content

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}