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

halo2_proofs: Replace `Option<V>` with `Value<V>`

This commit is contained in:
Jack Grigg 2022-06-07 23:15:35 +00:00
parent c17d52e5bf
commit 47f25ad632
19 changed files with 401 additions and 339 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
halo2_proofs/CHANGELOG.md
View File

@ -9,6 +9,36 @@ and this project adheres to Rust's notion of
### Added
- `halo2_proofs::circuit::Value`, a more usable and type-safe replacement for
`Option<V>` in circuit synthesis.
- `impl Mul<F: Field> for &Assigned<F>`
### Changed
All APIs that represented witnessed values as `Option<V>` now represent them as
`halo2_proofs::circuit::Value<V>`. The core API changes are listed below.
- The following APIs now take `Value<_>` instead of `Option<_>`:
- `halo2_proofs::plonk`:
- `Assignment::fill_from_row`
- The following APIs now take value closures that return `Value<V>` instead of
`Result<V, Error>`:
- `halo2_proofs::circuit`:
- `Region::{assign_advice, assign_fixed}`
- `Table::assign_cell`
- `halo2_proofs::circuit::layouter`:
- `RegionLayouter::{assign_advice, assign_fixed}`
- `TableLayouter::assign_cell`
- `halo2_proofs::plonk`:
- `Assignment::{assign_advice, assign_fixed}`
- The following APIs now return `Value<_>` instead of `Option<_>`:
- `halo2_proofs::circuit`:
- `AssignedCell::{value, value_field}`
- The following APIs now return `Result<Value<F>, Error>` instead of
`Result<Option<F>, Error>`:
- `halo2_proofs::plonk`:
- `Assignment::query_instance`
- The following APIs now return `Result<(Cell, Value<F>), Error>` instead of
`Result<(Cell, Option<F>), Error>`:
- `halo2_proofs::circuit::layouter`:
- `RegionLayouter::assign_advice_from_instance`
## [0.1.0] - 2022-05-10
### Added

6
halo2_proofs/benches/dev_lookup.rs
View File

@ -2,7 +2,7 @@
extern crate criterion;
use halo2_proofs::arithmetic::FieldExt;
use halo2_proofs::circuit::{Layouter, SimpleFloorPlanner};
use halo2_proofs::circuit::{Layouter, SimpleFloorPlanner, Value};
use halo2_proofs::dev::MockProver;
use halo2_proofs::plonk::*;
use halo2_proofs::poly::Rotation;
@ -63,7 +63,7 @@ fn criterion_benchmark(c: &mut Criterion) {
|| format!("row {}", row),
config.table,
row as usize,
|| Ok(F::from(row + 1)),
|| Value::known(F::from(row + 1)),
)?;
}
@ -80,7 +80,7 @@ fn criterion_benchmark(c: &mut Criterion) {
|| format!("offset {}", offset),
config.advice,
offset as usize,
|| Ok(F::from((offset % 256) + 1)),
|| Value::known(F::from((offset % 256) + 1)),
)?;
}

87
halo2_proofs/benches/plonk.rs
View File

