From 53ade6ea266b33194004f06c908bcff2fc4eabaf Mon Sep 17 00:00:00 2001 From: Ahmad Afuni Date: Tue, 6 May 2025 06:59:59 +1000 Subject: [PATCH] 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. * 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. --- src/backends/plonky2/circuits/common.rs | 77 ++-- src/backends/plonky2/circuits/mainpod.rs | 452 +++++++++++++++++----- src/backends/plonky2/mainpod/statement.rs | 2 +- src/frontend/mod.rs | 37 +- src/middleware/operation.rs | 39 +- src/middleware/statement.rs | 14 +- 6 files changed, 451 insertions(+), 170 deletions(-) diff --git a/src/backends/plonky2/circuits/common.rs b/src/backends/plonky2/circuits/common.rs index cd12f63..615ade7 100644 --- a/src/backends/plonky2/circuits/common.rs +++ b/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, 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. - fn assert_less_if(&mut self, b: BoolTarget, x: ValueTarget, y: ValueTarget); + + /// Checks whether `x` is an i64, which involves checking that it + /// 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 for CircuitBuilder { self.is_equal_slice(&arg.elements[VALUE_SIZE..], &zeros) } - fn assert_less_if(&mut self, b: BoolTarget, x: ValueTarget, y: ValueTarget) { - const NUM_BITS: usize = 32; + fn assert_i64(&mut self, x: ValueTarget) { + // `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 for CircuitBuilder { builder.range_check(expr, NUM_BITS); }; - // 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); - - // `x` and `y` should only have two limbs each. - 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)); + // Check if `x` and `y` have the same sign. If not, swap. + let x_is_negative = self.i64_is_negative(x); + let y_is_negative = self.i64_is_negative(y); + let same_sign_ind = self.is_equal(x_is_negative.target, y_is_negative.target); + let (x, y) = ( + self.select_value(same_sign_ind, x, y), + self.select_value(same_sign_ind, y, x), + ); 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]); diff --git a/src/backends/plonky2/circuits/mainpod.rs b/src/backends/plonky2/circuits/mainpod.rs index b2a7a38..2db0adc 100644 --- a/src/backends/plonky2/circuits/mainpod.rs +++ b/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, + 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::>(); + arg_is_valueof + .into_iter() + .reduce(|a, b| builder.and(a, b)) + .expect("No args specified.") + } + fn eval( &self, builder: &mut CircuitBuilder, @@ -60,7 +81,6 @@ impl OperationVerifyGadget { .map(|&i| builder.vec_ref(prev_statements, i)) .collect::>() }; - // 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 - // as 'eval' restricted to the op of type X, where the - // returned target is `false` if the input targets lie outside - // of the domain. + // Op checks to carry out. Each 'eval_X' should + // be thought of as 'eval' restricted to the op of type X, + // where the returned target is `false` if the input targets + // 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 op_arg_type_checks = resolved_op_args - .iter() - .take(2) - .map(|op_arg| op_arg.has_native_type(builder, &self.params, NativePredicate::ValueOf)) - .collect::>(); - let op_arg_types_ok = builder.all(op_arg_type_checks); + let arg_types_ok = self.first_n_args_are_valueofs(builder, 2, resolved_op_args); - // The values embedded in the op args must be values, i.e. the - // last `STATEMENT_ARG_F_LEN - VALUE_SIZE` slots of each being - // 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); + let merkle_root_value = resolved_op_args[0].args[1].as_value(); + let key_value = resolved_op_args[1].args[1].as_value(); // 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( - &key_arg.elements[..VALUE_SIZE], - &resolved_merkle_claim.key.elements, - ), + builder.is_equal_slice(&key_value.elements, &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([ - op_code_ok, - op_arg_types_ok, - op_arg_range_ok, - merkle_proof_ok, - st_ok, - ]) + builder.all([op_code_ok, arg_types_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 op_arg_type_checks = resolved_op_args - .iter() - .take(2) - .map(|op_arg| op_arg.has_native_type(builder, &self.params, NativePredicate::ValueOf)) - .collect::>(); - let op_arg_types_ok = builder.all(op_arg_type_checks); + let arg_types_ok = self.first_n_args_are_valueofs(builder, 2, resolved_op_args); - // The values embedded in the op args must match, the last - // `STATEMENT_ARG_F_LEN - VALUE_SIZE` slots of each being 0. - let arg1_value = &resolved_op_args[0].args[1]; - 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_value = &resolved_op_args[0].args[1].as_value(); + let arg2_value = resolved_op_args[1].args[1].as_value(); + let op_args_eq = builder.is_equal_slice(&arg1_value.elements, &arg2_value.elements); 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([ - op_code_ok, - op_arg_types_ok, - op_arg_range_ok, - op_args_eq, - st_ok, - ]) + builder.all([op_code_ok, arg_types_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, 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 op_arg_type_checks = resolved_op_args - .iter() - .take(2) - .map(|op_arg| op_arg.has_native_type(builder, &self.params, NativePredicate::ValueOf)) - .collect::>(); - let op_arg_types_ok = builder.all(op_arg_type_checks); + let lt_op_st_code_ok = { + let op_code_ok = op.has_native_type(builder, NativeOperation::LtFromEntries); + let st_code_ok = st.has_native_type(builder, &self.params, NativePredicate::Lt); + builder.and(op_code_ok, st_code_ok) + }; + let lteq_op_st_code_ok = { + 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 - // last `STATEMENT_ARG_F_LEN - VALUE_SIZE` slots of each being - // 0. - let arg1_value = &resolved_op_args[0].args[1]; - let arg2_value = &resolved_op_args[1].args[1]; - let op_arg_range_checks = [arg1_value, arg2_value] - .into_iter() - .map(|x| builder.statement_arg_is_value(x)) - .collect::>(); - let op_arg_range_ok = builder.all(op_arg_range_checks); - builder.assert_less_if( - op_code_ok, - ValueTarget::from_slice(&arg1_value.elements[..VALUE_SIZE]), - ValueTarget::from_slice(&arg2_value.elements[..VALUE_SIZE]), - ); + let arg_types_ok = self.first_n_args_are_valueofs(builder, 2, resolved_op_args); + + let arg1_value = resolved_op_args[0].args[1].as_value(); + let arg2_value = resolved_op_args[1].args[1].as_value(); + + // If we are not dealing with the right op & statement types, + // replace args with dummy values in the following checks. + let value1 = builder.select_value(op_st_code_ok, arg1_value, zero); + let value2 = builder.select_value(op_st_code_ok, arg2_value, one); + + // Range check + builder.assert_i64(value1); + builder.assert_i64(value2); + + // 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::>(), + ); + + 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 diff --git a/src/backends/plonky2/mainpod/statement.rs b/src/backends/plonky2/mainpod/statement.rs index b1fc4d2..7fa9c6c 100644 --- a/src/backends/plonky2/mainpod/statement.rs +++ b/src/backends/plonky2/mainpod/statement.rs @@ -59,7 +59,7 @@ impl TryFrom 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) diff --git a/src/frontend/mod.rs b/src/frontend/mod.rs index f5e592b..56d33ab 100644 --- a/src/frontend/mod.rs +++ b/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 = 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 - // syntax sugar operations? - DictContainsFromEntries => self.op_args_entries(public, args)?, - 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)?, + _ => Err(Error::custom(format!( + "Unexpected syntactic sugar: {:?}", + op_type + )))?, }, OperationType::Custom(cpr) => { let pred = &cpr.batch.predicates[cpr.index]; diff --git a/src/middleware/operation.rs b/src/middleware/operation.rs index 7c1d71e..405a32c 100644 --- a/src/middleware/operation.rs +++ b/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 = 9, - ContainsFromEntries = 10, - NotContainsFromEntries = 11, - SumOf = 13, - ProductOf = 14, - MaxOf = 15, + LtToNotEqual = 8, + ContainsFromEntries = 9, + NotContainsFromEntries = 10, + SumOf = 11, + ProductOf = 12, + MaxOf = 13, // 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) => { - Self::GtFromEntries(s1, s2) + (NO::LtEqFromEntries, (Some(s1), Some(s2), None), OA::None, 2) => { + 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)) => { - Ok(v1 > v2 && ak3 == ak1 && ak4 == ak2) + (Self::LtEqFromEntries(ValueOf(ak1, v1), ValueOf(ak2, v2)), LtEq(ak3, ak4)) => { + 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)), diff --git a/src/middleware/statement.rs b/src/middleware/statement.rs index a542bfe..2327335 100644 --- a/src/middleware/statement.rs +++ b/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()) }