Implement conditional_check_verify for NIZKs (#195)

* Implement `ToBitsGadget` for `UInt8` and `Vec<UInt8>`
* Add `kary_or` function to `Boolean`.
This commit is contained in:
Bruno França
2020-04-22 21:30:33 +01:00
committed by GitHub
parent 5cc094be6b
commit bbb7d75ec8
7 changed files with 97 additions and 5 deletions

View File

@@ -20,4 +20,16 @@ pub trait NIZKVerifierGadget<N: NIZK, ConstraintF: Field> {
CS: ConstraintSystem<ConstraintF>, CS: ConstraintSystem<ConstraintF>,
I: Iterator<Item = &'a T>, I: Iterator<Item = &'a T>,
T: 'a + ToBitsGadget<ConstraintF> + ?Sized; T: 'a + ToBitsGadget<ConstraintF> + ?Sized;
fn conditional_check_verify<'a, CS, I, T>(
cs: CS,
verification_key: &Self::VerificationKeyGadget,
input: I,
proof: &Self::ProofGadget,
condition: &Boolean,
) -> Result<(), SynthesisError>
where
CS: ConstraintSystem<ConstraintF>,
I: Iterator<Item = &'a T>,
T: 'a + ToBitsGadget<ConstraintF> + ?Sized;
} }

View File

@@ -109,10 +109,31 @@ where
type ProofGadget = ProofGadget<PairingE, ConstraintF, P>; type ProofGadget = ProofGadget<PairingE, ConstraintF, P>;
fn check_verify<'a, CS, I, T>( fn check_verify<'a, CS, I, T>(
cs: CS,
vk: &Self::VerificationKeyGadget,
public_inputs: I,
proof: &Self::ProofGadget,
) -> Result<(), SynthesisError>
where
CS: ConstraintSystem<ConstraintF>,
I: Iterator<Item = &'a T>,
T: 'a + ToBitsGadget<ConstraintF> + ?Sized,
{
<Self as NIZKVerifierGadget<Gm17<PairingE, C, V>, ConstraintF>>::conditional_check_verify(
cs,
vk,
public_inputs,
proof,
&Boolean::constant(true),
)
}
fn conditional_check_verify<'a, CS, I, T>(
mut cs: CS, mut cs: CS,
vk: &Self::VerificationKeyGadget, vk: &Self::VerificationKeyGadget,
mut public_inputs: I, mut public_inputs: I,
proof: &Self::ProofGadget, proof: &Self::ProofGadget,
condition: &Boolean,
) -> Result<(), SynthesisError> ) -> Result<(), SynthesisError>
where where
CS: ConstraintSystem<ConstraintF>, CS: ConstraintSystem<ConstraintF>,
@@ -189,8 +210,8 @@ where
let test2 = P::final_exponentiation(cs.ns(|| "Final Exp 2"), &test2_exp)?; let test2 = P::final_exponentiation(cs.ns(|| "Final Exp 2"), &test2_exp)?;
let one = P::GTGadget::one(cs.ns(|| "GT One"))?; let one = P::GTGadget::one(cs.ns(|| "GT One"))?;
test1.enforce_equal(cs.ns(|| "Test 1"), &one)?; test1.conditional_enforce_equal(cs.ns(|| "Test 1"), &one, condition)?;
test2.enforce_equal(cs.ns(|| "Test 2"), &one)?; test2.conditional_enforce_equal(cs.ns(|| "Test 2"), &one, condition)?;
Ok(()) Ok(())
} }
} }

View File

