Refactor NIZK/MT verification to return a bit

This commit is contained in:
Pratyush Mishra
2020-08-29 13:04:13 -07:00
parent 6cca9327be
commit d2d1b61d08
6 changed files with 46 additions and 111 deletions

View File

@@ -30,39 +30,21 @@ where
parameters: &CRHGadget::ParametersVar,
root: &CRHGadget::OutputVar,
leaf: impl ToBytesGadget<ConstraintF>,
) -> Result<(), SynthesisError> {
self.conditionally_check_membership(parameters, root, leaf, &Boolean::Constant(true))
}
pub fn conditionally_check_membership(
&self,
parameters: &CRHGadget::ParametersVar,
root: &CRHGadget::OutputVar,
leaf: impl ToBytesGadget<ConstraintF>,
should_enforce: &Boolean<ConstraintF>,
) -> Result<(), SynthesisError> {
) -> Result<Boolean<ConstraintF>, SynthesisError> {
assert_eq!(self.path.len(), P::HEIGHT - 1);
// Check that the hash of the given leaf matches the leaf hash in the membership
// proof.
let leaf_bits = leaf.to_bytes()?;
let leaf_hash = CRHGadget::evaluate(parameters, &leaf_bits)?;
let cs = leaf_hash
.cs()
.or(root.cs())
.or(should_enforce.cs())
.unwrap();
let cs = leaf_hash.cs().or(root.cs()).unwrap();
// Check if leaf is one of the bottom-most siblings.
let leaf_is_left = Boolean::new_witness(cs.ns("leaf_is_left"), || {
Ok(leaf_hash.value()?.eq(&self.path[0].0.value()?))
})?;
leaf_hash.conditional_enforce_equal_or(
&leaf_is_left,
&self.path[0].0,
&self.path[0].1,
should_enforce,
)?;
let mut result =
leaf_hash.is_eq(&leaf_is_left.select(&self.path[0].0, &self.path[0].1)?)?;
// Check levels between leaf level and root.
let mut previous_hash = leaf_hash;
@@ -77,12 +59,8 @@ where
"enforcing that inner hash is correct at i-th level{}",
i
));
previous_hash.conditional_enforce_equal_or(
&previous_is_left,
left_hash,
right_hash,
should_enforce,
)?;
let equality_cmp = previous_is_left.select(left_hash, right_hash)?;
result = result.and(&previous_hash.is_eq(&equality_cmp)?)?;
drop(ns);
previous_hash =
@@ -90,7 +68,7 @@ where
i += 1;
}
root.conditional_enforce_equal(&previous_hash, should_enforce)
result.and(&root.is_eq(&previous_hash)?)
}
}
@@ -235,6 +213,8 @@ mod test {
println!("constraints from path: {}", constraints_from_path);
let leaf_g: &[_] = leaf_g.as_slice();
cw.check_membership(&crh_parameters, &root, &leaf_g)
.unwrap()
.enforce_equal(&Boolean::TRUE)
.unwrap();
if !cs.is_satisfied().unwrap() {
satisfied = false;

View File

@@ -39,21 +39,11 @@ pub trait NIZKVerifierGadget<N: NIZK, ConstraintF: Field> {
verification_key: &Self::VerificationKeyVar,
input: impl IntoIterator<Item = &'a T>,
proof: &Self::ProofVar,
) -> Result<(), SynthesisError> {
Self::conditional_verify(verification_key, input, proof, &Boolean::constant(true))
}
) -> Result<Boolean<ConstraintF>, SynthesisError>;
fn conditional_verify<'a, T: 'a + ToBitsGadget<ConstraintF> + ?Sized>(
verification_key: &Self::VerificationKeyVar,
input: impl IntoIterator<Item = &'a T>,
proof: &Self::ProofVar,
condition: &Boolean<ConstraintF>,
) -> Result<(), SynthesisError>;
fn conditional_verify_prepared<'a, T: 'a + ToBitsGadget<ConstraintF> + ?Sized>(
fn verify_prepared<'a, T: 'a + ToBitsGadget<ConstraintF> + ?Sized>(
prepared_verification_key: &Self::PreparedVerificationKeyVar,
input: impl IntoIterator<Item = &'a T>,
proof: &Self::ProofVar,
condition: &Boolean<ConstraintF>,
) -> Result<(), SynthesisError>;
) -> Result<Boolean<ConstraintF>, SynthesisError>;
}

