feat(backend): implement more ops (#222)

* Implement more ops

* Split up op verification tests

* Code review

src/backends/plonky2/circuits/common.rs

@@ -222,6 +222,7 @@ pub trait Flattenable {
 /// For the purpose of op verification, we need only look up the
 /// Merkle claim rather than the Merkle proof since it is verified
 /// elsewhere.
+#[derive(Copy, Clone)]
 pub struct MerkleClaimTarget {
     pub(crate) enabled: BoolTarget,
     pub(crate) root: HashOutTarget,

src/backends/plonky2/circuits/mainpod.rs

@@ -1,3 +1,5 @@
+use std::array;
+
 use itertools::zip_eq;
 use plonky2::{
     hash::{hash_types::HashOutTarget, poseidon::PoseidonHash},
@@ -37,13 +39,16 @@ struct OperationVerifyGadget {
 }
 
 impl OperationVerifyGadget {
-    fn first_n_args_are_valueofs(
+    /// Checks whether the first `N` arguments to an op are ValueOf
+    /// statements, returning a boolean target indicating whether this
+    /// is the case as well as the value targets derived from each
+    /// argument.
+    fn first_n_args_as_values<const N: usize>(
         &self,
         builder: &mut CircuitBuilder<F, D>,
-        n: usize,
         resolved_op_args: &[StatementTarget],
-    ) -> BoolTarget {
+    ) -> (BoolTarget, [ValueTarget; N]) {
-        let arg_is_valueof = resolved_op_args[..n]
+        let arg_is_valueof = resolved_op_args[..N]
             .iter()
             .map(|arg| {
                 let st_type_ok =
@@ -52,10 +57,12 @@ impl OperationVerifyGadget {
                 builder.and(st_type_ok, value_arg_ok)
             })
             .collect::<Vec<_>>();
-        arg_is_valueof
+        let first_n_args_are_valueofs = arg_is_valueof
             .into_iter()
             .reduce(|a, b| builder.and(a, b))
-            .expect("No args specified.")
+            .expect("No args specified.");
+        let values = array::from_fn(|i| resolved_op_args[i].args[1].as_value());
+        (first_n_args_are_valueofs, values)
     }
 
     fn eval(
@@ -106,20 +113,31 @@ impl OperationVerifyGadget {
             } else {
                 vec![
                     self.eval_copy(builder, st, op, &resolved_op_args)?,
-                    self.eval_eq_from_entries(builder, st, op, &resolved_op_args),
+                    self.eval_eq_neq_from_entries(builder, st, op, &resolved_op_args),
                     self.eval_lt_lteq_from_entries(builder, st, op, &resolved_op_args),
+                    self.eval_transitive_eq(builder, st, op, &resolved_op_args),
+                    self.eval_lt_to_neq(builder, st, op, &resolved_op_args),
                     self.eval_hash_of(builder, st, op, &resolved_op_args),
                 ]
             },
             // Skip these if there are no resolved Merkle claims
             if let Some(resolved_merkle_claim) = resolved_merkle_claim {
-                vec![self.eval_not_contains_from_entries(
+                vec![
-                    builder,
+                    self.eval_contains_from_entries(
-                    st,
+                        builder,
-                    op,
+                        st,
-                    resolved_merkle_claim,
+                        op,
-                    &resolved_op_args,
+                        resolved_merkle_claim,
-                )]
+                        &resolved_op_args,
+                    ),
+                    self.eval_not_contains_from_entries(
+                        builder,
+                        st,
+                        op,
+                        resolved_merkle_claim,
+                        &resolved_op_args,
+                    ),
+                ]
             } else {
                 vec![]
             },
@@ -133,6 +151,51 @@ impl OperationVerifyGadget {
         Ok(())
     }
 
+    fn eval_contains_from_entries(
+        &self,
+        builder: &mut CircuitBuilder<F, D>,
+        st: &StatementTarget,
+        op: &OperationTarget,
+        resolved_merkle_claim: MerkleClaimTarget,
+        resolved_op_args: &[StatementTarget],
+    ) -> BoolTarget {
+        let op_code_ok = op.has_native_type(builder, NativeOperation::ContainsFromEntries);
+
+        let (arg_types_ok, [merkle_root_value, key_value, value_value]) =
+            self.first_n_args_as_values(builder, resolved_op_args);
+
+        // Check Merkle proof (verified elsewhere) against op args.
+        let merkle_proof_checks = [
+            /* The supplied Merkle proof must be enabled. */
+            resolved_merkle_claim.enabled,
+            /* ...and it must be an existence proof. */
+            resolved_merkle_claim.existence,
+            /* ...for the root-key-value triple in the resolved op args. */
+            builder.is_equal_slice(
+                &merkle_root_value.elements,
+                &resolved_merkle_claim.root.elements,
+            ),
+            builder.is_equal_slice(&key_value.elements, &resolved_merkle_claim.key.elements),
+            builder.is_equal_slice(&value_value.elements, &resolved_merkle_claim.value.elements),
+        ];
+
+        let merkle_proof_ok = builder.all(merkle_proof_checks);
+
+        // Check output statement
+        let arg1_key = resolved_op_args[0].args[0].clone();
+        let arg2_key = resolved_op_args[1].args[0].clone();
+        let arg3_key = resolved_op_args[2].args[0].clone();
+        let expected_statement = StatementTarget::new_native(
+            builder,
+            &self.params,
+            NativePredicate::Contains,
+            &[arg1_key, arg2_key, arg3_key],
+        );
+        let st_ok = builder.is_equal_flattenable(st, &expected_statement);
+
+        builder.all([op_code_ok, arg_types_ok, merkle_proof_ok, st_ok])
+    }
+
     fn eval_not_contains_from_entries(
         &self,
         builder: &mut CircuitBuilder<F, D>,
@@ -143,10 +206,8 @@ impl OperationVerifyGadget {
     ) -> BoolTarget {
         let op_code_ok = op.has_native_type(builder, NativeOperation::NotContainsFromEntries);
 
-        let arg_types_ok = self.first_n_args_are_valueofs(builder, 2, resolved_op_args);
+        let (arg_types_ok, [merkle_root_value, key_value]) =
-
+            self.first_n_args_as_values(builder, resolved_op_args);
-        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 = [
@@ -178,32 +239,52 @@ impl OperationVerifyGadget {
         builder.all([op_code_ok, arg_types_ok, merkle_proof_ok, st_ok])
     }
 
-    fn eval_eq_from_entries(
+    /// Carries out the checks necessary for EqualFromEntries and
+    /// NotEqualFromEntries.
+    fn eval_eq_neq_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::EqualFromEntries);
+        let eq_op_st_code_ok = {
+            let op_code_ok = op.has_native_type(builder, NativeOperation::EqualFromEntries);
+            let st_code_ok = st.has_native_type(builder, &self.params, NativePredicate::Equal);
+            builder.and(op_code_ok, st_code_ok)
+        };
+        let neq_op_st_code_ok = {
+            let op_code_ok = op.has_native_type(builder, NativeOperation::NotEqualFromEntries);
+            let st_code_ok = st.has_native_type(builder, &self.params, NativePredicate::NotEqual);
+            builder.and(op_code_ok, st_code_ok)
+        };
+        let op_st_code_ok = builder.or(eq_op_st_code_ok, neq_op_st_code_ok);
 
-        let arg_types_ok = self.first_n_args_are_valueofs(builder, 2, resolved_op_args);
+        let (arg_types_ok, [arg1_value, arg2_value]) =
+            self.first_n_args_as_values(builder, 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();
         let op_args_eq = builder.is_equal_slice(&arg1_value.elements, &arg2_value.elements);
+        let op_args_ok = builder.is_equal(op_args_eq.target, eq_op_st_code_ok.target);
 
         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::Equal,
-            &[arg1_key, arg2_key],
-        );
-        let st_ok = builder.is_equal_flattenable(st, &expected_statement);
 
-        builder.all([op_code_ok, arg_types_ok, op_args_eq, 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, op_args_ok, st_args_ok])
     }
 
     /// Carries out the checks necessary for LtFromEntries and
@@ -230,10 +311,8 @@ impl OperationVerifyGadget {
         };
         let op_st_code_ok = builder.or(lt_op_st_code_ok, lteq_op_st_code_ok);
 
-        let arg_types_ok = self.first_n_args_are_valueofs(builder, 2, resolved_op_args);
+        let (arg_types_ok, [arg1_value, arg2_value]) =
-
+            self.first_n_args_as_values(builder, 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.
@@ -285,11 +364,8 @@ impl OperationVerifyGadget {
     ) -> BoolTarget {
         let op_code_ok = op.has_native_type(builder, NativeOperation::HashOf);
 
-        let arg_types_ok = self.first_n_args_are_valueofs(builder, 3, resolved_op_args);
+        let (arg_types_ok, [arg1_value, arg2_value, arg3_value]) =
-
+            self.first_n_args_as_values(builder, 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();
-        let arg3_value = resolved_op_args[2].args[1].as_value();
 
         let expected_hash_value = builder.hash_values(arg2_value, arg3_value);
 
@@ -310,6 +386,39 @@ impl OperationVerifyGadget {
         builder.all([op_code_ok, arg_types_ok, hash_value_ok, st_ok])
     }
 
+    fn eval_transitive_eq(
+        &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::TransitiveEqualFromStatements);
+
+        let arg1_type_ok =
+            resolved_op_args[0].has_native_type(builder, &self.params, NativePredicate::Equal);
+        let arg2_type_ok =
+            resolved_op_args[1].has_native_type(builder, &self.params, NativePredicate::Equal);
+        let arg_types_ok = builder.all([arg1_type_ok, arg2_type_ok]);
+
+        let arg1_key1 = &resolved_op_args[0].args[0];
+        let arg1_key2 = &resolved_op_args[0].args[1];
+        let arg2_key1 = &resolved_op_args[1].args[0];
+        let arg2_key2 = &resolved_op_args[1].args[1];
+
+        let inner_keys_match = builder.is_equal_slice(&arg1_key2.elements, &arg2_key1.elements);
+
+        let expected_statement = StatementTarget::new_native(
+            builder,
+            &self.params,
+            NativePredicate::Equal,
+            &[arg1_key1.clone(), arg2_key2.clone()],
+        );
+        let st_ok = builder.is_equal_flattenable(st, &expected_statement);
+
+        builder.all([op_code_ok, arg_types_ok, inner_keys_match, st_ok])
+    }
     fn eval_none(
         &self,
         builder: &mut CircuitBuilder<F, D>,
@@ -360,6 +469,32 @@ impl OperationVerifyGadget {
         builder.all([op_code_ok, st_code_ok, arg_prefix_ok, no_dupes_ok])
     }
 
+    fn eval_lt_to_neq(
+        &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::LtToNotEqual);
+
+        let arg_type_ok =
+            resolved_op_args[0].has_native_type(builder, &self.params, NativePredicate::Lt);
+
+        let arg1_key = resolved_op_args[0].args[0].clone();
+        let arg2_key = resolved_op_args[0].args[1].clone();
+
+        let expected_statement = StatementTarget::new_native(
+            builder,
+            &self.params,
+            NativePredicate::NotEqual,
+            &[arg1_key, arg2_key],
+        );
+        let st_ok = builder.is_equal_flattenable(st, &expected_statement);
+
+        builder.all([op_code_ok, arg_type_ok, st_ok])
+    }
+
     fn eval_copy(
         &self,
         builder: &mut CircuitBuilder<F, D>,
@@ -772,10 +907,61 @@ mod tests {
     }
 
     #[test]
-    fn test_operation_verify() -> Result<()> {
+    fn test_eq_neq_verify_failures() {
-        let params = Params::default();
+        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 prev_statements = [st1, st2, st3];
 
-        // None
+        [
+            // 56 == 55, 55 != 55 should fail to verify
+            (
+                mainpod::Operation(
+                    OperationType::Native(NativeOperation::EqualFromEntries),
+                    vec![OperationArg::Index(1), OperationArg::Index(0)],
+                    OperationAux::None,
+                ),
+                Statement::Equal(
+                    AnchoredKey::from((PodId(RawValue::from(75).into()), "world")),
+                    AnchoredKey::from((SELF, "hello")),
+                )
+                .into(),
+            ),
+            (
+                mainpod::Operation(
+                    OperationType::Native(NativeOperation::NotEqualFromEntries),
+                    vec![OperationArg::Index(0), OperationArg::Index(0)],
+                    OperationAux::None,
+                ),
+                Statement::NotEqual(
+                    AnchoredKey::from((SELF, "hello")),
+                    AnchoredKey::from((SELF, "hello")),
+                )
+                .into(),
+            ),
+        ]
+        .into_iter()
+        .for_each(|(op, st)| {
+            assert!(operation_verify(st, op, prev_statements.to_vec(), vec![]).is_err())
+        });
+    }
+
+    #[test]
+    fn test_operation_verify_none() -> Result<()> {
         let st: mainpod::Statement = Statement::None.into();
         let op = mainpod::Operation(
             OperationType::Native(NativeOperation::None),
@@ -783,15 +969,11 @@ mod tests {
             OperationAux::None,
         );
         let prev_statements = vec![Statement::None.into()];
-        let merkle_proofs = vec![];
+        operation_verify(st, op, prev_statements, vec![])
-        operation_verify(
+    }
-            st.clone(),
-            op,
-            prev_statements.clone(),
-            merkle_proofs.clone(),
-        )?;
 
-        // NewEntry
+    #[test]
+    fn test_operation_verify_newentry() -> Result<()> {
         let st1: mainpod::Statement =
             Statement::ValueOf(AnchoredKey::from((SELF, "hello")), Value::from(55)).into();
         let st2: mainpod::Statement = Statement::ValueOf(
@@ -805,14 +987,11 @@ mod tests {
             vec![],
             OperationAux::None,
         );
-        operation_verify(
+        operation_verify(st1, op, prev_statements, vec![])
-            st1.clone(),
+    }
-            op,
-            prev_statements.clone(),
-            merkle_proofs.clone(),
-        )?;
 
-        // Copy
+    #[test]
+    fn test_operation_verify_copy() -> Result<()> {
         let st: mainpod::Statement = Statement::None.into();
         let op = mainpod::Operation(
             OperationType::Native(NativeOperation::CopyStatement),
@@ -820,9 +999,13 @@ mod tests {
             OperationAux::None,
         );
         let prev_statements = vec![Statement::None.into()];
-        operation_verify(st, op, prev_statements, merkle_proofs.clone())?;
+        operation_verify(st, op, prev_statements, vec![])
+    }
 
-        // Eq
+    #[test]
+    fn test_operation_verify_eq() -> Result<()> {
+        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(55),
@@ -838,10 +1021,37 @@ mod tests {
             vec![OperationArg::Index(0), OperationArg::Index(1)],
             OperationAux::None,
         );
-        let prev_statements = vec![st1.clone(), st2];
+        let prev_statements = vec![st1, st2];
-        operation_verify(st, op, prev_statements, merkle_proofs.clone())?;
+        operation_verify(st, op, prev_statements, vec![])
+    }
 
-        // Lt
+    #[test]
+    fn test_operation_verify_neq() -> Result<()> {
+        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(58),
+        )
+        .into();
+        let st: mainpod::Statement = Statement::NotEqual(
+            AnchoredKey::from((SELF, "hello")),
+            AnchoredKey::from((PodId(RawValue::from(75).into()), "world")),
+        )
+        .into();
+        let op = mainpod::Operation(
+            OperationType::Native(NativeOperation::NotEqualFromEntries),
+            vec![OperationArg::Index(0), OperationArg::Index(1)],
+            OperationAux::None,
+        );
+        let prev_statements = vec![st1, st2];
+        operation_verify(st, op, prev_statements, vec![])
+    }
+
+    #[test]
+    fn test_operation_verify_lt() -> Result<()> {
+        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(88).into()), "hello")),
             Value::from(56),
@@ -857,8 +1067,9 @@ mod tests {
             vec![OperationArg::Index(0), OperationArg::Index(1)],
             OperationAux::None,
         );
-        let prev_statements = vec![st1.clone(), st2.clone()];
+        let prev_statements = vec![st1, st2.clone()];
-        operation_verify(st, op, prev_statements, merkle_proofs.clone())?;
+        operation_verify(st, op, prev_statements, vec![])?;
+
         // Also check negative < negative
         let st3: mainpod::Statement = Statement::ValueOf(
             AnchoredKey::from((PodId(RawValue::from(89).into()), "hola")),
@@ -881,7 +1092,8 @@ mod tests {
             OperationAux::None,
         );
         let prev_statements = vec![st3.clone(), st4];
-        operation_verify(st, op, prev_statements, merkle_proofs.clone())?;
+        operation_verify(st, op, prev_statements, vec![])?;
+
         // Also check negative < positive
         let st: mainpod::Statement = Statement::Lt(
             AnchoredKey::from((PodId(RawValue::from(89).into()), "hola")),
@@ -893,10 +1105,14 @@ mod tests {
             vec![OperationArg::Index(0), OperationArg::Index(1)],
             OperationAux::None,
         );
-        let prev_statements = vec![st3.clone(), st2];
+        let prev_statements = vec![st3, st2];
-        operation_verify(st, op, prev_statements, merkle_proofs.clone())?;
+        operation_verify(st, op, prev_statements, vec![])
+    }
 
-        // LtEq
+    #[test]
+    fn test_operation_verify_lteq() -> Result<()> {
+        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(88).into()), "hello")),
             Value::from(56),
@@ -912,8 +1128,9 @@ mod tests {
             vec![OperationArg::Index(0), OperationArg::Index(1)],
             OperationAux::None,
         );
-        let prev_statements = vec![st1.clone(), st2.clone()];
+        let prev_statements = vec![st1, st2.clone()];
-        operation_verify(st, op, prev_statements, merkle_proofs.clone())?;
+        operation_verify(st, op, prev_statements, vec![])?;
+
         // Also check negative <= negative
         let st3: mainpod::Statement = Statement::ValueOf(
             AnchoredKey::from((PodId(RawValue::from(89).into()), "hola")),
@@ -936,7 +1153,8 @@ mod tests {
             OperationAux::None,
         );
         let prev_statements = vec![st3.clone(), st4];
-        operation_verify(st, op, prev_statements, merkle_proofs.clone())?;
+        operation_verify(st, op, prev_statements, vec![])?;
+
         // Also check negative <= positive
         let st: mainpod::Statement = Statement::LtEq(
             AnchoredKey::from((PodId(RawValue::from(89).into()), "hola")),
@@ -949,7 +1167,8 @@ mod tests {
             OperationAux::None,
         );
         let prev_statements = vec![st3, st2];
-        operation_verify(st, op, prev_statements.clone(), merkle_proofs.clone())?;
+        operation_verify(st, op, prev_statements.clone(), vec![])?;
+
         // Also check equality, both positive and negative.
         let st: mainpod::Statement = Statement::LtEq(
             AnchoredKey::from((PodId(RawValue::from(89).into()), "hola")),
@@ -961,7 +1180,7 @@ mod tests {
             vec![OperationArg::Index(0), OperationArg::Index(0)],
             OperationAux::None,
         );
-        operation_verify(st, op, prev_statements.clone(), merkle_proofs.clone())?;
+        operation_verify(st, op, prev_statements.clone(), vec![])?;
         let st: mainpod::Statement = Statement::LtEq(
             AnchoredKey::from((PodId(RawValue::from(88).into()), "hello")),
             AnchoredKey::from((PodId(RawValue::from(88).into()), "hello")),
@@ -972,9 +1191,11 @@ mod tests {
             vec![OperationArg::Index(1), OperationArg::Index(1)],
             OperationAux::None,
         );
-        operation_verify(st, op, prev_statements, merkle_proofs.clone())?;
+        operation_verify(st, op, prev_statements, vec![])
+    }
 
-        // HashOf
+    #[test]
+    fn test_operation_verify_hashof() -> Result<()> {
         let input_values = [
             Value::from(RawValue([
                 GoldilocksField(1),
@@ -1019,9 +1240,60 @@ mod tests {
             OperationAux::None,
         );
         let prev_statements = vec![st1, st2, st3];
-        operation_verify(st, op, prev_statements, merkle_proofs.clone())?;
+        operation_verify(st, op, prev_statements, vec![])
+    }
+
+    #[test]
+    fn test_operation_verify_lt_to_neq() -> Result<()> {
+        let st: mainpod::Statement = Statement::NotEqual(
+            AnchoredKey::from((SELF, "hello")),
+            AnchoredKey::from((PodId(RawValue::from(88).into()), "hello")),
+        )
+        .into();
+        let st1: mainpod::Statement = Statement::Lt(
+            AnchoredKey::from((SELF, "hello")),
+            AnchoredKey::from((PodId(RawValue::from(88).into()), "hello")),
+        )
+        .into();
+        let op = mainpod::Operation(
+            OperationType::Native(NativeOperation::LtToNotEqual),
+            vec![OperationArg::Index(0)],
+            OperationAux::None,
+        );
+        let prev_statements = vec![st1];
+        operation_verify(st, op, prev_statements, vec![])
+    }
+
+    #[test]
+    fn test_operation_verify_transitive_eq() -> Result<()> {
+        let st: mainpod::Statement = Statement::Equal(
+            AnchoredKey::from((SELF, "hello")),
+            AnchoredKey::from((PodId(RawValue::from(88).into()), "hola")),
+        )
+        .into();
+        let st1: mainpod::Statement = Statement::Equal(
+            AnchoredKey::from((SELF, "hello")),
+            AnchoredKey::from((PodId(RawValue::from(89).into()), "world")),
+        )
+        .into();
+        let st2: mainpod::Statement = Statement::Equal(
+            AnchoredKey::from((PodId(RawValue::from(89).into()), "world")),
+            AnchoredKey::from((PodId(RawValue::from(88).into()), "hola")),
+        )
+        .into();
+        let op = mainpod::Operation(
+            OperationType::Native(NativeOperation::TransitiveEqualFromStatements),
+            vec![OperationArg::Index(0), OperationArg::Index(1)],
+            OperationAux::None,
+        );
+        let prev_statements = vec![st1, st2];
+        operation_verify(st, op, prev_statements, vec![])
+    }
+
+    #[test]
+    fn test_operation_verify_sintains() -> Result<()> {
+        let params = Params::default();
 
-        // NotContainsFromEntries
         let kvs = [
             (1.into(), 55.into()),
             (2.into(), 88.into()),
@@ -1055,8 +1327,54 @@ mod tests {
             no_key_pf,
         )];
         let prev_statements = vec![root_st, key_st];
-        operation_verify(st, op, prev_statements, merkle_proofs.clone())?;
+        operation_verify(st, op, prev_statements, merkle_proofs)
+    }
 
-        Ok(())
+    #[test]
+    fn test_operation_verify_contains() -> Result<()> {
+        let params = Params::default();
+
+        let kvs = [
+            (1.into(), 55.into()),
+            (2.into(), 88.into()),
+            (175.into(), 0.into()),
+        ]
+        .into_iter()
+        .collect();
+        let mt = MerkleTree::new(params.max_depth_mt_gadget, &kvs)?;
+
+        let root = Value::from(mt.root());
+        let root_ak = AnchoredKey::from((PodId(RawValue::from(88).into()), "merkle root"));
+
+        let key = 175.into();
+        let key_ak = AnchoredKey::from((PodId(RawValue::from(70).into()), "key"));
+
+        let (value, key_pf) = mt.prove(&key)?;
+        let value_ak = AnchoredKey::from((PodId(RawValue::from(72).into()), "value"));
+
+        let root_st: mainpod::Statement = Statement::ValueOf(root_ak.clone(), root.clone()).into();
+        let key_st: mainpod::Statement = Statement::ValueOf(key_ak.clone(), key.into()).into();
+        let value_st: mainpod::Statement =
+            Statement::ValueOf(value_ak.clone(), value.into()).into();
+
+        let st: mainpod::Statement = Statement::Contains(root_ak, key_ak, value_ak).into();
+        let op = mainpod::Operation(
+            OperationType::Native(NativeOperation::ContainsFromEntries),
+            vec![
+                OperationArg::Index(0),
+                OperationArg::Index(1),
+                OperationArg::Index(2),
+            ],
+            OperationAux::MerkleProofIndex(0),
+        );
+
+        let merkle_proofs = vec![MerkleClaimAndProof::new(
+            Hash::from(root.raw()),
+            key,
+            Some(value),
+            key_pf,
+        )];
+        let prev_statements = vec![root_st, key_st, value_st];
+        operation_verify(st, op, prev_statements, merkle_proofs)
     }
 }