From ac70805dd1c3463513dc4afc1579d40a13caa6a3 Mon Sep 17 00:00:00 2001 From: David Nevado Date: Thu, 11 Jan 2024 18:06:12 +0100 Subject: [PATCH 1/2] Fix underconstrained `sign` function. - `sign` has been moved from `maingate` to `integer` - An extra range check on the auxiliary witness has been added. --- integer/src/chip.rs | 46 ++++++++++++++++++++++-- integer/src/rns.rs | 3 ++ maingate/src/instructions.rs | 34 +----------------- maingate/src/main_gate.rs | 68 ------------------------------------ 4 files changed, 48 insertions(+), 103 deletions(-) diff --git a/integer/src/chip.rs b/integer/src/chip.rs index 39694251..b87a4fb7 100644 --- a/integer/src/chip.rs +++ b/integer/src/chip.rs @@ -5,7 +5,11 @@ use crate::instructions::{IntegerInstructions, Range}; use crate::rns::{Common, Integer, Rns}; use halo2::halo2curves::ff::PrimeField; use halo2::plonk::Error; -use maingate::{halo2, AssignedCondition, AssignedValue, MainGateInstructions, RegionCtx}; +use maingate::halo2::circuit::Value; +use maingate::{ + halo2, AssignedCondition, AssignedValue, CombinationOptionCommon, MainGateInstructions, + RangeInstructions, RegionCtx, Term, +}; use maingate::{MainGate, MainGateConfig}; use maingate::{RangeChip, RangeConfig}; @@ -516,7 +520,45 @@ impl, ) -> Result, Error> { self.assert_in_field(ctx, a)?; - self.main_gate().sign(ctx, a.limb(0)) + + // Assignes new value equals to `1` if least significant bit of `a` is `1` or assigns + // `0` if lsb of `a` is `0`. + let w: Value<(N, N)> = a.limb(0).value().map(|value| { + use maingate::{big_to_fe, fe_to_big}; + use num_bigint::BigUint; + use num_traits::{One, Zero}; + let value = &fe_to_big(*value); + let half = big_to_fe(value / 2usize); + let sign = ((value & BigUint::one() != BigUint::zero()) as u64).into(); + (sign, half) + }); + + let sign = self.main_gate.assign_bit(ctx, w.map(|w| w.0))?; + + let half_a = self + .main_gate + .apply( + ctx, + [ + Term::Unassigned(w.map(|w| w.1), N::from(2)), + Term::Assigned(&sign, N::ONE), + Term::Assigned(a.limb(0), -N::ONE), + ], + N::ZERO, + CombinationOptionCommon::OneLinerAdd.into(), + )? + .swap_remove(0); + + // Enforce half_a in [0, (LIMB_MAX_VAL / 2) ) + let assigned = self.range_chip.decompose( + ctx, + half_a.value_field().evaluate(), + Self::sublimb_bit_len(), + BIT_LEN_LIMB - 1, + )?; + self.main_gate.assert_equal(ctx, &assigned.0, &half_a)?; + + Ok(sign) } } diff --git a/integer/src/rns.rs b/integer/src/rns.rs index 9d0f0c37..b5875598 100644 --- a/integer/src/rns.rs +++ b/integer/src/rns.rs @@ -618,12 +618,15 @@ impl: Chip { cond: &AssignedCondition, ) -> Result, Error>; - /// Assignes new value equals to `1` if first bit of `a` is `1` or assigns - /// `0` if first bit of `a` is `0` - fn sign( - &self, - ctx: &mut RegionCtx<'_, F>, - a: &AssignedValue, - ) -> Result, Error> { - let w: Value<(F, F)> = a.value().map(|value| { - use num_bigint::BigUint; - use num_traits::{One, Zero}; - let value = &fe_to_big(*value); - let half = big_to_fe(value / 2usize); - let sign = ((value & BigUint::one() != BigUint::zero()) as u64).into(); - (sign, half) - }); - - let sign = self.assign_bit(ctx, w.map(|w| w.0))?; - - self.apply( - ctx, - [ - Term::Unassigned(w.map(|w| w.1), F::from(2)), - Term::Assigned(&sign, F::ONE), - Term::Assigned(a, -F::ONE), - ], - F::ZERO, - CombinationOptionCommon::OneLinerAdd.into(), - )?; - - Ok(sign) - } - /// Assigns array values of bit values which is equal to decomposition of /// given assigned value fn to_bits( diff --git a/maingate/src/main_gate.rs b/maingate/src/main_gate.rs index fd842bea..0d15fda8 100644 --- a/maingate/src/main_gate.rs +++ b/maingate/src/main_gate.rs @@ -1522,72 +1522,4 @@ mod tests { }; assert_eq!(prover.verify(), Ok(())); } - - #[derive(Default)] - struct TestCircuitSign { - _marker: PhantomData, - } - - impl Circuit for TestCircuitSign { - type Config = TestCircuitConfig; - type FloorPlanner = SimpleFloorPlanner; - #[cfg(feature = "circuit-params")] - type Params = (); - - fn without_witnesses(&self) -> Self { - Self::default() - } - - fn configure(meta: &mut ConstraintSystem) -> Self::Config { - let main_gate_config = MainGate::::configure(meta); - TestCircuitConfig { main_gate_config } - } - - fn synthesize( - &self, - config: Self::Config, - mut layouter: impl Layouter, - ) -> Result<(), Error> { - let main_gate = MainGate:: { - config: config.main_gate_config, - _marker: PhantomData, - }; - - layouter.assign_region( - || "region 0", - |region| { - let offset = 0; - let ctx = &mut RegionCtx::new(region, offset); - - let a = F::from(20u64); - let assigned = main_gate.assign_value(ctx, Value::known(a))?; - let assigned_sign = main_gate.sign(ctx, &assigned)?; - main_gate.assert_zero(ctx, &assigned_sign)?; - - let a = F::from(21u64); - let assigned = main_gate.assign_value(ctx, Value::known(a))?; - let assigned_sign = main_gate.sign(ctx, &assigned)?; - main_gate.assert_one(ctx, &assigned_sign)?; - - Ok(()) - }, - )?; - - Ok(()) - } - } - - #[test] - fn test_main_gate_sign() { - const K: u32 = 10; - let circuit = TestCircuitSign:: { - _marker: PhantomData::, - }; - let public_inputs = vec![vec![]]; - let prover = match MockProver::run(K, &circuit, public_inputs) { - Ok(prover) => prover, - Err(e) => panic!("{:#?}", e), - }; - assert_eq!(prover.verify(), Ok(())); - } } From 327f58b6a0718c6a4faf4cb3fd3d926f88c539df Mon Sep 17 00:00:00 2001 From: David Nevado Date: Tue, 23 Jan 2024 17:21:44 +0100 Subject: [PATCH 2/2] update toolchain --- rust-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain b/rust-toolchain index 7cc6ef41..dc87e8af 100644 --- a/rust-toolchain +++ b/rust-toolchain @@ -1 +1 @@ -1.63.0 \ No newline at end of file +1.74.0