View File

@@ -176,24 +176,20 @@ where
})
}
fn conditional_verify<'a, T: 'a + ToBitsGadget<E::Fq> + ?Sized>(
fn verify<'a, T: 'a + ToBitsGadget<E::Fq> + ?Sized>(
vk: &Self::VerificationKeyVar,
input: impl IntoIterator<Item = &'a T>,
proof: &Self::ProofVar,
condition: &Boolean<E::Fq>,
) -> Result<(), SynthesisError> {
) -> Result<Boolean<E::Fq>, SynthesisError> {
let pvk = vk.prepare()?;
<Self as NIZKVerifierGadget<Gm17<E, C, V>, E::Fq>>::conditional_verify_prepared(
&pvk, input, proof, condition,
)
<Self as NIZKVerifierGadget<Gm17<E, C, V>, E::Fq>>::verify_prepared(&pvk, input, proof)
}
fn conditional_verify_prepared<'a, T: 'a + ToBitsGadget<E::Fq> + ?Sized>(
fn verify_prepared<'a, T: 'a + ToBitsGadget<E::Fq> + ?Sized>(
pvk: &Self::PreparedVerificationKeyVar,
input: impl IntoIterator<Item = &'a T>,
proof: &Self::ProofVar,
condition: &Boolean<E::Fq>,
) -> Result<(), SynthesisError> {
) -> Result<Boolean<E::Fq>, SynthesisError> {
let pvk = pvk.clone();
// e(A*G^{alpha}, B*H^{beta}) = e(G^{alpha}, H^{beta}) * e(G^{psi}, H^{gamma}) *
// e(C, H) where psi = \sum_{i=0}^l input_i pvk.query[i]
@@ -256,9 +252,7 @@ where
let test2 = P::final_exponentiation(&test2_exp)?;
let one = P::GTVar::one();
test1.conditional_enforce_equal(&one, condition)?;
test2.conditional_enforce_equal(&one, condition)?;
Ok(())
test1.is_eq(&one)?.and(&test2.is_eq(&one)?)
}
}
@@ -506,7 +500,10 @@ mod test {
&input_gadgets,
&proof_gadget,
)
.unwrap()
.enforce_equal(&Boolean::TRUE)
.unwrap();
if !cs.is_satisfied().unwrap() {
println!("=========================================================");
println!("Unsatisfied constraints:");
@@ -648,7 +645,8 @@ mod test_recursive {
&vk_gadget,
&input_gadgets,
&proof_gadget,
)?;
)?
.enforce_equal(&Boolean::TRUE)?;
Ok(())
}
}
@@ -752,6 +750,8 @@ mod test_recursive {
&input_gadgets,
&proof_gadget,
)
.unwrap()
.enforce_equal(&Boolean::TRUE)
.unwrap();
if !cs.is_satisfied().unwrap() {
println!("=========================================================");

View File

@@ -164,24 +164,20 @@ where
})
}
fn conditional_verify<'a, T: 'a + ToBitsGadget<E::Fq> + ?Sized>(
fn verify<'a, T: 'a + ToBitsGadget<E::Fq> + ?Sized>(
vk: &Self::VerificationKeyVar,
input: impl IntoIterator<Item = &'a T>,
proof: &Self::ProofVar,
condition: &Boolean<E::Fq>,
) -> Result<(), SynthesisError> {
) -> Result<Boolean<E::Fq>, SynthesisError> {
let pvk = vk.prepare()?;
<Self as NIZKVerifierGadget<Groth16<E, C, V>, E::Fq>>::conditional_verify_prepared(
&pvk, input, proof, condition,
)
<Self as NIZKVerifierGadget<Groth16<E, C, V>, E::Fq>>::verify_prepared(&pvk, input, proof)
}
fn conditional_verify_prepared<'a, T: 'a + ToBitsGadget<E::Fq> + ?Sized>(
fn verify_prepared<'a, T: 'a + ToBitsGadget<E::Fq> + ?Sized>(
pvk: &Self::PreparedVerificationKeyVar,
public_inputs: impl IntoIterator<Item = &'a T>,
proof: &Self::ProofVar,
condition: &Boolean<E::Fq>,
) -> Result<(), SynthesisError> {
) -> Result<Boolean<E::Fq>, SynthesisError> {
let pvk = pvk.clone();
let g_ic = {
@@ -216,10 +212,8 @@ where
)?
};
let test = P::final_exponentiation(&test_exp).unwrap();
test.conditional_enforce_equal(&pvk.alpha_g1_beta_g2, condition)?;
Ok(())
let test = P::final_exponentiation(&test_exp)?;
test.is_eq(&pvk.alpha_g1_beta_g2)
}
}
@@ -468,6 +462,8 @@ mod test {
&input_gadgets,
&proof_gadget,
)
.unwrap()
.enforce_equal(&Boolean::TRUE)
.unwrap();
if !cs.is_satisfied().unwrap() {
println!("=========================================================");
@@ -610,7 +606,8 @@ mod test_recursive {
&vk_gadget,
&input_gadgets,
&proof_gadget,
)?;
)?
.enforce_equal(&Boolean::TRUE)?;
Ok(())
}
}
@@ -714,6 +711,8 @@ mod test_recursive {
&input_gadgets,
&proof_gadget,
)
.unwrap()
.enforce_equal(&Boolean::TRUE)
.unwrap();
if !cs.is_satisfied().unwrap() {
println!("=========================================================");

View File

@@ -7,6 +7,7 @@ use r1cs_core::{lc, ConstraintSystemRef, LinearCombination, Namespace, Synthesis
/// Represents a variable in the constraint system which is guaranteed
/// to be either zero or one.
#[derive(Clone, Debug, Eq, PartialEq)]
#[must_use]
pub struct AllocatedBit<F: Field> {
variable: Variable,
cs: ConstraintSystemRef<F>,
@@ -216,6 +217,7 @@ impl<F: Field> CondSelectGadget<F> for AllocatedBit<F> {
/// This is a boolean value which may be either a constant or
/// an interpretation of an `AllocatedBit`.
#[derive(Clone, Debug, Eq, PartialEq)]
#[must_use]
pub enum Boolean<F: Field> {
/// Existential view of the boolean variable
Is(AllocatedBit<F>),
@@ -245,6 +247,12 @@ impl<F: Field> R1CSVar<F> for Boolean<F> {
}
impl<F: Field> Boolean<F> {
/// Returns the constrant `true`.
pub const TRUE: Self = Boolean::Constant(true);
/// Returns the constrant `false`.
pub const FALSE: Self = Boolean::Constant(false);
pub fn lc(&self) -> LinearCombination<F> {
match self {
Boolean::Constant(false) => lc!(),

View File

@@ -87,45 +87,3 @@ impl<T: EqGadget<F> + R1CSVar<F>, F: Field> EqGadget<F> for [T] {
}
}
}
pub trait OrEqualsGadget<ConstraintF: Field>
where
Self: Sized,
{
/// If `should_enforce == true`, enforce that `self` equals
/// (a) `first` (if `cond` is `true`)
/// (b) `second` (if `cond` is `false`)
fn conditional_enforce_equal_or(
&self,
cond: &Boolean<ConstraintF>,
first: &Self,
second: &Self,
should_enforce: &Boolean<ConstraintF>,
) -> Result<(), SynthesisError>;
fn enforce_equal_or(
&self,
cond: &Boolean<ConstraintF>,
first: &Self,
second: &Self,
) -> Result<(), SynthesisError> {
self.conditional_enforce_equal_or(cond, first, second, &Boolean::Constant(true))
}
}
impl<ConstraintF, T> OrEqualsGadget<ConstraintF> for T
where
ConstraintF: Field,
T: Sized + EqGadget<ConstraintF> + CondSelectGadget<ConstraintF>,
{
fn conditional_enforce_equal_or(
&self,
cond: &Boolean<ConstraintF>,
first: &Self,
second: &Self,
should_enforce: &Boolean<ConstraintF>,
) -> Result<(), SynthesisError> {
let match_opt = cond.select(first, second)?;
self.conditional_enforce_equal(&match_opt, should_enforce)
}
}