diff --git a/src/circuit/gadget/sinsemilla.rs b/src/circuit/gadget/sinsemilla.rs index f4173010..c0130f9c 100644 --- a/src/circuit/gadget/sinsemilla.rs +++ b/src/circuit/gadget/sinsemilla.rs @@ -9,6 +9,7 @@ use pasta_curves::arithmetic::{CurveAffine, FieldExt}; use std::{convert::TryInto, fmt::Debug}; pub mod chip; +pub mod commit_ivk; pub mod merkle; mod message; @@ -30,7 +31,7 @@ pub trait SinsemillaInstructions where SinsemillaChip: SinsemillaInstructions + Clone + Debug + Eq, @@ -162,6 +163,16 @@ where inner: SinsemillaChip::MessagePiece, } +impl + MessagePiece +where + SinsemillaChip: SinsemillaInstructions + Clone + Debug + Eq, +{ + fn inner(&self) -> SinsemillaChip::MessagePiece { + self.inner + } +} + impl MessagePiece where diff --git a/src/circuit/gadget/sinsemilla/commit_ivk.rs b/src/circuit/gadget/sinsemilla/commit_ivk.rs new file mode 100644 index 00000000..6d8cf86f --- /dev/null +++ b/src/circuit/gadget/sinsemilla/commit_ivk.rs @@ -0,0 +1,623 @@ +use halo2::{ + circuit::Layouter, + plonk::{Advice, Column, ConstraintSystem, Error, Expression, Selector}, + poly::Rotation, +}; +use pasta_curves::{arithmetic::FieldExt, pallas}; + +use crate::{ + circuit::gadget::{ + ecc::{chip::EccChip, X}, + utilities::{bitrange_subset, bool_check, copy, CellValue, Var}, + }, + constants::T_P, +}; + +use super::{ + chip::{SinsemillaChip, SinsemillaCommitDomains, SinsemillaConfig}, + CommitDomain, Message, MessagePiece, +}; + +// +// We need to hash `ak || nk` where each of `ak`, `nk` is a field element (255 bits). +// +// a = bits 0..=249 of `ak` +// b = b_0||b_1||b_2` = (bits 250..=253 of `ak`) || (bit 254 of `ak`) || (bits 0..=4 of `nk`) +// c = bits 5..=244 of `nk` +// d = d_0||d_1` = (bits 245..=253 of `nk`) || (bit 254 of `nk`) + +#[derive(Clone, Debug)] +pub struct CommitIvkConfig { + q_canon: Selector, + advices: [Column; 10], + sinsemilla_config: SinsemillaConfig, +} + +impl CommitIvkConfig { + pub(in crate::circuit) fn configure( + meta: &mut ConstraintSystem, + advices: [Column; 10], + sinsemilla_config: SinsemillaConfig, + ) -> Self { + let q_canon = meta.selector(); + + let config = Self { + q_canon, + advices, + sinsemilla_config, + }; + + // + // We need to hash `ak || nk` where each of `ak`, `nk` is a field element (255 bits). + // + // a = bits 0..=249 of `ak` + // b = b_0||b_1||b_2` + // = (bits 250..=253 of `ak`) || (bit 254 of `ak`) || (bits 0..=4 of `nk`) + // c = bits 5..=244 of `nk` + // d = d_0||d_1` = (bits 245..=253 of `nk`) || (bit 254 of `nk`) + // + // `a`, `b`, `c`, `d` have been constrained by the Sinsemilla hash to be: + // - a: 250 bits, + // - b: 10 bits, + // - c: 240 bits, + // - d: 10 bits + // + meta.create_gate("CommitIvk canonicity check", |meta| { + let q_canon = meta.query_selector(config.q_canon); + + // Useful constants + let two_pow_4 = pallas::Base::from_u64(1 << 4); + let two_pow_5 = pallas::Base::from_u64(1 << 5); + let two_pow_9 = two_pow_4 * two_pow_5; + let two_pow_250 = pallas::Base::from_u128(1 << 125).square(); + let two_pow_254 = two_pow_250 * pallas::Base::from_u64(1 << 4); + + // `a` is constrained by the Sinsemilla hash to be 250 bits. + let a = meta.query_advice(config.advices[0], Rotation::prev()); + // `b` is constrained by the Sinsemilla hash to be 10 bits. + let b_whole = meta.query_advice(config.advices[1], Rotation::prev()); + // `c` is constrained by the Sinsemilla hash to be 240 bits. + let c = meta.query_advice(config.advices[2], Rotation::prev()); + // `d` is constrained by the Sinsemilla hash to be 10 bits. + let d_whole = meta.query_advice(config.advices[3], Rotation::prev()); + let ak = meta.query_advice(config.advices[4], Rotation::prev()); + let nk = meta.query_advice(config.advices[5], Rotation::prev()); + + // b = b_0||b_1||b_2` + // = (bits 250..=253 of `ak`) || (bit 254 of `ak`) || (bits 0..=4 of `nk`) + // + // b_0 has been constrained outside this gate to be a four-bit value. + let b_0 = meta.query_advice(config.advices[6], Rotation::prev()); + // This gate constrains b_1 to be a one-bit value. + let b_1 = meta.query_advice(config.advices[7], Rotation::prev()); + // b_2 has been constrained outside this gate to be a five-bit value. + let b_2 = meta.query_advice(config.advices[8], Rotation::prev()); + // Check that b_whole is consistent with the witnessed subpieces. + let b_decomposition_check = + b_whole - (b_0.clone() + b_1.clone() * two_pow_4 + b_2.clone() * two_pow_5); + + // d = d_0||d_1` = (bits 245..=253 of `nk`) || (bit 254 of `nk`) + // + // d_0 has been constrained outside this gate to be a nine-bit value. + let d_0 = meta.query_advice(config.advices[9], Rotation::prev()); + // This gate constrains d_1 to be a one-bit value. + let d_1 = meta.query_advice(config.advices[0], Rotation::cur()); + // Check that d_whole is consistent with the witnessed subpieces. + let d_decomposition_check = d_whole - (d_0.clone() + d_1.clone() * two_pow_9); + + // Check `b_1` is a single-bit value + let b1_bool_check = bool_check(b_1.clone()); + + // Check `d_1` is a single-bit value + let d1_bool_check = bool_check(d_1.clone()); + + // Check that ak = a (250 bits) || b_0 (4 bits) || b_1 (1 bit) + let ak_decomposition_check = + a.clone() + b_0.clone() * two_pow_250 + b_1.clone() * two_pow_254 - ak; + + // Check that nk = b_2 (5 bits) || c (240 bits) || d_0 (9 bits) || d_1 (1 bit) + let nk_decomposition_check = { + let two_pow_245 = pallas::Base::from_u64(1 << 49).pow(&[5, 0, 0, 0]); + + b_2.clone() + + c.clone() * two_pow_5 + + d_0.clone() * two_pow_245 + + d_1.clone() * two_pow_254 + - nk + }; + + // ak = a (250 bits) || b_0 (4 bits) || b_1 (1 bit) + // The `ak` canonicity checks are enforced if and only if `b_1` = 1. + let ak_canonicity_checks = { + // b_1 = 1 => b_0 = 0 + let b0_canon_check = b_1.clone() * b_0; + + // z13_a is the 13th running sum output by the 10-bit Sinsemilla decomposition of `a`. + // b_1 = 1 => z13_a = 0 + let z13_a_check = { + let z13_a = meta.query_advice(config.advices[1], Rotation::cur()); + b_1.clone() * z13_a + }; + + // Check that a_prime = a + 2^130 - t_P. + // This is checked regardless of the value of b_1. + let a_prime_check = { + let a_prime = meta.query_advice(config.advices[2], Rotation::cur()); + let two_pow_130 = + Expression::Constant(pallas::Base::from_u128(1 << 65).square()); + let t_p = Expression::Constant(pallas::Base::from_u128(T_P)); + a + two_pow_130 - t_p - a_prime + }; + + // Check that the running sum output by the 130-bit little-endian decomposition of + // `a_prime` is zero. + let a_prime_decomposition = { + let a_prime_decomposition = + meta.query_advice(config.advices[3], Rotation::cur()); + b_1 * a_prime_decomposition + }; + + std::iter::empty() + .chain(Some(b0_canon_check)) + .chain(Some(z13_a_check)) + .chain(Some(a_prime_check)) + .chain(Some(a_prime_decomposition)) + }; + + // nk = b_2 (5 bits) || c (240 bits) || d_0 (9 bits) || d_1 (1 bit) + // The `nk` canonicity checks are enforced if and only if `d_1` = 1. + let nk_canonicity_checks = { + // d_1 = 1 => d_0 = 0 + let c0_canon_check = d_1.clone() * d_0; + + // d_1 = 1 => z14_c = 0, where z14_c is the 14th running sum + // output by the 10-bit Sinsemilla decomposition of `c`. + let z14_c_check = { + let z14_c = meta.query_advice(config.advices[4], Rotation::cur()); + d_1.clone() * z14_c + }; + + // Check that b2_c_prime = b_2 + c * 2^5 + 2^140 - t_P. + // This is checked regardless of the value of d_1. + let b2_c_prime_check = { + let two_pow_5 = pallas::Base::from_u64(5); + let two_pow_140 = + Expression::Constant(pallas::Base::from_u128(1 << 70).square()); + let t_p = Expression::Constant(pallas::Base::from_u128(T_P)); + let b2_c_prime = meta.query_advice(config.advices[5], Rotation::cur()); + b_2 + c * two_pow_5 + two_pow_140 - t_p - b2_c_prime + }; + + // Check that the running sum output by the 140-bit little- + // endian decomposition of b2_c_prime is zero. + let b2_c_prime_decomposition = { + let b2_c_prime_decomposition = + meta.query_advice(config.advices[6], Rotation::cur()); + d_1 * b2_c_prime_decomposition + }; + + std::iter::empty() + .chain(Some(c0_canon_check)) + .chain(Some(z14_c_check)) + .chain(Some(b2_c_prime_check)) + .chain(Some(b2_c_prime_decomposition)) + }; + + std::iter::empty() + .chain(Some(b1_bool_check)) + .chain(Some(d1_bool_check)) + .chain(Some(b_decomposition_check)) + .chain(Some(d_decomposition_check)) + .chain(Some(ak_decomposition_check)) + .chain(Some(nk_decomposition_check)) + .chain(ak_canonicity_checks) + .chain(nk_canonicity_checks) + .map(move |poly| q_canon.clone() * poly) + }); + + config + } + + #[allow(non_snake_case)] + #[allow(clippy::type_complexity)] + pub(in crate::circuit) fn assign_region( + &self, + sinsemilla_chip: SinsemillaChip, + ecc_chip: EccChip, + mut layouter: impl Layouter, + ak: CellValue, + nk: CellValue, + rivk: Option, + ) -> Result, Error> { + // + // We need to hash `ak || nk` where each of `ak`, `nk` is a field element (255 bits). + // + // a = bits 0..=249 of `ak` + // b = b_0||b_1||b_2` + // = (bits 250..=253 of `ak`) || (bit 254 of `ak`) || (bits 0..=4 of `nk`) + // c = bits 5..=244 of `nk` + // d = d_0||d_1` = (bits 245..=253 of `nk`) || (bit 254 of `nk`) + + // `a` = bits 0..=249 of `ak` + let a = { + let a = ak.value().map(|value| bitrange_subset(value, 0..250)); + MessagePiece::from_field_elem( + sinsemilla_chip.clone(), + layouter.namespace(|| "a"), + a, + 25, + )? + }; + + // `b = b_0||b_1||b_2` + // = (bits 250..=253 of `ak`) || (bit 254 of `ak`) || (bits 0..=4 of `nk`) + let (b_0, b_1, b_2, b) = { + let b_0 = ak.value().map(|value| bitrange_subset(value, 250..254)); + let b_1 = ak.value().map(|value| bitrange_subset(value, 254..255)); + let b_2 = nk.value().map(|value| bitrange_subset(value, 0..5)); + + let b = b_0.zip(b_1).zip(b_2).map(|((b_0, b_1), b_2)| { + let b1_shifted = b_1 * pallas::Base::from_u64(1 << 4); + let b2_shifted = b_2 * pallas::Base::from_u64(1 << 5); + b_0 + b1_shifted + b2_shifted + }); + + // Constrain b_0 to be 4 bits. + let b_0 = self.sinsemilla_config.lookup_config_0.witness_short_check( + layouter.namespace(|| "b_0 is 4 bits"), + b_0, + 4, + )?; + // Constrain b_2 to be 5 bits. + let b_2 = self.sinsemilla_config.lookup_config_1.witness_short_check( + layouter.namespace(|| "b_2 is 5 bits"), + b_2, + 5, + )?; + // b_1 will be boolean-constrained in the custom gate. + + let b = MessagePiece::from_field_elem( + sinsemilla_chip.clone(), + layouter.namespace(|| "b = b_0 || b_1 || b_2"), + b, + 1, + )?; + + (b_0, b_1, b_2, b) + }; + + // c = bits 5..=244 of `nk` + let c = { + let c = nk.value().map(|value| bitrange_subset(value, 5..245)); + MessagePiece::from_field_elem( + sinsemilla_chip.clone(), + layouter.namespace(|| "c"), + c, + 24, + )? + }; + + // `d = d_0||d_1` = (bits 245..=253 of `nk`) || (bit 254 of `nk`) + let (d_0, d_1, d) = { + let d_0 = nk.value().map(|value| bitrange_subset(value, 245..254)); + let d_1 = nk.value().map(|value| bitrange_subset(value, 254..255)); + + let d = d_0 + .zip(d_1) + .map(|(d_0, d_1)| d_0 + d_1 * pallas::Base::from_u64(1 << 9)); + + // Constrain d_0 to be 9 bits. + let d_0 = self.sinsemilla_config.lookup_config_2.witness_short_check( + layouter.namespace(|| "d_0 is 9 bits"), + d_0, + 9, + )?; + // d_1 will be boolean-constrained in the custom gate. + + let d = MessagePiece::from_field_elem( + sinsemilla_chip.clone(), + layouter.namespace(|| "c = d_0 || d_1"), + d, + 1, + )?; + + (d_0, d_1, d) + }; + + let (ivk, zs) = { + let message = Message::from_pieces( + sinsemilla_chip.clone(), + vec![a.clone(), b.clone(), c.clone(), d.clone()], + ); + let domain = CommitDomain::new( + sinsemilla_chip, + ecc_chip, + &SinsemillaCommitDomains::CommitIvk, + ); + domain.short_commit(layouter.namespace(|| "Hash ak||nk"), message, rivk)? + }; + + let z13_a = zs[0][13]; + let z14_c = zs[2][14]; + + let (a_prime, a_prime_decomposition) = self.ak_canonicity( + layouter.namespace(|| "ak canonicity"), + a.inner().cell_value(), + )?; + + let (b2_c_prime, b2_c_prime_decomposition) = self.nk_canonicity( + layouter.namespace(|| "nk canonicity"), + b_2, + c.inner().cell_value(), + )?; + + let gate_cells = GateCells { + a: a.inner().cell_value(), + b: b.inner().cell_value(), + c: c.inner().cell_value(), + d: d.inner().cell_value(), + ak, + nk, + b_0, + b_1, + b_2, + d_0, + d_1, + z13_a, + a_prime, + a_prime_decomposition, + z14_c, + b2_c_prime, + b2_c_prime_decomposition, + }; + + self.assign_gate( + layouter.namespace(|| "Assign cells used in canonicity gate"), + gate_cells, + )?; + + Ok(ivk) + } + + #[allow(clippy::type_complexity)] + // Check canonicity of `ak` encoding + fn ak_canonicity( + &self, + mut layouter: impl Layouter, + a: CellValue, + ) -> Result<(CellValue, CellValue), Error> { + // `ak` = `a (250 bits) || b_0 (4 bits) || b_1 (1 bit)` + // - b_1 = 1 => b_0 = 0 + // - b_1 = 1 => a < t_P + // - (0 ≤ a < 2^130) => z13_a of SinsemillaHash(a) == 0 + // - 0 ≤ a + 2^130 - t_P < 2^130 (thirteen 10-bit lookups) + + // Decompose the low 130 bits of a_prime = a + 2^130 - t_P, and output + // the running sum at the end of it. If a_prime < 2^130, the running sum + // will be 0. + let a_prime = a.value().map(|a| { + let two_pow_130 = pallas::Base::from_u128(1u128 << 65).square(); + let t_p = pallas::Base::from_u128(T_P); + a + two_pow_130 - t_p + }); + let (a_prime, zs) = self.sinsemilla_config.lookup_config_3.witness_check( + layouter.namespace(|| "Decompose low 130 bits of (a + 2^130 - t_P)"), + a_prime, + 13, + false, + )?; + assert_eq!(zs.len(), 14); // [z_0, z_1, ..., z13_a] + + Ok((a_prime, zs[13])) + } + + #[allow(clippy::type_complexity)] + // Check canonicity of `nk` encoding + fn nk_canonicity( + &self, + mut layouter: impl Layouter, + b_2: CellValue, + c: CellValue, + ) -> Result<(CellValue, CellValue), Error> { + // `nk` = `b_2 (5 bits) || c (240 bits) || d_0 (9 bits) || d_1 (1 bit) + // - d_1 = 1 => d_0 = 0 + // - d_1 = 1 => b_2 + c * 2^5 < t_P + // - 0 ≤ b_2 + c * 2^5 < 2^140 + // - b_2 was constrained to be 5 bits. + // - z_13 of SinsemillaHash(c) constrains bits 5..=134 to 130 bits + // - so b_2 + c * 2^5 is constrained to be 135 bits < 2^140. + // - 0 ≤ b_2 + c * 2^5 + 2^140 - t_P < 2^140 (14 ten-bit lookups) + + // Decompose the low 140 bits of b2_c_prime = b_2 + c * 2^5 + 2^140 - t_P, and output + // the running sum at the end of it. If b2_c_prime < 2^140, the running sum will be 0. + let b2_c_prime = b_2.value().zip(c.value()).map(|(b_2, c)| { + let two_pow_5 = pallas::Base::from_u64(5); + let two_pow_140 = pallas::Base::from_u128(1u128 << 70).square(); + let t_p = pallas::Base::from_u128(T_P); + b_2 + c * two_pow_5 + two_pow_140 - t_p + }); + let (b2_c_prime, zs) = self.sinsemilla_config.lookup_config_4.witness_check( + layouter.namespace(|| "Decompose low 140 bits of (b_2 + c * 2^5 + 2^140 - t_P)"), + b2_c_prime, + 14, + false, + )?; + assert_eq!(zs.len(), 15); // [z_0, z_1, ..., z14] + + Ok((b2_c_prime, zs[14])) + } + + // Assign cells for the canonicity gate. + fn assign_gate( + &self, + mut layouter: impl Layouter, + gate_cells: GateCells, + ) -> Result<(), Error> { + layouter.assign_region( + || "Assign cells used in canonicity gate", + |mut region| { + // Enable selector on offset 1 + self.q_canon.enable(&mut region, 1)?; + + // Offset 0 + { + let offset = 0; + // Copy in `a` + copy(&mut region, || "a", self.advices[0], offset, &gate_cells.a)?; + + // Copy in `b` + copy(&mut region, || "b", self.advices[1], offset, &gate_cells.b)?; + + // Copy in `c` + copy(&mut region, || "c", self.advices[2], offset, &gate_cells.c)?; + + // Copy in `d` + copy(&mut region, || "d", self.advices[3], offset, &gate_cells.d)?; + + // Copy in `ak` + copy( + &mut region, + || "ak", + self.advices[4], + offset, + &gate_cells.ak, + )?; + + // Copy in `nk` + copy( + &mut region, + || "nk", + self.advices[5], + offset, + &gate_cells.nk, + )?; + + // Copy in `b_0` + copy( + &mut region, + || "b_0", + self.advices[6], + offset, + &gate_cells.b_0, + )?; + + // Witness `b_1` + region.assign_advice( + || "Witness b_1", + self.advices[7], + offset, + || gate_cells.b_1.ok_or(Error::SynthesisError), + )?; + + // Copy in `b_2` + copy( + &mut region, + || "b_2", + self.advices[8], + offset, + &gate_cells.b_2, + )?; + + // Copy in `d_0` + copy( + &mut region, + || "d_0", + self.advices[9], + offset, + &gate_cells.d_0, + )?; + } + + // Offset 1 + { + let offset = 1; + + // Witness `d_1` + region.assign_advice( + || "Witness d_1", + self.advices[0], + offset, + || gate_cells.d_1.ok_or(Error::SynthesisError), + )?; + + // Copy in z13_a + copy( + &mut region, + || "z13_a", + self.advices[1], + offset, + &gate_cells.z13_a, + )?; + + // Copy in a_prime + copy( + &mut region, + || "a_prime", + self.advices[2], + offset, + &gate_cells.a_prime, + )?; + + // Copy in a_prime_decomposition + copy( + &mut region, + || "a_prime_decomposition", + self.advices[3], + offset, + &gate_cells.a_prime_decomposition, + )?; + + // Copy in z14_c + copy( + &mut region, + || "z14_c", + self.advices[4], + offset, + &gate_cells.z14_c, + )?; + + // Copy in b2_c_prime + copy( + &mut region, + || "b2_c_prime", + self.advices[5], + offset, + &gate_cells.b2_c_prime, + )?; + + // Copy in b2_c_prime_decomposition + copy( + &mut region, + || "b2_c_prime_decomposition", + self.advices[6], + offset, + &gate_cells.b2_c_prime_decomposition, + )?; + } + + Ok(()) + }, + ) + } +} + +// Cells used in the canonicity gate. +struct GateCells { + a: CellValue, + b: CellValue, + c: CellValue, + d: CellValue, + ak: CellValue, + nk: CellValue, + b_0: CellValue, + b_1: Option, + b_2: CellValue, + d_0: CellValue, + d_1: Option, + z13_a: CellValue, + a_prime: CellValue, + a_prime_decomposition: CellValue, + z14_c: CellValue, + b2_c_prime: CellValue, + b2_c_prime_decomposition: CellValue, +} diff --git a/src/circuit/gadget/utilities.rs b/src/circuit/gadget/utilities.rs index 19c95752..6fd2ef9c 100644 --- a/src/circuit/gadget/utilities.rs +++ b/src/circuit/gadget/utilities.rs @@ -102,6 +102,11 @@ pub fn transpose_option_array( ret } +/// Checks that an expresssion is either 1 or 0. +pub fn bool_check(value: Expression) -> Expression { + value.clone() * (Expression::Constant(F::one()) - value) +} + /// Takes a specified subsequence of the little-endian bit representation of a field element. /// The bits are numbered from 0 for the LSB. pub fn bitrange_subset(field_elem: F, bitrange: Range) -> F {