From f0b0f28474b06e3bcb8d96c6ace5e512b9841ccb Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Thu, 22 Oct 2026 16:42:55 +0200 Subject: [PATCH 1/4] probe(dr-math): separate law/proof/target recipe from versioned DR population --- .../dr-math-binding-probe/RECIPE_ADMISSION.md | 13 ++ crates/dr-math-binding-probe/src/lib.rs | 3 + crates/dr-math-binding-probe/src/recipe.rs | 140 ++++++++++++++++++ crates/dr-math-binding-probe/tests/recipe.rs | 92 ++++++++++++ 4 files changed, 248 insertions(+) create mode 100644 crates/dr-math-binding-probe/RECIPE_ADMISSION.md create mode 100644 crates/dr-math-binding-probe/src/recipe.rs create mode 100644 crates/dr-math-binding-probe/tests/recipe.rs 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..bf5b56375 --- /dev/null +++ b/crates/dr-math-binding-probe/RECIPE_ADMISSION.md @@ -0,0 +1,13 @@ +# 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. + +A `ProofReference` identifies external checker revision and proof digest. `CompiledReference` identifies separate compiler revision, code artifact, target ABI and backend (existing R2IL/mask-risc or direct resident SIMD). `RecipeOffer` remains **metadata**, not bytes to execute. The `CheckedByExternalAuthority` enum is **caller asserted** in this probe. It does not run or independently authenticate a proof; a production owner must require actual independent checker receipts, pinned law/ISA versions and source metadata. Zero digest refuses only a missing identity, not a forged nonzero digest. + +Stage 2's finite-focus `PopulationReport` CANNOT produce a `ProofReference`. Even a complete 64x64 population pass is not a theorem outside its declared scope. + +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 7d9440e48..b50b6b063 100644 --- a/crates/dr-math-binding-probe/src/lib.rs +++ b/crates/dr-math-binding-probe/src/lib.rs @@ -152,3 +152,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..8ad554063 --- /dev/null +++ b/crates/dr-math-binding-probe/src/recipe.rs @@ -0,0 +1,140 @@ +//! D-DRMC-3: mathematical LAW identity != compiled TARGET recipe != current DATA binding. +//! +//! Metadata-only guarded admission, NEVER a compiler, proof checker, 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. +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, +} + +/// An assertion *from an external checking boundary*. Supplying `Checked` is +/// not proof! The production owner must run an independent checker against +/// the referenced statement, domain axioms and replay capsule, and attest it. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum ProofDisposition { + Candidate, + CheckedByExternalAuthority, +} +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct ProofReference { + pub law: LawReference, + pub checker_revision: u32, + pub proof_digest: [u8; 32], + pub status: ProofDisposition, +} + +#[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, +} + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum Capability { + PureMathematics, + Proposal, + EffectfulAction, +} + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum RecipeRefusal { + UnsupportedMathematicalShape, + LawChanged, + UncheckedLaw, + MissingProofIdentity, + MissingCodeIdentity, + WrongTarget, + EffectRequiresSeparateAuthorization, +} + +/// This is a *selection receipt* for an already compiled artifact, not +/// executable machine code or a substitute for source/version validation. +#[derive(Clone, Copy, Debug)] +pub struct RecipeOffer<'a> { + pub operand: BoundDr64<'a>, + pub artifact: CompiledReference, + pub proof: ProofReference, +} + +/// Cold-stage metadata selection for a mathematically typed, already-bound +/// register. It does not verify proof hashes or attest their provenance; it +/// refuses a missing/unchecked proof *even if* a finite-population report +/// happened to find zero counterexamples. +pub fn offer_recipe<'a>( + operand: BoundDr64<'a>, + primitive: Primitive, + proof: ProofReference, + compiled: CompiledReference, + runtime_abi: u32, + capability: Capability, +) -> Result, RecipeRefusal> { + if capability != Capability::PureMathematics { + return Err(RecipeRefusal::EffectRequiresSeparateAuthorization); + } + let observed_shape = LawShape::for_method(operand.method, primitive); + if proof.law.shape != observed_shape { + return Err(RecipeRefusal::UnsupportedMathematicalShape); + } + if proof.law != compiled.law { + return Err(RecipeRefusal::LawChanged); + } + if proof.status != ProofDisposition::CheckedByExternalAuthority { + return Err(RecipeRefusal::UncheckedLaw); + } + if proof.checker_revision == 0 || proof.proof_digest == [0u8; 32] { + return Err(RecipeRefusal::MissingProofIdentity); + } + if compiled.compiler_revision == 0 || compiled.compiled_digest == [0u8; 32] { + return Err(RecipeRefusal::MissingCodeIdentity); + } + if compiled.target_abi != runtime_abi { + return Err(RecipeRefusal::WrongTarget); + } + Ok(RecipeOffer { operand, artifact: compiled, proof }) +} 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..66bb1d799 --- /dev/null +++ b/crates/dr-math-binding-probe/tests/recipe.rs @@ -0,0 +1,92 @@ +use dr_math_binding_probe::{ + bind_dr64, Axis, AxisKind, BindingWitness, MethodSignature, + recipe::{ + offer_recipe, Backend, Capability, CompiledReference, LawReference, + LawShape, Primitive, ProofDisposition, ProofReference, RecipeRefusal, + }, +}; +fn witness() -> BindingWitness { + BindingWitness { source_revision:1, relation_map_revision:2,coordinate_revision:3, + focus_revision:4,authorization_scope:5 } +} +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 proof(m:MethodSignature) -> ProofReference { + ProofReference { + law: LawReference { id:41, revision:7, + shape:LawShape::for_method(m,Primitive::CountViolations) }, + checker_revision:1, proof_digest:[17;32], + status:ProofDisposition::CheckedByExternalAuthority, + } +} +fn compiled(p:ProofReference) -> CompiledReference { + CompiledReference { law:p.law, compiled_digest:[18;32], + compiler_revision:2,target_abi:3,backend:Backend::R2ilMaskRisc } +} +#[test] +fn one_law_shape_reuses_two_classes_without_reusing_their_source_binding() { + let rows=[0u64;64]; + let m1=method(1,2,true); + let m2=method(22,8,true); + let a=bind_dr64(m1,m1,witness(),witness(),&rows).unwrap(); + let b=bind_dr64(m2,m2,witness(),witness(),&rows).unwrap(); + let p=proof(m1); + let c=compiled(p); + let aa=offer_recipe(a,Primitive::CountViolations,p,c,3,Capability::PureMathematics).unwrap(); + let bb=offer_recipe(b,Primitive::CountViolations,p,c,3,Capability::PureMathematics).unwrap(); + assert_eq!(aa.proof.law,bb.proof.law); + assert_ne!(aa.operand.method.owner_class,bb.operand.method.owner_class); +} +#[test] +fn same_bytes_but_different_axes_cannot_reuse_law() { + let rows=[0u64;64]; + let id2=method(1,2,false); + let bound=bind_dr64(id2,id2,witness(),witness(),&rows).unwrap(); + let p=proof(method(1,2,true)); + assert_eq!(offer_recipe(bound,Primitive::CountViolations,p,compiled(p),3,Capability::PureMathematics) + .unwrap_err(),RecipeRefusal::UnsupportedMathematicalShape); +} +#[test] +fn unverified_conjecture_is_not_admitted_by_a_bare_flag_free_path() { + let rows=[0u64;64];let m=method(1,2,true); + let bound=bind_dr64(m,m,witness(),witness(),&rows).unwrap(); + let mut p=proof(m);p.status=ProofDisposition::Candidate; + assert_eq!(offer_recipe(bound,Primitive::CountViolations,p,compiled(p),3,Capability::PureMathematics) + .unwrap_err(),RecipeRefusal::UncheckedLaw); +} +#[test] +fn changed_law_revision_or_target_refuses_cached_recipe() { + let rows=[0u64;64];let m=method(1,2,true); + let bound=bind_dr64(m,m,witness(),witness(),&rows).unwrap(); + let p=proof(m);let mut c=compiled(p);c.law.revision+=1; + assert_eq!(offer_recipe(bound,Primitive::CountViolations,p,c,3,Capability::PureMathematics) + .unwrap_err(),RecipeRefusal::LawChanged); + let c=compiled(p); + assert_eq!(offer_recipe(bound,Primitive::CountViolations,p,c,4,Capability::PureMathematics) + .unwrap_err(),RecipeRefusal::WrongTarget); +} +#[test] +fn missing_proof_and_code_identities_refuse() { + let rows=[0u64;64];let m=method(1,2,true); + let bound=bind_dr64(m,m,witness(),witness(),&rows).unwrap(); + let mut p=proof(m);p.proof_digest=[0;32]; + assert_eq!(offer_recipe(bound,Primitive::CountViolations,p,compiled(p),3,Capability::PureMathematics) + .unwrap_err(),RecipeRefusal::MissingProofIdentity); + let p=proof(m);let mut c=compiled(p);c.compiled_digest=[0;32]; + assert_eq!(offer_recipe(bound,Primitive::CountViolations,p,c,3,Capability::PureMathematics) + .unwrap_err(),RecipeRefusal::MissingCodeIdentity); +} +#[test] +fn proof_of_math_never_authorizes_a_cognitive_commit() { + let rows=[0u64;64];let m=method(1,2,true); + let bound=bind_dr64(m,m,witness(),witness(),&rows).unwrap(); + let p=proof(m); + for kind in [Capability::Proposal,Capability::EffectfulAction] { + assert_eq!(offer_recipe(bound,Primitive::CountViolations,p,compiled(p),3,kind) + .unwrap_err(),RecipeRefusal::EffectRequiresSeparateAuthorization); + } +} From 55f88ef4771c8831c3ccaceb4d85f89350385b25 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 22 Oct 2026 15:22:50 +0000 Subject: [PATCH 2/4] probe(dr-math): take proof and target identity from Stage B Coresearch D-DRMC item X15 (operator-chosen) and X17 for the recipe fixtures. - ProofDisposition (a caller-set "checked" flag) and the caller-supplied proof digest are gone. ProofReference has private fields and one constructor, rechecked(law, ReplayCapsule), which requires the capsule to prove law.statement (Stage B's SemanticKey) and re-runs ReplayCapsule::recheck. A forged nonzero digest used to pass; it can no longer be written (compile_fail doctest), and a real proof of a different statement is ProofOfOtherStatement. - CompiledReference carries Stage B's TargetAbi instead of a bare u32. - Recipe fixtures bind non-zero registers. - dr-math-binding-probe now depends on egglog-r2il-probe (egglog and ogar-loco by git, ndarray through the sibling patch). Limit: Stage B proves exact-integer substitution statements only. No statement language or checker exists for Boolean-DR64 laws, so the tests pair a DR64 shape with E1's statement to exercise the plumbing; that is not a claim that E1 says anything about DR64 (RECIPE_ADMISSION.md). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg --- crates/dr-math-binding-probe/Cargo.toml | 12 + .../dr-math-binding-probe/RECIPE_ADMISSION.md | 6 +- crates/dr-math-binding-probe/src/recipe.rs | 101 ++++-- crates/dr-math-binding-probe/tests/recipe.rs | 300 ++++++++++++++---- 4 files changed, 317 insertions(+), 102 deletions(-) diff --git a/crates/dr-math-binding-probe/Cargo.toml b/crates/dr-math-binding-probe/Cargo.toml index 4969346c0..867e6aa6b 100644 --- a/crates/dr-math-binding-probe/Cargo.toml +++ b/crates/dr-math-binding-probe/Cargo.toml @@ -10,3 +10,15 @@ description = "Borrowed DR64 / ClassView-style typed structure and source witnes [dependencies] lance-graph-contract = { path = "../lance-graph-contract" } +# Stage B's proof capsule and target ABI (D-DRMC-3 takes proof and target +# identity from there instead of re-spelling them). Pulls egglog and ogar-loco +# by git and ndarray through the sibling patch below. +egglog-r2il-probe = { path = "../egglog-r2il-probe" } + +# The same patches egglog-r2il-probe carries (a path dependency's [patch] +# tables do not apply): one contract and one ndarray identity. +[patch."https://github.com/AdaWorldAPI/lance-graph"] +lance-graph-contract = { path = "../lance-graph-contract" } + +[patch."https://github.com/AdaWorldAPI/ndarray"] +ndarray = { path = "../../../ndarray" } diff --git a/crates/dr-math-binding-probe/RECIPE_ADMISSION.md b/crates/dr-math-binding-probe/RECIPE_ADMISSION.md index bf5b56375..c96ebda33 100644 --- a/crates/dr-math-binding-probe/RECIPE_ADMISSION.md +++ b/crates/dr-math-binding-probe/RECIPE_ADMISSION.md @@ -1,8 +1,10 @@ # 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. +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, law revision and the statement a proof must prove. 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. -A `ProofReference` identifies external checker revision and proof digest. `CompiledReference` identifies separate compiler revision, code artifact, target ABI and backend (existing R2IL/mask-risc or direct resident SIMD). `RecipeOffer` remains **metadata**, not bytes to execute. The `CheckedByExternalAuthority` enum is **caller asserted** in this probe. It does not run or independently authenticate a proof; a production owner must require actual independent checker receipts, pinned law/ISA versions and source metadata. Zero digest refuses only a missing identity, not a forged nonzero digest. +Proof and target identity are Stage B's, not re-spelled here. A `ProofReference` has private fields and one constructor, `ProofReference::rechecked`, which requires the `ReplayCapsule` to prove the law's `statement` (Stage B's `SemanticKey`) and re-runs `ReplayCapsule::recheck` (a fresh egglog proof session, byte-equal proof). There is no caller-set "checked" flag and no caller-supplied proof digest, so the earlier hole (a forged nonzero digest passed) cannot be written. `CompiledReference` identifies the compiler revision, code artifact, backend and Stage B's `TargetAbi`. `RecipeOffer` remains **metadata**, not bytes to execute. + +**Limit, stated plainly:** Stage B's checker proves exact-integer substitution statements. No statement language and no checker exist yet for a Boolean-DR64 law, so the tests pair a DR64 law shape with Stage B's E1 statement to exercise the admission plumbing only; that pairing is not a claim that E1 says anything about DR64. Adding the dependency also brings egglog and ogar-loco (git) and the ndarray sibling patch into this probe's build. Stage 2's finite-focus `PopulationReport` CANNOT produce a `ProofReference`. Even a complete 64x64 population pass is not a theorem outside its declared scope. diff --git a/crates/dr-math-binding-probe/src/recipe.rs b/crates/dr-math-binding-probe/src/recipe.rs index 8ad554063..78ed44dd8 100644 --- a/crates/dr-math-binding-probe/src/recipe.rs +++ b/crates/dr-math-binding-probe/src/recipe.rs @@ -1,9 +1,19 @@ //! D-DRMC-3: mathematical LAW identity != compiled TARGET recipe != current DATA binding. //! -//! Metadata-only guarded admission, NEVER a compiler, proof checker, 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. +//! 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. +//! +//! Proof and target identity are Stage B's (`egglog-r2il-probe`): a +//! [`ProofReference`] exists only as a [`ReplayCapsule`] that egglog's own +//! checker re-proved, and the target is Stage B's [`TargetAbi`]. Nothing here +//! lets a caller declare a law checked. Stage B's checker proves exact-integer +//! substitution statements; no statement language or checker exists yet for a +//! Boolean-DR64 law, so the only statements this layer can carry are Stage B's. +use egglog_r2il_probe::artifact::ReplayCapsule; +use egglog_r2il_probe::catalogue::{SemanticKey, TargetAbi}; + use crate::{AxisKind, BoundDr64, Population, Truth}; #[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] @@ -37,27 +47,51 @@ impl LawShape { } } -#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] +/// A law: its id and revision, the DR64 shape it applies to, and the statement +/// a proof must prove. +#[derive(Clone, Debug, PartialEq, Eq)] pub struct LawReference { pub id: u64, pub revision: u32, pub shape: LawShape, + pub statement: SemanticKey, } -/// An assertion *from an external checking boundary*. Supplying `Checked` is -/// not proof! The production owner must run an independent checker against -/// the referenced statement, domain axioms and replay capsule, and attest it. -#[derive(Clone, Copy, Debug, PartialEq, Eq)] -pub enum ProofDisposition { - Candidate, - CheckedByExternalAuthority, -} -#[derive(Clone, Copy, Debug, PartialEq, Eq)] +/// A law together with a proof of its statement that was re-checked when this +/// value was made. Fields are private and the only constructor runs +/// [`ReplayCapsule::recheck`], so a caller can neither assert "checked" nor +/// attach a digest of its own. +/// +/// ```compile_fail +/// use dr_math_binding_probe::recipe::ProofReference; +/// // No public fields: a proof cannot be written down, only re-checked. +/// let forged = ProofReference { law: todo!(), capsule: todo!() }; +/// ``` +#[derive(Clone, Debug)] pub struct ProofReference { - pub law: LawReference, - pub checker_revision: u32, - pub proof_digest: [u8; 32], - pub status: ProofDisposition, + law: LawReference, + capsule: ReplayCapsule, +} + +impl ProofReference { + /// Re-check `capsule` with a fresh egglog proof session, and require that + /// it proves `law.statement`. + pub fn rechecked(law: LawReference, capsule: ReplayCapsule) -> Result { + if SemanticKey::from(capsule.problem()) != law.statement { + return Err(RecipeRefusal::ProofOfOtherStatement); + } + capsule.recheck().map_err(|_| RecipeRefusal::UncheckedLaw)?; + Ok(Self { law, capsule }) + } + + pub fn law(&self) -> &LawReference { + &self.law + } + + /// egglog's checked proof rendering. + pub fn proof(&self) -> &str { + self.capsule.proof() + } } #[derive(Clone, Copy, Debug, PartialEq, Eq)] @@ -66,12 +100,12 @@ pub enum Backend { ResidentDr64Simd, } -#[derive(Clone, Copy, Debug, PartialEq, Eq)] +#[derive(Clone, Debug, PartialEq, Eq)] pub struct CompiledReference { pub law: LawReference, pub compiled_digest: [u8; 32], pub compiler_revision: u32, - pub target_abi: u32, + pub target: TargetAbi, pub backend: Backend, } @@ -86,8 +120,10 @@ pub enum Capability { pub enum RecipeRefusal { UnsupportedMathematicalShape, LawChanged, + /// The proof did not survive a fresh re-check. UncheckedLaw, - MissingProofIdentity, + /// The proof re-checks, but for a different statement than the law's. + ProofOfOtherStatement, MissingCodeIdentity, WrongTarget, EffectRequiresSeparateAuthorization, @@ -95,7 +131,7 @@ pub enum RecipeRefusal { /// This is a *selection receipt* for an already compiled artifact, not /// executable machine code or a substitute for source/version validation. -#[derive(Clone, Copy, Debug)] +#[derive(Clone, Debug)] pub struct RecipeOffer<'a> { pub operand: BoundDr64<'a>, pub artifact: CompiledReference, @@ -103,15 +139,14 @@ pub struct RecipeOffer<'a> { } /// Cold-stage metadata selection for a mathematically typed, already-bound -/// register. It does not verify proof hashes or attest their provenance; it -/// refuses a missing/unchecked proof *even if* a finite-population report -/// happened to find zero counterexamples. +/// register. The proof was re-checked when the [`ProofReference`] was made; a +/// finite-population report cannot make one. pub fn offer_recipe<'a>( operand: BoundDr64<'a>, primitive: Primitive, proof: ProofReference, compiled: CompiledReference, - runtime_abi: u32, + runtime: &TargetAbi, capability: Capability, ) -> Result, RecipeRefusal> { if capability != Capability::PureMathematics { @@ -124,17 +159,15 @@ pub fn offer_recipe<'a>( if proof.law != compiled.law { return Err(RecipeRefusal::LawChanged); } - if proof.status != ProofDisposition::CheckedByExternalAuthority { - return Err(RecipeRefusal::UncheckedLaw); - } - if proof.checker_revision == 0 || proof.proof_digest == [0u8; 32] { - return Err(RecipeRefusal::MissingProofIdentity); - } if compiled.compiler_revision == 0 || compiled.compiled_digest == [0u8; 32] { return Err(RecipeRefusal::MissingCodeIdentity); } - if compiled.target_abi != runtime_abi { + if &compiled.target != runtime { return Err(RecipeRefusal::WrongTarget); } - Ok(RecipeOffer { operand, artifact: compiled, proof }) + Ok(RecipeOffer { + operand, + artifact: compiled, + proof, + }) } diff --git a/crates/dr-math-binding-probe/tests/recipe.rs b/crates/dr-math-binding-probe/tests/recipe.rs index 66bb1d799..b6be122f8 100644 --- a/crates/dr-math-binding-probe/tests/recipe.rs +++ b/crates/dr-math-binding-probe/tests/recipe.rs @@ -1,92 +1,260 @@ +//! Proof and target identity come from Stage B. The statement used below is +//! Stage B's E1 substitution problem: it is the only kind of statement a +//! checker exists for. Pairing it with a Boolean-DR64 law shape exercises the +//! admission plumbing; it does not claim that E1 proves anything about DR64. use dr_math_binding_probe::{ - bind_dr64, Axis, AxisKind, BindingWitness, MethodSignature, + Axis, AxisKind, BoundDr64, Focus, FrameRevisions, FrameStore, Guards, MethodSignature, Operand, + Scope, bind_dr64, recipe::{ - offer_recipe, Backend, Capability, CompiledReference, LawReference, - LawShape, Primitive, ProofDisposition, ProofReference, RecipeRefusal, + Backend, Capability, CompiledReference, LawReference, LawShape, Primitive, ProofReference, + RecipeRefusal, offer_recipe, }, }; -fn witness() -> BindingWitness { - BindingWitness { source_revision:1, relation_map_revision:2,coordinate_revision:3, - focus_revision:4,authorization_scope:5 } +use egglog_r2il_probe::artifact::ReplayCapsule; +use egglog_r2il_probe::catalogue::{SemanticKey, TargetAbi}; +use egglog_r2il_probe::{chain_problem, e1_problem}; + +const FOCUS: Focus = Focus { revision: 4 }; +const SCOPE: Scope = Scope { id: 5 }; + +fn store() -> FrameStore { + FrameStore::new(FrameRevisions { + source: 1, + relation_map: 2, + coordinates: 3, + }) } -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 }) +/// 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 proof(m:MethodSignature) -> ProofReference { - ProofReference { - law: LawReference { id:41, revision:7, - shape:LawShape::for_method(m,Primitive::CountViolations) }, - checker_revision:1, proof_digest:[17;32], - status:ProofDisposition::CheckedByExternalAuthority, +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), + statement: SemanticKey::from(&e1_problem()), } } -fn compiled(p:ProofReference) -> CompiledReference { - CompiledReference { law:p.law, compiled_digest:[18;32], - compiler_revision:2,target_abi:3,backend:Backend::R2ilMaskRisc } +fn capsule() -> ReplayCapsule { + ReplayCapsule::certify(&e1_problem(), 8).expect("cold E1 certificate") +} +fn proof(m: MethodSignature) -> ProofReference { + ProofReference::rechecked(law(m), capsule()).expect("E1 re-checks") +} +fn abi() -> TargetAbi { + TargetAbi { + revision: 3, + target: "r2il-scalar".to_owned(), + } } +fn compiled(p: &ProofReference) -> CompiledReference { + CompiledReference { + law: p.law().clone(), + compiled_digest: [18; 32], + compiler_revision: 2, + target: abi(), + backend: Backend::R2ilMaskRisc, + } +} + #[test] fn one_law_shape_reuses_two_classes_without_reusing_their_source_binding() { - let rows=[0u64;64]; - let m1=method(1,2,true); - let m2=method(22,8,true); - let a=bind_dr64(m1,m1,witness(),witness(),&rows).unwrap(); - let b=bind_dr64(m2,m2,witness(),witness(),&rows).unwrap(); - let p=proof(m1); - let c=compiled(p); - let aa=offer_recipe(a,Primitive::CountViolations,p,c,3,Capability::PureMathematics).unwrap(); - let bb=offer_recipe(b,Primitive::CountViolations,p,c,3,Capability::PureMathematics).unwrap(); - assert_eq!(aa.proof.law,bb.proof.law); - assert_ne!(aa.operand.method.owner_class,bb.operand.method.owner_class); + let st = store(); + let r = rows(); + let (m1, m2) = (method(1, 2, true), method(22, 8, true)); + let p = proof(m1); + let c = compiled(&p); + let a = offer_recipe( + bind(&st, m1, &r), + Primitive::CountViolations, + p.clone(), + c.clone(), + &abi(), + Capability::PureMathematics, + ) + .unwrap(); + let b = offer_recipe( + bind(&st, m2, &r), + Primitive::CountViolations, + p, + c, + &abi(), + Capability::PureMathematics, + ) + .unwrap(); + assert_eq!(a.proof.law(), b.proof.law()); + assert_ne!(a.operand.method.owner_class, b.operand.method.owner_class); + assert!(!a.proof.proof().is_empty()); } + #[test] fn same_bytes_but_different_axes_cannot_reuse_law() { - let rows=[0u64;64]; - let id2=method(1,2,false); - let bound=bind_dr64(id2,id2,witness(),witness(),&rows).unwrap(); - let p=proof(method(1,2,true)); - assert_eq!(offer_recipe(bound,Primitive::CountViolations,p,compiled(p),3,Capability::PureMathematics) - .unwrap_err(),RecipeRefusal::UnsupportedMathematicalShape); + let st = store(); + let r = rows(); + let p = proof(method(1, 2, true)); + let c = compiled(&p); + assert_eq!( + offer_recipe( + bind(&st, method(1, 2, false), &r), + Primitive::CountViolations, + p, + c, + &abi(), + Capability::PureMathematics + ) + .unwrap_err(), + RecipeRefusal::UnsupportedMathematicalShape + ); } + +/// The forged-digest hole is closed: there is no status flag and no digest +/// field to set, and a real, re-checking proof of a DIFFERENT statement is +/// refused. (Building a `ProofReference` by struct literal does not compile; +/// see the `compile_fail` doctest on the type.) #[test] -fn unverified_conjecture_is_not_admitted_by_a_bare_flag_free_path() { - let rows=[0u64;64];let m=method(1,2,true); - let bound=bind_dr64(m,m,witness(),witness(),&rows).unwrap(); - let mut p=proof(m);p.status=ProofDisposition::Candidate; - assert_eq!(offer_recipe(bound,Primitive::CountViolations,p,compiled(p),3,Capability::PureMathematics) - .unwrap_err(),RecipeRefusal::UncheckedLaw); +fn a_proof_of_another_statement_is_refused() { + let mut l = law(method(1, 2, true)); + l.statement = SemanticKey::from(&chain_problem()); + assert_ne!(l.statement, SemanticKey::from(&e1_problem())); + assert_eq!( + ProofReference::rechecked(l, capsule()).unwrap_err(), + RecipeRefusal::ProofOfOtherStatement + ); } + #[test] fn changed_law_revision_or_target_refuses_cached_recipe() { - let rows=[0u64;64];let m=method(1,2,true); - let bound=bind_dr64(m,m,witness(),witness(),&rows).unwrap(); - let p=proof(m);let mut c=compiled(p);c.law.revision+=1; - assert_eq!(offer_recipe(bound,Primitive::CountViolations,p,c,3,Capability::PureMathematics) - .unwrap_err(),RecipeRefusal::LawChanged); - let c=compiled(p); - assert_eq!(offer_recipe(bound,Primitive::CountViolations,p,c,4,Capability::PureMathematics) - .unwrap_err(),RecipeRefusal::WrongTarget); + let st = store(); + let r = rows(); + let m = method(1, 2, true); + let p = proof(m); + let mut c = compiled(&p); + c.law.revision += 1; + assert_eq!( + offer_recipe( + bind(&st, m, &r), + Primitive::CountViolations, + p.clone(), + c, + &abi(), + Capability::PureMathematics + ) + .unwrap_err(), + RecipeRefusal::LawChanged + ); + for runtime in [ + TargetAbi { + revision: 4, + ..abi() + }, + TargetAbi { + target: "resident-dr64-simd".to_owned(), + ..abi() + }, + ] { + assert_eq!( + offer_recipe( + bind(&st, m, &r), + Primitive::CountViolations, + p.clone(), + compiled(&p), + &runtime, + Capability::PureMathematics + ) + .unwrap_err(), + RecipeRefusal::WrongTarget + ); + } } + #[test] -fn missing_proof_and_code_identities_refuse() { - let rows=[0u64;64];let m=method(1,2,true); - let bound=bind_dr64(m,m,witness(),witness(),&rows).unwrap(); - let mut p=proof(m);p.proof_digest=[0;32]; - assert_eq!(offer_recipe(bound,Primitive::CountViolations,p,compiled(p),3,Capability::PureMathematics) - .unwrap_err(),RecipeRefusal::MissingProofIdentity); - let p=proof(m);let mut c=compiled(p);c.compiled_digest=[0;32]; - assert_eq!(offer_recipe(bound,Primitive::CountViolations,p,c,3,Capability::PureMathematics) - .unwrap_err(),RecipeRefusal::MissingCodeIdentity); +fn missing_code_identity_refuses() { + let st = store(); + let r = rows(); + let m = method(1, 2, true); + let p = proof(m); + for broken in [ + CompiledReference { + compiled_digest: [0; 32], + ..compiled(&p) + }, + CompiledReference { + compiler_revision: 0, + ..compiled(&p) + }, + ] { + assert_eq!( + offer_recipe( + bind(&st, m, &r), + Primitive::CountViolations, + p.clone(), + broken, + &abi(), + Capability::PureMathematics + ) + .unwrap_err(), + RecipeRefusal::MissingCodeIdentity + ); + } } + #[test] fn proof_of_math_never_authorizes_a_cognitive_commit() { - let rows=[0u64;64];let m=method(1,2,true); - let bound=bind_dr64(m,m,witness(),witness(),&rows).unwrap(); - let p=proof(m); - for kind in [Capability::Proposal,Capability::EffectfulAction] { - assert_eq!(offer_recipe(bound,Primitive::CountViolations,p,compiled(p),3,kind) - .unwrap_err(),RecipeRefusal::EffectRequiresSeparateAuthorization); + let st = store(); + let r = rows(); + let m = method(1, 2, true); + let p = proof(m); + for kind in [Capability::Proposal, Capability::EffectfulAction] { + assert_eq!( + offer_recipe( + bind(&st, m, &r), + Primitive::CountViolations, + p.clone(), + compiled(&p), + &abi(), + kind + ) + .unwrap_err(), + RecipeRefusal::EffectRequiresSeparateAuthorization + ); } } From b14dc0377d7d6ce821299ec7019432980f3d4dc3 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 22 Oct 2026 15:23:11 +0000 Subject: [PATCH 3/4] docs(dr-math): state that the recheck call has no failing test yet Disabling ReplayCapsule::recheck in ProofReference::rechecked leaves every test green: a capsule can only come from certify in-process. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg --- crates/dr-math-binding-probe/RECIPE_ADMISSION.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crates/dr-math-binding-probe/RECIPE_ADMISSION.md b/crates/dr-math-binding-probe/RECIPE_ADMISSION.md index c96ebda33..87ab45c44 100644 --- a/crates/dr-math-binding-probe/RECIPE_ADMISSION.md +++ b/crates/dr-math-binding-probe/RECIPE_ADMISSION.md @@ -4,7 +4,7 @@ This experimental metadata layer enforces the **shape of reuse**, not its scient Proof and target identity are Stage B's, not re-spelled here. A `ProofReference` has private fields and one constructor, `ProofReference::rechecked`, which requires the `ReplayCapsule` to prove the law's `statement` (Stage B's `SemanticKey`) and re-runs `ReplayCapsule::recheck` (a fresh egglog proof session, byte-equal proof). There is no caller-set "checked" flag and no caller-supplied proof digest, so the earlier hole (a forged nonzero digest passed) cannot be written. `CompiledReference` identifies the compiler revision, code artifact, backend and Stage B's `TargetAbi`. `RecipeOffer` remains **metadata**, not bytes to execute. -**Limit, stated plainly:** Stage B's checker proves exact-integer substitution statements. No statement language and no checker exist yet for a Boolean-DR64 law, so the tests pair a DR64 law shape with Stage B's E1 statement to exercise the admission plumbing only; that pairing is not a claim that E1 says anything about DR64. Adding the dependency also brings egglog and ogar-loco (git) and the ndarray sibling patch into this probe's build. +**Limit, stated plainly:** Stage B's checker proves exact-integer substitution statements. No statement language and no checker exist yet for a Boolean-DR64 law, so the tests pair a DR64 law shape with Stage B's E1 statement to exercise the admission plumbing only; that pairing is not a claim that E1 says anything about DR64. Adding the dependency also brings egglog and ogar-loco (git) and the ndarray sibling patch into this probe's build. The `recheck` call in `rechecked` has no failing test: a `ReplayCapsule` can only be produced in-process by `certify`, so it always re-checks (disabling the call leaves every test green). The call starts to matter when capsules are stored and loaded; a test for it belongs with that loader. Stage 2's finite-focus `PopulationReport` CANNOT produce a `ProofReference`. Even a complete 64x64 population pass is not a theorem outside its declared scope. From ca88feaf524d27ec3b8172f93ae221934cf980bd Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 22 Oct 2026 15:27:59 +0000 Subject: [PATCH 4/4] =?UTF-8?q?probe(dr-math):=20correct=20X15=20=E2=80=94?= =?UTF-8?q?=20opaque=20certificate,=20ReplayCapsule=20is=20not=20the=20aut?= =?UTF-8?q?hority?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 55f88ef4 made ReplayCapsule::recheck the proof authority for DR64 recipes and paired a DR64 law shape with Stage B's scalar E1 statement in the tests. That conflated two things: egglog derives and checks proofs; ReplayCapsule only retains and replays one E1 compilation. It also treated E1's scalar substitution language as if it covered relational DR64 laws. Corrected: - RecipeCertificate is opaque (no public constructor, no status field), issued only by a certified-compiler boundary after egglog's proof check, law admission and a lowering check. The caller-set CheckedByExternalAuthority flag and the caller-supplied digest stay removed. - No such boundary exists for Boolean-DR64 laws, so admit_recipe runs every metadata check and then refuses with NoCertifiedCompiler. - The egglog-r2il-probe dependency and the ndarray patch are gone; E1 stays Stage B's own replay artifact. - Law identity no longer carries Stage B's SemanticKey; target ABI is back to this probe's own u32. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg --- crates/dr-math-binding-probe/Cargo.toml | 12 - .../dr-math-binding-probe/RECIPE_ADMISSION.md | 8 +- crates/dr-math-binding-probe/src/recipe.rs | 137 ++++++------ crates/dr-math-binding-probe/tests/recipe.rs | 209 ++++++------------ 4 files changed, 143 insertions(+), 223 deletions(-) diff --git a/crates/dr-math-binding-probe/Cargo.toml b/crates/dr-math-binding-probe/Cargo.toml index 867e6aa6b..4969346c0 100644 --- a/crates/dr-math-binding-probe/Cargo.toml +++ b/crates/dr-math-binding-probe/Cargo.toml @@ -10,15 +10,3 @@ description = "Borrowed DR64 / ClassView-style typed structure and source witnes [dependencies] lance-graph-contract = { path = "../lance-graph-contract" } -# Stage B's proof capsule and target ABI (D-DRMC-3 takes proof and target -# identity from there instead of re-spelling them). Pulls egglog and ogar-loco -# by git and ndarray through the sibling patch below. -egglog-r2il-probe = { path = "../egglog-r2il-probe" } - -# The same patches egglog-r2il-probe carries (a path dependency's [patch] -# tables do not apply): one contract and one ndarray identity. -[patch."https://github.com/AdaWorldAPI/lance-graph"] -lance-graph-contract = { path = "../lance-graph-contract" } - -[patch."https://github.com/AdaWorldAPI/ndarray"] -ndarray = { path = "../../../ndarray" } diff --git a/crates/dr-math-binding-probe/RECIPE_ADMISSION.md b/crates/dr-math-binding-probe/RECIPE_ADMISSION.md index 87ab45c44..c431c4989 100644 --- a/crates/dr-math-binding-probe/RECIPE_ADMISSION.md +++ b/crates/dr-math-binding-probe/RECIPE_ADMISSION.md @@ -1,12 +1,12 @@ # 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, law revision and the statement a proof must prove. 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. +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. -Proof and target identity are Stage B's, not re-spelled here. A `ProofReference` has private fields and one constructor, `ProofReference::rechecked`, which requires the `ReplayCapsule` to prove the law's `statement` (Stage B's `SemanticKey`) and re-runs `ReplayCapsule::recheck` (a fresh egglog proof session, byte-equal proof). There is no caller-set "checked" flag and no caller-supplied proof digest, so the earlier hole (a forged nonzero digest passed) cannot be written. `CompiledReference` identifies the compiler revision, code artifact, backend and Stage B's `TargetAbi`. `RecipeOffer` remains **metadata**, not bytes to execute. +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. -**Limit, stated plainly:** Stage B's checker proves exact-integer substitution statements. No statement language and no checker exist yet for a Boolean-DR64 law, so the tests pair a DR64 law shape with Stage B's E1 statement to exercise the admission plumbing only; that pairing is not a claim that E1 says anything about DR64. Adding the dependency also brings egglog and ogar-loco (git) and the ndarray sibling patch into this probe's build. The `recheck` call in `rechecked` has no failing test: a `ReplayCapsule` can only be produced in-process by `certify`, so it always re-checks (disabling the call leaves every test green). The call starts to matter when capsules are stored and loaded; a test for it belongs with that loader. +**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 `ProofReference`. Even a complete 64x64 population pass is not a theorem outside its declared scope. +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. diff --git a/crates/dr-math-binding-probe/src/recipe.rs b/crates/dr-math-binding-probe/src/recipe.rs index 78ed44dd8..d727d7766 100644 --- a/crates/dr-math-binding-probe/src/recipe.rs +++ b/crates/dr-math-binding-probe/src/recipe.rs @@ -5,15 +5,17 @@ //! deliberately excludes class/method and source versions so a proof about a //! mathematical shape can potentially be reused across ClassViews. //! -//! Proof and target identity are Stage B's (`egglog-r2il-probe`): a -//! [`ProofReference`] exists only as a [`ReplayCapsule`] that egglog's own -//! checker re-proved, and the target is Stage B's [`TargetAbi`]. Nothing here -//! lets a caller declare a law checked. Stage B's checker proves exact-integer -//! substitution statements; no statement language or checker exists yet for a -//! Boolean-DR64 law, so the only statements this layer can carry are Stage B's. -use egglog_r2il_probe::artifact::ReplayCapsule; -use egglog_r2il_probe::catalogue::{SemanticKey, TargetAbi}; - +//! 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)] @@ -47,51 +49,11 @@ impl LawShape { } } -/// A law: its id and revision, the DR64 shape it applies to, and the statement -/// a proof must prove. -#[derive(Clone, Debug, PartialEq, Eq)] +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] pub struct LawReference { pub id: u64, pub revision: u32, pub shape: LawShape, - pub statement: SemanticKey, -} - -/// A law together with a proof of its statement that was re-checked when this -/// value was made. Fields are private and the only constructor runs -/// [`ReplayCapsule::recheck`], so a caller can neither assert "checked" nor -/// attach a digest of its own. -/// -/// ```compile_fail -/// use dr_math_binding_probe::recipe::ProofReference; -/// // No public fields: a proof cannot be written down, only re-checked. -/// let forged = ProofReference { law: todo!(), capsule: todo!() }; -/// ``` -#[derive(Clone, Debug)] -pub struct ProofReference { - law: LawReference, - capsule: ReplayCapsule, -} - -impl ProofReference { - /// Re-check `capsule` with a fresh egglog proof session, and require that - /// it proves `law.statement`. - pub fn rechecked(law: LawReference, capsule: ReplayCapsule) -> Result { - if SemanticKey::from(capsule.problem()) != law.statement { - return Err(RecipeRefusal::ProofOfOtherStatement); - } - capsule.recheck().map_err(|_| RecipeRefusal::UncheckedLaw)?; - Ok(Self { law, capsule }) - } - - pub fn law(&self) -> &LawReference { - &self.law - } - - /// egglog's checked proof rendering. - pub fn proof(&self) -> &str { - self.capsule.proof() - } } #[derive(Clone, Copy, Debug, PartialEq, Eq)] @@ -100,15 +62,40 @@ pub enum Backend { ResidentDr64Simd, } -#[derive(Clone, Debug, PartialEq, Eq)] +#[derive(Clone, Copy, Debug, PartialEq, Eq)] pub struct CompiledReference { pub law: LawReference, pub compiled_digest: [u8; 32], pub compiler_revision: u32, - pub target: TargetAbi, + 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, @@ -120,54 +107,62 @@ pub enum Capability { pub enum RecipeRefusal { UnsupportedMathematicalShape, LawChanged, - /// The proof did not survive a fresh re-check. - UncheckedLaw, - /// The proof re-checks, but for a different statement than the law's. - ProofOfOtherStatement, 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 an already compiled artifact, not +/// 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 artifact: CompiledReference, - pub proof: ProofReference, + pub certificate: RecipeCertificate, } -/// Cold-stage metadata selection for a mathematically typed, already-bound -/// register. The proof was re-checked when the [`ProofReference`] was made; a -/// finite-population report cannot make one. -pub fn offer_recipe<'a>( +/// 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, - proof: ProofReference, + law: LawReference, compiled: CompiledReference, - runtime: &TargetAbi, + runtime_abi: u32, capability: Capability, ) -> Result, RecipeRefusal> { if capability != Capability::PureMathematics { return Err(RecipeRefusal::EffectRequiresSeparateAuthorization); } - let observed_shape = LawShape::for_method(operand.method, primitive); - if proof.law.shape != observed_shape { + if law.shape != LawShape::for_method(operand.method, primitive) { return Err(RecipeRefusal::UnsupportedMathematicalShape); } - if proof.law != compiled.law { + 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 != runtime { + if compiled.target_abi != runtime_abi { return Err(RecipeRefusal::WrongTarget); } + let certificate = certify(law, compiled)?; Ok(RecipeOffer { operand, - artifact: compiled, - proof, + 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 index b6be122f8..651d1fecc 100644 --- a/crates/dr-math-binding-probe/tests/recipe.rs +++ b/crates/dr-math-binding-probe/tests/recipe.rs @@ -1,21 +1,19 @@ -//! Proof and target identity come from Stage B. The statement used below is -//! Stage B's E1 substitution problem: it is the only kind of statement a -//! checker exists for. Pairing it with a Boolean-DR64 law shape exercises the -//! admission plumbing; it does not claim that E1 proves anything about DR64. +//! 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, ProofReference, - RecipeRefusal, offer_recipe, + Backend, Capability, CompiledReference, LawReference, LawShape, Primitive, RecipeRefusal, + admit_recipe, }, }; -use egglog_r2il_probe::artifact::ReplayCapsule; -use egglog_r2il_probe::catalogue::{SemanticKey, TargetAbi}; -use egglog_r2il_probe::{chain_problem, e1_problem}; const FOCUS: Focus = Focus { revision: 4 }; const SCOPE: Scope = Scope { id: 5 }; +const ABI: u32 = 3; fn store() -> FrameStore { FrameStore::new(FrameRevisions { @@ -71,167 +69,116 @@ fn law(m: MethodSignature) -> LawReference { id: 41, revision: 7, shape: LawShape::for_method(m, Primitive::CountViolations), - statement: SemanticKey::from(&e1_problem()), } } -fn capsule() -> ReplayCapsule { - ReplayCapsule::certify(&e1_problem(), 8).expect("cold E1 certificate") -} -fn proof(m: MethodSignature) -> ProofReference { - ProofReference::rechecked(law(m), capsule()).expect("E1 re-checks") -} -fn abi() -> TargetAbi { - TargetAbi { - revision: 3, - target: "r2il-scalar".to_owned(), - } -} -fn compiled(p: &ProofReference) -> CompiledReference { +fn compiled(l: LawReference) -> CompiledReference { CompiledReference { - law: p.law().clone(), + law: l, compiled_digest: [18; 32], compiler_revision: 2, - target: abi(), + target_abi: ABI, backend: Backend::R2ilMaskRisc, } } - -#[test] -fn one_law_shape_reuses_two_classes_without_reusing_their_source_binding() { - let st = store(); +fn admit( + st: &FrameStore, + m: MethodSignature, + l: LawReference, + c: CompiledReference, + runtime_abi: u32, + capability: Capability, +) -> RecipeRefusal { let r = rows(); - let (m1, m2) = (method(1, 2, true), method(22, 8, true)); - let p = proof(m1); - let c = compiled(&p); - let a = offer_recipe( - bind(&st, m1, &r), - Primitive::CountViolations, - p.clone(), - c.clone(), - &abi(), - Capability::PureMathematics, - ) - .unwrap(); - let b = offer_recipe( - bind(&st, m2, &r), + admit_recipe( + bind(st, m, &r), Primitive::CountViolations, - p, + l, c, - &abi(), - Capability::PureMathematics, + runtime_abi, + capability, ) - .unwrap(); - assert_eq!(a.proof.law(), b.proof.law()); - assert_ne!(a.operand.method.owner_class, b.operand.method.owner_class); - assert!(!a.proof.proof().is_empty()); + .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 same_bytes_but_different_axes_cannot_reuse_law() { +fn one_law_key_spans_two_classes_and_neither_is_certified() { let st = store(); - let r = rows(); - let p = proof(method(1, 2, true)); - let c = compiled(&p); - assert_eq!( - offer_recipe( - bind(&st, method(1, 2, false), &r), - Primitive::CountViolations, - p, - c, - &abi(), - Capability::PureMathematics - ) - .unwrap_err(), - RecipeRefusal::UnsupportedMathematicalShape - ); + 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 + ); + } } -/// The forged-digest hole is closed: there is no status flag and no digest -/// field to set, and a real, re-checking proof of a DIFFERENT statement is -/// refused. (Building a `ProofReference` by struct literal does not compile; -/// see the `compile_fail` doctest on the type.) #[test] -fn a_proof_of_another_statement_is_refused() { - let mut l = law(method(1, 2, true)); - l.statement = SemanticKey::from(&chain_problem()); - assert_ne!(l.statement, SemanticKey::from(&e1_problem())); +fn same_bytes_but_different_axes_cannot_reuse_law() { + let st = store(); + let l = law(method(1, 2, true)); assert_eq!( - ProofReference::rechecked(l, capsule()).unwrap_err(), - RecipeRefusal::ProofOfOtherStatement + admit( + &st, + method(1, 2, false), + l, + compiled(l), + ABI, + Capability::PureMathematics + ), + RecipeRefusal::UnsupportedMathematicalShape ); } #[test] -fn changed_law_revision_or_target_refuses_cached_recipe() { +fn changed_law_revision_or_target_refuses_before_certification() { let st = store(); - let r = rows(); let m = method(1, 2, true); - let p = proof(m); - let mut c = compiled(&p); + let mut c = compiled(law(m)); c.law.revision += 1; assert_eq!( - offer_recipe( - bind(&st, m, &r), - Primitive::CountViolations, - p.clone(), - c, - &abi(), - Capability::PureMathematics - ) - .unwrap_err(), + admit(&st, m, law(m), c, ABI, Capability::PureMathematics), RecipeRefusal::LawChanged ); - for runtime in [ - TargetAbi { - revision: 4, - ..abi() - }, - TargetAbi { - target: "resident-dr64-simd".to_owned(), - ..abi() - }, - ] { - assert_eq!( - offer_recipe( - bind(&st, m, &r), - Primitive::CountViolations, - p.clone(), - compiled(&p), - &runtime, - Capability::PureMathematics - ) - .unwrap_err(), - RecipeRefusal::WrongTarget - ); - } + 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 r = rows(); let m = method(1, 2, true); - let p = proof(m); for broken in [ CompiledReference { compiled_digest: [0; 32], - ..compiled(&p) + ..compiled(law(m)) }, CompiledReference { compiler_revision: 0, - ..compiled(&p) + ..compiled(law(m)) }, ] { assert_eq!( - offer_recipe( - bind(&st, m, &r), - Primitive::CountViolations, - p.clone(), - broken, - &abi(), - Capability::PureMathematics - ) - .unwrap_err(), + admit(&st, m, law(m), broken, ABI, Capability::PureMathematics), RecipeRefusal::MissingCodeIdentity ); } @@ -240,20 +187,10 @@ fn missing_code_identity_refuses() { #[test] fn proof_of_math_never_authorizes_a_cognitive_commit() { let st = store(); - let r = rows(); let m = method(1, 2, true); - let p = proof(m); for kind in [Capability::Proposal, Capability::EffectfulAction] { assert_eq!( - offer_recipe( - bind(&st, m, &r), - Primitive::CountViolations, - p.clone(), - compiled(&p), - &abi(), - kind - ) - .unwrap_err(), + admit(&st, m, law(m), compiled(law(m)), ABI, kind), RecipeRefusal::EffectRequiresSeparateAuthorization ); }