@ -3,7 +3,7 @@ extern crate criterion;
use group::ff::Field;
use halo2_proofs::arithmetic::FieldExt;
use halo2_proofs::circuit::{Cell, Layouter, SimpleFloorPlanner};
use halo2_proofs::circuit::{Cell, Layouter, SimpleFloorPlanner, Value};
use halo2_proofs::pasta::{EqAffine, Fp};
use halo2_proofs::plonk::*;
use halo2_proofs::poly::{commitment::Params, Rotation};
@ -38,20 +38,20 @@ fn criterion_benchmark(c: &mut Criterion) {
f: F,
) -> Result<(Cell, Cell, Cell), Error>
where
F: FnMut() -> Result<(FF, FF, FF), Error>;
F: FnMut() -> Value<(Assigned<FF>, Assigned<FF>, Assigned<FF>)>;
fn raw_add<F>(
&self,
layouter: &mut impl Layouter<FF>,
f: F,
) -> Result<(Cell, Cell, Cell), Error>
where
F: FnMut() -> Result<(FF, FF, FF), Error>;
F: FnMut() -> Value<(Assigned<FF>, Assigned<FF>, Assigned<FF>)>;
fn copy(&self, layouter: &mut impl Layouter<FF>, a: Cell, b: Cell) -> Result<(), Error>;
}
#[derive(Clone)]
struct MyCircuit<F: FieldExt> {
a: Option<F>,
a: Value<F>,
k: u32,
}
@ -76,7 +76,7 @@ fn criterion_benchmark(c: &mut Criterion) {
mut f: F,
) -> Result<(Cell, Cell, Cell), Error>
where
F: FnMut() -> Result<(FF, FF, FF), Error>,
F: FnMut() -> Value<(Assigned<FF>, Assigned<FF>, Assigned<FF>)>,
{
layouter.assign_region(
|| "raw_multiply",
@ -87,27 +87,32 @@ fn criterion_benchmark(c: &mut Criterion) {
self.config.a,
0,
|| {
value = Some(f()?);
Ok(value.ok_or(Error::Synthesis)?.0)
value = Some(f());
value.unwrap().map(|v| v.0)
},
)?;
let rhs = region.assign_advice(
|| "rhs",
self.config.b,
0,
|| Ok(value.ok_or(Error::Synthesis)?.1),
|| value.unwrap().map(|v| v.1),
)?;
let out = region.assign_advice(
|| "out",
self.config.c,
0,
|| Ok(value.ok_or(Error::Synthesis)?.2),
|| value.unwrap().map(|v| v.2),
)?;
region.assign_fixed(|| "a", self.config.sa, 0, || Ok(FF::zero()))?;
region.assign_fixed(|| "b", self.config.sb, 0, || Ok(FF::zero()))?;
region.assign_fixed(|| "c", self.config.sc, 0, || Ok(FF::one()))?;
region.assign_fixed(|| "a * b", self.config.sm, 0, || Ok(FF::one()))?;
region.assign_fixed(|| "a", self.config.sa, 0, || Value::known(FF::zero()))?;
region.assign_fixed(|| "b", self.config.sb, 0, || Value::known(FF::zero()))?;
region.assign_fixed(|| "c", self.config.sc, 0, || Value::known(FF::one()))?;
region.assign_fixed(
|| "a * b",
self.config.sm,
0,
|| Value::known(FF::one()),
)?;
Ok((lhs.cell(), rhs.cell(), out.cell()))
},
)
@ -118,7 +123,7 @@ fn criterion_benchmark(c: &mut Criterion) {
mut f: F,
) -> Result<(Cell, Cell, Cell), Error>
where
F: FnMut() -> Result<(FF, FF, FF), Error>,
F: FnMut() -> Value<(Assigned<FF>, Assigned<FF>, Assigned<FF>)>,
{
layouter.assign_region(
|| "raw_add",
@ -129,27 +134,32 @@ fn criterion_benchmark(c: &mut Criterion) {
self.config.a,
0,
|| {
value = Some(f()?);
Ok(value.ok_or(Error::Synthesis)?.0)
value = Some(f());
value.unwrap().map(|v| v.0)
},
)?;
let rhs = region.assign_advice(
|| "rhs",
self.config.b,
0,
|| Ok(value.ok_or(Error::Synthesis)?.1),
|| value.unwrap().map(|v| v.1),
)?;
let out = region.assign_advice(
|| "out",
self.config.c,
0,
|| Ok(value.ok_or(Error::Synthesis)?.2),
|| value.unwrap().map(|v| v.2),
)?;
region.assign_fixed(|| "a", self.config.sa, 0, || Ok(FF::one()))?;
region.assign_fixed(|| "b", self.config.sb, 0, || Ok(FF::one()))?;
region.assign_fixed(|| "c", self.config.sc, 0, || Ok(FF::one()))?;
region.assign_fixed(|| "a * b", self.config.sm, 0, || Ok(FF::zero()))?;
region.assign_fixed(|| "a", self.config.sa, 0, || Value::known(FF::one()))?;
region.assign_fixed(|| "b", self.config.sb, 0, || Value::known(FF::one()))?;
region.assign_fixed(|| "c", self.config.sc, 0, || Value::known(FF::one()))?;
region.assign_fixed(
|| "a * b",
self.config.sm,
0,
|| Value::known(FF::zero()),
)?;
Ok((lhs.cell(), rhs.cell(), out.cell()))
},
)
@ -169,7 +179,10 @@ fn criterion_benchmark(c: &mut Criterion) {
type FloorPlanner = SimpleFloorPlanner;
fn without_witnesses(&self) -> Self {
Self { a: None, k: self.k }
Self {
a: Value::unknown(),
k: self.k,
}
}
fn configure(meta: &mut ConstraintSystem<F>) -> PlonkConfig {
@ -220,22 +233,17 @@ fn criterion_benchmark(c: &mut Criterion) {
let cs = StandardPlonk::new(config);
for _ in 0..((1 << (self.k - 1)) - 3) {
let mut a_squared = None;
let a: Value<Assigned<_>> = self.a.into();
let mut a_squared = Value::unknown();
let (a0, _, c0) = cs.raw_multiply(&mut layouter, || {
a_squared = self.a.map(|a| a.square());
Ok((
self.a.ok_or(Error::Synthesis)?,
self.a.ok_or(Error::Synthesis)?,
a_squared.ok_or(Error::Synthesis)?,
))
a_squared = a.square();
a.zip(a_squared).map(|(a, a_squared)| (a, a, a_squared))
})?;
let (a1, b1, _) = cs.raw_add(&mut layouter, || {
let fin = a_squared.and_then(|a2| self.a.map(|a| a + a2));
Ok((
self.a.ok_or(Error::Synthesis)?,
a_squared.ok_or(Error::Synthesis)?,
fin.ok_or(Error::Synthesis)?,
))
let fin = a_squared + a;
a.zip(a_squared)
.zip(fin)
.map(|((a, a_squared), fin)| (a, a_squared, fin))
})?;
cs.copy(&mut layouter, a0, a1)?;
cs.copy(&mut layouter, b1, c0)?;
@ -247,7 +255,10 @@ fn criterion_benchmark(c: &mut Criterion) {
fn keygen(k: u32) -> (Params<EqAffine>, ProvingKey<EqAffine>) {
let params: Params<EqAffine> = Params::new(k);
let empty_circuit: MyCircuit<Fp> = MyCircuit { a: None, k };
let empty_circuit: MyCircuit<Fp> = MyCircuit {
a: Value::unknown(),
k,
};
let vk = keygen_vk(&params, &empty_circuit).expect("keygen_vk should not fail");
let pk = keygen_pk(&params, vk, &empty_circuit).expect("keygen_pk should not fail");
(params, pk)
@ -257,7 +268,7 @@ fn criterion_benchmark(c: &mut Criterion) {
let rng = OsRng;
let circuit: MyCircuit<Fp> = MyCircuit {
a: Some(Fp::random(rng)),
a: Value::known(Fp::random(rng)),
k,
};

110
halo2_proofs/examples/circuit-layout.rs
View File

@ -1,9 +1,9 @@
use ff::Field;
use halo2_proofs::{
arithmetic::FieldExt,
circuit::{Cell, Layouter, Region, SimpleFloorPlanner},
circuit::{Cell, Layouter, Region, SimpleFloorPlanner, Value},
pasta::Fp,
plonk::{Advice, Circuit, Column, ConstraintSystem, Error, Fixed, TableColumn},
plonk::{Advice, Assigned, Circuit, Column, ConstraintSystem, Error, Fixed, TableColumn},
poly::Rotation,
};
use rand_core::OsRng;
@ -31,16 +31,16 @@ struct PlonkConfig {
trait StandardCs<FF: FieldExt> {
fn raw_multiply<F>(&self, region: &mut Region<FF>, f: F) -> Result<(Cell, Cell, Cell), Error>
where
F: FnMut() -> Result<(FF, FF, FF), Error>;
F: FnMut() -> Value<(Assigned<FF>, Assigned<FF>, Assigned<FF>)>;
fn raw_add<F>(&self, region: &mut Region<FF>, f: F) -> Result<(Cell, Cell, Cell), Error>
where
F: FnMut() -> Result<(FF, FF, FF), Error>;
F: FnMut() -> Value<(Assigned<FF>, Assigned<FF>, Assigned<FF>)>;
fn copy(&self, region: &mut Region<FF>, a: Cell, b: Cell) -> Result<(), Error>;
fn lookup_table(&self, layouter: &mut impl Layouter<FF>, values: &[FF]) -> Result<(), Error>;
}
struct MyCircuit<F: FieldExt> {
a: Option<F>,
a: Value<F>,
lookup_table: Vec<F>,
}
@ -65,7 +65,7 @@ impl<FF: FieldExt> StandardCs<FF> for StandardPlonk<FF> {
mut f: F,
) -> Result<(Cell, Cell, Cell), Error>
where
F: FnMut() -> Result<(FF, FF, FF), Error>,
F: FnMut() -> Value<(Assigned<FF>, Assigned<FF>, Assigned<FF>)>,
{
let mut value = None;
let lhs = region.assign_advice(
@ -73,44 +73,36 @@ impl<FF: FieldExt> StandardCs<FF> for StandardPlonk<FF> {
self.config.a,
0,
|| {
value = Some(f()?);
Ok(value.ok_or(Error::Synthesis)?.0)
value = Some(f());
value.unwrap().map(|v| v.0)
},
)?;
region.assign_advice(
|| "lhs^4",
self.config.d,
0,
|| Ok(value.ok_or(Error::Synthesis)?.0.square().square()),
)?;
let rhs = region.assign_advice(
|| "rhs",
self.config.b,
0,
|| Ok(value.ok_or(Error::Synthesis)?.1),
|| value.unwrap().map(|v| v.0).square().square(),
)?;
let rhs =
region.assign_advice(|| "rhs", self.config.b, 0, || value.unwrap().map(|v| v.1))?;
region.assign_advice(
|| "rhs^4",
self.config.e,
0,
|| Ok(value.ok_or(Error::Synthesis)?.1.square().square()),
)?;
let out = region.assign_advice(
|| "out",
self.config.c,
0,
|| Ok(value.ok_or(Error::Synthesis)?.2),
|| value.unwrap().map(|v| v.1).square().square(),
)?;
let out =
region.assign_advice(|| "out", self.config.c, 0, || value.unwrap().map(|v| v.2))?;
region.assign_fixed(|| "a", self.config.sa, 0, || Ok(FF::zero()))?;
region.assign_fixed(|| "b", self.config.sb, 0, || Ok(FF::zero()))?;
region.assign_fixed(|| "c", self.config.sc, 0, || Ok(FF::one()))?;
region.assign_fixed(|| "a * b", self.config.sm, 0, || Ok(FF::one()))?;
region.assign_fixed(|| "a", self.config.sa, 0, || Value::known(FF::zero()))?;
region.assign_fixed(|| "b", self.config.sb, 0, || Value::known(FF::zero()))?;
region.assign_fixed(|| "c", self.config.sc, 0, || Value::known(FF::one()))?;
region.assign_fixed(|| "a * b", self.config.sm, 0, || Value::known(FF::one()))?;
Ok((lhs.cell(), rhs.cell(), out.cell()))
}
fn raw_add<F>(&self, region: &mut Region<FF>, mut f: F) -> Result<(Cell, Cell, Cell), Error>
where
F: FnMut() -> Result<(FF, FF, FF), Error>,
F: FnMut() -> Value<(Assigned<FF>, Assigned<FF>, Assigned<FF>)>,
{
let mut value = None;
let lhs = region.assign_advice(
@ -118,39 +110,31 @@ impl<FF: FieldExt> StandardCs<FF> for StandardPlonk<FF> {
self.config.a,
0,
|| {
value = Some(f()?);
Ok(value.ok_or(Error::Synthesis)?.0)
value = Some(f());
value.unwrap().map(|v| v.0)
},
)?;
region.assign_advice(
|| "lhs^4",
self.config.d,
0,
|| Ok(value.ok_or(Error::Synthesis)?.0.square().square()),
)?;
let rhs = region.assign_advice(
|| "rhs",
self.config.b,
0,
|| Ok(value.ok_or(Error::Synthesis)?.1),
|| value.unwrap().map(|v| v.0.square().square()),
)?;
let rhs =
region.assign_advice(|| "rhs", self.config.b, 0, || value.unwrap().map(|v| v.1))?;
region.assign_advice(
|| "rhs^4",
self.config.e,
0,
|| Ok(value.ok_or(Error::Synthesis)?.1.square().square()),
)?;
let out = region.assign_advice(
|| "out",
self.config.c,
0,
|| Ok(value.ok_or(Error::Synthesis)?.2),
|| value.unwrap().map(|v| v.1.square().square()),
)?;
let out =
region.assign_advice(|| "out", self.config.c, 0, || value.unwrap().map(|v| v.2))?;
region.assign_fixed(|| "a", self.config.sa, 0, || Ok(FF::one()))?;
region.assign_fixed(|| "b", self.config.sb, 0, || Ok(FF::one()))?;
region.assign_fixed(|| "c", self.config.sc, 0, || Ok(FF::one()))?;
region.assign_fixed(|| "a * b", self.config.sm, 0, || Ok(FF::zero()))?;
region.assign_fixed(|| "a", self.config.sa, 0, || Value::known(FF::one()))?;
region.assign_fixed(|| "b", self.config.sb, 0, || Value::known(FF::one()))?;
region.assign_fixed(|| "c", self.config.sc, 0, || Value::known(FF::one()))?;
region.assign_fixed(|| "a * b", self.config.sm, 0, || Value::known(FF::zero()))?;
Ok((lhs.cell(), rhs.cell(), out.cell()))
}
fn copy(&self, region: &mut Region<FF>, left: Cell, right: Cell) -> Result<(), Error> {
@ -161,7 +145,12 @@ impl<FF: FieldExt> StandardCs<FF> for StandardPlonk<FF> {
|| "",
|mut table| {
for (index, &value) in values.iter().enumerate() {
table.assign_cell(|| "table col", self.config.sl, index, || Ok(value))?;
table.assign_cell(
|| "table col",
self.config.sl,
index,
|| Value::known(value),
)?;
}
Ok(())
},
@ -176,7 +165,7 @@ impl<F: FieldExt> Circuit<F> for MyCircuit<F> {
fn without_witnesses(&self) -> Self {
Self {
a: None,
a: Value::unknown(),
lookup_table: self.lookup_table.clone(),
}
}
@ -257,22 +246,17 @@ impl<F: FieldExt> Circuit<F> for MyCircuit<F> {
layouter.assign_region(
|| format!("region_{}", i),
|mut region| {
let mut a_squared = None;
let a: Value<Assigned<_>> = self.a.into();
let mut a_squared = Value::unknown();
let (a0, _, c0) = cs.raw_multiply(&mut region, || {
a_squared = self.a.map(|a| a.square());
Ok((
self.a.ok_or(Error::Synthesis)?,
self.a.ok_or(Error::Synthesis)?,
a_squared.ok_or(Error::Synthesis)?,
))
a_squared = a.square();
a.zip(a_squared).map(|(a, a_squared)| (a, a, a_squared))
})?;
let (a1, b1, _) = cs.raw_add(&mut region, || {
let fin = a_squared.and_then(|a2| self.a.map(|a| a + a2));
Ok((
self.a.ok_or(Error::Synthesis)?,
a_squared.ok_or(Error::Synthesis)?,
fin.ok_or(Error::Synthesis)?,
))
let fin = a_squared + a;
a.zip(a_squared)
.zip(fin)
.map(|((a, a_squared), fin)| (a, a_squared, fin))
})?;
cs.copy(&mut region, a0, a1)?;
cs.copy(&mut region, b1, c0)
@ -294,7 +278,7 @@ fn main() {
let instance = Fp::one() + Fp::one();
let lookup_table = vec![instance, a, a, Fp::zero()];
let circuit: MyCircuit<Fp> = MyCircuit {
a: None,
a: Value::unknown(),
lookup_table,
};

30
halo2_proofs/examples/simple-example.rs
View File

@ -2,7 +2,7 @@ use std::marker::PhantomData;
use halo2_proofs::{
arithmetic::FieldExt,
circuit::{AssignedCell, Chip, Layouter, Region, SimpleFloorPlanner},
circuit::{AssignedCell, Chip, Layouter, Region, SimpleFloorPlanner, Value},
plonk::{Advice, Circuit, Column, ConstraintSystem, Error, Fixed, Instance, Selector},
poly::Rotation,
};
@ -13,7 +13,7 @@ trait NumericInstructions<F: FieldExt>: Chip<F> {
type Num;
/// Loads a number into the circuit as a private input.
fn load_private(&self, layouter: impl Layouter<F>, a: Option<F>) -> Result<Self::Num, Error>;
fn load_private(&self, layouter: impl Layouter<F>, a: Value<F>) -> Result<Self::Num, Error>;
/// Loads a number into the circuit as a fixed constant.
fn load_constant(&self, layouter: impl Layouter<F>, constant: F) -> Result<Self::Num, Error>;
@ -151,7 +151,7 @@ impl<F: FieldExt> NumericInstructions<F> for FieldChip<F> {
fn load_private(
&self,
mut layouter: impl Layouter<F>,
value: Option<F>,
value: Value<F>,
) -> Result<Self::Num, Error> {
let config = self.config();
@ -159,12 +159,7 @@ impl<F: FieldExt> NumericInstructions<F> for FieldChip<F> {
|| "load private",
|mut region| {
region
.assign_advice(
|| "private input",
config.advice[0],
0,
|| value.ok_or(Error::Synthesis),
)
.assign_advice(|| "private input", config.advice[0], 0, || value)
.map(Number)
},
)
@ -212,17 +207,12 @@ impl<F: FieldExt> NumericInstructions<F> for FieldChip<F> {
// Now we can assign the multiplication result, which is to be assigned
// into the output position.
let value = a.0.value().and_then(|a| b.0.value().map(|b| *a * *b));
let value = a.0.value().copied() * b.0.value();
// Finally, we do the assignment to the output, returning a
// variable to be used in another part of the circuit.
region
.assign_advice(
|| "lhs * rhs",
config.advice[0],
1,
|| value.ok_or(Error::Synthesis),
)
.assign_advice(|| "lhs * rhs", config.advice[0], 1, || value)
.map(Number)
},
)
@ -250,8 +240,8 @@ impl<F: FieldExt> NumericInstructions<F> for FieldChip<F> {
#[derive(Default)]
struct MyCircuit<F: FieldExt> {
constant: F,
a: Option<F>,
b: Option<F>,
a: Value<F>,
b: Value<F>,
}
impl<F: FieldExt> Circuit<F> for MyCircuit<F> {
@ -329,8 +319,8 @@ fn main() {
// Instantiate the circuit with the private inputs.
let circuit = MyCircuit {
constant,
a: Some(a),
b: Some(b),
a: Value::known(a),
b: Value::known(b),
};
// Arrange the public input. We expose the multiplication result in row 0

47
halo2_proofs/examples/two-chip.rs
View File

@ -2,7 +2,7 @@ use std::marker::PhantomData;
use halo2_proofs::{
arithmetic::FieldExt,
circuit::{AssignedCell, Chip, Layouter, Region, SimpleFloorPlanner},
circuit::{AssignedCell, Chip, Layouter, Region, SimpleFloorPlanner, Value},
plonk::{Advice, Circuit, Column, ConstraintSystem, Error, Instance, Selector},
poly::Rotation,
};
@ -20,7 +20,7 @@ trait FieldInstructions<F: FieldExt>: AddInstructions<F> + MulInstructions<F> {
fn load_private(
&self,
layouter: impl Layouter<F>,
a: Option<F>,
a: Value<F>,
) -> Result<<Self as FieldInstructions<F>>::Num, Error>;
/// Returns `d = (a + b) * c`.
@ -217,17 +217,12 @@ impl<F: FieldExt> AddInstructions<F> for AddChip<F> {
// Now we can compute the addition result, which is to be assigned
// into the output position.
let value = a.0.value().and_then(|a| b.0.value().map(|b| *a + *b));
let value = a.0.value().copied() + b.0.value();
// Finally, we do the assignment to the output, returning a
// variable to be used in another part of the circuit.
region
.assign_advice(
|| "lhs + rhs",
config.advice[0],
1,
|| value.ok_or(Error::Synthesis),
)
.assign_advice(|| "lhs + rhs", config.advice[0], 1, || value)
.map(Number)
},
)
@ -343,17 +338,12 @@ impl<F: FieldExt> MulInstructions<F> for MulChip<F> {
// Now we can compute the multiplication result, which is to be assigned
// into the output position.
let value = a.0.value().and_then(|a| b.0.value().map(|b| *a * *b));
let value = a.0.value().copied() * b.0.value();
// Finally, we do the assignment to the output, returning a
// variable to be used in another part of the circuit.
region
.assign_advice(
|| "lhs * rhs",
config.advice[0],
1,
|| value.ok_or(Error::Synthesis),
)
.assign_advice(|| "lhs * rhs", config.advice[0], 1, || value)
.map(Number)
},
)
@ -412,7 +402,7 @@ impl<F: FieldExt> FieldInstructions<F> for FieldChip<F> {
fn load_private(
&self,
mut layouter: impl Layouter<F>,
value: Option<F>,
value: Value<F>,
) -> Result<<Self as FieldInstructions<F>>::Num, Error> {
let config = self.config();
@ -420,12 +410,7 @@ impl<F: FieldExt> FieldInstructions<F> for FieldChip<F> {
|| "load private",
|mut region| {
region
.assign_advice(
|| "private input",
config.advice[0],
0,
|| value.ok_or(Error::Synthesis),
)
.assign_advice(|| "private input", config.advice[0], 0, || value)
.map(Number)
},
)
@ -459,14 +444,14 @@ impl<F: FieldExt> FieldInstructions<F> for FieldChip<F> {
// ANCHOR: circuit
/// The full circuit implementation.
///
/// In this struct we store the private input variables. We use `Option<F>` because
/// In this struct we store the private input variables. We use `Value<F>` because
/// they won't have any value during key generation. During proving, if any of these
/// were `None` we would get an error.
/// were `Value::unknown()` we would get an error.
#[derive(Default)]
struct MyCircuit<F: FieldExt> {
a: Option<F>,
b: Option<F>,
c: Option<F>,
a: Value<F>,
b: Value<F>,
c: Value<F>,
}
impl<F: FieldExt> Circuit<F> for MyCircuit<F> {
@ -529,9 +514,9 @@ fn main() {
// Instantiate the circuit with the private inputs.
let circuit = MyCircuit {
a: Some(a),
b: Some(b),
c: Some(c),
a: Value::known(a),
b: Value::known(b),
c: Value::known(c),
};
// Arrange the public input. We expose the multiplication result in row 0

45
halo2_proofs/src/circuit.rs
View File

@ -98,14 +98,14 @@ pub struct Cell {
/// An assigned cell.
#[derive(Clone, Debug)]
pub struct AssignedCell<V, F: Field> {
value: Option<V>,
value: Value<V>,
cell: Cell,
_marker: PhantomData<F>,
}
impl<V, F: Field> AssignedCell<V, F> {
/// Returns the value of the [`AssignedCell`].
pub fn value(&self) -> Option<&V> {
pub fn value(&self) -> Value<&V> {
self.value.as_ref()
}
@ -120,8 +120,8 @@ where
for<'v> Assigned<F>: From<&'v V>,
{
/// Returns the field element value of the [`AssignedCell`].
pub fn value_field(&self) -> Option<Assigned<F>> {
self.value().map(|v| v.into())
pub fn value_field(&self) -> Value<Assigned<F>> {
self.value.to_field()
}
}
@ -132,7 +132,7 @@ impl<F: Field> AssignedCell<Assigned<F>, F> {
/// If the denominator is zero, the returned cell's value is zero.
pub fn evaluate(self) -> AssignedCell<F, F> {
AssignedCell {
value: self.value.map(|v| v.evaluate()),
value: self.value.evaluate(),
cell: self.cell,
_marker: Default::default(),
}
@ -158,9 +158,8 @@ where
A: Fn() -> AR,
AR: Into<String>,
{
let assigned_cell = region.assign_advice(annotation, column, offset, || {
self.value.clone().ok_or(Error::Synthesis)
})?;
let assigned_cell =
region.assign_advice(annotation, column, offset, || self.value.clone())?;
region.constrain_equal(assigned_cell.cell(), self.cell())?;
Ok(assigned_cell)
@ -216,19 +215,19 @@ impl<'r, F: Field> Region<'r, F> {
mut to: V,
) -> Result<AssignedCell<VR, F>, Error>
where
V: FnMut() -> Result<VR, Error> + 'v,
V: FnMut() -> Value<VR> + 'v,
for<'vr> Assigned<F>: From<&'vr VR>,
A: Fn() -> AR,
AR: Into<String>,
{
let mut value = None;
let mut value = Value::unknown();
let cell =
self.region
.assign_advice(&|| annotation().into(), column, offset, &mut || {
let v = to()?;
let value_f = (&v).into();
value = Some(v);
Ok(value_f)
let v = to();
let value_f = v.to_field();
value = v;
value_f
})?;
Ok(AssignedCell {
@ -264,7 +263,7 @@ impl<'r, F: Field> Region<'r, F> {
)?;
Ok(AssignedCell {
value: Some(constant),
value: Value::known(constant),
cell,
_marker: PhantomData,
})
@ -312,19 +311,19 @@ impl<'r, F: Field> Region<'r, F> {
mut to: V,
) -> Result<AssignedCell<VR, F>, Error>
where
V: FnMut() -> Result<VR, Error> + 'v,
V: FnMut() -> Value<VR> + 'v,
for<'vr> Assigned<F>: From<&'vr VR>,
A: Fn() -> AR,
AR: Into<String>,
{
let mut value = None;
let mut value = Value::unknown();
let cell =
self.region
.assign_fixed(&|| annotation().into(), column, offset, &mut || {
let v = to()?;
let value_f = (&v).into();
value = Some(v);
Ok(value_f)
let v = to();
let value_f = v.to_field();
value = v;
value_f
})?;
Ok(AssignedCell {
@ -379,14 +378,14 @@ impl<'r, F: Field> Table<'r, F> {
mut to: V,
) -> Result<(), Error>
where
V: FnMut() -> Result<VR, Error> + 'v,
V: FnMut() -> Value<VR> + 'v,
VR: Into<Assigned<F>>,
A: Fn() -> AR,
AR: Into<String>,
{
self.table
.assign_cell(&|| annotation().into(), column, offset, &mut || {
to().map(|v| v.into())
to().into_field()
})
}
}

27
halo2_proofs/src/circuit/floor_planner/single_pass.rs
View File

@ -8,7 +8,7 @@ use ff::Field;
use crate::{
circuit::{
layouter::{RegionColumn, RegionLayouter, RegionShape, TableLayouter},
Cell, Layouter, Region, RegionIndex, RegionStart, Table,
Cell, Layouter, Region, RegionIndex, RegionStart, Table, Value,
},
plonk::{
Advice, Any, Assigned, Assignment, Circuit, Column, Error, Fixed, FloorPlanner, Instance,
@ -131,7 +131,7 @@ impl<'a, F: Field, CS: Assignment<F> + 'a> Layouter<F> for SingleChipLayouter<'a
|| format!("Constant({:?})", constant.evaluate()),
constants_column,
*next_constant_row,
|| Ok(constant),
|| Value::known(constant),
)?;
self.cs.copy(
constants_column.into(),
@ -280,7 +280,7 @@ impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> RegionLayouter<F>
annotation: &'v (dyn Fn() -> String + 'v),
column: Column<Advice>,
offset: usize,
to: &'v mut (dyn FnMut() -> Result<Assigned<F>, Error> + 'v),
to: &'v mut (dyn FnMut() -> Value<Assigned<F>> + 'v),
) -> Result<Cell, Error> {
self.layouter.cs.assign_advice(
annotation,
@ -303,7 +303,8 @@ impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> RegionLayouter<F>
offset: usize,
constant: Assigned<F>,
) -> Result<Cell, Error> {
let advice = self.assign_advice(annotation, column, offset, &mut || Ok(constant))?;
let advice =
self.assign_advice(annotation, column, offset, &mut || Value::known(constant))?;
self.constrain_constant(advice, constant)?;
Ok(advice)
@ -316,12 +317,10 @@ impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> RegionLayouter<F>
row: usize,
advice: Column<Advice>,
offset: usize,
) -> Result<(Cell, Option<F>), Error> {
) -> Result<(Cell, Value<F>), Error> {
let value = self.layouter.cs.query_instance(instance, row)?;
let cell = self.assign_advice(annotation, advice, offset, &mut || {
value.ok_or(Error::Synthesis).map(|v| v.into())
})?;
let cell = self.assign_advice(annotation, advice, offset, &mut || value.to_field())?;
self.layouter.cs.copy(
cell.column,
@ -338,7 +337,7 @@ impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> RegionLayouter<F>
annotation: &'v (dyn Fn() -> String + 'v),
column: Column<Fixed>,
offset: usize,
to: &'v mut (dyn FnMut() -> Result<Assigned<F>, Error> + 'v),
to: &'v mut (dyn FnMut() -> Value<Assigned<F>> + 'v),
) -> Result<Cell, Error> {
self.layouter.cs.assign_fixed(
annotation,
@ -376,9 +375,9 @@ impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> RegionLayouter<F>
/// - The outer `Option` tracks whether the value in row 0 of the table column has been
/// assigned yet. This will always be `Some` once a valid table has been completely
/// assigned.
/// - The inner `Option` tracks whether the underlying `Assignment` is evaluating
/// - The inner `Value` tracks whether the underlying `Assignment` is evaluating
/// witnesses or not.
type DefaultTableValue<F> = Option<Option<Assigned<F>>>;
type DefaultTableValue<F> = Option<Value<Assigned<F>>>;
pub(crate) struct SimpleTableLayouter<'r, 'a, F: Field, CS: Assignment<F> + 'a> {
cs: &'a mut CS,
@ -414,7 +413,7 @@ impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> TableLayouter<F>
annotation: &'v (dyn Fn() -> String + 'v),
column: TableColumn,
offset: usize,
to: &'v mut (dyn FnMut() -> Result<Assigned<F>, Error> + 'v),
to: &'v mut (dyn FnMut() -> Value<Assigned<F>> + 'v),
) -> Result<(), Error> {
if self.used_columns.contains(&column) {
return Err(Error::Synthesis); // TODO better error
@ -422,14 +421,14 @@ impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> TableLayouter<F>
let entry = self.default_and_assigned.entry(column).or_default();
let mut value = None;
let mut value = Value::unknown();
self.cs.assign_fixed(
annotation,
column.inner(),
offset, // tables are always assigned starting at row 0
|| {
let res = to();
value = res.as_ref().ok().cloned();
value = res;
res
},
)?;

17
halo2_proofs/src/circuit/floor_planner/v1.rs
View File

@ -6,7 +6,7 @@ use crate::{
circuit::{
floor_planner::single_pass::SimpleTableLayouter,
layouter::{RegionColumn, RegionLayouter, RegionShape, TableLayouter},
Cell, Layouter, Region, RegionIndex, RegionStart, Table,
Cell, Layouter, Region, RegionIndex, RegionStart, Table, Value,
},
plonk::{
Advice, Any, Assigned, Assignment, Circuit, Column, Error, Fixed, FloorPlanner, Instance,
@ -126,7 +126,7 @@ impl FloorPlanner for V1 {
|| format!("Constant({:?})", value.evaluate()),
fixed_column,
fixed_row,
|| Ok(value),
|| Value::known(value),
)?;
plan.cs.copy(
fixed_column.into(),
@ -396,7 +396,7 @@ impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> RegionLayouter<F> for V1Region<'r
annotation: &'v (dyn Fn() -> String + 'v),
column: Column<Advice>,
offset: usize,
to: &'v mut (dyn FnMut() -> Result<Assigned<F>, Error> + 'v),
to: &'v mut (dyn FnMut() -> Value<Assigned<F>> + 'v),
) -> Result<Cell, Error> {
self.plan.cs.assign_advice(
annotation,
@ -419,7 +419,8 @@ impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> RegionLayouter<F> for V1Region<'r
offset: usize,
constant: Assigned<F>,
) -> Result<Cell, Error> {
let advice = self.assign_advice(annotation, column, offset, &mut || Ok(constant))?;
let advice =
self.assign_advice(annotation, column, offset, &mut || Value::known(constant))?;
self.constrain_constant(advice, constant)?;
Ok(advice)
@ -432,12 +433,10 @@ impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> RegionLayouter<F> for V1Region<'r
row: usize,
advice: Column<Advice>,
offset: usize,
) -> Result<(Cell, Option<F>), Error> {
) -> Result<(Cell, Value<F>), Error> {
let value = self.plan.cs.query_instance(instance, row)?;
let cell = self.assign_advice(annotation, advice, offset, &mut || {
value.ok_or(Error::Synthesis).map(|v| v.into())
})?;
let cell = self.assign_advice(annotation, advice, offset, &mut || value.to_field())?;
self.plan.cs.copy(
cell.column,
@ -454,7 +453,7 @@ impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> RegionLayouter<F> for V1Region<'r
annotation: &'v (dyn Fn() -> String + 'v),
column: Column<Fixed>,
offset: usize,
to: &'v mut (dyn FnMut() -> Result<Assigned<F>, Error> + 'v),
to: &'v mut (dyn FnMut() -> Value<Assigned<F>> + 'v),
) -> Result<Cell, Error> {
self.plan.cs.assign_fixed(
annotation,

20
halo2_proofs/src/circuit/layouter.rs
View File

@ -6,7 +6,7 @@ use std::fmt;
use ff::Field;
use super::{Cell, RegionIndex};
use super::{Cell, RegionIndex, Value};
use crate::plonk::{Advice, Any, Assigned, Column, Error, Fixed, Instance, Selector, TableColumn};
/// Helper trait for implementing a custom [`Layouter`].
@ -54,7 +54,7 @@ pub trait RegionLayouter<F: Field>: fmt::Debug {
annotation: &'v (dyn Fn() -> String + 'v),
column: Column<Advice>,
offset: usize,
to: &'v mut (dyn FnMut() -> Result<Assigned<F>, Error> + 'v),
to: &'v mut (dyn FnMut() -> Value<Assigned<F>> + 'v),
) -> Result<Cell, Error>;
/// Assigns a constant value to the column `advice` at `offset` within this region.
@ -82,7 +82,7 @@ pub trait RegionLayouter<F: Field>: fmt::Debug {
row: usize,
advice: Column<Advice>,
offset: usize,
) -> Result<(Cell, Option<F>), Error>;
) -> Result<(Cell, Value<F>), Error>;
/// Assign a fixed value
fn assign_fixed<'v>(
@ -90,7 +90,7 @@ pub trait RegionLayouter<F: Field>: fmt::Debug {
annotation: &'v (dyn Fn() -> String + 'v),
column: Column<Fixed>,
offset: usize,
to: &'v mut (dyn FnMut() -> Result<Assigned<F>, Error> + 'v),
to: &'v mut (dyn FnMut() -> Value<Assigned<F>> + 'v),
) -> Result<Cell, Error>;
/// Constrains a cell to have a constant value.
@ -118,7 +118,7 @@ pub trait TableLayouter<F: Field>: fmt::Debug {
annotation: &'v (dyn Fn() -> String + 'v),
column: TableColumn,
offset: usize,
to: &'v mut (dyn FnMut() -> Result<Assigned<F>, Error> + 'v),
to: &'v mut (dyn FnMut() -> Value<Assigned<F>> + 'v),
) -> Result<(), Error>;
}
@ -214,7 +214,7 @@ impl<F: Field> RegionLayouter<F> for RegionShape {
_: &'v (dyn Fn() -> String + 'v),
column: Column<Advice>,
offset: usize,
_to: &'v mut (dyn FnMut() -> Result<Assigned<F>, Error> + 'v),
_to: &'v mut (dyn FnMut() -> Value<Assigned<F>> + 'v),
) -> Result<Cell, Error> {
self.columns.insert(Column::<Any>::from(column).into());
self.row_count = cmp::max(self.row_count, offset + 1);
@ -234,7 +234,7 @@ impl<F: Field> RegionLayouter<F> for RegionShape {
constant: Assigned<F>,
) -> Result<Cell, Error> {
// The rest is identical to witnessing an advice cell.
self.assign_advice(annotation, column, offset, &mut || Ok(constant))
self.assign_advice(annotation, column, offset, &mut || Value::known(constant))
}
fn assign_advice_from_instance<'v>(
@ -244,7 +244,7 @@ impl<F: Field> RegionLayouter<F> for RegionShape {
_: usize,
advice: Column<Advice>,
offset: usize,
) -> Result<(Cell, Option<F>), Error> {
) -> Result<(Cell, Value<F>), Error> {
self.columns.insert(Column::<Any>::from(advice).into());
self.row_count = cmp::max(self.row_count, offset + 1);
@ -254,7 +254,7 @@ impl<F: Field> RegionLayouter<F> for RegionShape {
row_offset: offset,
column: advice.into(),
},
None,
Value::unknown(),
))
}
@ -263,7 +263,7 @@ impl<F: Field> RegionLayouter<F> for RegionShape {
_: &'v (dyn Fn() -> String + 'v),
column: Column<Fixed>,
offset: usize,
_to: &'v mut (dyn FnMut() -> Result<Assigned<F>, Error> + 'v),
_to: &'v mut (dyn FnMut() -> Value<Assigned<F>> + 'v),
) -> Result<Cell, Error> {
self.columns.insert(Column::<Any>::from(column).into());
self.row_count = cmp::max(self.row_count, offset + 1);

75
halo2_proofs/src/dev.rs
View File

@ -11,6 +11,7 @@ use ff::Field;
use crate::plonk::Assigned;
use crate::{
arithmetic::{FieldExt, Group},
circuit,
plonk::{
permutation, Advice, Any, Assignment, Circuit, Column, ColumnType, ConstraintSystem, Error,
Expression, Fixed, FloorPlanner, Instance, Selector, VirtualCell,
@ -167,7 +168,7 @@ impl<F: Group + Field> Mul<F> for Value<F> {
/// ```
/// use halo2_proofs::{
/// arithmetic::FieldExt,
/// circuit::{Layouter, SimpleFloorPlanner},
/// circuit::{Layouter, SimpleFloorPlanner, Value},
/// dev::{FailureLocation, MockProver, VerifyFailure},
/// pasta::Fp,
/// plonk::{Advice, Any, Circuit, Column, ConstraintSystem, Error, Selector},
@ -185,8 +186,8 @@ impl<F: Group + Field> Mul<F> for Value<F> {
///
/// #[derive(Clone, Default)]
/// struct MyCircuit {
/// a: Option<u64>,
/// b: Option<u64>,
/// a: Value<u64>,
/// b: Value<u64>,
/// }
///
/// impl<F: FieldExt> Circuit<F> for MyCircuit {
@ -220,15 +221,13 @@ impl<F: Group + Field> Mul<F> for Value<F> {
/// layouter.assign_region(|| "Example region", |mut region| {
/// config.s.enable(&mut region, 0)?;
/// region.assign_advice(|| "a", config.a, 0, || {
/// self.a.map(|v| F::from(v)).ok_or(Error::Synthesis)
/// self.a.map(F::from)
/// })?;
/// region.assign_advice(|| "b", config.b, 0, || {
/// self.b.map(|v| F::from(v)).ok_or(Error::Synthesis)
/// self.b.map(F::from)
/// })?;
/// region.assign_advice(|| "c", config.c, 0, || {
/// self.a
/// .and_then(|a| self.b.map(|b| F::from(a * b)))
/// .ok_or(Error::Synthesis)
/// (self.a * self.b).map(F::from)
/// })?;
/// Ok(())
/// })
@ -237,8 +236,8 @@ impl<F: Group + Field> Mul<F> for Value<F> {
///
/// // Assemble the private inputs to the circuit.
/// let circuit = MyCircuit {
/// a: Some(2),
/// b: Some(4),
/// a: Value::known(2),
/// b: Value::known(4),
/// };
///
/// // This circuit has no public inputs.
@ -340,7 +339,11 @@ impl<F: Field + Group> Assignment<F> for MockProver<F> {
Ok(())
}
fn query_instance(&self, column: Column<Instance>, row: usize) -> Result<Option<F>, Error> {
fn query_instance(
&self,
column: Column<Instance>,
row: usize,
) -> Result<circuit::Value<F>, Error> {
if !self.usable_rows.contains(&row) {
return Err(Error::not_enough_rows_available(self.k));
}
@ -348,7 +351,7 @@ impl<F: Field + Group> Assignment<F> for MockProver<F> {
self.instance
.get(column.index())
.and_then(|column| column.get(row))
.map(|v| Some(*v))
.map(|v| circuit::Value::known(*v))
.ok_or(Error::BoundsFailure)
}
@ -360,7 +363,7 @@ impl<F: Field + Group> Assignment<F> for MockProver<F> {
to: V,
) -> Result<(), Error>
where
V: FnOnce() -> Result<VR, Error>,
V: FnOnce() -> circuit::Value<VR>,
VR: Into<Assigned<F>>,
A: FnOnce() -> AR,
AR: Into<String>,
@ -378,7 +381,8 @@ impl<F: Field + Group> Assignment<F> for MockProver<F> {
.advice
.get_mut(column.index())
.and_then(|v| v.get_mut(row))
.ok_or(Error::BoundsFailure)? = CellValue::Assigned(to()?.into().evaluate());
.ok_or(Error::BoundsFailure)? =
CellValue::Assigned(to().into_field().evaluate().assign()?);
Ok(())
}
@ -391,7 +395,7 @@ impl<F: Field + Group> Assignment<F> for MockProver<F> {
to: V,
) -> Result<(), Error>
where
V: FnOnce() -> Result<VR, Error>,
V: FnOnce() -> circuit::Value<VR>,
VR: Into<Assigned<F>>,
A: FnOnce() -> AR,
AR: Into<String>,
@ -409,7 +413,8 @@ impl<F: Field + Group> Assignment<F> for MockProver<F> {
.fixed
.get_mut(column.index())
.and_then(|v| v.get_mut(row))
.ok_or(Error::BoundsFailure)? = CellValue::Assigned(to()?.into().evaluate());
.ok_or(Error::BoundsFailure)? =
CellValue::Assigned(to().into_field().evaluate().assign()?);
Ok(())
}
@ -433,14 +438,14 @@ impl<F: Field + Group> Assignment<F> for MockProver<F> {
&mut self,
col: Column<Fixed>,
from_row: usize,
to: Option<Assigned<F>>,
to: circuit::Value<Assigned<F>>,
) -> Result<(), Error> {
if !self.usable_rows.contains(&from_row) {
return Err(Error::not_enough_rows_available(self.k));
}
for row in self.usable_rows.clone().skip(from_row) {
self.assign_fixed(|| "", col, row, || to.ok_or(Error::Synthesis))?;
self.assign_fixed(|| "", col, row, || to)?;
}
Ok(())
@ -876,7 +881,7 @@ mod tests {
use super::{FailureLocation, MockProver, VerifyFailure};
use crate::{
circuit::{Layouter, SimpleFloorPlanner},
circuit::{Layouter, SimpleFloorPlanner, Value},
plonk::{
Advice, Any, Circuit, Column, ConstraintSystem, Error, Expression, Selector,
TableColumn,
@ -933,7 +938,7 @@ mod tests {
config.q.enable(&mut region, 1)?;
// Assign a = 0.
region.assign_advice(|| "a", config.a, 0, || Ok(Fp::zero()))?;
region.assign_advice(|| "a", config.a, 0, || Value::known(Fp::zero()))?;
// BUG: Forget to assign b = 0! This could go unnoticed during
// development, because cell values default to zero, which in this
@ -1011,7 +1016,7 @@ mod tests {
|| format!("table[{}] = {}", i, 2 * i),
config.table,
i - 1,
|| Ok(Fp::from(2 * i as u64)),
|| Value::known(Fp::from(2 * i as u64)),
)
})
.fold(Ok(()), |acc, res| acc.and(res))
@ -1026,8 +1031,18 @@ mod tests {
config.q.enable(&mut region, 1)?;
// Assign a = 2 and a = 6.
region.assign_advice(|| "a = 2", config.a, 0, || Ok(Fp::from(2)))?;
region.assign_advice(|| "a = 6", config.a, 1, || Ok(Fp::from(6)))?;
region.assign_advice(
|| "a = 2",
config.a,
0,
|| Value::known(Fp::from(2)),
)?;
region.assign_advice(
|| "a = 6",
config.a,
1,
|| Value::known(Fp::from(6)),
)?;
Ok(())
},
@ -1041,10 +1056,20 @@ mod tests {
config.q.enable(&mut region, 1)?;
// Assign a = 4.
region.assign_advice(|| "a = 4", config.a, 0, || Ok(Fp::from(4)))?;
region.assign_advice(
|| "a = 4",
config.a,
0,
|| Value::known(Fp::from(4)),
)?;
// BUG: Assign a = 5, which doesn't exist in the table!
region.assign_advice(|| "a = 5", config.a, 1, || Ok(Fp::from(5)))?;
region.assign_advice(
|| "a = 5",
config.a,
1,
|| Value::known(Fp::from(5)),
)?;
Ok(())
},

11
halo2_proofs/src/dev/cost.rs
View File

@ -11,6 +11,7 @@ use ff::{Field, PrimeField};
use group::prime::PrimeGroup;
use crate::{
circuit::Value,
plonk::{
Advice, Any, Assigned, Assignment, Circuit, Column, ConstraintSystem, Error, Fixed,
FloorPlanner, Instance, Selector,
@ -68,8 +69,8 @@ impl<F: Field> Assignment<F> for Assembly {
Ok(())
}
fn query_instance(&self, _: Column<Instance>, _: usize) -> Result<Option<F>, Error> {
Ok(None)
fn query_instance(&self, _: Column<Instance>, _: usize) -> Result<Value<F>, Error> {
Ok(Value::unknown())
}
fn assign_advice<V, VR, A, AR>(
@ -80,7 +81,7 @@ impl<F: Field> Assignment<F> for Assembly {
_: V,
) -> Result<(), Error>
where
V: FnOnce() -> Result<VR, Error>,
V: FnOnce() -> Value<VR>,
VR: Into<Assigned<F>>,
A: FnOnce() -> AR,
AR: Into<String>,
@ -96,7 +97,7 @@ impl<F: Field> Assignment<F> for Assembly {
_: V,
) -> Result<(), Error>
where
V: FnOnce() -> Result<VR, Error>,
V: FnOnce() -> Value<VR>,
VR: Into<Assigned<F>>,
A: FnOnce() -> AR,
AR: Into<String>,
@ -112,7 +113,7 @@ impl<F: Field> Assignment<F> for Assembly {
&mut self,
_: Column<Fixed>,
_: usize,
_: Option<Assigned<F>>,
_: Value<Assigned<F>>,
) -> Result<(), Error> {
Ok(())
}

19
halo2_proofs/src/dev/graph.rs
View File

@ -1,9 +1,12 @@
use ff::Field;
use tabbycat::{AttrList, Edge, GraphBuilder, GraphType, Identity, StmtList};
use crate::plonk::{
Advice, Any, Assigned, Assignment, Circuit, Column, ConstraintSystem, Error, Fixed,
FloorPlanner, Instance, Selector,
use crate::{
circuit::Value,
plonk::{
Advice, Any, Assigned, Assignment, Circuit, Column, ConstraintSystem, Error, Fixed,
FloorPlanner, Instance, Selector,
},
};
pub mod layout;
@ -96,8 +99,8 @@ impl<F: Field> Assignment<F> for Graph {
Ok(())
}
fn query_instance(&self, _: Column<Instance>, _: usize) -> Result<Option<F>, Error> {
Ok(None)
fn query_instance(&self, _: Column<Instance>, _: usize) -> Result<Value<F>, Error> {
Ok(Value::unknown())
}
fn assign_advice<V, VR, A, AR>(
@ -108,7 +111,7 @@ impl<F: Field> Assignment<F> for Graph {
_: V,
) -> Result<(), Error>
where
V: FnOnce() -> Result<VR, Error>,
V: FnOnce() -> Value<VR>,
VR: Into<Assigned<F>>,
A: FnOnce() -> AR,
AR: Into<String>,
@ -125,7 +128,7 @@ impl<F: Field> Assignment<F> for Graph {
_: V,
) -> Result<(), Error>
where
V: FnOnce() -> Result<VR, Error>,
V: FnOnce() -> Value<VR>,
VR: Into<Assigned<F>>,
A: FnOnce() -> AR,
AR: Into<String>,
@ -149,7 +152,7 @@ impl<F: Field> Assignment<F> for Graph {
&mut self,
_: Column<Fixed>,
_: usize,
_: Option<Assigned<F>>,
_: Value<Assigned<F>>,
) -> Result<(), Error> {
Ok(())
}

20
halo2_proofs/src/dev/graph/layout.rs
View File

@ -7,10 +7,12 @@ use std::cmp;
use std::collections::HashSet;
use std::ops::Range;
use crate::circuit::layouter::RegionColumn;
use crate::plonk::{
Advice, Any, Assigned, Assignment, Circuit, Column, ConstraintSystem, Error, Fixed,
FloorPlanner, Instance, Selector,
use crate::{
circuit::{layouter::RegionColumn, Value},
plonk::{
Advice, Any, Assigned, Assignment, Circuit, Column, ConstraintSystem, Error, Fixed,
FloorPlanner, Instance, Selector,
},
};
/// Graphical renderer for circuit layouts.
@ -430,8 +432,8 @@ impl<F: Field> Assignment<F> for Layout {
Ok(())
}
fn query_instance(&self, _: Column<Instance>, _: usize) -> Result<Option<F>, Error> {
Ok(None)
fn query_instance(&self, _: Column<Instance>, _: usize) -> Result<Value<F>, Error> {
Ok(Value::unknown())
}
fn assign_advice<V, VR, A, AR>(
@ -442,7 +444,7 @@ impl<F: Field> Assignment<F> for Layout {
_: V,
) -> Result<(), Error>
where
V: FnOnce() -> Result<VR, Error>,
V: FnOnce() -> Value<VR>,
VR: Into<Assigned<F>>,
A: FnOnce() -> AR,
AR: Into<String>,
@ -459,7 +461,7 @@ impl<F: Field> Assignment<F> for Layout {
_: V,
) -> Result<(), Error>
where
V: FnOnce() -> Result<VR, Error>,
V: FnOnce() -> Value<VR>,
VR: Into<Assigned<F>>,
A: FnOnce() -> AR,
AR: Into<String>,
@ -483,7 +485,7 @@ impl<F: Field> Assignment<F> for Layout {
&mut self,
_: Column<Fixed>,
_: usize,
_: Option<Assigned<F>>,
_: Value<Assigned<F>>,
) -> Result<(), Error> {
Ok(())
}

7
halo2_proofs/src/plonk/assigned.rs
View File

@ -250,6 +250,13 @@ impl<F: Field> Mul<F> for Assigned<F> {
}
}
impl<F: Field> Mul<F> for &Assigned<F> {
type Output = Assigned<F>;
fn mul(self, rhs: F) -> Assigned<F> {
*self * rhs
}
}
impl<F: Field> Mul<&Assigned<F>> for Assigned<F> {
type Output = Assigned<F>;
fn mul(self, rhs: &Assigned<F>) -> Assigned<F> {

24
halo2_proofs/src/plonk/circuit.rs
View File

@ -7,8 +7,10 @@ use std::{
};
use super::{lookup, permutation, Assigned, Error};
use crate::circuit::Layouter;
use crate::{circuit::Region, poly::Rotation};
use crate::{
circuit::{Layouter, Region, Value},
poly::Rotation,
};
mod compress_selectors;
@ -226,7 +228,11 @@ impl TryFrom<Column<Any>> for Column<Instance> {
/// Selectors are disabled on all rows by default, and must be explicitly enabled on each
/// row when required:
/// ```
/// use halo2_proofs::{arithmetic::FieldExt, circuit::{Chip, Layouter}, plonk::{Advice, Column, Error, Selector}};
/// use halo2_proofs::{
/// arithmetic::FieldExt,
/// circuit::{Chip, Layouter, Value},
/// plonk::{Advice, Column, Error, Selector},
/// };
/// # use ff::Field;
/// # use halo2_proofs::plonk::Fixed;
///
@ -240,8 +246,8 @@ impl TryFrom<Column<Any>> for Column<Instance> {
/// let config = chip.config();
/// # let config: Config = todo!();
/// layouter.assign_region(|| "bar", |mut region| {
/// region.assign_advice(|| "a", config.a, 0, || Ok(F::one()))?;
/// region.assign_advice(|| "a", config.b, 1, || Ok(F::one()))?;
/// region.assign_advice(|| "a", config.a, 0, || Value::known(F::one()))?;
/// region.assign_advice(|| "a", config.b, 1, || Value::known(F::one()))?;
/// config.s.enable(&mut region, 1)
/// })?;
/// Ok(())
@ -329,7 +335,7 @@ pub trait Assignment<F: Field> {
/// Queries the cell of an instance column at a particular absolute row.
///
/// Returns the cell's value, if known.
fn query_instance(&self, column: Column<Instance>, row: usize) -> Result<Option<F>, Error>;
fn query_instance(&self, column: Column<Instance>, row: usize) -> Result<Value<F>, Error>;
/// Assign an advice column value (witness)
fn assign_advice<V, VR, A, AR>(
@ -340,7 +346,7 @@ pub trait Assignment<F: Field> {
to: V,
) -> Result<(), Error>
where
V: FnOnce() -> Result<VR, Error>,
V: FnOnce() -> Value<VR>,
VR: Into<Assigned<F>>,
A: FnOnce() -> AR,
AR: Into<String>;
@ -354,7 +360,7 @@ pub trait Assignment<F: Field> {
to: V,
) -> Result<(), Error>
where
V: FnOnce() -> Result<VR, Error>,
V: FnOnce() -> Value<VR>,
VR: Into<Assigned<F>>,
A: FnOnce() -> AR,
AR: Into<String>;
@ -373,7 +379,7 @@ pub trait Assignment<F: Field> {
&mut self,
column: Column<Fixed>,
row: usize,
to: Option<Assigned<F>>,
to: Value<Assigned<F>>,
) -> Result<(), Error>;
/// Creates a new (sub)namespace and enters into it.

27
halo2_proofs/src/plonk/keygen.rs
View File

@ -12,11 +12,15 @@ use super::{
},
permutation, Assigned, Error, LagrangeCoeff, Polynomial, ProvingKey, VerifyingKey,
};
use crate::poly::{
commitment::{Blind, Params},
EvaluationDomain,
use crate::{
arithmetic::CurveAffine,
circuit::Value,
poly::{
batch_invert_assigned,
commitment::{Blind, Params},
EvaluationDomain,
},
};
use crate::{arithmetic::CurveAffine, poly::batch_invert_assigned};
pub(crate) fn create_domain<C, ConcreteCircuit>(
params: &Params<C>,
@ -78,13 +82,13 @@ impl<F: Field> Assignment<F> for Assembly<F> {
Ok(())
}
fn query_instance(&self, _: Column<Instance>, row: usize) -> Result<Option<F>, Error> {
fn query_instance(&self, _: Column<Instance>, row: usize) -> Result<Value<F>, Error> {
if !self.usable_rows.contains(&row) {
return Err(Error::not_enough_rows_available(self.k));
}
// There is no instance in this context.
Ok(None)
Ok(Value::unknown())
}
fn assign_advice<V, VR, A, AR>(
@ -95,7 +99,7 @@ impl<F: Field> Assignment<F> for Assembly<F> {
_: V,
) -> Result<(), Error>
where
V: FnOnce() -> Result<VR, Error>,
V: FnOnce() -> Value<VR>,
VR: Into<Assigned<F>>,
A: FnOnce() -> AR,
AR: Into<String>,
@ -112,7 +116,7 @@ impl<F: Field> Assignment<F> for Assembly<F> {
to: V,
) -> Result<(), Error>
where
V: FnOnce() -> Result<VR, Error>,
V: FnOnce() -> Value<VR>,
VR: Into<Assigned<F>>,
A: FnOnce() -> AR,
AR: Into<String>,
@ -125,7 +129,7 @@ impl<F: Field> Assignment<F> for Assembly<F> {
.fixed
.get_mut(column.index())
.and_then(|v| v.get_mut(row))
.ok_or(Error::BoundsFailure)? = to()?.into();
.ok_or(Error::BoundsFailure)? = to().into_field().assign()?;
Ok(())
}
@ -149,7 +153,7 @@ impl<F: Field> Assignment<F> for Assembly<F> {
&mut self,
column: Column<Fixed>,
from_row: usize,
to: Option<Assigned<F>>,
to: Value<Assigned<F>>,
) -> Result<(), Error> {
if !self.usable_rows.contains(&from_row) {
return Err(Error::not_enough_rows_available(self.k));
@ -160,8 +164,9 @@ impl<F: Field> Assignment<F> for Assembly<F> {
.get_mut(column.index())
.ok_or(Error::BoundsFailure)?;
let filler = to.assign()?;
for row in self.usable_rows.clone().skip(from_row) {
col[row] = to.ok_or(Error::Synthesis)?;
col[row] = filler;
}
Ok(())

25
halo2_proofs/src/plonk/prover.rs
View File

@ -12,15 +12,16 @@ use super::{
lookup, permutation, vanishing, ChallengeBeta, ChallengeGamma, ChallengeTheta, ChallengeX,
ChallengeY, Error, ProvingKey,
};
use crate::poly::{
self,
commitment::{Blind, Params},
multiopen::{self, ProverQuery},
Coeff, ExtendedLagrangeCoeff, LagrangeCoeff, Polynomial,
};
use crate::{
arithmetic::{eval_polynomial, CurveAffine, FieldExt},
circuit::Value,
plonk::Assigned,
poly::{
self,
commitment::{Blind, Params},
multiopen::{self, ProverQuery},
Coeff, ExtendedLagrangeCoeff, LagrangeCoeff, Polynomial,
},
};
use crate::{
poly::batch_invert_assigned,
@ -171,7 +172,7 @@ pub fn create_proof<
&self,
column: Column<Instance>,
row: usize,
) -> Result<Option<F>, Error> {
) -> Result<Value<F>, Error> {
if !self.usable_rows.contains(&row) {
return Err(Error::not_enough_rows_available(self.k));
}
@ -179,7 +180,7 @@ pub fn create_proof<
self.instances
.get(column.index())
.and_then(|column| column.get(row))
.map(|v| Some(*v))
.map(|v| Value::known(*v))
.ok_or(Error::BoundsFailure)
}
@ -191,7 +192,7 @@ pub fn create_proof<
to: V,
) -> Result<(), Error>
where
V: FnOnce() -> Result<VR, Error>,
V: FnOnce() -> Value<VR>,
VR: Into<Assigned<F>>,
A: FnOnce() -> AR,
AR: Into<String>,
@ -204,7 +205,7 @@ pub fn create_proof<
.advice
.get_mut(column.index())
.and_then(|v| v.get_mut(row))
.ok_or(Error::BoundsFailure)? = to()?.into();
.ok_or(Error::BoundsFailure)? = to().into_field().assign()?;
Ok(())
}
@ -217,7 +218,7 @@ pub fn create_proof<
_: V,
) -> Result<(), Error>
where
V: FnOnce() -> Result<VR, Error>,
V: FnOnce() -> Value<VR>,
VR: Into<Assigned<F>>,
A: FnOnce() -> AR,
AR: Into<String>,
@ -243,7 +244,7 @@ pub fn create_proof<
&mut self,
_: Column<Fixed>,
_: usize,
_: Option<Assigned<F>>,
_: Value<Assigned<F>>,
) -> Result<(), Error> {
Ok(())
}

113
halo2_proofs/tests/plonk_api.rs
View File

@ -3,12 +3,12 @@
use assert_matches::assert_matches;
use halo2_proofs::arithmetic::{CurveAffine, FieldExt};
use halo2_proofs::circuit::{Cell, Layouter, SimpleFloorPlanner};
use halo2_proofs::circuit::{Cell, Layouter, SimpleFloorPlanner, Value};
use halo2_proofs::dev::MockProver;
use halo2_proofs::pasta::{Eq, EqAffine, Fp};
use halo2_proofs::plonk::{
create_proof, keygen_pk, keygen_vk, verify_proof, Advice, BatchVerifier, Circuit, Column,
ConstraintSystem, Error, Fixed, SingleVerifier, TableColumn, VerificationStrategy,
create_proof, keygen_pk, keygen_vk, verify_proof, Advice, Assigned, BatchVerifier, Circuit,
Column, ConstraintSystem, Error, Fixed, SingleVerifier, TableColumn, VerificationStrategy,
};
use halo2_proofs::poly::commitment::{Guard, MSM};
use halo2_proofs::poly::{commitment::Params, Rotation};
@ -51,18 +51,18 @@ fn plonk_api() {
f: F,
) -> Result<(Cell, Cell, Cell), Error>
where
F: FnMut() -> Result<(FF, FF, FF), Error>;
F: FnMut() -> Value<(Assigned<FF>, Assigned<FF>, Assigned<FF>)>;
fn raw_add<F>(
&self,
layouter: &mut impl Layouter<FF>,
f: F,
) -> Result<(Cell, Cell, Cell), Error>
where
F: FnMut() -> Result<(FF, FF, FF), Error>;
F: FnMut() -> Value<(Assigned<FF>, Assigned<FF>, Assigned<FF>)>;
fn copy(&self, layouter: &mut impl Layouter<FF>, a: Cell, b: Cell) -> Result<(), Error>;
fn public_input<F>(&self, layouter: &mut impl Layouter<FF>, f: F) -> Result<Cell, Error>
where
F: FnMut() -> Result<FF, Error>;
F: FnMut() -> Value<FF>;
fn lookup_table(
&self,
layouter: &mut impl Layouter<FF>,
@ -72,7 +72,7 @@ fn plonk_api() {
#[derive(Clone)]
struct MyCircuit<F: FieldExt> {
a: Option<F>,
a: Value<F>,
lookup_table: Vec<F>,
}
@ -97,7 +97,7 @@ fn plonk_api() {
mut f: F,
) -> Result<(Cell, Cell, Cell), Error>
where
F: FnMut() -> Result<(FF, FF, FF), Error>,
F: FnMut() -> Value<(Assigned<FF>, Assigned<FF>, Assigned<FF>)>,
{
layouter.assign_region(
|| "raw_multiply",
@ -108,39 +108,44 @@ fn plonk_api() {
self.config.a,
0,
|| {
value = Some(f()?);
Ok(value.ok_or(Error::Synthesis)?.0)
value = Some(f());
value.unwrap().map(|v| v.0)
},
)?;
region.assign_advice(
|| "lhs^4",
self.config.d,
0,
|| Ok(value.ok_or(Error::Synthesis)?.0.square().square()),
|| value.unwrap().map(|v| v.0).square().square(),
)?;
let rhs = region.assign_advice(
|| "rhs",
self.config.b,
0,
|| Ok(value.ok_or(Error::Synthesis)?.1),
|| value.unwrap().map(|v| v.1),
)?;
region.assign_advice(
|| "rhs^4",
self.config.e,
0,
|| Ok(value.ok_or(Error::Synthesis)?.1.square().square()),
|| value.unwrap().map(|v| v.1).square().square(),
)?;
let out = region.assign_advice(
|| "out",
self.config.c,
0,
|| Ok(value.ok_or(Error::Synthesis)?.2),
|| value.unwrap().map(|v| v.2),
)?;
region.assign_fixed(|| "a", self.config.sa, 0, || Ok(FF::zero()))?;
region.assign_fixed(|| "b", self.config.sb, 0, || Ok(FF::zero()))?;
region.assign_fixed(|| "c", self.config.sc, 0, || Ok(FF::one()))?;
region.assign_fixed(|| "a * b", self.config.sm, 0, || Ok(FF::one()))?;
region.assign_fixed(|| "a", self.config.sa, 0, || Value::known(FF::zero()))?;
region.assign_fixed(|| "b", self.config.sb, 0, || Value::known(FF::zero()))?;
region.assign_fixed(|| "c", self.config.sc, 0, || Value::known(FF::one()))?;
region.assign_fixed(
|| "a * b",
self.config.sm,
0,
|| Value::known(FF::one()),
)?;
Ok((lhs.cell(), rhs.cell(), out.cell()))
},
)
@ -151,7 +156,7 @@ fn plonk_api() {
mut f: F,
) -> Result<(Cell, Cell, Cell), Error>
where
F: FnMut() -> Result<(FF, FF, FF), Error>,
F: FnMut() -> Value<(Assigned<FF>, Assigned<FF>, Assigned<FF>)>,
{
layouter.assign_region(
|| "raw_add",
@ -162,39 +167,44 @@ fn plonk_api() {
self.config.a,
0,
|| {
value = Some(f()?);
Ok(value.ok_or(Error::Synthesis)?.0)
value = Some(f());
value.unwrap().map(|v| v.0)
},
)?;
region.assign_advice(
|| "lhs^4",
self.config.d,
0,
|| Ok(value.ok_or(Error::Synthesis)?.0.square().square()),
|| value.unwrap().map(|v| v.0).square().square(),
)?;
let rhs = region.assign_advice(
|| "rhs",
self.config.b,
0,
|| Ok(value.ok_or(Error::Synthesis)?.1),
|| value.unwrap().map(|v| v.1),
)?;
region.assign_advice(
|| "rhs^4",
self.config.e,
0,
|| Ok(value.ok_or(Error::Synthesis)?.1.square().square()),
|| value.unwrap().map(|v| v.1).square().square(),
)?;
let out = region.assign_advice(
|| "out",
self.config.c,
0,
|| Ok(value.ok_or(Error::Synthesis)?.2),
|| value.unwrap().map(|v| v.2),
)?;
region.assign_fixed(|| "a", self.config.sa, 0, || Ok(FF::one()))?;
region.assign_fixed(|| "b", self.config.sb, 0, || Ok(FF::one()))?;
region.assign_fixed(|| "c", self.config.sc, 0, || Ok(FF::one()))?;
region.assign_fixed(|| "a * b", self.config.sm, 0, || Ok(FF::zero()))?;
region.assign_fixed(|| "a", self.config.sa, 0, || Value::known(FF::one()))?;
region.assign_fixed(|| "b", self.config.sb, 0, || Value::known(FF::one()))?;
region.assign_fixed(|| "c", self.config.sc, 0, || Value::known(FF::one()))?;
region.assign_fixed(
|| "a * b",
self.config.sm,
0,
|| Value::known(FF::zero()),
)?;
Ok((lhs.cell(), rhs.cell(), out.cell()))
},
)
@ -215,13 +225,18 @@ fn plonk_api() {
}
fn public_input<F>(&self, layouter: &mut impl Layouter<FF>, mut f: F) -> Result<Cell, Error>
where
F: FnMut() -> Result<FF, Error>,
F: FnMut() -> Value<FF>,
{
layouter.assign_region(
|| "public_input",
|mut region| {
let value = region.assign_advice(|| "value", self.config.a, 0, &mut f)?;
region.assign_fixed(|| "public", self.config.sp, 0, || Ok(FF::one()))?;
region.assign_fixed(
|| "public",
self.config.sp,
0,
|| Value::known(FF::one()),
)?;
Ok(value.cell())
},
@ -236,7 +251,12 @@ fn plonk_api() {
|| "",
|mut table| {
for (index, &value) in values.iter().enumerate() {
table.assign_cell(|| "table col", self.config.sl, index, || Ok(value))?;
table.assign_cell(
|| "table col",
self.config.sl,
index,
|| Value::known(value),
)?;
}
Ok(())
},
@ -251,7 +271,7 @@ fn plonk_api() {
fn without_witnesses(&self) -> Self {
Self {
a: None,
a: Value::unknown(),
lookup_table: self.lookup_table.clone(),
}
}
@ -353,25 +373,20 @@ fn plonk_api() {
) -> Result<(), Error> {
let cs = StandardPlonk::new(config);
let _ = cs.public_input(&mut layouter, || Ok(F::one() + F::one()))?;
let _ = cs.public_input(&mut layouter, || Value::known(F::one() + F::one()))?;
for _ in 0..10 {
let mut a_squared = None;
let a: Value<Assigned<_>> = self.a.into();
let mut a_squared = Value::unknown();
let (a0, _, c0) = cs.raw_multiply(&mut layouter, || {
a_squared = self.a.map(|a| a.square());
Ok((
self.a.ok_or(Error::Synthesis)?,
self.a.ok_or(Error::Synthesis)?,
a_squared.ok_or(Error::Synthesis)?,
))
a_squared = a.square();
a.zip(a_squared).map(|(a, a_squared)| (a, a, a_squared))
})?;
let (a1, b1, _) = cs.raw_add(&mut layouter, || {
let fin = a_squared.and_then(|a2| self.a.map(|a| a + a2));
Ok((
self.a.ok_or(Error::Synthesis)?,
a_squared.ok_or(Error::Synthesis)?,
fin.ok_or(Error::Synthesis)?,
))
let fin = a_squared + a;
a.zip(a_squared)
.zip(fin)
.map(|((a, a_squared), fin)| (a, a_squared, fin))
})?;
cs.copy(&mut layouter, a0, a1)?;
cs.copy(&mut layouter, b1, c0)?;
@ -388,12 +403,12 @@ fn plonk_api() {
let lookup_table = vec![instance, a, a, Fp::zero()];
let empty_circuit: MyCircuit<Fp> = MyCircuit {
a: None,
a: Value::unknown(),
lookup_table: lookup_table.clone(),
};
let circuit: MyCircuit<Fp> = MyCircuit {
a: Some(a),
a: Value::known(a),
lookup_table,
};