Skip to content

Commit f357b95

Browse files
kim-emkim-em
authored
Merge pull request #9207 from kim-em/agent/interval-proof-registry
interval: unify semantic and emitter package assembly
2 parents 6e0bfd1 + 8d98d78 commit f357b95

12 files changed

Lines changed: 417 additions & 22 deletions

File tree

‎HexInterval/Experiment/ProofRegistry.lean‎

Lines changed: 133 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,133 @@
1+
/-
2+
Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Kim Morrison
5+
-/
6+
7+
module
8+
9+
public import HexInterval.Experiment.ProofEmitter
10+
11+
@[expose] public section
12+
13+
/-!
14+
# Joint semantic and proof-emitter package assembly
15+
16+
An executable propagator package, its semantic replay schemas, and its tactic
17+
emission handles are three views of one extension point. This module keeps
18+
the latter two views in one descriptor and checks them against the executable
19+
registry in the same package order.
20+
21+
The full replay key includes the rule, event role, and payload schema. Joint
22+
assembly requires exact package-local equality of those keys: an emitter may
23+
neither omit a semantic schema nor borrow one from another package. The
24+
frontend therefore remains function-agnostic without maintaining a second,
25+
potentially divergent registry by hand.
26+
-/
27+
28+
namespace Hex.Interval.Experiment.ProofRegistry
29+
30+
open Propagator PayloadArena SemanticReplay ProofEmitter
31+
32+
/-- The proof-facing declarations contributed by one executable package.
33+
34+
`semantic` contains the package-owned checkers and the corresponding `emit`
35+
fragment contains exactly the handles a tactic may use to apply them. -/
36+
structure Package (semantics : Semantics Fact) (Handle : Type) where
37+
semantic : SemanticReplay.Package semantics
38+
emit : EmitPackage Handle
39+
40+
/-- A semantic registry and emitter table assembled from the same packages. -/
41+
structure Registry (semantics : Semantics Fact) (Handle : Type) where
42+
private mk ::
43+
semantic : SemanticReplay.Registry semantics
44+
emit : SchemaTable Handle
45+
46+
private def make (semantic : SemanticReplay.Registry semantics)
47+
(emit : SchemaTable Handle) : Registry semantics Handle :=
48+
{ semantic, emit }
49+
50+
/-- Failures specific to joint proof-package assembly.
51+
52+
Semantic failures retain the executable/semantic registry diagnostic. The
53+
remaining cases say which package failed exact emitter coverage. -/
54+
inductive BuildError where
55+
| semantic (error : SemanticReplay.BuildError)
56+
| duplicateEmit (key : ReplayKey)
57+
| missingEmit (package : Nat) (key : ReplayKey)
58+
| extraEmit (package : Nat) (key : ReplayKey)
59+
| invalidEmit
60+
deriving DecidableEq, Repr
61+
62+
namespace Package
63+
64+
/-- Exact semantic replay addresses owned by this package. -/
65+
def semanticKeys (package : Package semantics Handle) : List ReplayKey :=
66+
package.semantic.factSchemas.toList.map PackedFactSchema.key ++
67+
package.semantic.instanceSchemas.toList.map PackedInstanceSchema.key ++
68+
package.semantic.equalitySchemas.toList.map PackedEqualitySchema.key
69+
70+
/-- Exact tactic-emission addresses claimed by this package. -/
71+
def emitKeys (package : Package semantics Handle) : List ReplayKey :=
72+
package.emit.schemas.map (fun schema => schema.key)
73+
74+
end Package
75+
76+
def firstDuplicate (seen : List ReplayKey) :
77+
List (SchemaName Handle) -> Option ReplayKey
78+
| [] => none
79+
| schema :: rest =>
80+
if seen.contains schema.key then some schema.key
81+
else firstDuplicate (schema.key :: seen) rest
82+
83+
def checkMissing (package : Nat) (emit : List ReplayKey) :
84+
List ReplayKey -> Except BuildError Unit
85+
| [] => pure ()
86+
| key :: rest =>
87+
if emit.contains key then checkMissing package emit rest
88+
else throw (.missingEmit package key)
89+
90+
def checkExtra (package : Nat) (semantic : List ReplayKey) :
91+
List ReplayKey -> Except BuildError Unit
92+
| [] => pure ()
93+
| key :: rest =>
94+
if semantic.contains key then checkExtra package semantic rest
95+
else throw (.extraEmit package key)
96+
97+
def checkPackages (index : Nat) :
98+
List (Package semantics Handle) -> Except BuildError Unit
99+
| [] => pure ()
100+
| package :: rest => do
101+
let semantic := package.semanticKeys
102+
let emit := package.emitKeys
103+
checkMissing index emit semantic
104+
checkExtra index semantic emit
105+
checkPackages (index + 1) rest
106+
107+
/-- Build the semantic checker and tactic schema table from one package list.
108+
109+
The existing semantic builder first checks exact executable ownership and
110+
coverage. This layer additionally checks exact package-local correspondence
111+
between semantic schemas and emitter handles, plus global emitter uniqueness.
112+
The resulting table is selection data only: emitted theorem applications are
113+
still checked by Lean and by the transparent replay transitions. -/
114+
opaque build (executable : Propagator.Registry Fact)
115+
(packages : Array (Package semantics Handle)) :
116+
Except BuildError (Registry semantics Handle) := do
117+
let semanticPackages := packages.map (fun package => package.semantic)
118+
let semantic ←
119+
match SemanticReplay.Registry.build executable semanticPackages with
120+
| .ok registry => pure registry
121+
| .error error => throw (BuildError.semantic error)
122+
let emitPackages := packages.toList.map (fun package => package.emit)
123+
let entries := emitPackages.flatMap (fun package => package.schemas)
124+
if let some key := firstDuplicate [] entries then
125+
throw (BuildError.duplicateEmit key)
126+
match checkPackages 0 packages.toList with
127+
| .error error => throw error
128+
| .ok _ =>
129+
match SchemaTable.build emitPackages with
130+
| none => throw BuildError.invalidEmit
131+
| some emit => pure (make semantic emit)
132+
133+
end Hex.Interval.Experiment.ProofRegistry

