diff --git a/.gitignore b/.gitignore index 65983083..eb915932 100644 --- a/.gitignore +++ b/.gitignore @@ -8,6 +8,10 @@ Cargo.lock # These are backup files generated by rustfmt **/*.rs.bk + +# Local IDE configs +.idea/ +.vscode/ ======= /target diff --git a/halo2-base/Cargo.toml b/halo2-base/Cargo.toml index 183fb60f..1287d01d 100644 --- a/halo2-base/Cargo.toml +++ b/halo2-base/Cargo.toml @@ -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 } @@ -50,7 +51,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 = [] diff --git a/halo2-base/src/safe_types/bytes.rs b/halo2-base/src/safe_types/bytes.rs new file mode 100644 index 00000000..d85dc9bc --- /dev/null +++ b/halo2-base/src/safe_types/bytes.rs @@ -0,0 +1,90 @@ +#![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, Getters)] +pub struct VarLenBytes { + /// The byte array, right padded + #[getset(get = "pub")] + bytes: [SafeByte; MAX_LEN], + /// Witness representing the actual length of the byte array. Upon construction, this is range checked to be at most `MAX_LEN` + #[getset(get = "pub")] + len: AssignedValue, +} + +impl VarLenBytes { + // VarLenBytes can be only created by SafeChip. + pub(super) fn new(bytes: [SafeByte; MAX_LEN], len: AssignedValue) -> Self { + assert!( + len.value().le(&F::from(MAX_LEN as u64)), + "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 + } +} + +/// Represents a variable length byte array in circuit. Not encouraged 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 provided when constructing and `bytes.len()` == `MAX_LEN` is enforced. +/// 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, Getters)] +pub struct VarLenBytesVec { + /// The byte array, right padded + #[getset(get = "pub")] + bytes: Vec>, + /// Witness representing the actual length of the byte array. Upon construction, this is range checked to be at most `MAX_LEN` + #[getset(get = "pub")] + len: AssignedValue, +} + +impl VarLenBytesVec { + // VarLenBytesVec can be only created by SafeChip. + pub(super) fn new(bytes: Vec>, len: AssignedValue, 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 { + /// The byte array + #[getset(get = "pub")] + bytes: [SafeByte; LEN], +} + +impl FixLenBytes { + // FixLenBytes can be only created by SafeChip. + pub(super) fn new(bytes: [SafeByte; LEN]) -> Self { + Self { bytes } + } + + /// Returns the length of the byte array. + pub fn len(&self) -> usize { + LEN + } +} diff --git a/halo2-base/src/safe_types/mod.rs b/halo2-base/src/safe_types/mod.rs index 5a18c158..e4624049 100644 --- a/halo2-base/src/safe_types/mod.rs +++ b/halo2-base/src/safe_types/mod.rs @@ -3,11 +3,22 @@ pub use crate::{ flex_gate::GateInstructions, range::{RangeChip, RangeInstructions}, }, + safe_types::VarLenBytes, utils::ScalarField, AssignedValue, Context, QuantumCell::{self, Constant, Existing, Witness}, }; -use std::cmp::{max, min}; +use std::{ + borrow::{Borrow, BorrowMut}, + cmp::{max, min}, +}; + +mod bytes; +mod primitives; + +pub use bytes::*; +use itertools::Itertools; +pub use primitives::*; #[cfg(test)] pub mod tests; @@ -54,20 +65,26 @@ impl Self { value: raw_values } } - /// Return values in littile-endian. - pub fn value(&self) -> &RawAssignedValues { + /// Return values in little-endian. + pub fn value(&self) -> &[AssignedValue] { &self.value } } +impl AsRef<[AssignedValue]> + for SafeType +{ + fn as_ref(&self) -> &[AssignedValue] { + self.value() + } +} + /// Represent TOTAL_BITS with the least number of AssignedValue. /// (2^(F::NUM_BITS) - 1) might not be a valid value for F. e.g. max value of F is a prime in [2^(F::NUM_BITS-1), 2^(F::NUM_BITS) - 1] #[allow(type_alias_bounds)] type CompactSafeType = - SafeType; + SafeType; -/// SafeType for bool. -pub type SafeBool = CompactSafeType; /// SafeType for uint8. pub type SafeUint8 = CompactSafeType; /// SafeType for uint16. @@ -98,7 +115,7 @@ impl<'a, F: ScalarField> SafeTypeChip<'a, F> { Self { range_chip } } - /// Convert a vector of AssignedValue(treated as little-endian) to a SafeType. + /// Convert a vector of AssignedValue (treated as little-endian) to a SafeType. /// The number of bytes of inputs must equal to the number of bytes of outputs. /// This function also add contraints that a AssignedValue in inputs must be in the range of a byte. pub fn raw_bytes_to( @@ -134,6 +151,123 @@ impl<'a, F: ScalarField> SafeTypeChip<'a, F> { SafeType::::new(value) } + /// Constrains that the `input` is a boolean value (either 0 or 1) and wraps it in [`SafeBool`]. + pub fn assert_bool(&self, ctx: &mut Context, input: AssignedValue) -> SafeBool { + self.range_chip.gate().assert_bit(ctx, input); + SafeBool(input) + } + + /// Load a boolean value as witness and constrain it is either 0 or 1. + pub fn load_bool(&self, ctx: &mut Context, input: bool) -> SafeBool { + let input = ctx.load_witness(F::from(input)); + self.assert_bool(ctx, input) + } + + /// Unsafe method that directly converts `input` to [`SafeBool`] **without any checks**. + /// This should **only** be used if an external library needs to convert their types to [`SafeBool`]. + pub fn unsafe_to_bool(&self, input: AssignedValue) -> SafeBool { + SafeBool(input) + } + + /// Constrains that the `input` is a byte value and wraps it in [`SafeByte`]. + pub fn assert_byte(&self, ctx: &mut Context, input: AssignedValue) -> SafeByte { + self.range_chip.range_check(ctx, input, BITS_PER_BYTE); + SafeByte(input) + } + + /// Load a boolean value as witness and constrain it is either 0 or 1. + pub fn load_byte(&self, ctx: &mut Context, input: u8) -> SafeByte { + let input = ctx.load_witness(F::from(input as u64)); + self.assert_byte(ctx, input) + } + + /// Unsafe method that directly converts `input` to [`SafeByte`] **without any checks**. + /// This should **only** be used if an external library needs to convert their types to [`SafeByte`]. + pub fn unsafe_to_byte(input: AssignedValue) -> SafeByte { + SafeByte(input) + } + + /// Unsafe method that directly converts `inputs` to [`VarLenBytes`] **without any checks**. + /// This should **only** be used if an external library needs to convert their types to [`SafeByte`]. + pub fn unsafe_to_var_len_bytes( + inputs: [AssignedValue; MAX_LEN], + len: AssignedValue, + ) -> VarLenBytes { + VarLenBytes::::new(inputs.map(|input| Self::unsafe_to_byte(input)), len) + } + + /// Unsafe method that directly converts `inputs` to [`VarLenBytesVec`] **without any checks**. + /// This should **only** be used if an external library needs to convert their types to [`SafeByte`]. + pub fn unsafe_to_var_len_bytes_vec( + inputs: RawAssignedValues, + len: AssignedValue, + max_len: usize, + ) -> VarLenBytesVec { + VarLenBytesVec::::new( + inputs.iter().map(|input| Self::unsafe_to_byte(*input)).collect_vec(), + len, + max_len, + ) + } + + /// Unsafe method that directly converts `inputs` to [`FixLenBytes`] **without any checks**. + /// This should **only** be used if an external library needs to convert their types to [`SafeByte`]. + pub fn unsafe_to_fix_len_bytes( + inputs: [AssignedValue; MAX_LEN], + ) -> FixLenBytes { + FixLenBytes::::new(inputs.map(|input| Self::unsafe_to_byte(input))) + } + + /// Converts a slice of AssignedValue(treated as little-endian) to VarLenBytes. + /// + /// * ctx: Circuit [Context] to assign witnesses to. + /// * inputs: Slice representing the byte array. + /// * len: [AssignedValue] 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( + &self, + ctx: &mut Context, + inputs: [AssignedValue; MAX_LEN], + len: AssignedValue, + ) -> VarLenBytes { + self.range_chip.check_less_than_safe(ctx, len, MAX_LEN as u64); + VarLenBytes::::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] to assign witnesses to. + /// * inputs: Vector representing the byte array. + /// * len: [AssignedValue] 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, + inputs: RawAssignedValues, + len: AssignedValue, + max_len: usize, + ) -> VarLenBytesVec { + self.range_chip.check_less_than_safe(ctx, len, max_len as u64); + VarLenBytesVec::::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] to assign witnesses to. + /// * inputs: Slice representing the byte array. + /// * LEN: length of the byte array. + pub fn raw_to_fix_len_bytes( + &self, + ctx: &mut Context, + inputs: [AssignedValue; LEN], + ) -> FixLenBytes { + FixLenBytes::::new(inputs.map(|input| self.assert_byte(ctx, input))) + } + fn add_bytes_constraints( &self, ctx: &mut Context, @@ -148,6 +282,6 @@ impl<'a, F: ScalarField> SafeTypeChip<'a, F> { } } - // TODO: Add comprasion. e.g. is_less_than(SafeUint8, SafeUint8) -> SafeBool + // TODO: Add comparison. e.g. is_less_than(SafeUint8, SafeUint8) -> SafeBool // TODO: Add type castings. e.g. uint256 -> bytes32/uint32 -> uint64 } diff --git a/halo2-base/src/safe_types/primitives.rs b/halo2-base/src/safe_types/primitives.rs new file mode 100644 index 00000000..7bdeb209 --- /dev/null +++ b/halo2-base/src/safe_types/primitives.rs @@ -0,0 +1,47 @@ +use super::*; +/// SafeType for bool (1 bit). +/// +/// This is a separate struct from [`CompactSafeType`] with the same behavior. Because +/// we know only one [`AssignedValue`] is needed to hold the boolean value, we avoid +/// using [`CompactSafeType`] to avoid the additional heap allocation from a length 1 vector. +#[derive(Clone, Copy, Debug)] +pub struct SafeBool(pub(super) AssignedValue); + +/// SafeType for byte (8 bits). +/// +/// This is a separate struct from [`CompactSafeType`] with the same behavior. Because +/// we know only one [`AssignedValue`] is needed to hold the boolean value, we avoid +/// using [`CompactSafeType`] to avoid the additional heap allocation from a length 1 vector. +#[derive(Clone, Copy, Debug)] +pub struct SafeByte(pub(super) AssignedValue); + +macro_rules! safe_primitive_impls { + ($SafePrimitive:ty) => { + impl AsRef> for $SafePrimitive { + fn as_ref(&self) -> &AssignedValue { + &self.0 + } + } + + impl AsMut> for $SafePrimitive { + fn as_mut(&mut self) -> &mut AssignedValue { + &mut self.0 + } + } + + impl Borrow> for $SafePrimitive { + fn borrow(&self) -> &AssignedValue { + &self.0 + } + } + + impl BorrowMut> for $SafePrimitive { + fn borrow_mut(&mut self) -> &mut AssignedValue { + &mut self.0 + } + } + }; +} + +safe_primitive_impls!(SafeBool); +safe_primitive_impls!(SafeByte); diff --git a/halo2-base/src/safe_types/tests/bytes.rs b/halo2-base/src/safe_types/tests/bytes.rs new file mode 100644 index 00000000..a4b76779 --- /dev/null +++ b/halo2-base/src/safe_types/tests/bytes.rs @@ -0,0 +1,196 @@ +use crate::{ + gates::{ + builder::{GateThreadBuilder, RangeCircuitBuilder}, + RangeChip, + }, + halo2_proofs::{ + dev::MockProver, + halo2curves::bn256::{Bn256, Fr}, + plonk::{keygen_pk, keygen_vk}, + poly::kzg::commitment::ParamsKZG, + }, + safe_types::SafeTypeChip, + utils::testing::{base_test, check_proof, gen_proof}, + Context, +}; +use rand::rngs::OsRng; +use std::vec; + +// =========== Utilies =============== +fn mock_circuit_test, SafeTypeChip<'_, Fr>)>(mut f: FM) { + let mut builder = GateThreadBuilder::mock(); + let range = RangeChip::default(8); + let safe = SafeTypeChip::new(&range); + let ctx = builder.main(0); + f(ctx, safe); + let mut params = builder.config(10, Some(9)); + params.lookup_bits = Some(8); + let circuit = RangeCircuitBuilder::mock(builder, params); + MockProver::run(10 as u32, &circuit, vec![]).unwrap().assert_satisfied(); +} + +// =========== Mock Prover =========== + +// Circuit Satisfied for valid inputs +#[test] +fn pos_var_len_bytes() { + base_test().k(10).lookup_bits(8).run(|ctx, range| { + let safe = SafeTypeChip::new(&range); + let fake_bytes = ctx.assign_witnesses( + vec![255u64, 255u64, 255u64, 255u64].into_iter().map(Fr::from).collect::>(), + ); + let len = ctx.load_witness(Fr::from(3u64)); + safe.raw_to_var_len_bytes::<4>(ctx, fake_bytes.try_into().unwrap(), len); + }); +} + +// Checks circuit is unsatisfied for AssignedValue's are not in range 0..256 +#[test] +#[should_panic(expected = "circuit was not satisfied")] +fn neg_var_len_bytes_witness_values_not_bytes() { + mock_circuit_test(|ctx: &mut Context, safe: SafeTypeChip<'_, Fr>| { + let len = ctx.load_witness(Fr::from(3u64)); + let fake_bytes = ctx.assign_witnesses( + vec![500u64, 500u64, 500u64, 500u64].into_iter().map(Fr::from).collect::>(), + ); + safe.raw_to_var_len_bytes::<4>(ctx, fake_bytes.try_into().unwrap(), len); + }); +} + +//Checks assertion len < max_len +#[test] +#[should_panic] +fn neg_var_len_bytes_len_less_than_max_len() { + mock_circuit_test(|ctx: &mut Context, safe: SafeTypeChip<'_, Fr>| { + let len = ctx.load_witness(Fr::from(5u64)); + let fake_bytes = ctx.assign_witnesses( + vec![500u64, 500u64, 500u64, 500u64].into_iter().map(Fr::from).collect::>(), + ); + safe.raw_to_var_len_bytes::<4>(ctx, fake_bytes.try_into().unwrap(), len); + }); +} + +// Circuit Satisfied for valid inputs +#[test] +fn pos_var_len_bytes_vec() { + base_test().k(10).lookup_bits(8).run(|ctx, range| { + let safe = SafeTypeChip::new(&range); + let fake_bytes = ctx.assign_witnesses( + vec![255u64, 255u64, 255u64, 255u64].into_iter().map(Fr::from).collect::>(), + ); + let len = ctx.load_witness(Fr::from(3u64)); + safe.raw_to_var_len_bytes_vec(ctx, fake_bytes, len, 4); + }); +} + +// Checks circuit is unsatisfied for AssignedValue's are not in range 0..256 +#[test] +#[should_panic(expected = "circuit was not satisfied")] +fn neg_var_len_bytes_vec_witness_values_not_bytes() { + mock_circuit_test(|ctx: &mut Context, safe: SafeTypeChip<'_, Fr>| { + let len = ctx.load_witness(Fr::from(3u64)); + let fake_bytes = ctx.assign_witnesses( + vec![500u64, 500u64, 500u64, 500u64].into_iter().map(Fr::from).collect::>(), + ); + let max_len = fake_bytes.len(); + safe.raw_to_var_len_bytes_vec(ctx, fake_bytes, len, max_len); + }); +} + +//Checks assertion len != max_len +#[test] +#[should_panic] +fn neg_var_len_bytes_vec_len_less_than_max_len() { + mock_circuit_test(|ctx: &mut Context, safe: SafeTypeChip<'_, Fr>| { + let len = ctx.load_witness(Fr::from(5u64)); + let fake_bytes = ctx.assign_witnesses( + vec![500u64, 500u64, 500u64, 500u64].into_iter().map(Fr::from).collect::>(), + ); + let max_len = 5; + safe.raw_to_var_len_bytes_vec(ctx, fake_bytes, len, max_len); + }); +} + +// Circuit Satisfied for valid inputs +#[test] +fn pos_fix_len_bytes_vec() { + base_test().k(10).lookup_bits(8).run(|ctx, range| { + let safe = SafeTypeChip::new(&range); + let fake_bytes = ctx.assign_witnesses( + vec![255u64, 255u64, 255u64, 255u64].into_iter().map(Fr::from).collect::>(), + ); + safe.raw_to_fix_len_bytes::<4>(ctx, fake_bytes.try_into().unwrap()); + }); +} + +// =========== Prover =========== +#[test] +fn pos_prover_satisfied() { + const KEYGEN_MAX_LEN: usize = 4; + const PROVER_MAX_LEN: usize = 4; + let keygen_inputs = (vec![1u64, 2u64, 3u64, 4u64], 3); + let proof_inputs = (vec![1u64, 2u64, 3u64, 4u64], 3); + prover_satisfied::(keygen_inputs, proof_inputs); +} + +#[test] +fn pos_diff_len_same_max_len() { + const KEYGEN_MAX_LEN: usize = 4; + const PROVER_MAX_LEN: usize = 4; + let keygen_inputs = (vec![1u64, 2u64, 3u64, 4u64], 3); + let proof_inputs = (vec![1u64, 2u64, 3u64, 4u64], 2); + prover_satisfied::(keygen_inputs, proof_inputs); +} + +#[test] +#[should_panic] +fn neg_different_proof_max_len() { + const KEYGEN_MAX_LEN: usize = 4; + const PROVER_MAX_LEN: usize = 3; + let keygen_inputs = (vec![1u64, 2u64, 3u64, 4u64], 4); + let proof_inputs = (vec![1u64, 2u64, 3u64], 3); + prover_satisfied::(keygen_inputs, proof_inputs); +} + +//test circuit +fn var_byte_array_circuit( + k: usize, + phase: bool, + (bytes, len): (Vec, usize), +) -> RangeCircuitBuilder { + let lookup_bits = 3; + let mut builder = match phase { + true => GateThreadBuilder::prover(), + false => GateThreadBuilder::keygen(), + }; + let range = RangeChip::::default(lookup_bits); + let safe = SafeTypeChip::new(&range); + let ctx = builder.main(0); + let len = ctx.load_witness(Fr::from(len as u64)); + let fake_bytes = ctx.assign_witnesses(bytes.into_iter().map(Fr::from).collect::>()); + safe.raw_to_var_len_bytes::(ctx, fake_bytes.try_into().unwrap(), len); + let mut params = builder.config(k, Some(9)); + params.lookup_bits = Some(lookup_bits); + let circuit = match phase { + true => RangeCircuitBuilder::prover(builder, params, vec![vec![]]), + false => RangeCircuitBuilder::keygen(builder, params), + }; + circuit +} + +//Prover test +fn prover_satisfied( + keygen_inputs: (Vec, usize), + proof_inputs: (Vec, usize), +) { + let k = 11; + let rng = OsRng; + let params = ParamsKZG::::setup(k as u32, rng); + let keygen_circuit = var_byte_array_circuit::(k, false, keygen_inputs); + let vk = keygen_vk(¶ms, &keygen_circuit).unwrap(); + let pk = keygen_pk(¶ms, vk.clone(), &keygen_circuit).unwrap(); + + let proof_circuit = var_byte_array_circuit::(k, true, proof_inputs); + let proof = gen_proof(¶ms, &pk, proof_circuit); + check_proof(¶ms, &vk, &proof[..], true); +} diff --git a/halo2-base/src/safe_types/tests/mod.rs b/halo2-base/src/safe_types/tests/mod.rs new file mode 100644 index 00000000..ee37540f --- /dev/null +++ b/halo2-base/src/safe_types/tests/mod.rs @@ -0,0 +1,2 @@ +pub(crate) mod bytes; +pub(crate) mod safe_type; diff --git a/halo2-base/src/safe_types/tests.rs b/halo2-base/src/safe_types/tests/safe_type.rs similarity index 99% rename from halo2-base/src/safe_types/tests.rs rename to halo2-base/src/safe_types/tests/safe_type.rs index e71f3159..5434e789 100644 --- a/halo2-base/src/safe_types/tests.rs +++ b/halo2-base/src/safe_types/tests/safe_type.rs @@ -3,7 +3,6 @@ use crate::{ utils::testing::{check_proof, gen_proof}, }; -use super::*; use crate::{ gates::{ builder::{GateThreadBuilder, RangeCircuitBuilder}, @@ -13,6 +12,7 @@ use crate::{ plonk::keygen_pk, plonk::{keygen_vk, Assigned}, }, + safe_types::*, }; use itertools::Itertools; use rand::rngs::OsRng;