diff --git a/src/backends/plonky2/circuits/common.rs b/src/backends/plonky2/circuits/common.rs index c7ea061..72f129d 100644 --- a/src/backends/plonky2/circuits/common.rs +++ b/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, diff --git a/src/backends/plonky2/circuits/mainpod.rs b/src/backends/plonky2/circuits/mainpod.rs index dec3281..398c805 100644 --- a/src/backends/plonky2/circuits/mainpod.rs +++ b/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( &self, builder: &mut CircuitBuilder, - n: usize, resolved_op_args: &[StatementTarget], - ) -> BoolTarget { - let arg_is_valueof = resolved_op_args[..n] + ) -> (BoolTarget, [ValueTarget; 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::>(); - 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( - builder, - st, - op, - resolved_merkle_claim, - &resolved_op_args, - )] + vec![ + self.eval_contains_from_entries( + builder, + st, + op, + 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, + 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, @@ -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 merkle_root_value = resolved_op_args[0].args[1].as_value(); - let key_value = resolved_op_args[1].args[1].as_value(); + let (arg_types_ok, [merkle_root_value, key_value]) = + self.first_n_args_as_values(builder, resolved_op_args); // 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, 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::>(), + ); + + 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 arg1_value = resolved_op_args[0].args[1].as_value(); - let arg2_value = resolved_op_args[1].args[1].as_value(); + let (arg_types_ok, [arg1_value, arg2_value]) = + self.first_n_args_as_values(builder, resolved_op_args); // 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 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 (arg_types_ok, [arg1_value, arg2_value, arg3_value]) = + self.first_n_args_as_values(builder, resolved_op_args); 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, + 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, @@ -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, + 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, @@ -772,10 +907,61 @@ mod tests { } #[test] - fn test_operation_verify() -> Result<()> { - let params = Params::default(); + fn test_eq_neq_verify_failures() { + let st1: mainpod::Statement = + Statement::ValueOf(AnchoredKey::from((SELF, "hello")), Value::from(55)).into(); + let st2: mainpod::Statement = Statement::ValueOf( + AnchoredKey::from((PodId(RawValue::from(75).into()), "world")), + Value::from(56), + ) + .into(); + let st3: mainpod::Statement = Statement::ValueOf( + AnchoredKey::from((PodId(RawValue::from(88).into()), "hola")), + Value::from(RawValue([ + GoldilocksField::NEG_ONE, + GoldilocksField::ZERO, + GoldilocksField::ZERO, + GoldilocksField::ZERO, + ])), + ) + .into(); + let 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.clone(), - op, - prev_statements.clone(), - merkle_proofs.clone(), - )?; + operation_verify(st, op, prev_statements, vec![]) + } - // 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( - st1.clone(), - op, - prev_statements.clone(), - merkle_proofs.clone(), - )?; + operation_verify(st1, op, prev_statements, vec![]) + } - // 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]; - operation_verify(st, op, prev_statements, merkle_proofs.clone())?; + let prev_statements = vec![st1, st2]; + 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()]; - operation_verify(st, op, prev_statements, merkle_proofs.clone())?; + let prev_statements = vec![st1, st2.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]; - operation_verify(st, op, prev_statements, merkle_proofs.clone())?; + let prev_statements = vec![st3, st2]; + 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()]; - operation_verify(st, op, prev_statements, merkle_proofs.clone())?; + let prev_statements = vec![st1, st2.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) } }