From 95ecf72616299dcc907af345b582af32b64c5b67 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Fri, 30 Oct 2026 14:02:10 +0100 Subject: [PATCH 1/4] test(od-ontology): Gate A behavioral loss and source-qualification falsifiers --- .../tests/d_behavior_eqsat_gate_a.rs | 270 ++++++++++++++++++ 1 file changed, 270 insertions(+) create mode 100644 crates/od-ontology/tests/d_behavior_eqsat_gate_a.rs diff --git a/crates/od-ontology/tests/d_behavior_eqsat_gate_a.rs b/crates/od-ontology/tests/d_behavior_eqsat_gate_a.rs new file mode 100644 index 0000000..93a3514 --- /dev/null +++ b/crates/od-ontology/tests/d_behavior_eqsat_gate_a.rs @@ -0,0 +1,270 @@ +//! D-BEHAVIOR-EQSAT-0 / Gate A. Test-only, source-qualified behavioral loss. +//! +//! This deliberately reuses the #44 DR64 and DT registry helpers and #46's +//! source-only example. No new graph/schema, source interpreter or Odoo trace. +//! Source blob: data/account_move.spo.ndjson +//! 459659e1c1ece2303de2bc3c8eab715c27e6c53d (baseline #46). +//! A coarse relation proves a dependency, never effect order or authority. + +use std::collections::{BTreeMap, BTreeSet}; + +use od_ontology::{parse_ndjson, RecomputeDag, Triple}; +use serde_json::Value; + +mod common; +use common::cube::{facts, registry, strip, CLASS, UNATTESTED}; +use common::dr64::{compose_blocked, store, Blocked, Dom, Operand2, W}; + +const SOURCE: &str = include_str!("../../../data/account_move.spo.ndjson"); +const EXAMPLE: &str = include_str!("../../../docs/examples/odoo-codegraph-harvest-v1.example.json"); +const FIELD: &str = "account_move.currency_id"; +const COMPUTE: &str = "account_move._compute_currency_id"; +const ONCHANGE: &str = "account_move._onchange_invoice_vendor_bill"; + +fn source_writers(ts: &[Triple]) -> BTreeSet { + ts.iter() + .filter(|t| t.p == "emitted_by" && strip(&t.s) == FIELD) + .map(|t| strip(&t.o).to_owned()) + .collect() +} + +fn exported_writers(graph: &Value) -> BTreeSet { + graph["edges"] + .as_array() + .expect("the existing #46 example has edges") + .iter() + .filter(|e| { + e["kind"] == "emitted_by" + && e["source"] == "field:account.move:currency_id" + }) + .filter_map(|e| e["target"].as_str()) + .map(|s| s.replace("method:account.move:", "account_move.")) + .collect() +} + +/// Compares an independent source reference with a projection. This is the +/// load-bearing admission check: an omitted emitter cannot be accepted. +fn require_all_emitters( + expected: &BTreeSet, + projected: &BTreeSet, +) -> Result<(), &'static str> { + if expected == projected { + Ok(()) + } else { + Err("source_declared_emitter_mismatch") + } +} + +#[test] +fn source_codegraph_and_dt_registry_retain_both_currency_methods() { + let ts = parse_ndjson(SOURCE).expect("pinned source corpus parses"); + let source = source_writers(&ts); + assert_eq!( + source, + BTreeSet::from([COMPUTE.to_owned(), ONCHANGE.to_owned()]), + "the source oracle has exactly these distinct declared writers" + ); + + let example: Value = serde_json::from_str(EXAMPLE).unwrap(); + assert_eq!(example["metadata"]["snapshot_kind"], "source_harvest"); + assert!(example["metadata"].get("registry_snapshot").is_none()); + let projected = exported_writers(&example); + require_all_emitters(&source, &projected).unwrap(); + + let f = facts(); + let reg = registry(&f); + let do_position = reg.do_.get(FIELD).expect("existing DO position"); + let from_registry: BTreeSet = reg + .live(1) + .iter() + .filter(|((class, cell), _)| class == CLASS && cell.do_ == do_position) + .flat_map(|(_, methods)| methods.iter().cloned()) + .collect(); + require_all_emitters(&source, &from_registry).unwrap(); + + // Falsifier 1: omit either emitter, independent of JSON syntax validity. + for dropped in [COMPUTE, ONCHANGE] { + let mut damaged = projected.clone(); + assert!(damaged.remove(dropped)); + assert_eq!( + require_all_emitters(&source, &damaged), + Err("source_declared_emitter_mismatch") + ); + } + // Missing trigger is not evidence that the onchange does not exist. + let unattested = reg.on.get(UNATTESTED).unwrap(); + assert!(reg.live(1).iter().any(|((_, c), methods)| { + c.on == unattested && methods.contains(ONCHANGE) + })); +} + +type Pairs = BTreeSet<(String, String)>; + +/// Independently enumerated source relation. No DR kernel, RecomputeDag, +/// registry helper, or shared join iterator participates in this oracle. +fn enumerate_dependencies(ts: &[Triple]) -> (Pairs, Vec, Vec, Blocked, Blocked) { + let mut emit: BTreeMap> = BTreeMap::new(); + let mut read: BTreeMap> = BTreeMap::new(); + for t in ts { + if t.p == "emitted_by" { + emit.entry(strip(&t.s).to_owned()) + .or_default() + .insert(strip(&t.o).to_owned()); + } + if t.p == "reads_field" { + read.entry(strip(&t.o).to_owned()) + .or_default() + .insert(strip(&t.s).to_owned()); + } + } + let fields: Vec = emit + .keys() + .filter(|field| read.contains_key(*field)) + .cloned() + .collect(); + let methods: Vec = fields + .iter() + .flat_map(|f| emit[f].iter().chain(read[f].iter()).cloned()) + .collect::>() + .into_iter() + .collect(); + + let mut left = Blocked::new(methods.len(), fields.len()); + let mut right = Blocked::new(fields.len(), methods.len()); + let mut expected = Pairs::new(); + for (fi, field) in fields.iter().enumerate() { + for producer in &emit[field] { + let pi = methods.binary_search(producer).unwrap(); + left.set(pi, fi); + for consumer in &read[field] { + if producer != consumer { + expected.insert((producer.clone(), consumer.clone())); + } + } + } + for consumer in &read[field] { + let ci = methods.binary_search(consumer).unwrap(); + right.set(fi, ci); + } + } + (expected, methods, fields, left, right) +} + +#[test] +fn independent_enumeration_matches_dr_but_single_emitter_dag_loses_edges() { + let ts = parse_ndjson(SOURCE).unwrap(); + let (expected, methods, fields, emits, read_by) = enumerate_dependencies(&ts); + assert!(methods.len() <= W && fields.len() <= W, "slice 1 fits DR64"); + let st = store(); + let e = Operand2 { rel: &emits, row: Dom::Method, col: Dom::Field, ordinal: 0 }; + let r = Operand2 { rel: &read_by, row: Dom::Field, col: Dom::Method, ordinal: 1 }; + let (composed, _) = compose_blocked(&st, &e, &r); + let composed = composed.without_diagonal(); + + assert_eq!(composed.count(), expected.len()); + for (i, from) in methods.iter().enumerate() { + for (j, to) in methods.iter().enumerate() { + assert_eq!( + composed.get(i, j), + expected.contains(&(from.clone(), to.clone())), + "DR64 disagrees with independently enumerated {from} -> {to}" + ); + } + } + + let dag = RecomputeDag::from_triples(&ts); + let missing: Pairs = expected + .iter() + .filter(|(from, to)| !dag.has_edge(from, to)) + .cloned() + .collect(); + assert_eq!(dag.edge_count(), 44, "reproduce merged #44 baseline"); + assert_eq!(missing.len(), 26, "reproduce merged #44 loss, not a DR error"); + assert!( + expected.iter().all(|(from, to)| { + !dag.has_edge(from, to) || composed.get( + methods.binary_search(from).unwrap(), + methods.binary_search(to).unwrap(), + ) + }), + "the reduced DAG must not invent dependencies" + ); +} + +#[derive(Clone, Copy)] +enum Effect { + Set(i64), + Add(i64), +} + +fn run_ordered(initial: i64, ops: &[Effect]) -> i64 { + ops.iter().fold(initial, |state, effect| match effect { + Effect::Set(v) => *v, + Effect::Add(v) => state + v, + }) +} + +#[test] +fn unordered_spo_cannot_certify_effect_order_or_runtime_observation() { + // Synthetic scalar falsifier, NOT an observed Odoo execution trace. + let first = [Effect::Set(1), Effect::Add(1)]; + let reordered = [Effect::Add(1), Effect::Set(1)]; + assert_eq!(run_ordered(0, &first), 2); + assert_eq!(run_ordered(0, &reordered), 1); + // Both have the same unordered operation-kind set. + let coarse = BTreeSet::from(["Add", "Set"]); + assert_eq!(coarse, BTreeSet::from(["Set", "Add"])); + // The #46 source-only example contains no Odoo runtime attestation. + let example: Value = serde_json::from_str(EXAMPLE).unwrap(); + assert_eq!(example["metadata"]["snapshot_kind"], "source_harvest"); + assert!(example["metadata"].get("registry_snapshot").is_none()); + // None = UNKNOWN. A missing trigger/permission/effect-order witness must + // not silently be admitted as either TRUE or FALSE. + let trigger: Option = None; + let permission: Option = None; + let ordered_effects_witness: Option = None; + assert_ne!(trigger, Some(true)); + assert_ne!(trigger, Some(false)); + assert_ne!(permission, Some(true)); + assert_ne!(ordered_effects_witness, Some(true)); + let missing = example["metadata"]["coverage"]["missing_facts"] + .as_array() + .unwrap() + .iter() + .filter_map(Value::as_str) + .collect::>() + .join(" "); + assert!(missing.contains("trigger") && missing.contains("ACL")); +} + +#[test] +fn inherit_and_inherits_cannot_be_disambiguated_from_coarse_predicate() { + // The existing Ruff/Odoo upstream lift maps both source forms to the + // same `inherits_from` predicate (od-ontology/src/inheritance.rs). + // This is a synthetic non-injectivity proof, not a claim of one Odoo + // instance's effective MRO or delegation registry. + fn coarse_lift(kind: &str) -> &'static str { + match kind { + "_inherit" | "_inherits" => "inherits_from", + _ => panic!("not a tested Odoo source form"), + } + } + assert_eq!(coarse_lift("_inherit"), coarse_lift("_inherits")); + // Yet these have distinct method-inheritance semantics. + fn inherits_python_methods(kind: &str) -> bool { + kind == "_inherit" + } + assert!(inherits_python_methods("_inherit")); + assert!(!inherits_python_methods("_inherits")); + // The projected triple alone is insufficient to authorize method + // inheritance. Neither C3 nor relation composition repairs erased kind. + let projected = r#"{"s":"odoo:child","p":"inherits_from","o":"odoo:parent","f":1.0,"c":1.0}"#; + let ts = parse_ndjson(projected).unwrap(); + assert_eq!(ts.len(), 1); + assert_eq!(ts[0].p, "inherits_from"); + assert!(!projected.contains("_inherits")); + assert!(!projected.contains("_inherit\\\"")); + // No source-kind witness exists here: classification must remain UNKNOWN. + let witnessed_kind: Option<&str> = None; + assert_eq!(witnessed_kind, None); +} From 3b39fe87d456e7edb4c4ee03ef9dc80684044ace Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Fri, 30 Oct 2026 14:03:02 +0100 Subject: [PATCH 2/4] docs: record Gate A source-qualified loss and cross-domain stop gate --- docs/D-BEHAVIOR-EQSAT-0-GATE-A.md | 75 +++++++++++++++++++++++++++++++ 1 file changed, 75 insertions(+) create mode 100644 docs/D-BEHAVIOR-EQSAT-0-GATE-A.md diff --git a/docs/D-BEHAVIOR-EQSAT-0-GATE-A.md b/docs/D-BEHAVIOR-EQSAT-0-GATE-A.md new file mode 100644 index 0000000..795e83f --- /dev/null +++ b/docs/D-BEHAVIOR-EQSAT-0-GATE-A.md @@ -0,0 +1,75 @@ +# D-BEHAVIOR-EQSAT-0 — Gate A, behavioral non-injectivity + +**Status:** Gate A test-only candidate, **UNVERIFIED until CI runs**. 2026-10-30. No changes to production code, data, source vocabularies, Odoo registry, DR/DT, Ruff, OGAR, KinaXe, egglog or MLIR. No effective Odoo installation or execution trace is claimed. + +## Source / revision pins + +- odoo-rs #44 merged `a59f9e8be01ecf8e0342afa3b84ed989bd5de2fe`; #45 merged `7737a129491a289efde339e3e719539ec662b9b0`; #46 merged `558f12ac65c6c1c4667e1eb28f34c6a4f9c5647b`. +- `data/account_move.spo.ndjson` blob `459659e1c1ece2303de2bc3c8eab715c27e6c53d`. +- `data/odoo_inheritance_manifest.ndjson` blob `becf51e7f73faff45da3f7a17f518048eac0d942`. +- Existing `docs/examples/odoo-codegraph-harvest-v1.example.json` is illustrative **source only**; its `metadata.revision` is #45's merged commit. It is not an Odoo runtime export. +- Ruff #125 (`ruff_metta_spo`) and #127 (`Predicate::role`) merged. No Ruff vocabulary changes here. +- lance-graph #1849/#1850–#1853, ndarray #400, OGAR #357/#363 and KinaXe #21/#22 are reference owners, not modified dependencies beyond existing test-only `dr-math-binding-probe`. + +## Reused surfaces and result contract + +| Existing surface | What is checked | What is NOT implied | +|---|---|---| +| `od_ontology::parse_ndjson` | Original `emitted_by` and `reads_field` triples | Complete method bodies | +| #46 source example | Two separate `account_move.currency_id` emitter edges | Effective Odoo registry observation | +| #44 `RecomputeDag` | Last-emitter-only ordering subset | Complete behavioral ordering | +| #44 `common::dr64::{Blocked, compose_blocked}` | Boolean relation composition | Runtime effects, dispatch or triggers | +| #45 `common::cube::{facts, registry, live}` | Same-version coexistence in candidate ON/WHEN/DO registry | Verified authority for the `unattested` ON | +| Ruff #127 role vocabulary | `emitted_by` is effect, `reads_field` is read | Evidence that absence of calls/triggers/ACL proves purity | + +Independent reference: pair-by-pair enumeration of every `emitted_by` producer and `reads_field` consumer for each shared field. This shares no DR composition code and does not use `RecomputeDag`. + +**Expected historical acceptance:** slice 1 has 44 `RecomputeDag` edges plus 26 further distinct edges in the full composition; the executable test pins those counts and asks the independently enumerated pairs to match every DR bit. Do not substitute the old test's output for a new run. + +## Behavioral information loss: at least two different kinds + +1. **Emitter multiplicity.** `account_move.currency_id` has two distinct source-declared methods, `_compute_currency_id` and `_onchange_invoice_vendor_bill`. Dropping either from the #46 source projection must be rejected. On this corpus, `RecomputeDag` keeps only the last emitter of a field and misses 26 ordering candidates in slice 1. A complete Boolean composition restores candidate dependencies, not method execution. +2. **Inheritance kind.** `od-ontology/src/inheritance.rs` explicitly notes that Ruff's upstream lift sends both `_inherit` and `_inherits` into `inherits_from`. But `_inherit` participates in Python method inheritance, while `_inherits` delegates fields and does not inherit those Python methods. Thus two behaviorally distinct source declarations map to the same triple: the lift is not injective. Neither C3 nor DR relation composition can recover which source form was used. Gate A therefore **STOPS** at this boundary pending a source-qualified declaration-kind witness. This does not authorize a new Ruff predicate, alternative ontology or canonical IR. +3. **Effect order.** A *synthetic only* scalar example `Set(1); Add(1)` produces 2, whereas `Add(1); Set(1)` produces 1, despite having the same unordered operation names. No Odoo body order was obtained from the coarse source corpus, so applying this equivalence to real methods is UNKNOWN. +4. **Authority / unknownness.** Source harvesting lacks a pinned effective Odoo registry, installed-addon ordering, some triggers, permissions, body writes and calls. `UNATTESTED` must not be reinterpreted as an automatic event, FALSE or a passed authorization guard. The #46 sample supplies no runtime observation. + +## Negative controls and CI + +The test-only file `crates/od-ontology/tests/d_behavior_eqsat_gate_a.rs` exercises: + +- independent source corpus vs source-only example vs DT registry emitter parity, with two deliberate deleted-emitter negative cases; +- DR64 composition vs independent enumeration, while quantifying the `RecomputeDag` information deficit; +- a noncommuting effect order counterexample, labelled synthetic rather than an Odoo trace; +- `_inherit` / `_inherits` projection collision, with UNKNOWN source mode; +- unknown triggers, permissions and absent effective-registry witness. + +**Load-bearing disable candidate:** replace `require_all_emitters`'s comparison with unconditional `Ok(())`. The deleted-emitter negative test must turn red. **Not claimed executed** until a reproducible CI or local run verifies it. + +Reproduction requested: + +```sh +cargo test -p od-ontology --test dt64_relcomp_parity --test dt64_on_when_do_cube +cargo test -p od-ontology --test d_behavior_eqsat_gate_a -- --nocapture +``` + +The workspace's existing clippy `doc_markdown` finding from #44 may still affect `-D warnings`. Test compilation, execution, timing, allocations and copied bytes are not measured by this document. + +## Cross-domain contract inventory (research only) + +| Consumer | Shared candidates | Missing before genuine behavioral lowering | +|---|---|---| +| Odoo | `MethodId`, `emitted_by`/`reads_field`, `Live` registry, `DR relcomp`, C3 | Source-declaration kind, ordered body effects, effective registry/version and permission witness | +| HIRO/MARS | ON event, WHEN precondition, DO capability and OGIT permitted edges (OGAR #363) | Attested handler semantics, installation identity and permission check; schema declaration is not a run | +| Ruff MeTTa | #125 parsed rules, engine-specific `Lowerable` / `InterpreterOnly`; #127 closed predicate roles | Existing ModelGraph projection does not carry call edges/verdicts; variable bindings, quotation and effects need an independent engine oracle | +| KPEA | KinaXe #24/#25 read-only method graph (subsequently merged); frozen KPEA oracle, `kinaxe-meta` provenance | No inferred biological effect from source, no replacement for source/evidence roots, no registry-validated ClassId/MethodId | +| egglog / MLIR | Optional cold optimization for already admitted pure expressions | Independent rewrite-law certification, typed proof witness, actual supported IR and execution parity; **not examined by Gate A** | + +## Decision: STOP at Gate A loss, do not start B–E in this branch + +The smallest missing interface is **not** another graph. It is a read-only, source-qualified *declaration-kind and effect-order witness* associated with the existing method/source identities and versions; unknown kinds and absent order must refuse behavioral lowering. The authoritative owner is Ruff for the source harvest, Odoo for interpreting Odoo declarations, and DR/DT for eventual admission. + +**Falsifier for that interface:** present one `_inherit` and one `_inherits` relationship with equal `inherits_from` endpoints and the same graph neighborhood. Both coarse triples are identical. Method-inheritance eligibility must differ only when a separately verified declaration-kind witness is supplied. Without it, both remain UNKNOWN, not interchangeable. + +After the owner decides how the witness is carried, a **MeTTa harvesting comparison** is the next best *research* gate, since Ruff #125 already provides a conservative engine-specific lowerability classifier. KPEA CodeGraph can follow, but proof-backed MLIR lowering must wait for independently admitted pure semantics. No new source vocabulary or implementation is authorized here. + +No automatic merge. From 982d629d8678f5f2abce61ef084b59ab866ee259 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Fri, 30 Oct 2026 14:03:25 +0100 Subject: [PATCH 3/4] test: remove redundant string-escape assertion --- crates/od-ontology/tests/d_behavior_eqsat_gate_a.rs | 2 -- 1 file changed, 2 deletions(-) diff --git a/crates/od-ontology/tests/d_behavior_eqsat_gate_a.rs b/crates/od-ontology/tests/d_behavior_eqsat_gate_a.rs index 93a3514..4d2edc1 100644 --- a/crates/od-ontology/tests/d_behavior_eqsat_gate_a.rs +++ b/crates/od-ontology/tests/d_behavior_eqsat_gate_a.rs @@ -262,8 +262,6 @@ fn inherit_and_inherits_cannot_be_disambiguated_from_coarse_predicate() { let ts = parse_ndjson(projected).unwrap(); assert_eq!(ts.len(), 1); assert_eq!(ts[0].p, "inherits_from"); - assert!(!projected.contains("_inherits")); - assert!(!projected.contains("_inherit\\\"")); // No source-kind witness exists here: classification must remain UNKNOWN. let witnessed_kind: Option<&str> = None; assert_eq!(witnessed_kind, None); From 1975536cc90e77d917fac4aa54c7f973563e1409 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Fri, 30 Oct 2026 14:05:27 +0100 Subject: [PATCH 4/4] docs: independently verify Odoo Gate A source census and loss baseline --- docs/D-BEHAVIOR-EQSAT-0-GATE-A.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/docs/D-BEHAVIOR-EQSAT-0-GATE-A.md b/docs/D-BEHAVIOR-EQSAT-0-GATE-A.md index 795e83f..dadf403 100644 --- a/docs/D-BEHAVIOR-EQSAT-0-GATE-A.md +++ b/docs/D-BEHAVIOR-EQSAT-0-GATE-A.md @@ -26,6 +26,19 @@ Independent reference: pair-by-pair enumeration of every `emitted_by` producer a **Expected historical acceptance:** slice 1 has 44 `RecomputeDag` edges plus 26 further distinct edges in the full composition; the executable test pins those counts and asks the independently enumerated pairs to match every DR bit. Do not substitute the old test's output for a new run. +## Independent source-census verification (completed) + +The source blob was read anew through the GitHub connector and parsed as NDJSON in an independent JavaScript enumeration, without calling any Rust DR or RecomputeDag implementation. On the exact blob SHA above: + +- 1,825 source triples; +- 34 fields both emitted and read; +- 70 distinct non-reflexive producer → reader pairs by enumerating every emitter for each field; +- 44 distinct pairs using the existing last-emitter-per-field rule; +- **26 lost pairs** and zero last-emitter pairs absent from the complete set; +- the two exact `currency_id` writers match the #46 illustrative export, in both identities and multiplicity. + +This validates the input/oracle reference and historical #44 counts independently; **it does not run or validate the newly written Rust DR test**, so its pass/fail status remains unverified until Cargo/CI runs. + ## Behavioral information loss: at least two different kinds 1. **Emitter multiplicity.** `account_move.currency_id` has two distinct source-declared methods, `_compute_currency_id` and `_onchange_invoice_vendor_bill`. Dropping either from the #46 source projection must be rejected. On this corpus, `RecomputeDag` keeps only the last emitter of a field and misses 26 ordering candidates in slice 1. A complete Boolean composition restores candidate dependencies, not method execution.