Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix underconstrained sign function. #84

Merged
merged 2 commits into from
Jan 23, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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
Loading