zec
/
halo2
mirror of https://github.com/zcash/halo2.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Migrate to latest `halo2` API 

- `halo2::plonk::{create_proof, verify_proof}` now take instance columns
  as slices of values.
- `halo2::plonk::Permutation` has been replaced by a global permutation,
  to which columns can be added with `ConstraintSystem::enable_equality`.
- The introduction of blinding rows means that various tests now require
  larger circuit parameters.
This commit is contained in:
Jack Grigg 2021-07-15 12:52:15 +01:00
parent cf4c78f9a1
commit 15f9d254d9
25 changed files with 217 additions and 438 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Cargo.toml
View File

@ -62,5 +62,5 @@ name = "small"
harness = false
[patch.crates-io]
halo2 = { git = "https://github.com/zcash/halo2.git", rev = "d5be50a8488a433a9b20f1127ff1e21f121c5a2c" }
halo2 = { git = "https://github.com/zcash/halo2.git", rev = "4a9e329ded1c54347af105210c77587bb69f3c57" }
zcash_note_encryption = { git = "https://github.com/zcash/librustzcash.git", rev = "cc533a9da4f6a7209a7be05f82b12a03969152c9" }

33
src/circuit.rs
View File

@ -2,11 +2,10 @@
use std::mem;
use group::Curve;
use halo2::{
circuit::{Layouter, SimpleFloorPlanner},
plonk,
poly::{EvaluationDomain, LagrangeCoeff, Polynomial, Rotation},
poly::Rotation,
transcript::{Blake2bRead, Blake2bWrite},
};
use pasta_curves::{pallas, vesta};
@ -107,21 +106,9 @@ pub struct Instance {
}
impl Instance {
fn to_halo2_instance(
&self,
domain: &EvaluationDomain<vesta::Scalar>,
) -> [Polynomial<vesta::Scalar, LagrangeCoeff>; 1] {
fn to_halo2_instance(&self) -> [[vesta::Scalar; 0]; 1] {
// TODO
[domain.empty_lagrange()]
}
fn to_halo2_instance_commitments(&self, vk: &VerifyingKey) -> [vesta::Affine; 1] {
[vk.params
.commit_lagrange(
&self.to_halo2_instance(vk.vk.get_domain())[0],
Default::default(),
)
.to_affine()]
[[]]
}
}
@ -149,9 +136,10 @@ impl Proof {
circuits: &[Circuit],
instances: &[Instance],
) -> Result<Self, plonk::Error> {
let instances: Vec<_> = instances
let instances: Vec<_> = instances.iter().map(|i| i.to_halo2_instance()).collect();
let instances: Vec<Vec<_>> = instances
.iter()
.map(|i| i.to_halo2_instance(pk.pk.get_vk().get_domain()))
.map(|i| i.iter().map(|c| &c[..]).collect())
.collect();
let instances: Vec<_> = instances.iter().map(|i| &i[..]).collect();
@ -162,9 +150,10 @@ impl Proof {
/// Verifies this proof with the given instances.
pub fn verify(&self, vk: &VerifyingKey, instances: &[Instance]) -> Result<(), plonk::Error> {
let instances: Vec<_> = instances
let instances: Vec<_> = instances.iter().map(|i| i.to_halo2_instance()).collect();
let instances: Vec<Vec<_>> = instances
.iter()
.map(|i| i.to_halo2_instance_commitments(vk))
.map(|i| i.iter().map(|c| &c[..]).collect())
.collect();
let instances: Vec<_> = instances.iter().map(|i| &i[..]).collect();
@ -241,9 +230,9 @@ mod tests {
K,
circuit,
instance
.to_halo2_instance(vk.vk.get_domain())
.to_halo2_instance()
.iter()
.map(|p| p.iter().cloned().collect())
.map(|p| p.to_vec())
.collect()
)
.unwrap()

12
src/circuit/gadget/ecc.rs
View File

@ -422,18 +422,10 @@ mod tests {
meta.advice_column(),
meta.advice_column(),
];
let constants = [meta.fixed_column(), meta.fixed_column()];
let perm = meta.permutation(
&advices
.iter()
.map(|advice| (*advice).into())
.chain(constants.iter().map(|fixed| (*fixed).into()))
.collect::<Vec<_>>(),
);
let lookup_table = meta.fixed_column();
EccChip::configure(meta, advices, lookup_table, constants, perm)
EccChip::configure(meta, advices, lookup_table, constants)
}
fn synthesize(

65
src/circuit/gadget/ecc/chip.rs
View File

@ -12,7 +12,7 @@ use arrayvec::ArrayVec;
use group::prime::PrimeCurveAffine;
use halo2::{
circuit::{Chip, Layouter},
plonk::{Advice, Column, ConstraintSystem, Error, Fixed, Permutation, Selector},
plonk::{Advice, Column, ConstraintSystem, Error, Fixed, Selector},
};
use pasta_curves::{arithmetic::CurveAffine, pallas};
@ -111,12 +111,8 @@ pub struct EccConfig {
/// Witness point
pub q_point: Selector,
/// Shared fixed column used for loading constants. This is included in
/// the permutation so that cells in advice columns can be constrained to
/// equal cells in this fixed column.
/// Shared fixed column used for loading constants.
pub constants: Column<Fixed>,
/// Permutation over all advice columns and the `constants` fixed column.
pub perm: Permutation,
/// Lookup range check using 10-bit lookup table
pub lookup_config: LookupRangeCheckConfig<pallas::Base, { sinsemilla::K }>,
/// Running sum decomposition.
@ -151,6 +147,9 @@ impl EccChip {
Self { config }
}
/// # Side effects
///
/// All columns in `advices` and `constants` will be equality-enabled.
#[allow(non_snake_case)]
pub fn configure(
meta: &mut ConstraintSystem<pallas::Base>,
@ -158,18 +157,48 @@ impl EccChip {
lookup_table: Column<Fixed>,
// TODO: Replace with public inputs API
constants: [Column<Fixed>; 2],
perm: Permutation,
) -> <Self as Chip<pallas::Base>>::Config {
let lookup_config = LookupRangeCheckConfig::configure(
meta,
advices[9],
constants[0],
lookup_table,
perm.clone(),
);
// The following columns need to be equality-enabled for their use in sub-configs:
//
// add::Config and add_incomplete::Config:
// - advices[0]: x_p,
// - advices[1]: y_p,
// - advices[2]: x_qr,
// - advices[3]: y_qr,
//
// mul_fixed::Config:
// - advices[4]: window
// - advices[5]: u
//
// mul_fixed::base_field_element::Config:
// - [advices[6], advices[7], advices[8]]: canon_advices
//
// mul::overflow::Config:
// - [advices[0], advices[1], advices[2]]: advices
//
// mul::incomplete::Config
// - advices[4]: lambda1
// - advices[9]: z
//
// mul::complete::Config:
// - advices[9]: z_complete
//
// I have not yet figured out where constants[1] is used in an equality constraint
// but we get synthesis errors without it.
//
// TODO: Refactor away from `impl From<EccConfig> for _` so that sub-configs can
// equality-enable the columns they need to.
for column in &advices {
meta.enable_equality((*column).into());
}
// constants[0] is also equality-enabled here.
let lookup_config =
LookupRangeCheckConfig::configure(meta, advices[9], constants[0], lookup_table);
meta.enable_equality(constants[1].into());
let q_mul_fixed_running_sum = meta.selector();
let running_sum_config =
RunningSumConfig::configure(meta, q_mul_fixed_running_sum, advices[4], perm.clone());
RunningSumConfig::configure(meta, q_mul_fixed_running_sum, advices[4]);
let config = EccConfig {
advices,
@ -197,7 +226,6 @@ impl EccChip {
q_mul_fixed_running_sum,
q_point: meta.selector(),
constants: constants[1],
perm,
lookup_config,
running_sum_config,
};
@ -323,14 +351,13 @@ impl EccInstructions<pallas::Affine> for EccChip {
a: &Self::Point,
b: &Self::Point,
) -> Result<(), Error> {
let config = self.config().clone();
layouter.assign_region(
|| "constrain equal",
|mut region| {
// Constrain x-coordinates
region.constrain_equal(&config.perm, a.x().cell(), b.x().cell())?;
region.constrain_equal(a.x().cell(), b.x().cell())?;
// Constrain x-coordinates
region.constrain_equal(&config.perm, a.y().cell(), b.y().cell())
region.constrain_equal(a.y().cell(), b.y().cell())
},
)
}

13
src/circuit/gadget/ecc/chip/add.rs
View File

@ -5,7 +5,7 @@ use ff::Field;
use halo2::{
arithmetic::BatchInvert,
circuit::Region,
plonk::{Advice, Column, ConstraintSystem, Error, Expression, Permutation, Selector},
plonk::{Advice, Column, ConstraintSystem, Error, Expression, Selector},
poly::Rotation,
};
use pasta_curves::{arithmetic::FieldExt, pallas};
@ -32,8 +32,6 @@ pub struct Config {
gamma: Column<Advice>,
// δ = inv0(y_p + y_q) if x_q = x_p, 0 otherwise
delta: Column<Advice>,
// Permutation
perm: Permutation,
}
impl From<&EccConfig> for Config {
@ -49,7 +47,6 @@ impl From<&EccConfig> for Config {
beta: ecc_config.advices[6],
gamma: ecc_config.advices[7],
delta: ecc_config.advices[8],
perm: ecc_config.perm.clone(),
}
}
}
@ -208,12 +205,12 @@ impl Config {
self.q_add.enable(region, offset)?;
// Copy point `p` into `x_p`, `y_p` columns
copy(region, || "x_p", self.x_p, offset, &p.x, &self.perm)?;
copy(region, || "y_p", self.y_p, offset, &p.y, &self.perm)?;
copy(region, || "x_p", self.x_p, offset, &p.x)?;
copy(region, || "y_p", self.y_p, offset, &p.y)?;
// Copy point `q` into `x_qr`, `y_qr` columns
copy(region, || "x_q", self.x_qr, offset, &q.x, &self.perm)?;
copy(region, || "y_q", self.y_qr, offset, &q.y, &self.perm)?;
copy(region, || "x_q", self.x_qr, offset, &q.x)?;
copy(region, || "y_q", self.y_qr, offset, &q.y)?;
let (x_p, y_p) = (p.x.value(), p.y.value());
let (x_q, y_q) = (q.x.value(), q.y.value());

13
src/circuit/gadget/ecc/chip/add_incomplete.rs
View File

@ -4,7 +4,7 @@ use super::{copy, CellValue, EccConfig, EccPoint, Var};
use group::Curve;
use halo2::{
circuit::Region,
plonk::{Advice, Column, ConstraintSystem, Error, Permutation, Selector},
plonk::{Advice, Column, ConstraintSystem, Error, Selector},
poly::Rotation,
};
use pasta_curves::{arithmetic::CurveAffine, pallas};
@ -20,8 +20,6 @@ pub struct Config {
pub x_qr: Column<Advice>,
// y-coordinate of Q or R in P + Q = R
pub y_qr: Column<Advice>,
// Permutation
perm: Permutation,
}
impl From<&EccConfig> for Config {
@ -32,7 +30,6 @@ impl From<&EccConfig> for Config {
y_p: ecc_config.advices[1],
x_qr: ecc_config.advices[2],
y_qr: ecc_config.advices[3],
perm: ecc_config.perm.clone(),
}
}
}
@ -99,12 +96,12 @@ impl Config {
.transpose()?;
// Copy point `p` into `x_p`, `y_p` columns
copy(region, || "x_p", self.x_p, offset, &p.x, &self.perm)?;
copy(region, || "y_p", self.y_p, offset, &p.y, &self.perm)?;
copy(region, || "x_p", self.x_p, offset, &p.x)?;
copy(region, || "y_p", self.y_p, offset, &p.y)?;
// Copy point `q` into `x_qr`, `y_qr` columns
copy(region, || "x_q", self.x_qr, offset, &q.x, &self.perm)?;
copy(region, || "y_q", self.y_qr, offset, &q.y, &self.perm)?;
copy(region, || "x_q", self.x_qr, offset, &q.x)?;
copy(region, || "y_q", self.y_qr, offset, &q.y)?;
// Compute the sum `P + Q = R`
let r = {

7
src/circuit/gadget/ecc/chip/mul.rs
View File

@ -7,7 +7,7 @@ use ff::PrimeField;
use halo2::{
arithmetic::FieldExt,
circuit::{Layouter, Region},
plonk::{Column, ConstraintSystem, Error, Expression, Fixed, Permutation, Selector},
plonk::{Column, ConstraintSystem, Error, Expression, Fixed, Selector},
poly::Rotation,
};
@ -44,8 +44,6 @@ pub struct Config {
constants: Column<Fixed>,
// Selector used to check switching logic on LSB
q_mul_lsb: Selector,
// Permutation
perm: Permutation,
// Configuration used in complete addition
add_config: add::Config,
// Configuration used for `hi` bits of the scalar
@ -63,7 +61,6 @@ impl From<&EccConfig> for Config {
let config = Self {
constants: ecc_config.constants,
q_mul_lsb: ecc_config.q_mul_lsb,
perm: ecc_config.perm.clone(),
add_config: ecc_config.into(),
hi_config: ecc_config.into(),
lo_config: ecc_config.into(),
@ -318,7 +315,6 @@ impl Config {
self.add_config.x_p,
offset + 1,
&base.x(),
&self.perm,
)?;
copy(
region,
@ -326,7 +322,6 @@ impl Config {
self.add_config.y_p,
offset + 1,
&base.y(),
&self.perm,
)?;
// If `lsb` is 0, return `Acc + (-P)`. If `lsb` is 1, simply return `Acc + 0`.

7
src/circuit/gadget/ecc/chip/mul/complete.rs
View File

@ -3,7 +3,7 @@ use super::{COMPLETE_RANGE, X, Y, Z};
use halo2::{
circuit::Region,
plonk::{Advice, Column, ConstraintSystem, Error, Expression, Permutation, Selector},
plonk::{Advice, Column, ConstraintSystem, Error, Expression, Selector},
poly::Rotation,
};
@ -14,8 +14,6 @@ pub struct Config {
q_mul_decompose_var: Selector,
// Advice column used to decompose scalar in complete addition.
pub z_complete: Column<Advice>,
// Permutation
perm: Permutation,
// Configuration used in complete addition
add_config: add::Config,
}
@ -25,7 +23,6 @@ impl From<&EccConfig> for Config {
let config = Self {
q_mul_decompose_var: ecc_config.q_mul_decompose_var,
z_complete: ecc_config.advices[9],
perm: ecc_config.perm.clone(),
add_config: ecc_config.into(),
};
@ -113,7 +110,6 @@ impl Config {
self.z_complete,
offset,
&z,
&self.perm,
)?;
Z(z)
};
@ -150,7 +146,6 @@ impl Config {
self.z_complete,
row + offset + 1,
&base.y,
&self.perm,
)?;
// If the bit is set, use `y`; if the bit is not set, use `-y`

28
src/circuit/gadget/ecc/chip/mul/incomplete.rs
View File

@ -5,9 +5,7 @@ use super::{INCOMPLETE_HI_RANGE, INCOMPLETE_LO_RANGE, X, Y, Z};
use ff::Field;
use halo2::{
circuit::Region,
plonk::{
Advice, Column, ConstraintSystem, Error, Expression, Fixed, Permutation, VirtualCells,
},
plonk::{Advice, Column, ConstraintSystem, Error, Expression, Fixed, VirtualCells},
poly::Rotation,
};
@ -30,8 +28,6 @@ pub(super) struct Config {
pub(super) lambda1: Column<Advice>,
// lambda2 in each double-and-add iteration.
pub(super) lambda2: Column<Advice>,
// Permutation
pub(super) perm: Permutation,
}
// Columns used in processing the `hi` bits of the scalar.
@ -48,7 +44,6 @@ impl From<&EccConfig> for HiConfig {
x_a: ecc_config.advices[3],
lambda1: ecc_config.advices[4],
lambda2: ecc_config.advices[5],
perm: ecc_config.perm.clone(),
};
Self(config)
}
@ -75,7 +70,6 @@ impl From<&EccConfig> for LoConfig {
x_a: ecc_config.advices[7],
lambda1: ecc_config.advices[8],
lambda2: ecc_config.advices[2],
perm: ecc_config.perm.clone(),
};
Self(config)
}
@ -285,25 +279,11 @@ impl Config {
// Initialise double-and-add
let (mut x_a, mut y_a, mut z) = {
// Initialise the running `z` sum for the scalar bits.
let z = copy(region, || "starting z", self.z, offset, &acc.2, &self.perm)?;
let z = copy(region, || "starting z", self.z, offset, &acc.2)?;
// Initialise acc
let x_a = copy(
region,
|| "starting x_a",
self.x_a,
offset + 1,
&acc.0,
&self.perm,
)?;
let y_a = copy(
region,
|| "starting y_a",
self.lambda1,
offset,
&acc.1,
&self.perm,
)?;
let x_a = copy(region, || "starting x_a", self.x_a, offset + 1, &acc.0)?;
let y_a = copy(region, || "starting y_a", self.lambda1, offset, &acc.1)?;
(x_a, y_a.value(), z)
};

27
src/circuit/gadget/ecc/chip/mul/overflow.rs
View File

@ -6,7 +6,7 @@ use crate::{
};
use halo2::{
circuit::Layouter,
plonk::{Advice, Column, ConstraintSystem, Error, Expression, Permutation, Selector},
plonk::{Advice, Column, ConstraintSystem, Error, Expression, Selector},
poly::Rotation,
};
@ -22,8 +22,6 @@ pub struct Config {
lookup_config: LookupRangeCheckConfig<pallas::Base, { sinsemilla::K }>,
// Advice columns
advices: [Column<Advice>; 3],
// Permutation
perm: Permutation,
}
impl From<&EccConfig> for Config {
@ -36,7 +34,6 @@ impl From<&EccConfig> for Config {
ecc_config.advices[1],
ecc_config.advices[2],
],
perm: ecc_config.perm.clone(),
}
}
}
@ -137,14 +134,7 @@ impl Config {
self.q_mul_overflow.enable(&mut region, offset + 1)?;
// Copy `z_0`
copy(
&mut region,
|| "copy z_0",
self.advices[0],
offset,
&*zs[0],
&self.perm,
)?;
copy(&mut region, || "copy z_0", self.advices[0], offset, &*zs[0])?;
// Copy `z_130`
copy(
@ -153,7 +143,6 @@ impl Config {
self.advices[0],
offset + 1,
&*zs[130],
&self.perm,
)?;
// Witness η = inv0(z_130), where inv0(x) = 0 if x = 0, 1/x otherwise
@ -180,7 +169,6 @@ impl Config {
self.advices[1],
offset,
&*zs[254],
&self.perm,
)?;
// Copy original alpha
@ -190,7 +178,6 @@ impl Config {
self.advices[1],
offset + 1,
&alpha,
&self.perm,
)?;
// Copy weighted sum of the decomposition of s = alpha + k_254 ⋅ 2^130.
@ -200,18 +187,10 @@ impl Config {
self.advices[1],
offset + 2,
&s_minus_lo_130,
&self.perm,
)?;
// Copy witnessed s to check that it was properly derived from alpha and k_254.
copy(
&mut region,
|| "copy s",
self.advices[2],
offset + 1,
&s,
&self.perm,
)?;
copy(&mut region, || "copy s", self.advices[2], offset + 1, &s)?;
Ok(())
},

8
src/circuit/gadget/ecc/chip/mul_fixed.rs
View File

@ -10,10 +10,7 @@ use crate::constants::{
use group::Curve;
use halo2::{
circuit::Region,
plonk::{
Advice, Column, ConstraintSystem, Error, Expression, Fixed, Permutation, Selector,
VirtualCells,
},
plonk::{Advice, Column, ConstraintSystem, Error, Expression, Fixed, Selector, VirtualCells},
poly::Rotation,
};
use lazy_static::lazy_static;
@ -94,8 +91,6 @@ pub struct Config<const NUM_WINDOWS: usize> {
y_p: Column<Advice>,
// y-coordinate of accumulator (only used in the final row).
u: Column<Advice>,
// Permutation
perm: Permutation,
// Configuration for `add`
add_config: add::Config,
// Configuration for `add_incomplete`
@ -112,7 +107,6 @@ impl<const NUM_WINDOWS: usize> From<&EccConfig> for Config<NUM_WINDOWS> {
y_p: ecc_config.advices[1],
window: ecc_config.advices[4],
u: ecc_config.advices[5],
perm: ecc_config.perm.clone(),
add_config: ecc_config.into(),
add_incomplete_config: ecc_config.into(),
};

8
src/circuit/gadget/ecc/chip/mul_fixed/base_field_elem.rs
View File

@ -273,8 +273,6 @@ impl Config {
layouter.assign_region(
|| "Canonicity checks",
|mut region| {
let perm = &self.super_config.perm;
// Activate canonicity check gate
self.q_mul_fixed_base_field.enable(&mut region, 1)?;
@ -289,7 +287,6 @@ impl Config {
self.canon_advices[0],
offset,
&alpha,
perm,
)?;
// z_84_alpha = the top three bits of alpha.
@ -299,7 +296,6 @@ impl Config {
self.canon_advices[2],
offset,
&z_84_alpha,
perm,
)?;
}
@ -314,7 +310,6 @@ impl Config {
self.canon_advices[0],
offset,
&alpha_0_prime,
perm,
)?;
// Decompose α into three pieces,
@ -349,7 +344,6 @@ impl Config {
self.canon_advices[0],
offset,
&z_13_alpha_0_prime,
perm,
)?;
// Copy z_44_alpha
@ -359,7 +353,6 @@ impl Config {
self.canon_advices[1],
offset,
&z_44_alpha,
perm,
)?;
// Copy z_43_alpha
@ -369,7 +362,6 @@ impl Config {
self.canon_advices[2],
offset,
&z_43_alpha,
perm,
)?;
}

14
src/circuit/gadget/ecc/chip/mul_fixed/short.rs
View File

@ -145,7 +145,6 @@ impl Config {
self.super_config.window,
offset,
&scalar.sign,
&self.super_config.perm,
)?;
// Copy last window to `u` column.
@ -158,7 +157,6 @@ impl Config {
self.super_config.u,
offset,
&z_21,
&self.super_config.perm,
)?;
// Conditionally negate `y`-coordinate
@ -406,18 +404,10 @@ pub mod tests {
meta.advice_column(),
meta.advice_column(),
];
let constants = [meta.fixed_column(), meta.fixed_column()];
let perm = meta.permutation(
&advices
.iter()
.map(|advice| (*advice).into())
.chain(constants.iter().map(|fixed| (*fixed).into()))
.collect::<Vec<_>>(),
);
let lookup_table = meta.fixed_column();
EccChip::configure(meta, advices, lookup_table, constants, perm)
EccChip::configure(meta, advices, lookup_table, constants)
}
fn synthesize(

39
src/circuit/gadget/poseidon/pow5t3.rs
View File

@ -1,7 +1,9 @@
use std::iter;
use halo2::{
arithmetic::FieldExt,
circuit::{Cell, Chip, Layouter, Region},
plonk::{Advice, Column, ConstraintSystem, Error, Expression, Fixed, Permutation, Selector},
plonk::{Advice, Column, ConstraintSystem, Error, Expression, Fixed, Selector},
poly::Rotation,
};
@ -14,7 +16,6 @@ const WIDTH: usize = 3;
#[derive(Clone, Debug)]
pub struct Pow5T3Config<F: FieldExt> {
state: [Column<Advice>; WIDTH],
state_permutation: Permutation,
partial_sbox: Column<Advice>,
rc_a: [Column<Fixed>; WIDTH],
rc_b: [Column<Fixed>; WIDTH],
@ -38,6 +39,10 @@ pub struct Pow5T3Chip<F: FieldExt> {
impl<F: FieldExt> Pow5T3Chip<F> {
/// Configures this chip for use in a circuit.
///
/// # Side-effects
///
/// All columns in `state` will be equality-enabled.
//
// TODO: Does the rate need to be hard-coded here, or only the width? It probably
// needs to be known wherever we implement the hashing gadget, but it isn't strictly
@ -73,17 +78,12 @@ impl<F: FieldExt> Pow5T3Chip<F> {
// every permutation round, while rc_b is empty in the initial and final full
// rounds, so we use rc_b as "scratch space" for fixed values (enabling potential
// layouter optimisations).
let state_permutation = Permutation::new(
meta,
&[
state[0].into(),
state[1].into(),
state[2].into(),
rc_b[0].into(),
rc_b[1].into(),
rc_b[2].into(),
],
);
for column in iter::empty()
.chain(state.iter().cloned().map(|c| c.into()))
.chain(rc_b.iter().cloned().map(|c| c.into()))
{
meta.enable_equality(column);
}
let s_full = meta.selector();
let s_partial = meta.selector();
@ -195,7 +195,6 @@ impl<F: FieldExt> Pow5T3Chip<F> {
Pow5T3Config {
state,
state_permutation,
partial_sbox,
rc_a,
rc_b,
@ -302,7 +301,7 @@ impl<F: FieldExt, S: Spec<F, WIDTH, 2>> PoseidonDuplexInstructions<F, S, WIDTH,
0,
|| Ok(value),
)?;
region.constrain_equal(&config.state_permutation, var, fixed)?;
region.constrain_equal(var, fixed)?;
Ok(StateWord {
var,
value: Some(value),
@ -340,7 +339,7 @@ impl<F: FieldExt, S: Spec<F, WIDTH, 2>> PoseidonDuplexInstructions<F, S, WIDTH,
0,
|| value.ok_or(Error::SynthesisError),
)?;
region.constrain_equal(&config.state_permutation, initial_state[i].var, var)?;
region.constrain_equal(initial_state[i].var, var)?;
Ok(StateWord { var, value })
};
let initial_state = [
@ -372,7 +371,7 @@ impl<F: FieldExt, S: Spec<F, WIDTH, 2>> PoseidonDuplexInstructions<F, S, WIDTH,
1,
|| value.ok_or(Error::SynthesisError),
)?;
region.constrain_equal(&config.state_permutation, constraint_var, var)?;
region.constrain_equal(constraint_var, var)?;
Ok(StateWord { var, value })
};
@ -541,7 +540,7 @@ impl<F: FieldExt> Pow5T3State<F> {
0,
|| value.ok_or(Error::SynthesisError),
)?;
region.constrain_equal(&config.state_permutation, initial_state[i].var, var)?;
region.constrain_equal(initial_state[i].var, var)?;
Ok(StateWord { var, value })
};
@ -686,7 +685,7 @@ mod tests {
0,
|| Ok(expected_final_state[i]),
)?;
region.constrain_equal(&config.state_permutation, final_state[i].var, var)
region.constrain_equal(final_state[i].var, var)
};
final_state_word(0)?;
@ -771,7 +770,7 @@ mod tests {
|| self.output.ok_or(Error::SynthesisError),
)?;
let word: StateWord<_> = output.inner;
region.constrain_equal(&config.state_permutation, word.var, expected_var)
region.constrain_equal(word.var, expected_var)
},
)
}

15
src/circuit/gadget/sinsemilla.rs
View File

@ -366,32 +366,19 @@ mod tests {
// Fixed columns for the Sinsemilla generator lookup table
let lookup = (table_idx, meta.fixed_column(), meta.fixed_column());
let perm = meta.permutation(
&advices
.iter()
.map(|advice| (*advice).into())
.chain(constants_1.iter().map(|fixed| (*fixed).into()))
.chain(constants_2.iter().map(|fixed| (*fixed).into()))
.chain(ecc_constants.iter().map(|fixed| (*fixed).into()))
.collect::<Vec<_>>(),
);
let ecc_config =
EccChip::configure(meta, advices, table_idx, ecc_constants, perm.clone());
let ecc_config = EccChip::configure(meta, advices, table_idx, ecc_constants);
let config1 = SinsemillaChip::configure(
meta,
advices[..5].try_into().unwrap(),
lookup,
constants_1,
perm.clone(),
);
let config2 = SinsemillaChip::configure(
meta,
advices[5..].try_into().unwrap(),
lookup,
constants_2,
perm,
);
(ecc_config, config1, config2)
}

70
src/circuit/gadget/sinsemilla/chip.rs
View File

@ -15,10 +15,7 @@ use crate::{
use halo2::{
arithmetic::{CurveAffine, FieldExt},
circuit::{Chip, Layouter},
plonk::{
Advice, Column, ConstraintSystem, Error, Expression, Fixed, Permutation, Selector,
VirtualCells,
},
plonk::{Advice, Column, ConstraintSystem, Error, Expression, Fixed, Selector, VirtualCells},
poly::Rotation,
};
use pasta_curves::pallas;
@ -62,8 +59,6 @@ pub struct SinsemillaConfig {
/// x-coordinate of the domain $Q$, which is then constrained to equal the
/// initial $x_a$.
pub(super) constants: Column<Fixed>,
/// Permutation over all advice columns and the `constants` fixed column.
pub(super) perm: Permutation,
/// Configure each advice column to be able to perform lookup range checks.
pub(super) lookup_config_0: LookupRangeCheckConfig<pallas::Base, { sinsemilla::K }>,
pub(super) lookup_config_1: LookupRangeCheckConfig<pallas::Base, { sinsemilla::K }>,
@ -110,6 +105,9 @@ impl SinsemillaChip {
config.generator_table.load(layouter)
}
/// # Side-effects
///
/// All columns in `advices` and `constants` will be equality-enabled.
#[allow(clippy::too_many_arguments)]
#[allow(non_snake_case)]
pub fn configure(
@ -117,8 +115,23 @@ impl SinsemillaChip {
advices: [Column<Advice>; 5],
lookup: (Column<Fixed>, Column<Fixed>, Column<Fixed>),
constants: [Column<Fixed>; 6], // TODO: replace with public inputs API
perm: Permutation,
) -> <Self as Chip<pallas::Base>>::Config {
// This chip requires all advice columns and the `constants` fixed column to be
// equality-enabled. The advice columns are equality-enabled by the calls to
// LookupRangeCheckConfig::configure.
let lookup_config_0 =
LookupRangeCheckConfig::configure(meta, advices[0], constants[0], lookup.0);
let lookup_config_1 =
LookupRangeCheckConfig::configure(meta, advices[1], constants[1], lookup.0);
let lookup_config_2 =
LookupRangeCheckConfig::configure(meta, advices[2], constants[2], lookup.0);
let lookup_config_3 =
LookupRangeCheckConfig::configure(meta, advices[3], constants[3], lookup.0);
let lookup_config_4 =
LookupRangeCheckConfig::configure(meta, advices[4], constants[4], lookup.0);
let constants = constants[5];
meta.enable_equality(constants.into());
let config = SinsemillaConfig {
q_sinsemilla1: meta.selector(),
q_sinsemilla2: meta.fixed_column(),
@ -133,43 +146,12 @@ impl SinsemillaChip {
table_x: lookup.1,
table_y: lookup.2,
},
constants: constants[5],
lookup_config_0: LookupRangeCheckConfig::configure(
meta,
advices[0],
constants[0],
lookup.0,
perm.clone(),
),
lookup_config_1: LookupRangeCheckConfig::configure(
meta,
advices[1],
constants[1],
lookup.0,
perm.clone(),
),
lookup_config_2: LookupRangeCheckConfig::configure(
meta,
advices[2],
constants[2],
lookup.0,
perm.clone(),
),
lookup_config_3: LookupRangeCheckConfig::configure(
meta,
advices[3],
constants[3],
lookup.0,
perm.clone(),
),
lookup_config_4: LookupRangeCheckConfig::configure(
meta,
advices[4],
constants[4],
lookup.0,
perm.clone(),
),
perm,
constants,
lookup_config_0,
lookup_config_1,
lookup_config_2,
lookup_config_3,
lookup_config_4,
};
// Set up lookup argument

11
src/circuit/gadget/sinsemilla/chip/hash_to_point.rs
View File

@ -47,14 +47,7 @@ impl SinsemillaChip {
CellValue::new(cell, Some(x_q))
};
let x_a = copy(
region,
|| "x_q",
config.x_a,
offset,
&fixed_x_q,
&config.perm,
)?;
let x_a = copy(region, || "x_q", config.x_a, offset, &fixed_x_q)?;
// Constrain the initial x_a, lambda_1, lambda_2, x_p using the fixed y_q
// initializer. Assign `fixed_y_q` to be zero on every other row.
@ -291,7 +284,7 @@ impl SinsemillaChip {
offset,
|| piece.field_elem().ok_or(Error::SynthesisError),
)?;
region.constrain_equal(&config.perm, piece.cell(), cell)?;
region.constrain_equal(piece.cell(), cell)?;
zs.push(CellValue::new(cell, piece.field_elem()));
// Assign cumulative sum such that for 0 <= i < n,

11
src/circuit/gadget/sinsemilla/merkle.rs
View File

@ -206,15 +206,6 @@ pub mod tests {
meta.fixed_column(),
];
let perm = meta.permutation(
&advices
.iter()
.map(|advice| (*advice).into())
.chain(constants_1.iter().map(|fixed| (*fixed).into()))
.chain(constants_2.iter().map(|fixed| (*fixed).into()))
.collect::<Vec<_>>(),
);
// Fixed columns for the Sinsemilla generator lookup table
let lookup = (
meta.fixed_column(),
@ -227,7 +218,6 @@ pub mod tests {
advices[5..].try_into().unwrap(),
lookup,
constants_1,
perm.clone(),
);
let config1 = MerkleChip::configure(meta, sinsemilla_config_1);
@ -236,7 +226,6 @@ pub mod tests {
advices[..5].try_into().unwrap(),
lookup,
constants_2,
perm,
);
let config2 = MerkleChip::configure(meta, sinsemilla_config_2);

66
src/circuit/gadget/sinsemilla/merkle/chip.rs
View File

@ -1,6 +1,6 @@
use halo2::{
circuit::{Chip, Layouter},
plonk::{Advice, Column, ConstraintSystem, Error, Expression, Fixed, Permutation},
plonk::{Advice, Column, ConstraintSystem, Error, Expression, Fixed},
poly::Rotation,
};
use pasta_curves::{arithmetic::FieldExt, pallas};
@ -26,7 +26,6 @@ use std::{array, convert::TryInto};
pub struct MerkleConfig {
advices: [Column<Advice>; 5],
l_plus_1: Column<Fixed>,
perm: Permutation,
pub(super) cond_swap_config: CondSwapConfig,
pub(super) sinsemilla_config: SinsemillaConfig,
}
@ -54,9 +53,10 @@ impl MerkleChip {
meta: &mut ConstraintSystem<pallas::Base>,
sinsemilla_config: SinsemillaConfig,
) -> MerkleConfig {
// TODO: Check whether these advice columns were equality-enabled by
// SinsemillaConfig. We require all five columns to be equality-enabled.
let advices = sinsemilla_config.advices();
let cond_swap_config =
CondSwapChip::configure(meta, advices, sinsemilla_config.perm.clone());
let cond_swap_config = CondSwapChip::configure(meta, advices);
// This fixed column serves two purposes:
// - Fixing the value of l* for rows in which a Merkle path layer
@ -153,7 +153,6 @@ impl MerkleChip {
MerkleConfig {
advices,
l_plus_1,
perm: sinsemilla_config.perm.clone(),
cond_swap_config,
sinsemilla_config,
}
@ -298,7 +297,6 @@ impl MerkleInstructions<pallas::Affine, MERKLE_DEPTH_ORCHARD, { sinsemilla::K },
config.advices[0],
0,
&a.cell_value(),
&config.perm,
)?;
// Copy and assign `b` at the correct position.
copy(
@ -307,7 +305,6 @@ impl MerkleInstructions<pallas::Affine, MERKLE_DEPTH_ORCHARD, { sinsemilla::K },
config.advices[1],
0,
&b.cell_value(),
&config.perm,
)?;
// Copy and assign `c` at the correct position.
copy(
@ -316,64 +313,21 @@ impl MerkleInstructions<pallas::Affine, MERKLE_DEPTH_ORCHARD, { sinsemilla::K },
config.advices[2],
0,
&c.cell_value(),
&config.perm,
)?;
// Copy and assign the left node at the correct position.
copy(
&mut region,
|| "left",
config.advices[3],
0,
&left,
&config.perm,
)?;
copy(&mut region, || "left", config.advices[3], 0, &left)?;
// Copy and assign the right node at the correct position.
copy(
&mut region,
|| "right",
config.advices[4],
0,
&right,
&config.perm,
)?;
copy(&mut region, || "right", config.advices[4], 0, &right)?;
// Offset 1
// Copy and assign z_1 of SinsemillaHash(a) = a_1
copy(
&mut region,
|| "z1_a",
config.advices[0],
1,
&z1_a,
&config.perm,
)?;
copy(&mut region, || "z1_a", config.advices[0], 1, &z1_a)?;
// Copy and assign z_1 of SinsemillaHash(b) = b_1
copy(
&mut region,
|| "z1_b",
config.advices[1],
1,
&z1_b,
&config.perm,
)?;
copy(&mut region, || "z1_b", config.advices[1], 1, &z1_b)?;
// Copy `b_1`, which has been constrained to be a 5-bit value
copy(
&mut region,
|| "b_1",
config.advices[2],
1,
&b_1,
&config.perm,
)?;
copy(&mut region, || "b_1", config.advices[2], 1, &b_1)?;
// Copy `b_2`, which has been constrained to be a 5-bit value
copy(
&mut region,
|| "b_2",
config.advices[3],
1,
&b_2,
&config.perm,
)?;
copy(&mut region, || "b_2", config.advices[3], 1, &b_2)?;
Ok(())
},

14
src/circuit/gadget/utilities.rs
View File

@ -1,7 +1,7 @@
use ff::PrimeFieldBits;
use halo2::{
circuit::{Cell, Layouter, Region},
plonk::{Advice, Column, Error, Expression, Permutation},
plonk::{Advice, Column, Error, Expression},
};
use pasta_curves::arithmetic::FieldExt;
use std::{array, convert::TryInto, ops::Range};
@ -66,14 +66,16 @@ pub trait UtilitiesInstructions<F: FieldExt> {
/// Assigns a cell at a specific offset within the given region, constraining it
/// to the same value as another cell (which may be in any region).
///
/// Returns an error if either `column` or `copy` is not within `perm`.
/// Returns an error if either `column` or `copy` is not in a column that was passed to
/// [`ConstraintSystem::enable_equality`] during circuit configuration.
///
/// [`ConstraintSystem::enable_equality`]: halo2::plonk::ConstraintSystem::enable_equality
pub fn copy<A, AR, F: FieldExt>(
region: &mut Region<'_, F>,
annotation: A,
column: Column<Advice>,
offset: usize,
copy: &CellValue<F>,
perm: &Permutation,
) -> Result<CellValue<F>, Error>
where
A: Fn() -> AR,
@ -83,7 +85,7 @@ where
copy.value.ok_or(Error::SynthesisError)
})?;
region.constrain_equal(perm, cell, copy.cell)?;
region.constrain_equal(cell, copy.cell)?;
Ok(CellValue::new(cell, copy.value))
}
@ -203,13 +205,13 @@ mod tests {
for i in 0..8 {
let circuit: MyCircuit<8> = MyCircuit(i);
let prover = MockProver::<pallas::Base>::run(1, &circuit, vec![]).unwrap();
let prover = MockProver::<pallas::Base>::run(3, &circuit, vec![]).unwrap();
assert_eq!(prover.verify(), Ok(()));
}
{
let circuit: MyCircuit<8> = MyCircuit(8);
let prover = MockProver::<pallas::Base>::run(1, &circuit, vec![]).unwrap();
let prover = MockProver::<pallas::Base>::run(3, &circuit, vec![]).unwrap();
assert_eq!(
prover.verify(),
Err(vec![VerifyFailure::Constraint {

29
src/circuit/gadget/utilities/cond_swap.rs
View File

@ -1,7 +1,7 @@
use super::{copy, CellValue, UtilitiesInstructions, Var};
use halo2::{
circuit::{Chip, Layouter},
plonk::{Advice, Column, ConstraintSystem, Error, Expression, Permutation, Selector},
plonk::{Advice, Column, ConstraintSystem, Error, Expression, Selector},
poly::Rotation,
};
use pasta_curves::arithmetic::FieldExt;
@ -50,7 +50,6 @@ pub struct CondSwapConfig {
pub a_swapped: Column<Advice>,
pub b_swapped: Column<Advice>,
pub swap: Column<Advice>,
pub perm: Permutation,
}
impl<F: FieldExt> UtilitiesInstructions<F> for CondSwapChip<F> {
@ -74,7 +73,7 @@ impl<F: FieldExt> CondSwapInstructions<F> for CondSwapChip<F> {
config.q_swap.enable(&mut region, 0)?;
// Copy in `a` value
let a = copy(&mut region, || "copy a", config.a, 0, &pair.0, &config.perm)?;
let a = copy(&mut region, || "copy a", config.a, 0, &pair.0)?;
// Witness `b` value
let b = {
@ -144,23 +143,26 @@ impl<F: FieldExt> CondSwapInstructions<F> for CondSwapChip<F> {
impl<F: FieldExt> CondSwapChip<F> {
/// Configures this chip for use in a circuit.
///
/// `perm` must cover `advices[0..2]`, as well as any columns that will
/// be passed to this chip.
/// # Side-effects
///
/// `advices[0]` will be equality-enabled.
pub fn configure(
meta: &mut ConstraintSystem<F>,
advices: [Column<Advice>; 5],
perm: Permutation,
) -> CondSwapConfig {
let a = advices[0];
// Only column a is used in an equality constraint directly by this chip.
meta.enable_equality(a.into());
let q_swap = meta.selector();
let config = CondSwapConfig {
q_swap,
a: advices[0],
a,
b: advices[1],
a_swapped: advices[2],
b_swapped: advices[3],
swap: advices[4],
perm,
};
// TODO: optimise shape of gate for Merkle path validation
@ -212,7 +214,7 @@ mod tests {
use halo2::{
circuit::{Layouter, SimpleFloorPlanner},
dev::MockProver,
plonk::{Any, Circuit, Column, ConstraintSystem, Error},
plonk::{Circuit, ConstraintSystem, Error},
};
use pasta_curves::{arithmetic::FieldExt, pallas::Base};
@ -242,14 +244,7 @@ mod tests {
meta.advice_column(),
];
let perm = meta.permutation(
&advices
.iter()
.map(|advice| (*advice).into())
.collect::<Vec<Column<Any>>>(),
);
CondSwapChip::<F>::configure(meta, advices, perm)
CondSwapChip::<F>::configure(meta, advices)
}
fn synthesize(

23
src/circuit/gadget/utilities/decompose_running_sum.rs
View File

@ -25,7 +25,7 @@
use ff::PrimeFieldBits;
use halo2::{
circuit::Region,
plonk::{Advice, Column, ConstraintSystem, Error, Permutation, Selector},
plonk::{Advice, Column, ConstraintSystem, Error, Selector},
poly::Rotation,
};
@ -48,7 +48,6 @@ pub struct RunningSumConfig<F: FieldExt + PrimeFieldBits, const WINDOW_NUM_BITS:
q_range_check: Selector,
q_strict: Selector,
pub z: Column<Advice>,
perm: Permutation,
_marker: PhantomData<F>,
}
@ -60,19 +59,23 @@ impl<F: FieldExt + PrimeFieldBits, const WINDOW_NUM_BITS: usize>
/// # Panics
///
/// Panics if WINDOW_NUM_BITS > 3.
///
/// # Side-effects
///
/// `z` will be equality-enabled.
pub fn configure(
meta: &mut ConstraintSystem<F>,
q_range_check: Selector,
z: Column<Advice>,
perm: Permutation,
) -> Self {
assert!(WINDOW_NUM_BITS <= 3);
meta.enable_equality(z.into());
let config = Self {
q_range_check,
q_strict: meta.selector(),
z,
perm,
_marker: PhantomData,
};
@ -135,14 +138,7 @@ impl<F: FieldExt + PrimeFieldBits, const WINDOW_NUM_BITS: usize>
word_num_bits: usize,
num_windows: usize,
) -> Result<(CellValue<F>, RunningSum<F>), Error> {
let z_0 = copy(
region,
|| "copy z_0 = alpha",
self.z,
offset,
&alpha,
&self.perm,
)?;
let z_0 = copy(region, || "copy z_0 = alpha", self.z, offset, &alpha)?;
self.decompose(region, offset, z_0, strict, word_num_bits, num_windows)
}
@ -276,9 +272,8 @@ mod tests {
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
let z = meta.advice_column();
let q_range_check = meta.selector();
let perm = meta.permutation(&[z.into()]);
RunningSumConfig::<F, WINDOW_NUM_BITS>::configure(meta, q_range_check, z, perm)
RunningSumConfig::<F, WINDOW_NUM_BITS>::configure(meta, q_range_check, z)
}
fn synthesize(

43
src/circuit/gadget/utilities/enable_flag.rs
View File

@ -1,7 +1,7 @@
use super::{copy, CellValue, UtilitiesInstructions};
use halo2::{
circuit::{Chip, Layouter},
plonk::{Advice, Column, ConstraintSystem, Error, Expression, Permutation, Selector},
plonk::{Advice, Column, ConstraintSystem, Error, Expression, Selector},
poly::Rotation,
};
use pasta_curves::arithmetic::FieldExt;
@ -22,7 +22,6 @@ pub struct EnableFlagConfig {
q_enable: Selector,
value: Column<Advice>,
enable_flag: Column<Advice>,
perm: Permutation,
}
/// A chip implementing an enable flag.
@ -73,14 +72,7 @@ impl<F: FieldExt> EnableFlagInstructions<F> for EnableFlagChip<F> {
)?;
// Copy `value`
copy(
&mut region,
|| "copy value",
config.value,
0,
&value,
&config.perm,
)?;
copy(&mut region, || "copy value", config.value, 0, &value)?;
Ok(())
},
@ -91,20 +83,22 @@ impl<F: FieldExt> EnableFlagInstructions<F> for EnableFlagChip<F> {
impl<F: FieldExt> EnableFlagChip<F> {
/// Configures this chip for use in a circuit.
///
/// `perm` must cover `advices[0]`, as well as any columns that will be
/// passed to this chip.
/// # Side-effects
///
/// `advices[0]` will be equality-enabled.
pub fn configure(
meta: &mut ConstraintSystem<F>,
advices: [Column<Advice>; 2],
perm: Permutation,
) -> EnableFlagConfig {
let value = advices[0];
meta.enable_equality(value.into());
let q_enable = meta.selector();
let config = EnableFlagConfig {
q_enable,
value: advices[0],
value,
enable_flag: advices[1],
perm,
};
meta.create_gate("Enable flag", |meta| {
@ -133,7 +127,7 @@ mod tests {
use halo2::{
circuit::{Layouter, SimpleFloorPlanner},
dev::{MockProver, VerifyFailure},
plonk::{Any, Circuit, Column, ConstraintSystem, Error},
plonk::{Circuit, ConstraintSystem, Error},
};
use pasta_curves::{arithmetic::FieldExt, pallas::Base};
@ -156,14 +150,7 @@ mod tests {
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
let advices = [meta.advice_column(), meta.advice_column()];
let perm = meta.permutation(
&advices
.iter()
.map(|advice| (*advice).into())
.collect::<Vec<Column<Any>>>(),
);
EnableFlagChip::<F>::configure(meta, advices, perm)
EnableFlagChip::<F>::configure(meta, advices)
}
fn synthesize(
@ -190,7 +177,7 @@ mod tests {
value: Some(Base::one()),
enable_flag: Some(true),
};
let prover = MockProver::<Base>::run(1, &circuit, vec![]).unwrap();
let prover = MockProver::<Base>::run(3, &circuit, vec![]).unwrap();
assert_eq!(prover.verify(), Ok(()));
}
@ -200,7 +187,7 @@ mod tests {
value: Some(Base::zero()),
enable_flag: Some(false),
};
let prover = MockProver::<Base>::run(1, &circuit, vec![]).unwrap();
let prover = MockProver::<Base>::run(3, &circuit, vec![]).unwrap();
assert_eq!(prover.verify(), Ok(()));
}
@ -210,7 +197,7 @@ mod tests {
value: Some(Base::zero()),
enable_flag: Some(true),
};
let prover = MockProver::<Base>::run(1, &circuit, vec![]).unwrap();
let prover = MockProver::<Base>::run(3, &circuit, vec![]).unwrap();
assert_eq!(prover.verify(), Ok(()));
}
@ -220,7 +207,7 @@ mod tests {
value: Some(Base::one()),
enable_flag: Some(false),
};
let prover = MockProver::<Base>::run(1, &circuit, vec![]).unwrap();
let prover = MockProver::<Base>::run(3, &circuit, vec![]).unwrap();
assert_eq!(
prover.verify(),
Err(vec![VerifyFailure::Constraint {

53
src/circuit/gadget/utilities/lookup_range_check.rs
View File

@ -4,7 +4,7 @@
use crate::spec::lebs2ip;
use halo2::{
circuit::{Layouter, Region},
plonk::{Advice, Column, ConstraintSystem, Error, Fixed, Permutation, Selector},
plonk::{Advice, Column, ConstraintSystem, Error, Fixed, Selector},
poly::Rotation,
};
use std::{convert::TryInto, marker::PhantomData};
@ -21,7 +21,6 @@ pub struct LookupRangeCheckConfig<F: FieldExt + PrimeFieldBits, const K: usize>
pub running_sum: Column<Advice>,
constants: Column<Fixed>,
table_idx: Column<Fixed>,
perm: Permutation,
_marker: PhantomData<F>,
}
@ -33,13 +32,19 @@ impl<F: FieldExt + PrimeFieldBits, const K: usize> LookupRangeCheckConfig<F, K>
/// The `table_idx` fixed column contains values from [0..2^K). Looking up
/// a value in `table_idx` constrains it to be within this range. The table
/// can be loaded outside this helper.
///
/// # Side-effects
///
/// Both the `running_sum` and `constants` columns will be equality-enabled.
pub fn configure(
meta: &mut ConstraintSystem<F>,
running_sum: Column<Advice>,
constants: Column<Fixed>,
table_idx: Column<Fixed>,
perm: Permutation,
) -> Self {
meta.enable_equality(running_sum.into());
meta.enable_equality(constants.into());
let q_lookup = meta.selector();
let q_lookup_short = meta.selector();
let short_lookup_bitshift = meta.fixed_column();
@ -50,7 +55,6 @@ impl<F: FieldExt + PrimeFieldBits, const K: usize> LookupRangeCheckConfig<F, K>
running_sum,
constants,
table_idx,
perm,
_marker: PhantomData,
};
@ -115,6 +119,9 @@ impl<F: FieldExt + PrimeFieldBits, const K: usize> LookupRangeCheckConfig<F, K>
}
/// Range check on an existing cell that is copied into this helper.
///
/// Returns an error if `element` is not in a column that was passed to
/// [`ConstraintSystem::enable_equality`] during circuit configuration.
pub fn copy_check(
&self,
mut layouter: impl Layouter<F>,
@ -126,14 +133,7 @@ impl<F: FieldExt + PrimeFieldBits, const K: usize> LookupRangeCheckConfig<F, K>
|| format!("{:?} words range check", num_words),
|mut region| {
// Copy `element` and initialize running sum `z_0 = element` to decompose it.
let z_0 = copy(
&mut region,
|| "z_0",
self.running_sum,
0,
&element,
&self.perm,
)?;
let z_0 = copy(&mut region, || "z_0", self.running_sum, 0, &element)?;
self.range_check(&mut region, z_0, num_words, strict)
},
@ -247,7 +247,7 @@ impl<F: FieldExt + PrimeFieldBits, const K: usize> LookupRangeCheckConfig<F, K>
// Constrain the final `z` to be zero.
let cell =
region.assign_fixed(|| "zero", self.constants, words.len(), || Ok(F::zero()))?;
region.constrain_equal(&self.perm, z.cell(), cell)?;
region.constrain_equal(z.cell(), cell)?;
}
Ok(zs)
@ -269,14 +269,7 @@ impl<F: FieldExt + PrimeFieldBits, const K: usize> LookupRangeCheckConfig<F, K>
|| format!("Range check {:?} bits", num_bits),
|mut region| {
// Copy `element` to use in the k-bit lookup.
let element = copy(
&mut region,
|| "element",
self.running_sum,
0,
&element,
&self.perm,
)?;
let element = copy(&mut region, || "element", self.running_sum, 0, &element)?;
self.short_range_check(&mut region, element, num_bits)
},
@ -397,15 +390,8 @@ mod tests {
let running_sum = meta.advice_column();
let constants = meta.fixed_column();
let table_idx = meta.fixed_column();
let perm = meta.permutation(&[running_sum.into(), constants.into()]);
LookupRangeCheckConfig::<F, K>::configure(
meta,
running_sum,
constants,
table_idx,
perm,
)
LookupRangeCheckConfig::<F, K>::configure(meta, running_sum, constants, table_idx)
}
fn synthesize(
@ -509,15 +495,8 @@ mod tests {
let running_sum = meta.advice_column();
let constants = meta.fixed_column();
let table_idx = meta.fixed_column();
let perm = meta.permutation(&[running_sum.into()]);
LookupRangeCheckConfig::<F, K>::configure(
meta,
running_sum,
constants,
table_idx,
perm,
)
LookupRangeCheckConfig::<F, K>::configure(meta, running_sum, constants, table_idx)
}
fn synthesize(

44
src/circuit/gadget/utilities/plonk.rs
View File

@ -1,7 +1,7 @@
use super::{copy, CellValue, UtilitiesInstructions};
use halo2::{
circuit::{Chip, Layouter},
plonk::{Advice, Column, ConstraintSystem, Error, Fixed, Permutation},
plonk::{Advice, Column, ConstraintSystem, Error, Fixed},
poly::Rotation,
};
use pasta_curves::arithmetic::FieldExt;
@ -44,8 +44,6 @@ pub struct PLONKConfig {
sb: Column<Fixed>,
sc: Column<Fixed>,
sm: Column<Fixed>,
perm: Permutation,
}
#[allow(clippy::upper_case_acronyms)]
@ -90,13 +88,13 @@ impl<F: FieldExt> PLONKInstructions<F> for PLONKChip<F> {
let config = self.config().clone();
// Copy in `a`
copy(&mut region, || "copy a", config.a, 0, &a, &config.perm)?;
copy(&mut region, || "copy a", config.a, 0, &a)?;
// Copy in `b`
copy(&mut region, || "copy b", config.b, 0, &b, &config.perm)?;
copy(&mut region, || "copy b", config.b, 0, &b)?;
// Copy in `c`
copy(&mut region, || "copy c", config.c, 0, &c, &config.perm)?;
copy(&mut region, || "copy c", config.c, 0, &c)?;
// Assign fixed columns
region.assign_fixed(|| "sc", config.sc, 0, || sc.ok_or(Error::SynthesisError))?;
@ -138,13 +136,13 @@ impl<F: FieldExt> PLONKInstructions<F> for PLONKChip<F> {
|| "add",
|mut region| {
// Copy in `a`
copy(&mut region, || "copy a", config.a, 0, &a, &config.perm)?;
copy(&mut region, || "copy a", config.a, 0, &a)?;
// Copy in `b`
copy(&mut region, || "copy b", config.b, 0, &b, &config.perm)?;
copy(&mut region, || "copy b", config.b, 0, &b)?;
// Copy in `c`
copy(&mut region, || "copy c", config.c, 0, &c, &config.perm)?;
copy(&mut region, || "copy c", config.c, 0, &c)?;
// Assign fixed columns
region.assign_fixed(|| "a", config.sa, 0, || sa.ok_or(Error::SynthesisError))?;
@ -171,16 +169,16 @@ impl<F: FieldExt> PLONKInstructions<F> for PLONKChip<F> {
impl<F: FieldExt> PLONKChip<F> {
/// Configures this chip for use in a circuit.
///
/// `perm` must cover `advices`, as well as any columns that will be passed
/// to this chip.
pub fn configure(
meta: &mut ConstraintSystem<F>,
advices: [Column<Advice>; 3],
perm: Permutation,
) -> PLONKConfig {
/// # Side-effects
///
/// All columns in `advices` will be equality-enabled.
pub fn configure(meta: &mut ConstraintSystem<F>, advices: [Column<Advice>; 3]) -> PLONKConfig {
let a = advices[0];
let b = advices[1];
let c = advices[2];
meta.enable_equality(a.into());
meta.enable_equality(b.into());
meta.enable_equality(c.into());
let sa = meta.fixed_column();
let sb = meta.fixed_column();
@ -208,7 +206,6 @@ impl<F: FieldExt> PLONKChip<F> {
sb,
sc,
sm,
perm,
}
}
@ -227,7 +224,7 @@ mod tests {
use halo2::{
circuit::{Layouter, SimpleFloorPlanner},
dev::MockProver,
plonk::{Any, Circuit, Column, ConstraintSystem, Error},
plonk::{Circuit, ConstraintSystem, Error},
};
use pasta_curves::{arithmetic::FieldExt, pallas::Base};
@ -254,14 +251,7 @@ mod tests {
meta.advice_column(),
];
let perm = meta.permutation(
&advices
.iter()
.map(|advice| (*advice).into())
.collect::<Vec<Column<Any>>>(),
);
PLONKChip::<F>::configure(meta, advices, perm)
PLONKChip::<F>::configure(meta, advices)
}
fn synthesize(
@ -343,7 +333,7 @@ mod tests {
a: Some(Base::rand()),
b: Some(Base::rand()),
};
let prover = MockProver::<Base>::run(3, &circuit, vec![]).unwrap();
let prover = MockProver::<Base>::run(4, &circuit, vec![]).unwrap();
assert_eq!(prover.verify(), Ok(()));
}
}