‎HexInterval/SPEC/hex-interval.md‎

Lines changed: 11 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1395,14 +1395,17 @@ entry makes application construction or transparent replay fail. Current
13951395
safety comes from constant lookup, ordinary Lean typechecking, and the replay
13961396
transition's exact key check; only the resulting well-typed theorem
13971397
application enters the kernel.
1398-
The current table invariant proves exact-address uniqueness only; it does not
1399-
yet prove that an emitter fragment and an executable/semantic package fragment
1400-
came from one owner. The canary colocates those declarations, and a missing or
1401-
wrong handle fails during direct emission. Production should either construct
1402-
both registries from one package descriptor or perform an explicit coverage
1403-
cross-check. This ownership relation is a completeness and package-governance
1404-
requirement, not a prerequisite for sound use of selected handles: every
1405-
selected schema must still produce the required kernel-checked claim.
1398+
`ProofRegistry.Package` now joins each package's semantic schemas and emitter
1399+
fragment. Joint assembly first uses the semantic registry check to establish
1400+
exact package-for-package ownership and bidirectional coverage against the
1401+
executable formats. It then requires package-local equality of semantic and
1402+
emitter replay-key sets and global emitter uniqueness. Consequently a handle
1403+
cannot be omitted, added under an undeclared key, or borrowed from another
1404+
package even if the final flattened key set would happen to match. The live
1405+
real-sine semantic replay and direct-emission table are both projections of
1406+
this one checked registry. This governance relation is still defense in depth
1407+
rather than part of theorem soundness: every selected schema must produce the
1408+
required kernel-checked claim.
14061409

14071410
A Mathlib companion must instantiate those abstract schemas, decode each
14081411
frozen entry independently of package cache state, and recheck the

‎HexIntervalMathlib/Experiment/SineSign.lean‎

Lines changed: 36 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ module
88

99
public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
1010
public import Mathlib.Tactic.Linarith
11-
public import HexInterval.Experiment.ProofEmitter
11+
public import HexInterval.Experiment.ProofRegistry
1212
public import HexInterval.Experiment.GenericInstanceReconstruction
1313
public import HexInterval.Experiment.SineSign
1414

@@ -25,7 +25,7 @@ negation propagator, and generic equality transport.
2525

2626
namespace Hex.Interval.Experiment.SineSign
2727

28-
open Propagator SemanticReplay ChronologicalReplay ProofEmitter
28+
open Propagator SemanticReplay ChronologicalReplay ProofEmitter ProofRegistry
2929
open GenericInstanceReconstruction
3030

3131
/-! ## Real interpretation -/
@@ -341,15 +341,12 @@ def oddnessEqualitySchema : PackedEqualitySchema semantics where
341341
else none
342342
else none
343343

