probe(dr-math): guarded theorem/compiled-recipe identities across DR classes [3/5]

crates/dr-math-binding-probe/RECIPE_ADMISSION.md

@@ -0,0 +1,15 @@
+# D-DRMC-3 — law, proof, compiled recipe, runtime bind and effect are distinct
+
+This experimental metadata layer enforces the **shape of reuse**, not its scientific truth or physical execution. A `LawReference` keys a mathematical statement by primitive, row/column *kinds*, truth family, population semantics and law revision. It intentionally does not key on `ClassId`, method name, frame or source revision. A theorem about a genuinely common law could therefore be used by multiple ClassViews, after each class method is resolved to a matching mathematical shape. The fully typed method and witnesses remain on each `BoundDr64` and are never stored as law identity.
+
+Authority is split and none of it sits in this layer. **egglog** derives equivalences from admitted laws and checks its own proofs. **Law admission** owns the assumptions a law holds under. A **certified-compiler boundary**, after both of those and a lowering check, issues a `RecipeCertificate`: an opaque value with no public constructor and no caller-set status, so a caller can neither declare a law checked nor attach a digest of its own (the earlier hole, where any nonzero digest passed). Stage B's `ReplayCapsule` is replay and audit evidence for its own E1 substitution language; it is not a proof authority and is not used here. `CompiledReference` identifies compiler revision, code artifact, target ABI and backend. `RecipeOffer` remains **metadata**, not bytes to execute.
+
+**No DR64 certificate exists.** A certified-compiler boundary for Boolean-DR64 laws needs a typed relational statement language, egglog laws over it with checked proofs, and a lowering check; none exists. `admit_recipe` therefore runs every metadata check (effect capability, law shape, law identity, code identity, target) and then refuses with `NoCertifiedCompiler`. The tests pin each earlier refusal and that the end of the path is that refusal, never an offer.
+
+Stage 2's finite-focus `PopulationReport` CANNOT produce a `RecipeCertificate`. Even a complete 64x64 population pass is not a theorem outside its declared scope, and a proof that a derivation follows from admitted laws does not show the laws hold for a newly observed population.
+
+Relevant existing foundation: merged #1690–#1696 `egglog-r2il-probe` E1, with #1698 handling contradictory assumptions and exact-vs-checked overflow in a *different owned branch*. This PR does not reimplement or change egglog, Ruler, Enumo, eggcc or their proof format. Their admission must happen COLD, with source/outcome provenance, scalar/domain oracles, deterministic replay, effect-order constraints, measured costs and a target ABI gate.
+
+The next integration stage must prove an actual **ClassView→relation frame→method law→RelAlg AST→compiled recipe→mask-risc/native SIMD** round trip, including refusals, independent oracles and full cold/amortized economics. Until then this is an isolated falsifiable seam.
+
+ACT-R/Rubicon/kanban/cognitive-shader-driver are downstream consumers and are not allowed to use a mathematical proof as effect authorization. Thought-Git may link immutable law/proof/recipe/binding/replay/commit references when its own write and provenance contracts are ready.

crates/dr-math-binding-probe/src/lib.rs

@@ -274,3 +274,6 @@ pub fn bind_dr64<'a>(
 
 /// Independent 64x64 finite-population reference audit; NEVER a production evaluator.
 pub mod population;
+
+/// Reusable mathematical law / proof / compiled artifact identity separation (lab only).
+pub mod recipe;

crates/dr-math-binding-probe/src/recipe.rs

