From 8cac45f5834423c21fb3d65fe888cff8f20d1e3b Mon Sep 17 00:00:00 2001 From: Evan Laufer Date: Mon, 15 Sep 2025 14:01:58 -0700 Subject: [PATCH 1/2] Add container insert and update --- core/new_solver/src/edb.rs | 129 ++++++ .../src/handlers/container_insert.rs | 410 ++++++++++++++++++ .../src/handlers/container_update.rs | 303 +++++++++++++ core/new_solver/src/handlers/mod.rs | 4 + core/new_solver/src/op.rs | 2 + core/new_solver/src/proof_dag.rs | 56 ++- core/new_solver/src/replay.rs | 101 ++++- core/new_solver/src/types.rs | 16 + core/new_solver/src/util.rs | 25 +- 9 files changed, 1038 insertions(+), 8 deletions(-) create mode 100644 core/new_solver/src/handlers/container_insert.rs create mode 100644 core/new_solver/src/handlers/container_update.rs diff --git a/core/new_solver/src/edb.rs b/core/new_solver/src/edb.rs index 8e40885..5931fbf 100644 --- a/core/new_solver/src/edb.rs +++ b/core/new_solver/src/edb.rs @@ -45,6 +45,17 @@ pub trait EdbView { /// ContainsFromEntries support: get a value only if it comes from a full dictionary (generation). fn contains_full_value(&self, _root: &Hash, _key: &Key) -> Option; + /// Enumerate roots that can justify Insert(new_root,old_root,key,val) along with their provenance. + fn enumerate_insert_sources(&self, _key: &Key, _val: &Value) + -> Vec<(Hash, Hash, InsertSource)>; + + /// Enumerate roots that can justify Update(new_root,old_root,key,new_val) along with their provenance. + fn enumerate_update_sources( + &self, + _key: &Key, + _new_val: &Value, + ) -> Vec<(Hash, Hash, UpdateSource)>; + /// Enumerate existing custom heads matching the literal mask. /// `filters[i] = Some(v)` requires head arg i == v; `None` matches any. fn custom_matches( @@ -87,6 +98,19 @@ pub enum ContainsSource { GeneratedFromFullDict { root: Hash }, } +/// Provenance of an Insert(root,root,key,value) fact. +#[derive(Clone, Debug)] +pub enum InsertSource { + Copied { pod: PodRef }, + GeneratedFromFullDict { new_root: Hash, old_root: Hash }, +} +/// Provenance of an Update(root,old_root,key,new_value,old_value) fact. +#[derive(Clone, Debug)] +pub enum UpdateSource { + Copied { pod: PodRef }, + GeneratedFromFullDict { new_root: Hash, old_root: Hash }, +} + #[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)] enum IndexKey { Literal(RawOrdValue), @@ -627,6 +651,111 @@ impl EdbView for ImmutableEdb { .collect() } + fn enumerate_insert_sources(&self, key: &Key, val: &Value) -> Vec<(Hash, Hash, InsertSource)> { + let mut out = Vec::new(); + + // From copied statements + let results = self.query( + PredicateKey::Native(pod2::middleware::NativePredicate::ContainerInsert), + &[ + ArgSel::Val, // new_root (any) + ArgSel::Val, // old_root (any) + ArgSel::Literal(&Value::from(key.name())), // key (specific) + ArgSel::Literal(val), // value (specific) + ], + ); + for (stmt, pod_ref) in results { + if let Statement::ContainerInsert(new_root_ref, old_root_ref, _, _) = &stmt { + if let (ValueRef::Literal(new_root_val), ValueRef::Literal(old_root_val)) = + (new_root_ref, old_root_ref) + { + let new_root = Hash::from(new_root_val.raw()); + let old_root = Hash::from(old_root_val.raw()); + out.push((new_root, old_root, InsertSource::Copied { pod: pod_ref })); + } + } + } + + // From full dictionaries - create hash set of all known commitment hashes + let known_commitments: std::collections::HashSet = + self.full_dict_objs.keys().cloned().collect(); + + // For each dictionary, try inserting key=val and see if result exists in known commitments + for (old_root, old_dict) in self.full_dict_objs.iter() { + let mut new_dict = old_dict.clone(); + if new_dict.insert(key, val).is_ok() { + let new_commitment = new_dict.commitment(); + if known_commitments.contains(&new_commitment) { + out.push(( + new_commitment, + *old_root, + InsertSource::GeneratedFromFullDict { + new_root: new_commitment, + old_root: *old_root, + }, + )); + } + } + } + out + } + + fn enumerate_update_sources( + &self, + key: &Key, + new_val: &Value, + ) -> Vec<(Hash, Hash, UpdateSource)> { + let mut out = Vec::new(); + + // From copied statements + let results = self.query( + PredicateKey::Native(pod2::middleware::NativePredicate::ContainerUpdate), + &[ + ArgSel::Val, // new_root (any) + ArgSel::Val, // old_root (any) + ArgSel::Literal(&Value::from(key.name())), // key (specific) + ArgSel::Literal(new_val), // value (specific - this is the new value) + ], + ); + for (stmt, pod_ref) in results { + if let Statement::ContainerUpdate(new_root_ref, old_root_ref, _, _) = &stmt { + if let (ValueRef::Literal(new_root_val), ValueRef::Literal(old_root_val)) = + (new_root_ref, old_root_ref) + { + let new_root = Hash::from(new_root_val.raw()); + let old_root = Hash::from(old_root_val.raw()); + out.push((new_root, old_root, UpdateSource::Copied { pod: pod_ref })); + } + } + } + + // From full dictionaries - create hash set of all known commitment hashes + let known_commitments: std::collections::HashSet = + self.full_dict_objs.keys().cloned().collect(); + + // For each dictionary, try updating key to new_val and see if result exists in known commitments + for (old_root, old_dict) in self.full_dict_objs.iter() { + // Check if old dictionary contains the key (with any value) + if old_dict.get(key).is_ok() { + let mut new_dict = old_dict.clone(); + if new_dict.insert(key, new_val).is_ok() { + let new_commitment = new_dict.commitment(); + if known_commitments.contains(&new_commitment) { + out.push(( + new_commitment, + *old_root, + UpdateSource::GeneratedFromFullDict { + new_root: new_commitment, + old_root: *old_root, + }, + )); + } + } + } + } + out + } + fn get_secret_key(&self, public_key: &PublicKey) -> Option<&SecretKey> { self.keypairs.get(&OrderedPublicKey(*public_key)) } diff --git a/core/new_solver/src/handlers/container_insert.rs b/core/new_solver/src/handlers/container_insert.rs new file mode 100644 index 0000000..ef7eeab --- /dev/null +++ b/core/new_solver/src/handlers/container_insert.rs @@ -0,0 +1,410 @@ +use pod2::middleware::{ + containers::{Dictionary, Set}, + Hash, Key, NativePredicate, StatementTmplArg, TypedValue, +}; + +use super::util::{arg_to_selector, handle_copy_results}; +use crate::{ + edb::{EdbView, InsertSource}, + op::OpHandler, + prop::PropagatorResult, + types::{ConstraintStore, OpTag}, +}; + +/// Utility: extract a bound root hash from a template arg (literal or wildcard). +pub fn root_from_arg(arg: &StatementTmplArg, store: &ConstraintStore) -> Option { + match arg { + StatementTmplArg::Literal(v) => Some(Hash::from(v.raw())), + StatementTmplArg::Wildcard(w) => store.bindings.get(&w.index).map(|v| Hash::from(v.raw())), + _ => None, + } +} + +/// Utility: extract a Key from a template arg (literal string or wildcard bound to string). +pub fn key_from_arg(arg: &StatementTmplArg, store: &ConstraintStore) -> Option { + match arg { + StatementTmplArg::Literal(v) => { + if let Ok(s) = String::try_from(v.typed()) { + Some(Key::from(s)) + } else { + None + } + } + StatementTmplArg::Wildcard(w) => store.bindings.get(&w.index).and_then(|v| { + if let Ok(s) = String::try_from(v.typed()) { + Some(Key::from(s)) + } else { + None + } + }), + _ => None, + } +} + +/// Utility: extract an int from a template arg +pub fn int_from_arg(arg: &StatementTmplArg, store: &ConstraintStore) -> Option { + match arg { + StatementTmplArg::Literal(v) => i64::try_from(v.typed()).ok(), + StatementTmplArg::Wildcard(w) => store + .bindings + .get(&w.index) + .and_then(|v| i64::try_from(v.typed()).ok()), + _ => None, + } +} + +/// Copy existing ContainerInsert(root, key, value) statements from EDB. +/// Supports binding the value (third argument) when root and key are known. +pub struct CopyContainerInsertHandler; + +impl OpHandler for CopyContainerInsertHandler { + fn propagate( + &self, + args: &[StatementTmplArg], + store: &mut ConstraintStore, + edb: &dyn EdbView, + ) -> PropagatorResult { + if args.len() != 4 { + return PropagatorResult::Contradiction; + } + + // We need to store owned values for selectors, since ArgSel holds references. + let (mut a_val, mut a_root) = (None, None); + let (mut b_val, mut b_root) = (None, None); + let (mut c_val, mut c_root) = (None, None); + let (mut d_val, mut d_root) = (None, None); + + let sel_a = arg_to_selector(&args[0], store, &mut a_val, &mut a_root); + let sel_b = arg_to_selector(&args[1], store, &mut b_val, &mut b_root); + let sel_c = arg_to_selector(&args[2], store, &mut c_val, &mut c_root); + let sel_d = arg_to_selector(&args[3], store, &mut d_val, &mut d_root); + + let results = edb.query( + crate::edb::PredicateKey::Native(NativePredicate::ContainerInsert), + &[sel_a, sel_b, sel_c, sel_d], + ); + + handle_copy_results(results, args, store) + } +} + +/// ContainerInsertFromEntries: when the full dictionary is known, it can justify ContainerInsert operations. +pub struct ContainerInsertFromEntriesHandler; + +impl OpHandler for ContainerInsertFromEntriesHandler { + fn propagate( + &self, + args: &[StatementTmplArg], + store: &mut ConstraintStore, + edb: &dyn EdbView, + ) -> PropagatorResult { + if args.len() != 4 { + return PropagatorResult::Contradiction; + } + let (new_root, old_root, a_key, a_val) = (&args[0], &args[1], &args[2], &args[3]); + + let new_root_value = match new_root { + StatementTmplArg::Literal(v) => Some(v.clone()), + StatementTmplArg::Wildcard(w) => store.bindings.get(&w.index).cloned(), + _ => None, + }; + let old_root_value = match old_root { + StatementTmplArg::Literal(v) => Some(v.clone()), + StatementTmplArg::Wildcard(w) => store.bindings.get(&w.index).cloned(), + _ => None, + }; + + match (new_root_value, old_root_value) { + (Some(new_root_value), Some(old_root_value)) => { + match (new_root_value.typed(), old_root_value.typed()) { + (TypedValue::Dictionary(new_dict), TypedValue::Dictionary(old_dict)) => { + if let Some(key) = key_from_arg(a_key, store) { + return check_dict_insert_for_known_dicts( + new_dict, old_dict, &key, a_val, store, + ); + } + } + (TypedValue::Set(new_set), TypedValue::Set(old_set)) => { + if let Some(result) = + check_set_insert_for_known_set(new_set, old_set, a_key, a_val, store) + { + return result; + }; + } + _ => {} + } + } + _ => {} + } + + // Enumeration: if both roots are unbound wildcards and key/value are known, enumerate candidate root pairs + if let (StatementTmplArg::Wildcard(wnew), StatementTmplArg::Wildcard(wold)) = + (new_root, old_root) + { + if !store.bindings.contains_key(&wnew.index) + && !store.bindings.contains_key(&wold.index) + { + let key_opt = key_from_arg(a_key, store); + let val_opt = match a_val { + StatementTmplArg::Literal(v) => Some(v.clone()), + StatementTmplArg::Wildcard(wv) => store.bindings.get(&wv.index).cloned(), + _ => None, + }; + if let (Some(key), Some(val)) = (key_opt, val_opt) { + let mut alts = Vec::new(); + for (new_hash, old_hash, src) in edb.enumerate_insert_sources(&key, &val) { + let op_tag = match src { + InsertSource::GeneratedFromFullDict { .. } => { + OpTag::GeneratedContainerInsert { + new_root: new_hash, + old_root: old_hash, + key: key.clone(), + value: val.clone(), + } + } + InsertSource::Copied { pod } => OpTag::CopyStatement { source: pod }, + }; + alts.push(crate::prop::Choice { + bindings: vec![ + (wnew.index, new_hash.into()), + (wold.index, old_hash.into()), + ], + op_tag, + }); + } + tracing::trace!( + ?key, + ?val, + candidates = alts.len(), + "Insert enum root pairs" + ); + return if alts.is_empty() { + PropagatorResult::Contradiction + } else { + PropagatorResult::Choices { alternatives: alts } + }; + } + } + } + + // Need to handle other missing argument combinations with proper suspension + let waits = crate::prop::wildcards_in_args(args) + .into_iter() + .filter(|i| !store.bindings.contains_key(i)) + .collect::>(); + + if waits.is_empty() { + // All arguments are bound - validate the operation if possible + let new_hash_opt = root_from_arg(new_root, store); + let old_hash_opt = root_from_arg(old_root, store); + let key_opt = key_from_arg(a_key, store); + let val_opt = match a_val { + StatementTmplArg::Literal(v) => Some(v.clone()), + StatementTmplArg::Wildcard(wv) => store.bindings.get(&wv.index).cloned(), + _ => None, + }; + + if let (Some(new_hash), Some(old_hash), Some(key), Some(val)) = + (new_hash_opt, old_hash_opt, key_opt, val_opt) + { + // Check if this insert operation is valid by seeing if it exists in sources + for (enum_new, enum_old, _) in edb.enumerate_insert_sources(&key, &val) { + if enum_new == new_hash && enum_old == old_hash { + return PropagatorResult::Entailed { + bindings: vec![], + op_tag: OpTag::FromLiterals, + }; + } + } + PropagatorResult::Contradiction + } else { + // Some values couldn't be extracted - contradiction + PropagatorResult::Contradiction + } + } else { + PropagatorResult::Suspend { on: waits } + } + } +} + +fn check_dict_insert_for_known_dicts( + new_dict: &Dictionary, + old_dict: &Dictionary, + key: &Key, + a_val: &StatementTmplArg, + store: &ConstraintStore, +) -> PropagatorResult { + // get the value from the new_dict + let dict_value = new_dict.get(&key); + if dict_value.is_err() { + return PropagatorResult::Contradiction; + } + let dict_value = dict_value.unwrap(); + + // insert the value into the old dict and ensure equal to new_dict + let mut old_dict = old_dict.clone(); + if old_dict.insert(&key, &dict_value).is_err() || *new_dict != old_dict { + return PropagatorResult::Contradiction; + } + + // check the value matches the expected value + match a_val { + StatementTmplArg::Literal(v) => { + if dict_value == v { + PropagatorResult::Entailed { + bindings: vec![], + op_tag: OpTag::FromLiterals, + } + } else { + PropagatorResult::Contradiction + } + } + StatementTmplArg::Wildcard(wv) => { + if let Some(existing) = store.bindings.get(&wv.index) { + if existing == dict_value { + PropagatorResult::Entailed { + bindings: vec![], + op_tag: OpTag::FromLiterals, + } + } else { + PropagatorResult::Contradiction + } + } else { + PropagatorResult::Entailed { + bindings: vec![(wv.index, dict_value.clone())], + op_tag: OpTag::FromLiterals, + } + } + } + _ => PropagatorResult::Contradiction, + } +} + +fn check_set_insert_for_known_set( + new_set: &Set, + old_set: &Set, + a_key: &StatementTmplArg, + a_val: &StatementTmplArg, + store: &ConstraintStore, +) -> Option { + // For Sets, key and value arguments must unify to the same value. + let (value_opt, bindings_opt) = match (a_key, a_val) { + (StatementTmplArg::Literal(k), StatementTmplArg::Literal(v)) => { + if k != v { + return Some(PropagatorResult::Contradiction); + } + (Some(k.clone()), Some(vec![])) + } + (StatementTmplArg::Literal(k), StatementTmplArg::Wildcard(wv)) => { + if let Some(bound_v) = store.bindings.get(&wv.index) { + if k != bound_v { + return Some(PropagatorResult::Contradiction); + } + (Some(k.clone()), Some(vec![])) + } else { + (Some(k.clone()), Some(vec![(wv.index, k.clone())])) + } + } + (StatementTmplArg::Wildcard(wk), StatementTmplArg::Literal(v)) => { + if let Some(bound_k) = store.bindings.get(&wk.index) { + if v != bound_k { + return Some(PropagatorResult::Contradiction); + } + (Some(v.clone()), Some(vec![])) + } else { + (Some(v.clone()), Some(vec![(wk.index, v.clone())])) + } + } + (StatementTmplArg::Wildcard(wk), StatementTmplArg::Wildcard(wv)) => { + let k_bound = store.bindings.get(&wk.index); + let v_bound = store.bindings.get(&wv.index); + match (k_bound, v_bound) { + (Some(k), Some(v)) => { + if k != v { + return Some(PropagatorResult::Contradiction); + } + (Some(k.clone()), Some(vec![])) + } + (Some(k), None) => (Some(k.clone()), Some(vec![(wv.index, k.clone())])), + (None, Some(v)) => (Some(v.clone()), Some(vec![(wk.index, v.clone())])), + (None, None) => (None, None), // Cannot determine value if both unbound + } + } + _ => (None, None), + }; + + if value_opt.is_none() || bindings_opt.is_none() { + return None; + } + let (value, bindings) = (value_opt.unwrap(), bindings_opt.unwrap()); + + // ensure new set is old set with value inserted + let mut old_set = old_set.clone(); + if old_set.insert(&value).is_err() || *new_set != old_set { + return Some(PropagatorResult::Contradiction); + } + + Some(PropagatorResult::Entailed { + bindings, + op_tag: OpTag::FromLiterals, + }) +} + +/// Register ContainerInsert handlers with the operation registry. +pub fn register_container_insert_handlers(reg: &mut crate::op::OpRegistry) { + reg.register( + NativePredicate::ContainerInsert, + Box::new(CopyContainerInsertHandler), + ); + reg.register( + NativePredicate::ContainerInsert, + Box::new(ContainerInsertFromEntriesHandler), + ); +} + +#[cfg(test)] +mod tests { + use pod2::middleware::{StatementTmplArg, Value}; + + use super::*; + use crate::{edb::ImmutableEdbBuilder, types::ConstraintStore}; + + #[test] + fn test_copy_container_insert_handler() { + // Basic test structure - would need actual EDB with ContainerInsert statements + //let mut store = ConstraintStore::default(); + //let edb = ImmutableEdbBuilder::new().build(); + //let handler = CopyContainerInsertHandler; + + //let args = args_from(&["?0", "?1", "\"key\"", "\"value\""]); + //let result = handler.propagate(&args, &mut store, &edb); + + //// Should not find anything in empty EDB + //matches!(result, PropagatorResult::Contradiction); + } + + #[test] + fn test_container_insert_from_entries_dict() { + let mut store = ConstraintStore::default(); + let edb = ImmutableEdbBuilder::new().build(); + let handler = ContainerInsertFromEntriesHandler; + + // Test with all literal arguments + let new_root = Value::from("new_root_hash".to_string()); + let old_root = Value::from("old_root_hash".to_string()); + let key = Value::from("test_key".to_string()); + let value = Value::from("test_value".to_string()); + + let args = vec![ + StatementTmplArg::Literal(new_root), + StatementTmplArg::Literal(old_root), + StatementTmplArg::Literal(key), + StatementTmplArg::Literal(value), + ]; + + let result = handler.propagate(&args, &mut store, &edb); + + // Should succeed - all literals are considered valid for now + matches!(result, PropagatorResult::Entailed { .. }); + } +} diff --git a/core/new_solver/src/handlers/container_update.rs b/core/new_solver/src/handlers/container_update.rs new file mode 100644 index 0000000..c51eae9 --- /dev/null +++ b/core/new_solver/src/handlers/container_update.rs @@ -0,0 +1,303 @@ +use pod2::middleware::{ + containers::Dictionary, Key, NativePredicate, StatementTmplArg, TypedValue, +}; + +use super::util::{arg_to_selector, handle_copy_results}; +use crate::{ + edb::{EdbView, UpdateSource}, + op::OpHandler, + prop::PropagatorResult, + types::{ConstraintStore, OpTag}, +}; + +// Import utilities from container_insert module +use super::container_insert::{key_from_arg, root_from_arg}; + +/// Copy existing ContainerUpdate(new_root, old_root, key, value) statements from EDB. +pub struct CopyContainerUpdateHandler; + +impl OpHandler for CopyContainerUpdateHandler { + fn propagate( + &self, + args: &[StatementTmplArg], + store: &mut ConstraintStore, + edb: &dyn EdbView, + ) -> PropagatorResult { + if args.len() != 4 { + return PropagatorResult::Contradiction; + } + + // We need to store owned values for selectors, since ArgSel holds references. + let (mut a_val, mut a_root) = (None, None); + let (mut b_val, mut b_root) = (None, None); + let (mut c_val, mut c_root) = (None, None); + let (mut d_val, mut d_root) = (None, None); + + let sel_a = arg_to_selector(&args[0], store, &mut a_val, &mut a_root); + let sel_b = arg_to_selector(&args[1], store, &mut b_val, &mut b_root); + let sel_c = arg_to_selector(&args[2], store, &mut c_val, &mut c_root); + let sel_d = arg_to_selector(&args[3], store, &mut d_val, &mut d_root); + + let results = edb.query( + crate::edb::PredicateKey::Native(NativePredicate::ContainerUpdate), + &[sel_a, sel_b, sel_c, sel_d], + ); + + handle_copy_results(results, args, store) + } +} + +/// ContainerUpdateFromEntries: when the full dictionary is known, it can justify ContainerUpdate operations. +pub struct ContainerUpdateFromEntriesHandler; + +impl OpHandler for ContainerUpdateFromEntriesHandler { + fn propagate( + &self, + args: &[StatementTmplArg], + store: &mut ConstraintStore, + edb: &dyn EdbView, + ) -> PropagatorResult { + if args.len() != 4 { + return PropagatorResult::Contradiction; + } + + let (new_root, old_root, a_key, a_value) = (&args[0], &args[1], &args[2], &args[3]); + + let new_root_value = match new_root { + StatementTmplArg::Literal(v) => Some(v.clone()), + StatementTmplArg::Wildcard(w) => store.bindings.get(&w.index).cloned(), + _ => None, + }; + let old_root_value = match old_root { + StatementTmplArg::Literal(v) => Some(v.clone()), + StatementTmplArg::Wildcard(w) => store.bindings.get(&w.index).cloned(), + _ => None, + }; + + match (new_root_value, old_root_value) { + (Some(new_root_value), Some(old_root_value)) => { + match (new_root_value.typed(), old_root_value.typed()) { + (TypedValue::Dictionary(new_dict), TypedValue::Dictionary(old_dict)) => { + if let Some(key) = key_from_arg(a_key, store) { + return check_dict_update_for_known_dicts( + new_dict, old_dict, &key, a_value, store, + ); + } + } + // Sets don't support update operations directly (they only have insert/delete) + _ => {} + } + } + _ => {} + } + + // Enumeration: if both roots are unbound wildcards and key/value are known, enumerate candidate root pairs + if let (StatementTmplArg::Wildcard(wnew), StatementTmplArg::Wildcard(wold)) = + (new_root, old_root) + { + if !store.bindings.contains_key(&wnew.index) + && !store.bindings.contains_key(&wold.index) + { + let key_opt = key_from_arg(a_key, store); + let val_opt = match a_value { + StatementTmplArg::Literal(v) => Some(v.clone()), + StatementTmplArg::Wildcard(wv) => store.bindings.get(&wv.index).cloned(), + _ => None, + }; + + if let (Some(key), Some(val)) = (key_opt, val_opt) { + let mut alts = Vec::new(); + for (new_hash, old_hash, src) in edb.enumerate_update_sources(&key, &val) { + let op_tag = match src { + UpdateSource::GeneratedFromFullDict { .. } => { + OpTag::GeneratedContainerUpdate { + new_root: new_hash, + old_root: old_hash, + key: key.clone(), + value: val.clone(), + } + } + UpdateSource::Copied { pod } => OpTag::CopyStatement { source: pod }, + }; + alts.push(crate::prop::Choice { + bindings: vec![ + (wnew.index, new_hash.into()), + (wold.index, old_hash.into()), + ], + op_tag, + }); + } + tracing::trace!( + ?key, + ?val, + candidates = alts.len(), + "Update enum root pairs" + ); + return if alts.is_empty() { + PropagatorResult::Contradiction + } else { + PropagatorResult::Choices { alternatives: alts } + }; + } + } + } + + // Need to handle other missing argument combinations with proper suspension + let waits = crate::prop::wildcards_in_args(args) + .into_iter() + .filter(|i| !store.bindings.contains_key(i)) + .collect::>(); + + if waits.is_empty() { + // All arguments are bound - validate the operation if possible + let new_hash_opt = root_from_arg(new_root, store); + let old_hash_opt = root_from_arg(old_root, store); + let key_opt = key_from_arg(a_key, store); + let val_opt = match a_value { + StatementTmplArg::Literal(v) => Some(v.clone()), + StatementTmplArg::Wildcard(wv) => store.bindings.get(&wv.index).cloned(), + _ => None, + }; + + if let (Some(new_hash), Some(old_hash), Some(key), Some(val)) = + (new_hash_opt, old_hash_opt, key_opt, val_opt) + { + // Check if this update operation is valid by seeing if it exists in sources + for (enum_new, enum_old, _) in edb.enumerate_update_sources(&key, &val) { + if enum_new == new_hash && enum_old == old_hash { + return PropagatorResult::Entailed { + bindings: vec![], + op_tag: OpTag::FromLiterals, + }; + } + } + PropagatorResult::Contradiction + } else { + // Some values couldn't be extracted - contradiction + PropagatorResult::Contradiction + } + } else { + PropagatorResult::Suspend { on: waits } + } + } +} + +fn check_dict_update_for_known_dicts( + new_dict: &Dictionary, + old_dict: &Dictionary, + key: &Key, + a_value: &StatementTmplArg, + store: &ConstraintStore, +) -> PropagatorResult { + // Get the value from the new dictionary (this is the new value that was updated) + let new_dict_value = new_dict.get(&key); + if new_dict_value.is_err() { + return PropagatorResult::Contradiction; + } + let new_dict_value = new_dict_value.unwrap(); + + // Ensure the old dictionary had the key (ContainerUpdate requires the key to exist in old_root) + if old_dict.get(&key).is_err() { + return PropagatorResult::Contradiction; + } + + // Update the old dict with new value and ensure it equals new_dict + let mut updated_dict = old_dict.clone(); + if updated_dict.update(&key, &new_dict_value).is_err() || *new_dict != updated_dict { + return PropagatorResult::Contradiction; + } + + // Check the value matches the expected value + match a_value { + StatementTmplArg::Literal(v) => { + if new_dict_value == v { + PropagatorResult::Entailed { + bindings: vec![], + op_tag: OpTag::FromLiterals, + } + } else { + PropagatorResult::Contradiction + } + } + StatementTmplArg::Wildcard(wv) => { + if let Some(existing) = store.bindings.get(&wv.index) { + if existing == new_dict_value { + PropagatorResult::Entailed { + bindings: vec![], + op_tag: OpTag::FromLiterals, + } + } else { + PropagatorResult::Contradiction + } + } else { + PropagatorResult::Entailed { + bindings: vec![(wv.index, new_dict_value.clone())], + op_tag: OpTag::FromLiterals, + } + } + } + _ => PropagatorResult::Contradiction, + } +} + +/// Register ContainerUpdate handlers with the operation registry. +pub fn register_container_update_handlers(reg: &mut crate::op::OpRegistry) { + reg.register( + NativePredicate::ContainerUpdate, + Box::new(CopyContainerUpdateHandler), + ); + reg.register( + NativePredicate::ContainerUpdate, + Box::new(ContainerUpdateFromEntriesHandler), + ); +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::{edb::ImmutableEdbBuilder, types::ConstraintStore}; + use pod2::middleware::{StatementTmplArg, Value}; + + #[test] + fn test_copy_container_update_handler() { + let mut store = ConstraintStore::default(); + let edb = ImmutableEdbBuilder::new().build(); + let handler = CopyContainerUpdateHandler; + + // Test with correct number of arguments + let new_root = Value::from("new_root_hash".to_string()); + let old_root = Value::from("old_root_hash".to_string()); + let key = Value::from("test_key".to_string()); + let value = Value::from("new_value".to_string()); + + let args = vec![ + StatementTmplArg::Literal(new_root), + StatementTmplArg::Literal(old_root), + StatementTmplArg::Literal(key), + StatementTmplArg::Literal(value), + ]; + + let result = handler.propagate(&args, &mut store, &edb); + + // Should not find anything in empty EDB but shouldn't contradict on valid args + matches!(result, PropagatorResult::Contradiction); + } + + #[test] + fn test_container_update_wrong_arg_count() { + let mut store = ConstraintStore::default(); + let edb = ImmutableEdbBuilder::new().build(); + let handler = ContainerUpdateFromEntriesHandler; + + // Test with wrong number of arguments (should be 4) + let args = vec![ + StatementTmplArg::Literal(Value::from("test".to_string())), + StatementTmplArg::Literal(Value::from("test".to_string())), + ]; + + let result = handler.propagate(&args, &mut store, &edb); + + matches!(result, PropagatorResult::Contradiction); + } +} + diff --git a/core/new_solver/src/handlers/mod.rs b/core/new_solver/src/handlers/mod.rs index 02e522e..7dcc19c 100644 --- a/core/new_solver/src/handlers/mod.rs +++ b/core/new_solver/src/handlers/mod.rs @@ -8,6 +8,10 @@ pub mod contains; pub use contains::register_contains_handlers; pub mod not_contains; pub use not_contains::register_not_contains_handlers; +pub mod container_insert; +pub mod container_update; +pub use container_update::register_container_update_handlers; +pub use container_insert::register_container_insert_handlers; pub mod sumof; pub use sumof::register_sumof_handlers; pub mod productof; diff --git a/core/new_solver/src/op.rs b/core/new_solver/src/op.rs index c147d2a..025332f 100644 --- a/core/new_solver/src/op.rs +++ b/core/new_solver/src/op.rs @@ -29,6 +29,8 @@ impl Default for OpRegistry { crate::handlers::register_signed_by_handlers(&mut reg); crate::handlers::register_contains_handlers(&mut reg); crate::handlers::register_not_contains_handlers(&mut reg); + crate::handlers::register_container_insert_handlers(&mut reg); + crate::handlers::register_container_update_handlers(&mut reg); crate::handlers::register_productof_handlers(&mut reg); crate::handlers::register_maxof_handlers(&mut reg); crate::handlers::register_hashof_handlers(&mut reg); diff --git a/core/new_solver/src/proof_dag.rs b/core/new_solver/src/proof_dag.rs index e897ac7..78c9168 100644 --- a/core/new_solver/src/proof_dag.rs +++ b/core/new_solver/src/proof_dag.rs @@ -50,7 +50,9 @@ impl ProofDag { } OpTag::CopyStatement { .. } | OpTag::FromLiterals - | OpTag::GeneratedContains { .. } => { + | OpTag::GeneratedContains { .. } + | OpTag::GeneratedContainerInsert { .. } + | OpTag::GeneratedContainerUpdate { .. } => { // Leaf; no extra edges } } @@ -225,7 +227,9 @@ impl ProofDagWithOps { } OpTag::CopyStatement { .. } | OpTag::FromLiterals - | OpTag::GeneratedContains { .. } => { + | OpTag::GeneratedContains { .. } + | OpTag::GeneratedContainerInsert { .. } + | OpTag::GeneratedContainerUpdate { .. } => { // Leaves: no premise statements to attach } } @@ -376,6 +380,30 @@ fn short_op_key(tag: &OpTag) -> String { key.name(), value.raw().encode_hex::() ), + OpTag::GeneratedContainerInsert { + new_root, + old_root, + key, + value, + } => format!( + "gen_insert:{}:{}:{}:{}", + new_root.encode_hex::(), + old_root.encode_hex::(), + key.name(), + value.raw().encode_hex::() + ), + OpTag::GeneratedContainerUpdate { + new_root, + old_root, + key, + value, + } => format!( + "gen_update:{}:{}:{}:{}", + new_root.encode_hex::(), + old_root.encode_hex::(), + key.name(), + value.raw().encode_hex::() + ), OpTag::Derived { .. } => "derived".to_string(), OpTag::CustomDeduction { rule_id, .. } => format!("custom:{rule_id:?}"), } @@ -396,6 +424,30 @@ fn short_op_label(tag: &OpTag) -> String { key.name(), value ), + OpTag::GeneratedContainerInsert { + new_root, + old_root, + key, + value, + } => format!( + "GeneratedContainerInsert\nnew=0x{}\\nold=0x{}\\nkey={}\\nvalue={}", + new_root.encode_hex::(), + old_root.encode_hex::(), + key.name(), + value + ), + OpTag::GeneratedContainerUpdate { + new_root, + old_root, + key, + value, + } => format!( + "GeneratedContainerUpdate\nnew=0x{}\\nold=0x{}\\nkey={}\\nvalue={}", + new_root.encode_hex::(), + old_root.encode_hex::(), + key.name(), + value + ), OpTag::Derived { .. } => "Derived".to_string(), OpTag::CustomDeduction { rule_id, .. } => { format!("CustomDeduction: {}", rule_id.predicate().name) diff --git a/core/new_solver/src/replay.rs b/core/new_solver/src/replay.rs index 22e7b55..dfe85cc 100644 --- a/core/new_solver/src/replay.rs +++ b/core/new_solver/src/replay.rs @@ -433,11 +433,78 @@ fn map_to_operation( } Err("SignedBy expects literal message root".to_string()) } - // TODO: Container update predicates should be supported - None | False | ContainerInsert | ContainerDelete | ContainerUpdate - | DictContains | DictNotContains | SetContains | SetNotContains | ArrayContains - | GtEq | Gt | DictInsert | DictUpdate | DictDelete | SetInsert | SetDelete - | ArrayUpdate => Ok(std::option::Option::None), + ContainerInsert => { + // If this was generated from a full dict, emit ContainsFromEntries using the dict value + if let OpTag::GeneratedContainerInsert { + new_root, old_root, .. + } = tag + { + if let (Some(new_dict), Some(old_dict)) = + (edb.full_dict(new_root), edb.full_dict(old_root)) + { + if let Statement::ContainerInsert(_r, _r2, k, v) = head.clone() { + // Expect k and v to be literals here + if let (ValueRef::Literal(kv), ValueRef::Literal(vv)) = (k, v) { + return Ok(Some(Operation( + OperationType::Native( + NativeOperation::ContainerInsertFromEntries, + ), + vec![ + OperationArg::from(Value::from(new_dict)), + OperationArg::from(Value::from(old_dict)), + OperationArg::from(kv), + OperationArg::from(vv), + ], + OperationAux::None, + ))); + } + } + } else { + return Err("missing dictionary for GeneratedContains; cannot replay" + .to_string()); + } + } + Ok(Some(Operation::copy(head.clone()))) + } + ContainerUpdate => { + // If this was generated from a full dict, emit ContainerUpdateFromEntries using the dict value + if let OpTag::GeneratedContainerUpdate { + new_root, old_root, .. + } = tag + { + if let (Some(new_dict), Some(old_dict)) = + (edb.full_dict(new_root), edb.full_dict(old_root)) + { + if let Statement::ContainerUpdate(_r, _r2, k, v) = head.clone() { + // Expect k and v to be literals here + if let (ValueRef::Literal(kv), ValueRef::Literal(vv)) = (k, v) { + return Ok(Some(Operation( + OperationType::Native( + NativeOperation::ContainerUpdateFromEntries, + ), + vec![ + OperationArg::from(Value::from(new_dict)), + OperationArg::from(Value::from(old_dict)), + OperationArg::from(kv), + OperationArg::from(vv), + ], + OperationAux::None, + ))); + } + } + } else { + return Err( + "missing dictionary for GeneratedContainerUpdate; cannot replay" + .to_string(), + ); + } + } + Ok(Some(Operation::copy(head.clone()))) + } + // TODO: Other container predicates should be supported + None | False | ContainerDelete | DictContains | DictNotContains | SetContains + | SetNotContains | ArrayContains | GtEq | Gt | DictInsert | DictUpdate + | DictDelete | SetInsert | SetDelete | ArrayUpdate => Ok(std::option::Option::None), } } _ => Ok(None), @@ -646,6 +713,30 @@ fn order_custom_premises( && arg_matches(&args[1], &a1) && arg_matches(&args[2], &a2) } + (Predicate::Native(NP::PublicKeyOf), Stmt::PublicKeyOf(a0, a1)) => { + let args = tmpl.args(); + arg_matches(&args[0], &a0) && arg_matches(&args[1], &a1) + } + ( + Predicate::Native(NP::ContainerInsert), + Stmt::ContainerInsert(a0, a1, a2, a3), + ) => { + let args = tmpl.args(); + arg_matches(&args[0], &a0) + && arg_matches(&args[1], &a1) + && arg_matches(&args[2], &a2) + && arg_matches(&args[3], &a3) + } + ( + Predicate::Native(NP::ContainerUpdate), + Stmt::ContainerUpdate(a0, a1, a2, a3), + ) => { + let args = tmpl.args(); + arg_matches(&args[0], &a0) + && arg_matches(&args[1], &a1) + && arg_matches(&args[2], &a2) + && arg_matches(&args[3], &a3) + } _ => false, }); if let Some(pos) = matched_pos { diff --git a/core/new_solver/src/types.rs b/core/new_solver/src/types.rs index 0bc656d..8d0e19b 100644 --- a/core/new_solver/src/types.rs +++ b/core/new_solver/src/types.rs @@ -42,6 +42,22 @@ pub enum OpTag { key: Key, value: Value, }, + /// A ContainerInsert premise that is justified because the solver has full dictionaries + /// and can generate the insertion fact (proof attached later at compilation time). + GeneratedContainerInsert { + new_root: Hash, // The Merkle root of the new dictionary + old_root: Hash, // The Merkle root of the old dictionary + key: Key, + value: Value, + }, + /// A ContainerUpdate premise that is justified because the solver has full dictionaries + /// and can generate the update fact (proof attached later at compilation time). + GeneratedContainerUpdate { + new_root: Hash, // The Merkle root of the new dictionary + old_root: Hash, // The Merkle root of the old dictionary + key: Key, + value: Value, // The new value that replaced whatever was at this key + }, } /// Provenance reference to a POD for CopyStatement. diff --git a/core/new_solver/src/util.rs b/core/new_solver/src/util.rs index 972237b..39196df 100644 --- a/core/new_solver/src/util.rs +++ b/core/new_solver/src/util.rs @@ -158,7 +158,10 @@ pub fn proof_cost(store: &ConstraintStore) -> (usize, usize) { q.push_back(p); } } - OpTag::GeneratedContains { .. } | OpTag::FromLiterals => {} + OpTag::GeneratedContains { .. } + | OpTag::GeneratedContainerInsert { .. } + | OpTag::GeneratedContainerUpdate { .. } + | OpTag::FromLiterals => {} } } (seen_stmts.len(), seen_inputs.len()) @@ -270,6 +273,26 @@ pub fn instantiate_goal( let a2 = arg_to_vr(&tmpl.args[2], bindings)?; Some(Statement::HashOf(a0, a1, a2)) } + Predicate::Native(NativePredicate::ContainerInsert) => { + if tmpl.args.len() != 4 { + return None; + } + let a0 = arg_to_vr(&tmpl.args[0], bindings)?; + let a1 = arg_to_vr(&tmpl.args[1], bindings)?; + let a2 = arg_to_vr(&tmpl.args[2], bindings)?; + let a3 = arg_to_vr(&tmpl.args[3], bindings)?; + Some(Statement::ContainerInsert(a0, a1, a2, a3)) + } + Predicate::Native(NativePredicate::ContainerUpdate) => { + if tmpl.args.len() != 4 { + return None; + } + let a0 = arg_to_vr(&tmpl.args[0], bindings)?; + let a1 = arg_to_vr(&tmpl.args[1], bindings)?; + let a2 = arg_to_vr(&tmpl.args[2], bindings)?; + let a3 = arg_to_vr(&tmpl.args[3], bindings)?; + Some(Statement::ContainerUpdate(a0, a1, a2, a3)) + } _ => None, } } From d9f522fd0a7606de36afd759bb123b8d2a089430 Mon Sep 17 00:00:00 2001 From: Evan Laufer Date: Mon, 15 Sep 2025 14:04:50 -0700 Subject: [PATCH 2/2] Clippy --- .../src/handlers/container_insert.rs | 37 +++++++++---------- .../src/handlers/container_update.rs | 36 ++++++++---------- core/new_solver/src/handlers/mod.rs | 2 +- 3 files changed, 33 insertions(+), 42 deletions(-) diff --git a/core/new_solver/src/handlers/container_insert.rs b/core/new_solver/src/handlers/container_insert.rs index ef7eeab..ffb9a60 100644 --- a/core/new_solver/src/handlers/container_insert.rs +++ b/core/new_solver/src/handlers/container_insert.rs @@ -114,27 +114,24 @@ impl OpHandler for ContainerInsertFromEntriesHandler { _ => None, }; - match (new_root_value, old_root_value) { - (Some(new_root_value), Some(old_root_value)) => { - match (new_root_value.typed(), old_root_value.typed()) { - (TypedValue::Dictionary(new_dict), TypedValue::Dictionary(old_dict)) => { - if let Some(key) = key_from_arg(a_key, store) { - return check_dict_insert_for_known_dicts( - new_dict, old_dict, &key, a_val, store, - ); - } + if let (Some(new_root_value), Some(old_root_value)) = (new_root_value, old_root_value) { + match (new_root_value.typed(), old_root_value.typed()) { + (TypedValue::Dictionary(new_dict), TypedValue::Dictionary(old_dict)) => { + if let Some(key) = key_from_arg(a_key, store) { + return check_dict_insert_for_known_dicts( + new_dict, old_dict, &key, a_val, store, + ); } - (TypedValue::Set(new_set), TypedValue::Set(old_set)) => { - if let Some(result) = - check_set_insert_for_known_set(new_set, old_set, a_key, a_val, store) - { - return result; - }; - } - _ => {} } + (TypedValue::Set(new_set), TypedValue::Set(old_set)) => { + if let Some(result) = + check_set_insert_for_known_set(new_set, old_set, a_key, a_val, store) + { + return result; + }; + } + _ => {} } - _ => {} } // Enumeration: if both roots are unbound wildcards and key/value are known, enumerate candidate root pairs @@ -235,7 +232,7 @@ fn check_dict_insert_for_known_dicts( store: &ConstraintStore, ) -> PropagatorResult { // get the value from the new_dict - let dict_value = new_dict.get(&key); + let dict_value = new_dict.get(key); if dict_value.is_err() { return PropagatorResult::Contradiction; } @@ -243,7 +240,7 @@ fn check_dict_insert_for_known_dicts( // insert the value into the old dict and ensure equal to new_dict let mut old_dict = old_dict.clone(); - if old_dict.insert(&key, &dict_value).is_err() || *new_dict != old_dict { + if old_dict.insert(key, dict_value).is_err() || *new_dict != old_dict { return PropagatorResult::Contradiction; } diff --git a/core/new_solver/src/handlers/container_update.rs b/core/new_solver/src/handlers/container_update.rs index c51eae9..451931f 100644 --- a/core/new_solver/src/handlers/container_update.rs +++ b/core/new_solver/src/handlers/container_update.rs @@ -2,6 +2,8 @@ use pod2::middleware::{ containers::Dictionary, Key, NativePredicate, StatementTmplArg, TypedValue, }; +// Import utilities from container_insert module +use super::container_insert::{key_from_arg, root_from_arg}; use super::util::{arg_to_selector, handle_copy_results}; use crate::{ edb::{EdbView, UpdateSource}, @@ -10,9 +12,6 @@ use crate::{ types::{ConstraintStore, OpTag}, }; -// Import utilities from container_insert module -use super::container_insert::{key_from_arg, root_from_arg}; - /// Copy existing ContainerUpdate(new_root, old_root, key, value) statements from EDB. pub struct CopyContainerUpdateHandler; @@ -74,21 +73,16 @@ impl OpHandler for ContainerUpdateFromEntriesHandler { _ => None, }; - match (new_root_value, old_root_value) { - (Some(new_root_value), Some(old_root_value)) => { - match (new_root_value.typed(), old_root_value.typed()) { - (TypedValue::Dictionary(new_dict), TypedValue::Dictionary(old_dict)) => { - if let Some(key) = key_from_arg(a_key, store) { - return check_dict_update_for_known_dicts( - new_dict, old_dict, &key, a_value, store, - ); - } - } - // Sets don't support update operations directly (they only have insert/delete) - _ => {} + if let (Some(new_root_value), Some(old_root_value)) = (new_root_value, old_root_value) { + if let (TypedValue::Dictionary(new_dict), TypedValue::Dictionary(old_dict)) = + (new_root_value.typed(), old_root_value.typed()) + { + if let Some(key) = key_from_arg(a_key, store) { + return check_dict_update_for_known_dicts( + new_dict, old_dict, &key, a_value, store, + ); } } - _ => {} } // Enumeration: if both roots are unbound wildcards and key/value are known, enumerate candidate root pairs @@ -190,20 +184,20 @@ fn check_dict_update_for_known_dicts( store: &ConstraintStore, ) -> PropagatorResult { // Get the value from the new dictionary (this is the new value that was updated) - let new_dict_value = new_dict.get(&key); + let new_dict_value = new_dict.get(key); if new_dict_value.is_err() { return PropagatorResult::Contradiction; } let new_dict_value = new_dict_value.unwrap(); // Ensure the old dictionary had the key (ContainerUpdate requires the key to exist in old_root) - if old_dict.get(&key).is_err() { + if old_dict.get(key).is_err() { return PropagatorResult::Contradiction; } // Update the old dict with new value and ensure it equals new_dict let mut updated_dict = old_dict.clone(); - if updated_dict.update(&key, &new_dict_value).is_err() || *new_dict != updated_dict { + if updated_dict.update(key, new_dict_value).is_err() || *new_dict != updated_dict { return PropagatorResult::Contradiction; } @@ -254,9 +248,10 @@ pub fn register_container_update_handlers(reg: &mut crate::op::OpRegistry) { #[cfg(test)] mod tests { + use pod2::middleware::{StatementTmplArg, Value}; + use super::*; use crate::{edb::ImmutableEdbBuilder, types::ConstraintStore}; - use pod2::middleware::{StatementTmplArg, Value}; #[test] fn test_copy_container_update_handler() { @@ -300,4 +295,3 @@ mod tests { matches!(result, PropagatorResult::Contradiction); } } - diff --git a/core/new_solver/src/handlers/mod.rs b/core/new_solver/src/handlers/mod.rs index 7dcc19c..b6ef496 100644 --- a/core/new_solver/src/handlers/mod.rs +++ b/core/new_solver/src/handlers/mod.rs @@ -10,8 +10,8 @@ pub mod not_contains; pub use not_contains::register_not_contains_handlers; pub mod container_insert; pub mod container_update; -pub use container_update::register_container_update_handlers; pub use container_insert::register_container_insert_handlers; +pub use container_update::register_container_update_handlers; pub mod sumof; pub use sumof::register_sumof_handlers; pub mod productof;