LEM eval completed #617

gabriel-barrett · 2023-08-16T22:44:17Z

This PR implements the rest of the Lurk step function in LEM

src/circuit/gadgets/constraints.rs

porcuquine · 2023-08-17T00:25:18Z

src/circuit/gadgets/constraints.rs

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


Because this logic is tricky and we already abstract it elsewhere for that purpose, I think it would be better to isolate implementation there. Concretely, I think you can use enforce_implication_lc_zero(diff) here.

We will also eventually want an allocating version of this (allocating a bit) so we can do erroring type checks. It doesn't have to happen now, but in the interest of thinking about how we want to normalize decomposition of these gadgets, I would suggest that this has an is_pack (maybe there is a better name) part, which is a predicate that returns a linear combination.

Then from that we can create an allocated predicated, an 'implies' function, and an 'enforce' function. Then we could just define our predicates and derive the rest with a proc macro (or more manually, but in a transparent procedural way).

porcuquine · 2023-08-17T00:29:24Z

src/circuit/gadgets/constraints.rs

+        let alloc_num = AllocatedNum::alloc(&mut cs.namespace(|| "num"), || {
+            Ok(Fr::from_str_vartime("42").unwrap())
+        })
+        .unwrap();


Even if not a full-on proptest, I would love to see this test made at least a little more convincing. For example, can we call it on 0, 1, and the largest U64?

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

thanks, just added it

porcuquine · 2023-08-17T00:31:15Z

src/circuit/gadgets/constraints.rs

