From f1f9bdae6465430353d6757f81239ecbcee64a35 Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Tue, 15 Aug 2023 22:04:54 -0300 Subject: [PATCH] Added equality operator --- src/lem/circuit.rs | 37 ++++++++++++++++++++++++++++++------- src/lem/eval.rs | 18 ++++++++++++------ src/lem/interpreter.rs | 24 ++++++++++++++++++++++++ src/lem/macros.rs | 34 ++++++++++++++++++++++++++++++++++ src/lem/mod.rs | 22 ++++++++++++++++++++-- 5 files changed, 120 insertions(+), 15 deletions(-) diff --git a/src/lem/circuit.rs b/src/lem/circuit.rs index 438160f60c..5b7d5c177f 100644 --- a/src/lem/circuit.rs +++ b/src/lem/circuit.rs @@ -585,10 +585,35 @@ impl Func { let allocated_ptr = AllocatedPtr::from_parts(tag, src.hash().clone()); bound_allocations.insert(tgt.clone(), allocated_ptr); } + Op::EqTag(tgt, a, b) => { + let a = bound_allocations.get(a)?; + let b = bound_allocations.get(b)?; + let a_num = a.tag(); + let b_num = b.tag(); + let eq = alloc_equal(&mut cs.namespace(|| "equal_tag"), a_num, b_num)?; + let c_num = boolean_to_num(&mut cs.namespace(|| "equal_tag.to_num"), &eq)?; + let tag = g + .global_allocator + .get_or_alloc_const(cs, Tag::Expr(Num).to_field())?; + let c = AllocatedPtr::from_parts(tag, c_num); + bound_allocations.insert(tgt.clone(), c); + } + Op::EqVal(tgt, a, b) => { + let a = bound_allocations.get(a)?; + let b = bound_allocations.get(b)?; + let a_num = a.hash(); + let b_num = b.hash(); + let eq = alloc_equal(&mut cs.namespace(|| "equal_val"), a_num, b_num)?; + let c_num = boolean_to_num(&mut cs.namespace(|| "equal_val.to_num"), &eq)?; + let tag = g + .global_allocator + .get_or_alloc_const(cs, Tag::Expr(Num).to_field())?; + let c = AllocatedPtr::from_parts(tag, c_num); + bound_allocations.insert(tgt.clone(), c); + } Op::Add(tgt, a, b) => { let a = bound_allocations.get(a)?; let b = bound_allocations.get(b)?; - // TODO check that the tags are correct let a_num = a.hash(); let b_num = b.hash(); let c_num = add(&mut cs.namespace(|| "add"), a_num, b_num)?; @@ -601,7 +626,6 @@ impl Func { Op::Sub(tgt, a, b) => { let a = bound_allocations.get(a)?; let b = bound_allocations.get(b)?; - // TODO check that the tags are correct let a_num = a.hash(); let b_num = b.hash(); let c_num = sub(&mut cs.namespace(|| "sub"), a_num, b_num)?; @@ -614,7 +638,6 @@ impl Func { Op::Mul(tgt, a, b) => { let a = bound_allocations.get(a)?; let b = bound_allocations.get(b)?; - // TODO check that the tags are correct let a_num = a.hash(); let b_num = b.hash(); let c_num = mul(&mut cs.namespace(|| "mul"), a_num, b_num)?; @@ -627,7 +650,6 @@ impl Func { Op::Div(tgt, a, b) => { let a = bound_allocations.get(a)?; let b = bound_allocations.get(b)?; - // TODO check that the tags are correct let a_num = a.hash(); let b_num = b.hash(); @@ -652,7 +674,6 @@ impl Func { Op::Lt(tgt, a, b) => { let a = bound_allocations.get(a)?; let b = bound_allocations.get(b)?; - // TODO check that the tags are correct let tag = g .global_allocator .get_or_alloc_const(cs, Tag::Expr(Num).to_field())?; @@ -782,10 +803,8 @@ impl Func { Ctrl::IfEq(x, y, eq_block, else_block) => { let x = bound_allocations.get(x)?.hash(); let y = bound_allocations.get(y)?.hash(); - // TODO should we check whether the tags are equal too? let eq = alloc_equal(&mut cs.namespace(|| "if_eq.alloc_equal"), x, y)?; let not_eq = eq.not(); - // TODO is this the most efficient way of doing if statements? let not_dummy_and_eq = and(&mut cs.namespace(|| "if_eq.and"), not_dummy, &eq)?; let not_dummy_and_not_eq = and(&mut cs.namespace(|| "if_eq.and.2"), not_dummy, ¬_eq)?; @@ -1027,6 +1046,10 @@ impl Func { Op::Cast(_tgt, tag, _src) => { globals.insert(FWrap(tag.to_field())); } + Op::EqTag(_, _, _) | Op::EqVal(_, _, _) => { + globals.insert(FWrap(Tag::Expr(Num).to_field())); + num_constraints += 5; + } Op::Add(_, _, _) | Op::Sub(_, _, _) | Op::Mul(_, _, _) => { globals.insert(FWrap(Tag::Expr(Num).to_field())); num_constraints += 1; diff --git a/src/lem/eval.rs b/src/lem/eval.rs index 3c0ba02b00..d9cd0f62f8 100644 --- a/src/lem/eval.rs +++ b/src/lem/eval.rs @@ -725,11 +725,17 @@ fn apply_cont() -> Func { return(hidden, env, continuation, makethunk) } Symbol("eq") => { - // TODO should we check whether the tags are also equal? - if evaled_arg == result { - return (t, env, continuation, makethunk) + let eq_tag = eq_tag(evaled_arg, result); + let eq_val = eq_val(evaled_arg, result); + let eq = mul(eq_tag, eq_val); + match eq.val { + Num(0) => { + return (nil, env, continuation, makethunk) + } + Num(1) => { + return (t, env, continuation, makethunk) + } } - return (nil, env, continuation, makethunk) } Symbol("+") => { match args_num_type.val { @@ -924,8 +930,8 @@ mod tests { use blstrs::Scalar as Fr; const NUM_INPUTS: usize = 1; - const NUM_AUX: usize = 8781; - const NUM_CONSTRAINTS: usize = 10875; + const NUM_AUX: usize = 8868; + const NUM_CONSTRAINTS: usize = 11096; const NUM_SLOTS: SlotsCounter = SlotsCounter { hash2: 16, hash3: 4, diff --git a/src/lem/interpreter.rs b/src/lem/interpreter.rs index 52641a6263..cfff4d2ced 100644 --- a/src/lem/interpreter.rs +++ b/src/lem/interpreter.rs @@ -111,6 +111,30 @@ impl Block { let tgt_ptr = src_ptr.cast(*tag); bindings.insert(tgt.clone(), tgt_ptr); } + Op::EqTag(tgt, a, b) => { + let a = bindings.get(a)?; + let b = bindings.get(b)?; + let c = if a.tag() == b.tag() { + Ptr::Leaf(Tag::Expr(Num), F::ONE) + } else { + Ptr::Leaf(Tag::Expr(Num), F::ZERO) + }; + bindings.insert(tgt.clone(), c); + } + Op::EqVal(tgt, a, b) => { + let a = bindings.get(a)?; + let b = bindings.get(b)?; + // In order to compare Ptrs, we *must* resolve the hashes. Otherwise, we risk failing to recognize equality of + // compound data with opaque data in either element's transitive closure. + let a_hash = store.hash_ptr(a)?.hash; + let b_hash = store.hash_ptr(b)?.hash; + let c = if a_hash == b_hash { + Ptr::Leaf(Tag::Expr(Num), F::ONE) + } else { + Ptr::Leaf(Tag::Expr(Num), F::ZERO) + }; + bindings.insert(tgt.clone(), c); + } Op::Add(tgt, a, b) => { let a = bindings.get(a)?; let b = bindings.get(b)?; diff --git a/src/lem/macros.rs b/src/lem/macros.rs index a691b381af..977fdfe600 100644 --- a/src/lem/macros.rs +++ b/src/lem/macros.rs @@ -58,6 +58,20 @@ macro_rules! op { $crate::var!($src), ) }; + ( let $tgt:ident = eq_tag($a:ident, $b:ident) ) => { + $crate::lem::Op::EqTag( + $crate::var!($tgt), + $crate::var!($a), + $crate::var!($b), + ) + }; + ( let $tgt:ident = eq_val($a:ident, $b:ident) ) => { + $crate::lem::Op::EqVal( + $crate::var!($tgt), + $crate::var!($a), + $crate::var!($b), + ) + }; ( let $tgt:ident = add($a:ident, $b:ident) ) => { $crate::lem::Op::Add( $crate::var!($tgt), @@ -250,6 +264,26 @@ macro_rules! block { $($tail)* ) }; + (@seq {$($limbs:expr)*}, let $tgt:ident = eq_tag($a:ident, $b:ident) ; $($tail:tt)*) => { + $crate::block! ( + @seq + { + $($limbs)* + $crate::op!(let $tgt = eq_tag($a, $b)) + }, + $($tail)* + ) + }; + (@seq {$($limbs:expr)*}, let $tgt:ident = eq_val($a:ident, $b:ident) ; $($tail:tt)*) => { + $crate::block! ( + @seq + { + $($limbs)* + $crate::op!(let $tgt = eq_val($a, $b)) + }, + $($tail)* + ) + }; (@seq {$($limbs:expr)*}, let $tgt:ident = add($a:ident, $b:ident) ; $($tail:tt)*) => { $crate::block! ( @seq diff --git a/src/lem/mod.rs b/src/lem/mod.rs index 41ea92320c..230c99258a 100644 --- a/src/lem/mod.rs +++ b/src/lem/mod.rs @@ -238,6 +238,10 @@ pub enum Op { /// `Cast(y, t, x)` binds `y` to a pointer with tag `t` and the hash of `x` Cast(Var, Tag, Var), /// `Add(y, a, b)` binds `y` to the sum of `a` and `b` + EqTag(Var, Var, Var), + /// `EqVal(y, a, b)` binds `y` to `1` if `a.val != b.val`, or to `0` otherwise + EqVal(Var, Var, Var), + /// `Lt(y, a, b)` binds `y` to `1` if `a < b`, or to `0` otherwise Add(Var, Var, Var), /// `Sub(y, a, b)` binds `y` to the sum of `a` and `b` Sub(Var, Var, Var), @@ -245,7 +249,7 @@ pub enum Op { Mul(Var, Var, Var), /// `Div(y, a, b)` binds `y` to the sum of `a` and `b` Div(Var, Var, Var), - /// `Lt(y, a, b)` binds `y` to `t` if `a < b`, or to `nil` otherwise + /// `Lt(y, a, b)` binds `y` to `1` if `a < b`, or to `0` otherwise Lt(Var, Var, Var), /// `Emit(v)` simply prints out the value of `v` when interpreting the code Emit(Var), @@ -342,7 +346,9 @@ impl Func { is_bound(src, map)?; is_unique(tgt, map); } - Op::Add(tgt, a, b) + Op::EqTag(tgt, a, b) + | Op::EqVal(tgt, a, b) + | Op::Add(tgt, a, b) | Op::Sub(tgt, a, b) | Op::Mul(tgt, a, b) | Op::Div(tgt, a, b) @@ -554,6 +560,18 @@ impl Block { let tgt = insert_one(map, uniq, &tgt); ops.push(Op::Cast(tgt, tag, src)) } + Op::EqTag(tgt, a, b) => { + let a = map.get_cloned(&a)?; + let b = map.get_cloned(&b)?; + let tgt = insert_one(map, uniq, &tgt); + ops.push(Op::EqTag(tgt, a, b)) + } + Op::EqVal(tgt, a, b) => { + let a = map.get_cloned(&a)?; + let b = map.get_cloned(&b)?; + let tgt = insert_one(map, uniq, &tgt); + ops.push(Op::EqVal(tgt, a, b)) + } Op::Add(tgt, a, b) => { let a = map.get_cloned(&a)?; let b = map.get_cloned(&b)?;