interval: unify semantic and emitter package assembly

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

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

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) :=

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

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 =>

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 }