Skip to content

Commit

Permalink
Refactor VarLenBytes
Browse files Browse the repository at this point in the history
Add VarLenBytesVec and FixLenBytes
Fix tests
  • Loading branch information
nyunyunyunyu committed Aug 17, 2023
1 parent bfa3e63 commit 339bc40
Show file tree
Hide file tree
Showing 5 changed files with 224 additions and 108 deletions.
7 changes: 6 additions & 1 deletion halo2-base/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ rayon = "1.7"
serde = { version = "1.0", features = ["derive"] }
serde_json = "1.0"
log = "0.4"
getset = "0.1.2"

# Use Axiom's custom halo2 monorepo for faster proving when feature = "halo2-axiom" is on
halo2_proofs_axiom = { git = "https://github.com/axiom-crypto/halo2.git", package = "halo2_proofs", optional = true }
Expand Down Expand Up @@ -45,7 +46,11 @@ mimalloc = { version = "0.1", default-features = false, optional = true }
[features]
default = ["halo2-axiom", "display"]
asm = ["halo2_proofs_axiom?/asm"]
dev-graph = ["halo2_proofs?/dev-graph", "halo2_proofs_axiom?/dev-graph", "plotters"]
dev-graph = [
"halo2_proofs?/dev-graph",
"halo2_proofs_axiom?/dev-graph",
"plotters",
]
halo2-pse = ["halo2_proofs/circuit-params"]
halo2-axiom = ["halo2_proofs_axiom"]
display = []
Expand Down
84 changes: 62 additions & 22 deletions halo2-base/src/safe_types/bytes.rs
Original file line number Diff line number Diff line change
@@ -1,51 +1,91 @@
#![allow(clippy::len_without_is_empty)]
use crate::AssignedValue;

use super::{SafeByte, ScalarField};

use getset::Getters;

/// Represents a variable length byte array in circuit.
///
/// Each element is guaranteed to be a byte, given by type [`SafeByte`].
/// To represent a variable length array, we must know the maximum possible length `MAX_LEN` the array could be -- this is some additional context the user must provide.
/// Then we right pad the array with 0s to the maximum length (we do **not** constrain that these paddings must be 0s).
#[derive(Debug, Clone)]
#[derive(Debug, Clone, Getters)]
pub struct VarLenBytes<F: ScalarField, const MAX_LEN: usize> {
/// The byte array, right padded with 0s
pub bytes: [SafeByte<F>; MAX_LEN],
/// The byte array, right padded
#[getset(get = "pub")]
bytes: [SafeByte<F>; MAX_LEN],
/// Witness representing the actual length of the byte array. Upon construction, this is range checked to be at most `MAX_LEN`
pub var_len: AssignedValue<F>,
#[getset(get = "pub")]
len: AssignedValue<F>,
}

