diff --git a/src/backends/mock_main.rs b/src/backends/mock_main.rs
index d9ec4fa..b670547 100644
--- a/src/backends/mock_main.rs
+++ b/src/backends/mock_main.rs
@@ -1,6 +1,7 @@
 use crate::middleware::{
-    self, Hash, MainPod, MainPodInputs, NativeOperation, NativeStatement, NoneMainPod,
-    NoneSignedPod, Params, PodId, PodProver, SignedPod, Statement, StatementArg, ToFields,
+    self, hash_str, AnchoredKey, Hash, MainPod, MainPodInputs, NativeOperation, NativeStatement,
+    NoneMainPod, NoneSignedPod, Params, PodId, PodProver, SignedPod, Statement, StatementArg,
+    ToFields, KEY_TYPE, SELF,
 };
 use anyhow::Result;
 use itertools::Itertools;
@@ -33,6 +34,22 @@ impl OperationArg {
 #[derive(Clone, Debug, PartialEq, Eq)]
 struct Operation(pub NativeOperation, pub Vec<OperationArg>);
 
+impl Operation {
+    pub fn deref(&self, statements: &[Statement]) -> crate::middleware::Operation {
+        let deref_args = self
+            .1
+            .iter()
+            .map(|arg| match arg {
+                OperationArg::None => middleware::OperationArg::None,
+                OperationArg::Index(i) => {
+                    middleware::OperationArg::Statement(statements[*i].clone())
+                }
+            })
+            .collect();
+        middleware::Operation(self.0, deref_args)
+    }
+}
+
 impl fmt::Display for Operation {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
         write!(f, "{:?} ", self.0)?;
@@ -206,8 +223,12 @@ impl MockMainPod {
         }
 
         // Public statements
-        assert!(inputs.public_statements.len() <= params.max_public_statements);
-        for i in 0..params.max_public_statements {
+        assert!(inputs.public_statements.len() < params.max_public_statements);
+        statements.push(Statement(
+            NativeStatement::ValueOf,
+            vec![StatementArg::Key(AnchoredKey(SELF, hash_str(KEY_TYPE)))],
+        ));
+        for i in 0..(params.max_public_statements - 1) {
             let mut st = inputs.public_statements.get(i).unwrap_or(&st_none).clone();
             Self::pad_statement_args(params, &mut st.1);
             statements.push(st);
@@ -275,8 +296,9 @@ impl MockMainPod {
         let op_none = Self::operation_none(params);
 
         let offset_public_statements = statements.len() - params.max_public_statements;
-        for i in 0..params.max_public_statements {
-            let st = &statements[offset_public_statements + i];
+        operations.push(Operation(NativeOperation::NewEntry, vec![]));
+        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(NativeOperation::None, vec![])
             } else {
@@ -311,7 +333,8 @@ impl MockMainPod {
             .collect_vec();
         let input_main_pods = inputs.main_pods.iter().map(|p| (*p).clone()).collect_vec();
         let input_statements = inputs.statements.iter().cloned().collect_vec();
-        let public_statements = inputs.public_statements.iter().cloned().collect_vec();
+        let public_statements =
+            statements[statements.len() - params.max_public_statements..].to_vec();
 
         // get the id out of the public statements
         let id: PodId = PodId(hash_statements(&public_statements)?);
@@ -363,26 +386,94 @@ pub fn hash_statements(statements: &[middleware::Statement]) -> Result<middlewar
 
 impl MainPod for MockMainPod {
     fn verify(&self) -> bool {
-        // TODO
-        // - define input_statements as `statements.[self.offset_input_statements()..]`
-        // - Calculate the id from a subset of the statements.  Check it's equal to self.id
-        // - Find a ValueOf statement from the public statements with key=KEY_TYPE and check that
-        // the value is PodType::MockMainPod
-        // - Check that all `input_statements` of type `ValueOf` with origin=SELF have unique keys
+        let input_statement_offset = self.offset_input_statements();
+        // get the input_statements from the self.statements
+        let input_statements = &self.statements[input_statement_offset..];
+        // get the id out of the public statements, and ensure it is equal to self.id
+        let ids_match = self.id == PodId(hash_statements(&self.public_statements).unwrap());
+        // find a ValueOf statement from the public statements with key=KEY_TYPE and check that the
+        // value is PodType::MockMainPod
+        let has_type_statement = self
+            .public_statements
+            .iter()
+            .find(|s| {
+                s.0 == NativeStatement::ValueOf
+                    && s.1.len() > 0
+                    && if let StatementArg::Key(AnchoredKey(pod_id, key_hash)) = s.1[0] {
+                        pod_id == SELF && key_hash == hash_str(KEY_TYPE)
+                    } else {
+                        false
+                    }
+            })
+            .is_some();
+        // check that all `input_statements` of type `ValueOf` with origin=SELF have unique keys
         // (no duplicates)
-        // - Verify that all `input_statements` are correctly generated
+        // TODO: Instead of doing this, do a uniqueness check when verifying the output of a
+        // `NewValue` operation.
+        let value_ofs_unique = {
+            let key_id_pairs = input_statements
+                .into_iter()
+                .enumerate()
+                .map(|(i, s)| {
+                    (
+                        // Separate private from public statements.
+                        if i < self.params.max_priv_statements() {
+                            0
+                        } else {
+                            1
+                        },
+                        s,
+                    )
+                })
+                .filter(|(i, s)| s.0 == NativeStatement::ValueOf)
+                .flat_map(|(i, s)| {
+                    if let StatementArg::Key(ak) = &s.1[0] {
+                        vec![(i, ak.1, ak.0)]
+                    } else {
+                        vec![]
+                    }
+                })
+                .collect::<Vec<_>>();
+            !(0..key_id_pairs.len() - 1).any(|i| key_id_pairs[i + 1..].contains(&key_id_pairs[i]))
+        };
+        // verify that all `input_statements` are correctly generated
         // by `self.operations` (where each operation can only access previous statements)
-        todo!()
+        let statement_check = input_statements
+            .iter()
+            .enumerate()
+            .map(|(i, s)| {
+                self.operations[i]
+                    .deref(&self.statements[..input_statement_offset + i])
+                    .check(s.clone())
+            })
+            .collect::<Result<Vec<_>>>()
+            .unwrap();
+        ids_match && has_type_statement && value_ofs_unique & statement_check.into_iter().all(|b| b)
     }
     fn id(&self) -> PodId {
         self.id
     }
     fn pub_statements(&self) -> Vec<Statement> {
-        // TODO: All arguments that use origin=SELF need to be replaced by origin=self.id()
+        // return the public statements, where when origin=SELF is replaced by origin=self.id()
         self.statements
             .iter()
             .skip(self.offset_public_statements())
             .cloned()
+            .map(|statement| {
+                Statement(
+                    statement.0.clone(),
+                    statement
+                        .1
+                        .iter()
+                        .map(|sa| match &sa {
+                            StatementArg::Key(AnchoredKey(pod_id, h)) if *pod_id == SELF => {
+                                StatementArg::Key(AnchoredKey(self.id(), *h))
+                            }
+                            _ => sa.clone(),
+                        })
+                        .collect(),
+                )
+            })
             .collect()
     }
 
@@ -419,8 +510,8 @@ pub mod tests {
 
         println!("{:#}", pod);
 
-        // assert_eq!(pod.verify(), true); // TODO
-        // println!("id: {}", pod.id());
-        // println!("kvs: {:?}", pod.pub_statements());
+        assert_eq!(pod.verify(), true); // TODO
+                                        // println!("id: {}", pod.id());
+                                        // println!("pub_statements: {:?}", pod.pub_statements());
     }
 }
diff --git a/src/backends/plonky2.rs b/src/backends/plonky2.rs
index e69de29..8b13789 100644
--- a/src/backends/plonky2.rs
+++ b/src/backends/plonky2.rs
@@ -0,0 +1 @@
+
diff --git a/src/middleware.rs b/src/middleware.rs
index ef2a517..809d5df 100644
--- a/src/middleware.rs
+++ b/src/middleware.rs
@@ -1,7 +1,7 @@
 //! The middleware includes the type definitions and the traits used to connect the frontend and
 //! the backend.
 
-use anyhow::Result;
+use anyhow::{anyhow, Error, Result};
 use dyn_clone::DynClone;
 use hex::{FromHex, FromHexError};
 use itertools::Itertools;
@@ -12,7 +12,7 @@ use plonky2::plonk::config::{Hasher, PoseidonGoldilocksConfig};
 use std::any::Any;
 use std::cmp::{Ord, Ordering};
 use std::collections::HashMap;
-use std::fmt;
+use std::{array, fmt};
 use strum_macros::FromRepr;
 
 pub const KEY_SIGNER: &str = "_signer";
@@ -57,6 +57,22 @@ impl From<i64> for Value {
     }
 }
 
+impl TryInto<i64> for Value {
+    type Error = Error;
+    fn try_into(self) -> std::result::Result<i64, Self::Error> {
+        let value = self.0;
+        if &value[2..] != &[F::ZERO, F::ZERO]
+            || value[..2]
+                .iter()
+                .all(|x| x.to_canonical_u64() > u32::MAX as u64)
+        {
+            Err(anyhow!("Value not an element of the i64 embedding."))
+        } else {
+            Ok((value[0].to_canonical_u64() + value[1].to_canonical_u64() << 32) as i64)
+        }
+    }
+}
+
 impl fmt::Display for Value {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         if self.0[2].is_zero() && self.0[3].is_zero() {
@@ -284,8 +300,18 @@ impl ToFields for NativeStatement {
 }
 
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
+/// AnchoredKey is a tuple containing (OriginId: PodId, key: Hash)
 pub struct AnchoredKey(pub PodId, pub Hash);
 
+impl AnchoredKey {
+    pub fn origin(&self) -> PodId {
+        self.0
+    }
+    pub fn key(&self) -> Hash {
+        self.1
+    }
+}
+
 #[derive(Clone, Debug, PartialEq, Eq)]
 pub enum StatementArg {
     None,
@@ -307,6 +333,18 @@ impl StatementArg {
     pub fn is_none(&self) -> bool {
         matches!(self, Self::None)
     }
+    pub fn literal(&self) -> Result<Value> {
+        match self {
+            Self::Literal(value) => Ok(*value),
+            _ => Err(anyhow!("Statement argument {:?} is not a literal.", self)),
+        }
+    }
+    pub fn key(&self) -> Result<AnchoredKey> {
+        match self {
+            Self::Key(ak) => Ok(ak.clone()),
+            _ => Err(anyhow!("Statement argument {:?} is not a key.", self)),
+        }
+    }
 }
 
 impl ToFields for StatementArg {
@@ -339,6 +377,7 @@ impl ToFields for StatementArg {
     }
 }
 
+// TODO: Replace this with a more stringly typed enum as in the Devcon implementation.
 #[derive(Clone, Debug, PartialEq, Eq)]
 pub struct Statement(pub NativeStatement, pub Vec<StatementArg>);
 
@@ -358,6 +397,12 @@ impl fmt::Display for Statement {
 }
 
 impl Statement {
+    pub fn code(&self) -> NativeStatement {
+        self.0
+    }
+    pub fn args(&self) -> &[StatementArg] {
+        &self.1
+    }
     pub fn is_none(&self) -> bool {
         matches!(self.0, NativeStatement::None)
     }
@@ -409,9 +454,130 @@ pub enum OperationArg {
     Key(AnchoredKey),
 }
 
+impl OperationArg {
+    pub fn is_none(&self) -> bool {
+        matches!(self, Self::None)
+    }
+    pub fn statement(&self) -> Result<Statement> {
+        match self {
+            Self::Statement(statement) => Ok(statement.clone()),
+            _ => Err(anyhow!("Operation argument {:?} is not a statement.", self)),
+        }
+    }
+    pub fn key(&self) -> Result<AnchoredKey> {
+        match self {
+            Self::Key(ak) => Ok(ak.clone()),
+            _ => Err(anyhow!("Operation argument {:?} is not a key.", self)),
+        }
+    }
+}
+
+// TODO: Replace this with a more stringly typed enum as in the Devcon implementation.
 #[derive(Clone, Debug, PartialEq, Eq)]
 pub struct Operation(pub NativeOperation, pub Vec<OperationArg>);
 
+impl Operation {
+    pub fn code(&self) -> NativeOperation {
+        self.0
+    }
+    pub fn args(&self) -> &[OperationArg] {
+        &self.1
+    }
+    // TODO: Argument checking.
+    // TODO: Use `Err` for all type mismatches rather than `false`.
+    /// Checks the given operation against a statement.
+    pub fn check(&self, output_statement: Statement) -> Result<bool> {
+        use NativeOperation::*;
+        match self.0 {
+            // Nothing to check.
+            None => Ok(output_statement.code() == NativeStatement::None),
+            // Check that the resulting statement is of type `ValueOf`
+            // and its origin is `SELF`.
+            NewEntry =>
+                Ok(output_statement.code() == NativeStatement::ValueOf && output_statement.args()[0].key()?.origin() == SELF)
+            ,
+            // Check that the operation acts on a statement *and* the
+            // output is equal to this statement.
+            CopyStatement => Ok(output_statement == self.args()[0].statement()?)
+            ,
+            EqualFromEntries => {
+                let s1 = self.args()[0].statement()?;
+                let (s1_key, s1_value) = (s1.args()[0].key()?, s1.args()[1].literal()?);
+                let s2 = self.args()[1].statement()?;
+                let (s2_key, s2_value) = (s2.args()[0].key()?, s2.args()[1].literal()?);
+                let statements_equal = s1.code() == NativeStatement::ValueOf && s2.code() == NativeStatement::ValueOf && s1_value == s2_value;
+                Ok(statements_equal && output_statement.code() == NativeStatement::Equal && output_statement.args()[0].key()? == s1_key && output_statement.args()[1].key()? == s2_key)}
+            ,
+            NotEqualFromEntries => {
+                let s1 = self.args()[0].statement()?;
+                let (s1_key, s1_value) = (s1.args()[0].key()?, s1.args()[1].literal()?);
+                let s2 = self.args()[1].statement()?;
+                let (s2_key, s2_value) = (s2.args()[0].key()?, s2.args()[1].literal()?);
+                let statements_not_equal = s1.code() == NativeStatement::ValueOf && s2.code() == NativeStatement::ValueOf && s1_value != s2_value;
+                Ok(statements_not_equal && output_statement.code() == NativeStatement::NotEqual && output_statement.args()[0].key()? == s1_key && output_statement.args()[1].key()? == s2_key)}                ,
+            GtFromEntries => {
+                let s1 = self.args()[0].statement()?;
+                let (s1_key, s1_value) = (s1.args()[0].key()?, s1.args()[1].literal()?);
+                let s2 = self.args()[1].statement()?;
+                let (s2_key, s2_value) = (s2.args()[0].key()?, s2.args()[1].literal()?);
+                let statements_not_equal = s1.code() == NativeStatement::ValueOf && s2.code() == NativeStatement::ValueOf && s1_value > s2_value;
+                Ok(statements_not_equal && output_statement.code() == NativeStatement::Gt && output_statement.args()[0].key()? == s1_key && output_statement.args()[1].key()? == s2_key)},
+            LtFromEntries => {
+                let s1 = self.args()[0].statement()?;
+                let (s1_key, s1_value) = (s1.args()[0].key()?, s1.args()[1].literal()?);
+                let s2 = self.args()[1].statement()?;
+                let (s2_key, s2_value) = (s2.args()[0].key()?, s2.args()[1].literal()?);
+                let statements_not_equal = s1.code() == NativeStatement::ValueOf && s2.code() == NativeStatement::ValueOf && s1_value < s2_value;
+                Ok(statements_not_equal && output_statement.code() == NativeStatement::Lt && output_statement.args()[0].key()? == s1_key && output_statement.args()[1].key()? == s2_key)},
+            TransitiveEqualFromStatements => {
+                let s1 = self.args()[0].statement()?;
+                let s2 = self.args()[1].statement()?;
+                let key1 = s1.args()[0].key()?;
+                let key2 = s1.args()[1].key()?;
+                let key3 = s2.args()[0].key()?;
+                let key4 = s2.args()[1].key()?;
+                let statements_satisfy_transitivity = s1.code() == NativeStatement::Equal && s2.code() == NativeStatement::Equal && key2 == key3;
+                Ok(statements_satisfy_transitivity && output_statement.code() == NativeStatement::Equal && output_statement.args()[0].key()? == key1 && output_statement.args()[1].key()? == key4)
+            },
+            GtToNotEqual => {
+                let s = self.args()[0].statement()?;
+                let arg_is_gt = s.code() == NativeStatement::Gt;
+                Ok(arg_is_gt && output_statement.code() == NativeStatement::NotEqual && output_statement.args() == s.args())
+            },
+            LtToNotEqual => {
+                let s = self.args()[0].statement()?;
+                let arg_is_lt = s.code() == NativeStatement::Lt;
+                Ok(arg_is_lt && output_statement.code() == NativeStatement::NotEqual && output_statement.args() == s.args())
+            },
+            RenameContainedBy => {
+                let s1 = self.args()[0].statement()?;
+                let s2 = self.args()[1].statement()?;
+                let key1 = s1.args()[0].key()?;
+                let key2 = s1.args()[1].key()?;
+                let key3 = s2.args()[0].key()?;
+                let key4 = s2.args()[1].key()?;
+                let args_satisfy_rename = s1.code() == NativeStatement::Contains && s2.code() == NativeStatement::Equal && key1 == key3;
+                Ok(args_satisfy_rename && output_statement.code() == NativeStatement::Contains && output_statement.args()[0].key()? == key4 && output_statement.args()[1].key()? == key2)
+            },
+            SumOf => {
+                let s1 = self.args()[0].statement()?;
+                let s1_key = s1.args()[0].key()?;
+                let s1_value: i64 = s1.args()[1].literal()?.try_into()?;
+                let s2 = self.args()[1].statement()?;
+                let s2_key = s2.args()[0].key()?;
+                let s2_value:i64 = s2.args()[1].literal()?.try_into()?;
+                let s3 = self.args()[2].statement()?;
+                let s3_key = s3.args()[0].key()?;
+                let s3_value: i64 = s3.args()[1].literal()?.try_into()?;
+                let sum_holds = s1.code() == NativeStatement::ValueOf && s2.code() == NativeStatement::ValueOf && s3.code() == NativeStatement::ValueOf && s1_value == s2_value + s3_value;
+                Ok(sum_holds && output_statement.code() == NativeStatement::SumOf && output_statement.args()[0].key()? == s1_key && output_statement.args()[1].key()? == s2_key && output_statement.args()[2].key()? == s3_key)
+            },
+            // TODO: Remaining ops.
+            _ => Ok(true)
+        }
+    }
+}
+
 pub trait MainPod: fmt::Debug + DynClone {
     fn verify(&self) -> bool;
     fn id(&self) -> PodId;