From b46d39d160a6130983bce4583d5c36565682f2ba Mon Sep 17 00:00:00 2001 From: taskooh Date: Thu, 20 Jun 2024 20:42:13 +0900 Subject: [PATCH 1/2] :white_check_mark: Add circuits test for enforce_smaller_eq_than --- Cargo.toml | 1 + examples/bin_test_marlin.rs | 1 + mpc-algebra/src/wire.rs | 3 +- src/circuits.rs | 4 +- src/circuits/enforce_smaller_or_eq_than.rs | 41 +++++++++++++++++++ src/marlin.rs | 46 +++++++++++++++++++++- 6 files changed, 92 insertions(+), 4 deletions(-) create mode 100644 src/circuits/enforce_smaller_or_eq_than.rs diff --git a/Cargo.toml b/Cargo.toml index 580bfead..ce19f194 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -46,6 +46,7 @@ zeroize = { version = "1", default-features = false, features = ["zeroize_derive mpc-algebra = { path = "mpc-algebra", version = "0.1.0" } mpc-net = { path = "mpc-net", version = "0.1.0" } mpc-trait = { path = "mpc-trait", version = "0.1.0" } +itertools = "0.13.0" [dev-dependencies] criterion = { version = "0.4", features = ["html_reports"] } diff --git a/examples/bin_test_marlin.rs b/examples/bin_test_marlin.rs index b67b1a81..c258c4fd 100644 --- a/examples/bin_test_marlin.rs +++ b/examples/bin_test_marlin.rs @@ -22,4 +22,5 @@ fn main() { marlin::mpc_test_prove_and_verify_pedersen(1); marlin::test_equality_zero(1); marlin::test_bit_decomposition(1); + marlin::test_enforce_smaller_eq_than(5); } diff --git a/mpc-algebra/src/wire.rs b/mpc-algebra/src/wire.rs index 4aa57e3f..b6eee390 100644 --- a/mpc-algebra/src/wire.rs +++ b/mpc-algebra/src/wire.rs @@ -1,5 +1,6 @@ -pub mod field; pub mod boolean_field; +pub mod field; +pub use boolean_field::*; pub use field::*; pub mod group; pub use group::*; diff --git a/src/circuits.rs b/src/circuits.rs index 2ee9c3fe..bbb62393 100644 --- a/src/circuits.rs +++ b/src/circuits.rs @@ -4,6 +4,6 @@ pub mod pedersen; pub use pedersen::*; pub mod werewolf; pub use werewolf::*; -pub mod equality_zero; - pub mod bit_decomposition; +pub mod enforce_smaller_or_eq_than; +pub mod equality_zero; diff --git a/src/circuits/enforce_smaller_or_eq_than.rs b/src/circuits/enforce_smaller_or_eq_than.rs new file mode 100644 index 00000000..406bacc2 --- /dev/null +++ b/src/circuits/enforce_smaller_or_eq_than.rs @@ -0,0 +1,41 @@ +use ark_ff::One; +use ark_ff::PrimeField; +use ark_r1cs_std::{alloc::AllocVar, boolean::Boolean}; +use ark_relations::r1cs::{ConstraintSynthesizer, ConstraintSystemRef, SynthesisError}; +use mpc_algebra::{malicious_majority::MpcField, MpcBoolean}; + +type Fr = ark_bls12_377::Fr; +type MFr = MpcField; + +pub struct SmallerEqThanCircuit { + pub a: Vec, + // instance + pub b: Fr, +} + +impl ConstraintSynthesizer for SmallerEqThanCircuit { + fn generate_constraints(self, cs: ConstraintSystemRef) -> Result<(), SynthesisError> { + // let a_var = MpcFpVar::new_witness(cs.clone(), || Ok(self.a))?; + let a_var = self + .a + .iter() + .map(|x| MpcBoolean::new_witness(cs.clone(), || Ok(x)).unwrap()) + .collect::>(); + + let _ = MpcBoolean::enforce_smaller_or_equal_than_le(&a_var, self.b.into_repr()).unwrap(); + Ok(()) + } +} + +impl ConstraintSynthesizer for SmallerEqThanCircuit { + fn generate_constraints(self, cs: ConstraintSystemRef) -> Result<(), SynthesisError> { + let a_var = self + .a + .iter() + .map(|x| Boolean::new_witness(cs.clone(), || Ok(x.is_one())).unwrap()) + .collect::>(); + + let _ = Boolean::enforce_smaller_or_equal_than_le(&a_var, self.b.into_repr()).unwrap(); + Ok(()) + } +} diff --git a/src/marlin.rs b/src/marlin.rs index 427d9dbe..4f521f4d 100644 --- a/src/marlin.rs +++ b/src/marlin.rs @@ -8,13 +8,17 @@ use ark_relations::r1cs::ConstraintSynthesizer; use ark_std::{end_timer, start_timer, test_rng, PubUniformRand, UniformRand}; use blake2::Blake2s; +use itertools::Itertools; // use mpc_algebra::honest_but_curious::*; -use mpc_algebra::malicious_majority::*; +use mpc_algebra::{ + malicious_majority::*, BooleanWire, MpcBooleanField, SpdzFieldShare, UniformBitRand, +}; use mpc_algebra::{FromLocal, Reveal}; use mpc_net::{MpcMultiNet, MpcNet}; use ark_std::{One, Zero}; +use crate::circuits::enforce_smaller_or_eq_than::SmallerEqThanCircuit; use crate::{ circuits::{ bit_decomposition::BitDecompositionCircuit, circuit::MyCircuit, @@ -300,6 +304,7 @@ pub fn test_bit_decomposition(n_iters: usize) { for _ in 0..n_iters { let mpc_circuit = BitDecompositionCircuit { a: MFr::rand(rng) }; + // TODO assert!(prove_and_verify( &mpc_index_pk, &index_vk, @@ -308,3 +313,42 @@ pub fn test_bit_decomposition(n_iters: usize) { )); } } + +// Test +pub fn test_enforce_smaller_eq_than(n_iters: usize) { + let rng = &mut test_rng(); + + for _ in 0..n_iters { + let (local_a_bit_rand, _) = + MpcBooleanField::>::rand_number_bitwise(rng); + let local_a_bit_rand = local_a_bit_rand.iter().map(|x| x.reveal()).collect_vec(); + let b = Fr::rand(rng); + + let local_circuit = SmallerEqThanCircuit { + a: local_a_bit_rand, + b, + }; + let (mpc_index_pk, index_vk) = setup_and_index(local_circuit); + // generate random shared bits + let (a_bit_rand, a_rand) = + MpcBooleanField::>::rand_number_bitwise(rng); + let a_bit_rand = a_bit_rand.into_iter().map(|x| x.field()).collect_vec(); + let mpc_circuit = SmallerEqThanCircuit { a: a_bit_rand, b }; + let inputs = vec![]; + if a_rand.reveal() <= b { + assert!(prove_and_verify( + &mpc_index_pk, + &index_vk, + mpc_circuit, + inputs + )); + } else { + assert!(!prove_and_verify( + &mpc_index_pk, + &index_vk, + mpc_circuit, + inputs + )); + } + } +} From 851c825cc7c28d4f873a27f2558351dc5fb37ea0 Mon Sep 17 00:00:00 2001 From: taskooh Date: Thu, 27 Jun 2024 20:28:55 +0900 Subject: [PATCH 2/2] :bulb: Remove resolved todo comment --- src/marlin.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/src/marlin.rs b/src/marlin.rs index 4f521f4d..c8e5a83a 100644 --- a/src/marlin.rs +++ b/src/marlin.rs @@ -304,7 +304,6 @@ pub fn test_bit_decomposition(n_iters: usize) { for _ in 0..n_iters { let mpc_circuit = BitDecompositionCircuit { a: MFr::rand(rng) }; - // TODO assert!(prove_and_verify( &mpc_index_pk, &index_vk,