chore: implement Gt and GtEq as syntactic sugar (#216)

* Implement Gt and GtEq as syntactic sugar

* Update src/backends/plonky2/circuits/mainpod.rs

Co-authored-by: Eduard S. <eduardsanou@posteo.net>

* Op verification circuit refactor

* Code review

* Add range check to Eq case of LtEq

* Style

* Factor out ValueOf statement argument type checks

* Formatting

* Clean-up

* Safety

* Take sign into account

* Simplify sign check

---------

Co-authored-by: Eduard S. <eduardsanou@posteo.net>

src/backends/plonky2/circuits/common.rs

@@ -30,6 +30,7 @@ use crate::{
 };
 
 pub const CODE_SIZE: usize = HASH_SIZE + 2;
+const NUM_BITS: usize = 32;
 
 #[derive(Copy, Clone)]
 pub struct ValueTarget {
@@ -102,6 +103,13 @@ impl StatementArgTarget {
     ) -> Self {
         Self::new(*pod_id, *key)
     }
+
+    /// StatementArgTarget to ValueTarget coercion. Make sure to check
+    /// that the arg is a value using the `statement_arg_is_value` method
+    /// first!
+    pub fn as_value(&self) -> ValueTarget {
+        ValueTarget::from_slice(&self.elements[..VALUE_SIZE])
+    }
 }
 
 #[derive(Clone)]
@@ -300,9 +308,17 @@ pub trait CircuitBuilderPod<F: RichField + Extendable<D>, const D: usize> {
     // Convenience methods for checking values.
     /// Checks whether `xs` is right-padded with 0s so as to represent a `Value`.
     fn statement_arg_is_value(&mut self, arg: &StatementArgTarget) -> BoolTarget;
-    /// Checks whether `x < y` if `b` is true. This involves checking
+
-    /// that `x` and `y` each consist of two `u32` limbs.
+    /// Checks whether `x` is an i64, which involves checking that it
-    fn assert_less_if(&mut self, b: BoolTarget, x: ValueTarget, y: ValueTarget);
+    /// consists of two `u32` limbs.
+    fn assert_i64(&mut self, x: ValueTarget);
+
+    /// Checks whether an i64 is negative.
+    fn i64_is_negative(&mut self, x: ValueTarget) -> BoolTarget;
+
+    /// Checks whether `x < y` if `b` is true. This assumes that `x`
+    /// and `y` each consist of two `u32` limbs.
+    fn assert_i64_less_if(&mut self, b: BoolTarget, x: ValueTarget, y: ValueTarget);
 
     // Convenience methods for accessing and connecting elements of
     // (vectors of) flattenables.
@@ -389,14 +405,34 @@ impl CircuitBuilderPod<F, D> for CircuitBuilder<F, D> {
         self.is_equal_slice(&arg.elements[VALUE_SIZE..], &zeros)
     }
 
-    fn assert_less_if(&mut self, b: BoolTarget, x: ValueTarget, y: ValueTarget) {
+    fn assert_i64(&mut self, x: ValueTarget) {
-        const NUM_BITS: usize = 32;
+        // `x` should only have two limbs.
+        x.elements
+            .into_iter()
+            .skip(2)
+            .for_each(|l| self.assert_zero(l));
 
-        // Lt assertion with 32-bit range check.
+        // 32-bit range check.
+        self.range_check(x.elements[0], NUM_BITS);
+        self.range_check(x.elements[1], NUM_BITS);
+    }
+
+    fn i64_is_negative(&mut self, x: ValueTarget) -> BoolTarget {
+        // x is negative if the most significant bit of its most
+        // significant limb is 1.
+        let high_bits = self.split_le(x.elements[1], NUM_BITS);
+        high_bits[31]
+    }
+
+    fn assert_i64_less_if(&mut self, b: BoolTarget, x: ValueTarget, y: ValueTarget) {
+        // If b is false, replace `x` and `y` with dummy values.
+        let zero = ValueTarget::zero(self);
+        let one = ValueTarget::one(self);
+        let x = self.select_value(b, x, zero);
+        let y = self.select_value(b, y, one);
+
+        // Lt assertion.
         let assert_limb_lt = |builder: &mut Self, x, y| {
-            // Check that targets fit within `NUM_BITS` bits.
-            builder.range_check(x, NUM_BITS);
-            builder.range_check(y, NUM_BITS);
             // Check that `y-1-x` fits within `NUM_BITS` bits.
             let one = builder.one();
             let y_minus_one = builder.sub(y, one);
@@ -404,21 +440,14 @@ impl CircuitBuilderPod<F, D> for CircuitBuilder<F, D> {
             builder.range_check(expr, NUM_BITS);
         };
 
-        // If b is false, replace `x` and `y` with dummy values.
+        // Check if `x` and `y` have the same sign. If not, swap.
-        let zero = ValueTarget::zero(self);
+        let x_is_negative = self.i64_is_negative(x);
-        let one = ValueTarget::one(self);
+        let y_is_negative = self.i64_is_negative(y);
-        let x = self.select_value(b, x, zero);
+        let same_sign_ind = self.is_equal(x_is_negative.target, y_is_negative.target);
-        let y = self.select_value(b, y, one);
+        let (x, y) = (
-
+            self.select_value(same_sign_ind, x, y),
-        // `x` and `y` should only have two limbs each.
+            self.select_value(same_sign_ind, y, x),
-        x.elements
+        );
-            .into_iter()
-            .skip(2)
-            .for_each(|l| self.assert_zero(l));
-        y.elements
-            .into_iter()
-            .skip(2)
-            .for_each(|l| self.assert_zero(l));
 
         let big_limbs_eq = self.is_equal(x.elements[1], y.elements[1]);
         let lhs = self.select(big_limbs_eq, x.elements[0], x.elements[1]);

src/backends/plonky2/circuits/mainpod.rs

@@ -11,7 +11,7 @@ use crate::{
         circuits::{
             common::{
                 CircuitBuilderPod, Flattenable, MerkleClaimTarget, OperationTarget,
-                StatementTarget, ValueTarget,
+                StatementArgTarget, StatementTarget, ValueTarget,
             },
             signedpod::{SignedPodVerifyGadget, SignedPodVerifyTarget},
         },
@@ -37,6 +37,27 @@ struct OperationVerifyGadget {
 }
 
 impl OperationVerifyGadget {
+    fn first_n_args_are_valueofs(
+        &self,
+        builder: &mut CircuitBuilder<F, D>,
+        n: usize,
+        resolved_op_args: &[StatementTarget],
+    ) -> BoolTarget {
+        let arg_is_valueof = resolved_op_args[..n]
+            .iter()
+            .map(|arg| {
+                let st_type_ok =
+                    arg.has_native_type(builder, &self.params, NativePredicate::ValueOf);
+                let value_arg_ok = builder.statement_arg_is_value(&arg.args[1]);
+                builder.and(st_type_ok, value_arg_ok)
+            })
+            .collect::<Vec<_>>();
+        arg_is_valueof
+            .into_iter()
+            .reduce(|a, b| builder.and(a, b))
+            .expect("No args specified.")
+    }
+
     fn eval(
         &self,
         builder: &mut CircuitBuilder<F, D>,
@@ -60,7 +81,6 @@ impl OperationVerifyGadget {
                 .map(|&i| builder.vec_ref(prev_statements, i))
                 .collect::<Vec<_>>()
         };
-
         // Certain operations (Contains/NotContains) will refer to one
         // of the provided Merkle proofs (if any). These proofs have already
         // been verified, so we need only look up the claim.
@@ -71,10 +91,10 @@ impl OperationVerifyGadget {
         // `OperationVerifyTarget` so that we can set during witness generation.
 
         // For now only support native operations
-        // Op checks to carry out. Each 'eval_X' should be thought of
+        // Op checks to carry out. Each 'eval_X' should
-        // as 'eval' restricted to the op of type X, where the
+        // be thought of as 'eval' restricted to the op of type X,
-        // returned target is `false` if the input targets lie outside
+        // where the returned target is `false` if the input targets
-        // of the domain.
+        // lie outside of the domain.
         let op_checks = [
             vec![
                 self.eval_none(builder, st, op),
@@ -87,7 +107,7 @@ impl OperationVerifyGadget {
                 vec![
                     self.eval_copy(builder, st, op, &resolved_op_args)?,
                     self.eval_eq_from_entries(builder, st, op, &resolved_op_args),
-                    self.eval_lt_from_entries(builder, st, op, &resolved_op_args),
+                    self.eval_lt_lteq_from_entries(builder, st, op, &resolved_op_args),
                 ]
             },
             // Skip these if there are no resolved Merkle claims
@@ -122,24 +142,10 @@ impl OperationVerifyGadget {
     ) -> BoolTarget {
         let op_code_ok = op.has_native_type(builder, NativeOperation::NotContainsFromEntries);
 
-        // Expect 2 op args of type `ValueOf`.
+        let arg_types_ok = self.first_n_args_are_valueofs(builder, 2, resolved_op_args);
-        let op_arg_type_checks = resolved_op_args
-            .iter()
-            .take(2)
-            .map(|op_arg| op_arg.has_native_type(builder, &self.params, NativePredicate::ValueOf))
-            .collect::<Vec<_>>();
-        let op_arg_types_ok = builder.all(op_arg_type_checks);
 
-        // The values embedded in the op args must be values, i.e. the
+        let merkle_root_value = resolved_op_args[0].args[1].as_value();
-        // last `STATEMENT_ARG_F_LEN - VALUE_SIZE` slots of each being
+        let key_value = resolved_op_args[1].args[1].as_value();
-        // 0.
-        let merkle_root_arg = &resolved_op_args[0].args[1];
-        let key_arg = &resolved_op_args[1].args[1];
-        let op_arg_range_checks = [
-            builder.statement_arg_is_value(merkle_root_arg),
-            builder.statement_arg_is_value(key_arg),
-        ];
-        let op_arg_range_ok = builder.all(op_arg_range_checks);
 
         // Check Merkle proof (verified elsewhere) against op args.
         let merkle_proof_checks = [
@@ -149,13 +155,10 @@ impl OperationVerifyGadget {
             builder.not(resolved_merkle_claim.existence),
             /* ...for the root-key pair in the resolved op args. */
             builder.is_equal_slice(
-                &merkle_root_arg.elements[..VALUE_SIZE],
+                &merkle_root_value.elements,
                 &resolved_merkle_claim.root.elements,
             ),
-            builder.is_equal_slice(
+            builder.is_equal_slice(&key_value.elements, &resolved_merkle_claim.key.elements),
-                &key_arg.elements[..VALUE_SIZE],
-                &resolved_merkle_claim.key.elements,
-            ),
         ];
 
         let merkle_proof_ok = builder.all(merkle_proof_checks);
@@ -171,13 +174,7 @@ impl OperationVerifyGadget {
         );
         let st_ok = builder.is_equal_flattenable(st, &expected_statement);
 
-        builder.all([
+        builder.all([op_code_ok, arg_types_ok, merkle_proof_ok, st_ok])
-            op_code_ok,
-            op_arg_types_ok,
-            op_arg_range_ok,
-            merkle_proof_ok,
-            st_ok,
-        ])
     }
 
     fn eval_eq_from_entries(
@@ -189,27 +186,11 @@ impl OperationVerifyGadget {
     ) -> BoolTarget {
         let op_code_ok = op.has_native_type(builder, NativeOperation::EqualFromEntries);
 
-        // Expect 2 op args of type `ValueOf`.
+        let arg_types_ok = self.first_n_args_are_valueofs(builder, 2, resolved_op_args);
-        let op_arg_type_checks = resolved_op_args
-            .iter()
-            .take(2)
-            .map(|op_arg| op_arg.has_native_type(builder, &self.params, NativePredicate::ValueOf))
-            .collect::<Vec<_>>();
-        let op_arg_types_ok = builder.all(op_arg_type_checks);
 
-        // The values embedded in the op args must match, the last
+        let arg1_value = &resolved_op_args[0].args[1].as_value();
-        // `STATEMENT_ARG_F_LEN - VALUE_SIZE` slots of each being 0.
+        let arg2_value = resolved_op_args[1].args[1].as_value();
-        let arg1_value = &resolved_op_args[0].args[1];
+        let op_args_eq = builder.is_equal_slice(&arg1_value.elements, &arg2_value.elements);
-        let arg2_value = &resolved_op_args[1].args[1];
-        let op_arg_range_checks = [
-            builder.statement_arg_is_value(arg1_value),
-            builder.statement_arg_is_value(arg2_value),
-        ];
-        let op_arg_range_ok = builder.all(op_arg_range_checks);
-        let op_args_eq = builder.is_equal_slice(
-            &arg1_value.elements[..VALUE_SIZE],
-            &arg2_value.elements[..VALUE_SIZE],
-        );
 
         let arg1_key = resolved_op_args[0].args[0].clone();
         let arg2_key = resolved_op_args[1].args[0].clone();
@@ -221,59 +202,77 @@ impl OperationVerifyGadget {
         );
         let st_ok = builder.is_equal_flattenable(st, &expected_statement);
 
-        builder.all([
+        builder.all([op_code_ok, arg_types_ok, op_args_eq, st_ok])
-            op_code_ok,
-            op_arg_types_ok,
-            op_arg_range_ok,
-            op_args_eq,
-            st_ok,
-        ])
     }
 
-    fn eval_lt_from_entries(
+    /// Carries out the checks necessary for LtFromEntries and
+    /// LtEqFromEntries.
+    fn eval_lt_lteq_from_entries(
         &self,
         builder: &mut CircuitBuilder<F, D>,
         st: &StatementTarget,
         op: &OperationTarget,
         resolved_op_args: &[StatementTarget],
     ) -> BoolTarget {
-        let op_code_ok = op.has_native_type(builder, NativeOperation::LtFromEntries);
+        let zero = ValueTarget::zero(builder);
+        let one = ValueTarget::one(builder);
 
-        // Expect 2 op args of type `ValueOf`.
+        let lt_op_st_code_ok = {
-        let op_arg_type_checks = resolved_op_args
+            let op_code_ok = op.has_native_type(builder, NativeOperation::LtFromEntries);
-            .iter()
+            let st_code_ok = st.has_native_type(builder, &self.params, NativePredicate::Lt);
-            .take(2)
+            builder.and(op_code_ok, st_code_ok)
-            .map(|op_arg| op_arg.has_native_type(builder, &self.params, NativePredicate::ValueOf))
+        };
-            .collect::<Vec<_>>();
+        let lteq_op_st_code_ok = {
-        let op_arg_types_ok = builder.all(op_arg_type_checks);
+            let op_code_ok = op.has_native_type(builder, NativeOperation::LtEqFromEntries);
+            let st_code_ok = st.has_native_type(builder, &self.params, NativePredicate::LtEq);
+            builder.and(op_code_ok, st_code_ok)
+        };
+        let op_st_code_ok = builder.or(lt_op_st_code_ok, lteq_op_st_code_ok);
 
-        // The values embedded in the op args must satisfy `<`, the
+        let arg_types_ok = self.first_n_args_are_valueofs(builder, 2, resolved_op_args);
-        // last `STATEMENT_ARG_F_LEN - VALUE_SIZE` slots of each being
+
-        // 0.
+        let arg1_value = resolved_op_args[0].args[1].as_value();
-        let arg1_value = &resolved_op_args[0].args[1];
+        let arg2_value = resolved_op_args[1].args[1].as_value();
-        let arg2_value = &resolved_op_args[1].args[1];
+
-        let op_arg_range_checks = [arg1_value, arg2_value]
+        // If we are not dealing with the right op & statement types,
-            .into_iter()
+        // replace args with dummy values in the following checks.
-            .map(|x| builder.statement_arg_is_value(x))
+        let value1 = builder.select_value(op_st_code_ok, arg1_value, zero);
-            .collect::<Vec<_>>();
+        let value2 = builder.select_value(op_st_code_ok, arg2_value, one);
-        let op_arg_range_ok = builder.all(op_arg_range_checks);
+
-        builder.assert_less_if(
+        // Range check
-            op_code_ok,
+        builder.assert_i64(value1);
-            ValueTarget::from_slice(&arg1_value.elements[..VALUE_SIZE]),
+        builder.assert_i64(value2);
-            ValueTarget::from_slice(&arg2_value.elements[..VALUE_SIZE]),
+
-        );
+        // Check for equality.
+        let args_equal = builder.is_equal_slice(&value1.elements, &value2.elements);
+
+        // Check < if applicable.
+        let lt_check_flag = {
+            let not_args_equal = builder.not(args_equal);
+            let lteq_eq_case = builder.and(lteq_op_st_code_ok, not_args_equal);
+            builder.or(lt_op_st_code_ok, lteq_eq_case)
+        };
+        builder.assert_i64_less_if(lt_check_flag, value1, value2);
 
         let arg1_key = resolved_op_args[0].args[0].clone();
         let arg2_key = resolved_op_args[1].args[0].clone();
-        let expected_statement = StatementTarget::new_native(
-            builder,
-            &self.params,
-            NativePredicate::Lt,
-            &[arg1_key, arg2_key],
-        );
-        let st_ok = builder.is_equal_flattenable(st, &expected_statement);
 
-        builder.all([op_code_ok, op_arg_types_ok, op_arg_range_ok, st_ok])
+        let expected_st_args: Vec<_> = [arg1_key, arg2_key]
+            .into_iter()
+            .chain(std::iter::repeat_with(|| StatementArgTarget::none(builder)))
+            .take(self.params.max_statement_args)
+            .flat_map(|arg| arg.elements)
+            .collect();
+
+        let st_args_ok = builder.is_equal_slice(
+            &expected_st_args,
+            &st.args
+                .iter()
+                .flat_map(|arg| arg.elements)
+                .collect::<Vec<_>>(),
+        );
+
+        builder.all([op_st_code_ok, arg_types_ok, st_args_ok])
     }
 
     fn eval_none(
@@ -522,7 +521,10 @@ impl MainPodVerifyCircuit {
 
 #[cfg(test)]
 mod tests {
-    use plonky2::plonk::{circuit_builder::CircuitBuilder, circuit_data::CircuitConfig};
+    use plonky2::{
+        field::{goldilocks_field::GoldilocksField, types::Field},
+        plonk::{circuit_builder::CircuitBuilder, circuit_data::CircuitConfig},
+    };
 
     use super::*;
     use crate::{
@@ -583,7 +585,7 @@ mod tests {
         for (merkle_proof_target, merkle_proof) in
             merkle_proofs_target.iter().zip(merkle_proofs.iter())
         {
-            merkle_proof_target.set_targets(&mut pw, true, &merkle_proof)?
+            merkle_proof_target.set_targets(&mut pw, true, merkle_proof)?
         }
 
         // generate & verify proof
@@ -594,6 +596,146 @@ mod tests {
         Ok(())
     }
 
+    #[test]
+    fn test_lt_lteq_verify_failures() {
+        let st1: mainpod::Statement =
+            Statement::ValueOf(AnchoredKey::from((SELF, "hello")), Value::from(55)).into();
+        let st2: mainpod::Statement = Statement::ValueOf(
+            AnchoredKey::from((PodId(RawValue::from(75).into()), "world")),
+            Value::from(56),
+        )
+        .into();
+        let st3: mainpod::Statement = Statement::ValueOf(
+            AnchoredKey::from((PodId(RawValue::from(88).into()), "hola")),
+            Value::from(RawValue([
+                GoldilocksField::NEG_ONE,
+                GoldilocksField::ZERO,
+                GoldilocksField::ZERO,
+                GoldilocksField::ZERO,
+            ])),
+        )
+        .into();
+        let st4: mainpod::Statement = Statement::ValueOf(
+            AnchoredKey::from((PodId(RawValue::from(74).into()), "mundo")),
+            Value::from(-55),
+        )
+        .into();
+        let st5: mainpod::Statement = Statement::ValueOf(
+            AnchoredKey::from((PodId(RawValue::from(70).into()), "que")),
+            Value::from(-56),
+        )
+        .into();
+
+        let prev_statements = [st1, st2, st3, st4, st5];
+
+        [
+            // 56 < 55, 55 < 55, 56 <= 55, -55 < -55, -55 < -56, -55 <= -56 should fail to verify
+            (
+                mainpod::Operation(
+                    OperationType::Native(NativeOperation::LtFromEntries),
+                    vec![OperationArg::Index(1), OperationArg::Index(0)],
+                    OperationAux::None,
+                ),
+                Statement::Lt(
+                    AnchoredKey::from((PodId(RawValue::from(75).into()), "world")),
+                    AnchoredKey::from((SELF, "hello")),
+                )
+                .into(),
+            ),
+            (
+                mainpod::Operation(
+                    OperationType::Native(NativeOperation::LtFromEntries),
+                    vec![OperationArg::Index(0), OperationArg::Index(0)],
+                    OperationAux::None,
+                ),
+                Statement::Lt(
+                    AnchoredKey::from((SELF, "hello")),
+                    AnchoredKey::from((SELF, "hello")),
+                )
+                .into(),
+            ),
+            (
+                mainpod::Operation(
+                    OperationType::Native(NativeOperation::LtEqFromEntries),
+                    vec![OperationArg::Index(1), OperationArg::Index(0)],
+                    OperationAux::None,
+                ),
+                Statement::LtEq(
+                    AnchoredKey::from((PodId(RawValue::from(75).into()), "world")),
+                    AnchoredKey::from((SELF, "hello")),
+                )
+                .into(),
+            ),
+            (
+                mainpod::Operation(
+                    OperationType::Native(NativeOperation::LtFromEntries),
+                    vec![OperationArg::Index(3), OperationArg::Index(3)],
+                    OperationAux::None,
+                ),
+                Statement::Lt(
+                    AnchoredKey::from((PodId(RawValue::from(74).into()), "mundo")),
+                    AnchoredKey::from((PodId(RawValue::from(74).into()), "mundo")),
+                )
+                .into(),
+            ),
+            (
+                mainpod::Operation(
+                    OperationType::Native(NativeOperation::LtFromEntries),
+                    vec![OperationArg::Index(3), OperationArg::Index(4)],
+                    OperationAux::None,
+                ),
+                Statement::Lt(
+                    AnchoredKey::from((PodId(RawValue::from(74).into()), "mundo")),
+                    AnchoredKey::from((PodId(RawValue::from(70).into()), "que")),
+                )
+                .into(),
+            ),
+            (
+                mainpod::Operation(
+                    OperationType::Native(NativeOperation::LtEqFromEntries),
+                    vec![OperationArg::Index(3), OperationArg::Index(4)],
+                    OperationAux::None,
+                ),
+                Statement::LtEq(
+                    AnchoredKey::from((PodId(RawValue::from(74).into()), "mundo")),
+                    AnchoredKey::from((PodId(RawValue::from(70).into()), "que")),
+                )
+                .into(),
+            ),
+            // 56 < p-1 and p-1 <= p-1 should fail to verify, where p
+            // is the Goldilocks prime and 'p-1' occupies a single
+            // limb.
+            (
+                mainpod::Operation(
+                    OperationType::Native(NativeOperation::LtFromEntries),
+                    vec![OperationArg::Index(1), OperationArg::Index(2)],
+                    OperationAux::None,
+                ),
+                Statement::Lt(
+                    AnchoredKey::from((PodId(RawValue::from(75).into()), "world")),
+                    AnchoredKey::from((PodId(RawValue::from(88).into()), "hola")),
+                )
+                .into(),
+            ),
+            (
+                mainpod::Operation(
+                    OperationType::Native(NativeOperation::LtEqFromEntries),
+                    vec![OperationArg::Index(2), OperationArg::Index(2)],
+                    OperationAux::None,
+                ),
+                Statement::LtEq(
+                    AnchoredKey::from((PodId(RawValue::from(88).into()), "hola")),
+                    AnchoredKey::from((PodId(RawValue::from(88).into()), "hola")),
+                )
+                .into(),
+            ),
+        ]
+        .into_iter()
+        .for_each(|(op, st)| {
+            assert!(operation_verify(st, op, prev_statements.to_vec(), vec![]).is_err())
+        });
+    }
+
     #[test]
     fn test_operation_verify() -> Result<()> {
         let params = Params::default();
@@ -680,7 +822,121 @@ mod tests {
             vec![OperationArg::Index(0), OperationArg::Index(1)],
             OperationAux::None,
         );
-        let prev_statements = vec![st1.clone(), st2];
+        let prev_statements = vec![st1.clone(), st2.clone()];
+        operation_verify(st, op, prev_statements, merkle_proofs.clone())?;
+        // Also check negative < negative
+        let st3: mainpod::Statement = Statement::ValueOf(
+            AnchoredKey::from((PodId(RawValue::from(89).into()), "hola")),
+            Value::from(-56),
+        )
+        .into();
+        let st4: mainpod::Statement = Statement::ValueOf(
+            AnchoredKey::from((PodId(RawValue::from(84).into()), "mundo")),
+            Value::from(-55),
+        )
+        .into();
+        let st: mainpod::Statement = Statement::Lt(
+            AnchoredKey::from((PodId(RawValue::from(89).into()), "hola")),
+            AnchoredKey::from((PodId(RawValue::from(84).into()), "mundo")),
+        )
+        .into();
+        let op = mainpod::Operation(
+            OperationType::Native(NativeOperation::LtFromEntries),
+            vec![OperationArg::Index(0), OperationArg::Index(1)],
+            OperationAux::None,
+        );
+        let prev_statements = vec![st3.clone(), st4];
+        operation_verify(st, op, prev_statements, merkle_proofs.clone())?;
+        // Also check negative < positive
+        let st: mainpod::Statement = Statement::Lt(
+            AnchoredKey::from((PodId(RawValue::from(89).into()), "hola")),
+            AnchoredKey::from((PodId(RawValue::from(88).into()), "hello")),
+        )
+        .into();
+        let op = mainpod::Operation(
+            OperationType::Native(NativeOperation::LtFromEntries),
+            vec![OperationArg::Index(0), OperationArg::Index(1)],
+            OperationAux::None,
+        );
+        let prev_statements = vec![st3.clone(), st2];
+        operation_verify(st, op, prev_statements, merkle_proofs.clone())?;
+
+        // LtEq
+        let st2: mainpod::Statement = Statement::ValueOf(
+            AnchoredKey::from((PodId(RawValue::from(88).into()), "hello")),
+            Value::from(56),
+        )
+        .into();
+        let st: mainpod::Statement = Statement::LtEq(
+            AnchoredKey::from((SELF, "hello")),
+            AnchoredKey::from((PodId(RawValue::from(88).into()), "hello")),
+        )
+        .into();
+        let op = mainpod::Operation(
+            OperationType::Native(NativeOperation::LtEqFromEntries),
+            vec![OperationArg::Index(0), OperationArg::Index(1)],
+            OperationAux::None,
+        );
+        let prev_statements = vec![st1.clone(), st2.clone()];
+        operation_verify(st, op, prev_statements, merkle_proofs.clone())?;
+        // Also check negative <= negative
+        let st3: mainpod::Statement = Statement::ValueOf(
+            AnchoredKey::from((PodId(RawValue::from(89).into()), "hola")),
+            Value::from(-56),
+        )
+        .into();
+        let st4: mainpod::Statement = Statement::ValueOf(
+            AnchoredKey::from((PodId(RawValue::from(84).into()), "mundo")),
+            Value::from(-55),
+        )
+        .into();
+        let st: mainpod::Statement = Statement::LtEq(
+            AnchoredKey::from((PodId(RawValue::from(89).into()), "hola")),
+            AnchoredKey::from((PodId(RawValue::from(84).into()), "mundo")),
+        )
+        .into();
+        let op = mainpod::Operation(
+            OperationType::Native(NativeOperation::LtEqFromEntries),
+            vec![OperationArg::Index(0), OperationArg::Index(1)],
+            OperationAux::None,
+        );
+        let prev_statements = vec![st3.clone(), st4];
+        operation_verify(st, op, prev_statements, merkle_proofs.clone())?;
+        // Also check negative <= positive
+        let st: mainpod::Statement = Statement::LtEq(
+            AnchoredKey::from((PodId(RawValue::from(89).into()), "hola")),
+            AnchoredKey::from((PodId(RawValue::from(88).into()), "hello")),
+        )
+        .into();
+        let op = mainpod::Operation(
+            OperationType::Native(NativeOperation::LtEqFromEntries),
+            vec![OperationArg::Index(0), OperationArg::Index(1)],
+            OperationAux::None,
+        );
+        let prev_statements = vec![st3, st2];
+        operation_verify(st, op, prev_statements.clone(), merkle_proofs.clone())?;
+        // Also check equality, both positive and negative.
+        let st: mainpod::Statement = Statement::LtEq(
+            AnchoredKey::from((PodId(RawValue::from(89).into()), "hola")),
+            AnchoredKey::from((PodId(RawValue::from(89).into()), "hola")),
+        )
+        .into();
+        let op = mainpod::Operation(
+            OperationType::Native(NativeOperation::LtEqFromEntries),
+            vec![OperationArg::Index(0), OperationArg::Index(0)],
+            OperationAux::None,
+        );
+        operation_verify(st, op, prev_statements.clone(), merkle_proofs.clone())?;
+        let st: mainpod::Statement = Statement::LtEq(
+            AnchoredKey::from((PodId(RawValue::from(88).into()), "hello")),
+            AnchoredKey::from((PodId(RawValue::from(88).into()), "hello")),
+        )
+        .into();
+        let op = mainpod::Operation(
+            OperationType::Native(NativeOperation::LtEqFromEntries),
+            vec![OperationArg::Index(1), OperationArg::Index(1)],
+            OperationAux::None,
+        );
         operation_verify(st, op, prev_statements, merkle_proofs.clone())?;
 
         // NotContainsFromEntries

src/backends/plonky2/mainpod/statement.rs

@@ -59,7 +59,7 @@ impl TryFrom<Statement> for middleware::Statement {
                 (NP::NotEqual, (Some(SA::Key(ak1)), Some(SA::Key(ak2)), None), 2) => {
                     S::NotEqual(ak1, ak2)
                 }
-                (NP::Gt, (Some(SA::Key(ak1)), Some(SA::Key(ak2)), None), 2) => S::Gt(ak1, ak2),
+                (NP::LtEq, (Some(SA::Key(ak1)), Some(SA::Key(ak2)), None), 2) => S::LtEq(ak1, ak2),
                 (NP::Lt, (Some(SA::Key(ak1)), Some(SA::Key(ak2)), None), 2) => S::Lt(ak1, ak2),
                 (NP::Contains, (Some(SA::Key(ak1)), Some(SA::Key(ak2)), Some(SA::Key(ak3))), 3) => {
                     S::Contains(ak1, ak2, ak3)

src/frontend/mod.rs

@@ -234,6 +234,8 @@ impl MainPodBuilder {
 
     /// Lower syntactic sugar operation into backend compatible operation.
     /// - {Dict,Array,Set}Contains/NotContains becomes Contains/NotContains.
+    /// - GtEqFromEntries/GtFromEntries/GtToNotEqual becomes
+    ///   LtEqFromEntries/LtFromEntries/LtToNotEqual.
     fn lower_op(op: Operation) -> Operation {
         use NativeOperation::*;
         use OperationType::*;
@@ -259,6 +261,15 @@ impl MainPodBuilder {
                 let [array, index, value] = op.1.try_into().unwrap(); // TODO: Error handling
                 Operation(Native(ContainsFromEntries), vec![array, index, value], op.2)
             }
+            Native(GtEqFromEntries) => {
+                let [entry1, entry2] = op.1.try_into().unwrap(); // TODO: Error handling
+                Operation(Native(LtEqFromEntries), vec![entry2, entry1], op.2)
+            }
+            Native(GtFromEntries) => {
+                let [entry1, entry2] = op.1.try_into().unwrap(); // TODO: Error handling
+                Operation(Native(LtFromEntries), vec![entry2, entry1], op.2)
+            }
+            Native(GtToNotEqual) => Operation(Native(LtToNotEqual), op.1, op.2),
             _ => op,
         }
     }
@@ -315,17 +326,14 @@ impl MainPodBuilder {
         let st_args: Vec<StatementArg> = match op_type {
             OperationType::Native(o) => match o {
                 None => vec![],
-                NewEntry => self.op_args_entries(public, args)?,
+                NewEntry | EqualFromEntries | NotEqualFromEntries | LtFromEntries
+                | LtEqFromEntries => self.op_args_entries(public, args)?,
                 CopyStatement => match &args[0] {
                     OperationArg::Statement(s) => s.args().clone(),
                     _ => {
                         return Err(Error::op_invalid_args("copy".to_string()));
                     }
                 },
-                EqualFromEntries => self.op_args_entries(public, args)?,
-                NotEqualFromEntries => self.op_args_entries(public, args)?,
-                GtFromEntries => self.op_args_entries(public, args)?,
-                LtFromEntries => self.op_args_entries(public, args)?,
                 TransitiveEqualFromStatements => {
                     match (args[0].clone(), args[1].clone()) {
                         (
@@ -350,14 +358,6 @@ impl MainPodBuilder {
                         }
                     }
                 }
-                GtToNotEqual => match args[0].clone() {
-                    OperationArg::Statement(Statement::Gt(ak0, ak1)) => {
-                        vec![StatementArg::Key(ak0), StatementArg::Key(ak1)]
-                    }
-                    _ => {
-                        return Err(Error::op_invalid_args("gt-to-neq".to_string()));
-                    }
-                },
                 LtToNotEqual => match args[0].clone() {
                     OperationArg::Statement(Statement::Lt(ak0, ak1)) => {
                         vec![StatementArg::Key(ak0), StatementArg::Key(ak1)]
@@ -437,13 +437,10 @@ impl MainPodBuilder {
                 },
                 ContainsFromEntries => self.op_args_entries(public, args)?,
                 NotContainsFromEntries => self.op_args_entries(public, args)?,
-                // NOTE: Could we remove these and assume that this function is never called with
+                _ => Err(Error::custom(format!(
-                // syntax sugar operations?
+                    "Unexpected syntactic sugar: {:?}",
-                DictContainsFromEntries => self.op_args_entries(public, args)?,
+                    op_type
-                DictNotContainsFromEntries => self.op_args_entries(public, args)?,
+                )))?,
-                SetContainsFromEntries => self.op_args_entries(public, args)?,
-                SetNotContainsFromEntries => self.op_args_entries(public, args)?,
-                ArrayContainsFromEntries => self.op_args_entries(public, args)?,
             },
             OperationType::Custom(cpr) => {
                 let pred = &cpr.batch.predicates[cpr.index];

src/middleware/operation.rs

@@ -60,16 +60,15 @@ pub enum NativeOperation {
     CopyStatement = 2,
     EqualFromEntries = 3,
     NotEqualFromEntries = 4,
-    GtFromEntries = 5,
+    LtEqFromEntries = 5,
     LtFromEntries = 6,
     TransitiveEqualFromStatements = 7,
-    GtToNotEqual = 8,
+    LtToNotEqual = 8,
-    LtToNotEqual = 9,
+    ContainsFromEntries = 9,
-    ContainsFromEntries = 10,
+    NotContainsFromEntries = 10,
-    NotContainsFromEntries = 11,
+    SumOf = 11,
-    SumOf = 13,
+    ProductOf = 12,
-    ProductOf = 14,
+    MaxOf = 13,
-    MaxOf = 15,
 
     // Syntactic sugar operations.  These operations are not supported by the backend.  The
     // frontend compiler is responsible of translating these operations into the operations above.
@@ -78,6 +77,9 @@ pub enum NativeOperation {
     SetContainsFromEntries = 1003,
     SetNotContainsFromEntries = 1004,
     ArrayContainsFromEntries = 1005,
+    GtEqFromEntries = 1006,
+    GtFromEntries = 1007,
+    GtToNotEqual = 1008,
 }
 
 impl ToFields for NativeOperation {
@@ -102,12 +104,11 @@ impl OperationType {
                 NativeOperation::NotEqualFromEntries => {
                     Some(Predicate::Native(NativePredicate::NotEqual))
                 }
-                NativeOperation::GtFromEntries => Some(Predicate::Native(NativePredicate::Gt)),
+                NativeOperation::LtEqFromEntries => Some(Predicate::Native(NativePredicate::LtEq)),
                 NativeOperation::LtFromEntries => Some(Predicate::Native(NativePredicate::Lt)),
                 NativeOperation::TransitiveEqualFromStatements => {
                     Some(Predicate::Native(NativePredicate::Equal))
                 }
-                NativeOperation::GtToNotEqual => Some(Predicate::Native(NativePredicate::NotEqual)),
                 NativeOperation::LtToNotEqual => Some(Predicate::Native(NativePredicate::NotEqual)),
                 NativeOperation::ContainsFromEntries => {
                     Some(Predicate::Native(NativePredicate::Contains))
@@ -133,10 +134,9 @@ pub enum Operation {
     CopyStatement(Statement),
     EqualFromEntries(Statement, Statement),
     NotEqualFromEntries(Statement, Statement),
-    GtFromEntries(Statement, Statement),
+    LtEqFromEntries(Statement, Statement),
     LtFromEntries(Statement, Statement),
     TransitiveEqualFromStatements(Statement, Statement),
-    GtToNotEqual(Statement),
     LtToNotEqual(Statement),
     ContainsFromEntries(
         /* root  */ Statement,
@@ -165,10 +165,9 @@ impl Operation {
             Self::CopyStatement(_) => OT::Native(CopyStatement),
             Self::EqualFromEntries(_, _) => OT::Native(EqualFromEntries),
             Self::NotEqualFromEntries(_, _) => OT::Native(NotEqualFromEntries),
-            Self::GtFromEntries(_, _) => OT::Native(GtFromEntries),
+            Self::LtEqFromEntries(_, _) => OT::Native(LtEqFromEntries),
             Self::LtFromEntries(_, _) => OT::Native(LtFromEntries),
             Self::TransitiveEqualFromStatements(_, _) => OT::Native(TransitiveEqualFromStatements),
-            Self::GtToNotEqual(_) => OT::Native(GtToNotEqual),
             Self::LtToNotEqual(_) => OT::Native(LtToNotEqual),
             Self::ContainsFromEntries(_, _, _, _) => OT::Native(ContainsFromEntries),
             Self::NotContainsFromEntries(_, _, _) => OT::Native(NotContainsFromEntries),
@@ -186,10 +185,9 @@ impl Operation {
             Self::CopyStatement(s) => vec![s],
             Self::EqualFromEntries(s1, s2) => vec![s1, s2],
             Self::NotEqualFromEntries(s1, s2) => vec![s1, s2],
-            Self::GtFromEntries(s1, s2) => vec![s1, s2],
+            Self::LtEqFromEntries(s1, s2) => vec![s1, s2],
             Self::LtFromEntries(s1, s2) => vec![s1, s2],
             Self::TransitiveEqualFromStatements(s1, s2) => vec![s1, s2],
-            Self::GtToNotEqual(s) => vec![s],
             Self::LtToNotEqual(s) => vec![s],
             Self::ContainsFromEntries(s1, s2, s3, _pf) => vec![s1, s2, s3],
             Self::NotContainsFromEntries(s1, s2, _pf) => vec![s1, s2],
@@ -229,8 +227,8 @@ impl Operation {
                 (NO::NotEqualFromEntries, (Some(s1), Some(s2), None), OA::None, 2) => {
                     Self::NotEqualFromEntries(s1, s2)
                 }
-                (NO::GtFromEntries, (Some(s1), Some(s2), None), OA::None, 2) => {
+                (NO::LtEqFromEntries, (Some(s1), Some(s2), None), OA::None, 2) => {
-                    Self::GtFromEntries(s1, s2)
+                    Self::LtEqFromEntries(s1, s2)
                 }
                 (NO::LtFromEntries, (Some(s1), Some(s2), None), OA::None, 2) => {
                     Self::LtFromEntries(s1, s2)
@@ -282,8 +280,8 @@ impl Operation {
             (Self::NotEqualFromEntries(ValueOf(ak1, v1), ValueOf(ak2, v2)), NotEqual(ak3, ak4)) => {
                 Ok(v1 != v2 && ak3 == ak1 && ak4 == ak2)
             }
-            (Self::GtFromEntries(ValueOf(ak1, v1), ValueOf(ak2, v2)), Gt(ak3, ak4)) => {
+            (Self::LtEqFromEntries(ValueOf(ak1, v1), ValueOf(ak2, v2)), LtEq(ak3, ak4)) => {
-                Ok(v1 > v2 && ak3 == ak1 && ak4 == ak2)
+                Ok(v1 <= v2 && ak3 == ak1 && ak4 == ak2)
             }
             (Self::LtFromEntries(ValueOf(ak1, v1), ValueOf(ak2, v2)), Lt(ak3, ak4)) => {
                 Ok(v1 < v2 && ak3 == ak1 && ak4 == ak2)
@@ -302,7 +300,6 @@ impl Operation {
                 Self::TransitiveEqualFromStatements(Equal(ak1, ak2), Equal(ak3, ak4)),
                 Equal(ak5, ak6),
             ) => Ok(ak2 == ak3 && ak5 == ak1 && ak6 == ak4),
-            (Self::GtToNotEqual(Gt(ak1, ak2)), NotEqual(ak3, ak4)) => Ok(ak1 == ak3 && ak2 == ak4),
             (Self::LtToNotEqual(Lt(ak1, ak2)), NotEqual(ak3, ak4)) => Ok(ak1 == ak3 && ak2 == ak4),
             (
                 Self::SumOf(ValueOf(ak1, v1), ValueOf(ak2, v2), ValueOf(ak3, v3)),

src/middleware/statement.rs

@@ -25,7 +25,7 @@ pub enum NativePredicate {
     ValueOf = 1,
     Equal = 2,
     NotEqual = 3,
-    Gt = 4,
+    LtEq = 4,
     Lt = 5,
     Contains = 6,
     NotContains = 7,
@@ -40,6 +40,8 @@ pub enum NativePredicate {
     SetContains = 1002,
     SetNotContains = 1003,
     ArrayContains = 1004, // there is no ArrayNotContains
+    GtEq = 1005,
+    Gt = 1006,
 }
 
 impl ToFields for NativePredicate {
@@ -89,7 +91,7 @@ pub enum Statement {
     ValueOf(AnchoredKey, Value),
     Equal(AnchoredKey, AnchoredKey),
     NotEqual(AnchoredKey, AnchoredKey),
-    Gt(AnchoredKey, AnchoredKey),
+    LtEq(AnchoredKey, AnchoredKey),
     Lt(AnchoredKey, AnchoredKey),
     Contains(
         /* root  */ AnchoredKey,
@@ -114,7 +116,7 @@ impl Statement {
             Self::ValueOf(_, _) => Native(NativePredicate::ValueOf),
             Self::Equal(_, _) => Native(NativePredicate::Equal),
             Self::NotEqual(_, _) => Native(NativePredicate::NotEqual),
-            Self::Gt(_, _) => Native(NativePredicate::Gt),
+            Self::LtEq(_, _) => Native(NativePredicate::LtEq),
             Self::Lt(_, _) => Native(NativePredicate::Lt),
             Self::Contains(_, _, _) => Native(NativePredicate::Contains),
             Self::NotContains(_, _) => Native(NativePredicate::NotContains),
@@ -131,7 +133,7 @@ impl Statement {
             Self::ValueOf(ak, v) => vec![Key(ak), Literal(v)],
             Self::Equal(ak1, ak2) => vec![Key(ak1), Key(ak2)],
             Self::NotEqual(ak1, ak2) => vec![Key(ak1), Key(ak2)],
-            Self::Gt(ak1, ak2) => vec![Key(ak1), Key(ak2)],
+            Self::LtEq(ak1, ak2) => vec![Key(ak1), Key(ak2)],
             Self::Lt(ak1, ak2) => vec![Key(ak1), Key(ak2)],
             Self::Contains(ak1, ak2, ak3) => vec![Key(ak1), Key(ak2), Key(ak3)],
             Self::NotContains(ak1, ak2) => vec![Key(ak1), Key(ak2)],
@@ -172,11 +174,11 @@ impl Statement {
                     Err(Error::incorrect_statements_args())
                 }
             }
-            Native(NativePredicate::Gt) => {
+            Native(NativePredicate::LtEq) => {
                 if let (StatementArg::Key(a0), StatementArg::Key(a1)) =
                     (args[0].clone(), args[1].clone())
                 {
-                    Ok(Self::Gt(a0, a1))
+                    Ok(Self::LtEq(a0, a1))
                 } else {
                     Err(Error::incorrect_statements_args())
                 }