@@ -0,0 +1,168 @@
+//! D-DRMC-3: mathematical LAW identity != compiled TARGET recipe != current DATA binding.
+//!
+//! Metadata-only guarded admission, NEVER a compiler, runtime scheduler,
+//! binary loader, effect executor or data source attestor. The math law key
+//! deliberately excludes class/method and source versions so a proof about a
+//! mathematical shape can potentially be reused across ClassViews.
+//!
+//! Authority is split, and none of it sits here:
+//! - egglog derives equivalences from admitted laws and checks its own proofs;
+//! - law admission owns the assumptions a law holds under (a finite-population
+//!   report never admits a law);
+//! - a certified-compiler boundary, after both of those and a lowering check,
+//!   issues a [`RecipeCertificate`];
+//! - Stage B's `ReplayCapsule` is replay and audit evidence for its own E1
+//!   substitution language, not a proof authority for anything else.
+//!
+//! No certified-compiler boundary exists for a Boolean-DR64 law yet, so this
+//! layer checks everything it can and then refuses with `NoCertifiedCompiler`.
+use crate::{AxisKind, BoundDr64, Population, Truth};
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
+pub enum Primitive {
+    Selection,
+    BooleanCompose,
+    ArgmaxMasked,
+    CountViolations,
+}
+
+/// Semantics on which a *single mathematical transformation* is conditional.
+/// Not a ClassId/MethodId, not a data snapshot or a cache address.
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
+pub struct LawShape {
+    pub primitive: Primitive,
+    pub row_kind: AxisKind,
+    pub column_kind: AxisKind,
+    pub truth: Truth,
+    pub population: Population,
+}
+
+impl LawShape {
+    pub fn for_method(method: crate::MethodSignature, primitive: Primitive) -> Self {
+        Self {
+            primitive,
+            row_kind: method.row.kind,
+            column_kind: method.column.kind,
+            truth: method.truth,
+            population: method.population,
+        }
+    }
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
+pub struct LawReference {
+    pub id: u64,
+    pub revision: u32,
+    pub shape: LawShape,
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub enum Backend {
+    R2ilMaskRisc,
+    ResidentDr64Simd,
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub struct CompiledReference {
+    pub law: LawReference,
+    pub compiled_digest: [u8; 32],
+    pub compiler_revision: u32,
+    pub target_abi: u32,
+    pub backend: Backend,
+}
+
+/// The only thing that makes a recipe reusable: issued by the certified-
+/// compiler boundary once egglog's proof check, law admission and the lowering
+/// check have all passed. No public constructor and no caller-set status, so a
+/// caller can neither declare a law checked nor attach a digest of its own.
+///
+/// ```compile_fail
+/// use dr_math_binding_probe::recipe::RecipeCertificate;
+/// let forged = RecipeCertificate { law: todo!(), compiled: todo!() };
+/// ```
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub struct RecipeCertificate {
+    law: LawReference,
+    compiled: CompiledReference,
+}
+
+impl RecipeCertificate {
+    pub fn law(&self) -> &LawReference {
+        &self.law
+    }
+
+    pub fn compiled(&self) -> &CompiledReference {
+        &self.compiled
+    }
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub enum Capability {
+    PureMathematics,
+    Proposal,
+    EffectfulAction,
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub enum RecipeRefusal {
+    UnsupportedMathematicalShape,
+    LawChanged,
+    MissingCodeIdentity,
+    WrongTarget,
+    EffectRequiresSeparateAuthorization,
+    /// Every other check passed, but no certified-compiler boundary exists
+    /// for this law shape, so no certificate can be issued.
+    NoCertifiedCompiler,
+}
+
+/// This is a *selection receipt* for a certified compiled artifact, not
+/// executable machine code or a substitute for source/version validation.
+#[derive(Clone, Debug)]
+pub struct RecipeOffer<'a> {
+    pub operand: BoundDr64<'a>,
+    pub certificate: RecipeCertificate,
+}
+
+/// Cold-stage metadata admission for a mathematically typed, already-bound
+/// register: effect capability, law shape, law identity, code identity and
+/// target first, then certification. Certification refuses for every shape
+/// today; see the module docs.
+pub fn admit_recipe<'a>(
+    operand: BoundDr64<'a>,
+    primitive: Primitive,
+    law: LawReference,
+    compiled: CompiledReference,
+    runtime_abi: u32,
+    capability: Capability,
+) -> Result<RecipeOffer<'a>, RecipeRefusal> {
+    if capability != Capability::PureMathematics {
+        return Err(RecipeRefusal::EffectRequiresSeparateAuthorization);
+    }
+    if law.shape != LawShape::for_method(operand.method, primitive) {
+        return Err(RecipeRefusal::UnsupportedMathematicalShape);
+    }
+    if law != compiled.law {
+        return Err(RecipeRefusal::LawChanged);
+    }
+    if compiled.compiler_revision == 0 || compiled.compiled_digest == [0u8; 32] {
+        return Err(RecipeRefusal::MissingCodeIdentity);
+    }
+    if compiled.target_abi != runtime_abi {
+        return Err(RecipeRefusal::WrongTarget);
+    }
+    let certificate = certify(law, compiled)?;
+    Ok(RecipeOffer {
+        operand,
+        certificate,
+    })
+}
+
+/// The certified-compiler boundary. It has no implementation for any
+/// Boolean-DR64 law shape: that needs a typed relational statement language,
+/// egglog laws over it with checked proofs, and a lowering check.
+fn certify(
+    _law: LawReference,
+    _compiled: CompiledReference,
+) -> Result<RecipeCertificate, RecipeRefusal> {
+    Err(RecipeRefusal::NoCertifiedCompiler)
+}

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

@@ -0,0 +1,197 @@
+//! No certified-compiler boundary exists for a Boolean-DR64 law, so every
+//! admission that passes the metadata checks ends in `NoCertifiedCompiler`.
+//! The tests pin that each earlier check refuses on its own, and that nothing
+//! (no flag, no digest, no finite-population report) produces a certificate.
+use dr_math_binding_probe::{
+    Axis, AxisKind, BoundDr64, Focus, FrameRevisions, FrameStore, Guards, MethodSignature, Operand,
+    Scope, bind_dr64,
+    recipe::{
+        Backend, Capability, CompiledReference, LawReference, LawShape, Primitive, RecipeRefusal,
+        admit_recipe,
+    },
+};
+
+const FOCUS: Focus = Focus { revision: 4 };
+const SCOPE: Scope = Scope { id: 5 };
+const ABI: u32 = 3;
+
+fn store() -> FrameStore {
+    FrameStore::new(FrameRevisions {
+        source: 1,
+        relation_map: 2,
+        coordinates: 3,
+    })
+}
+/// Non-empty operand, so a test cannot pass only because the register is zero.
+fn rows() -> [u64; 64] {
+    let mut rows = [0u64; 64];
+    rows[3] = (1 << 5) | (1 << 40);
+    rows[60] = 1 << 1;
+    rows
+}
+fn method(class: u16, ordinal: u16, property: bool) -> MethodSignature {
+    let kind = if property {
+        AxisKind::Property
+    } else {
+        AxisKind::Identity
+    };
+    MethodSignature::presence(
+        class,
+        ordinal,
+        Axis {
+            class,
+            kind: AxisKind::Identity,
+        },
+        Axis { class, kind },
+    )
+}
+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()
+}
+fn law(m: MethodSignature) -> LawReference {
+    LawReference {
+        id: 41,
+        revision: 7,
+        shape: LawShape::for_method(m, Primitive::CountViolations),
+    }
+}
+fn compiled(l: LawReference) -> CompiledReference {
+    CompiledReference {
+        law: l,
+        compiled_digest: [18; 32],
+        compiler_revision: 2,
+        target_abi: ABI,
+        backend: Backend::R2ilMaskRisc,
+    }
+}
+fn admit(
+    st: &FrameStore,
+    m: MethodSignature,
+    l: LawReference,
+    c: CompiledReference,
+    runtime_abi: u32,
+    capability: Capability,
+) -> RecipeRefusal {
+    let r = rows();
+    admit_recipe(
+        bind(st, m, &r),
+        Primitive::CountViolations,
+        l,
+        c,
+        runtime_abi,
+        capability,
+    )
+    .unwrap_err()
+}
+
+/// One law key serves two classes (the key holds no ClassId); both pass every
+/// metadata check and stop at certification, which does not exist for DR64.
+#[test]
+fn one_law_key_spans_two_classes_and_neither_is_certified() {
+    let st = store();
+    let (m1, m2) = (method(1, 2, true), method(22, 8, true));
+    assert_eq!(law(m1), law(m2));
+    assert_ne!(m1.owner_class, m2.owner_class);
+    for m in [m1, m2] {
+        assert_eq!(
+            admit(
+                &st,
+                m,
+                law(m1),
+                compiled(law(m1)),
+                ABI,
+                Capability::PureMathematics
+            ),
+            RecipeRefusal::NoCertifiedCompiler
+        );
+    }
+}
+
+#[test]
+fn same_bytes_but_different_axes_cannot_reuse_law() {
+    let st = store();
+    let l = law(method(1, 2, true));
+    assert_eq!(
+        admit(
+            &st,
+            method(1, 2, false),
+            l,
+            compiled(l),
+            ABI,
+            Capability::PureMathematics
+        ),
+        RecipeRefusal::UnsupportedMathematicalShape
+    );
+}
+
+#[test]
+fn changed_law_revision_or_target_refuses_before_certification() {
+    let st = store();
+    let m = method(1, 2, true);
+    let mut c = compiled(law(m));
+    c.law.revision += 1;
+    assert_eq!(
+        admit(&st, m, law(m), c, ABI, Capability::PureMathematics),
+        RecipeRefusal::LawChanged
+    );
+    assert_eq!(
+        admit(
+            &st,
+            m,
+            law(m),
+            compiled(law(m)),
+            ABI + 1,
+            Capability::PureMathematics
+        ),
+        RecipeRefusal::WrongTarget
+    );
+}
+
+#[test]
+fn missing_code_identity_refuses() {
+    let st = store();
+    let m = method(1, 2, true);
+    for broken in [
+        CompiledReference {
+            compiled_digest: [0; 32],
+            ..compiled(law(m))
+        },
+        CompiledReference {
+            compiler_revision: 0,
+            ..compiled(law(m))
+        },
+    ] {
+        assert_eq!(
+            admit(&st, m, law(m), broken, ABI, Capability::PureMathematics),
+            RecipeRefusal::MissingCodeIdentity
+        );
+    }
+}
+
+#[test]
+fn proof_of_math_never_authorizes_a_cognitive_commit() {
+    let st = store();
+    let m = method(1, 2, true);
+    for kind in [Capability::Proposal, Capability::EffectfulAction] {
+        assert_eq!(
+            admit(&st, m, law(m), compiled(law(m)), ABI, kind),
+            RecipeRefusal::EffectRequiresSeparateAuthorization
+        );
+    }
+}