@@ -35,10 +35,10 @@ impl<E: PairingEngine, C: ConstraintSynthesizer<E::Fr>, V: ToConstraintField<E::
{ {
type Circuit = C; type Circuit = C;
type AssignedCircuit = C; type AssignedCircuit = C;
type VerifierInput = V;
type ProvingParameters = Parameters<E>; type ProvingParameters = Parameters<E>;
type VerificationParameters = VerifyingKey<E>; type VerificationParameters = VerifyingKey<E>;
type PreparedVerificationParameters = PreparedVerifyingKey<E>; type PreparedVerificationParameters = PreparedVerifyingKey<E>;
type VerifierInput = V;
type Proof = Proof<E>; type Proof = Proof<E>;
fn setup<R: Rng>( fn setup<R: Rng>(

View File

@@ -110,10 +110,31 @@ where
type ProofGadget = ProofGadget<PairingE, ConstraintF, P>; type ProofGadget = ProofGadget<PairingE, ConstraintF, P>;
fn check_verify<'a, CS, I, T>( fn check_verify<'a, CS, I, T>(
cs: CS,
vk: &Self::VerificationKeyGadget,
public_inputs: I,
proof: &Self::ProofGadget,
) -> Result<(), SynthesisError>
where
CS: ConstraintSystem<ConstraintF>,
I: Iterator<Item = &'a T>,
T: 'a + ToBitsGadget<ConstraintF> + ?Sized,
{
<Self as NIZKVerifierGadget<Groth16<PairingE, C, V>, ConstraintF>>::conditional_check_verify(
cs,
vk,
public_inputs,
proof,
&Boolean::constant(true),
)
}
fn conditional_check_verify<'a, CS, I, T>(
mut cs: CS, mut cs: CS,
vk: &Self::VerificationKeyGadget, vk: &Self::VerificationKeyGadget,
mut public_inputs: I, mut public_inputs: I,
proof: &Self::ProofGadget, proof: &Self::ProofGadget,
condition: &Boolean,
) -> Result<(), SynthesisError> ) -> Result<(), SynthesisError>
where where
CS: ConstraintSystem<ConstraintF>, CS: ConstraintSystem<ConstraintF>,
@@ -161,7 +182,7 @@ where
let test = P::final_exponentiation(cs.ns(|| "Final Exp"), &test_exp).unwrap(); let test = P::final_exponentiation(cs.ns(|| "Final Exp"), &test_exp).unwrap();
test.enforce_equal(cs.ns(|| "Test 1"), &pvk.alpha_g1_beta_g2)?; test.conditional_enforce_equal(cs.ns(|| "Test 1"), &pvk.alpha_g1_beta_g2, condition)?;
Ok(()) Ok(())
} }
} }

View File

@@ -35,10 +35,10 @@ impl<E: PairingEngine, C: ConstraintSynthesizer<E::Fr>, V: ToConstraintField<E::
{ {
type Circuit = C; type Circuit = C;
type AssignedCircuit = C; type AssignedCircuit = C;
type VerifierInput = V;
type ProvingParameters = Parameters<E>; type ProvingParameters = Parameters<E>;
type VerificationParameters = VerifyingKey<E>; type VerificationParameters = VerifyingKey<E>;
type PreparedVerificationParameters = PreparedVerifyingKey<E>; type PreparedVerificationParameters = PreparedVerifyingKey<E>;
type VerifierInput = V;
type Proof = Proof<E>; type Proof = Proof<E>;
fn setup<R: Rng>( fn setup<R: Rng>(

View File

@@ -549,6 +549,22 @@ impl Boolean {
Ok(cur) Ok(cur)
} }
pub fn kary_or<ConstraintF, CS>(mut cs: CS, bits: &[Self]) -> Result<Self, SynthesisError>
where
ConstraintF: Field,
CS: ConstraintSystem<ConstraintF>,
{
assert!(!bits.is_empty());
let mut bits = bits.iter();
let mut cur: Self = *bits.next().unwrap();
for (i, next) in bits.enumerate() {
cur = Boolean::or(cs.ns(|| format!("OR {}", i)), &cur, next)?;
}
Ok(cur)
}
/// Asserts that at least one operand is false. /// Asserts that at least one operand is false.
pub fn enforce_nand<ConstraintF, CS>(mut cs: CS, bits: &[Self]) -> Result<(), SynthesisError> pub fn enforce_nand<ConstraintF, CS>(mut cs: CS, bits: &[Self]) -> Result<(), SynthesisError>
where where

View File

@@ -58,6 +58,15 @@ impl<ConstraintF: Field> ToBitsGadget<ConstraintF> for Vec<Boolean> {
} }
} }
impl<ConstraintF: Field> ToBitsGadget<ConstraintF> for UInt8 {
fn to_bits<CS: ConstraintSystem<ConstraintF>>(
&self,
_cs: CS,
) -> Result<Vec<Boolean>, SynthesisError> {
Ok(self.into_bits_le())
}
}
impl<ConstraintF: Field> ToBitsGadget<ConstraintF> for [UInt8] { impl<ConstraintF: Field> ToBitsGadget<ConstraintF> for [UInt8] {
fn to_bits<CS: ConstraintSystem<ConstraintF>>( fn to_bits<CS: ConstraintSystem<ConstraintF>>(
&self, &self,
@@ -71,6 +80,19 @@ impl<ConstraintF: Field> ToBitsGadget<ConstraintF> for [UInt8] {
} }
} }
impl<ConstraintF: Field> ToBitsGadget<ConstraintF> for Vec<UInt8> {
fn to_bits<CS: ConstraintSystem<ConstraintF>>(
&self,
_cs: CS,
) -> Result<Vec<Boolean>, SynthesisError> {
let mut result = Vec::with_capacity(&self.len() * 8);
for byte in self {
result.extend_from_slice(&byte.into_bits_le());
}
Ok(result)
}
}
pub trait ToBytesGadget<ConstraintF: Field> { pub trait ToBytesGadget<ConstraintF: Field> {
/// Outputs a canonical byte-wise representation of `self`. /// Outputs a canonical byte-wise representation of `self`.
/// ///