From 8d98d78603e2b1524978e7bfcca891ed8f0bf50a Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 11 Aug 2026 17:16:59 +0000 Subject: [PATCH] Propagate provenance honesty through proof registry; progress 20260811T171522Z --- HexInterval/Experiment/ProofRegistry.lean | 133 ++++++++++++++++++ HexInterval/SPEC/hex-interval.md | 19 +-- HexIntervalMathlib/Experiment/SineSign.lean | 45 ++++-- .../ProofRegistryConformance.lean | 124 ++++++++++++++++ .../SineProofConformance.lean | 2 +- .../SineSignConformance.lean | 7 +- lakefile.lean | 3 +- progress/20260811T113644Z.md | 32 +++++ progress/20260811T114837Z.md | 19 +++ progress/20260811T161403Z.md | 27 ++++ progress/20260811T163611Z.md | 22 +++ .../bench/proof_only_runtime_exemptions.json | 6 + 12 files changed, 417 insertions(+), 22 deletions(-) create mode 100644 HexInterval/Experiment/ProofRegistry.lean create mode 100644 conformance/HexIntervalMathlib/ProofRegistryConformance.lean create mode 100644 progress/20260811T113644Z.md create mode 100644 progress/20260811T114837Z.md create mode 100644 progress/20260811T161403Z.md create mode 100644 progress/20260811T163611Z.md diff --git a/HexInterval/Experiment/ProofRegistry.lean b/HexInterval/Experiment/ProofRegistry.lean new file mode 100644 index 000000000..48b054531 --- /dev/null +++ b/HexInterval/Experiment/ProofRegistry.lean @@ -0,0 +1,133 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ + +module + +public import HexInterval.Experiment.ProofEmitter + +@[expose] public section + +/-! +# Joint semantic and proof-emitter package assembly + +An executable propagator package, its semantic replay schemas, and its tactic +emission handles are three views of one extension point. This module keeps +the latter two views in one descriptor and checks them against the executable +registry in the same package order. + +The full replay key includes the rule, event role, and payload schema. Joint +assembly requires exact package-local equality of those keys: an emitter may +neither omit a semantic schema nor borrow one from another package. The +frontend therefore remains function-agnostic without maintaining a second, +potentially divergent registry by hand. +-/ + +namespace Hex.Interval.Experiment.ProofRegistry + +open Propagator PayloadArena SemanticReplay ProofEmitter + +/-- The proof-facing declarations contributed by one executable package. + +`semantic` contains the package-owned checkers and the corresponding `emit` +fragment contains exactly the handles a tactic may use to apply them. -/ +structure Package (semantics : Semantics Fact) (Handle : Type) where + semantic : SemanticReplay.Package semantics + emit : EmitPackage Handle + +/-- A semantic registry and emitter table assembled from the same packages. -/ +structure Registry (semantics : Semantics Fact) (Handle : Type) where + private mk :: + semantic : SemanticReplay.Registry semantics + emit : SchemaTable Handle + +private def make (semantic : SemanticReplay.Registry semantics) + (emit : SchemaTable Handle) : Registry semantics Handle := + { semantic, emit } + +/-- Failures specific to joint proof-package assembly. + +Semantic failures retain the executable/semantic registry diagnostic. The +remaining cases say which package failed exact emitter coverage. -/ +inductive BuildError where + | semantic (error : SemanticReplay.BuildError) + | duplicateEmit (key : ReplayKey) + | missingEmit (package : Nat) (key : ReplayKey) + | extraEmit (package : Nat) (key : ReplayKey) + | invalidEmit + deriving DecidableEq, Repr + +namespace Package + +/-- Exact semantic replay addresses owned by this package. -/ +def semanticKeys (package : Package semantics Handle) : List ReplayKey := + package.semantic.factSchemas.toList.map PackedFactSchema.key ++ + package.semantic.instanceSchemas.toList.map PackedInstanceSchema.key ++ + package.semantic.equalitySchemas.toList.map PackedEqualitySchema.key + +/-- Exact tactic-emission addresses claimed by this package. -/ +def emitKeys (package : Package semantics Handle) : List ReplayKey := + package.emit.schemas.map (fun schema => schema.key) + +end Package + +def firstDuplicate (seen : List ReplayKey) : + List (SchemaName Handle) -> Option ReplayKey + | [] => none + | schema :: rest => + if seen.contains schema.key then some schema.key + else firstDuplicate (schema.key :: seen) rest + +def checkMissing (package : Nat) (emit : List ReplayKey) : + List ReplayKey -> Except BuildError Unit + | [] => pure () + | key :: rest => + if emit.contains key then checkMissing package emit rest + else throw (.missingEmit package key) + +def checkExtra (package : Nat) (semantic : List ReplayKey) : + List ReplayKey -> Except BuildError Unit + | [] => pure () + | key :: rest => + if semantic.contains key then checkExtra package semantic rest + else throw (.extraEmit package key) + +def checkPackages (index : Nat) : + List (Package semantics Handle) -> Except BuildError Unit + | [] => pure () + | package :: rest => do + let semantic := package.semanticKeys + let emit := package.emitKeys + checkMissing index emit semantic + checkExtra index semantic emit + checkPackages (index + 1) rest + +/-- Build the semantic checker and tactic schema table from one package list. + +The existing semantic builder first checks exact executable ownership and +coverage. This layer additionally checks exact package-local correspondence +between semantic schemas and emitter handles, plus global emitter uniqueness. +The resulting table is selection data only: emitted theorem applications are +still checked by Lean and by the transparent replay transitions. -/ +opaque build (executable : Propagator.Registry Fact) + (packages : Array (Package semantics Handle)) : + Except BuildError (Registry semantics Handle) := do + let semanticPackages := packages.map (fun package => package.semantic) + let semantic ← + match SemanticReplay.Registry.build executable semanticPackages with + | .ok registry => pure registry + | .error error => throw (BuildError.semantic error) + let emitPackages := packages.toList.map (fun package => package.emit) + let entries := emitPackages.flatMap (fun package => package.schemas) + if let some key := firstDuplicate [] entries then + throw (BuildError.duplicateEmit key) + match checkPackages 0 packages.toList with + | .error error => throw error + | .ok _ => + match SchemaTable.build emitPackages with + | none => throw BuildError.invalidEmit + | some emit => pure (make semantic emit) + +end Hex.Interval.Experiment.ProofRegistry diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index 67d51777a..6fb0733a7 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -1395,14 +1395,17 @@ entry makes application construction or transparent replay fail. Current safety comes from constant lookup, ordinary Lean typechecking, and the replay transition's exact key check; only the resulting well-typed theorem application enters the kernel. -The current table invariant proves exact-address uniqueness only; it does not -yet prove that an emitter fragment and an executable/semantic package fragment -came from one owner. The canary colocates those declarations, and a missing or -wrong handle fails during direct emission. Production should either construct -both registries from one package descriptor or perform an explicit coverage -cross-check. This ownership relation is a completeness and package-governance -requirement, not a prerequisite for sound use of selected handles: every -selected schema must still produce the required kernel-checked claim. +`ProofRegistry.Package` now joins each package's semantic schemas and emitter +fragment. Joint assembly first uses the semantic registry check to establish +exact package-for-package ownership and bidirectional coverage against the +executable formats. It then requires package-local equality of semantic and +emitter replay-key sets and global emitter uniqueness. Consequently a handle +cannot be omitted, added under an undeclared key, or borrowed from another +package even if the final flattened key set would happen to match. The live +real-sine semantic replay and direct-emission table are both projections of +this one checked registry. This governance relation is still defense in depth +rather than part of theorem soundness: every selected schema must produce the +required kernel-checked claim. A Mathlib companion must instantiate those abstract schemas, decode each frozen entry independently of package cache state, and recheck the diff --git a/HexIntervalMathlib/Experiment/SineSign.lean b/HexIntervalMathlib/Experiment/SineSign.lean index 51af76f37..aaa99cfec 100644 --- a/HexIntervalMathlib/Experiment/SineSign.lean +++ b/HexIntervalMathlib/Experiment/SineSign.lean @@ -8,7 +8,7 @@ module public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic public import Mathlib.Tactic.Linarith -public import HexInterval.Experiment.ProofEmitter +public import HexInterval.Experiment.ProofRegistry public import HexInterval.Experiment.GenericInstanceReconstruction public import HexInterval.Experiment.SineSign @@ -25,7 +25,7 @@ negation propagator, and generic equality transport. namespace Hex.Interval.Experiment.SineSign -open Propagator SemanticReplay ChronologicalReplay ProofEmitter +open Propagator SemanticReplay ChronologicalReplay ProofEmitter ProofRegistry open GenericInstanceReconstruction /-! ## Real interpretation -/ @@ -341,15 +341,12 @@ def oddnessEqualitySchema : PackedEqualitySchema semantics where else none else none -def semanticPackages : Array (SemanticReplay.Package semantics) := - #[{ factSchemas := #[] }, - { factSchemas := #[negationFactSchema] }, - { factSchemas := #[sineFactSchema] - instanceSchemas := #[oddnessInstanceSchema] - equalitySchemas := #[oddnessEqualitySchema] }] - /-! ## Tactic-side schema contributions -/ +/-- The source package has no proof-producing replay formats. -/ +def sourceEmit : EmitPackage Lean.Name := + { schemas := [] } + /-- The negation package exposes only its own fact theorem to proof emitters. -/ def negationEmit : EmitPackage Lean.Name := { schemas := @@ -368,6 +365,36 @@ def sineEmit : EmitPackage Lean.Name := { key := oddnessEqualitySchema.key handle := ``oddnessEqualitySchema }] } +/-! ## Joint package registry -/ + +/-- Joint proof declaration for the source-expression package. -/ +def sourceProof : ProofRegistry.Package semantics Lean.Name := + { semantic := { factSchemas := #[] } + emit := sourceEmit } + +/-- Joint proof declaration for the independent negation package. -/ +def negationProof : ProofRegistry.Package semantics Lean.Name := + { semantic := { factSchemas := #[negationFactSchema] } + emit := negationEmit } + +/-- Joint proof declaration for sine propagation and oddness instantiation. -/ +def sineProof : ProofRegistry.Package semantics Lean.Name := + { semantic := + { factSchemas := #[sineFactSchema] + instanceSchemas := #[oddnessInstanceSchema] + equalitySchemas := #[oddnessEqualitySchema] } + emit := sineEmit } + +/-- One descriptor per executable package, in executable registry order. +This is the source of both semantic replay registration and tactic schema +selection; neither frontend keeps a separate function enumeration. -/ +def proofPackages : Array (ProofRegistry.Package semantics Lean.Name) := + #[sourceProof, negationProof, sineProof] + +/-- Compatibility projection for runtime-only semantic replay clients. -/ +def semanticPackages : Array (SemanticReplay.Package semantics) := + proofPackages.map (fun package => package.semantic) + /-! ## Ordinary emitted proof chain -/ def baseFacts : List (NodeFact Range) := diff --git a/conformance/HexIntervalMathlib/ProofRegistryConformance.lean b/conformance/HexIntervalMathlib/ProofRegistryConformance.lean new file mode 100644 index 000000000..fe759ff91 --- /dev/null +++ b/conformance/HexIntervalMathlib/ProofRegistryConformance.lean @@ -0,0 +1,124 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ + +import HexIntervalMathlib.SineSignConformance + +/-! +# Joint proof-package registry conformance + +The live real-sine executable registry is assembled with its semantic replay +schemas and tactic handles from one package list. Mutations demonstrate that +coverage is exact and package-local rather than merely global. +-/ + +namespace Hex.IntervalMathlib.ProofRegistryConformance + +open Hex.Interval.Experiment +open Propagator PayloadArena SemanticReplay ProofEmitter ProofRegistry SineSign +open SineSignConformance + +def built? : Option (ProofRegistry.Registry semantics Lean.Name) := do + let session ← transported? + match ProofRegistry.build session.registry proofPackages with + | .ok registry => some registry + | .error _ => none + +#guard + built?.any fun registry => + registry.emit.find? sineFactSchema.key == some ``sineFactSchema && + registry.emit.find? negationFactSchema.key == some ``negationFactSchema && + registry.emit.find? oddnessInstanceSchema.key == + some ``oddnessInstanceSchema && + registry.emit.find? oddnessEqualitySchema.key == + some ``oddnessEqualitySchema + +private def missingSine : Array (ProofRegistry.Package semantics Lean.Name) := + #[sourceProof, negationProof, + { semantic := sineProof.semantic + emit := + { schemas := + [{ key := oddnessInstanceSchema.key + handle := ``oddnessInstanceSchema }, + { key := oddnessEqualitySchema.key + handle := ``oddnessEqualitySchema }] } }] + +#guard + transported?.any fun session => + match ProofRegistry.build session.registry missingSine with + | .error (.missingEmit 2 key) => key == sineFactSchema.key + | _ => false + +private def extraKey : ReplayKey := + { rule := sineRuleKey, role := .fact, schema := 99 } + +private def extraSine : Array (ProofRegistry.Package semantics Lean.Name) := + #[sourceProof, negationProof, + { semantic := sineProof.semantic + emit := + { schemas := sineEmit.schemas ++ + [{ key := extraKey, handle := ``sineFactSchema }] } }] + +#guard + transported?.any fun session => + match ProofRegistry.build session.registry extraSine with + | .error (.extraEmit 2 key) => key == extraKey + | _ => false + +private def borrowed : Array (ProofRegistry.Package semantics Lean.Name) := + #[sourceProof, + { semantic := negationProof.semantic + emit := + { schemas := negationEmit.schemas ++ + [{ key := sineFactSchema.key, handle := ``sineFactSchema }] } }, + { semantic := sineProof.semantic + emit := + { schemas := + [{ key := oddnessInstanceSchema.key + handle := ``oddnessInstanceSchema }, + { key := oddnessEqualitySchema.key + handle := ``oddnessEqualitySchema }] } }] + +#guard + transported?.any fun session => + match ProofRegistry.build session.registry borrowed with + | .error (.extraEmit 1 key) => key == sineFactSchema.key + | _ => false + +private def duplicateSine : Array (ProofRegistry.Package semantics Lean.Name) := + #[sourceProof, negationProof, + { semantic := sineProof.semantic + emit := + { schemas := sineEmit.schemas ++ + [{ key := sineFactSchema.key, handle := ``sineFactSchema }] } }] + +#guard + transported?.any fun session => + match ProofRegistry.build session.registry duplicateSine with + | .error (.duplicateEmit key) => key == sineFactSchema.key + | _ => false + +private def wrongRole : ReplayKey := + { sineFactSchema.key with role := .instance } + +private def wrongRolePackages : + Array (ProofRegistry.Package semantics Lean.Name) := + #[sourceProof, negationProof, + { semantic := sineProof.semantic + emit := + { schemas := + [{ key := wrongRole, handle := ``sineFactSchema }, + { key := oddnessInstanceSchema.key + handle := ``oddnessInstanceSchema }, + { key := oddnessEqualitySchema.key + handle := ``oddnessEqualitySchema }] } }] + +#guard + transported?.any fun session => + match ProofRegistry.build session.registry wrongRolePackages with + | .error (.missingEmit 2 key) => key == sineFactSchema.key + | _ => false + +end Hex.IntervalMathlib.ProofRegistryConformance diff --git a/conformance/HexIntervalMathlib/SineProofConformance.lean b/conformance/HexIntervalMathlib/SineProofConformance.lean index e56db1e48..c429c4cf1 100644 --- a/conformance/HexIntervalMathlib/SineProofConformance.lean +++ b/conformance/HexIntervalMathlib/SineProofConformance.lean @@ -24,7 +24,7 @@ open Propagator PayloadArena SemanticReplay ChronologicalReplay ProofEmitter open SineSign SineSignConformance def emitTable? : Option (SchemaTable Lean.Name) := - SchemaTable.build [negationEmit, sineEmit] + fixture?.map (fun fixture => fixture.registry.emit) #guard emitTable?.any fun table => diff --git a/conformance/HexIntervalMathlib/SineSignConformance.lean b/conformance/HexIntervalMathlib/SineSignConformance.lean index e1ca8c214..a4c53cc33 100644 --- a/conformance/HexIntervalMathlib/SineSignConformance.lean +++ b/conformance/HexIntervalMathlib/SineSignConformance.lean @@ -19,6 +19,7 @@ namespace Hex.IntervalMathlib.SineSignConformance open Hex.Interval.Experiment open Propagator PolicySession SemanticReplay ChronologicalReplay TraceReplay + ProofRegistry open SineSign def offer? (session : PolicySession.Session Range) @@ -164,11 +165,11 @@ def transported? : Option (PolicySession.Session Range) := do structure Fixture where session : PolicySession.Session Range - registry : SemanticReplay.Registry semantics + registry : ProofRegistry.Registry semantics Lean.Name def fixture? : Option Fixture := do let session <- transported? - match SemanticReplay.Registry.build session.registry semanticPackages with + match ProofRegistry.build session.registry proofPackages with | .ok registry => some { session, registry } | .error _ => none @@ -204,7 +205,7 @@ def replayed? : let trace := TraceReplay.Trace.ofEngine fixture.session.state.engine fixture.session.arena - TraceReplay.replayInput checkerInput fixture.registry rangeSchema laws + TraceReplay.replayInput checkerInput fixture.registry.semantic rangeSchema laws buildInstance trace baseStable (by simp [checkerInput, baseProgram, node]) { node := node 2, version := 1 } diff --git a/lakefile.lean b/lakefile.lean index efca6a658..a3012e113 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -310,6 +310,7 @@ lean_lib HexIntervalExperiment where `HexInterval.Experiment.ChronologicalReplay, `HexInterval.Experiment.GenericInstanceReconstruction, `HexInterval.Experiment.ProofEmitter, + `HexInterval.Experiment.ProofRegistry, `HexInterval.Experiment.TraceReplay, `HexInterval.Experiment.SineSign] @@ -379,7 +380,7 @@ lean_lib HexRCFProofProbeScientific where -- `*_emit_fixtures` exes below, carrying `srcDir := "conformance"`. lean_lib HexConformance where srcDir := "conformance" - globs := #[`HexArith.Conformance, `HexArith.CrossCheck, `HexBerlekamp.Conformance, `HexBerlekampZassenhaus.Conformance, `HexBerlekampZassenhaus.CrossCheck, `HexConway.Conformance, `HexGF2.Conformance, `HexGF2.CrossCheck, `HexGF2.FastCheck, `HexGFq.Conformance, `HexGFq.CrossCheck, `HexGFqField.Conformance, `HexGFqRing.Conformance, `HexGramSchmidt.Conformance, `HexHensel.Conformance, `HexHensel.CrossCheck, `HexInterval.Conformance, `HexInterval.CenterConformance, `HexInterval.ScaleConformance, `HexInterval.PropagatorConformance, `HexInterval.ScopeConformance, `HexInterval.StructuralMatcherConformance, `HexInterval.MatcherSchedulerConformance, `HexInterval.StructureViewConformance, `HexInterval.PolicyConformance, `HexInterval.PolicyFrontierConformance, `HexInterval.PolicyDriverConformance, `HexInterval.PackageRegistryConformance, `HexInterval.DyadicIntervalConformance, `HexInterval.DyadicRulesConformance, `HexInterval.PayloadArenaConformance, `HexInterval.PayloadSessionConformance, `HexInterval.PolicySessionConformance, `HexInterval.PolicyFunctionConformance, `HexInterval.SemanticReplayConformance, `HexInterval.ChronologicalReplayConformance, `HexInterval.GenericInstanceReconstructionConformance, `HexInterval.ProofEmitterConformance, `HexInterval.TraceReplayConformance, `HexIntervalMathlib.SineSignConformance, `HexIntervalMathlib.SineProofConformance, `HexIntervalMathlib.SineTacticConformance, `HexLLL.Conformance, `HexMatrix.Conformance, `HexMvPolyFixtures, `HexMvPoly.Conformance, `HexMvPolyMathlib.Conformance, `HexRowReduce.Conformance, `HexDeterminant.Conformance, `HexBareiss.Conformance, `HexModArith.Conformance, `HexModArith.FastCheck, `HexNumberField.Conformance, `HexNumberFieldTower.Conformance, `HexPoly.Conformance, `HexPolyFp.Conformance, `HexPolyZ.Conformance, `HexRCF.Conformance, `HexRealRoots.Conformance, `HexRealRootsMathlib.Conformance, `HexResultant.Conformance, `HexRoots.Conformance].map Glob.one + globs := #[`HexArith.Conformance, `HexArith.CrossCheck, `HexBerlekamp.Conformance, `HexBerlekampZassenhaus.Conformance, `HexBerlekampZassenhaus.CrossCheck, `HexConway.Conformance, `HexGF2.Conformance, `HexGF2.CrossCheck, `HexGF2.FastCheck, `HexGFq.Conformance, `HexGFq.CrossCheck, `HexGFqField.Conformance, `HexGFqRing.Conformance, `HexGramSchmidt.Conformance, `HexHensel.Conformance, `HexHensel.CrossCheck, `HexInterval.Conformance, `HexInterval.CenterConformance, `HexInterval.ScaleConformance, `HexInterval.PropagatorConformance, `HexInterval.ScopeConformance, `HexInterval.StructuralMatcherConformance, `HexInterval.MatcherSchedulerConformance, `HexInterval.StructureViewConformance, `HexInterval.PolicyConformance, `HexInterval.PolicyFrontierConformance, `HexInterval.PolicyDriverConformance, `HexInterval.PackageRegistryConformance, `HexInterval.DyadicIntervalConformance, `HexInterval.DyadicRulesConformance, `HexInterval.PayloadArenaConformance, `HexInterval.PayloadSessionConformance, `HexInterval.PolicySessionConformance, `HexInterval.PolicyFunctionConformance, `HexInterval.SemanticReplayConformance, `HexInterval.ChronologicalReplayConformance, `HexInterval.GenericInstanceReconstructionConformance, `HexInterval.ProofEmitterConformance, `HexInterval.TraceReplayConformance, `HexIntervalMathlib.SineSignConformance, `HexIntervalMathlib.SineProofConformance, `HexIntervalMathlib.SineTacticConformance, `HexIntervalMathlib.ProofRegistryConformance, `HexLLL.Conformance, `HexMatrix.Conformance, `HexMvPolyFixtures, `HexMvPoly.Conformance, `HexMvPolyMathlib.Conformance, `HexRowReduce.Conformance, `HexDeterminant.Conformance, `HexBareiss.Conformance, `HexModArith.Conformance, `HexModArith.FastCheck, `HexNumberField.Conformance, `HexNumberFieldTower.Conformance, `HexPoly.Conformance, `HexPolyFp.Conformance, `HexPolyZ.Conformance, `HexRCF.Conformance, `HexRealRoots.Conformance, `HexRealRootsMathlib.Conformance, `HexResultant.Conformance, `HexRoots.Conformance].map Glob.one -- Public umbrellas intentionally contain only the supported API. Executable -- examples and regression tests are compiled through this separate target so diff --git a/progress/20260811T113644Z.md b/progress/20260811T113644Z.md new file mode 100644 index 000000000..f6de35f6c --- /dev/null +++ b/progress/20260811T113644Z.md @@ -0,0 +1,32 @@ +# Accomplished + +- Added a Mathlib-free joint proof-package registry which assembles semantic + replay schemas and tactic emission handles against the same executable + package order. +- Enforced exact package-local replay-key coverage, global emitter uniqueness, + and preservation of the rule/role/schema dispatch address. +- Made the real sine, negation, and source packages the single source for both + semantic replay registration and tactic schema selection. +- Routed the live sine trace checker and direct proof-emitting tactic through + that joint registry. +- Added live conformance mutations for missing, extra, borrowed, duplicated, + and wrong-role emitter declarations. +- Updated the SPEC and passed the focused 1,959-target build plus structural, + conformance-registration, freshness, and banned-proof checks. + +# Current frontier + +Arbitrary function packages now contribute executable behavior, semantic +replay, and frontend handles without a central function enumeration or a +second independently assembled proof table. The real-sine frontend still +constructs its caller graph and final target through canary-specific code. + +# Next step + +Extract the function-independent event fold and goal-to-base-graph boundary +from the sine conformance fixture into a reusable frontend module, then test a +second mathematical function package through the same API. + +# Blockers + +None. diff --git a/progress/20260811T114837Z.md b/progress/20260811T114837Z.md new file mode 100644 index 000000000..e4233cdcc --- /dev/null +++ b/progress/20260811T114837Z.md @@ -0,0 +1,19 @@ +# Accomplished + +- Sealed the joint proof-registry constructor so callers cannot bypass package + ownership and coverage checks by manually pairing unrelated registries. +- Kept assembly executable through an opaque checked builder and rebuilt the + real-sine joint-registry conformance target. + +# Current frontier + +The joint package invariant is now enforced by the public API as well as by +the builder's validation. + +# Next step + +Continue extracting the generic proof-event fold from the sine tactic canary. + +# Blockers + +None. diff --git a/progress/20260811T161403Z.md b/progress/20260811T161403Z.md new file mode 100644 index 000000000..40f089f8c --- /dev/null +++ b/progress/20260811T161403Z.md @@ -0,0 +1,27 @@ +# Accomplished + +- Reconciled joint semantic/emitter package assembly with repeated + instantiation and the current proof-emission stack. +- Preserved exact package-local replay-key coverage, global address + uniqueness, and construction of both proof registries from one package + order. +- Adapted the joint registry to the current handle-polymorphic schema type and + refreshed the exact proof-only Lake registration exemption. +- Built the joint registry, sine tactic, and proof-registry conformance targets + successfully. + +# Current frontier + +Function packages now contribute semantic replay and proof-emission handles +through one checked descriptor aligned with the executable registry. The next +layer moves the generic event fold out of the sine fixture into a reusable +frontend. + +# Next step + +Push the reconciled exact head for independent review, then reconcile and test +the generic frontend with a second function package. + +# Blockers + +None. diff --git a/progress/20260811T163611Z.md b/progress/20260811T163611Z.md new file mode 100644 index 000000000..cc586d560 --- /dev/null +++ b/progress/20260811T163611Z.md @@ -0,0 +1,22 @@ +# Accomplished + +- Propagated the selected-schema trust correction and guarded sine theorem + axiom report into the sealed joint proof registry. +- Reconciled the wording with the registry's stronger invariant: semantic and + emitter fragments now have checked package ownership and bidirectional key + coverage, while kernel typechecking remains the proof-safety boundary. + +# Current frontier + +The joint registry supplies package governance and completeness checks without +being confused with trusted evidence. Selected schema applications still must +construct the exact kernel-checked claim. + +# Next step + +Finish builds and static checks, push the exact head for review, then propagate +the repair into the reusable generic proof frontend. + +# Blockers + +None. diff --git a/scripts/bench/proof_only_runtime_exemptions.json b/scripts/bench/proof_only_runtime_exemptions.json index c069bd6f5..b013f2a96 100644 --- a/scripts/bench/proof_only_runtime_exemptions.json +++ b/scripts/bench/proof_only_runtime_exemptions.json @@ -89,6 +89,12 @@ "current_blob": "efca6a658b0a62ad3de48d957ed2c834966e68c1", "reason": "Additionally registers the elaborator canary which runs interval planning and emits the existing transparent Real.sin proof; the factorization service target and executable dependency graph are unchanged." }, + { + "path": "lakefile.lean", + "baseline_blob": "6dd80771ae2212333b2a9b925b52056e0037ff56", + "current_blob": "a3012e11352a5930dad20e5f88fce9a0826214f2", + "reason": "Additionally registers joint interval semantic/emitter package assembly and its conformance module only; the factorization service target and executable dependency graph are unchanged." + }, { "path": "HexBerlekamp/FactorTacticTests.lean", "baseline_blob": "4063e15934a89c671ac72d201fa60c2ef6feaf59",