✅ Add circuits test for enforce_smaller_eq_than

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"] }

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);
 }

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::*;

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;

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<Fr>;
+
+pub struct SmallerEqThanCircuit<F: PrimeField> {
+    pub a: Vec<F>,
+    // instance
+    pub b: Fr,
+}
+
+impl ConstraintSynthesizer<MFr> for SmallerEqThanCircuit<MFr> {
+    fn generate_constraints(self, cs: ConstraintSystemRef<MFr>) -> 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::<Vec<_>>();
+
+        let _ = MpcBoolean::enforce_smaller_or_equal_than_le(&a_var, self.b.into_repr()).unwrap();
+        Ok(())
+    }
+}
+
+impl ConstraintSynthesizer<Fr> for SmallerEqThanCircuit<Fr> {
+    fn generate_constraints(self, cs: ConstraintSystemRef<Fr>) -> Result<(), SynthesisError> {
+        let a_var = self
+            .a
+            .iter()
+            .map(|x| Boolean::new_witness(cs.clone(), || Ok(x.is_one())).unwrap())
+            .collect::<Vec<_>>();
+
+        let _ = Boolean::enforce_smaller_or_equal_than_le(&a_var, self.b.into_repr()).unwrap();
+        Ok(())
+    }
+}

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,
@@ -308,3 +312,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::<Fr, SpdzFieldShare<Fr>>::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::<Fr, SpdzFieldShare<Fr>>::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
+            ));
+        }
+    }
+}