Skip to content

Commit

Permalink
Merge pull request #84 from privacy-scaling-explorations/nev@fix/sign
Browse files Browse the repository at this point in the history
Fix underconstrained `sign` function.
  • Loading branch information
davidnevadoc authored Jan 23, 2024
2 parents 5233325 + 327f58b commit 8260abc
Show file tree
Hide file tree
Showing 5 changed files with 49 additions and 104 deletions.
46 changes: 44 additions & 2 deletions integer/src/chip.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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};

Expand Down Expand Up @@ -516,7 +520,45 @@ impl<W: PrimeField, N: PrimeField, const NUMBER_OF_LIMBS: usize, const BIT_LEN_L
a: &AssignedInteger<W, N, NUMBER_OF_LIMBS, BIT_LEN_LIMB>,
) -> Result<AssignedCondition<N>, 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)
}
}

Expand Down
3 changes: 3 additions & 0 deletions integer/src/rns.rs
Original file line number Diff line number Diff line change
Expand Up @@ -618,12 +618,15 @@ impl<W: PrimeField, N: PrimeField, const NUMBER_OF_LIMBS: usize, const BIT_LEN_L
self.max_most_significant_operand_limb.bits() as usize % self.bit_len_lookup;
let max_most_significant_reduced_limb_size =
self.max_most_significant_reduced_limb.bits() as usize % self.bit_len_lookup;
// For sign function
let sign_aux = self.bit_len_lookup - 1;
vec![
self.mul_v_bit_len % self.bit_len_lookup,
self.red_v_bit_len % self.bit_len_lookup,
max_most_significant_mul_quotient_limb_size,
max_most_significant_operand_limb_size,
max_most_significant_reduced_limb_size,
sign_aux,
]
}
}
Expand Down
34 changes: 1 addition & 33 deletions maingate/src/instructions.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ use crate::{
};
use halo2wrong::{
curves::ff::PrimeField,
utils::{big_to_fe, decompose, fe_to_big, power_of_two},
utils::{decompose, power_of_two},
RegionCtx,
};
use std::iter;
Expand Down Expand Up @@ -962,38 +962,6 @@ pub trait MainGateInstructions<F: PrimeField, const WIDTH: usize>: Chip<F> {
cond: &AssignedCondition<F>,
) -> Result<AssignedValue<F>, 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<F>,
) -> Result<AssignedCondition<F>, 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(
Expand Down
68 changes: 0 additions & 68 deletions maingate/src/main_gate.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1522,72 +1522,4 @@ mod tests {
};
assert_eq!(prover.verify(), Ok(()));
}

#[derive(Default)]
struct TestCircuitSign<F: PrimeField> {
_marker: PhantomData<F>,
}

impl<F: PrimeField> Circuit<F> for TestCircuitSign<F> {
type Config = TestCircuitConfig;
type FloorPlanner = SimpleFloorPlanner;
#[cfg(feature = "circuit-params")]
type Params = ();

fn without_witnesses(&self) -> Self {
Self::default()
}

fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
let main_gate_config = MainGate::<F>::configure(meta);
TestCircuitConfig { main_gate_config }
}

fn synthesize(
&self,
config: Self::Config,
mut layouter: impl Layouter<F>,
) -> Result<(), Error> {
let main_gate = MainGate::<F> {
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::<Fp> {
_marker: PhantomData::<Fp>,
};
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(()));
}
}
2 changes: 1 addition & 1 deletion rust-toolchain
Original file line number Diff line number Diff line change
@@ -1 +1 @@
1.63.0
1.74.0

0 comments on commit 8260abc

Please sign in to comment.