diff --git a/.github/workflows/dr-math-binding-probe.yml b/.github/workflows/dr-math-binding-probe.yml new file mode 100644 index 000000000..b5cc18156 --- /dev/null +++ b/.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 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..ff46aec0e --- /dev/null +++ b/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 + ); +}