LEM eval completed

src/circuit/gadgets/constraints.rs

@@ -152,30 +152,67 @@ pub(crate) fn add_to_lc<F: PrimeField, CS: ConstraintSystem<F>>(
     Ok(v_lc)
 }
 
-// Enforce v is the bit decomposition of num, therefore we have that 0 <= num < 2ˆ(sizeof(v)).
-pub(crate) fn enforce_pack<F: LurkField, CS: ConstraintSystem<F>>(
+pub(crate) fn implies_u64<F: LurkField, CS: ConstraintSystem<F>>(
+    mut cs: CS,
+    premise: &Boolean,
+    a: &AllocatedNum<F>,
+) -> Result<(), SynthesisError> {
+    let mut a_u64 = a.get_value().and_then(|a| a.to_u64()).unwrap_or(0);
+
+    let mut bits: Vec<Boolean> = Vec::with_capacity(64);
+    for i in 0..64 {
+        let b = a_u64 & 1;
+        let b_bool = Boolean::Is(AllocatedBit::alloc(
+            &mut cs.namespace(|| format!("b.{i}")),
+            Some(b == 1),
+        )?);
+        bits.push(b_bool);
+
+        a_u64 /= 2;
+    }
+
+    // premise -> a = sum(bits)
+    implies_pack(
+        &mut cs.namespace(|| "u64 bit decomposition check"),
+        premise,
+        &bits,
+        a,
+    )?;
+
+    Ok(())
+}
+
+// If premise is true, enforce v is the bit decomposition of num, therefore we have that 0 <= num < 2ˆ(sizeof(v)).
+pub(crate) fn implies_pack<F: LurkField, CS: ConstraintSystem<F>>(
     mut cs: CS,
+    premise: &Boolean,
     v: &[Boolean],
     num: &AllocatedNum<F>,
 ) -> Result<(), SynthesisError> {
     let mut coeff = F::ONE;
-
-    let mut v_lc = LinearCombination::<F>::zero();
+    let mut pack = LinearCombination::<F>::zero();
     for b in v {
-        v_lc = add_to_lc::<F, CS>(b, v_lc, coeff)?;
+        pack = add_to_lc::<F, CS>(b, pack, coeff)?;
         coeff = coeff.double();
     }
+    let diff = |_| pack - num.get_variable();
+    let premise_lc = |_| premise.lc(CS::one(), F::ONE);
+    let zero = |lc| lc;
 
-    cs.enforce(
-        || "pack",
-        |_| v_lc,
-        |lc| lc + CS::one(),
-        |lc| lc + num.get_variable(),
-    );
+    cs.enforce(|| "pack", diff, premise_lc, zero);
 
     Ok(())
 }
 
+// Enforce v is the bit decomposition of num, therefore we have that 0 <= num < 2ˆ(sizeof(v)).
+pub(crate) fn enforce_pack<F: LurkField, CS: ConstraintSystem<F>>(
+    cs: CS,
+    v: &[Boolean],
+    num: &AllocatedNum<F>,
+) -> Result<(), SynthesisError> {
+    implies_pack(cs, &Boolean::Constant(true), v, num)
+}
+
 /// Adds a constraint to CS, enforcing a difference relationship between the allocated numbers a, b, and difference.
 ///
 /// a - b = difference
@@ -1282,4 +1319,48 @@ mod tests {
 
         assert!(cs.is_satisfied());
     }
+
+    #[test]
+    fn test_enforce_u64() {
+        let mut cs = TestConstraintSystem::<Fr>::new();
+
+        let alloc_num = AllocatedNum::alloc(&mut cs.namespace(|| "num"), || {
+            Ok(Fr::from_str_vartime("42").unwrap())
+        })
+        .unwrap();
+
+        let t = Boolean::Constant(true);
+        implies_u64(&mut cs.namespace(|| "enforce u64"), &t, &alloc_num).unwrap();
+        assert!(cs.is_satisfied());
+    }
+
+    #[test]
+    fn test_enforce_u64_negative() {
+        let mut cs = TestConstraintSystem::<Fr>::new();
+
+        let alloc_num = AllocatedNum::alloc(&mut cs.namespace(|| "num"), || {
+            Ok(Fr::from_str_vartime("18446744073709551616").unwrap())
+        })
+        .unwrap();
+
+        let t = Boolean::Constant(true);
+        implies_u64(&mut cs.namespace(|| "enforce u64"), &t, &alloc_num).unwrap();
+        assert!(!cs.is_satisfied());
+    }
+
+    proptest!{
+        #[test]
+        fn test_implies_u64(f in any::<FWrap<Fr>>()) {
+            let mut cs = TestConstraintSystem::<Fr>::new();
+
+            let num = AllocatedNum::alloc(cs.namespace(|| "num"), || Ok(f.0)).unwrap();
+
+            let t = Boolean::Constant(true);
+            implies_u64(&mut cs.namespace(|| "enforce u64"), &t, &num).unwrap();
+
+            let f_u64_roundtrip: Fr = f.0.to_u64_unchecked().into();
+            let was_u64 = f_u64_roundtrip == f.0;
+            prop_assert_eq!(was_u64, cs.is_satisfied());
+        }
+    }
 }

src/field.rs

@@ -141,6 +141,18 @@ pub trait LurkField: PrimeField + PrimeFieldBits {
         Some(u64::from_le_bytes(byte_array))
     }
 
+    /// Attempts to convert the field element to a u64
+    fn to_u128(&self) -> Option<u128> {
+        for x in &self.to_repr().as_ref()[16..] {
+            if *x != 0 {
+                return None;
+            }
+        }
+        let mut byte_array = [0u8; 16];
+        byte_array.copy_from_slice(&self.to_repr().as_ref()[0..16]);
+        Some(u128::from_le_bytes(byte_array))
+    }
+
     /// Converts the first 4 bytes of the field element to a u32
     fn to_u32_unchecked(&self) -> u32 {
         let mut byte_array = [0u8; 4];
@@ -155,6 +167,13 @@ pub trait LurkField: PrimeField + PrimeFieldBits {
         u64::from_le_bytes(byte_array)
     }
 
+    /// Converts the first 16 bytes of the field element to a u128
+    fn to_u128_unchecked(&self) -> u128 {
+        let mut byte_array = [0u8; 16];
+        byte_array.copy_from_slice(&self.to_repr().as_ref()[0..16]);
+        u128::from_le_bytes(byte_array)
+    }
+
     /// Constructs a field element from a u64
     fn from_u64(x: u64) -> Self {
         x.into()