344-
def semanticPackages : Array (SemanticReplay.Package semantics) :=
345-
#[{ factSchemas := #[] },
346-
{ factSchemas := #[negationFactSchema] },
347-
{ factSchemas := #[sineFactSchema]
348-
instanceSchemas := #[oddnessInstanceSchema]
349-
equalitySchemas := #[oddnessEqualitySchema] }]
350-
351344
/-! ## Tactic-side schema contributions -/
352345

346+
/-- The source package has no proof-producing replay formats. -/
347+
def sourceEmit : EmitPackage Lean.Name :=
348+
{ schemas := [] }
349+
353350
/-- The negation package exposes only its own fact theorem to proof emitters. -/
354351
def negationEmit : EmitPackage Lean.Name :=
355352
{ schemas :=
@@ -368,6 +365,36 @@ def sineEmit : EmitPackage Lean.Name :=
368365
{ key := oddnessEqualitySchema.key
369366
handle := ``oddnessEqualitySchema }] }
370367

368+
/-! ## Joint package registry -/
369+
370+
/-- Joint proof declaration for the source-expression package. -/
371+
def sourceProof : ProofRegistry.Package semantics Lean.Name :=
372+
{ semantic := { factSchemas := #[] }
373+
emit := sourceEmit }
374+
375+
/-- Joint proof declaration for the independent negation package. -/
376+
def negationProof : ProofRegistry.Package semantics Lean.Name :=
377+
{ semantic := { factSchemas := #[negationFactSchema] }
378+
emit := negationEmit }
379+
380+
/-- Joint proof declaration for sine propagation and oddness instantiation. -/
381+
def sineProof : ProofRegistry.Package semantics Lean.Name :=
382+
{ semantic :=
383+
{ factSchemas := #[sineFactSchema]
384+
instanceSchemas := #[oddnessInstanceSchema]
385+
equalitySchemas := #[oddnessEqualitySchema] }
386+
emit := sineEmit }
387+
388+
/-- One descriptor per executable package, in executable registry order.
389+
This is the source of both semantic replay registration and tactic schema
390+
selection; neither frontend keeps a separate function enumeration. -/
391+
def proofPackages : Array (ProofRegistry.Package semantics Lean.Name) :=
392+
#[sourceProof, negationProof, sineProof]
393+
394+
/-- Compatibility projection for runtime-only semantic replay clients. -/
395+
def semanticPackages : Array (SemanticReplay.Package semantics) :=
396+
proofPackages.map (fun package => package.semantic)
397+
371398
/-! ## Ordinary emitted proof chain -/
372399

373400
def baseFacts : List (NodeFact Range) :=

‎conformance/HexIntervalMathlib/ProofRegistryConformance.lean‎

Lines changed: 124 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,124 @@
1+
/-
2+
Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Kim Morrison
5+
-/
6+
7+
import HexIntervalMathlib.SineSignConformance
8+
9+
/-!
10+
# Joint proof-package registry conformance
11+
12+
The live real-sine executable registry is assembled with its semantic replay
13+
schemas and tactic handles from one package list. Mutations demonstrate that
14+
coverage is exact and package-local rather than merely global.
15+
-/
16+
17+
namespace Hex.IntervalMathlib.ProofRegistryConformance
18+
19+
open Hex.Interval.Experiment
20+
open Propagator PayloadArena SemanticReplay ProofEmitter ProofRegistry SineSign
21+
open SineSignConformance
22+
23+
def built? : Option (ProofRegistry.Registry semantics Lean.Name) := do
24+
let session ← transported?
25+
match ProofRegistry.build session.registry proofPackages with
26+
| .ok registry => some registry
27+
| .error _ => none
28+
29+
#guard
30+
built?.any fun registry =>
31+
registry.emit.find? sineFactSchema.key == some ``sineFactSchema &&
32+
registry.emit.find? negationFactSchema.key == some ``negationFactSchema &&
33+
registry.emit.find? oddnessInstanceSchema.key ==
34+
some ``oddnessInstanceSchema &&
35+
registry.emit.find? oddnessEqualitySchema.key ==
36+
some ``oddnessEqualitySchema
37+
38+
private def missingSine : Array (ProofRegistry.Package semantics Lean.Name) :=
39+
#[sourceProof, negationProof,
40+
{ semantic := sineProof.semantic
41+
emit :=
42+
{ schemas :=
43+
[{ key := oddnessInstanceSchema.key
44+
handle := ``oddnessInstanceSchema },
45+
{ key := oddnessEqualitySchema.key
46+
handle := ``oddnessEqualitySchema }] } }]
47+
48+
#guard
49+
transported?.any fun session =>
50+
match ProofRegistry.build session.registry missingSine with
51+
| .error (.missingEmit 2 key) => key == sineFactSchema.key
52+
| _ => false
53+
54+
private def extraKey : ReplayKey :=
55+
{ rule := sineRuleKey, role := .fact, schema := 99 }
56+
57+
private def extraSine : Array (ProofRegistry.Package semantics Lean.Name) :=
58+
#[sourceProof, negationProof,
59+
{ semantic := sineProof.semantic
60+
emit :=
61+
{ schemas := sineEmit.schemas ++
62+
[{ key := extraKey, handle := ``sineFactSchema }] } }]
63+
64+
#guard
65+
transported?.any fun session =>
66+
match ProofRegistry.build session.registry extraSine with
67+
| .error (.extraEmit 2 key) => key == extraKey
68+
| _ => false
69+
70+
private def borrowed : Array (ProofRegistry.Package semantics Lean.Name) :=
71+
#[sourceProof,
72+
{ semantic := negationProof.semantic
73+
emit :=
74+
{ schemas := negationEmit.schemas ++
75+
[{ key := sineFactSchema.key, handle := ``sineFactSchema }] } },
76+
{ semantic := sineProof.semantic
77+
emit :=
78+
{ schemas :=
79+
[{ key := oddnessInstanceSchema.key
80+
handle := ``oddnessInstanceSchema },
81+
{ key := oddnessEqualitySchema.key
82+
handle := ``oddnessEqualitySchema }] } }]
83+
84+
#guard
85+
transported?.any fun session =>
86+
match ProofRegistry.build session.registry borrowed with
87+
| .error (.extraEmit 1 key) => key == sineFactSchema.key
88+
| _ => false
89+
90+
private def duplicateSine : Array (ProofRegistry.Package semantics Lean.Name) :=
91+
#[sourceProof, negationProof,
92+
{ semantic := sineProof.semantic
93+
emit :=
94+
{ schemas := sineEmit.schemas ++
95+
[{ key := sineFactSchema.key, handle := ``sineFactSchema }] } }]
96+
97+
#guard
98+
transported?.any fun session =>
99+
match ProofRegistry.build session.registry duplicateSine with
100+
| .error (.duplicateEmit key) => key == sineFactSchema.key
101+
| _ => false
102+
103+
private def wrongRole : ReplayKey :=
104+
{ sineFactSchema.key with role := .instance }
105+
106+
private def wrongRolePackages :
107+
Array (ProofRegistry.Package semantics Lean.Name) :=
108+
#[sourceProof, negationProof,
109+
{ semantic := sineProof.semantic
110+
emit :=
111+
{ schemas :=
112+
[{ key := wrongRole, handle := ``sineFactSchema },
113+
{ key := oddnessInstanceSchema.key
114+
handle := ``oddnessInstanceSchema },
115+
{ key := oddnessEqualitySchema.key
116+
handle := ``oddnessEqualitySchema }] } }]
117+
118+
#guard
119+
transported?.any fun session =>
120+
match ProofRegistry.build session.registry wrongRolePackages with
121+
| .error (.missingEmit 2 key) => key == sineFactSchema.key
122+
| _ => false
123+
124+
end Hex.IntervalMathlib.ProofRegistryConformance

