Unsatisfied constraints with field emulation gadgets

[srinathsetty]

There might be an issue with the field emulation library. The tests associated with bls12-381 emulation with pasta fields pass. However, when I changed the field from bls12-381's base field to BN254's base field (and adjusted EmulatedFieldParams trait appropriately), the tests fail in the following manner (similar errors for other tests).

---- fields::bn_fp::tests::test_random_add stdout ----
fail: "a+b = c/a = b/check limbs equality/right shift to get carry 0/enforce equality between input value and weighted sum of higher order bits"
Some("a+b = c/a = b/check limbs equality/right shift to get carry 0/enforce equality between input value and weighted sum of higher order bits")
fail: "a+b = c/a = b/check limbs equality/right shift to get carry 0/enforce equality between input value and weighted sum of higher order bits"
thread 'fields::bn_fp::tests::test_random_add' panicked at crates/bls12381/src/fields/bn_fp.rs:279:9:
assertion failed: cs.is_satisfied()
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Here's what the trait implementation looks like:

use halo2curves::bn256::Fq as BnFp;

pub struct Bn254FpParams;

impl EmulatedFieldParams for Bn254FpParams {
    fn num_limbs() -> usize {
        4
    }

    fn bits_per_limb() -> usize {
        64
    }

    fn modulus() -> BigInt {
        BigInt::parse_bytes(
            b"30644e72e131a029b85045b68181585d97816a916871ca8d3c208c16d87cfd47",             
            16,
        )
        .unwrap()
    }

    fn is_modulus_pseudo_mersenne() -> bool {
        false
    }

    fn pseudo_mersenne_params() -> Option<PseudoMersennePrime> {
        None
    }
}

pub type Bn254Fp<F> = EmulatedFieldElement<F, Bn254FpParams>;

[srinathsetty]

FYI: @huitseeker @wwared

[wwared]

To clarify, the EmulatedFieldParams trait is for specifying the field that is being emulated, not the native field that the emulation happens in. In the case of the pairing gadget, we're emulating BLS12-381 so the field params should always be the BLS12-381 ones. In the tests, we instantiate the TestConstraintSystem using pasta_curves::Fp and this is what defines the native field that the emulation happens in.

