From bd8b208a231a18a2d472717797e5d69141003ff0 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 11 Aug 2026 17:17:59 +0000 Subject: [PATCH] Propagate provenance honesty through generic frontend; progress 20260811T171522Z --- HexInterval/Experiment/Frontend.lean | 118 +++++ HexInterval/Experiment/ProofFrontend.lean | 369 +++++++++++++++ HexInterval/SPEC/hex-interval.md | 64 +-- .../SineTacticConformance.lean | 426 +++--------------- lakefile.lean | 2 + progress/20260811T115319Z.md | 31 ++ progress/20260811T121548Z.md | 25 + progress/20260811T161652Z.md | 27 ++ progress/20260811T163700Z.md | 22 + .../bench/proof_only_runtime_exemptions.json | 6 + 10 files changed, 686 insertions(+), 404 deletions(-) create mode 100644 HexInterval/Experiment/Frontend.lean create mode 100644 HexInterval/Experiment/ProofFrontend.lean create mode 100644 progress/20260811T115319Z.md create mode 100644 progress/20260811T121548Z.md create mode 100644 progress/20260811T161652Z.md create mode 100644 progress/20260811T163700Z.md diff --git a/HexInterval/Experiment/Frontend.lean b/HexInterval/Experiment/Frontend.lean new file mode 100644 index 000000000..edd6e1308 --- /dev/null +++ b/HexInterval/Experiment/Frontend.lean @@ -0,0 +1,118 @@ +/- +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.ProofRegistry + +@[expose] public section + +/-! +# Function-independent tactic frontend data + +The compiled engine retains fact and instantiation records in separate arrays +and one compact chronology describing their interleaving. This module quotes +that state into the three proof-producing event shapes understood by +`ProofEmitter`. It is parameterized only by the fact type: no operation or +mathematical function is enumerated here. + +Quotation checks exact role-local ordering and complete consumption. The +subsequent proof fold remains responsible for causal availability of facts, +equalities, and program versions; quoted values are plain data, not evidence. +-/ + +namespace Hex.Interval.Experiment.Frontend + +open Propagator PayloadArena SemanticReplay ProofEmitter + +/-- Proof-producing events in their authoritative cross-history order. -/ +inductive Event (Fact : Type) where + | instantiation (quote : InstanceQuote) + | rule (step : RuleStep Fact) + | transport (step : TransportStep Fact) + +/-- A final expression program and its completely quoted proof chronology. -/ +structure Trace (Fact : Type) where + program : Program + events : List (Event Fact) + +/-- Resolve the fact values named by one frozen action from retained history. +This is quotation only; the proof fold must find evidence for the same versions +in its already-established prefix. -/ +def resolveFacts? (engine : Engine Fact) (inputs : List SeenVersion) : + Option (List (NodeFact Fact)) := + inputs.mapM fun input => do + let fact ← engine.factAt? input + pure { node := input.node, fact } + +/-- Quote one rule-produced fact record and its immutable payload entry. -/ +def ruleStep? (engine : Engine Fact) (arena : Arena) + (event : FactEvent Fact) : Option (RuleStep Fact) := do + let .rule action _ payload := event.cause | none + let entry ← arena.entry? payload .fact + let assumptions ← resolveFacts? engine action.inputs + let previous ← engine.factAt? event.previous + pure { event, payload, entry, assumptions, previous } + +/-- Quote one equality-transport fact record, retained edge, and payload. -/ +def transportStep? (engine : Engine Fact) (arena : Arena) + (event : FactEvent Fact) : Option (TransportStep Fact) := do + let .transport equality source := event.cause | none + let edge ← engine.equalities[equality.index]? + let entry ← arena.entry? edge.payload .equality + let assumptions ← resolveFacts? engine edge.origin.inputs + let previous ← engine.factAt? event.previous + let sourceFact ← engine.factAt? source + pure + { event + equality + edge + payload := edge.payload + entry + assumptions + previous + sourceFact } + +/-- Quote a complete compact chronology. + +Indices in each role must be gap-free and increasing, and the final counters +must exhaust both detailed histories. Cross-role causal checks deliberately +belong to the dependent proof fold, which has the evidence and program state +needed to validate them. -/ +def quote? (engine : Engine Fact) (arena : Arena) : + List HistoryEvent → Nat → Nat → Option (List (Event Fact)) + | [], nextFact, nextInstance => + if nextFact == engine.history.size && + nextInstance == engine.instanceHistory.size then + some [] + else + none + | .instance index :: rest, nextFact, nextInstance => do + if index != nextInstance then none else pure () + let event ← engine.instanceHistory[index]? + let entry ← arena.entry? event.payload .instance + let tail ← quote? engine arena rest nextFact (nextInstance + 1) + pure + (.instantiation + { event + payload := event.payload + entry } :: tail) + | .fact index :: rest, nextFact, nextInstance => do + if index != nextFact then none else pure () + let event ← engine.history[index]? + let head ← + match event.cause with + | .rule _ _ _ => (ruleStep? engine arena event).map .rule + | .transport _ _ => (transportStep? engine arena event).map .transport + let tail ← quote? engine arena rest (nextFact + 1) nextInstance + pure (head :: tail) + +/-- Quote the engine's retained chronology and final program. -/ +def trace? (engine : Engine Fact) (arena : Arena) : Option (Trace Fact) := do + let events ← quote? engine arena engine.chronology.toList 0 0 + pure { program := engine.program, events } + +end Hex.Interval.Experiment.Frontend diff --git a/HexInterval/Experiment/ProofFrontend.lean b/HexInterval/Experiment/ProofFrontend.lean new file mode 100644 index 000000000..daa4246aa --- /dev/null +++ b/HexInterval/Experiment/ProofFrontend.lean @@ -0,0 +1,369 @@ +/- +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 Lean +public import HexInterval.Experiment.Frontend +public import HexInterval.Experiment.GenericInstanceReconstruction + +@[expose] public section + +/-! +# Generic direct-proof frontend + +This module folds an arbitrary quoted interval chronology into an ordinary +Lean proof term. It carries the current expression program, independently +checked program version, conservative-extension evidence, and an exact table +of proofs indexed by `(node, version)`. + +The fold has no operation or mathematical-function cases. A semantics adapter +supplies its domain laws and prefix-stability theorem, while each propagator +package is selected through the joint proof registry. A small encoder turns +plain runtime data into Lean expressions; those expressions remain untrusted +until the emitted replay applications typecheck. +-/ + +namespace Hex.Interval.Experiment.ProofFrontend + +open Lean Meta +open Propagator PayloadArena SemanticReplay ChronologicalReplay ProofEmitter +open GenericInstanceReconstruction ProofRegistry Frontend + +/-- Reification boundary for a frontend's concrete fact representation. +Structural trace data may use a shared encoder; only fact-bearing values vary +between interval domains. -/ +structure Encoder (Fact : Type) where + program : Program → MetaM Expr + nodeId : NodeId → MetaM Expr + node : Node → MetaM Expr + fact : Fact → MetaM Expr + nodeFact : NodeFact Fact → MetaM Expr + instanceQuote : InstanceQuote → MetaM Expr + ruleStep : RuleStep Fact → MetaM Expr + transportStep : TransportStep Fact → MetaM Expr + +/-- Kernel constants and runtime values needed by the generic fold. + +Every `Expr` field is checked again at its use site. In particular, +`finalPrefix` and `sameOperations` must have types referring to the reified +final program; a caller cannot attach them to a different expression graph. -/ +structure Context (Fact Handle : Type) where + encoder : Encoder Fact + resolveSchema : Handle → MetaM Name + semantics : Expr + domain : Expr + laws : Expr + stableLaw : Expr + input : Expr + assumed : Name + baseFacts : List (NodeFact Fact) + baseFactsTerm : Expr + baseProgram : Program + baseProgramTerm : Expr + basePrefix : Expr + baseWithin : Expr + initialExtension : Expr + finalPrefix : Expr + sameOperations : Expr + top : DomainId → Fact + +/-- One kernel proof already available at an exact engine fact version. -/ +structure FactProof (Fact : Type) where + seen : SeenVersion + fact : Fact + within : Expr + proof : Expr + +/-- Dependent proof state carried through the quoted chronology. -/ +structure State (Fact : Type) where + version : Nat + programValue : Program + program : Expr + snapshot : Expr + basePrefix : Expr + baseWithin : Expr + extension : Expr + known : List (FactProof Fact) + +/-- Preserve an already checked program proposition while giving the emitter a +stable declaration to apply to reified programs. -/ +theorem keepCheck (program : Program) (checked : program.check = true) : + program.check = true := + checked + +/-- Project an accepted transparent replay result. The supplied equality is +ordinary kernel reduction. -/ +def replayGet {α : Type} (result : Option α) (success : result.isSome = true) : α := + result.get success + +/-- Resolve one exact package-owned schema handle to a declaration. -/ +def schemaName (context : Context Fact Handle) (table : SchemaTable Handle) + (label : String) (entry : Entry) : MetaM Name := do + let some handle := table.find? entry.replayKey + | throwError "interval frontend: no proof schema for {label}" + let declaration ← context.resolveSchema handle + discard <| getConstInfo declaration + pure declaration + +/-- Find one previously established fact without substituting a newer value. -/ +def findFact? [BEq Fact] (known : List (FactProof Fact)) (seen : SeenVersion) + (fact : Fact) : Option (FactProof Fact) := do + let item ← known.find? fun item => item.seen == seen + if item.fact == fact then some item else none + +/-- Find the proof term for one exact fact version. -/ +def findProof? [BEq Fact] (known : List (FactProof Fact)) + (seen : SeenVersion) (fact : Fact) : Option Expr := + (findFact? known seen fact).map (fun item => item.proof) + +/-- Insert a newly proved version, rejecting duplicate provenance. -/ +def insertProof (known : List (FactProof Fact)) (item : FactProof Fact) : + MetaM (List (FactProof Fact)) := do + if known.any fun old => old.seen == item.seen then + throwError "interval frontend: duplicate proof for a fact version" + pure (item :: known) + +/-- Assemble dependency evidence in the action's exact input order. -/ +def inputProofs [BEq Fact] (context : Context Fact Handle) (program : Expr) + (known : List (FactProof Fact)) : + List SeenVersion → List (NodeFact Fact) → MetaM Expr + | [], [] => + mkAppM ``EntailsList.empty + #[context.semantics, program, context.baseFactsTerm] + | seen :: seenTail, fact :: factTail => do + unless seen.node == fact.node do + throwError "interval frontend: input node does not match resolved fact" + let some head := findProof? known seen fact.fact + | throwError "interval frontend: input fact has not been proved yet" + let tail ← inputProofs context program known seenTail factTail + mkAppM ``EntailsList.cons #[head, tail] + | _, _ => + throwError "interval frontend: input versions and facts differ in length" + +/-- Package ordered dependency terms as the proposition consumed by replay. -/ +def soundInputs [BEq Fact] (context : Context Fact Handle) (program : Expr) + (known : List (FactProof Fact)) (seen : List SeenVersion) + (facts : List (NodeFact Fact)) : MetaM Expr := do + let proofs ← inputProofs context program known seen facts + mkAppM ``EntailsList.sound #[proofs] + +def replayResult (result : Expr) : MetaM Expr := do + let success ← mkAppM ``Eq.refl #[mkConst ``Bool.true] + mkAppM ``replayGet #[result, success] + +/-- Seed caller-owned version-zero facts by exact positions in the base list. -/ +def seedBase (context : Context Fact Handle) (program : Expr) (basePrefix : Expr) : + MetaM (List (FactProof Fact)) := do + let mut known := [] + let baseWithinProgram ← + mkAppM ``ProofEmitter.liftFacts #[basePrefix, context.baseWithin] + for (fact, index) in context.baseFacts.zipIdx do + let factTerm ← context.encoder.nodeFact fact + let someFact ← mkAppM ``Option.some #[factTerm] + let found ← mkAppM ``Eq.refl #[someFact] + let proof ← + mkAppM context.assumed + #[program, context.baseFactsTerm, mkNatLit index, factTerm, found] + let within ← + mkAppM ``ProofEmitter.factWithinAt + #[program, context.baseFactsTerm, baseWithinProgram, + mkNatLit index, factTerm, found] + known ← insertProof known + { seen := { node := fact.node, version := 0 } + fact := fact.fact + within + proof } + pure known + +/-- Seed domain-top evidence for exactly one instance's fresh-node suffix. -/ +def seedNew [BEq Fact] (context : Context Fact Handle) (programValue : Program) + (program : Expr) (newNodes : List NodeId) (known : List (FactProof Fact)) : + MetaM (List (FactProof Fact)) := do + let mut known := known + for node in newNodes do + let some instruction := programValue.node? node + | throwError "interval frontend: fresh node is absent from the program" + let nodeTerm ← context.encoder.nodeId node + let instructionTerm ← context.encoder.node instruction + let factValue := context.top instruction.domain + let someInstruction ← mkAppM ``Option.some #[instructionTerm] + let found ← mkAppM ``Eq.refl #[someInstruction] + let proof ← + mkAppM ``ProofEmitter.topFact + #[context.domain, program, context.baseFactsTerm, + nodeTerm, instructionTerm, found] + let within ← + mkAppM ``ProofEmitter.nodeWithin + #[program, nodeTerm, instructionTerm, found] + known ← insertProof known + { seen := { node, version := 0 } + fact := factValue + within + proof } + pure known + +/-- Lift every established fact across one stable program extension. -/ +def liftKnown (stable stepPrefix baseWithin : Expr) + (known : List (FactProof Fact)) : MetaM (List (FactProof Fact)) := + 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 } + +/-- Construct the initial generic reconstruction snapshot. -/ +def initialSnapshot (context : Context Fact Handle) (finalProgram : Expr) : MetaM Expr := do + let checked ← mkAppM ``Eq.refl #[mkConst ``Bool.true] + let finalChecked ← mkAppM ``keepCheck #[finalProgram, checked] + let baseChecked ← mkAppM ``keepCheck #[context.baseProgramTerm, checked] + mkAppM ``GenericInstanceReconstruction.Snapshot.mk + #[finalChecked, baseChecked, context.finalPrefix, context.sameOperations] + +/-- Replay one arbitrary package-owned instantiation. -/ +def emitInstance (context : Context Fact Handle) (version : Nat) + (before after : Expr) (basePrefix stepPrefix sameOperations : Expr) + (quote : InstanceQuote) (quoteTerm : Expr) (previous : Expr) + (table : SchemaTable Handle) : MetaM Expr := do + let schema ← schemaName context table "instantiation" quote.entry + let result ← + mkAppM ``ProofEmitter.replayInstance + #[mkConst schema, context.input, mkNatLit version, before, after, + basePrefix, stepPrefix, sameOperations, quoteTerm, previous] + replayResult result + +/-- Replay and install one instantiation event. -/ +def emitInstantiation [BEq Fact] (context : Context Fact Handle) + (finalValue : Program) (finalProgram : Expr) (table : SchemaTable Handle) + (state : State Fact) (quote : InstanceQuote) : MetaM (State Fact) := do + let eventTerm ← context.encoder.instanceQuote quote + let reconstruction ← + mkAppM ``GenericInstanceReconstruction.reconstruct? + #[context.stableLaw, finalProgram, state.program, state.snapshot, + ← mkAppM ``InstanceQuote.event #[eventTerm]] + let step ← replayResult 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 context state.version state.program after state.basePrefix + stepPrefix sameOperations quote eventTerm 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 context afterValue after quote.event.newNodes known + pure + { version := quote.event.programVersion + programValue := afterValue + program := after + snapshot := nextSnapshot + basePrefix + baseWithin + extension + known } + +/-- Replay one arbitrary fact propagator. -/ +def emitRule [BEq Fact] (context : Context Fact Handle) (state : State Fact) + (table : SchemaTable Handle) (step : RuleStep Fact) : MetaM (State Fact) := do + unless step.event.programVersion == state.version do + throwError "interval frontend: rule event has the wrong program version" + let .rule action _ _ := step.event.cause + | throwError "interval frontend: rule quote has a transport cause" + let some previous := findFact? state.known step.event.previous step.previous + | throwError "interval frontend: rule previous fact has not been proved" + let inputs ← soundInputs context state.program state.known + action.inputs step.assumptions + let schema ← schemaName context table "fact rule" step.entry + let stepTerm ← context.encoder.ruleStep step + let result ← + mkAppM ``ProofEmitter.replayRule + #[mkConst schema, context.domain, context.input, state.program, + state.basePrefix, context.baseFactsTerm, stepTerm, previous.proof, inputs] + let proof ← replayResult result + let known ← insertProof state.known + { seen := { node := step.event.node, version := step.event.version } + fact := step.event.fact + within := previous.within + proof } + pure { state with known } + +/-- Replay one generic equality transport. -/ +def emitTransport [BEq Fact] (context : Context Fact Handle) (state : State Fact) + (table : SchemaTable Handle) (step : TransportStep Fact) : + MetaM (State Fact) := do + unless step.event.programVersion == state.version do + throwError "interval frontend: transport event has the wrong program version" + let .transport _ source := step.event.cause + | throwError "interval frontend: transport quote has a rule cause" + let some previous := findFact? state.known step.event.previous step.previous + | throwError "interval frontend: transport previous fact is unavailable" + let some sourceProof := findProof? state.known source step.sourceFact + | throwError "interval frontend: equality source fact is unavailable" + let inputs ← soundInputs context state.program state.known + step.edge.origin.inputs step.assumptions + let schema ← schemaName context table "equality transport" step.entry + let stepTerm ← context.encoder.transportStep step + let result ← + mkAppM ``ProofEmitter.replayTransport + #[mkConst schema, context.domain, context.laws, context.input, + mkNatLit state.version, state.program, state.basePrefix, + context.baseFactsTerm, stepTerm, previous.proof, sourceProof, inputs] + let proof ← replayResult result + let known ← insertProof state.known + { seen := { node := step.event.node, version := step.event.version } + fact := step.event.fact + within := previous.within + proof } + pure { state with known } + +/-- Fold arbitrary proof events in their supplied chronology. -/ +def emitEvents [BEq Fact] (context : Context Fact Handle) (finalValue : Program) + (finalProgram : Expr) (table : SchemaTable Handle) : + List (Frontend.Event Fact) → State Fact → MetaM (State Fact) + | [], state => pure state + | .instantiation quote :: rest, state => do + let state ← emitInstantiation context finalValue finalProgram table state quote + emitEvents context finalValue finalProgram table rest state + | .rule step :: rest, state => do + let state ← emitRule context state table step + emitEvents context finalValue finalProgram table rest state + | .transport step :: rest, state => do + let state ← emitTransport context state table step + emitEvents context finalValue finalProgram table rest state + +/-- Emit the complete generic state for one final program and chronology. -/ +def emitTrace [BEq Fact] (context : Context Fact Handle) (programValue : Program) + (events : List (Frontend.Event Fact)) (table : SchemaTable Handle) : + MetaM (State Fact) := do + unless programValue.check do + throwError "interval frontend: final expression program is not checked" + let finalProgram ← context.encoder.program programValue + let snapshot ← initialSnapshot context finalProgram + let known ← seedBase context context.baseProgramTerm context.basePrefix + let initial : State Fact := + { version := 0 + programValue := context.baseProgram + program := context.baseProgramTerm + snapshot + basePrefix := context.basePrefix + baseWithin := context.baseWithin + extension := context.initialExtension + known } + let state ← emitEvents context programValue finalProgram table events initial + unless state.programValue == programValue do + throwError "interval frontend: trace did not consume the complete final program" + pure state + +end Hex.Interval.Experiment.ProofFrontend diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index 6fb0733a7..6f48bb912 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -1315,37 +1315,44 @@ if the quote or schema is wrong, elaboration fails. The assigned term consumes the actual returned quote and reified final program. Its checked literal event chain is a separate field-for-field regression and cheap goal-shape probe. -This is a complete direct proof assembler for the fixed real-sine graph, not -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. 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 emitter's -declared base-assumption list; the caller hypotheses supplied to final closure -discharge that same list. This direct emitter does not yet construct the -`InitialContext` witness that relates the declared list position-for-position -to `CheckerInput.initialFacts`. The complete `TraceReplay` checker already -constructs its `initialBase` position-for-position from -`CheckerInput.initialFacts`; separately, +`Frontend` now performs function-independent quotation of any engine history +into instance, rule, and transport records, with exact role-local ordering and +history exhaustion. `ProofFrontend` is the reusable direct proof assembler. +It walks an 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. +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 a wrong rule or transport program version, fails before +replay. + +The fold is polymorphic in the fact type and contains no sine, negation, or +other function case. Its `Context` receives the semantics/domain laws, +prefix-stability theorem, caller program, a declared base-assumption list, and +a plain-data encoder; packages remain responsible for their replay schemas. +It seeds caller facts by checked position in that declared list, and the caller +hypotheses supplied to final closure discharge the same list. The reusable +frontend does not yet construct the `InitialContext` witness that relates the +declared list position-for-position to `CheckerInput.initialFacts`. The +complete `TraceReplay` checker already constructs its `initialBase` +position-for-position from `CheckerInput.initialFacts`; separately, `ChronologicalReplay.Cursor.startInput` consumes `InitialContext` for cursor replay. The later generic frontend must carry the corresponding binding into direct emission. The current replay applications and final closure remain indexed by the exact `CheckerInput.baseProgram` and target. The emitter also seeds each 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, declared base-assumption list and its caller-input binding, -semantic bridge, and final target for an arbitrary caller expression instead -of naming this canary's fixed contexts. +lookup in the reified final program. The real-sine tactic is now a client of +this module rather than the owner of the fold, but it still names the canary's +fixed base graph, base list, semantic bridge, and final target. The next +frontend experiment must derive those pieces and the caller-input binding from +an arbitrary caller expression and validate the same API with a second +mathematical function package. The fixed canary also requires a live session with no dropped work and an exact proof history of one instance, one equality, three fact events, and the @@ -1354,9 +1361,8 @@ expected interleaving before it reads historical values through `Session.complete` holds. The values are quoted as data, while their proofs come from caller assumptions, top soundness, or an earlier emitted replay result. A future arbitrary-trace emitter must likewise obtain evidence from -its chronological proof table; a successful full-history -lookup is never evidence that the dependency was available at the required -earlier step. +its chronological proof table; a successful full-history lookup is never +evidence that the dependency was available at the required earlier step. The quotation walker consumes arbitrary `HistoryEvent` lists, requires sequential role-local indices, and rejects omitted or duplicated fact or diff --git a/conformance/HexIntervalMathlib/SineTacticConformance.lean b/conformance/HexIntervalMathlib/SineTacticConformance.lean index 3627e99ad..e6126a94c 100644 --- a/conformance/HexIntervalMathlib/SineTacticConformance.lean +++ b/conformance/HexIntervalMathlib/SineTacticConformance.lean @@ -5,6 +5,7 @@ Authors: Kim Morrison -/ import HexIntervalMathlib.SineProofConformance +import HexInterval.Experiment.ProofFrontend import Mathlib.Lean.Elab.Tactic.Meta /-! @@ -27,6 +28,7 @@ namespace Hex.IntervalMathlib.SineTacticConformance open Lean Elab Tactic Meta open Hex.Interval.Experiment open Propagator PayloadArena SemanticReplay ChronologicalReplay ProofEmitter +open Frontend ProofFrontend open SineSign SineSignConformance SineProofConformance private structure LiveQuotes where @@ -35,16 +37,6 @@ private structure LiveQuotes where negation : RuleStep Range transport : TransportStep Range -/-- Proof-producing event shapes extracted from arbitrary engine chronology. -/ -private inductive LiveEvent where - | instantiation (quote : InstanceQuote) - | rule (step : RuleStep Range) - | transport (step : TransportStep Range) - -private structure LiveTrace where - program : Program - events : List LiveEvent - /-! ## A second-instantiation canary -/ private def noopKey : RuleKey := @@ -105,70 +97,8 @@ private def noopEmit : EmitPackage Name := [{ key := noopSchema.key handle := ``noopSchema }] } -private def resolveFacts? (engine : Engine Range) (inputs : List SeenVersion) : - Option (List (NodeFact Range)) := - inputs.mapM fun input => do - let fact <- engine.factAt? input - pure { node := input.node, fact } - -private def ruleStep? (engine : Engine Range) (arena : Arena) - (event : FactEvent Range) : Option (RuleStep Range) := do - let .rule action _ payload := event.cause | none - let entry <- arena.entry? payload .fact - let assumptions <- resolveFacts? engine action.inputs - let previous <- engine.factAt? event.previous - pure { event, payload, entry, assumptions, previous } - -private def transportStep? (engine : Engine Range) (arena : Arena) - (event : FactEvent Range) : Option (TransportStep Range) := do - let .transport equality source := event.cause | none - let edge <- engine.equalities[equality.index]? - let entry <- arena.entry? edge.payload .equality - let assumptions <- resolveFacts? engine edge.origin.inputs - let previous <- engine.factAt? event.previous - let sourceFact <- engine.factAt? source - pure - { event - equality - edge - payload := edge.payload - entry - assumptions - previous - sourceFact } - -/-- Walk the engine's cross-history chronology once, requiring exact -sequential indices and complete fact/instance exhaustion. -/ -private def quoteChronology? (engine : Engine Range) (arena : Arena) : - List HistoryEvent -> Nat -> Nat -> Option (List LiveEvent) - | [], nextFact, nextInstance => - if nextFact == engine.history.size && - nextInstance == engine.instanceHistory.size then - some [] - else - none - | .instance index :: rest, nextFact, nextInstance => do - if index != nextInstance then none else pure () - let event <- engine.instanceHistory[index]? - let entry <- arena.entry? event.payload .instance - let tail <- quoteChronology? engine arena rest nextFact (nextInstance + 1) - pure - (.instantiation - { event - payload := event.payload - entry } :: tail) - | .fact index :: rest, nextFact, nextInstance => do - if index != nextFact then none else pure () - let event <- engine.history[index]? - let head <- - match event.cause with - | .rule _ _ _ => (ruleStep? engine arena event).map .rule - | .transport _ _ => (transportStep? engine arena event).map .transport - let tail <- quoteChronology? engine arena rest (nextFact + 1) nextInstance - pure (head :: tail) - /-- Extract the complete proof-event list from the actual returned state. -/ -private def liveTrace? : Option LiveTrace := +private def liveTrace? : Option (Frontend.Trace Range) := match transported? with | none => none | some session => do @@ -177,9 +107,7 @@ private def liveTrace? : Option LiveTrace := none else pure () - let events <- - quoteChronology? engine session.arena engine.chronology.toList 0 0 - pure { program := engine.program, events } + Frontend.trace? engine session.arena /-- Specialize the generic quote to the literal-regression fixture. -/ private def liveQuotes? : Option LiveQuotes := do @@ -191,10 +119,11 @@ private def liveQuotes? : Option LiveQuotes := do #guard transported?.any fun session => let engine := session.state.engine - (quoteChronology? engine session.arena engine.chronology.toList 0 0).isSome && - (quoteChronology? engine session.arena + (Frontend.quote? engine session.arena + engine.chronology.toList 0 0).isSome && + (Frontend.quote? engine session.arena [.instance 0, .fact 0, .fact 0, .fact 2] 0 0).isNone && - (quoteChronology? engine session.arena + (Frontend.quote? engine session.arena [.instance 0, .fact 0, .fact 1] 0 0).isNone private def listExpr (type : Expr) (items : List Expr) : Expr := @@ -446,10 +375,6 @@ private meta def checkQuoteData (quote : LiveQuotes) : MetaM Unit := do checkQuote "equality transport" (← transportStepExpr quote.transport) (mkConst ``transportStep) -private meta def getReplay (result : Expr) : MetaM Expr := do - let success <- mkAppM ``Eq.refl #[mkConst ``Bool.true] - mkAppM ``Option.get #[result, success] - /-- Specialize generic caller-assumption seeding to this semantics adapter; the elaborator still supplies the program, base list, index, and fact. -/ private def seedAssumed (program : Program) (base : List (NodeFact Range)) @@ -457,304 +382,47 @@ 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 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 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 - if known.any fun old => old.seen == item.seen then - throwError "interval_sine: duplicate proof for a fact version" - pure (item :: known) - -/-- Assemble dependency evidence in the action's exact input order. -/ -private meta def inputProofs (program : Expr) (known : List FactProof) : - List SeenVersion -> List (NodeFact Range) -> MetaM Expr - | [], [] => - mkAppM ``EntailsList.empty - #[mkConst ``semantics, program, mkConst ``baseFacts] - | seen :: seenTail, fact :: factTail => do - unless seen.node == fact.node do - throwError "interval_sine: input node does not match resolved fact" - let some head := findProof? known seen fact.fact - | throwError "interval_sine: input fact has not been proved yet" - let tail <- inputProofs program known seenTail factTail - mkAppM ``EntailsList.cons #[head, tail] - | _, _ => - throwError "interval_sine: input versions and resolved facts differ in length" - -private meta def soundInputs (program : Expr) (known : List FactProof) - (seen : List SeenVersion) (facts : List (NodeFact Range)) : MetaM Expr := do - let proofs <- inputProofs program known seen facts - mkAppM ``EntailsList.sound #[proofs] - -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 version, - before, - after, - basePrefix, - stepPrefix, - sameOperations, - ← instanceQuoteExpr quote, - previous] - getReplay result - -/-- 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] - let found <- mkAppM ``Eq.refl #[someFact] - 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" - let nodeTerm <- nodeExpr node - let instructionTerm <- instructionExpr instruction - let someInstruction <- mkAppM ``Option.some #[instructionTerm] - let found <- mkAppM ``Eq.refl #[someInstruction] - let proof <- - 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 - -/-- 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 basePrefix : 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 := 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 - let result <- - mkAppM ``ProofEmitter.replayRule - #[mkConst schema, - mkConst ``rangeSchema, - mkConst ``checkerInput, - program, - basePrefix, - mkConst ``baseFacts, - ← ruleStepExpr step, - 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 basePrefix : 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 := 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" - let inputs <- soundInputs program known step.edge.origin.inputs step.assumptions - let schema <- schemaName table "equality transport" step.entry - let result <- - mkAppM ``ProofEmitter.replayTransport - #[mkConst schema, - mkConst ``rangeSchema, - mkConst ``laws, - mkConst ``checkerInput, - mkNatLit version, - program, - basePrefix, - mkConst ``baseFacts, - ← transportStepExpr step, - 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 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.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.basePrefix state.version table state.known step - emitEvents finalValue finalProgram table rest { state with known } +/-- The real-sine adapter for the function-independent proof-event fold. -/ +private def frontendContext : ProofFrontend.Context Range Name := + { encoder := + { program := programExpr + nodeId := nodeExpr + node := instructionExpr + fact := fun fact => pure (rangeExpr fact) + nodeFact := nodeFactExpr + instanceQuote := instanceQuoteExpr + ruleStep := ruleStepExpr + transportStep := transportStepExpr } + resolveSchema := pure + semantics := mkConst ``semantics + domain := mkConst ``rangeSchema + laws := mkConst ``laws + stableLaw := mkConst ``stableLaw + input := mkConst ``checkerInput + assumed := ``seedAssumed + baseFacts + baseFactsTerm := mkConst ``baseFacts + baseProgram := SineSign.baseProgram + baseProgramTerm := mkConst ``baseProgram + basePrefix := mkConst ``basePrefix + baseWithin := mkConst ``baseWithin + initialExtension := mkConst ``initialExtension + finalPrefix := mkConst ``programPrefix + sameOperations := mkConst ``sameOperations + top := fun domain => rangeSchema.top domain } /-- Emit a proof by folding arbitrary fact events through an exact `(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) +private meta def emitTrace (programValue : Program) + (events : List (Frontend.Event Range)) (table : SchemaTable Name) : MetaM Expr := do - 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 state ← + ProofFrontend.emitTrace frontendContext programValue events table let target := { node := node 2, version := 1 : SeenVersion } - let some final := findProof? state.known target .nonpositive + let some final := ProofFrontend.findProof? state.known target .nonpositive | throwError "interval_sine: trace did not prove the requested target" mkAppM ``closeEvidence #[state.extension, final] @@ -866,7 +534,7 @@ example : True := by .rule quote.negation, .instantiation oversizedNoop, .transport lateTransport ] repeatTable)).isSome then throwError "interval_sine test: oversized repeated instantiation was accepted" - let reordered : List LiveEvent := + let reordered : List (Frontend.Event Range) := [ .instantiation quote.instantiation, .rule quote.negation, .rule quote.sine, .transport quote.transport ] if (← observing? (emitTrace extendedProgram reordered table)).isSome then @@ -878,12 +546,20 @@ example : True := by [ .instantiation quote.instantiation, .rule quote.sine, .rule quote.negation, .transport wrongVersion ] table)).isSome then throwError "interval_sine test: stale transport program version was accepted" + let staleSine : RuleStep Range := + { quote.sine with + event := { quote.sine.event with programVersion := 2 } } + if (← observing? (emitTrace extendedProgram + [ .instantiation quote.instantiation, .rule staleSine, + .rule quote.negation, .transport quote.transport ] table)).isSome then + throwError "interval_sine test: stale rule program version was accepted" if (← observing? (emitTrace baseProgram [ .instantiation quote.instantiation, .rule quote.sine, .rule quote.negation, .transport quote.transport ] table)).isSome then throwError "interval_sine test: emission against the wrong final program was accepted" if (← observing? - (seedNew baseProgram (mkConst ``baseProgram) [node 3] [])).isSome then + (ProofFrontend.seedNew frontendContext 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" diff --git a/lakefile.lean b/lakefile.lean index a3012e113..ad632dd23 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -311,6 +311,8 @@ lean_lib HexIntervalExperiment where `HexInterval.Experiment.GenericInstanceReconstruction, `HexInterval.Experiment.ProofEmitter, `HexInterval.Experiment.ProofRegistry, + `HexInterval.Experiment.Frontend, + `HexInterval.Experiment.ProofFrontend, `HexInterval.Experiment.TraceReplay, `HexInterval.Experiment.SineSign] diff --git a/progress/20260811T115319Z.md b/progress/20260811T115319Z.md new file mode 100644 index 000000000..0dde060e3 --- /dev/null +++ b/progress/20260811T115319Z.md @@ -0,0 +1,31 @@ +# Accomplished + +- Extracted function-independent engine-history quotation into a Mathlib-free + `Frontend` module parameterized only by the fact type. +- Extracted the dependent direct-proof fold into a Mathlib-free + `ProofFrontend` module with a semantics/context adapter and plain-data + encoder. +- The generic fold now carries the exact program version, reconstructed + program prefix, conservative extension, base bounds, and versioned fact + evidence through arbitrary instance, rule, and transport events. +- Routed the live `Real.sin` tactic and its repeated-instantiation mutations + through the generic fold. +- Added a stale rule-version rejection test and removed the duplicated stale + transport test. +- Updated the SPEC and passed the focused 1,960-target build and all structural + checks. + +# Current frontier + +The search-to-proof path is now fact-polymorphic and contains no mathematical +function cases. The sine companion supplies only its concrete fact encoder, +semantics constants, caller graph, and final-target closure. + +# Next step + +Validate the extracted API with a second mathematical function package, then +replace the fixed caller graph/target adapter with goal-driven construction. + +# Blockers + +None. diff --git a/progress/20260811T121548Z.md b/progress/20260811T121548Z.md new file mode 100644 index 000000000..9c60e3e91 --- /dev/null +++ b/progress/20260811T121548Z.md @@ -0,0 +1,25 @@ +# Generic frontend review repairs + +## Accomplished + +- Removed the obsolete sine-specific proof fold after confirming that the live + tactic delegates entirely to the generic frontend. +- Generalized the frontend over emitter handle representation; a context now + resolves package-owned handles to Lean declarations at the elaboration + boundary. +- Rebuilt the complete real-sine tactic conformance target and reran structural + and trust-surface checks. + +## Current frontier + +The generic proof frontend has one implementation of chronological evidence +assembly and does not require schema tables to store `Lean.Name` directly. + +## Next step + +Push the repaired PR head, obtain a fresh exact-head second opinion, and rebase +the independent exponential package experiment onto this API. + +## Blockers + +None. diff --git a/progress/20260811T161652Z.md b/progress/20260811T161652Z.md new file mode 100644 index 000000000..402436355 --- /dev/null +++ b/progress/20260811T161652Z.md @@ -0,0 +1,27 @@ +# Accomplished + +- Reconciled the reusable generic chronology and proof frontend with the + current joint package registry and repeated-instantiation stack. +- Preserved exact role-local history exhaustion, program/version reconstruction, + versioned evidence lookup, and package-addressed proof emission without + function cases. +- Kept the real-sine tactic as a client of the generic frontend and retained + stale-version, future-dependency, malformed-payload, and schema-selection + rejection tests. +- Refreshed the exact Lake registration exemption and rebuilt the frontend, + proof registry, and sine tactic conformance targets successfully. + +# Current frontier + +The function-independent event fold now lives in reusable Mathlib-free modules. +The next vertical must show that a second mathematical function can use the +same registry, frontend, and target-closing path without adding a central case. + +# Next step + +Push the reconciled exact head for independent review, then reconcile the +independent exponential-function vertical. + +# Blockers + +None. diff --git a/progress/20260811T163700Z.md b/progress/20260811T163700Z.md new file mode 100644 index 000000000..a17c60255 --- /dev/null +++ b/progress/20260811T163700Z.md @@ -0,0 +1,22 @@ +# Accomplished + +- Propagated the selected-schema trust correction, guarded theorem axiom + report, and joint package-registry invariant into the reusable generic proof + frontend. +- Preserved the frontend's function-agnostic event fold, seed authentication, + and schema-handle abstraction. + +# Current frontier + +The reusable frontend has no mathematical-function cases. It receives quoted +events and package-owned schema handles, then emits only typechecked replay +applications against an authenticated evidence table. + +# Next step + +Finish checks, push the exact head for review, then propagate the reconciled +frontend into the independent `Real.exp` vertical. + +# Blockers + +None. diff --git a/scripts/bench/proof_only_runtime_exemptions.json b/scripts/bench/proof_only_runtime_exemptions.json index b013f2a96..327ec7c0e 100644 --- a/scripts/bench/proof_only_runtime_exemptions.json +++ b/scripts/bench/proof_only_runtime_exemptions.json @@ -95,6 +95,12 @@ "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": "lakefile.lean", + "baseline_blob": "6dd80771ae2212333b2a9b925b52056e0037ff56", + "current_blob": "ad632dd2368f1771255d0831dd6e1d4981b2a155", + "reason": "Additionally registers the Mathlib-free generic interval chronology quotation and proof-frontend modules only; the factorization service target and executable dependency graph are unchanged." + }, { "path": "HexBerlekamp/FactorTacticTests.lean", "baseline_blob": "4063e15934a89c671ac72d201fa60c2ef6feaf59",