test(dr-math): ClassView→DR→math offer→ACT-R handoff and isolated CI [4/5]

.github/workflows/dr-math-binding-probe.yml

@@ -0,0 +1,64 @@
+name: DR Mathematical Binding Probe
+# Own [workspace] excluded from root tests; a lab gate, not production
+# admission. Mirrors egglog-r2il-probe.yml's toolchain setup: the pinned
+# toolchain from rust-toolchain.toml, never `stable`.
+on:
+  pull_request:
+    paths:
+      - "crates/dr-math-binding-probe/**"
+      - "crates/lance-graph-contract/**"
+      - "crates/lance-graph-act-r/**"
+      - ".github/workflows/dr-math-binding-probe.yml"
+      - "rust-toolchain.toml"
+  push:
+    branches: [main]
+    paths:
+      - "crates/dr-math-binding-probe/**"
+      - "crates/lance-graph-contract/**"
+      - "crates/lance-graph-act-r/**"
+      - ".github/workflows/dr-math-binding-probe.yml"
+      - "rust-toolchain.toml"
+  workflow_dispatch:
+permissions:
+  contents: read
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+env:
+  CARGO_TERM_COLOR: always
+  CARGO_INCREMENTAL: "0"
+  CARGO_PROFILE_DEV_DEBUG: "0"
+  CARGO_PROFILE_TEST_DEBUG: "0"
+  RUST_BACKTRACE: "1"
+jobs:
+  isolated-probe:
+    name: excluded-crate fmt, clippy and tests
+    runs-on: ubuntu-24.04
+    timeout-minutes: 60
+    defaults:
+      run:
+        working-directory: lance-graph
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          path: lance-graph
+          persist-credentials: false
+      - name: Rust toolchain
+        run: rustup show
+      - name: Resolve target-cpu=native for this runner
+        id: cpu
+        run: |
+          flags=$(.github/scripts/resolve-native-rustflags.sh)
+          echo "RUSTFLAGS=$flags" >> "$GITHUB_ENV"
+          hash=$(printf %s "$flags" | sha256sum | cut -c1-16)
+          echo "flags=$hash" >> "$GITHUB_OUTPUT"
+      - uses: Swatinem/rust-cache@v2
+        with:
+          key: cpu-${{ steps.cpu.outputs.flags }}
+          workspaces: lance-graph/crates/dr-math-binding-probe
+      - name: fmt
+        run: cargo fmt --manifest-path crates/dr-math-binding-probe/Cargo.toml --check
+      - name: clippy
+        run: cargo clippy --manifest-path crates/dr-math-binding-probe/Cargo.toml --all-targets -- -D warnings
+      - name: tests
+        run: cargo test --release --manifest-path crates/dr-math-binding-probe/Cargo.toml

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" }

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.

crates/dr-math-binding-probe/tests/contract_handoff.rs

@@ -0,0 +1,198 @@
+//! D-DRMC-4: cross-layer *contract* fixture, no proof engine or write path.
+//! No certified-compiler boundary exists for DR64 laws, so the recipe offer
+//! refuses with `NoCertifiedCompiler`; ACT-R arbitration runs on the census
+//! eligibility alone and never on a proof.
+use dr_math_binding_probe::{
+    Axis, AxisKind, BoundDr64, Focus, FrameRevisions, FrameStore, Guards, MethodSignature, Operand,
+    Scope, bind_dr64,
+    population::observe_focus,
+    recipe::{
+        Backend, Capability, CompiledReference, LawReference, LawShape, Primitive, RecipeRefusal,
+        admit_recipe,
+    },
+};
+use lance_graph_act_r::{
+    Candidate, Refusal as ArbitrationRefusal, Snapshot, arbitrate, witness_matches,
+};
+use lance_graph_contract::class_view::{ClassId, ClassView, ComputeEdge, compute_dag_topo_order};
+use lance_graph_contract::ontology::{DisplayTemplate, FieldRef};
+
+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 { &[] }
+    }
+}
+const FOCUS: Focus = Focus { revision: 12 };
+const SCOPE: Scope = Scope { id: 13 };
+
+fn signature(method: u16) -> MethodSignature {
+    MethodSignature::presence(
+        7,
+        method,
+        Axis {
+            class: 7,
+            kind: AxisKind::Identity,
+        },
+        Axis {
+            class: 7,
+            kind: AxisKind::Property,
+        },
+    )
+}
+fn store() -> FrameStore {
+    FrameStore::new(FrameRevisions {
+        source: 9,
+        relation_map: 10,
+        coordinates: 11,
+    })
+}
+fn bind<'a>(st: &FrameStore, m: MethodSignature, rows: &'a [u64; 64]) -> BoundDr64<'a> {
+    let at = Guards {
+        frame: st.seal(),
+        focus: FOCUS,
+        scope: SCOPE,
+    };
+    bind_dr64(
+        st,
+        m,
+        m,
+        &at,
+        (FOCUS, SCOPE),
+        Operand {
+            rows,
+            validity: None,
+        },
+    )
+    .unwrap()
+}
+const ABI: u32 = 3;
+fn law() -> LawReference {
+    LawReference {
+        id: 42,
+        revision: 1,
+        shape: LawShape::for_method(signature(1), Primitive::CountViolations),
+    }
+}
+fn compiled(backend: Backend) -> CompiledReference {
+    CompiledReference {
+        law: law(),
+        compiled_digest: [2; 32],
+        compiler_revision: 1,
+        target_abi: ABI,
+        backend,
+    }
+}
+
+#[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 st = store();
+    // Gamma and R are different bits: R holds the selected pair and one more.
+    let mut selected = [0u64; 64];
+    selected[2] = 1u64 << 17;
+    let mut relation = [0u64; 64];
+    relation[2] = (1u64 << 17) | (1u64 << 18);
+    assert_ne!(selected, relation);
+    let g = bind(&st, signature(2), &selected);
+    let r = bind(&st, signature(1), &relation);
+    let report = observe_focus(&st, &g, &r).unwrap();
+    let checked = report.universal_on_focus().unwrap();
+    assert_eq!(
+        (
+            checked.eligible,
+            checked.true_pairs,
+            checked.false_pairs,
+            checked.unknown_pairs
+        ),
+        (1, 1, 0, 0)
+    );
+
+    // Every metadata check passes; no DR64 certificate can be issued.
+    assert_eq!(
+        admit_recipe(
+            r.clone(),
+            Primitive::CountViolations,
+            law(),
+            compiled(Backend::R2ilMaskRisc),
+            ABI,
+            Capability::PureMathematics,
+        )
+        .unwrap_err(),
+        RecipeRefusal::NoCertifiedCompiler
+    );
+
+    // ACT-R consumes external eligibility only. No action executor or write.
+    // The snapshot version comes from the bound frame, not a second literal.
+    let observed = Snapshot {
+        thought_address: 77,
+        witness_version: r.frame.revisions().source,
+    };
+    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: observed.witness_version + 1,
+    };
+    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 st = store();
+    let mut selected = [0u64; 64];
+    selected[2] = 1u64 << 17;
+    let b = bind(&st, signature(1), &selected);
+    assert_eq!(
+        admit_recipe(
+            b,
+            Primitive::CountViolations,
+            law(),
+            compiled(Backend::ResidentDr64Simd),
+            ABI,
+            Capability::EffectfulAction
+        )
+        .unwrap_err(),
+        RecipeRefusal::EffectRequiresSeparateAuthorization
+    );
+}