midnight_circuits/vec/
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
14use std::ops::Range;
15
16use midnight_proofs::circuit::Value;
17
18use crate::{
19    field::AssignedNative,
20    types::{AssignedByte, InnerValue},
21    CircuitField,
22};
23
24/// A variable-length vector of elements of type T, with size bound M.
25/// - `len` is the (potentially secret) effective length of the vector, its
26///   value is guaranteed to be in the range `[0, M]`.
27/// - `buffer` is the padded payload of this vector; it contains the effective
28///   data of the vector as well as filler values, which are UNCONSTRAINED.
29///
30/// The effective payload in the data is aligned in A sized chunks. This
31/// enables more efficient implementations of instructions like hashing
32/// over this type. As a result of this alignment, the data may contain filler
33/// values before and after the effective payload. The padding in front of
34/// the payload will always be 0 mod A, so that the payload begins aligned in A
35/// sized chunks. The padding at the end of the payload will have a size in
36/// [0, A) such that | front_pad | + | payload | + | back_pad | = M.
37///
38/// **Invariant: `M` must be a multiple of `A`** (and `A > 0`, `M >= A`).
39/// Several operations (`padding_flag`, `get_limits`, hashing, …) rely on this
40/// to guarantee that the buffer decomposes into exactly `M / A` full chunks
41/// and that a full-capacity vector (`len == M`) can always be placed without
42/// overflow. This is enforced by the entry points
43/// [`assign_with_filler`](crate::instructions::VectorInstructions::assign_with_filler) and
44/// [`assign`](crate::instructions::AssignmentInstructions::assign).
45#[derive(Clone, Debug)]
46pub struct AssignedVector<F: CircuitField, T: Vectorizable, const M: usize, const A: usize> {
47    /// Padded payload of the vector. Boxed to keep large buffers
48    /// off the stack.
49    pub(crate) buffer: Box<[T; M]>,
50
51    /// Effective length of the vector.
52    pub(crate) len: AssignedNative<F>,
53}
54
55/// Returns the range where the data should be placed in the buffer.
56pub fn get_lims<const M: usize, const A: usize>(len: usize) -> Range<usize> {
57    let final_pad_len = (A - (len % A)) % A;
58    M - len - final_pad_len..M - final_pad_len
59}
60
61impl<F: CircuitField, const M: usize, T: Vectorizable, const A: usize> InnerValue
62    for AssignedVector<F, T, M, A>
63{
64    type Element = Vec<T::Element>;
65
66    fn value(&self) -> Value<Self::Element> {
67        let data = Value::<Vec<T::Element>>::from_iter(self.buffer.iter().map(|v| v.value()));
68        let idxs: Value<_> = self.len.value().map(|len| {
69            let len: usize = len.to_biguint().try_into().unwrap();
70
71            let end_pad = (A - (len % A)) % A;
72            (M - len - end_pad, M - end_pad)
73        });
74        data.zip(idxs).map(|(data, idxs)| data[idxs.0..idxs.1].to_vec())
75    }
76}
77
78/// Trait for the individual elements of an AssignedVector.
79pub trait Vectorizable: InnerValue {
80    /// Value to fill the space in the buffer that is not occupied with vector
81    /// data.
82    const FILLER: Self::Element;
83}
84
85impl<F: CircuitField> Vectorizable for AssignedNative<F> {
86    const FILLER: F = F::ZERO;
87}
88
89impl<F: CircuitField> Vectorizable for AssignedByte<F> {
90    const FILLER: u8 = 0u8;
91}
midnight_circuits/vec/vector.rs

midnight_circuits/vec/
vector.rs