impl<F: ScalarField, const MAX_LEN: usize> VarLenBytes<F, MAX_LEN> {
fn new(bytes: [SafeByte<F>; MAX_LEN], var_len: AssignedValue<F>) -> Self {
Self { bytes, var_len }
// VarLenBytes can be only created by SafeChip.
pub(super) fn new(bytes: [SafeByte<F>; MAX_LEN], len: AssignedValue<F>) -> Self {
assert!(
len.value().le(&F::from_u128(MAX_LEN as u128)),
"Invalid length which exceeds MAX_LEN {}",
MAX_LEN
);
Self { bytes, len }
}

/// Returns the maximum length of the byte array.
pub fn max_len(&self) -> usize {
MAX_LEN
}
}

impl<F: ScalarField, const MAX_LEN: usize> AsRef<[SafeByte<F>]> for VarLenBytes<F, MAX_LEN> {
fn as_ref(&self) -> &[SafeByte<F>] {
&self.bytes
}
}

impl<F: ScalarField, const MAX_LEN: usize> AsMut<[SafeByte<F>]> for VarLenBytes<F, MAX_LEN> {
fn as_mut(&mut self) -> &mut [SafeByte<F>] {
&mut self.bytes
}
}

/// Represents a variable length byte array in circuit.
/// Represents a variable length byte array in circuit. Not encourged to use because `MAX_LEN` cannot be verified at compile time.
///
/// Each element is guaranteed to be a byte, given by type [`SafeByte`].
/// To represent a variable length array, we must know the maximum possible length `MAX_LEN` the array could be -- this is some additional context the user must provide.
/// Then we right pad the array with 0s to the maximum length (we do **not** constrain that these paddings must be 0s).
#[derive(Debug, Clone)]
#[derive(Debug, Clone, Getters)]
pub struct VarLenBytesVec<F: ScalarField> {
/// The byte array, right padded with 0s
/// The byte array, right padded
#[getset(get = "pub")]
bytes: Vec<SafeByte<F>>,
/// Witness representing the actual length of the byte array. Upon construction, this is range checked to be at most `MAX_LEN`
pub var_len: AssignedValue<F>,
#[getset(get = "pub")]
len: AssignedValue<F>,
}

impl<F: ScalarField> VarLenBytesVec<F> {
// VarLenBytesVec can be only created by SafeChip.
pub(super) fn new(bytes: Vec<SafeByte<F>>, len: AssignedValue<F>, max_len: usize) -> Self {
assert!(
len.value().le(&F::from_u128(max_len as u128)),
"Invalid length which exceeds MAX_LEN {}",
max_len
);
assert!(bytes.len() == max_len, "bytes is not padded correctly");
Self { bytes, len }
}

/// Returns the maximum length of the byte array.
pub fn max_len(&self) -> usize {
self.bytes.len()
}
}

/// Represents a fixed length byte array in circuit.
#[derive(Debug, Clone, Getters)]
pub struct FixLenBytes<F: ScalarField, const LEN: usize> {
/// The byte array
#[getset(get = "pub")]
bytes: [SafeByte<F>; LEN],
}

impl<F: ScalarField, const LEN: usize> FixLenBytes<F, LEN> {
// FixLenBytes can be only created by SafeChip.
pub(super) fn new(bytes: [SafeByte<F>; LEN]) -> Self {
Self { bytes }
}

/// Returns the length of the byte array.
pub fn len(&self) -> usize {
LEN
}
}
55 changes: 45 additions & 10 deletions halo2-base/src/safe_types/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ pub use crate::{
flex_gate::GateInstructions,
range::{RangeChip, RangeInstructions},
},
safe_types::VarLenBytes,
utils::ScalarField,
AssignedValue, Context,
QuantumCell::{self, Constant, Existing, Witness},
Expand All @@ -16,6 +17,7 @@ mod bytes;
mod primitives;

pub use bytes::*;
use itertools::Itertools;
pub use primitives::*;

#[cfg(test)]
Expand Down Expand Up @@ -185,21 +187,54 @@ impl<'a, F: ScalarField> SafeTypeChip<'a, F> {
SafeByte(input)
}

/// Converts a vector of AssignedValue(treated as little-endian) to VariableAssignedBytes.
/// Converts a slice of AssignedValue(treated as little-endian) to VarLenBytes.
///
/// * ctx: Circuit [Context]<F> to assign witnesses to.
/// * inputs: Vector of [RawAssignedValues]<F> representing the byte array.
/// * var_len: [AssignedValue]<F> witness representing the variable elements within the byte array from 0..=var_len.
/// * max_var_len: [usize] representing the maximum length of the byte array and the number of elements it must contain.
pub fn raw_var_bytes_to<const MAX_VAR_LEN: usize>(
/// * inputs: Slice representing the byte array.
/// * len: [AssignedValue]<F> witness representing the variable elements within the byte array from 0..=len.
/// * MAX_LEN: [usize] representing the maximum length of the byte array and the number of elements it must contain.
pub fn raw_to_var_len_bytes<const MAX_LEN: usize>(
&self,
ctx: &mut Context<F>,
inputs: [AssignedValue<F>; MAX_LEN],
len: AssignedValue<F>,
) -> VarLenBytes<F, MAX_LEN> {
self.range_chip.check_less_than_safe(ctx, len, MAX_LEN as u64);
VarLenBytes::<F, MAX_LEN>::new(inputs.map(|input| self.assert_byte(ctx, input)), len)
}

/// Converts a vector of AssignedValue(treated as little-endian) to VarLenBytesVec. Not encourged to use because `MAX_LEN` cannot be verified at compile time.
///
/// * ctx: Circuit [Context]<F> to assign witnesses to.
/// * inputs: Vector representing the byte array.
/// * len: [AssignedValue]<F> witness representing the variable elements within the byte array from 0..=len.
/// * max_len: [usize] representing the maximum length of the byte array and the number of elements it must contain.
pub fn raw_to_var_len_bytes_vec(
&self,
ctx: &mut Context<F>,
inputs: RawAssignedValues<F>,
var_len: AssignedValue<F>,
) -> VariableByteArray<F, MAX_VAR_LEN> {
self.add_bytes_constraints(ctx, &inputs, BITS_PER_BYTE * MAX_VAR_LEN);
self.range_chip.check_less_than_safe(ctx, var_len, MAX_VAR_LEN as u64);
VariableByteArray::<F, MAX_VAR_LEN>::new(inputs, var_len)
len: AssignedValue<F>,
max_len: usize,
) -> VarLenBytesVec<F> {
self.range_chip.check_less_than_safe(ctx, len, max_len as u64);
VarLenBytesVec::<F>::new(
inputs.iter().map(|input| self.assert_byte(ctx, *input)).collect_vec(),
len,
max_len,
)
}

/// Converts a slice of AssignedValue(treated as little-endian) to FixLenBytes.
///
/// * ctx: Circuit [Context]<F> to assign witnesses to.
/// * inputs: Slice representing the byte array.
/// * LEN: length of the byte array.
pub fn raw_to_fix_len_bytes<const LEN: usize>(
&self,
ctx: &mut Context<F>,
inputs: [AssignedValue<F>; LEN],
) -> FixLenBytes<F, LEN> {
FixLenBytes::<F, LEN>::new(inputs.map(|input| self.assert_byte(ctx, input)))
}

fn add_bytes_constraints(
Expand Down
4 changes: 2 additions & 2 deletions halo2-base/src/safe_types/tests/mod.rs
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
pub (crate) mod var_byte_array;
pub (crate) mod safe_type;
pub(crate) mod safe_type;
pub(crate) mod var_byte_array;
Loading

0 comments on commit 339bc40

Please sign in to comment.