halo2_gadgets: Documentation fixes

This commit is contained in:
Jack Grigg 2022-05-10 20:26:49 +00:00
parent ac67b117ca
commit 4b802a7d07
15 changed files with 94 additions and 45 deletions

View File

@ -1,4 +1,4 @@
//! Gadgets for elliptic curve operations.
//! Elliptic curve operations.
use std::fmt::Debug;
@ -169,17 +169,7 @@ pub trait FixedPoints<C: CurveAffine>: Debug + Eq + Clone {
type Base: Debug + Eq + Clone;
}
/// An element of the given elliptic curve's base field, that is used as a scalar
/// in variable-base scalar mul.
///
/// It is not true in general that a scalar field element fits in a curve's
/// base field, and in particular it is untrue for the Pallas curve, whose
/// scalar field `Fq` is larger than its base field `Fp`.
///
/// However, the only use of variable-base scalar mul in the Orchard protocol
/// is in deriving diversified addresses `[ivk] g_d`, and `ivk` is guaranteed
/// to be in the base field of the curve. (See non-normative notes in
/// https://zips.z.cash/protocol/nu5.pdf#orchardkeycomponents.)
/// An integer representing an element of the scalar field for a specific elliptic curve.
#[derive(Debug)]
pub struct ScalarVar<C: CurveAffine, EccChip: EccInstructions<C>> {
chip: EccChip,
@ -264,7 +254,7 @@ impl<C: CurveAffine, EccChip: EccInstructions<C>> ScalarFixedShort<C, EccChip> {
}
}
/// A non-identity elliptic curve point over the given curve.
/// A point on a specific elliptic curve that is guaranteed to not be the identity.
#[derive(Copy, Clone, Debug)]
pub struct NonIdentityPoint<C: CurveAffine, EccChip: EccInstructions<C>> {
chip: EccChip,
@ -382,7 +372,7 @@ impl<C: CurveAffine, EccChip: EccInstructions<C> + Clone + Debug + Eq>
}
}
/// An elliptic curve point over the given curve.
/// A point on a specific elliptic curve.
#[derive(Copy, Clone, Debug)]
pub struct Point<C: CurveAffine, EccChip: EccInstructions<C> + Clone + Debug + Eq> {
chip: EccChip,
@ -444,8 +434,7 @@ impl<C: CurveAffine, EccChip: EccInstructions<C> + Clone + Debug + Eq> Point<C,
}
}
/// The affine short Weierstrass x-coordinate of an elliptic curve point over the
/// given curve.
/// The affine short Weierstrass x-coordinate of a point on a specific elliptic curve.
#[derive(Debug)]
pub struct X<C: CurveAffine, EccChip: EccInstructions<C>> {
chip: EccChip,
@ -464,26 +453,29 @@ impl<C: CurveAffine, EccChip: EccInstructions<C>> X<C, EccChip> {
}
}
/// A constant elliptic curve point over the given curve, for which window tables have
/// been provided to make scalar multiplication more efficient.
/// Precomputed multiples of a fixed point, for full-width scalar multiplication.
///
/// Used in scalar multiplication with full-width scalars.
/// Fixing the curve point enables window tables to be baked into the circuit, making
/// scalar multiplication more efficient. These window tables are tuned to full-width
/// scalar multiplication.
#[derive(Clone, Debug)]
pub struct FixedPoint<C: CurveAffine, EccChip: EccInstructions<C>> {
chip: EccChip,
inner: <EccChip::FixedPoints as FixedPoints<C>>::FullScalar,
}
/// A constant elliptic curve point over the given curve, used in scalar multiplication
/// with a base field element
/// Precomputed multiples of a fixed point, that can be multiplied by base-field elements.
///
/// Fixing the curve point enables window tables to be baked into the circuit, making
/// scalar multiplication more efficient. These window tables are tuned to scalar
/// multiplication by base-field elements.
#[derive(Clone, Debug)]
pub struct FixedPointBaseField<C: CurveAffine, EccChip: EccInstructions<C>> {
chip: EccChip,
inner: <EccChip::FixedPoints as FixedPoints<C>>::Base,
}
/// A constant elliptic curve point over the given curve, used in scalar multiplication
/// with a short signed exponent
/// Precomputed multiples of a fixed point, for short signed scalar multiplication.
#[derive(Clone, Debug)]
pub struct FixedPointShort<C: CurveAffine, EccChip: EccInstructions<C>> {
chip: EccChip,

View File

@ -133,7 +133,7 @@ impl From<NonIdentityEccPoint> for EccPoint {
}
}
/// Configuration for the ECC chip
/// Configuration for [`EccChip`].
#[derive(Clone, Debug, Eq, PartialEq)]
#[allow(non_snake_case)]
pub struct EccConfig<FixedPoints: super::FixedPoints<pallas::Affine>> {
@ -224,7 +224,7 @@ pub trait FixedPoint<C: CurveAffine>: std::fmt::Debug + Eq + Clone {
}
}
/// A chip implementing EccInstructions
/// An [`EccInstructions`] chip that uses 10 advice columns.
#[derive(Clone, Debug, Eq, PartialEq)]
pub struct EccChip<FixedPoints: super::FixedPoints<pallas::Affine>> {
config: EccConfig<FixedPoints>,
@ -397,7 +397,9 @@ pub enum ScalarVar {
/// However, the only use of variable-base scalar mul in the Orchard protocol
/// is in deriving diversified addresses `[ivk] g_d`, and `ivk` is guaranteed
/// to be in the base field of the curve. (See non-normative notes in
/// https://zips.z.cash/protocol/nu5.pdf#orchardkeycomponents.)
/// [4.2.3 Orchard Key Components][orchardkeycomponents].)
///
/// [orchardkeycomponents]: https://zips.z.cash/protocol/protocol.pdf#orchardkeycomponents
BaseFieldElem(AssignedCell<pallas::Base, pallas::Base>),
/// A full-width scalar. This is unimplemented for halo2_gadgets v0.1.0.
FullWidth,

View File

@ -184,7 +184,7 @@ impl Config {
let bits_incomplete_lo = &bits[INCOMPLETE_LO_RANGE];
let lsb = bits[pallas::Scalar::NUM_BITS as usize - 1];
// Initialize the accumulator `acc = [2]base`
// Initialize the accumulator `acc = [2]base` using complete addition.
let acc =
self.add_config
.assign_region(&base_point, &base_point, offset, &mut region)?;
@ -192,7 +192,12 @@ impl Config {
// Increase the offset by 1 after complete addition.
let offset = offset + 1;
// Initialize the running sum for scalar decomposition to zero
// Initialize the running sum for scalar decomposition to zero.
//
// `incomplete::Config::double_and_add` will copy this cell directly into
// itself. This is fine because we are just assigning the same value to
// the same cell twice, and then applying an equality constraint between
// the cell and itself (which the permutation argument treats as a no-op).
let z_init = Z(region.assign_advice_from_constant(
|| "z_init = 0",
self.hi_config.z,
@ -441,7 +446,7 @@ fn decompose_for_scalar_mul(scalar: Option<&pallas::Base>) -> Vec<Option<bool>>
let t_q = U256::from_little_endian(&T_Q.to_le_bytes());
let k = scalar + t_q;
// Big-endian bit representation of `k`.
// Little-endian bit representation of `k`.
let bitstring: Vec<bool> = {
let mut le_bytes = [0u8; 32];
k.to_little_endian(&mut le_bytes);
@ -454,7 +459,7 @@ fn decompose_for_scalar_mul(scalar: Option<&pallas::Base>) -> Vec<Option<bool>>
})
};
// Take the first 255 bits.
// Take the first 255 bits, and reverse to get the big-endian bit representation.
let mut bitstring = bitstring[0..pallas::Scalar::NUM_BITS as usize].to_vec();
bitstring.reverse();
bitstring

View File

@ -168,6 +168,14 @@ impl Config {
.zip(k.as_ref())
.map(|(base_y, k)| if !k { -base_y } else { base_y });
// Assign the conditionally-negated y coordinate into the cell it will be
// used from by both the complete addition gate, and the decomposition and
// conditional negation gate.
//
// The complete addition gate will copy this cell onto itself. This is
// fine because we are just assigning the same value to the same cell
// twice, and then applying an equality constraint between the cell and
// itself (which the permutation argument treats as a no-op).
region.assign_advice(
|| "y_p",
self.add_config.y_p,

View File

@ -190,7 +190,7 @@ impl<FixedPoints: super::FixedPoints<pallas::Affine>> Config<FixedPoints> {
// Process all windows excluding least and most significant windows
let acc = self.add_incomplete::<F, NUM_WINDOWS>(region, offset, acc, base, scalar)?;
// Process most significant window using complete addition
// Process most significant window
let mul_b = self.process_msb::<F, NUM_WINDOWS>(region, offset, base, scalar)?;
Ok((acc, mul_b))
@ -433,8 +433,11 @@ impl From<&EccBaseFieldElemFixed> for ScalarFixed {
}
impl ScalarFixed {
// The scalar decomposition was done in the base field. For computation
// outside the circuit, we now convert them back into the scalar field.
/// The scalar decomposition was done in the base field. For computation
/// outside the circuit, we now convert them back into the scalar field.
///
/// This function does not require that the base field fits inside the scalar field,
/// because the window size fits into either field.
fn windows_field(&self) -> Vec<Option<pallas::Scalar>> {
let running_sum_to_windows = |zs: Vec<AssignedCell<pallas::Base, pallas::Base>>| {
(0..(zs.len() - 1))
@ -444,6 +447,9 @@ impl ScalarFixed {
let word = z_cur
.zip(z_next)
.map(|(z_cur, z_next)| z_cur - z_next * *H_BASE);
// This assumes that the endianness of the encodings of pallas::Base
// and pallas::Scalar are the same. They happen to be, but we need to
// be careful if this is generalised.
word.map(|word| pallas::Scalar::from_repr(word.to_repr()).unwrap())
})
.collect::<Vec<_>>()
@ -463,6 +469,9 @@ impl ScalarFixed {
.expect("EccScalarFixed has been witnessed")
.iter()
.map(|bits| {
// This assumes that the endianness of the encodings of pallas::Base
// and pallas::Scalar are the same. They happen to be, but we need to
// be careful if this is generalised.
bits.value()
.map(|value| pallas::Scalar::from_repr(value.to_repr()).unwrap())
})

View File

@ -43,7 +43,7 @@ impl<Fixed: FixedPoints<pallas::Affine>> Config<Fixed> {
.coords_check(meta, window.clone())
.into_iter()
// Constrain each window to a 3-bit value:
// 1 * (window - 0) * (window - 1) * ... * (window - 7)
// window * (1 - window) * ... * (7 - window)
.chain(Some(("window range check", range_check(window, H)))),
)
});

View File

@ -37,7 +37,7 @@ impl<Fixed: FixedPoints<pallas::Affine>> Config<Fixed> {
let q_mul_fixed_short = meta.query_selector(self.q_mul_fixed_short);
let y_p = meta.query_advice(self.super_config.add_config.y_p, Rotation::cur());
let y_a = meta.query_advice(self.super_config.add_config.y_qr, Rotation::cur());
// z_21
// z_21 = k_21
let last_window = meta.query_advice(self.super_config.u, Rotation::cur());
let sign = meta.query_advice(self.super_config.window, Rotation::cur());
@ -73,6 +73,10 @@ impl<Fixed: FixedPoints<pallas::Affine>> Config<Fixed> {
});
}
/// Constraints `magnitude` to be at most 66 bits.
///
/// The final window is separately constrained to be a single bit, which completes the
/// 64-bit range constraint.
fn decompose(
&self,
region: &mut Region<'_, pallas::Base>,

View File

@ -1,4 +1,18 @@
//! # halo2_gadgets
//! This crate provides various common gadgets and chips for use with `halo2_proofs`.
//!
//! # Gadgets
//!
//! Gadgets are an abstraction for writing reusable and interoperable circuit logic. They
//! do not create any circuit constraints or assignments themselves, instead interacting
//! with the circuit through a defined "instruction set". A circuit developer uses gadgets
//! by instantiating them with a particular choice of chip.
//!
//! # Chips
//!
//! Chips implement the low-level circuit constraints. The same instructions may be
//! implemented by multiple chips, enabling different performance trade-offs to be made.
//! Chips can be highly optimised by their developers, as long as they conform to the
//! defined instructions.
#![cfg_attr(docsrs, feature(doc_cfg))]
// Temporary until we have more of the crate implemented.
@ -12,6 +26,7 @@
pub mod ecc;
pub mod poseidon;
#[cfg(feature = "unstable")]
#[cfg_attr(docsrs, doc(cfg(feature = "unstable")))]
pub mod sha256;
pub mod sinsemilla;
pub mod utilities;

View File

@ -1,4 +1,4 @@
//! Gadget and chips for the Poseidon algebraic hash function.
//! The Poseidon algebraic hash function.
use std::convert::TryInto;
use std::fmt;

View File

@ -291,7 +291,7 @@ pub trait Domain<F: FieldExt, const RATE: usize> {
/// A Poseidon hash function used with constant input length.
///
/// Domain specified in section 4.2 of https://eprint.iacr.org/2019/458.pdf
/// Domain specified in [ePrint 2019/458 section 4.2](https://eprint.iacr.org/2019/458.pdf).
#[derive(Clone, Copy, Debug)]
pub struct ConstantLength<const L: usize>;

View File

@ -1,6 +1,11 @@
//! https://github.com/daira/pasta-hadeshash
//! Constants for using Poseidon with the Pallas field.
//!
//! The constants can be reproduced by running the following Sage script from
//! [this repository](https://github.com/daira/pasta-hadeshash):
//!
//! ```text
//! $ sage generate_parameters_grain.sage 1 0 255 3 8 56 0x40000000000000000000000000000000224698fc094cf91b992d30ed00000001
//! ```
use pasta_curves::pallas;
// Number of round constants: 192

View File

@ -1,6 +1,11 @@
//! https://github.com/daira/pasta-hadeshash
//! Constants for using Poseidon with the Vesta field.
//!
//! The constants can be reproduced by running the following Sage script from
//! [this repository](https://github.com/daira/pasta-hadeshash):
//!
//! ```text
//! sage generate_parameters_grain.sage 1 0 255 3 8 56 0x40000000000000000000000000000000224698fc0994a8dd8c46eb2100000001
//! ```
use pasta_curves::vesta;
// Number of round constants: 192

View File

@ -1,4 +1,4 @@
//! Gadget and chips for the [SHA-256] hash function.
//! The [SHA-256] hash function.
//!
//! [SHA-256]: https://tools.ietf.org/html/rfc6234

View File

@ -1,4 +1,6 @@
//! Gadgets for the Sinsemilla hash function.
//! The [Sinsemilla] hash function.
//!
//! [Sinsemilla]: https://zips.z.cash/protocol/protocol.pdf#concretesinsemillahash
use crate::{
ecc::{self, EccInstructions, FixedPoints},
utilities::{FieldValue, RangeConstrained, Var},
@ -224,7 +226,9 @@ where
}
/// Constructs a `MessagePiece` by concatenating a sequence of [`RangeConstrained`]
/// subpieces.
/// subpiece values.
///
/// The `MessagePiece` is assigned to the circuit, but not constrained in any way.
///
/// # Panics
///

View File

@ -1,9 +1,9 @@
use super::K;
use pasta_curves::pallas;
/// The precomputed bases for the Sinsemilla hash function.
/// The precomputed bases for the [Sinsemilla hash function][concretesinsemillahash].
///
/// https://zips.z.cash/protocol/protocol.pdf#concretesinsemillahash
/// [concretesinsemillahash]: https://zips.z.cash/protocol/protocol.pdf#concretesinsemillahash
pub const SINSEMILLA_S: [(pallas::Base, pallas::Base); 1 << K] = [
(
pallas::Base::from_raw([