‎conformance/HexIntervalMathlib/SineProofConformance.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ open Propagator PayloadArena SemanticReplay ChronologicalReplay ProofEmitter
2424
open SineSign SineSignConformance
2525

2626
def emitTable? : Option (SchemaTable Lean.Name) :=
27-
SchemaTable.build [negationEmit, sineEmit]
27+
fixture?.map (fun fixture => fixture.registry.emit)
2828

2929
#guard
3030
emitTable?.any fun table =>

‎conformance/HexIntervalMathlib/SineSignConformance.lean‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ namespace Hex.IntervalMathlib.SineSignConformance
1919

2020
open Hex.Interval.Experiment
2121
open Propagator PolicySession SemanticReplay ChronologicalReplay TraceReplay
22+
ProofRegistry
2223
open SineSign
2324

2425
def offer? (session : PolicySession.Session Range)
@@ -164,11 +165,11 @@ def transported? : Option (PolicySession.Session Range) := do
164165

165166
structure Fixture where
166167
session : PolicySession.Session Range
167-
registry : SemanticReplay.Registry semantics
168+
registry : ProofRegistry.Registry semantics Lean.Name
168169

169170
def fixture? : Option Fixture := do
170171
let session <- transported?
171-
match SemanticReplay.Registry.build session.registry semanticPackages with
172+
match ProofRegistry.build session.registry proofPackages with
172173
| .ok registry => some { session, registry }
173174
| .error _ => none
174175

@@ -204,7 +205,7 @@ def replayed? :
204205
let trace :=
205206
TraceReplay.Trace.ofEngine fixture.session.state.engine
206207
fixture.session.arena
207-
TraceReplay.replayInput checkerInput fixture.registry rangeSchema laws
208+
TraceReplay.replayInput checkerInput fixture.registry.semantic rangeSchema laws
208209
buildInstance trace baseStable
209210
(by simp [checkerInput, baseProgram, node])
210211
{ node := node 2, version := 1 }

0 commit comments

Comments
 (0)