Allow literals in statements (#276)

Implements #229 and #261.
This commit is contained in:
Daniel Gulotta 2025-06-13 10:27:19 -07:00 committed by GitHub
parent 21ab3c2d0d
commit 7d0d3ad769
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
20 changed files with 992 additions and 825 deletions

View file

@ -26,9 +26,9 @@ use crate::{
STANDARD_REC_MAIN_POD_CIRCUIT_DATA,
},
middleware::{
self, resolve_wildcard_values, AnchoredKey, CustomPredicateBatch, DynError, Hash,
MainPodInputs, NativeOperation, OperationType, Params, Pod, PodId, PodProver, PodType,
RecursivePod, StatementArg, ToFields, VDSet, F, KEY_TYPE, SELF,
self, resolve_wildcard_values, value_from_op, AnchoredKey, CustomPredicateBatch, DynError,
Hash, MainPodInputs, NativeOperation, OperationType, Params, Pod, PodId, PodProver,
PodType, RecursivePod, StatementArg, ToFields, VDSet, F, KEY_TYPE, SELF,
},
};
@ -125,31 +125,40 @@ pub(crate) fn extract_custom_predicate_verifications(
pub(crate) fn extract_merkle_proofs(
params: &Params,
operations: &[middleware::Operation],
statements: &[middleware::Statement],
) -> Result<Vec<MerkleClaimAndProof>> {
assert_eq!(operations.len(), statements.len());
let merkle_proofs: Vec<_> = operations
.iter()
.flat_map(|op| match op {
middleware::Operation::ContainsFromEntries(
middleware::Statement::ValueOf(_, root),
middleware::Statement::ValueOf(_, key),
middleware::Statement::ValueOf(_, value),
pf,
) => Some(MerkleClaimAndProof::new(
Hash::from(root.raw()),
key.raw(),
Some(value.raw()),
pf.clone(),
)),
middleware::Operation::NotContainsFromEntries(
middleware::Statement::ValueOf(_, root),
middleware::Statement::ValueOf(_, key),
pf,
) => Some(MerkleClaimAndProof::new(
Hash::from(root.raw()),
key.raw(),
None,
pf.clone(),
)),
.zip(statements.iter())
.flat_map(|(op, st)| match (op, st) {
(
middleware::Operation::ContainsFromEntries(root_s, key_s, value_s, pf),
middleware::Statement::Contains(root_ref, key_ref, value_ref),
) => {
let root = value_from_op(root_s, root_ref)?;
let key = value_from_op(key_s, key_ref)?;
let value = value_from_op(value_s, value_ref)?;
Some(MerkleClaimAndProof::new(
Hash::from(root.raw()),
key.raw(),
Some(value.raw()),
pf.clone(),
))
}
(
middleware::Operation::NotContainsFromEntries(root_s, key_s, pf),
middleware::Statement::NotContains(root_ref, key_ref),
) => {
let root = value_from_op(root_s, root_ref)?;
let key = value_from_op(key_s, key_ref)?;
Some(MerkleClaimAndProof::new(
Hash::from(root.raw()),
key.raw(),
None,
pf.clone(),
))
}
_ => None,
})
.collect();
@ -320,9 +329,9 @@ pub(crate) fn layout_statements(
// Public statements
assert!(inputs.public_statements.len() < params.max_public_statements);
let mut type_st = middleware::Statement::ValueOf(
AnchoredKey::from((SELF, KEY_TYPE)),
middleware::Value::from(PodType::MockMain),
let mut type_st = middleware::Statement::Equal(
AnchoredKey::from((SELF, KEY_TYPE)).into(),
middleware::Value::from(PodType::MockMain).into(),
)
.into();
pad_statement(params, &mut type_st);
@ -470,7 +479,7 @@ impl Prover {
})
.collect_vec();
let merkle_proofs = extract_merkle_proofs(params, inputs.operations)?;
let merkle_proofs = extract_merkle_proofs(params, inputs.operations, inputs.statements)?;
let custom_predicate_batches = extract_custom_predicate_batches(params, inputs.operations)?;
let custom_predicate_verifications = extract_custom_predicate_verifications(
params,
@ -805,12 +814,12 @@ pub mod tests {
max_signed_pod_values: 2,
max_public_statements: 2,
num_public_statements_id: 4,
max_statement_args: 2,
max_statement_args: 3,
max_operation_args: 3,
max_custom_predicate_batches: 2,
max_custom_predicate_verifications: 2,
max_custom_predicate_arity: 2,
max_custom_predicate_wildcards: 2,
max_custom_predicate_wildcards: 3,
max_custom_batch_size: 2,
max_merkle_proofs_containers: 2,
max_depth_mt_containers: 4,
@ -905,7 +914,7 @@ pub mod tests {
let vd_set = &*DEFAULT_VD_SET;
let mut cpb_builder = CustomPredicateBatchBuilder::new(params.clone(), "cpb".into());
let stb0 = STB::new(NP::ValueOf)
let stb0 = STB::new(NP::Equal)
.arg(("id", key("score")))
.arg(literal(42));
let stb1 = STB::new(NP::Equal)

View file

@ -75,7 +75,11 @@ impl Operation {
.iter()
.flat_map(|arg| match arg {
OperationArg::None => None,
OperationArg::Index(i) => Some(statements[*i].clone().try_into()),
OperationArg::Index(i) => {
let st: Result<crate::middleware::Statement> =
statements[*i].clone().try_into();
Some(st)
}
})
.collect::<Result<Vec<_>>>()?;
let deref_aux = match self.2 {

View file

@ -48,41 +48,25 @@ impl TryFrom<Statement> for middleware::Statement {
type NP = NativePredicate;
type SA = StatementArg;
let proper_args = s.args();
let args = (
proper_args.first().cloned(),
proper_args.get(1).cloned(),
proper_args.get(2).cloned(),
);
Ok(match s.0 {
Predicate::Native(np) => match (np, args, proper_args.len()) {
(NP::None, _, 0) => S::None,
(NP::ValueOf, (Some(SA::Key(ak)), Some(SA::Literal(v)), None), 2) => {
S::ValueOf(ak, v)
Predicate::Native(np) => match (np, &proper_args.as_slice()) {
(NP::None, &[]) => S::None,
(NP::Equal, &[a1, a2]) => S::Equal(a1.try_into()?, a2.try_into()?),
(NP::NotEqual, &[a1, a2]) => S::NotEqual(a1.try_into()?, a2.try_into()?),
(NP::LtEq, &[a1, a2]) => S::LtEq(a1.try_into()?, a2.try_into()?),
(NP::Lt, &[a1, a2]) => S::Lt(a1.try_into()?, a2.try_into()?),
(NP::Contains, &[a1, a2, a3]) => {
S::Contains(a1.try_into()?, a2.try_into()?, a3.try_into()?)
}
(NP::Equal, (Some(SA::Key(ak1)), Some(SA::Key(ak2)), None), 2) => {
S::Equal(ak1, ak2)
(NP::NotContains, &[a1, a2]) => S::NotContains(a1.try_into()?, a2.try_into()?),
(NP::SumOf, &[a1, a2, a3]) => {
S::SumOf(a1.try_into()?, a2.try_into()?, a3.try_into()?)
}
(NP::NotEqual, (Some(SA::Key(ak1)), Some(SA::Key(ak2)), None), 2) => {
S::NotEqual(ak1, ak2)
(NP::ProductOf, &[a1, a2, a3]) => {
S::ProductOf(a1.try_into()?, a2.try_into()?, a3.try_into()?)
}
(NP::LtEq, (Some(SA::Key(ak1)), Some(SA::Key(ak2)), None), 2) => S::LtEq(ak1, ak2),
(NP::Lt, (Some(SA::Key(ak1)), Some(SA::Key(ak2)), None), 2) => S::Lt(ak1, ak2),
(NP::Contains, (Some(SA::Key(ak1)), Some(SA::Key(ak2)), Some(SA::Key(ak3))), 3) => {
S::Contains(ak1, ak2, ak3)
}
(NP::NotContains, (Some(SA::Key(ak1)), Some(SA::Key(ak2)), None), 2) => {
S::NotContains(ak1, ak2)
}
(NP::SumOf, (Some(SA::Key(ak1)), Some(SA::Key(ak2)), Some(SA::Key(ak3))), 3) => {
S::SumOf(ak1, ak2, ak3)
}
(
NP::ProductOf,
(Some(SA::Key(ak1)), Some(SA::Key(ak2)), Some(SA::Key(ak3))),
3,
) => S::ProductOf(ak1, ak2, ak3),
(NP::MaxOf, (Some(SA::Key(ak1)), Some(SA::Key(ak2)), Some(SA::Key(ak3))), 3) => {
S::MaxOf(ak1, ak2, ak3)
(NP::MaxOf, &[a1, a2, a3]) => {
S::MaxOf(a1.try_into()?, a2.try_into()?, a3.try_into()?)
}
_ => Err(Error::custom(format!(
"Ill-formed statement expression {:?}",