From 492974eaab0c970eb5d2e731ac87ddd05e2b6e5f Mon Sep 17 00:00:00 2001 From: parazyd Date: Tue, 27 Feb 2024 11:23:31 +0100 Subject: [PATCH] zk/gadget: Implement is_equal and assert_equal chips. --- src/zk/gadget/cond_select.rs | 1 + src/zk/gadget/is_equal.rs | 205 +++++++++++++++++++++++++++++++++++ src/zk/gadget/mod.rs | 3 + 3 files changed, 209 insertions(+) create mode 100644 src/zk/gadget/is_equal.rs diff --git a/src/zk/gadget/cond_select.rs b/src/zk/gadget/cond_select.rs index a8971bfdc..7ff7f2fea 100644 --- a/src/zk/gadget/cond_select.rs +++ b/src/zk/gadget/cond_select.rs @@ -120,6 +120,7 @@ impl + Ord> ConditionalSelectChip { let cell = region.assign_advice(|| "select result", config.advices[2], 0, || selected)?; + Ok(cell) }, )?; diff --git a/src/zk/gadget/is_equal.rs b/src/zk/gadget/is_equal.rs new file mode 100644 index 000000000..ca5d67221 --- /dev/null +++ b/src/zk/gadget/is_equal.rs @@ -0,0 +1,205 @@ +/* This file is part of DarkFi (https://dark.fi) + * + * Copyright (C) 2020-2024 Dyne.org foundation + * Copyright (C) 2022 zkMove Authors (Apache-2.0) + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU Affero General Public License as + * published by the Free Software Foundation, either version 3 of the + * License, or (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Affero General Public License for more details. + * + * You should have received a copy of the GNU Affero General Public License + * along with this program. If not, see . + */ + +use std::marker::PhantomData; + +use halo2_proofs::{ + circuit::{AssignedCell, Chip, Layouter, Region}, + pasta::group::ff::WithSmallOrderMulGroup, + plonk::{self, Advice, Column, ConstraintSystem, Expression, Selector}, + poly::Rotation, +}; + +const NUM_OF_UTILITY_ADVICE_COLUMNS: usize = 4; + +#[derive(Clone, Debug)] +pub struct IsEqualConfig + Ord> { + s_is_eq: Selector, + advices: [Column; NUM_OF_UTILITY_ADVICE_COLUMNS], + _marker: PhantomData, +} + +pub struct IsEqualChip + Ord> { + config: IsEqualConfig, +} + +impl + Ord> Chip for IsEqualChip { + type Config = IsEqualConfig; + type Loaded = (); + + fn config(&self) -> &Self::Config { + &self.config + } + + fn loaded(&self) -> &Self::Loaded { + &() + } +} + +impl + Ord> IsEqualChip { + pub fn construct( + config: >::Config, + _loaded: >::Loaded, + ) -> Self { + Self { config } + } + + pub fn configure( + meta: &mut ConstraintSystem, + advices: [Column; NUM_OF_UTILITY_ADVICE_COLUMNS], + ) -> >::Config { + let s_is_eq = meta.selector(); + meta.create_gate("is_eq", |meta| { + let lhs = meta.query_advice(advices[0], Rotation::cur()); + let rhs = meta.query_advice(advices[1], Rotation::cur()); + let out = meta.query_advice(advices[2], Rotation::cur()); + let delta_invert = meta.query_advice(advices[3], Rotation::cur()); + let s_is_eq = meta.query_selector(s_is_eq); + let one = Expression::Constant(F::ONE); + + vec![ + // out is 0 or 1 + s_is_eq.clone() * (out.clone() * (one.clone() - out.clone())), + // if a != b then (a - b) * inverse(a - b) == 1 - out + // if a == b then (a - b) * 1 == 1 - out + s_is_eq.clone() * + ((lhs.clone() - rhs.clone()) * delta_invert.clone() + (out - one.clone())), + // constrain delta_invert: (a - b) * inverse(a - b) must be 1 or 0 + s_is_eq * (lhs.clone() - rhs.clone()) * ((lhs - rhs) * delta_invert - one), + ] + }); + + IsEqualConfig { s_is_eq, advices, _marker: PhantomData } + } + + pub fn is_eq_with_output( + &self, + layouter: &mut impl Layouter, + a: AssignedCell, + b: AssignedCell, + ) -> Result, plonk::Error> { + let config = self.config(); + + let out = layouter.assign_region( + || "is_eq", + |mut region: Region<'_, F>| { + config.s_is_eq.enable(&mut region, 0)?; + + a.copy_advice(|| "copy a", &mut region, config.advices[0], 0)?; + b.copy_advice(|| "copy b", &mut region, config.advices[1], 0)?; + + let delta_invert = a.value().copied().to_field().zip(b.value()).map(|(a, b)| { + if a == b.into() { + F::ONE.into() + } else { + let delta = a - *b; + delta.invert() + } + }); + + region.assign_advice(|| "delta invert", config.advices[3], 0, || delta_invert)?; + + let is_eq = + a.value_field().evaluate().zip(b.value_field().evaluate()).map(|(lhs, rhs)| { + if lhs == rhs { + F::ONE + } else { + F::ZERO + } + }); + + let cell = region.assign_advice(|| "is_eq", config.advices[2], 0, || is_eq)?; + Ok(cell) + }, + )?; + + Ok(out) + } +} + +#[derive(Clone, Debug)] +pub struct AssertEqualConfig + Ord> { + s_eq: Selector, + advices: [Column; 2], + _marker: PhantomData, +} + +pub struct AssertEqualChip + Ord> { + config: AssertEqualConfig, +} + +impl + Ord> Chip for AssertEqualChip { + type Config = AssertEqualConfig; + type Loaded = (); + + fn config(&self) -> &Self::Config { + &self.config + } + + fn loaded(&self) -> &Self::Loaded { + &() + } +} + +impl + Ord> AssertEqualChip { + pub fn construct( + config: >::Config, + _loaded: >::Loaded, + ) -> Self { + Self { config } + } + + pub fn configure( + meta: &mut ConstraintSystem, + advices: [Column; 2], + ) -> >::Config { + let s_eq = meta.selector(); + meta.create_gate("assert_eq", |meta| { + let lhs = meta.query_advice(advices[0], Rotation::cur()); + let rhs = meta.query_advice(advices[1], Rotation::cur()); + let s_eq = meta.query_selector(s_eq); + + vec![s_eq * (lhs - rhs)] + }); + + AssertEqualConfig { s_eq, advices, _marker: PhantomData } + } + + pub fn assert_equal( + &self, + layouter: &mut impl Layouter, + a: AssignedCell, + b: AssignedCell, + ) -> Result<(), plonk::Error> { + let config = self.config(); + + layouter.assign_region( + || "assert_eq", + |mut region: Region<'_, F>| { + config.s_eq.enable(&mut region, 0)?; + + a.copy_advice(|| "copy a", &mut region, config.advices[0], 0)?; + b.copy_advice(|| "copy b", &mut region, config.advices[1], 0)?; + Ok(()) + }, + )?; + + Ok(()) + } +} diff --git a/src/zk/gadget/mod.rs b/src/zk/gadget/mod.rs index e2a2798ad..a3dfeaa97 100644 --- a/src/zk/gadget/mod.rs +++ b/src/zk/gadget/mod.rs @@ -31,6 +31,9 @@ pub mod less_than; /// is_zero comparison gadget pub mod is_zero; +/// is_equal comparison gadget +pub mod is_equal; + /// Conditional selection pub mod cond_select;