diff --git a/.github/workflows/typos.toml b/.github/workflows/typos.toml
index 66d2d657..07d01ab6 100644
--- a/.github/workflows/typos.toml
+++ b/.github/workflows/typos.toml
@@ -4,3 +4,4 @@ BA = "BA"
 Ded = "Ded" # "ANDed", it thought "Ded" should be "Dead"
 OT = "OT"
 aks = "aks" # anchored keys
+nin = "nin" # not in
diff --git a/src/backends/plonky2/circuits/mainpod.rs b/src/backends/plonky2/circuits/mainpod.rs
index e7238d77..c0cdfe91 100644
--- a/src/backends/plonky2/circuits/mainpod.rs
+++ b/src/backends/plonky2/circuits/mainpod.rs
@@ -491,7 +491,10 @@ impl MainPodVerifyCircuit {
 mod tests {
     use super::*;
     use crate::backends::plonky2::mock::mainpod;
-    use crate::backends::plonky2::{basetypes::C, mock::mainpod::OperationArg};
+    use crate::backends::plonky2::{
+        basetypes::C,
+        mock::mainpod::{OperationArg, OperationAux},
+    };
     use crate::middleware::{OperationType, PodId};
     use plonky2::plonk::{circuit_builder::CircuitBuilder, circuit_data::CircuitConfig};
 
@@ -571,20 +574,29 @@ mod tests {
     fn test_operation_verify() -> Result<()> {
         // None
         let st: mainpod::Statement = Statement::None.into();
-        let op = mainpod::Operation(OperationType::Native(NativeOperation::None), vec![]);
+        let op = mainpod::Operation(
+            OperationType::Native(NativeOperation::None),
+            vec![],
+            OperationAux::None,
+        );
         let prev_statements = vec![Statement::None.into()];
         operation_verify(st.clone(), op, prev_statements.clone())?;
 
         // NewEntry
         let st1: mainpod::Statement =
             Statement::ValueOf(AnchoredKey(SELF, "hello".into()), 55.into()).into();
-        let op = mainpod::Operation(OperationType::Native(NativeOperation::NewEntry), vec![]);
+        let op = mainpod::Operation(
+            OperationType::Native(NativeOperation::NewEntry),
+            vec![],
+            OperationAux::None,
+        );
         operation_verify(st1.clone(), op, vec![])?;
 
         // Copy
         let op = mainpod::Operation(
             OperationType::Native(NativeOperation::CopyStatement),
             vec![OperationArg::Index(0)],
+            OperationAux::None,
         );
         operation_verify(st, op, prev_statements)?;
 
@@ -602,6 +614,7 @@ mod tests {
         let op = mainpod::Operation(
             OperationType::Native(NativeOperation::EqualFromEntries),
             vec![OperationArg::Index(0), OperationArg::Index(1)],
+            OperationAux::None,
         );
         let prev_statements = vec![st1.clone(), st2];
         operation_verify(st, op, prev_statements)?;
@@ -620,6 +633,7 @@ mod tests {
         let op = mainpod::Operation(
             OperationType::Native(NativeOperation::LtFromEntries),
             vec![OperationArg::Index(0), OperationArg::Index(1)],
+            OperationAux::None,
         );
         let prev_statements = vec![st1.clone(), st2];
         operation_verify(st, op, prev_statements)?;
diff --git a/src/backends/plonky2/mock/mainpod/mod.rs b/src/backends/plonky2/mock/mainpod/mod.rs
index 6f2e5071..d3cee821 100644
--- a/src/backends/plonky2/mock/mainpod/mod.rs
+++ b/src/backends/plonky2/mock/mainpod/mod.rs
@@ -8,10 +8,13 @@ use serde::{Deserialize, Serialize};
 use std::any::Any;
 use std::fmt;
 
-use crate::middleware::{
-    self, hash_str, AnchoredKey, Hash, MainPodInputs, NativeOperation, NativePredicate, NonePod,
-    OperationType, Params, Pod, PodId, PodProver, Predicate, StatementArg, ToFields, KEY_TYPE,
-    SELF,
+use crate::{
+    backends::plonky2::primitives::merkletree::MerkleProof,
+    middleware::{
+        self, hash_str, AnchoredKey, Hash, MainPodInputs, NativeOperation, NativePredicate,
+        NonePod, OperationType, Params, Pod, PodId, PodProver, Predicate, StatementArg, ToFields,
+        KEY_TYPE, SELF,
+    },
 };
 
 mod operation;
@@ -41,6 +44,9 @@ pub struct MockMainPod {
     operations: Vec<Operation>,
     // All statements (inherited + new)
     statements: Vec<Statement>,
+    // All Merkle proofs
+    // TODO: Use a backend-specific representation
+    merkle_proofs: Vec<MerkleProof>,
 }
 
 impl fmt::Display for MockMainPod {
@@ -243,9 +249,28 @@ impl MockMainPod {
         }
     }
 
+    fn find_op_aux(
+        merkle_proofs: &[MerkleProof],
+        op_aux: &middleware::OperationAux,
+    ) -> Result<OperationAux> {
+        match op_aux {
+            middleware::OperationAux::None => Ok(OperationAux::None),
+            middleware::OperationAux::MerkleProof(pf_arg) => merkle_proofs
+                .iter()
+                .enumerate()
+                .find_map(|(i, pf)| (pf == pf_arg).then_some(i))
+                .map(OperationAux::MerkleProofIndex)
+                .ok_or(anyhow!(
+                    "Merkle proof corresponding to op arg {} not found",
+                    op_aux
+                )),
+        }
+    }
+
     fn process_private_statements_operations(
         params: &Params,
         statements: &[Statement],
+        merkle_proofs: &[MerkleProof],
         input_operations: &[middleware::Operation],
     ) -> Result<Vec<Operation>> {
         let mut operations = Vec::new();
@@ -259,8 +284,12 @@ impl MockMainPod {
                 .iter()
                 .map(|mid_arg| Self::find_op_arg(statements, mid_arg))
                 .collect::<Result<Vec<_>>>()?;
+
+            let mid_aux = op.aux();
+            let aux = Self::find_op_aux(merkle_proofs, &mid_aux)?;
+
             Self::pad_operation_args(params, &mut args);
-            operations.push(Operation(op.op_type(), args));
+            operations.push(Operation(op.op_type(), args, aux));
         }
         Ok(operations)
     }
@@ -278,17 +307,22 @@ impl MockMainPod {
         operations.push(Operation(
             OperationType::Native(NativeOperation::NewEntry),
             vec![],
+            OperationAux::None,
         ));
         for i in 0..(params.max_public_statements - 1) {
             let st = &statements[offset_public_statements + i + 1];
             let mut op = if st.is_none() {
-                Operation(OperationType::Native(NativeOperation::None), vec![])
+                Operation(
+                    OperationType::Native(NativeOperation::None),
+                    vec![],
+                    OperationAux::None,
+                )
             } else {
                 let mid_arg = st.clone();
                 Operation(
                     OperationType::Native(NativeOperation::CopyStatement),
-                    // TODO
-                    vec![Self::find_op_arg(statements, &mid_arg.try_into().unwrap())?],
+                    vec![Self::find_op_arg(statements, &mid_arg.try_into()?)?],
+                    OperationAux::None,
                 )
             };
             fill_pad(&mut op.1, OperationArg::None, params.max_operation_args);
@@ -304,8 +338,21 @@ impl MockMainPod {
         // TODO: Insert a new public statement of ValueOf with `key=KEY_TYPE,
         // value=PodType::MockMainPod`
         let statements = Self::layout_statements(params, &inputs);
-        let operations =
-            Self::process_private_statements_operations(params, &statements, inputs.operations)?;
+        let merkle_proofs = inputs
+            .operations
+            .iter()
+            .flat_map(|op| match op {
+                middleware::Operation::ContainsFromEntries(_, _, _, pf) => Some(pf.clone()),
+                middleware::Operation::NotContainsFromEntries(_, _, pf) => Some(pf.clone()),
+                _ => None,
+            })
+            .collect::<Vec<_>>();
+        let operations = Self::process_private_statements_operations(
+            params,
+            &statements,
+            &merkle_proofs,
+            inputs.operations,
+        )?;
         let operations =
             Self::process_public_statements_operations(params, &statements, operations)?;
 
@@ -340,6 +387,7 @@ impl MockMainPod {
             public_statements,
             statements,
             operations,
+            merkle_proofs,
         })
     }
 
@@ -350,7 +398,11 @@ impl MockMainPod {
     }
 
     fn operation_none(params: &Params) -> Operation {
-        let mut op = Operation(OperationType::Native(NativeOperation::None), vec![]);
+        let mut op = Operation(
+            OperationType::Native(NativeOperation::None),
+            vec![],
+            OperationAux::None,
+        );
         fill_pad(&mut op.1, OperationArg::None, params.max_operation_args);
         op
     }
@@ -444,7 +496,10 @@ impl Pod for MockMainPod {
             .enumerate()
             .map(|(i, s)| {
                 self.operations[i]
-                    .deref(&self.statements[..input_statement_offset + i])
+                    .deref(
+                        &self.statements[..input_statement_offset + i],
+                        &self.merkle_proofs,
+                    )
                     .unwrap()
                     .check_and_log(&self.params, &s.clone().try_into().unwrap())
             })
@@ -513,13 +568,18 @@ pub mod tests {
         zu_kyc_sign_pod_builders,
     };
     use crate::middleware;
+    use crate::middleware::containers::Set;
 
     #[test]
     fn test_mock_main_zu_kyc() -> Result<()> {
         let params = middleware::Params::default();
+        let sanctions_values = ["A343434340"].map(|s| crate::frontend::Value::from(s));
+        let sanction_set = crate::frontend::Value::Set(crate::frontend::containers::Set::new(
+            sanctions_values.to_vec(),
+        )?);
 
         let (gov_id_builder, pay_stub_builder, sanction_list_builder) =
-            zu_kyc_sign_pod_builders(&params);
+            zu_kyc_sign_pod_builders(&params, &sanction_set);
         let mut signer = MockSigner {
             pk: "ZooGov".into(),
         };
diff --git a/src/backends/plonky2/mock/mainpod/operation.rs b/src/backends/plonky2/mock/mainpod/operation.rs
index 631407a4..b7ad24d5 100644
--- a/src/backends/plonky2/mock/mainpod/operation.rs
+++ b/src/backends/plonky2/mock/mainpod/operation.rs
@@ -1,6 +1,9 @@
 use super::Statement;
-use crate::middleware::{self, OperationType, Params, ToFields, F};
-use anyhow::Result;
+use crate::{
+    backends::plonky2::primitives::merkletree::MerkleProof,
+    middleware::{self, OperationType, Params, ToFields, F},
+};
+use anyhow::{anyhow, Result};
 use plonky2::field::types::{Field, PrimeField64};
 use serde::{Deserialize, Serialize};
 use std::fmt;
@@ -28,7 +31,13 @@ impl OperationArg {
 }
 
 #[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
-pub struct Operation(pub OperationType, pub Vec<OperationArg>);
+pub enum OperationAux {
+    None,
+    MerkleProofIndex(usize),
+}
+
+#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
+pub struct Operation(pub OperationType, pub Vec<OperationArg>, pub OperationAux);
 
 impl Operation {
     pub fn op_type(&self) -> OperationType {
@@ -37,7 +46,11 @@ impl Operation {
     pub fn args(&self) -> &[OperationArg] {
         &self.1
     }
-    pub fn deref(&self, statements: &[Statement]) -> Result<crate::middleware::Operation> {
+    pub fn deref(
+        &self,
+        statements: &[Statement],
+        merkle_proofs: &[MerkleProof],
+    ) -> Result<crate::middleware::Operation> {
         let deref_args = self
             .1
             .iter()
@@ -45,8 +58,16 @@ impl Operation {
                 OperationArg::None => None,
                 OperationArg::Index(i) => Some(statements[*i].clone().try_into()),
             })
-            .collect::<Result<Vec<crate::middleware::Statement>>>()?;
-        middleware::Operation::op(self.0.clone(), &deref_args)
+            .collect::<Result<Vec<_>>>()?;
+        let deref_aux = match self.2 {
+            OperationAux::None => Ok(crate::middleware::OperationAux::None),
+            OperationAux::MerkleProofIndex(i) => merkle_proofs
+                .get(i)
+                .cloned()
+                .ok_or(anyhow!("Missing Merkle proof index {}", i))
+                .map(crate::middleware::OperationAux::MerkleProof),
+        }?;
+        middleware::Operation::op(self.0.clone(), &deref_args, &deref_aux)
     }
 }
 
@@ -64,6 +85,10 @@ impl fmt::Display for Operation {
                 }
             }
         }
+        match self.2 {
+            OperationAux::None => (),
+            OperationAux::MerkleProofIndex(i) => write!(f, "merkle_proof_{:02}", i)?,
+        }
         Ok(())
     }
 }
diff --git a/src/backends/plonky2/mock/mainpod/statement.rs b/src/backends/plonky2/mock/mainpod/statement.rs
index cb0dd6ae..bdbf1f2c 100644
--- a/src/backends/plonky2/mock/mainpod/statement.rs
+++ b/src/backends/plonky2/mock/mainpod/statement.rs
@@ -60,8 +60,8 @@ impl TryFrom<Statement> for middleware::Statement {
                 }
                 (NP::Gt, (Some(SA::Key(ak1)), Some(SA::Key(ak2)), None), 2) => S::Gt(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)), None), 2) => {
-                    S::Contains(ak1, ak2)
+                (NP::Contains, (Some(SA::Key(ak1)), Some(SA::Key(ak2)), Some(SA::Key(ak3))), 3) => {
+                    S::Contains(ak1, ak2, ak3)
                 }
                 (NP::NotContains, (Some(SA::Key(ak1)), Some(SA::Key(ak2)), None), 2) => {
                     S::NotContains(ak1, ak2)
diff --git a/src/backends/plonky2/primitives/merkletree.rs b/src/backends/plonky2/primitives/merkletree.rs
index 84dcf4c4..c98729af 100644
--- a/src/backends/plonky2/primitives/merkletree.rs
+++ b/src/backends/plonky2/primitives/merkletree.rs
@@ -2,6 +2,7 @@
 //! https://0xparc.github.io/pod2/merkletree.html .
 use anyhow::{anyhow, Result};
 use plonky2::field::types::Field;
+use serde::{Deserialize, Serialize};
 use std::collections::HashMap;
 use std::fmt;
 use std::iter::IntoIterator;
@@ -207,7 +208,7 @@ impl fmt::Display for MerkleTree {
     }
 }
 
-#[derive(Clone, Debug)]
+#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
 pub struct MerkleProof {
     // note: currently we don't use the `_existence` field, we would use if we merge the methods
     // `verify` and `verify_nonexistence` into a single one
diff --git a/src/examples/mod.rs b/src/examples/mod.rs
index d6685147..b52ad356 100644
--- a/src/examples/mod.rs
+++ b/src/examples/mod.rs
@@ -17,6 +17,7 @@ use crate::op;
 
 pub fn zu_kyc_sign_pod_builders(
     params: &Params,
+    sanction_set: &Value,
 ) -> (SignedPodBuilder, SignedPodBuilder, SignedPodBuilder) {
     let mut gov_id = SignedPodBuilder::new(params);
     gov_id.insert("idNumber", "4242424242");
@@ -44,17 +45,27 @@ pub fn zu_kyc_pod_builder(
     pay_stub: &SignedPod,
     sanction_list: &SignedPod,
 ) -> Result<MainPodBuilder> {
+    let sanction_set = match sanction_list.kvs.get("sanctionList") {
+        Some(Value::Set(s)) => Ok(s),
+        _ => Err(anyhow!("Missing sanction list!")),
+    }?;
     let now_minus_18y: i64 = 1169909388;
     let now_minus_1y: i64 = 1706367566;
 
+    let gov_id_kvs = gov_id.kvs();
+    let id_number_value = gov_id_kvs.get(&"idNumber".into()).unwrap();
+
     let mut kyc = MainPodBuilder::new(params);
     kyc.add_signed_pod(gov_id);
     kyc.add_signed_pod(pay_stub);
     kyc.add_signed_pod(sanction_list);
     kyc.pub_op(op!(
-        not_contains,
+        set_not_contains,
         (sanction_list, "sanctionList"),
-        (gov_id, "idNumber")
+        (gov_id, "idNumber"),
+        sanction_set
+            .middleware_set()
+            .prove_nonexistence(id_number_value)?
     ))?;
     kyc.pub_op(op!(lt, (gov_id, "dateOfBirth"), now_minus_18y))?;
     kyc.pub_op(op!(
@@ -251,6 +262,8 @@ pub fn great_boy_pod_builder(
             PodType::MockSigned as i64
         ))?;
         for issuer_idx in 0..2 {
+            let pod_kvs = good_boy_pods[good_boy_idx * 2 + issuer_idx].kvs();
+
             // Type check
             great_boy.pub_op(op!(
                 eq,
@@ -258,10 +271,19 @@ pub fn great_boy_pod_builder(
                 PodType::MockSigned as i64
             ))?;
             // Each good boy POD comes from a valid issuer
+            let good_boy_proof = match good_boy_issuers {
+                Value::Dictionary(dict) => Ok(dict),
+                _ => Err(anyhow!("Invalid good boy issuers!")),
+            }?
+            .middleware_dict()
+            .prove(pod_kvs.get(&KEY_SIGNER.into()).unwrap())?
+            .1;
             great_boy.pub_op(op!(
-                contains,
+                dict_contains,
                 good_boy_issuers,
-                (good_boy_pods[good_boy_idx * 2 + issuer_idx], KEY_SIGNER)
+                (good_boy_pods[good_boy_idx * 2 + issuer_idx], KEY_SIGNER),
+                0,
+                good_boy_proof
             ))?;
             // Each good boy has 2 good boy pods
             great_boy.pub_op(op!(
@@ -338,7 +360,13 @@ pub fn great_boy_pod_full_flow() -> Result<MainPodBuilder> {
     alice_friend_pods.push(friend.sign(&mut bob_signer).unwrap());
     alice_friend_pods.push(friend.sign(&mut charlie_signer).unwrap());
 
-    let good_boy_issuers_dict = Value::Dictionary(Dictionary::new(HashMap::new()).unwrap()); // empty
+    let good_boy_issuers = Value::Dictionary(Dictionary::new(
+        good_boy_issuers
+            .into_iter()
+            .map(|issuer| (issuer.to_string(), 0.into()))
+            .collect(),
+    )?);
+
     great_boy_pod_builder(
         &params,
         [
@@ -348,7 +376,7 @@ pub fn great_boy_pod_full_flow() -> Result<MainPodBuilder> {
             &charlie_good_boys[1],
         ],
         [&alice_friend_pods[0], &alice_friend_pods[1]],
-        &good_boy_issuers_dict,
+        &good_boy_issuers,
         alice,
     )
 }
@@ -372,8 +400,13 @@ pub fn tickets_pod_builder(
     signed_pod: &SignedPod,
     expected_event_id: i64,
     expect_consumed: bool,
-    blacklisted_emails: &Value,
+    blacklisted_emails: &Dictionary,
 ) -> Result<MainPodBuilder> {
+    let attendee_email_value = signed_pod.kvs.get("attendeeEmail").unwrap();
+    let attendee_nin_blacklist_pf = blacklisted_emails
+        .middleware_dict()
+        .prove_nonexistence(&attendee_email_value.into())?;
+    let blacklisted_email_dict_value = Value::Dictionary(blacklisted_emails.clone());
     // Create a main pod referencing this signed pod with some statements
     let mut builder = MainPodBuilder::new(params);
     builder.add_signed_pod(signed_pod);
@@ -381,9 +414,10 @@ pub fn tickets_pod_builder(
     builder.pub_op(op!(eq, (signed_pod, "isConsumed"), expect_consumed))?;
     builder.pub_op(op!(eq, (signed_pod, "isRevoked"), false))?;
     builder.pub_op(op!(
-        not_contains,
-        blacklisted_emails,
-        (signed_pod, "attendeeEmail")
+        dict_not_contains,
+        blacklisted_email_dict_value,
+        (signed_pod, "attendeeEmail"),
+        attendee_nin_blacklist_pf
     ))?;
     Ok(builder)
 }
@@ -397,6 +431,6 @@ pub fn tickets_pod_full_flow() -> Result<MainPodBuilder> {
         &signed_pod,
         123,
         true,
-        &Value::Dictionary(Dictionary::new(HashMap::new()).unwrap()),
+        &Dictionary::new(HashMap::new())?,
     )
 }
diff --git a/src/frontend/containers.rs b/src/frontend/containers.rs
index 956f2130..18edf0e5 100644
--- a/src/frontend/containers.rs
+++ b/src/frontend/containers.rs
@@ -19,7 +19,12 @@ pub struct Set(Vec<Value>, #[serde(skip)] MiddlewareSet);
 
 impl Set {
     pub fn new(values: Vec<Value>) -> Result<Self> {
-        let set = MiddlewareSet::new(&values.iter().map(|v| MiddlewareValue::from(v)).collect())?;
+        let set = MiddlewareSet::new(
+            &values
+                .iter()
+                .map(|v| MiddlewareValue::from(v))
+                .collect::<Vec<_>>(),
+        )?;
         Ok(Self(values, set))
     }
 
@@ -85,8 +90,12 @@ pub struct Array(Vec<Value>, #[serde(skip)] MiddlewareArray);
 
 impl Array {
     pub fn new(values: Vec<Value>) -> Result<Self> {
-        let array =
-            MiddlewareArray::new(&values.iter().map(|v| MiddlewareValue::from(v)).collect())?;
+        let array = MiddlewareArray::new(
+            &values
+                .iter()
+                .map(|v| MiddlewareValue::from(v))
+                .collect::<Vec<_>>(),
+        )?;
         Ok(Self(values, array))
     }
 
diff --git a/src/frontend/mod.rs b/src/frontend/mod.rs
index 109dc1f8..d891a7e9 100644
--- a/src/frontend/mod.rs
+++ b/src/frontend/mod.rs
@@ -3,10 +3,9 @@
 
 use crate::frontend::serialization::*;
 use crate::middleware::{
-    self, hash_str, Hash, MainPodInputs, NativeOperation, NativePredicate, Params, PodId,
-    PodProver, PodSigner, SELF,
+    self, hash_str, Hash, MainPodInputs, Params, PodId, PodProver, PodSigner, SELF,
 };
-use crate::middleware::{OperationType, Predicate, KEY_SIGNER, KEY_TYPE};
+use crate::middleware::{KEY_SIGNER, KEY_TYPE};
 use anyhow::{anyhow, Error, Result};
 use containers::{Array, Dictionary, Set};
 use env_logger;
@@ -18,13 +17,17 @@ use std::collections::HashMap;
 use std::convert::From;
 use std::{fmt, hash as h};
 
+use crate::middleware::{hash_value, OperationAux, EMPTY_VALUE};
+
 pub mod containers;
 mod custom;
 mod operation;
+mod predicate;
 mod serialization;
 mod statement;
 pub use custom::*;
 pub use operation::*;
+pub use predicate::*;
 pub use statement::*;
 
 /// This type is just for presentation purposes.
@@ -122,6 +125,12 @@ impl From<middleware::Value> for Value {
     }
 }
 
+impl From<middleware::Hash> for Value {
+    fn from(v: middleware::Hash) -> Self {
+        Self::Raw(v.into())
+    }
+}
+
 impl TryInto<i64> for Value {
     type Error = Error;
     fn try_into(self) -> std::result::Result<i64, Self::Error> {
@@ -405,9 +414,9 @@ impl MainPodBuilder {
         self.op(false, op)
     }
 
-    fn op(&mut self, public: bool, mut op: Operation) -> Result<Statement> {
+    fn op(&mut self, public: bool, mut op: Operation) -> Result<Statement, anyhow::Error> {
         use NativeOperation::*;
-        let Operation(op_type, ref mut args) = &mut op;
+        let Operation(op_type, ref mut args, _) = &mut op;
         // TODO: argument type checking
         let pred = op_type
             .output_predicate()
@@ -486,8 +495,6 @@ impl MainPodBuilder {
                         return Err(anyhow!("Invalid arguments to lt-to-neq operation"));
                     }
                 },
-                ContainsFromEntries => self.op_args_entries(public, args)?,
-                NotContainsFromEntries => self.op_args_entries(public, args)?,
                 SumOf => match (args[0].clone(), args[1].clone(), args[2].clone()) {
                     (
                         OperationArg::Statement(Statement {
@@ -635,12 +642,17 @@ impl MainPodBuilder {
                         return Err(anyhow!("Invalid arguments to operation"));
                     }
                 },
+                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)?,
             },
             OperationType::Custom(cpr) => {
                 // All args should be statements to be pattern matched against statement templates.
                 let args = args.iter().map(
                     |a| match a {
-                        OperationArg::Statement(s) => middleware::Statement::try_from(s.clone()),
+                        OperationArg::Statement(s) => Ok(middleware::Statement::try_from(s.clone())?),
                             _ => Err(anyhow!("Invalid argument {} to operation corresponding to custom predicate {:?}.", a, cpr))
                     }
                 ).collect::<Result<Vec<_>>>()?;
@@ -712,6 +724,7 @@ impl MainPodBuilder {
             Operation(
                 OperationType::Native(NativeOperation::NewEntry),
                 vec![OperationArg::Entry(k.clone(), v)],
+                OperationAux::None,
             ),
         )
     }
@@ -843,6 +856,13 @@ struct MainPodCompiler {
     // Output
     statements: Vec<middleware::Statement>,
     operations: Vec<middleware::Operation>,
+    // Internal state
+    // Tracks literal constants assigned to ValueOf statements by self.literal()
+    // If `val` has been added as a literal,
+    // then `self.literals.get(&val)` returns `Some(idx)`, and
+    // then `self.statements[idx]` is the ValueOf statement
+    // where it was introduced.
+    literals: HashMap<middleware::Value, usize>,
 }
 
 impl MainPodCompiler {
@@ -851,6 +871,7 @@ impl MainPodCompiler {
             params: params.clone(),
             statements: Vec::new(),
             operations: Vec::new(),
+            literals: HashMap::new(),
         }
     }
 
@@ -876,34 +897,154 @@ impl MainPodCompiler {
         }
     }
 
-    fn compile_st(&self, st: &Statement) -> Result<middleware::Statement> {
+    // Introduces a literal value if it hasn't been introduced,
+    // or else returns the existing ValueOf statement where it was first introduced.
+    // TODO: this might produce duplicate keys, fix
+    fn literal<V: Clone + Into<middleware::Value>>(&mut self, val: V) -> &middleware::Statement {
+        let val: middleware::Value = val.into();
+        match self.literals.get(&val) {
+            Some(idx) => &self.statements[*idx],
+            None => {
+                let ak = middleware::AnchoredKey(SELF, hash_value(&val));
+                let st = middleware::Statement::ValueOf(ak, val);
+                let op = middleware::Operation::NewEntry;
+                self.statements.push(st);
+                self.operations.push(op);
+                self.statements.last().unwrap()
+            }
+        }
+    }
+
+    // Returns the existing ValueOf statement where it was first introduced,
+    // or None if it does not exist.
+    fn get_literal<V: Clone + Into<middleware::Value>>(
+        &self,
+        val: V,
+    ) -> Option<&middleware::Statement> {
+        let val: middleware::Value = val.into();
+        match self.literals.get(&val) {
+            Some(idx) => Some(&self.statements[*idx]),
+            None => None,
+        }
+    }
+
+    // This function handles cases where one frontend statement
+    // compiles to multiple middleware statements.
+    // For example: DictContains(x, y) on the frontend compiles to:
+    // ValueOf(empty, EMPTY_VALUE)
+    // Contains(x, y, empty)
+    fn manual_compile_st_op(&mut self, st: &Statement, op: &Operation) -> Result<()> {
+        match st.predicate {
+            Predicate::Native(NativePredicate::DictContains) => {
+                let empty_st = self.literal(EMPTY_VALUE).clone();
+                let empty_ak = match empty_st {
+                    middleware::Statement::ValueOf(ak, _) => ak,
+                    _ => unreachable!(),
+                };
+                let (ak1, ak2) = match (st.args.get(0).cloned(), st.args.get(1).cloned()) {
+                    (Some(StatementArg::Key(ak1)), Some(StatementArg::Key(ak2))) => (ak1, ak2),
+                    _ => Err(anyhow!("Ill-formed statement: {}", st))?,
+                };
+                let middle_st =
+                    middleware::Statement::Contains(ak1.into(), ak2.into(), empty_ak.clone());
+                let middle_op = middleware::Operation::ContainsFromEntries(
+                    match &op.1[0] {
+                        OperationArg::Statement(s) => self.compile_st(&s)?,
+                        _ => Err(anyhow!("Statement compile failed in manual compile"))?,
+                    },
+                    match &op.1[1] {
+                        OperationArg::Statement(s) => self.compile_st(&s)?,
+                        _ => Err(anyhow!("Statement compile failed in manual compile"))?,
+                    },
+                    empty_st,
+                    match &op.2 {
+                        OperationAux::MerkleProof(mp) => mp.clone(),
+                        _ => {
+                            return Err(anyhow!(
+                                "Auxiliary argument to DictContainsFromEntries must be Merkle proof"
+                            ));
+                        }
+                    },
+                );
+                self.statements.push(middle_st);
+                self.operations.push(middle_op);
+                assert_eq!(self.statements.len(), self.operations.len());
+                Ok(())
+            }
+            _ => unreachable!(),
+        }
+    }
+
+    // If the frontend statement `st` compiles to a single middleware statement,
+    // returns that middleware statement.
+    // If it compiles to multiple middlewarestatements, returns StatementConversionError.
+    // This is only a helper method within compile_st_op().
+    // If you want to compile a statement in general, run compile_st().
+    fn compile_st_try_simple(
+        &self,
+        st: &Statement,
+    ) -> Result<middleware::Statement, StatementConversionError> {
         st.clone().try_into()
     }
 
+    // Compiles the frontend statement `st` to a middleware statement.
+    // This function assumes the middleware statement already exists --
+    // it should not be called from compile_st_op.
+    fn compile_st(&self, st: &Statement) -> Result<middleware::Statement> {
+        match self.compile_st_try_simple(st) {
+            Ok(s) => Ok(s),
+            Err(StatementConversionError::Error(e)) => Err(e),
+            Err(StatementConversionError::MCR(_)) => {
+                let empty_st = self
+                    .get_literal(EMPTY_VALUE)
+                    .clone()
+                    .ok_or(anyhow!("Literal value not found for empty literal."))?;
+                let empty_ak = match empty_st {
+                    middleware::Statement::ValueOf(ak, _) => ak,
+                    _ => unreachable!(),
+                };
+                let (ak1, ak2) = match (st.args.get(0).cloned(), st.args.get(1).cloned()) {
+                    (Some(StatementArg::Key(ak1)), Some(StatementArg::Key(ak2))) => (ak1, ak2),
+                    _ => Err(anyhow!("Ill-formed statement: {}", st))?,
+                };
+                let middle_st =
+                    middleware::Statement::Contains(ak1.into(), ak2.into(), empty_ak.clone());
+                Ok(middle_st)
+            }
+        }
+    }
+
     fn compile_op(&self, op: &Operation) -> Result<middleware::Operation> {
-        // TODO
-        let mop_code: OperationType = op.0.clone();
+        let mop_code: middleware::OperationType = op.0.clone().try_into()?;
+
+        // TODO: Take Merkle proof into account.
         let mop_args =
             op.1.iter()
-                .flat_map(|arg| self.compile_op_arg(arg).map(|s| Ok(s.try_into()?)))
-                .collect::<Result<Vec<middleware::Statement>>>()?;
-        middleware::Operation::op(mop_code, &mop_args)
+                .flat_map(|arg| self.compile_op_arg(arg).map(|op_arg| Ok(op_arg)))
+                .collect::<Result<Vec<_>>>()?;
+        middleware::Operation::op(mop_code, &mop_args, &op.2)
     }
 
     fn compile_st_op(&mut self, st: &Statement, op: &Operation, params: &Params) -> Result<()> {
-        let middle_st = self.compile_st(st)?;
-        let middle_op = self.compile_op(op)?;
-        let is_correct = middle_op.check(params, &middle_st)?;
-        if !is_correct {
-            // todo: improve error handling
-            Err(anyhow!(
-                "Compile failed due to invalid deduction:\n {} ⇏ {}",
-                middle_op,
-                middle_st
-            ))
-        } else {
-            self.push_st_op(middle_st, middle_op);
-            Ok(())
+        let middle_st_res = self.compile_st_try_simple(st);
+        match middle_st_res {
+            Ok(middle_st) => {
+                let middle_op = self.compile_op(op)?;
+                let is_correct = middle_op.check(params, &middle_st)?;
+                if !is_correct {
+                    // todo: improve error handling
+                    Err(anyhow!(
+                        "Compile failed due to invalid deduction:\n {} ⇏ {}",
+                        middle_op,
+                        middle_st
+                    ))
+                } else {
+                    self.push_st_op(middle_st, middle_op);
+                    Ok(())
+                }
+            }
+            Err(StatementConversionError::Error(e)) => Err(e),
+            Err(StatementConversionError::MCR(_)) => self.manual_compile_st_op(st, op),
         }
     }
 
@@ -950,55 +1091,66 @@ pub mod build_utils {
     #[macro_export]
     macro_rules! op {
         (new_entry, ($key:expr, $value:expr)) => { $crate::frontend::Operation(
-            $crate::middleware::OperationType::Native($crate::middleware::NativeOperation::NewEntry),
-            $crate::op_args!(($key, $value))) };
+            $crate::frontend::OperationType::Native($crate::frontend::NativeOperation::NewEntry),
+            $crate::op_args!(($key, $value)), crate::middleware::OperationAux::None) };
         (eq, $($arg:expr),+) => { $crate::frontend::Operation(
-            $crate::middleware::OperationType::Native($crate::middleware::NativeOperation::EqualFromEntries),
-            $crate::op_args!($($arg),*)) };
+            $crate::frontend::OperationType::Native($crate::frontend::NativeOperation::EqualFromEntries),
+            $crate::op_args!($($arg),*), crate::middleware::OperationAux::None) };
         (ne, $($arg:expr),+) => { $crate::frontend::Operation(
-            $crate::middleware::OperationType::Native($crate::middleware::NativeOperation::NotEqualFromEntries),
-            $crate::op_args!($($arg),*)) };
+            $crate::frontend::OperationType::Native($crate::frontend::NativeOperation::NotEqualFromEntries),
+            $crate::op_args!($($arg),*), crate::middleware::OperationAux::None) };
         (gt, $($arg:expr),+) => { crate::frontend::Operation(
-            crate::middleware::OperationType::Native(crate::middleware::NativeOperation::GtFromEntries),
-            crate::op_args!($($arg),*)) };
+            crate::frontend::OperationType::Native(crate::frontend::NativeOperation::GtFromEntries),
+            crate::op_args!($($arg),*), crate::middleware::OperationAux::None) };
         (lt, $($arg:expr),+) => { crate::frontend::Operation(
-            crate::middleware::OperationType::Native(crate::middleware::NativeOperation::LtFromEntries),
-            crate::op_args!($($arg),*)) };
+            crate::frontend::OperationType::Native(crate::frontend::NativeOperation::LtFromEntries),
+            crate::op_args!($($arg),*), crate::middleware::OperationAux::None) };
         (transitive_eq, $($arg:expr),+) => { crate::frontend::Operation(
-            crate::middleware::OperationType::Native(crate::middleware::NativeOperation::TransitiveEqualFromStatements),
-            crate::op_args!($($arg),*)) };
+            crate::frontend::OperationType::Native(crate::frontend::NativeOperation::TransitiveEqualFromStatements),
+            crate::op_args!($($arg),*), crate::middleware::OperationAux::None) };
         (gt_to_ne, $($arg:expr),+) => { crate::frontend::Operation(
-            crate::middleware::OperationType::Native(crate::middleware::NativeOperation::GtToNotEqual),
-            crate::op_args!($($arg),*)) };
+            crate::frontend::OperationType::Native(crate::frontend::NativeOperation::GtToNotEqual),
+            crate::op_args!($($arg),*), crate::middleware::OperationAux::None) };
         (lt_to_ne, $($arg:expr),+) => { crate::frontend::Operation(
-            crate::middleware::OperationType::Native(crate::middleware::NativeOperation::LtToNotEqual),
-            crate::op_args!($($arg),*)) };
-        (contains, $($arg:expr),+) => { crate::frontend::Operation(
-            crate::middleware::OperationType::Native(crate::middleware::NativeOperation::ContainsFromEntries),
-            crate::op_args!($($arg),*)) };
-        (not_contains, $($arg:expr),+) => { crate::frontend::Operation(
-            crate::middleware::OperationType::Native(crate::middleware::NativeOperation::NotContainsFromEntries),
-            crate::op_args!($($arg),*)) };
+            crate::frontend::OperationType::Native(crate::frontend::NativeOperation::LtToNotEqual),
+            crate::op_args!($($arg),*), crate::middleware::OperationAux::None) };
         (sum_of, $($arg:expr),+) => { crate::frontend::Operation(
-            crate::middleware::OperationType::Native(crate::middleware::NativeOperation::SumOf),
-            crate::op_args!($($arg),*)) };
+            crate::frontend::OperationType::Native(crate::frontend::NativeOperation::SumOf),
+            crate::op_args!($($arg),*), crate::middleware::OperationAux::None) };
         (product_of, $($arg:expr),+) => { crate::frontend::Operation(
-            crate::middleware::OperationType::Native(crate::middleware::NativeOperation::ProductOf),
-            crate::op_args!($($arg),*)) };
+            crate::frontend::OperationType::Native(crate::frontend::NativeOperation::ProductOf),
+            crate::op_args!($($arg),*), crate::middleware::OperationAux::None) };
         (max_of, $($arg:expr),+) => { crate::frontend::Operation(
-            crate::middleware::OperationType::Native(crate::middleware::NativeOperation::MaxOf),
-            crate::op_args!($($arg),*)) };
+            crate::frontend::OperationType::Native(crate::frontend::NativeOperation::MaxOf),
+            crate::op_args!($($arg),*), crate::middleware::OperationAux::None) };
         (custom, $op:expr, $($arg:expr),+) => { $crate::frontend::Operation(
-            $crate::middleware::OperationType::Custom($op),
-            $crate::op_args!($($arg),*)) };
+            $crate::frontend::OperationType::Custom($op),
+            $crate::op_args!($($arg),*), crate::middleware::OperationAux::None) };
+        (dict_contains, $dict:expr, $key:expr, $value:expr, $aux:expr) => { crate::frontend::Operation(
+            crate::frontend::OperationType::Native(crate::frontend::NativeOperation::DictContainsFromEntries),
+            crate::op_args!($dict, $key, $value), crate::middleware::OperationAux::MerkleProof($aux)) };
+        (dict_not_contains, $dict:expr, $key:expr, $aux:expr) => { crate::frontend::Operation(
+            crate::frontend::OperationType::Native(crate::frontend::NativeOperation::DictNotContainsFromEntries),
+            crate::op_args!($dict, $key), crate::middleware::OperationAux::MerkleProof($aux)) };
+        (set_contains, $set:expr, $value:expr, $aux:expr) => { crate::frontend::Operation(
+            crate::frontend::OperationType::Native(crate::frontend::NativeOperation::SetContainsFromEntries),
+            crate::op_args!($set, $value), crate::middleware::OperationAux::MerkleProof($aux)) };
+        (set_not_contains, $set:expr, $value:expr, $aux:expr) => { crate::frontend::Operation(
+            crate::frontend::OperationType::Native(crate::frontend::NativeOperation::SetNotContainsFromEntries),
+            crate::op_args!($set, $value), crate::middleware::OperationAux::MerkleProof($aux)) };
+        (array_contains, $array:expr, $value:expr, $aux:expr) => { crate::frontend::Operation(
+            crate::frontend::OperationType::Native(crate::frontend::NativeOperation::ArrayContainsFromEntries),
+            crate::op_args!($array, $value), crate::middleware::OperationAux::MerkleProof($aux)) };
     }
 }
 
 #[cfg(test)]
 pub mod tests {
     use super::*;
+    use crate::backends::plonky2::basetypes;
     use crate::backends::plonky2::mock::mainpod::MockProver;
     use crate::backends::plonky2::mock::signedpod::MockSigner;
+    use crate::backends::plonky2::primitives::merkletree::MerkleTree;
     use crate::examples::{
         eth_dos_pod_builder, eth_friend_signed_pod_builder, great_boy_pod_full_flow,
         tickets_pod_full_flow, zu_kyc_pod_builder, zu_kyc_sign_pod_builders,
@@ -1007,8 +1159,12 @@ pub mod tests {
     // Check that frontend public statements agree with those
     // embedded in a MainPod.
     fn check_public_statements(pod: &MainPod) -> Result<()> {
-        std::iter::zip(pod.public_statements.clone(), pod.pod.pub_statements()).try_for_each(
-            |(fes, s)| crate::middleware::Statement::try_from(fes).map(|fes| assert_eq!(fes, s)),
+        Ok(
+            std::iter::zip(pod.public_statements.clone(), pod.pod.pub_statements()).try_for_each(
+                |(fes, s)| {
+                    crate::middleware::Statement::try_from(fes).map(|fes| assert_eq!(fes, s))
+                },
+            )?,
         )
     }
 
@@ -1041,7 +1197,9 @@ pub mod tests {
     #[test]
     fn test_front_zu_kyc() -> Result<()> {
         let params = Params::default();
-        let (gov_id, pay_stub, sanction_list) = zu_kyc_sign_pod_builders(&params);
+        let sanctions_values = vec!["A343434340".into()];
+        let sanction_set = Value::Set(Set::new(sanctions_values)?);
+        let (gov_id, pay_stub, sanction_list) = zu_kyc_sign_pod_builders(&params, &sanction_set);
 
         println!("{}", gov_id);
         println!("{}", pay_stub);
@@ -1164,6 +1322,7 @@ pub mod tests {
                 OperationArg::from((&signed_pod, "a")),
                 OperationArg::from((&signed_pod, "b")),
             ],
+            OperationAux::None,
         );
         let st1 = builder.op(true, op_eq1).unwrap();
         let op_eq2 = Operation(
@@ -1172,12 +1331,14 @@ pub mod tests {
                 OperationArg::from((&signed_pod, "b")),
                 OperationArg::from((&signed_pod, "a")),
             ],
+            OperationAux::None,
         );
         let st2 = builder.op(true, op_eq2).unwrap();
 
         let op_eq3 = Operation(
             OperationType::Native(NativeOperation::TransitiveEqualFromStatements),
             vec![OperationArg::Statement(st1), OperationArg::Statement(st2)],
+            OperationAux::None,
         );
         let st3 = builder.op(true, op_eq3);
 
@@ -1214,6 +1375,58 @@ pub mod tests {
     }
 
     #[test]
+    fn test_dictionaries() -> Result<()> {
+        let params = Params::default();
+        let mut builder = SignedPodBuilder::new(&params);
+
+        type BeValue = basetypes::Value;
+        let mut my_dict_kvs: HashMap<String, Value> = HashMap::new();
+        my_dict_kvs.insert("a".to_string(), Value::from(1));
+        my_dict_kvs.insert("b".to_string(), Value::from(2));
+        my_dict_kvs.insert("c".to_string(), Value::from(3));
+        //        let my_dict_as_mt = MerkleTree::new(5, &my_dict_kvs).unwrap();
+        //        let dict = Dictionary { mt: my_dict_as_mt };
+        let dict = Dictionary::new(my_dict_kvs)?;
+        let dict_root = Value::Dictionary(dict.clone());
+        builder.insert("dict", dict_root);
+
+        let mut signer = MockSigner {
+            pk: "signer".into(),
+        };
+        let pod = builder.sign(&mut signer).unwrap();
+
+        let mut builder = MainPodBuilder::new(&params);
+        builder.add_signed_pod(&pod);
+        let st0 = Statement::from((&pod, "dict"));
+        let st1 = builder.op(true, op!(new_entry, ("key", "a"))).unwrap();
+        let st2 = builder.literal(false, &Value::Int(1)).unwrap();
+
+        builder
+            .pub_op(Operation(
+                // OperationType
+                OperationType::Native(NativeOperation::DictContainsFromEntries),
+                // Vec<OperationArg>
+                vec![
+                    OperationArg::Statement(st0),
+                    OperationArg::Statement(st1),
+                    OperationArg::Statement(st2),
+                ],
+                OperationAux::MerkleProof(
+                    dict.middleware_dict()
+                        .prove(&Hash::from("a").into())
+                        .unwrap()
+                        .1,
+                ),
+            ))
+            .unwrap();
+        let mut main_prover = MockProver {};
+        let main_pod = builder.prove(&mut main_prover, &params).unwrap();
+
+        println!("{}", main_pod);
+
+        Ok(())
+    }
+
     #[should_panic]
     fn test_incorrect_pod() {
         // try to insert the same key multiple times
@@ -1234,7 +1447,11 @@ pub mod tests {
                     StatementArg::Literal(Value::Int(3)),
                 ],
             ),
-            Operation(OperationType::Native(NativeOperation::NewEntry), vec![]),
+            Operation(
+                OperationType::Native(NativeOperation::NewEntry),
+                vec![],
+                OperationAux::None,
+            ),
         ));
         builder.insert((
             Statement::new(
@@ -1247,7 +1464,11 @@ pub mod tests {
                     StatementArg::Literal(Value::Int(28)),
                 ],
             ),
-            Operation(OperationType::Native(NativeOperation::NewEntry), vec![]),
+            Operation(
+                OperationType::Native(NativeOperation::NewEntry),
+                vec![],
+                OperationAux::None,
+            ),
         ));
 
         let mut prover = MockProver {};
@@ -1283,11 +1504,19 @@ pub mod tests {
 
         builder.insert((
             value_of_a.clone(),
-            Operation(OperationType::Native(NativeOperation::NewEntry), vec![]),
+            Operation(
+                OperationType::Native(NativeOperation::NewEntry),
+                vec![],
+                OperationAux::None,
+            ),
         ));
         builder.insert((
             value_of_b.clone(),
-            Operation(OperationType::Native(NativeOperation::NewEntry), vec![]),
+            Operation(
+                OperationType::Native(NativeOperation::NewEntry),
+                vec![],
+                OperationAux::None,
+            ),
         ));
         builder.insert((
             Statement::new(
@@ -1300,6 +1529,7 @@ pub mod tests {
                     OperationArg::Statement(value_of_a),
                     OperationArg::Statement(value_of_b),
                 ],
+                OperationAux::None,
             ),
         ));
 
diff --git a/src/frontend/operation.rs b/src/frontend/operation.rs
index 9c0ace23..9a6be7a9 100644
--- a/src/frontend/operation.rs
+++ b/src/frontend/operation.rs
@@ -1,7 +1,10 @@
 use std::fmt;
 
-use super::{SignedPod, Statement, Value};
-use crate::middleware::OperationType;
+use super::{NativePredicate, Predicate, SignedPod, Statement, Value};
+use crate::{
+    backends::plonky2::primitives::merkletree::MerkleProof,
+    middleware::{self, OperationAux},
+};
 
 #[derive(Clone, Debug, PartialEq, Eq)]
 pub enum OperationArg {
@@ -69,7 +72,120 @@ impl<V: Into<Value>> From<(&str, V)> for OperationArg {
 }
 
 #[derive(Clone, Debug, PartialEq, Eq)]
-pub struct Operation(pub OperationType, pub Vec<OperationArg>);
+pub enum OperationType {
+    Native(NativeOperation),
+    Custom(middleware::CustomPredicateRef),
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub enum NativeOperation {
+    None = 0,
+    NewEntry = 1,
+    CopyStatement = 2,
+    EqualFromEntries = 3,
+    NotEqualFromEntries = 4,
+    GtFromEntries = 5,
+    LtFromEntries = 6,
+    TransitiveEqualFromStatements = 7,
+    GtToNotEqual = 8,
+    LtToNotEqual = 9,
+    SumOf = 13,
+    ProductOf = 14,
+    MaxOf = 15,
+    DictContainsFromEntries = 16,
+    DictNotContainsFromEntries = 17,
+    SetContainsFromEntries = 18,
+    SetNotContainsFromEntries = 19,
+    ArrayContainsFromEntries = 20,
+}
+
+impl TryFrom<OperationType> for middleware::OperationType {
+    type Error = anyhow::Error;
+    fn try_from(fe_ot: OperationType) -> Result<Self, Self::Error> {
+        type FeOT = OperationType;
+        type FeNO = NativeOperation;
+        type MwOT = middleware::OperationType;
+        type MwNO = middleware::NativeOperation;
+        let mw_ot = match fe_ot {
+            FeOT::Native(FeNO::None) => MwOT::Native(MwNO::None),
+            FeOT::Native(FeNO::NewEntry) => MwOT::Native(MwNO::NewEntry),
+            FeOT::Native(FeNO::CopyStatement) => MwOT::Native(MwNO::CopyStatement),
+            FeOT::Native(FeNO::EqualFromEntries) => MwOT::Native(MwNO::EqualFromEntries),
+            FeOT::Native(FeNO::NotEqualFromEntries) => MwOT::Native(MwNO::NotEqualFromEntries),
+            FeOT::Native(FeNO::GtFromEntries) => MwOT::Native(MwNO::GtFromEntries),
+            FeOT::Native(FeNO::LtFromEntries) => MwOT::Native(MwNO::LtFromEntries),
+            FeOT::Native(FeNO::TransitiveEqualFromStatements) => {
+                MwOT::Native(MwNO::TransitiveEqualFromStatements)
+            }
+            FeOT::Native(FeNO::GtToNotEqual) => MwOT::Native(MwNO::GtToNotEqual),
+            FeOT::Native(FeNO::LtToNotEqual) => MwOT::Native(MwNO::LtToNotEqual),
+            FeOT::Native(FeNO::SumOf) => MwOT::Native(MwNO::SumOf),
+            FeOT::Native(FeNO::ProductOf) => MwOT::Native(MwNO::ProductOf),
+            FeOT::Native(FeNO::MaxOf) => MwOT::Native(MwNO::MaxOf),
+            FeOT::Native(FeNO::DictContainsFromEntries) => MwOT::Native(MwNO::ContainsFromEntries),
+            FeOT::Native(FeNO::DictNotContainsFromEntries) => {
+                MwOT::Native(MwNO::NotContainsFromEntries)
+            }
+            FeOT::Native(FeNO::SetContainsFromEntries) => MwOT::Native(MwNO::ContainsFromEntries),
+            FeOT::Native(FeNO::SetNotContainsFromEntries) => {
+                MwOT::Native(MwNO::NotContainsFromEntries)
+            }
+            FeOT::Native(FeNO::ArrayContainsFromEntries) => MwOT::Native(MwNO::ContainsFromEntries),
+            FeOT::Custom(mw_cpr) => MwOT::Custom(mw_cpr),
+        };
+        Ok(mw_ot)
+    }
+}
+
+impl OperationType {
+    /// Gives the type of predicate that the operation will output, if known.
+    /// CopyStatement may output any predicate (it will match the statement copied),
+    /// so output_predicate returns None on CopyStatement.
+    pub fn output_predicate(&self) -> Option<Predicate> {
+        match self {
+            OperationType::Native(native_op) => match native_op {
+                NativeOperation::None => Some(Predicate::Native(NativePredicate::None)),
+                NativeOperation::NewEntry => Some(Predicate::Native(NativePredicate::ValueOf)),
+                NativeOperation::CopyStatement => None,
+                NativeOperation::EqualFromEntries => {
+                    Some(Predicate::Native(NativePredicate::Equal))
+                }
+                NativeOperation::NotEqualFromEntries => {
+                    Some(Predicate::Native(NativePredicate::NotEqual))
+                }
+                NativeOperation::GtFromEntries => Some(Predicate::Native(NativePredicate::Gt)),
+                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::SumOf => Some(Predicate::Native(NativePredicate::SumOf)),
+                NativeOperation::ProductOf => Some(Predicate::Native(NativePredicate::ProductOf)),
+                NativeOperation::MaxOf => Some(Predicate::Native(NativePredicate::MaxOf)),
+                NativeOperation::DictContainsFromEntries => {
+                    Some(Predicate::Native(NativePredicate::DictContains))
+                }
+                NativeOperation::DictNotContainsFromEntries => {
+                    Some(Predicate::Native(NativePredicate::DictNotContains))
+                }
+                NativeOperation::SetContainsFromEntries => {
+                    Some(Predicate::Native(NativePredicate::SetContains))
+                }
+                NativeOperation::SetNotContainsFromEntries => {
+                    Some(Predicate::Native(NativePredicate::SetNotContains))
+                }
+                NativeOperation::ArrayContainsFromEntries => {
+                    Some(Predicate::Native(NativePredicate::ArrayContains))
+                }
+            },
+            OperationType::Custom(cpr) => Some(Predicate::Custom(cpr.clone())),
+        }
+    }
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct Operation(pub OperationType, pub Vec<OperationArg>, pub OperationAux);
 
 impl fmt::Display for Operation {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
diff --git a/src/frontend/predicate.rs b/src/frontend/predicate.rs
new file mode 100644
index 00000000..58a774bd
--- /dev/null
+++ b/src/frontend/predicate.rs
@@ -0,0 +1,39 @@
+use anyhow::{anyhow, Result};
+use schemars::JsonSchema;
+use serde::{Deserialize, Serialize};
+use std::fmt;
+
+use super::{AnchoredKey, SignedPod, Value};
+//use crate::middleware::{self, NativePredicate, Predicate};
+use crate::middleware::{self, CustomPredicateRef};
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Serialize, Deserialize, JsonSchema)]
+pub enum NativePredicate {
+    None = 0,
+    ValueOf = 1,
+    Equal = 2,
+    NotEqual = 3,
+    Gt = 4,
+    Lt = 5,
+    SumOf = 8,
+    ProductOf = 9,
+    MaxOf = 10,
+    DictContains = 11,
+    DictNotContains = 12,
+    SetContains = 13,
+    SetNotContains = 14,
+    ArrayContains = 15, // there is no ArrayNotContains
+}
+
+#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, JsonSchema)]
+pub enum Predicate {
+    Native(NativePredicate),
+    BatchSelf(usize),
+    Custom(CustomPredicateRef),
+}
+
+impl From<NativePredicate> for Predicate {
+    fn from(v: NativePredicate) -> Self {
+        Self::Native(v)
+    }
+}
diff --git a/src/frontend/serialization.rs b/src/frontend/serialization.rs
index 036f3fe0..199a67ef 100644
--- a/src/frontend/serialization.rs
+++ b/src/frontend/serialization.rs
@@ -151,6 +151,8 @@ pub fn transform_value_schema(schema: &mut Schema) {
 
 #[cfg(test)]
 mod tests {
+    use anyhow::Result;
+
     use crate::{
         backends::plonky2::mock::{mainpod::MockProver, signedpod::MockSigner},
         examples::{zu_kyc_pod_builder, zu_kyc_sign_pod_builders},
@@ -260,11 +262,13 @@ mod tests {
     }
 
     #[test]
-    fn test_main_pod_serialization() {
+    fn test_main_pod_serialization() -> Result<()> {
         let params = middleware::Params::default();
+        let sanctions_values = vec!["A343434340".into()];
+        let sanction_set = Value::Set(Set::new(sanctions_values)?);
 
         let (gov_id_builder, pay_stub_builder, sanction_list_builder) =
-            zu_kyc_sign_pod_builders(&params);
+            zu_kyc_sign_pod_builders(&params, &sanction_set);
         let mut signer = MockSigner {
             pk: "ZooGov".into(),
         };
@@ -289,9 +293,8 @@ mod tests {
 
         assert_eq!(kyc_pod.public_statements, deserialized.public_statements);
         assert_eq!(kyc_pod.pod.id(), deserialized.pod.id());
-        assert_eq!(
-            kyc_pod.pod.verify().is_ok(),
-            deserialized.pod.verify().is_ok()
-        );
+        assert_eq!(kyc_pod.pod.verify()?, deserialized.pod.verify()?);
+
+        Ok(())
     }
 }
diff --git a/src/frontend/statement.rs b/src/frontend/statement.rs
index dcdf848c..8b7858ca 100644
--- a/src/frontend/statement.rs
+++ b/src/frontend/statement.rs
@@ -1,5 +1,5 @@
-use super::{AnchoredKey, SignedPod, Value};
-use crate::middleware::{self, NativePredicate, Predicate};
+use super::{AnchoredKey, NativePredicate, Predicate, SignedPod, Value};
+use crate::middleware;
 use anyhow::{anyhow, Result};
 use schemars::JsonSchema;
 use serde::{Deserialize, Serialize};
@@ -50,9 +50,35 @@ impl From<(&SignedPod, &str)> for Statement {
     }
 }
 
+#[derive(Debug)]
+pub struct ManualConversionRequired();
+
+impl std::fmt::Display for StatementConversionError {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(
+            f,
+            "Statement conversion error: statement conversion must be implemented manually."
+        )
+    }
+}
+
+impl std::error::Error for StatementConversionError {}
+
+#[derive(Debug)]
+pub enum StatementConversionError {
+    MCR(ManualConversionRequired),
+    Error(anyhow::Error),
+}
+
+impl From<anyhow::Error> for StatementConversionError {
+    fn from(value: anyhow::Error) -> Self {
+        Self::Error(value)
+    }
+}
+
 impl TryFrom<Statement> for middleware::Statement {
-    type Error = anyhow::Error;
-    fn try_from(s: Statement) -> Result<Self> {
+    type Error = StatementConversionError;
+    fn try_from(s: Statement) -> Result<Self, StatementConversionError> {
         type MS = middleware::Statement;
         type NP = NativePredicate;
         type SA = StatementArg;
@@ -79,12 +105,6 @@ impl TryFrom<Statement> for middleware::Statement {
                 (NP::Lt, (Some(SA::Key(ak1)), Some(SA::Key(ak2)), None)) => {
                     MS::Lt(ak1.into(), ak2.into())
                 }
-                (NP::Contains, (Some(SA::Key(ak1)), Some(SA::Key(ak2)), None)) => {
-                    MS::Contains(ak1.into(), ak2.into())
-                }
-                (NP::NotContains, (Some(SA::Key(ak1)), Some(SA::Key(ak2)), None)) => {
-                    MS::NotContains(ak1.into(), ak2.into())
-                }
                 (NP::SumOf, (Some(SA::Key(ak1)), Some(SA::Key(ak2)), Some(SA::Key(ak3)))) => {
                     MS::SumOf(ak1.into(), ak2.into(), ak3.into())
                 }
@@ -94,6 +114,19 @@ impl TryFrom<Statement> for middleware::Statement {
                 (NP::MaxOf, (Some(SA::Key(ak1)), Some(SA::Key(ak2)), Some(SA::Key(ak3)))) => {
                     MS::MaxOf(ak1.into(), ak2.into(), ak3.into())
                 }
+                (
+                    NP::DictContains,
+                    (Some(SA::Key(ak1)), Some(SA::Key(ak2)), Some(SA::Key(ak3))),
+                ) => MS::Contains(ak1.into(), ak2.into(), ak3.into()),
+                (NP::DictNotContains, (Some(SA::Key(ak1)), Some(SA::Key(ak2)), None)) => {
+                    MS::NotContains(ak1.into(), ak2.into())
+                }
+                (NP::SetContains, (Some(SA::Key(ak1)), Some(SA::Key(ak2)), None)) => {
+                    return Err(StatementConversionError::MCR(ManualConversionRequired()));
+                }
+                (NP::SetNotContains, (Some(SA::Key(ak1)), Some(SA::Key(ak2)), None)) => {
+                    MS::NotContains(ak1.into(), ak2.into())
+                }
                 _ => Err(anyhow!("Ill-formed statement: {}", s))?,
             },
             Predicate::Custom(cpr) => MS::Custom(
diff --git a/src/middleware/containers.rs b/src/middleware/containers.rs
index 11b58b09..b28d111e 100644
--- a/src/middleware/containers.rs
+++ b/src/middleware/containers.rs
@@ -73,7 +73,7 @@ pub struct Set {
 }
 
 impl Set {
-    pub fn new(set: &Vec<Value>) -> Result<Self> {
+    pub fn new(set: &[Value]) -> Result<Self> {
         let kvs: HashMap<Value, Value> = set
             .iter()
             .map(|e| {
@@ -126,7 +126,7 @@ pub struct Array {
 }
 
 impl Array {
-    pub fn new(array: &Vec<Value>) -> Result<Self> {
+    pub fn new(array: &[Value]) -> Result<Self> {
         let kvs: HashMap<Value, Value> = array
             .iter()
             .enumerate()
diff --git a/src/middleware/operation.rs b/src/middleware/operation.rs
index 52d3e1ca..669de0d7 100644
--- a/src/middleware/operation.rs
+++ b/src/middleware/operation.rs
@@ -6,7 +6,10 @@ use std::fmt;
 use std::iter;
 
 use super::{CustomPredicateRef, NativePredicate, Statement, StatementArg, ToFields, F};
-use crate::middleware::{AnchoredKey, Params, Predicate, Value, SELF};
+use crate::{
+    backends::plonky2::primitives::merkletree::{MerkleProof, MerkleTree},
+    middleware::{AnchoredKey, Params, Predicate, Value, SELF},
+};
 
 #[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
 pub enum OperationType {
@@ -14,6 +17,22 @@ pub enum OperationType {
     Custom(CustomPredicateRef),
 }
 
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub enum OperationAux {
+    None,
+    MerkleProof(MerkleProof),
+}
+
+impl fmt::Display for OperationAux {
+    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        match self {
+            Self::None => write!(f, "<no aux>")?,
+            Self::MerkleProof(pf) => write!(f, "merkle_proof({})", pf)?,
+        }
+        Ok(())
+    }
+}
+
 impl ToFields for OperationType {
     fn to_fields(&self, params: &Params) -> Vec<F> {
         let mut fields: Vec<F> = match self {
@@ -106,8 +125,17 @@ pub enum Operation {
     TransitiveEqualFromStatements(Statement, Statement),
     GtToNotEqual(Statement),
     LtToNotEqual(Statement),
-    ContainsFromEntries(Statement, Statement),
-    NotContainsFromEntries(Statement, Statement),
+    ContainsFromEntries(
+        /* root  */ Statement,
+        /* key   */ Statement,
+        /* value */ Statement,
+        /* proof */ MerkleProof,
+    ),
+    NotContainsFromEntries(
+        /* root  */ Statement,
+        /* key   */ Statement,
+        /* proof */ MerkleProof,
+    ),
     SumOf(Statement, Statement, Statement),
     ProductOf(Statement, Statement, Statement),
     MaxOf(Statement, Statement, Statement),
@@ -129,8 +157,8 @@ impl Operation {
             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),
+            Self::ContainsFromEntries(_, _, _, _) => OT::Native(ContainsFromEntries),
+            Self::NotContainsFromEntries(_, _, _) => OT::Native(NotContainsFromEntries),
             Self::SumOf(_, _, _) => OT::Native(SumOf),
             Self::ProductOf(_, _, _) => OT::Native(ProductOf),
             Self::MaxOf(_, _, _) => OT::Native(MaxOf),
@@ -150,16 +178,27 @@ impl Operation {
             Self::TransitiveEqualFromStatements(s1, s2) => vec![s1, s2],
             Self::GtToNotEqual(s) => vec![s],
             Self::LtToNotEqual(s) => vec![s],
-            Self::ContainsFromEntries(s1, s2) => vec![s1, s2],
-            Self::NotContainsFromEntries(s1, s2) => vec![s1, s2],
+            Self::ContainsFromEntries(s1, s2, s3, pf) => vec![s1, s2, s3],
+            Self::NotContainsFromEntries(s1, s2, pf) => vec![s1, s2],
             Self::SumOf(s1, s2, s3) => vec![s1, s2, s3],
             Self::ProductOf(s1, s2, s3) => vec![s1, s2, s3],
             Self::MaxOf(s1, s2, s3) => vec![s1, s2, s3],
             Self::Custom(_, args) => args,
         }
     }
+
+    /// Extracts auxiliary data from operation.
+    pub fn aux(&self) -> OperationAux {
+        match self {
+            Self::ContainsFromEntries(_, _, _, mp) => OperationAux::MerkleProof(mp.clone()),
+            Self::NotContainsFromEntries(_, _, mp) => OperationAux::MerkleProof(mp.clone()),
+            _ => OperationAux::None,
+        }
+    }
+
     /// Forms operation from op-code and arguments.
-    pub fn op(op_code: OperationType, args: &[Statement]) -> Result<Self> {
+    pub fn op(op_code: OperationType, args: &[Statement], aux: &OperationAux) -> Result<Self> {
+        type OA = OperationAux;
         type NO = NativeOperation;
         let arg_tup = (
             args.first().cloned(),
@@ -167,27 +206,39 @@ impl Operation {
             args.get(2).cloned(),
         );
         Ok(match op_code {
-            OperationType::Native(o) => match (o, arg_tup, args.len()) {
-                (NO::None, (None, None, None), 0) => Self::None,
-                (NO::NewEntry, (None, None, None), 0) => Self::NewEntry,
-                (NO::CopyStatement, (Some(s), None, None), 1) => Self::CopyStatement(s),
-                (NO::EqualFromEntries, (Some(s1), Some(s2), None), 2) => {
+            OperationType::Native(o) => match (o, arg_tup, aux.clone(), args.len()) {
+                (NO::None, (None, None, None), OA::None, 0) => Self::None,
+                (NO::NewEntry, (None, None, None), OA::None, 0) => Self::NewEntry,
+                (NO::CopyStatement, (Some(s), None, None), OA::None, 1) => Self::CopyStatement(s),
+                (NO::EqualFromEntries, (Some(s1), Some(s2), None), OA::None, 2) => {
                     Self::EqualFromEntries(s1, s2)
                 }
-                (NO::NotEqualFromEntries, (Some(s1), Some(s2), None), 2) => {
+                (NO::NotEqualFromEntries, (Some(s1), Some(s2), None), OA::None, 2) => {
                     Self::NotEqualFromEntries(s1, s2)
                 }
-                (NO::GtFromEntries, (Some(s1), Some(s2), None), 2) => Self::GtFromEntries(s1, s2),
-                (NO::LtFromEntries, (Some(s1), Some(s2), None), 2) => Self::LtFromEntries(s1, s2),
-                (NO::ContainsFromEntries, (Some(s1), Some(s2), None), 2) => {
-                    Self::ContainsFromEntries(s1, s2)
+                (NO::GtFromEntries, (Some(s1), Some(s2), None), OA::None, 2) => {
+                    Self::GtFromEntries(s1, s2)
+                }
+                (NO::LtFromEntries, (Some(s1), Some(s2), None), OA::None, 2) => {
+                    Self::LtFromEntries(s1, s2)
                 }
-                (NO::NotContainsFromEntries, (Some(s1), Some(s2), None), 2) => {
-                    Self::NotContainsFromEntries(s1, s2)
+                (
+                    NO::ContainsFromEntries,
+                    (Some(s1), Some(s2), Some(s3)),
+                    OA::MerkleProof(pf),
+                    3,
+                ) => Self::ContainsFromEntries(s1, s2, s3, pf),
+                (
+                    NO::NotContainsFromEntries,
+                    (Some(s1), Some(s2), None),
+                    OA::MerkleProof(pf),
+                    2,
+                ) => Self::NotContainsFromEntries(s1, s2, pf),
+                (NO::SumOf, (Some(s1), Some(s2), Some(s3)), OA::None, 3) => Self::SumOf(s1, s2, s3),
+                (NO::ProductOf, (Some(s1), Some(s2), Some(s3)), OA::None, 3) => {
+                    Self::ProductOf(s1, s2, s3)
                 }
-                (NO::SumOf, (Some(s1), Some(s2), Some(s3)), 3) => Self::SumOf(s1, s2, s3),
-                (NO::ProductOf, (Some(s1), Some(s2), Some(s3)), 3) => Self::ProductOf(s1, s2, s3),
-                (NO::MaxOf, (Some(s1), Some(s2), Some(s3)), 3) => Self::MaxOf(s1, s2, s3),
+                (NO::MaxOf, (Some(s1), Some(s2), Some(s3)), OA::None, 3) => Self::MaxOf(s1, s2, s3),
                 _ => Err(anyhow!(
                     "Ill-formed operation {:?} with arguments {:?}.",
                     op_code,
@@ -270,20 +321,25 @@ impl Operation {
             Self::LtToNotEqual(_) => {
                 return Err(anyhow!("Invalid operation"));
             }
-            Self::ContainsFromEntries(ValueOf(ak1, v1), ValueOf(ak2, v2)) =>
-            /* TODO */
+            Self::ContainsFromEntries(ValueOf(ak1, v1), ValueOf(ak2, v2), ValueOf(ak3, v3), pf)
+                if MerkleTree::verify(pf.siblings.len(), (*v1).into(), &pf, v2, v3)? == () =>
             {
-                Some(vec![StatementArg::Key(*ak1), StatementArg::Key(*ak2)])
+                Some(vec![
+                    StatementArg::Key(*ak1),
+                    StatementArg::Key(*ak2),
+                    StatementArg::Key(*ak3),
+                ])
             }
-            Self::ContainsFromEntries(_, _) => {
+            Self::ContainsFromEntries(_, _, _, _) => {
                 return Err(anyhow!("Invalid operation"));
             }
-            Self::NotContainsFromEntries(ValueOf(ak1, v1), ValueOf(ak2, v2)) =>
-            /* TODO */
+            Self::NotContainsFromEntries(ValueOf(ak1, v1), ValueOf(ak2, v2), pf)
+                if MerkleTree::verify_nonexistence(pf.siblings.len(), (*v1).into(), &pf, v2)?
+                    == () =>
             {
                 Some(vec![StatementArg::Key(*ak1), StatementArg::Key(*ak2)])
             }
-            Self::NotContainsFromEntries(_, _) => {
+            Self::NotContainsFromEntries(_, _, _) => {
                 return Err(anyhow!("Invalid operation"));
             }
             Self::SumOf(ValueOf(ak1, v1), ValueOf(ak2, v2), ValueOf(ak3, v3)) => {
@@ -361,12 +417,12 @@ impl Operation {
             (Self::LtFromEntries(ValueOf(ak1, v1), ValueOf(ak2, v2)), Lt(ak3, ak4)) => {
                 Ok(v1 < v2 && ak3 == ak1 && ak4 == ak2)
             }
-            (Self::ContainsFromEntries(_, _), Contains(_, _)) =>
+            (Self::ContainsFromEntries(_, _, _, _), Contains(_, _, _)) =>
             /* TODO */
             {
                 Ok(true)
             }
-            (Self::NotContainsFromEntries(_, _), NotContains(_, _)) =>
+            (Self::NotContainsFromEntries(_, _, _), NotContains(_, _)) =>
             /* TODO */
             {
                 Ok(true)
diff --git a/src/middleware/statement.rs b/src/middleware/statement.rs
index 7454f19a..f9001139 100644
--- a/src/middleware/statement.rs
+++ b/src/middleware/statement.rs
@@ -44,8 +44,12 @@ pub enum Statement {
     NotEqual(AnchoredKey, AnchoredKey),
     Gt(AnchoredKey, AnchoredKey),
     Lt(AnchoredKey, AnchoredKey),
-    Contains(AnchoredKey, AnchoredKey),
-    NotContains(AnchoredKey, AnchoredKey),
+    Contains(
+        /* root  */ AnchoredKey,
+        /* key   */ AnchoredKey,
+        /* value */ AnchoredKey,
+    ),
+    NotContains(/* root  */ AnchoredKey, /* key   */ AnchoredKey),
     SumOf(AnchoredKey, AnchoredKey, AnchoredKey),
     ProductOf(AnchoredKey, AnchoredKey, AnchoredKey),
     MaxOf(AnchoredKey, AnchoredKey, AnchoredKey),
@@ -65,7 +69,7 @@ impl Statement {
             Self::NotEqual(_, _) => Native(NativePredicate::NotEqual),
             Self::Gt(_, _) => Native(NativePredicate::Gt),
             Self::Lt(_, _) => Native(NativePredicate::Lt),
-            Self::Contains(_, _) => Native(NativePredicate::Contains),
+            Self::Contains(_, _, _) => Native(NativePredicate::Contains),
             Self::NotContains(_, _) => Native(NativePredicate::NotContains),
             Self::SumOf(_, _, _) => Native(NativePredicate::SumOf),
             Self::ProductOf(_, _, _) => Native(NativePredicate::ProductOf),
@@ -82,7 +86,7 @@ impl Statement {
             Self::NotEqual(ak1, ak2) => vec![Key(ak1), Key(ak2)],
             Self::Gt(ak1, ak2) => vec![Key(ak1), Key(ak2)],
             Self::Lt(ak1, ak2) => vec![Key(ak1), Key(ak2)],
-            Self::Contains(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)],
             Self::SumOf(ak1, ak2, ak3) => vec![Key(ak1), Key(ak2), Key(ak3)],
             Self::ProductOf(ak1, ak2, ak3) => vec![Key(ak1), Key(ak2), Key(ak3)],
@@ -130,8 +134,10 @@ impl Statement {
                 }
             }
             Native(NativePredicate::Contains) => {
-                if let (StatementArg::Key(a0), StatementArg::Key(a1)) = (args[0], args[1]) {
-                    Ok(Self::Contains(a0, a1))
+                if let (StatementArg::Key(a0), StatementArg::Key(a1), StatementArg::Key(a2)) =
+                    (args[0], args[1], args[2])
+                {
+                    Ok(Self::Contains(a0, a1, a2))
                 } else {
                     Err(anyhow!("Incorrect statement args"))
                 }