From 63d27f35e07f97bcfeb27bef7eccd8d02d67e6d2 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Thu, 22 Oct 2026 16:46:02 +0200 Subject: [PATCH] test(dr-math): ClassView-to-ACT-R handoff with isolated CI and remaining gates --- .github/workflows/dr-math-binding-probe.yml | 28 +++++ crates/dr-math-binding-probe/Cargo.toml | 3 + .../dr-math-binding-probe/END_TO_END_GATES.md | 53 ++++++++ .../tests/contract_handoff.rs | 113 ++++++++++++++++++ 4 files changed, 197 insertions(+) create mode 100644 .github/workflows/dr-math-binding-probe.yml create mode 100644 crates/dr-math-binding-probe/END_TO_END_GATES.md create mode 100644 crates/dr-math-binding-probe/tests/contract_handoff.rs diff --git a/.github/workflows/dr-math-binding-probe.yml b/.github/workflows/dr-math-binding-probe.yml new file mode 100644 index 000000000..0775fe8ec --- /dev/null +++ b/.github/workflows/dr-math-binding-probe.yml @@ -0,0 +1,28 @@ +name: DR Mathematical Binding Probe +on: + push: + paths: + - "crates/dr-math-binding-probe/**" + - "crates/lance-graph-contract/**" + - "crates/lance-graph-act-r/**" + - ".github/workflows/dr-math-binding-probe.yml" + pull_request: + paths: + - "crates/dr-math-binding-probe/**" + - "crates/lance-graph-contract/**" + - "crates/lance-graph-act-r/**" + - ".github/workflows/dr-math-binding-probe.yml" +jobs: + isolated-probe: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: dtolnay/rust-toolchain@stable + with: + components: clippy, rustfmt + - name: Format + run: cargo fmt --manifest-path crates/dr-math-binding-probe/Cargo.toml --all -- --check + - name: Clippy + run: cargo clippy --manifest-path crates/dr-math-binding-probe/Cargo.toml --all-targets -- -D warnings + - name: Tests + run: cargo test --manifest-path crates/dr-math-binding-probe/Cargo.toml diff --git a/crates/dr-math-binding-probe/Cargo.toml b/crates/dr-math-binding-probe/Cargo.toml index 4969346c0..1ee8ff503 100644 --- a/crates/dr-math-binding-probe/Cargo.toml +++ b/crates/dr-math-binding-probe/Cargo.toml @@ -10,3 +10,6 @@ description = "Borrowed DR64 / ClassView-style typed structure and source witnes [dependencies] lance-graph-contract = { path = "../lance-graph-contract" } + +[dev-dependencies] +lance-graph-act-r = { path = "../lance-graph-act-r" } diff --git a/crates/dr-math-binding-probe/END_TO_END_GATES.md b/crates/dr-math-binding-probe/END_TO_END_GATES.md new file mode 100644 index 000000000..5acb4c3b4 --- /dev/null +++ b/crates/dr-math-binding-probe/END_TO_END_GATES.md @@ -0,0 +1,53 @@ +# D-DRMC-4 — integration, harvesting and downstream acceptance + +**Status: STAGED LAB TEST + FUTURE DEPENDENCY MATRIX, not production completion.** + +## What this stacked PR actually exercises + +- An actual `ClassView` fixture declares `memberOf -> effectiveRoles` via the existing `compute_dag` method and its Kahn-order contract. +- Stage 1 binds typed `Identity×Property` DR64 planes as borrowed words against caller-supplied source/map/focus/scope numbers. +- Stage 2 compares constrained finite-focus observations to reference mask counting (and its scalar differential tests). +- Stage 3 gates a *synthetic* mathematical proof reference against a distinct compiled artifact identity. **The checked proof flag is not real checker attestation.** +- The existing `lance-graph-act-r` crate accepts eligible outputs to arbitrate a deterministic decision proposal and refuses a changed snapshot. No ActionDef or write, no Cognitive Shader Driver dependency. + +This tests boundary shapes and refusals only. It does **not** run an egglog theorem compiler, execute R2IL, attest a Lance snapshot or execute a real class method. A positive CI job is *not* the science result. + +## Remaining staged, independently owned gates + +| Gate | Reused owner / implementation | Proof or falsifier | +| --- | --- | --- | +| G0 Class method -> operation | `class_view::compute_dag`; D-QSP/D-RFT #1667 and EXO-121 | Method-specific law, declared dependencies, non-participating fields, no semantic label inside hot register | +| G1 Real source / map seal | OGAR, D-RMAP-1A separate RelationshipMaps/MapPalettes, Quack binding | Immutable dataset+branch+version; map/index row-address seal; scope/ACL; coordinate rollover; >64 focus frontier; no invented foreign gather | +| G2 Discovery and constraint scope | DR bounded register + independent population observer | Empty/unknown/one false/out-of-focus counterexample, bag vs distinct; held-out reality generalization explicitly separate | +| G3 Oracle intake | MeTTa declaration frontend; MORK/PathMap unification; datafrog recursion; scalar/PG K3 | Count Set and BAG separately; output identity vs support; per-loop cycle; no self-support/negative recursion silently accepted | +| G4 Candidate rewrite discovery | Ruler/Enumo-style rule proposal, `set_rules`, egglog | Type/sort and arithmetic law guards, explicit premise consistency, finite fuel, independent oracle differential | +| G5 Effect-safe extraction | eggcc-inspired stateful extraction / GKAT `gkat-probe` | Prefetch and source/permission gates not reordered; K3 guard valid; side-effect proposal not committed; causal assumptions declared | +| G6 Certified compilation | `egglog-r2il-probe` #1690–#1698 (owner) | External portable proof checker, range/overflow/domain witness, checked target ABI, reproducible law/compiler version | +| G7 Physical execution | R2IL/Quack lowering → mask-risc/ndarray SIMD; direct prepared-DR native folds | Same answer vs independent oracle; no second hot evaluator; count bind/index/readahead/prefetch/scratch/output costs | +| G8 Deterministic orchestration | ACT-R, Rubicon, Kanban, cognitive-shader-driver; Thought-Git separate | Stale eligibility refusal; proposal vs action permission vs commit receipts; replay traces and separate writing authority | +| G9 Heritage and cross-domain reuse | Thought-Git audit references; proposed 27-atom hypothesis | Historical source quotation/attribution separately verified; one law + proof + compiled recipe, two different classes and snapshots; counterexample discovers bad abstraction | + +### Math heritage example (not implemented) + +A *product rule* ascribed to Leibniz is a source lead. Only after faithful source transcription, formal differentiation semantics, independent proof, domain constraints and target lowering may it be called a compiled theorem. Merely storing a label `Leibniz` or egglog rendering a term is no certificate. The 27 mathematical low-code atoms are a falsifiable empirical compression *hypothesis*; measure coverage over published proofs, not a universal basis claim. + +### Performance / amortization + +Design a controlled 256-rule × 4096-frame experiment with a baseline that must include non-sharing, cold compile/certification, binding/index building, source snapshot validation, state updates, warm/cold caches, direct DR register SIMD vs generic Quack/R2IL, generated code size, and false-positive/escape frontier. An expected fast fold by itself does not amortize a slow binder or compiler. No timings asserted here. + +### Ownership and flow + +- Do not modify overlapping #1698 mathematics-correction branch, #1667 method/SQL parity plans, EXO-98 Thought-Git storage, or `cognitive-shader-driver`. +- Preserve the fast resident-register SIMD ruling for #1685: consuming already-prepared bits is **not** a forbidden bypass of R2IL; R2IL remains the general polyfill, not compulsory redispatch of prepared operands. +- A law proof is not evidence of a causal connection in nature. Theorems, observational finite certificates, generalization evidence, executable artifact and committed effects are independently versioned objects. +- No merges or production API promotions without a separately owned change, targeted CI, independent truth oracle and reviewer agreement. + +## Run + +`cargo test --manifest-path crates/dr-math-binding-probe/Cargo.toml` + +`cargo clippy --manifest-path crates/dr-math-binding-probe/Cargo.toml --all-targets -- -D warnings` + +`cargo fmt --manifest-path crates/dr-math-binding-probe/Cargo.toml --all -- --check` + +This crate has its own workspace and is intentionally not covered by every root-workspace test. The workflow in this PR provides a separate CI gate. diff --git a/crates/dr-math-binding-probe/tests/contract_handoff.rs b/crates/dr-math-binding-probe/tests/contract_handoff.rs new file mode 100644 index 000000000..4d97b5241 --- /dev/null +++ b/crates/dr-math-binding-probe/tests/contract_handoff.rs @@ -0,0 +1,113 @@ +//! D-DRMC-4: cross-layer *contract* fixture, no proof engine or write path. +//! The checked proof is a synthetic external receipt, NOT a real verified law. +use dr_math_binding_probe::{ + bind_dr64, Axis, AxisKind, BindingWitness, MethodSignature, + population::observe_focus, + recipe::{ + offer_recipe, Backend, Capability, CompiledReference, LawReference, + LawShape, Primitive, ProofDisposition, ProofReference, + }, +}; +use lance_graph_contract::class_view::{ + ClassId, ClassView, ComputeEdge, compute_dag_topo_order, +}; +use lance_graph_contract::ontology::{DisplayTemplate, FieldRef}; +use lance_graph_act_r::{ + arbitrate, witness_matches, Candidate, Refusal as ArbitrationRefusal, Snapshot, +}; + +static COMPUTED_ROLES: [ComputeEdge; 1] = [ComputeEdge { + target: 1, inputs: &[0], +}]; +struct FixtureClass { + fields: [FieldRef; 2], +} +impl FixtureClass { + fn new() -> Self { + Self { + fields: [ + FieldRef::new("urn:fixture:memberOf", "memberOf"), + FieldRef::new("urn:fixture:effectiveRoles", "effectiveRoles"), + ], + } + } +} +impl ClassView for FixtureClass { + fn fields(&self, class: ClassId) -> &[FieldRef] { + if class == 7 { &self.fields } else { &[] } + } + fn template(&self, _: ClassId) -> DisplayTemplate { DisplayTemplate::Detail } + fn dolce_category_id(&self, _: ClassId) -> u8 { 0 } + fn compute_dag(&self, class: ClassId) -> &[ComputeEdge] { + if class == 7 { &COMPUTED_ROLES } else { &[] } + } +} +fn signature(method: u16) -> MethodSignature { + MethodSignature::presence(7, method, + Axis { class:7, kind:AxisKind::Identity }, + Axis { class:7, kind:AxisKind::Property }) +} +fn witness() -> BindingWitness { + BindingWitness { source_revision:9, relation_map_revision:10, + coordinate_revision:11, focus_revision:12, authorization_scope:13 } +} +fn checked_fixture_law() -> ProofReference { + ProofReference { + law:LawReference { id:42, revision:1, shape:LawShape::for_method( + signature(1),Primitive::CountViolations) }, + checker_revision:1, proof_digest:[1;32], + status:ProofDisposition::CheckedByExternalAuthority, + } +} +#[test] +fn class_dependency_to_mathematical_offer_to_act_r_proposal_has_no_effect_path() { + let view=FixtureClass::new(); + assert_eq!(compute_dag_topo_order(view.compute_dag(7)),Some(vec![1])); + let mut selected=[0u64;64]; + selected[2]=1u64<<17; + let m=signature(1); + let g=bind_dr64(m,m,witness(),witness(),&selected).unwrap(); + let r=bind_dr64(m,m,witness(),witness(),&selected).unwrap(); + let report=observe_focus(&g,&r,None,witness()).unwrap(); + let checked=report.universal_on_focus().unwrap(); + assert_eq!((checked.eligible,checked.false_pairs,checked.unknown_pairs),(1,0,0)); + + let proof=checked_fixture_law(); + let compiled=CompiledReference { + law:proof.law,compiled_digest:[2;32],compiler_revision:1, + target_abi:3,backend:Backend::R2ilMaskRisc, + }; + let offer=offer_recipe(r,Primitive::CountViolations,proof,compiled,3, + Capability::PureMathematics).unwrap(); + assert_eq!(offer.operand.method,signature(1)); + + // ACT-R consumes external eligibility only. No action executor or write. + let observed=Snapshot { thought_address:77,witness_version:9 }; + let candidate=Candidate { + rule_id:19,eligible:checked.false_pairs==0, + utility:0.7,activation:0.4,evaluated_at:observed, + }; + let decision=arbitrate(observed,&[candidate]).unwrap(); + assert_eq!(decision.rule_id,19); + assert!(witness_matches(&decision,observed)); + + let moved=Snapshot { thought_address:77,witness_version:10 }; + assert!(matches!( + arbitrate(moved,&[candidate]), + Err(ArbitrationRefusal::StaleCandidate {rule_id:19,..}) + )); +} +#[test] +fn class_declares_a_dependency_not_permission_to_write() { + let view=FixtureClass::new(); + assert_eq!(view.compute_dag(7)[0].inputs,&[0]); + let mut selected=[0u64;64]; + selected[2]=1u64<<17; + let m=signature(1); + let b=bind_dr64(m,m,witness(),witness(),&selected).unwrap(); + let p=checked_fixture_law(); + let c=CompiledReference { law:p.law,compiled_digest:[2;32], + compiler_revision:1,target_abi:3,backend:Backend::ResidentDr64Simd }; + assert!(offer_recipe(b,Primitive::CountViolations,p,c,3, + Capability::EffectfulAction).is_err()); +}