+        let mut cs = TestConstraintSystem::<Fr>::new();
+
+        let alloc_num = AllocatedNum::alloc(&mut cs.namespace(|| "num"), || {
+            Ok(Fr::from_str_vartime("18446744073709551616").unwrap())


Can we also at least test this on 2^64?

added a comment to make this edge case clear

porcuquine · 2023-08-18T16:49:03Z

src/lem/circuit.rs

+                        let b = u64::wrapping_sub(u64::wrapping_pow(2, *n), 1);
+                        let a = bound_allocations.get(a)?;
+                        let a_bits = a
+                            .hash()
+                            .to_bits_le_strict(&mut cs.namespace(|| "bitwise_and"))?;
+                        let mut trunc_bits = Vec::with_capacity(64);
+                        let mut b_rest = b;
+                        for a_bit in a_bits {
+                            let b_bit = b_rest & 1;
+                            if b_bit == 1 {
+                                trunc_bits.push(a_bit.clone());
+                            } else {
+                                trunc_bits.push(Boolean::Constant(false))
+                            }
+                            b_rest >>= 1;
+                        }


Considering the goal is truncation, and the reason to switch to that (from bitwise-and) was simplicity and less room for error in providing unneeded generality, I don't think using a bitwise-and operation under the hood as the implementation technique is ideal.

I think instead you should just do the obvious simple thing, which is just take the least significant n bits from a_bits. I think both b and any concept of bitwise-and just add noise and don't need to appear in the source at all.

If you need to have this be a constant sized/shaped circuit, regardless of n (which I understand), you can still pad with Boolean::Constant(false).

porcuquine · 2023-08-18T16:50:16Z

src/lem/circuit.rs

+                                .hash()
+                                .get_value()
+                                .map(|a| F::from_u64(a.to_u64_unchecked() & b))
+                                .unwrap();


I think this unwrap() is going to cause a problem when you're trying to synthesize the shape and don't have any value for a — but still need to construct constraints that will work for any a that may be supplied when generating a witness.

huitseeker

General impression: I'd love more testing, both on the gadgets, and on the larger lem invariants.

huitseeker · 2023-08-17T20:38:05Z

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> {


Just impl TryFrom<LurkField> for u128 should be more idiomatic.

This is following the pattern in the rest of the code. If anything, we can create an issue to rewrite all the functions at once

src/circuit/gadgets/constraints.rs

huitseeker · 2023-08-18T16:43:27Z

src/circuit/gadgets/constraints.rs

@@ -1282,4 +1319,32 @@ mod tests {

        assert!(cs.is_satisfied());
    }
+
+    #[test]
+    fn test_enforce_u64() {


This should be renamed to match what it's testing.

huitseeker · 2023-08-18T16:48:57Z

src/circuit/gadgets/constraints.rs

+        let alloc_num = AllocatedNum::alloc(&mut cs.namespace(|| "num"), || {
+            Ok(Fr::from_str_vartime("42").unwrap())
+        })
+        .unwrap();


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

huitseeker · 2023-08-18T16:56:03Z

src/lem/eval.rs

        let t = Symbol("t");
+        let zero = Num(0);
+        let size_u64 = Num(18446744073709551616);


the "at compile time" meaning may be overloaded, but inline_const is due to be stabilized soon™, which may help write u64::pow(2, 64) here.

src/lem/interpreter.rs

src/lem/mod.rs

porcuquine

Approved based on general characteristics of the language defined and circuit generated. Pending @huitseeker' approval.

This is not a complete review of either LEM or the circuit, but it's enough to merge this work.

huitseeker

Please add a docstring on implies_u64 such that reading it allows one to understand the difference with {implies, enforce}_pack.

src/circuit/gadgets/constraints.rs

huitseeker · 2023-08-18T20:43:40Z

src/lem/circuit.rs

+                        implies_u64(cs.namespace(|| "rem_u64"), not_dummy, &rem)?;
+                        implies_u64(cs.namespace(|| "diff_u64"), not_dummy, &diff)?;
+
+                        linear(cs, || "linear", b, &div, &rem, a);


I don't see that rename

huitseeker

This is great! thanks, all!

emmorais and others added 19 commits August 9, 2023 15:19

Implement div

821bec9

add Op::Lt

e77fd3d

Merge branch 'lem-lt' into lem_div

60df119

fix Op::Div parameters

c810654

Progress on u64

1eba1f3

Op::Lt finished

4f7915a

slot allocation for is_diff_neg

9f707aa

slot allocation for hide/open

3aee9fa

Implement enforce_u64

29fc20f

enforce_u64 -> implies_u64

110f719

Fixed implies_u64

184b13e

Progress on eval

6a01555

Added equality operator

f1f9bda

Fixed div namespace issue

6148c7f

rename debug display function

130c0df

Add and Sub for u64 finished

6eecd56

Fixed tests

d574786

More progress on eval

2e71c28

Eval finished!

e518043

gabriel-barrett requested review from a team as code owners August 16, 2023 22:44

gabriel-barrett and others added 4 commits August 16, 2023 20:03

div_rem fixed

310f1eb

solve conflicts

8868d12

fix nil instantiation in the step function

b1f8584

slight code improvements

7d6fe20

porcuquine reviewed Aug 17, 2023

View reviewed changes

src/circuit/gadgets/constraints.rs Outdated Show resolved Hide resolved

porcuquine reviewed Aug 17, 2023

View reviewed changes

porcuquine reviewed Aug 18, 2023

View reviewed changes

huitseeker reviewed Aug 18, 2023

View reviewed changes

gabriel-barrett and others added 4 commits August 18, 2023 14:47

Simplified Trunc

b9c6063

Added assertions around Trunc

53334d4

Include implie_u64 proptest

6f9d828

Rename unit tests

09a39fa

porcuquine previously approved these changes Aug 18, 2023

View reviewed changes

gabriel-barrett dismissed porcuquine’s stale review via 09a39fa August 18, 2023 20:31

arthurpaulino added 3 commits August 18, 2023 17:33

solve conflicts

b98904b

Merge branch 'lem_div' of github.com:lurk-lab/lurk-rs into lem_div

30a08e4

remove cargo lock

08dd708

huitseeker reviewed Aug 18, 2023

View reviewed changes

emmorais and others added 10 commits August 18, 2023 17:59

Rename linear to enforce_product_and_sum

ef37caa

code suggestions

6ca0102

Merge branch 'lem_div' of github.com:lurk-lab/lurk-rs into lem_div

660bd7a

Fmt

e0d2f81

fmt

c075c45

Merge branch 'lem_div' of github.com:lurk-lab/lurk-rs into lem_div

457c5b6

inline always -> inline

4a6fb1e

Add docstring to implies_u64

99f16c3

Review docstrings

fd984ff

Remove obsolete test

7a5a7d3

arthurpaulino requested a review from huitseeker August 18, 2023 22:16

porcuquine approved these changes Aug 19, 2023

View reviewed changes

porcuquine added this pull request to the merge queue Aug 19, 2023

huitseeker approved these changes Aug 19, 2023

View reviewed changes

Merged via the queue into master with commit 58105dc Aug 19, 2023
6 checks passed

porcuquine deleted the lem_div branch August 19, 2023 02:31

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

LEM eval completed #617

LEM eval completed #617

gabriel-barrett commented Aug 16, 2023

porcuquine Aug 17, 2023

porcuquine Aug 17, 2023

porcuquine Aug 17, 2023

huitseeker Aug 18, 2023

emmorais Aug 18, 2023

porcuquine Aug 17, 2023

emmorais Aug 18, 2023

porcuquine Aug 18, 2023

porcuquine Aug 18, 2023

porcuquine Aug 18, 2023

huitseeker left a comment

huitseeker Aug 17, 2023

arthurpaulino Aug 18, 2023

huitseeker Aug 18, 2023

huitseeker Aug 18, 2023

huitseeker Aug 18, 2023

porcuquine left a comment

huitseeker left a comment

huitseeker Aug 18, 2023

huitseeker left a comment

LEM eval completed #617

LEM eval completed #617

Conversation

gabriel-barrett commented Aug 16, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

huitseeker left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

porcuquine left a comment

Choose a reason for hiding this comment

huitseeker left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

huitseeker left a comment

Choose a reason for hiding this comment