From 2f2f7ee6925b344e08aff88bd5487ccfe2385879 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 11 Aug 2026 11:26:23 +0000 Subject: [PATCH 1/2] interval: replay repeated instantiations generically --- HexInterval/Experiment/ProofEmitter.lean | 38 +++ HexInterval/SPEC/hex-interval.md | 39 ++- HexIntervalMathlib/Experiment/SineSign.lean | 37 +++ .../SineTacticConformance.lean | 303 +++++++++++++++--- progress/20260811T112551Z.md | 40 +++ 5 files changed, 398 insertions(+), 59 deletions(-) create mode 100644 progress/20260811T112551Z.md diff --git a/HexInterval/Experiment/ProofEmitter.lean b/HexInterval/Experiment/ProofEmitter.lean index 51c21506d..2cd0d7712 100644 --- a/HexInterval/Experiment/ProofEmitter.lean +++ b/HexInterval/Experiment/ProofEmitter.lean @@ -152,6 +152,44 @@ def assumedAt {Fact : Type} {semantics : Semantics Fact} (program : Program) Evidence (semantics.Entails program base fact) := assumed (memOfGet? base index fact found) +/-- The node of a caller fact selected by `assumedAt` is within the current +program whenever the complete base list is. -/ +theorem factWithinAt {Fact : Type} (program : Program) + (base : List (NodeFact Fact)) (within : FactsWithin program base) + (index : Nat) (fact : NodeFact Fact) (found : base[index]? = some fact) : + fact.node.index < program.nodes.size := + within fact (memOfGet? base index fact found) + +/-- A successful exact node lookup proves the corresponding size bound. -/ +theorem nodeWithin (program : Program) (node : NodeId) (instruction : Node) + (found : program.node? node = some instruction) : + node.index < program.nodes.size := by + by_cases within : node.index < program.nodes.size + · exact within + · simp [Program.node?, within] at found + +/-- Old node membership remains valid across an append-only prefix. -/ +theorem liftNode {before after : Program} (step : ProgramPrefix before after) + {node : NodeId} (within : node.index < before.nodes.size) : + node.index < after.nodes.size := + Nat.lt_of_lt_of_le within step.nodeSize + +/-- A complete base context remains within every append-only program. -/ +theorem liftFacts {Fact : Type} {before after : Program} + (step : ProgramPrefix before after) {facts : List (NodeFact Fact)} + (within : FactsWithin before facts) : FactsWithin after facts := + fun fact member => liftNode step (within fact member) + +/-- Transport one table entry to an enlarged program. -/ +def liftFact {Fact : Type} {semantics : Semantics Fact} + {before after : Program} {base : List (NodeFact Fact)} + {fact : NodeFact Fact} (step : StableStep semantics before after) + (baseWithin : FactsWithin before base) + (sound : Evidence (semantics.Entails before base fact)) + (factWithin : fact.node.index < before.nodes.size) : + Evidence (semantics.Entails after base fact) := + liftEntails step baseWithin factWithin sound + /-- Prove the domain's top fact for any exactly checked node. The chronology emitter uses this theorem to seed generated nodes at version zero; that generated/version condition belongs to its evidence-table discipline, not to diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index 52088c427..abafbbb5f 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -1246,9 +1246,13 @@ central case split over function keys. The transparent the exact prefix of the retained final node array selected by `event.newNodes`, keeps the operation table fixed, and obtains stability from one semantics-wide prefix-locality law. It covers both ordinary node appends and -zero-node version-only instances. Integrating this arm into `TraceReplay` and -comparing it with package-dispatched reconstruction remains experimental. -Neither arm may introduce a central enumeration of functions. +zero-node version-only instances. The direct proof emitter now uses this arm +at every quoted instantiation event: it replays the owning package's +conservative-extension theorem, lifts every retained fact proof through the +semantics-wide stability law, and seeds exactly the event's fresh nodes with +top. Integrating the same arm into runtime `TraceReplay` and comparing it with +package-dispatched reconstruction remains experimental. Neither arm may +introduce a central enumeration of functions. The private chronological cursor is indexed by its exact program version and program value. Its instance transition requires the originating action to @@ -1314,15 +1318,20 @@ yet the general tactic. Its elaborator walks the arbitrary quoted event list and maintains an exact `(node, version)` evidence table. Rule and transport steps obtain their previous facts and ordered dependencies from this table, select their package schemas solely by replay address, and insert their proved -result versions. Reordering negation before the sine result it consumes fails -before replay. This event fold contains no sine, negation, or other function -case. It seeds caller facts by checked position in the exact base-assumption -list and seeds the instance event's fresh nodes with domain top after checking -their lookup in the reified final program; named sine-specific previous-fact -proofs are absent from the tactic term. The next frontend experiment must -derive the base program, semantic bridge, and final target for an arbitrary -caller expression, and reconstruct intermediate programs for later or -repeated instantiations, instead of naming this canary's fixed contexts. +result versions. The same fold accepts instantiation events at arbitrary +chronology positions. It reconstructs each intermediate graph as the exact +prefix of the reified final program, carries the independently established +program version, transports the complete evidence table across stability, and +then seeds the new-node suffix. A second zero-node instance can therefore +advance the version after the sine and negation rules while preserving the +negation evidence needed by a later equality transport. Reordering negation +before the sine result it consumes, or claiming the wrong program version, +fails before replay. This event fold contains no sine, negation, or other +function case. It seeds caller facts by checked position in the exact +base-assumption list; named sine-specific previous-fact proofs are absent from +the tactic term. The next frontend experiment must derive the base program, +semantic bridge, and final target for an arbitrary caller expression instead +of naming this canary's fixed contexts. The fixed canary also requires a live session with an exact proof history of one instance, one equality, three fact events, and the expected interleaving before it reads historical values through `Engine.factAt?`. Those values are quoted @@ -1334,9 +1343,9 @@ earlier step. The quotation walker consumes arbitrary `HistoryEvent` lists, requires sequential role-local indices, and rejects omitted or duplicated fact or instance records through final exhaustion. Proof emission then folds the -resulting fact events through its evidence state. The present fold permits one -leading instance event; supporting later or repeated instantiations requires -updating the checked program and seeding each new node at the corresponding +resulting fact and instance events through its dependent program/evidence +state. Repeated and zero-node instantiations update the checked program, +version, prefix, extension theorem, fact bounds, and fact proofs at the exact chronology position. A general direct emitter maintains a table from each already-established fact diff --git a/HexIntervalMathlib/Experiment/SineSign.lean b/HexIntervalMathlib/Experiment/SineSign.lean index 64278b3c3..3116242dc 100644 --- a/HexIntervalMathlib/Experiment/SineSign.lean +++ b/HexIntervalMathlib/Experiment/SineSign.lean @@ -9,6 +9,7 @@ module public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic public import Mathlib.Tactic.Linarith public import HexInterval.Experiment.ProofEmitter +public import HexInterval.Experiment.GenericInstanceReconstruction public import HexInterval.Experiment.SineSign @[expose] public section @@ -25,6 +26,7 @@ negation propagator, and generic equality transport. namespace Hex.Interval.Experiment.SineSign open Propagator SemanticReplay ChronologicalReplay ProofEmitter +open GenericInstanceReconstruction /-! ## Real interpretation -/ @@ -213,6 +215,41 @@ def stable : StableStep semantics baseProgram extendedProgram := Contains fact.fact (newValue fact.node) rw [agreement] } +theorem nodeAtPrefix {before after : Program} + (stepPrefix : ProgramPrefix before after) (target : NodeId) + (instruction : Node) + (found : before.node? target = some instruction) : + after.node? target = some instruction := by + have within : target.index < before.nodes.size := by + by_contra outside + have notWithin : ¬target.index < before.nodes.size := by omega + simp [Program.node?, notWithin] at found + rw [Program.node?, stepPrefix.nodeAt target.index within] + exact found + +/-- Node-local real semantics is stable across every checked, fixed-operation +program prefix. This law is independent of the sine oddness instantiator and +can therefore drive generic reconstruction of repeated instance events. -/ +def stableLaw : StableLaw semantics := + { stable := by + intro before after _ _ stepPrefix _ + refine + { programPrefix := stepPrefix + modelsBefore := ?_ + holdsOld := ?_ } + · intro valuation model + change Models after valuation at model + change Models before valuation + exact + ⟨fun found => model.1 (nodeAtPrefix stepPrefix _ _ found), + fun found => model.2.1 (nodeAtPrefix stepPrefix _ _ found), + fun found => model.2.2.1 (nodeAtPrefix stepPrefix _ _ found), + fun found => model.2.2.2 (nodeAtPrefix stepPrefix _ _ found)⟩ + · intro oldValue newValue fact _ _ _ agreement + change Contains fact.fact (oldValue fact.node) ↔ + Contains fact.fact (newValue fact.node) + rw [agreement] } + theorem oddnessEntails : semantics.EntailsEq extendedProgram [] (node 2) (node 4) := by change ∀ valuation : NodeId -> ℝ, Models extendedProgram valuation -> diff --git a/conformance/HexIntervalMathlib/SineTacticConformance.lean b/conformance/HexIntervalMathlib/SineTacticConformance.lean index d072c6f56..2cd0512a7 100644 --- a/conformance/HexIntervalMathlib/SineTacticConformance.lean +++ b/conformance/HexIntervalMathlib/SineTacticConformance.lean @@ -45,6 +45,66 @@ private structure LiveTrace where program : Program events : List LiveEvent +/-! ## A second-instantiation canary -/ + +private def noopKey : RuleKey := + { name := "sine-sign.noop-instance" } + +private def noopAction : Action := + { serial := 4 + programVersion := 1 + application := { index := 5 } + rule := { index := 3 } + key := noopKey + node := node 4 + kind := .instantiate + effort := 0 + generation := 1 + inputs := [] + writes := [] } + +private def noopEvent : InstanceEvent := + { programVersion := 2 + origin := noopAction + family := 2 + substitution := [node 4] + products := [] + newNodes := [] + generation := 2 + equalities := [{ index := 0 }] + newEqualities := [] + payload := payload 9 } + +private def noopEntry : Entry := + { origin := noopAction + role := .instance + schema := 1 + body := [] } + +private def noopQuote : InstanceQuote := + { event := noopEvent + payload := payload 9 + entry := noopEntry } + +private def noopSchema : PackedInstanceSchema semantics where + rule := noopKey + schema := 1 + Certificate := Unit + decode := fun body => if body.isEmpty then some () else none + replay := fun _ _ context _ => + if same : context.before = context.after then + some + { proof := by + simpa only [same] using + (extendRefl semantics context.before).proof } + else + none + +private def noopEmit : EmitPackage Name := + { schemas := + [{ key := noopSchema.key + handle := ``noopSchema }] } + private def resolveFacts? (engine : Engine Range) (inputs : List SeenVersion) : Option (List (NodeFact Range)) := inputs.mapM fun input => do @@ -397,16 +457,26 @@ private def seedAssumed (program : Program) (base : List (NodeFact Range)) Evidence (semantics.Entails program base fact) := ProofEmitter.assumedAt program base index fact found +private theorem checkedProgram (program : Program) + (checked : program.check = true) : + program.check = true := + checked + /-- One kernel proof already available at an exact engine fact version. -/ private structure FactProof where seen : SeenVersion fact : Range + within : Expr proof : Expr -private def findProof? (known : List FactProof) (seen : SeenVersion) - (fact : Range) : Option Expr := do +private def findFact? (known : List FactProof) (seen : SeenVersion) + (fact : Range) : Option FactProof := do let item <- known.find? fun item => item.seen == seen - if item.fact == fact then some item.proof else none + if item.fact == fact then some item else none + +private def findProof? (known : List FactProof) (seen : SeenVersion) + (fact : Range) : Option Expr := + (findFact? known seen fact).map (fun item => item.proof) private def insertProof (known : List FactProof) (item : FactProof) : MetaM (List FactProof) := do @@ -435,28 +505,31 @@ private meta def soundInputs (program : Expr) (known : List FactProof) let proofs <- inputProofs program known seen facts mkAppM ``EntailsList.sound #[proofs] -private meta def emitInstance (program : Expr) (quote : InstanceQuote) - (table : SchemaTable Name) : MetaM Expr := do +private meta def emitInstance (version : Nat) (before after : Expr) + (basePrefix stepPrefix sameOperations : Expr) (quote : InstanceQuote) + (previous : Expr) (table : SchemaTable Name) : MetaM Expr := do let schema <- schemaName table "instantiation" quote.entry let result <- mkAppM ``ProofEmitter.replayInstance #[mkConst schema, mkConst ``checkerInput, - mkNatLit 0, - mkConst ``baseProgram, - program, - mkConst ``basePrefix, - mkConst ``programPrefix, - mkConst ``sameOperations, + mkNatLit version, + before, + after, + basePrefix, + stepPrefix, + sameOperations, ← instanceQuoteExpr quote, - mkConst ``initialExtension] + previous] getReplay result -/-- Derive the initial table from the caller assumptions and the exact fresh -node suffix. No proof constant names a particular function or event. -/ -private meta def seedProofs (programValue : Program) (program : Expr) - (newNodes : List NodeId) : MetaM (List FactProof) := do +/-- Derive caller-owned version-zero facts at the current program prefix. -/ +private meta def seedBase (program : Expr) (basePrefix : Expr) : + MetaM (List FactProof) := do let mut known := [] + let baseWithinProgram <- + mkAppM ``ProofEmitter.liftFacts + #[basePrefix, mkConst ``baseWithin] for (fact, index) in baseFacts.zipIdx do let factTerm <- nodeFactExpr fact let someFact <- mkAppM ``Option.some #[factTerm] @@ -464,10 +537,22 @@ private meta def seedProofs (programValue : Program) (program : Expr) let proof <- mkAppM ``seedAssumed #[program, mkConst ``baseFacts, mkNatLit index, factTerm, found] + let within <- + mkAppM ``ProofEmitter.factWithinAt + #[program, mkConst ``baseFacts, baseWithinProgram, + mkNatLit index, factTerm, found] known <- insertProof known { seen := { node := fact.node, version := 0 } fact := fact.fact + within proof } + pure known + +/-- Add domain-top proofs for exactly one instantiation's fresh node suffix. -/ +private meta def seedNew (programValue : Program) (program : Expr) + (newNodes : List NodeId) (known : List FactProof) : + MetaM (List FactProof) := do + let mut known := known for node in newNodes do let some instruction := programValue.node? node | throwError "interval_sine: fresh node is absent from the final program" @@ -479,17 +564,96 @@ private meta def seedProofs (programValue : Program) (program : Expr) mkAppM ``ProofEmitter.topFact #[mkConst ``rangeSchema, program, mkConst ``baseFacts, nodeTerm, instructionTerm, found] + let within <- + mkAppM ``ProofEmitter.nodeWithin + #[program, nodeTerm, instructionTerm, found] known <- insertProof known { seen := { node, version := 0 } fact := rangeSchema.top instruction.domain + within proof } pure known -private meta def emitRule (program : Expr) (table : SchemaTable Name) - (known : List FactProof) (step : RuleStep Range) : MetaM (List FactProof) := do +/-- Dependent proof state carried through the quoted chronology. `Expr` +fields are indexed by `program` in the kernel even though the elaborator keeps +their relationships dynamically. -/ +private structure EmitState where + version : Nat + programValue : Program + program : Expr + snapshot : Expr + basePrefix : Expr + baseWithin : Expr + extension : Expr + known : List FactProof + +private meta def initialSnapshot (finalProgram : Expr) : MetaM Expr := do + let checked <- mkAppM ``Eq.refl #[mkConst ``Bool.true] + let finalChecked <- mkAppM ``checkedProgram #[finalProgram, checked] + let baseChecked <- + mkAppM ``checkedProgram #[mkConst ``baseProgram, checked] + mkAppM ``GenericInstanceReconstruction.Snapshot.mk + #[finalChecked, baseChecked, mkConst ``programPrefix, + mkConst ``sameOperations] + +private meta def liftKnown (stable stepPrefix baseWithin : Expr) + (known : List FactProof) : MetaM (List FactProof) := + known.mapM fun item => do + let proof <- + mkAppM ``ProofEmitter.liftFact + #[stable, baseWithin, item.proof, item.within] + let within <- + mkAppM ``ProofEmitter.liftNode #[stepPrefix, item.within] + pure { item with within, proof } + +private meta def emitInstantiation (finalValue : Program) (finalProgram : Expr) + (table : SchemaTable Name) (state : EmitState) (quote : InstanceQuote) : + MetaM EmitState := do + let event <- instanceEventExpr quote.event + let reconstruction <- + mkAppM ``GenericInstanceReconstruction.reconstruct? + #[mkConst ``stableLaw, finalProgram, state.program, state.snapshot, event] + let step <- getReplay reconstruction + let after <- + mkAppM ``GenericInstanceReconstruction.Step.after #[step] + let stepPrefix <- + mkAppM ``GenericInstanceReconstruction.Step.stepPrefix #[step] + let stable <- + mkAppM ``GenericInstanceReconstruction.Step.stable #[step] + let sameOperations <- + mkAppM ``GenericInstanceReconstruction.Step.sameOperations #[step] + let nextSnapshot <- + mkAppM ``GenericInstanceReconstruction.Step.next #[step] + let extension <- + emitInstance state.version state.program after state.basePrefix stepPrefix + sameOperations quote state.extension table + let known <- liftKnown stable stepPrefix state.baseWithin state.known + let baseWithin <- + mkAppM ``ProofEmitter.liftFacts #[stepPrefix, state.baseWithin] + let basePrefix <- + mkAppM ``ChronologicalReplay.prefixTrans #[state.basePrefix, stepPrefix] + let nextSize := state.programValue.nodes.size + quote.event.newNodes.length + let afterValue := + GenericInstanceReconstruction.programPrefix finalValue nextSize + let known <- seedNew afterValue after quote.event.newNodes known + pure + { version := quote.event.programVersion + programValue := afterValue + program := after + snapshot := nextSnapshot + basePrefix + baseWithin + extension + known } + +private meta def emitRule (program : Expr) (version : Nat) + (table : SchemaTable Name) (known : List FactProof) (step : RuleStep Range) : + MetaM (List FactProof) := do + unless step.event.programVersion == version do + throwError "interval_sine: rule event has the wrong program version" let .rule action _ _ := step.event.cause | throwError "interval_sine: rule quote has a transport cause" - let some previous := findProof? known step.event.previous step.previous + let some previous := findFact? known step.event.previous step.previous | throwError "interval_sine: rule previous fact has not been proved" let inputs <- soundInputs program known action.inputs step.assumptions let schema <- schemaName table "fact rule" step.entry @@ -502,20 +666,24 @@ private meta def emitRule (program : Expr) (table : SchemaTable Name) mkConst ``programPrefix, mkConst ``baseFacts, ← ruleStepExpr step, - previous, + previous.proof, inputs] let proof <- getReplay result insertProof known { seen := { node := step.event.node, version := step.event.version } fact := step.event.fact + within := previous.within proof } -private meta def emitTransport (program : Expr) (table : SchemaTable Name) - (known : List FactProof) (step : TransportStep Range) : +private meta def emitTransport (program : Expr) (version : Nat) + (table : SchemaTable Name) (known : List FactProof) + (step : TransportStep Range) : MetaM (List FactProof) := do + unless step.event.programVersion == version do + throwError "interval_sine: transport event has the wrong program version" let .transport _ source := step.event.cause | throwError "interval_sine: transport quote has a rule cause" - let some previous := findProof? known step.event.previous step.previous + let some previous := findFact? known step.event.previous step.previous | throwError "interval_sine: transport previous fact has not been proved" let some sourceProof := findProof? known source step.sourceFact | throwError "interval_sine: equality source fact has not been proved" @@ -527,46 +695,68 @@ private meta def emitTransport (program : Expr) (table : SchemaTable Name) mkConst ``rangeSchema, mkConst ``laws, mkConst ``checkerInput, - mkNatLit step.event.programVersion, + mkNatLit version, program, mkConst ``programPrefix, mkConst ``baseFacts, ← transportStepExpr step, - previous, + previous.proof, sourceProof, inputs] let proof <- getReplay result insertProof known { seen := { node := step.event.node, version := step.event.version } fact := step.event.fact + within := previous.within proof } -private meta def emitFacts (program : Expr) (table : SchemaTable Name) : - List LiveEvent -> List FactProof -> MetaM (List FactProof) - | [], known => pure known - | .rule step :: rest, known => do - emitFacts program table rest (← emitRule program table known step) - | .transport step :: rest, known => do - emitFacts program table rest (← emitTransport program table known step) - | .instantiation _ :: _, _ => - throwError "interval_sine: multiple instantiations are not supported yet" +private meta def emitEvents (finalValue : Program) (finalProgram : Expr) + (table : SchemaTable Name) : + List LiveEvent -> EmitState -> MetaM EmitState + | [], state => pure state + | .instantiation quote :: rest, state => do + let state <- + emitInstantiation finalValue finalProgram table state quote + emitEvents finalValue finalProgram table rest state + | .rule step :: rest, state => do + let known <- + emitRule state.program state.version table state.known step + emitEvents finalValue finalProgram table rest { state with known } + | .transport step :: rest, state => do + let known <- + emitTransport state.program state.version table state.known step + emitEvents finalValue finalProgram table rest { state with known } /-- Emit a proof by folding arbitrary fact events through an exact -`(node, version)` evidence table. The event fold does not name any function -or propagator; packages are selected only through their replay addresses. -/ +`(node, version)` evidence table and reconstructed program state. The event +fold does not name any function or propagator; packages are selected only +through their replay addresses. -/ private meta def emitTrace (programValue : Program) (events : List LiveEvent) (table : SchemaTable Name) : MetaM Expr := do - let .instantiation quote :: rest := events - | throwError "interval_sine: trace does not start with an instantiation" - let program <- programExpr programValue - let extension <- emitInstance program quote table - let initial <- seedProofs programValue program quote.event.newNodes - let known <- emitFacts program table rest initial + unless programValue.check do + throwError "interval_sine: final expression program is not checked" + let finalProgram <- programExpr programValue + let snapshot <- initialSnapshot finalProgram + let baseProgram := mkConst ``baseProgram + let basePrefix := mkConst ``basePrefix + let known <- seedBase baseProgram basePrefix + let initial : EmitState := + { version := 0 + programValue := SineSign.baseProgram + program := baseProgram + snapshot + basePrefix + baseWithin := mkConst ``baseWithin + extension := mkConst ``initialExtension + known } + let state <- emitEvents programValue finalProgram table events initial + unless state.programValue == programValue do + throwError "interval_sine: trace did not consume the complete final program" let target := { node := node 2, version := 1 : SeenVersion } - let some final := findProof? known target .nonpositive + let some final := findProof? state.known target .nonpositive | throwError "interval_sine: trace did not prove the requested target" - mkAppM ``closeEvidence #[extension, final] + mkAppM ``closeEvidence #[state.extension, final] private meta def emitQuote (quote : LiveQuotes) (table : SchemaTable Name) : MetaM Expr := @@ -642,11 +832,36 @@ example : True := by checkQuoteData quote let some table := emitTable? | throwError "interval_sine test: duplicate proof-schema address" + let some repeatTable := + SchemaTable.build [negationEmit, sineEmit, noopEmit] + | throwError "interval_sine test: repeated-instance schema table failed" + let lateTransport : TransportStep Range := + { quote.transport with + event := { quote.transport.event with programVersion := 2 } } + let _ <- emitTrace extendedProgram + [ .instantiation quote.instantiation, .rule quote.sine, + .rule quote.negation, .instantiation noopQuote, + .transport lateTransport ] repeatTable + let oversizedNoop : InstanceQuote := + { noopQuote with + event := { noopQuote.event with newNodes := [node 4] } } + if (← observing? (emitTrace extendedProgram + [ .instantiation quote.instantiation, .rule quote.sine, + .rule quote.negation, .instantiation oversizedNoop, + .transport lateTransport ] repeatTable)).isSome then + throwError "interval_sine test: oversized repeated instantiation was accepted" let reordered : List LiveEvent := [ .instantiation quote.instantiation, .rule quote.negation, .rule quote.sine, .transport quote.transport ] if (← observing? (emitTrace extendedProgram reordered table)).isSome then throwError "interval_sine test: future fact was accepted as a dependency" + let wrongVersion : TransportStep Range := + { quote.transport with + event := { quote.transport.event with programVersion := 2 } } + if (← observing? (emitTrace extendedProgram + [ .instantiation quote.instantiation, .rule quote.sine, + .rule quote.negation, .transport wrongVersion ] table)).isSome then + throwError "interval_sine test: stale transport program version was accepted" if (← observing? (emitTrace baseProgram [ .instantiation quote.instantiation, .rule quote.sine, .rule quote.negation, .transport quote.transport ] table)).isSome then diff --git a/progress/20260811T112551Z.md b/progress/20260811T112551Z.md new file mode 100644 index 000000000..f3755d4a3 --- /dev/null +++ b/progress/20260811T112551Z.md @@ -0,0 +1,40 @@ +# Accomplished + +- Proved a semantics-wide `StableLaw` for the real-function adapter: every + checked fixed-operation program prefix preserves old models and facts. +- Generalized the direct emitter state to carry the current program, version, + caller prefix, conservative-extension theorem, base-fact bounds, exact fact + proofs, and reconstruction snapshot. +- Integrated transparent `GenericInstanceReconstruction.reconstruct?` at every + quoted instance event. Existing fact evidence is lifted through stability, + and only the event's exact fresh-node suffix receives top evidence. +- Added generic fact/node bound helpers so dependent proof-table entries remain + well typed across repeated program extensions. +- Added a second zero-node instantiation fixture after the sine and negation + rules. Its successful proof emission demonstrates that the negation fact is + preserved across another version transition and consumed by later equality + transport. +- Added rejection tests for wrong fact-event versions, an oversized repeated + instance, missing generated nodes, and future dependencies. +- Inspected the emitted theorem term: it contains transparent generic + reconstruction and contains none of the named sine previous-fact constants. +- Updated the SPEC and passed the focused 1,957-target build, diff check, and + banned-proof audit. + +# Current frontier + +The event fold now handles rule, transport, ordinary node-appending instance, +and zero-node/repeated instance events without function cases. The remaining +canary-specific seams are construction of the caller graph and semantic bridge, +selection of the final target fact/version, and package-registry ownership. + +# Next step + +Derive the base program and target from an arbitrary tactic goal, then move the +generic quotation/emission state out of the sine conformance fixture into a +reusable frontend module. + +# Blockers + +None. The stacked branch must be reconciled with the newly repaired #9204 and +#9205 heads before its PR is opened. From 21d44e12b0b49f73384c3a6b0bf675fcc79457dd Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 11 Aug 2026 19:21:22 +0000 Subject: [PATCH 2/2] Repair repeated-instance prefix replay; progress 20260811T191915Z --- .../SineTacticConformance.lean | 25 ++++++++----------- progress/20260811T191915Z.md | 25 +++++++++++++++++++ 2 files changed, 36 insertions(+), 14 deletions(-) create mode 100644 progress/20260811T191915Z.md diff --git a/conformance/HexIntervalMathlib/SineTacticConformance.lean b/conformance/HexIntervalMathlib/SineTacticConformance.lean index 1e14e463b..3627e99ad 100644 --- a/conformance/HexIntervalMathlib/SineTacticConformance.lean +++ b/conformance/HexIntervalMathlib/SineTacticConformance.lean @@ -645,7 +645,8 @@ private meta def emitInstantiation (finalValue : Program) (finalProgram : Expr) baseWithin extension known } -private meta def emitRule (program : Expr) (version : Nat) + +private meta def emitRule (program basePrefix : Expr) (version : Nat) (table : SchemaTable Name) (known : List FactProof) (step : RuleStep Range) : MetaM (List FactProof) := do unless step.event.programVersion == version do @@ -662,7 +663,7 @@ private meta def emitRule (program : Expr) (version : Nat) mkConst ``rangeSchema, mkConst ``checkerInput, program, - mkConst ``programPrefix, + basePrefix, mkConst ``baseFacts, ← ruleStepExpr step, previous.proof, @@ -674,7 +675,7 @@ private meta def emitRule (program : Expr) (version : Nat) within := previous.within proof } -private meta def emitTransport (program : Expr) (version : Nat) +private meta def emitTransport (program basePrefix : Expr) (version : Nat) (table : SchemaTable Name) (known : List FactProof) (step : TransportStep Range) : MetaM (List FactProof) := do @@ -696,7 +697,7 @@ private meta def emitTransport (program : Expr) (version : Nat) mkConst ``checkerInput, mkNatLit version, program, - mkConst ``programPrefix, + basePrefix, mkConst ``baseFacts, ← transportStepExpr step, previous.proof, @@ -719,11 +720,11 @@ private meta def emitEvents (finalValue : Program) (finalProgram : Expr) emitEvents finalValue finalProgram table rest state | .rule step :: rest, state => do let known <- - emitRule state.program state.version table state.known step + emitRule state.program state.basePrefix state.version table state.known step emitEvents finalValue finalProgram table rest { state with known } | .transport step :: rest, state => do let known <- - emitTransport state.program state.version table state.known step + emitTransport state.program state.basePrefix state.version table state.known step emitEvents finalValue finalProgram table rest { state with known } /-- Emit a proof by folding arbitrary fact events through an exact @@ -880,14 +881,10 @@ example : True := by if (← observing? (emitTrace baseProgram [ .instantiation quote.instantiation, .rule quote.sine, .rule quote.negation, .transport quote.transport ] table)).isSome then - throwError "interval_sine test: absent generated nodes were accepted" - let wrongVersion : TransportStep Range := - { quote.transport with - event := { quote.transport.event with programVersion := 2 } } - if (← observing? (emitTrace extendedProgram - [ .instantiation quote.instantiation, .rule quote.sine, - .rule quote.negation, .transport wrongVersion ] table)).isSome then - throwError "interval_sine test: stale transport program version was accepted" + throwError "interval_sine test: emission against the wrong final program was accepted" + if (← observing? + (seedNew baseProgram (mkConst ``baseProgram) [node 3] [])).isSome then + throwError "interval_sine test: absent generated node received a top proof" if (← observing? (checkQuoteData malformed)).isSome then throwError "interval_sine test: malformed quote was accepted" if (← observing? (emitQuote malformed table)).isSome then diff --git a/progress/20260811T191915Z.md b/progress/20260811T191915Z.md new file mode 100644 index 000000000..c233a9ace --- /dev/null +++ b/progress/20260811T191915Z.md @@ -0,0 +1,25 @@ +# Accomplished + +- Repaired repeated-instantiation proof emission after a fresh independent + review: rule and equality-transport replay now consume the exact base prefix + carried by the dependent emitter state instead of the fixed final-program + prefix. +- Removed a duplicated stale-transport mutation and separated the wrong-final- + program rejection from a direct generated-node seeding rejection. +- Preserved the generic zero-node repeated-instantiation canary and the + ordinary kernel-checked sine theorem. + +# Current frontier + +The direct fold now threads the reconstructed prefix through instance, rule, +and transport replay. Final closure remains deliberately specialized to the +fixed sine target; later frontend layers remove that canary-specific seam. + +# Next step + +Finish the focused build and exact-head review, then propagate this repair +through the stacked package-registry and generic-frontend branches. + +# Blockers + +None.