add is_zero gadget

This commit is contained in:
Haichen Shen
2022-06-15 15:53:23 -07:00
parent 869d126132
commit b73b80f1f8
6 changed files with 92 additions and 19 deletions

3
Cargo.lock generated
View File

@@ -151,8 +151,7 @@ dependencies = [
[[package]]
name = "halo2_proofs"
version = "0.1.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "e925780549adee8364c7f2b685c753f6f3df23bde520c67416e93bf615933760"
source = "git+https://github.com/zcash/halo2.git?rev=a898d65ae3ad3d41987666f6a03cfc15edae01c4#a898d65ae3ad3d41987666f6a03cfc15edae01c4"
dependencies = [
"blake2b_simd",
"ff",

View File

@@ -5,9 +5,13 @@ edition = "2021"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
[lib]
name = "halo2_gadget"
path = "src/lib.rs"
[[bin]]
name = "example1"
path = "src/example1.rs"
[dependencies]
halo2_proofs = "0.1.0"
halo2_proofs = { git = "https://github.com/zcash/halo2.git", rev = "a898d65ae3ad3d41987666f6a03cfc15edae01c4"}

View File

@@ -64,8 +64,8 @@ impl<F: FieldExt> FiboChip<F> {
pub fn assign_first_row(
&self,
mut layouter: impl Layouter<F>,
a: Option<F>,
b: Option<F>,
a: Value<F>,
b: Value<F>,
) -> Result<(ACell<F>, ACell<F>, ACell<F>), Error>{
layouter.assign_region(
|| "first row",
@@ -76,23 +76,23 @@ impl<F: FieldExt> FiboChip<F> {
|| "a",
self.config.advice[0],
0,
|| a.ok_or(Error::Synthesis),
|| a,
).map(ACell)?;
let b_cell = region.assign_advice(
|| "b",
self.config.advice[1],
0,
|| b.ok_or(Error::Synthesis),
|| b,
).map(ACell)?;
let c_val = a.and_then(|a| b.map(|b| a + b));
let c_val = a + b;
let c_cell = region.assign_advice(
|| "c",
self.config.advice[2],
0,
|| c_val.ok_or(Error::Synthesis),
|| c_val,
).map(ACell)?;
Ok((a_cell, b_cell, c_cell))
@@ -113,17 +113,13 @@ impl<F: FieldExt> FiboChip<F> {
prev_b.0.copy_advice(|| "a", &mut region, self.config.advice[0], 0)?;
prev_c.0.copy_advice(|| "b", &mut region, self.config.advice[1], 0)?;
let c_val = prev_b.0.value().and_then(
|b| {
prev_c.0.value().map(|c| *b + *c)
}
);
let c_val = prev_b.0.value().copied() + prev_c.0.value();
let c_cell = region.assign_advice(
|| "c",
self.config.advice[2],
0,
|| c_val.ok_or(Error::Synthesis),
|| c_val,
).map(ACell)?;
Ok(c_cell)
@@ -143,8 +139,8 @@ impl<F: FieldExt> FiboChip<F> {
#[derive(Default)]
struct MyCircuit<F> {
pub a: Option<F>,
pub b: Option<F>,
pub a: Value<F>,
pub b: Value<F>,
}
impl<F: FieldExt> Circuit<F> for MyCircuit<F> {
@@ -201,8 +197,8 @@ fn main() {
let out = Fp::from(55); // F[9]
let circuit = MyCircuit {
a: Some(a),
b: Some(b),
a: Value::known(a),
b: Value::known(b),
};
let mut public_input = vec![a, b, out];

3
src/gadget.rs Normal file
View File

@@ -0,0 +1,3 @@
mod is_zero;
pub use is_zero::{IsZeroConfig, IsZeroChip};

68
src/gadget/is_zero.rs Normal file
View File

@@ -0,0 +1,68 @@
use halo2_proofs::{
arithmetic::FieldExt,
circuit::*,
plonk::*,
poly::Rotation,
};
#[derive(Clone, Debug)]
pub struct IsZeroConfig<F> {
pub value_inv: Column<Advice>,
pub is_zero_expr: Expression<F>,
}
pub struct IsZeroChip<F: FieldExt> {
config: IsZeroConfig<F>,
}
impl<F:FieldExt> IsZeroChip<F> {
pub fn construct(config: IsZeroConfig<F>) -> Self {
IsZeroChip { config }
}
pub fn configure(
meta: &mut ConstraintSystem<F>,
q_enable: impl FnOnce(&mut VirtualCells<'_, F>) -> Expression<F>,
value: impl FnOnce(&mut VirtualCells<'_, F>) -> Expression<F>,
value_inv: Column<Advice>,
) -> IsZeroConfig<F> {
//let value_inv = meta.advice_column();
let mut is_zero_expr = Expression::Constant(F::zero());
meta.create_gate("is_zero", |meta| {
// valid | value | value_inv | 1 - value * value_inv | value * (1 - value_inv * value)
// yes | x | 1/x | 0 | 0
// no | x | 0 | 1 | x
// yes | 0 | 0 | 1 | 0
// yes | 0 | y | 1 | 0
let value = value(meta);
let value_inv = meta.query_advice(value_inv, Rotation::cur());
let q_enable = q_enable(meta);
is_zero_expr = Expression::Constant(F::one()) - value.clone() * value_inv;
vec![q_enable * value * is_zero_expr.clone()]
});
IsZeroConfig {
value_inv,
is_zero_expr,
}
}
pub fn assign(
&self,
region: &mut Region<'_, F>,
offset: usize,
value: Value<F>,
) -> Result<(), Error> {
let value_inv = value.map(|value| value.invert().unwrap_or(F::zero()));
region.assign_advice(
|| "value inv",
self.config.value_inv,
offset,
|| value_inv,
)?;
Ok(())
}
}

3
src/lib.rs Normal file
View File

@@ -0,0 +1,3 @@
mod gadget;
pub use gadget::*;