diff --git a/crates/dr-math-binding-probe/RECIPE_ADMISSION.md b/crates/dr-math-binding-probe/RECIPE_ADMISSION.md new file mode 100644 index 000000000..c431c4989 --- /dev/null +++ b/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. diff --git a/crates/dr-math-binding-probe/src/lib.rs b/crates/dr-math-binding-probe/src/lib.rs index 81feb138d..7d6cd9909 100644 --- a/crates/dr-math-binding-probe/src/lib.rs +++ b/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; diff --git a/crates/dr-math-binding-probe/src/recipe.rs b/crates/dr-math-binding-probe/src/recipe.rs new file mode 100644 index 000000000..d727d7766 --- /dev/null +++ b/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, 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 { + Err(RecipeRefusal::NoCertifiedCompiler) +} diff --git a/crates/dr-math-binding-probe/tests/recipe.rs b/crates/dr-math-binding-probe/tests/recipe.rs new file mode 100644 index 000000000..651d1fecc --- /dev/null +++ b/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 + ); + } +}