Were you trying to change the native field from pasta's to BN256 or change the emulated field from BLS12-381 to BN256? If the former, you shouldn't need to make an EmulatedFieldParams at all, you would just change the generic parameter in this line (and the same for all other tests) to be halo2curves::bn256::Fq instead. (I've tried doing this in some files and none of the tests failed for me).

If you were trying to use the emulation gadgets for emulating BN256 in some other curve however, then it makes sense that the tests failed since the native code just uses bls12_381's Fp data type for calculating the expected result of the emulated operations. These would need to be replaced with a bn256 equivalent native crate (and the gadget code would probably need to be updated as necessary as well). If this is the case, can you share the code of your failing test_random_add test?

[srinathsetty]

If you were trying to use the emulation gadgets for emulating BN256 in some other curve however, then it makes sense that the tests failed since the native code just uses bls12_381's Fp data type for calculating the expected result of the emulated operations. These would need to be replaced with a bn256 equivalent.

I am attempting to emulate BN254's base field with pasta curves (in place of emulating bls12-381 with pasta curves). I did change the way BN254's base field is implemented via the halo2curves crate: use halo2curves::bn256::Fq as BnFp;

I'll share the code in the next comment.

[srinathsetty]

Here's the failing code (with minor edits compared to bls12-381's fp.rs to get it to emulate BN254's base field). We would just need to include halo2curves crate in Cargo.toml.

use bellpepper_core::{
    boolean::{AllocatedBit, Boolean},
    ConstraintSystem, SynthesisError,
};
use bellpepper_emulated::field_element::{
    EmulatedFieldElement, EmulatedFieldParams, PseudoMersennePrime,
};
use halo2curves::bn256::Fq as BnFp;
use ff::{PrimeField, PrimeFieldBits};
use num_bigint::{BigInt, Sign};
use ff::Field;

pub struct Bn254FpParams;

impl EmulatedFieldParams for Bn254FpParams {
    fn num_limbs() -> usize {
        4
    }

    fn bits_per_limb() -> usize {
        64
    }

    fn modulus() -> BigInt {
        BigInt::parse_bytes(
            b"30644e72e131a029b85045b68181585d97816a916871ca8d3c208c16d87cfd47", //30644e72e131a029b85045b68181585d97816a916871ca8d3c208c16d87cfd47",
            16,
        )
        .unwrap()
    }

    fn is_modulus_pseudo_mersenne() -> bool {
        false
    }

    fn pseudo_mersenne_params() -> Option<PseudoMersennePrime> {
        None
    }
}

pub type Bn254Fp<F> = EmulatedFieldElement<F, Bn254FpParams>;

#[derive(Clone)]
pub struct FpElement<F: PrimeField + PrimeFieldBits>(pub(crate) Bn254Fp<F>);

impl<F> From<&BnFp> for FpElement<F>
where
    F: PrimeField + PrimeFieldBits,
{
    fn from(value: &BnFp) -> Self {
        let bytes = value.to_bytes();
        assert!(bytes.len() == 32);
        let val = BigInt::from_bytes_be(Sign::Plus, &bytes);
        Self(Bn254Fp::<F>::from(&val))
    }
}

pub(crate) fn bigint_to_fpelem(val: &BigInt) -> Option<BnFp> {
    use num_traits::Zero;
    if val >= &Bn254FpParams::modulus() {
        return None;
    }
    let be_bytes = BigInt::to_bytes_be(val);
    if be_bytes.0 != Sign::Plus {
        // the sign is only non-positive if the value is exactly 0
        assert!(val == &BigInt::zero());
    }
    let mut bytes: Vec<u8> = be_bytes.1;
    assert!(bytes.len() <= 32);
    bytes.splice(0..0, vec![0; 32 - bytes.len()]);
    let bytes: [u8; 32] = bytes.try_into().unwrap();
    Some(BnFp::from_bytes(&bytes).unwrap())
}

pub(crate) fn emulated_to_native<F>(value: &Bn254Fp<F>) -> BnFp
where
    F: PrimeField + PrimeFieldBits,
{
    use std::ops::Rem;
    let p = &Bn254FpParams::modulus();
    let val = BigInt::from(value).rem(p);
    bigint_to_fpelem(&val).unwrap()
}

impl<F> From<&FpElement<F>> for BnFp
where
    F: PrimeField + PrimeFieldBits,
{
    fn from(value: &FpElement<F>) -> Self {
        emulated_to_native(&value.0)
    }
}

impl<F: PrimeField + PrimeFieldBits> FpElement<F> {
    pub fn from_dec(val: &str) -> Option<Self> {
        BigInt::parse_bytes(val.as_bytes(), 10)
            .as_ref()
            .and_then(bigint_to_fpelem)
            .as_ref()
            .map(Self::from)
    }

    pub fn zero() -> Self {
        Self(Bn254Fp::zero())
    }

    pub fn one() -> Self {
        Self(Bn254Fp::one())
    }

    pub fn alloc_element<CS>(cs: &mut CS, value: &BnFp) -> Result<Self, SynthesisError>
    where
        CS: ConstraintSystem<F>,
    {
        let val_alloc = FpElement::<F>::from(value);
        let alloc = val_alloc
            .0
            .allocate_field_element_unchecked(&mut cs.namespace(|| "alloc fp elm"))?;

        Ok(Self(alloc))
    }

    pub fn assert_is_equal<CS>(cs: &mut CS, a: &Self, b: &Self) -> Result<(), SynthesisError>
    where
        CS: ConstraintSystem<F>,
    {
        Bn254Fp::<F>::assert_is_equal(&mut cs.namespace(|| "a = b"), &a.0, &b.0)?;
        Ok(())
    }

    pub fn reduce<CS>(&self, cs: &mut CS) -> Result<Self, SynthesisError>
    where
        CS: ConstraintSystem<F>,
    {
        let val_reduced = self.0.reduce(&mut cs.namespace(|| "val mod P"))?;
        Ok(Self(val_reduced))
    }

    pub fn assert_equality_to_constant<CS>(
        &self,
        cs: &mut CS,
        constant: &Self,
    ) -> Result<(), SynthesisError>
    where
        CS: ConstraintSystem<F>,
    {
        self.0
            .assert_equality_to_constant(&mut cs.namespace(|| "val =? (const) val"), &constant.0)?;
        Ok(())
    }

    pub fn alloc_is_zero<CS>(&self, cs: &mut CS) -> Result<AllocatedBit, SynthesisError>
    where
        CS: ConstraintSystem<F>,
    {
        self.0.alloc_is_zero(&mut cs.namespace(|| "val =? 0"))
    }

    pub fn add<CS>(&self, cs: &mut CS, value: &Self) -> Result<Self, SynthesisError>
    where
        CS: ConstraintSystem<F>,
    {
        let res = self.0.add(&mut cs.namespace(|| "a + b"), &value.0)?;
        Ok(Self(res))
    }

    pub fn sub<CS>(&self, cs: &mut CS, value: &Self) -> Result<Self, SynthesisError>
    where
        CS: ConstraintSystem<F>,
    {
        let res = self.0.sub(&mut cs.namespace(|| "a - b"), &value.0)?;
        Ok(Self(res))
    }

    pub fn mul<CS>(&self, cs: &mut CS, value: &Self) -> Result<Self, SynthesisError>
    where
        CS: ConstraintSystem<F>,
    {
        let res = self.0.mul(&mut cs.namespace(|| "a * b"), &value.0)?;
        Ok(Self(res))
    }

    pub fn inverse<CS>(&self, cs: &mut CS) -> Result<Self, SynthesisError>
    where
        CS: ConstraintSystem<F>,
    {
        let res = self.0.inverse(&mut cs.namespace(|| "x.inverse()"))?;
        Ok(Self(res))
    }

    pub fn div_unchecked<CS>(&self, cs: &mut CS, value: &Self) -> Result<Self, SynthesisError>
    where
        CS: ConstraintSystem<F>,
    {
        let res = self.0.divide(&mut cs.namespace(|| "a div b"), &value.0)?;
        Ok(Self(res))
    }

    pub fn square<CS>(&self, cs: &mut CS) -> Result<Self, SynthesisError>
    where
        CS: ConstraintSystem<F>,
    {
        self.mul(&mut cs.namespace(|| "x.square()"), self)
    }

    pub fn double<CS>(&self, cs: &mut CS) -> Result<Self, SynthesisError>
    where
        CS: ConstraintSystem<F>,
    {
        self.add(&mut cs.namespace(|| "x.double()"), self)
    }

    pub fn mul_const<CS>(&self, cs: &mut CS, value: &BigInt) -> Result<Self, SynthesisError>
    where
        CS: ConstraintSystem<F>,
    {
        let res = self
            .0
            .mul_const(&mut cs.namespace(|| "a * constval"), value)?;
        Ok(Self(res))
    }

    pub fn neg<CS>(&self, cs: &mut CS) -> Result<Self, SynthesisError>
    where
        CS: ConstraintSystem<F>,
    {
        let res = self.0.neg(&mut cs.namespace(|| "-a"))?;
        Ok(Self(res))
    }

    pub fn conditionally_select<CS>(
        cs: &mut CS,
        z0: &Self,
        z1: &Self,
        condition: &Boolean,
    ) -> Result<Self, SynthesisError>
    where
        CS: ConstraintSystem<F>,
    {
        let res = Bn254Fp::<F>::conditionally_select(
            &mut cs.namespace(|| "cond val"),
            &z0.0,
            &z1.0,
            condition,
        )?;
        Ok(Self(res))
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use bellpepper_core::test_cs::TestConstraintSystem;
    use pasta_curves::Fp;

    use expect_test::{expect, Expect};
    fn expect_eq(computed: usize, expected: Expect) {
        expected.assert_eq(&computed.to_string());
    }

    #[test]
    fn test_random_add() {
        let mut rng = rand::thread_rng();
        let a = BnFp::random(&mut rng);
        let b = BnFp::random(&mut rng);
        let c = a + b;

        let mut cs = TestConstraintSystem::<Fp>::new();
        let a_alloc = FpElement::alloc_element(&mut cs.namespace(|| "alloc a"), &a).unwrap();
        let b_alloc = FpElement::alloc_element(&mut cs.namespace(|| "alloc b"), &b).unwrap();
        let c_alloc = FpElement::alloc_element(&mut cs.namespace(|| "alloc c"), &c).unwrap();
        let res_alloc = a_alloc.add(&mut cs.namespace(|| "a+b"), &b_alloc).unwrap();
        FpElement::assert_is_equal(&mut cs.namespace(|| "a+b = c"), &res_alloc, &c_alloc).unwrap();
        if !cs.is_satisfied() {
            eprintln!("{:?}", cs.which_is_unsatisfied())
        }
        assert!(cs.is_satisfied());
        expect_eq(cs.num_inputs(), expect!["1"]);
        expect_eq(cs.scalar_aux().len(), expect!["277"]);
        expect_eq(cs.num_constraints(), expect!["262"]);
    }
}

[wwared]

Alright, sorry for the confusion and thanks for the info! I can replicate the problem, and a quick look into it gave me:

• Trying to print the expected/calculated values in the test with eprintln!("c: {:?}\nr: {:?}", &c, BnFp::from(&res_alloc)); was dying in this line: Some(BnFp::from_bytes(&bytes).unwrap()). It seems that halo2curve's from_bytes expects little-endian and bigint_to_fpelem is calling .to_bytes_be() instead of .to_bytes_le()
• Fixing the above fixes the unwrap crash but the test keeps failing. However, the From impl for BnFpElement is also using from_bytes_be instead of from_bytes_le, so we fix the line let val = BigInt::from_bytes_be(Sign::Plus, &bytes); to call from_bytes_le instead as well
• Changing both of these functions to use little-endian instead makes the test pass!

[srinathsetty]

Fantastic! I was able to get this working on my side. Thanks for the help, @wwared!