From 316034f9cd97b8c26a16702c0a6dee94f4c1293d Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 11 Aug 2026 17:19:34 +0000 Subject: [PATCH] Propagate provenance honesty through goal frontend; progress 20260811T171522Z --- HexInterval/Experiment/GoalFrontend.lean | 255 ++++++++++++++++++ HexInterval/SPEC/hex-interval.md | 42 ++- .../ExpSignConformance.lean | 140 +++++++++- lakefile.lean | 1 + progress/20260811T122811Z.md | 30 +++ progress/20260811T124002Z.md | 25 ++ progress/20260811T124756Z.md | 26 ++ progress/20260811T130603Z.md | 25 ++ progress/20260811T162139Z.md | 28 ++ progress/20260811T163851Z.md | 22 ++ .../bench/proof_only_runtime_exemptions.json | 6 + 11 files changed, 594 insertions(+), 6 deletions(-) create mode 100644 HexInterval/Experiment/GoalFrontend.lean create mode 100644 progress/20260811T122811Z.md create mode 100644 progress/20260811T124002Z.md create mode 100644 progress/20260811T124756Z.md create mode 100644 progress/20260811T130603Z.md create mode 100644 progress/20260811T162139Z.md create mode 100644 progress/20260811T163851Z.md diff --git a/HexInterval/Experiment/GoalFrontend.lean b/HexInterval/Experiment/GoalFrontend.lean new file mode 100644 index 000000000..a12eda655 --- /dev/null +++ b/HexInterval/Experiment/GoalFrontend.lean @@ -0,0 +1,255 @@ +/- +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.SemanticReplay + +@[expose] public section + +/-! +# Extensible goal reification + +This experiment derives a typed expression program and checker input from Lean +expressions without a central case split over mathematical functions. Each +package owns one operation signature and a recognizer for that operation. +Reification tries all packages with the requested output domain, rejects +ambiguous matches, recursively reifies arguments in signature order, and +performs exact-expression common-subexpression elimination. + +Fact parsing is a separate adapter. It maps caller propositions to a term, +domain, and fact. Unrecognized hypotheses are ignored, while the target must +be recognized exactly. This division lets interval domains choose their own +open/closed fact language without putting it in the expression-DAG builder. +-/ + +namespace Hex.Interval.Experiment.GoalFrontend + +open Lean Meta +open Propagator SemanticReplay + +/-- Deterministic bounds for package discovery and recursive graph building. -/ +structure Limits where + maxPackages : Nat + maxNodes : Nat + maxDepth : Nat + deriving DecidableEq, Repr + +/-- One package-owned Lean-syntax view of an opaque engine operation. + +Nullary packages represent caller variables or constants. A recognizer must +return arguments in the exact order declared by `operation.inputs`. -/ +structure Package where + operation : Operation + recognize : Expr → MetaM (Option (List Expr)) + +/-- A validated operation/recognizer registry. -/ +structure Registry where + private mk :: + limits : Limits + packages : Array Package + operations : Array Operation + +private def makeRegistry (limits : Limits) (packages : Array Package) + (operations : Array Operation) : Registry := + { limits, packages, operations } + +namespace Registry + +private def uniqueKeys : List Operation → Bool + | [] => true + | operation :: rest => + !(rest.any fun other => other.key == operation.key) && uniqueKeys rest + +/-- Validate finite package assembly before inspecting a goal. -/ +opaque build (limits : Limits) (packages : Array Package) : + Except String Registry := do + if packages.size > limits.maxPackages then + throw "too many goal-reification packages" + let operations := packages.map (fun package => package.operation) + if !uniqueKeys operations.toList then + throw "duplicate goal-reification operation key" + pure (makeRegistry limits packages operations) + +end Registry + +/-- One exact Lean expression already assigned to a graph node and domain. -/ +structure TermRef where + expression : Expr + domain : DomainId + node : NodeId + +/-- Mutable-by-return graph construction state. -/ +structure State where + nodes : Array Node := #[] + terms : Array TermRef := #[] + +/-- A proposition parsed into one fact about one Lean term. -/ +structure Claim (Fact : Type) where + expression : Expr + domain : DomainId + fact : Fact + +/-- Domain-specific recognition of hypotheses and the requested target. -/ +structure Parser (Fact : Type) where + parse : Expr → MetaM (Option (Claim Fact)) + +/-- One caller proposition contributing to a version-zero meet. -/ +structure Assumption (Fact : Type) where + fact : Fact + proof : Expr + +/-- Complete provenance for one caller-owned version-zero fact. + +The empty list denotes domain top. Each later entry must be combined in order +through the fact-domain meet theorem, so several hypotheses about the same +expression cannot overwrite one another's proof dependency. -/ +structure Seed (Fact : Type) where + assumptions : List (Assumption Fact) := [] + +/-- Exact frontend result, including the syntax-to-node map needed to connect +kernel expressions to the opaque program. -/ +structure Result (Fact : Type) where + input : CheckerInput Fact + baseFacts : List (NodeFact Fact) + seeds : Array (Seed Fact) + terms : Array TermRef + +def State.find? (state : State) (expression : Expr) (domain : DomainId) : + Option NodeId := do + let found ← state.terms.toList.find? fun term => + term.domain == domain && term.expression == expression + pure found.node + +/-- Select exactly one package for an expression and expected output domain. +No matching package is ordinary absence; malformed or ambiguous matches remain +hard errors. -/ +def select? (registry : Registry) (expression : Expr) (domain : DomainId) : + MetaM (Option (Nat × Package × List Expr)) := do + let mut selected : Option (Nat × Package × List Expr) := none + for index in [0:registry.packages.size] do + let some package := registry.packages[index]? + | throwError "interval goal frontend: package index escaped its registry" + if package.operation.output == domain then + let match? ← withoutModifyingState <| package.recognize expression + match match? with + | none => pure () + | some arguments => + if arguments.length != package.operation.inputs.length then + throwError + "interval goal frontend: package returned the wrong argument count" + if selected.isSome then + throwError "interval goal frontend: ambiguous expression package" + selected := some (index, package, arguments) + pure selected + +/-- Recursively append one expression and its dependencies to the SSA graph. +Absence means that the expression is unsupported or exceeds the graph budget; +the input state is immutable, so a caller may discard the whole attempt. -/ +partial def reifyTerm? (registry : Registry) (expression : Expr) + (domain : DomainId) (depth : Nat) (state : State) : + MetaM (Option (NodeId × State)) := do + if registry.limits.maxDepth < depth then + return none + if let some node := state.find? expression domain then + return some (node, state) + let some (operationIndex, package, arguments) ← + select? registry expression domain + | return none + let mut state := state + let mut nodes := [] + for (argument, argumentDomain) in arguments.zip package.operation.inputs do + let some (node, next) ← + reifyTerm? registry argument argumentDomain (depth + 1) state + | return none + state := next + nodes := nodes.concat node + if registry.limits.maxNodes ≤ state.nodes.size then + return none + let node : NodeId := { index := state.nodes.size } + let instruction : Node := + { domain + op := { index := operationIndex } + args := nodes } + pure <| some + (node, + { nodes := state.nodes.push instruction + terms := state.terms.push { expression, domain, node } }) + +private def installedFact (domain : FactDomain Fact) (nodeDomain : DomainId) + (current proposed : Fact) : Except String Fact := + match domain.narrow nodeDomain current proposed with + | .noChange => pure current + | .improved installed | .contradiction installed => pure installed + | .malformed _ => throw "malformed caller interval fact" + | .resourceLimit _ => throw "caller interval fact exceeded its resource bound" + +/-- Reify a target and all recognized local hypotheses into one checker input. + +The target is traversed first, so its node and dependencies have stable early +identifiers. Later hypotheses reuse those nodes by exact-expression CSE and +may append additional expressions needed only by their facts. -/ +opaque reify (registry : Registry) (factDomain : FactDomain Fact) + (parser : Parser Fact) (hypotheses : List (Expr × Expr)) (target : Expr) : + MetaM (Result Fact) := do + let some targetClaim ← withoutModifyingState <| parser.parse target + | throwError "interval goal frontend: target is not an interval claim" + let some (targetNode, initial) ← + reifyTerm? registry targetClaim.expression targetClaim.domain 0 {} + | throwError "interval goal frontend: target expression is unsupported or exceeds its resource bound" + let mut state := initial + let mut assumed : List (NodeFact Fact × Expr) := [] + for (proposition, proof) in hypotheses do + let parsed ← withoutModifyingState <| parser.parse proposition + match parsed with + | none => pure () + | some claim => + match ← reifyTerm? registry claim.expression claim.domain 0 state with + | none => pure () + | some (node, next) => + state := next + assumed := assumed.concat ({ node, fact := claim.fact }, proof) + let program : Program := + { operations := registry.operations + nodes := state.nodes } + unless program.check do + throwError "interval goal frontend: reified program failed structural validation" + let mut facts := #[] + let mut seeds := #[] + for index in [0:state.nodes.size] do + let some instruction := state.nodes[index]? + | throwError "interval goal frontend: node index escaped the graph" + facts := facts.push (factDomain.top instruction.domain) + seeds := seeds.push {} + for (fact, proof) in assumed do + let some instruction := state.nodes[fact.node.index]? + | throwError "interval goal frontend: assumption node escaped the graph" + let some current := facts[fact.node.index]? + | throwError "interval goal frontend: assumption fact escaped the graph" + let some seed := seeds[fact.node.index]? + | throwError "interval goal frontend: assumption seed escaped the graph" + let installed ← + match installedFact factDomain instruction.domain current fact.fact with + | .ok installed => pure installed + | .error message => throwError "interval goal frontend: {message}" + facts := facts.set! fact.node.index installed + seeds := seeds.set! fact.node.index + { assumptions := seed.assumptions.concat { fact := fact.fact, proof } } + let targetFact : NodeFact Fact := + { node := targetNode, fact := targetClaim.fact } + pure + { input := + { baseProgram := program + initialFacts := facts + target := targetFact } + baseFacts := + List.ofFn fun index : Fin facts.size => + { node := { index := index.val }, fact := facts[index] } + seeds + terms := state.terms } + +end Hex.Interval.Experiment.GoalFrontend diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index f9accc618..2e7f7a5f0 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -1348,8 +1348,9 @@ 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. 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. +this module rather than the owner of the fold. Its semantic bridge and final +proof closure still name the canary's fixed base graph, declared base list, +and target; the goal reifier below begins removing that specialization. A second live vertical validates this separation with `Real.exp`. Its Mathlib-free package uses a distinct three-element fact lattice, contributes @@ -1359,9 +1360,40 @@ one replay schema. The same policy session, joint package registry, fact-polymorphic quotation, shared structural encoder, and generic evidence fold produce the ordinary theorem `0 ≤ Real.exp x`. Thus both a multi-package graph-growing sine proof and a single-rule exponential proof pass through the -same frontend API without a function switch. The next frontend experiment -must derive the fixed context pieces and the caller-input binding from an -arbitrary caller expression. +same frontend API without a function switch. The goal reifier below derives +candidate context pieces from an arbitrary caller expression, but generic +proof emission has not yet bound its recorded seed recipe to the frontend's +declared base list. + +The first goal-reification experiment now derives the exponential canary's +base program, version-zero fact array, and target fact from the actual Lean +goal before running its compiled fixture. Expression packages contribute an +opaque operation signature and a Lean-expression recognizer; the reifier has +no switch for exponential, sine, or any other mathematical function. It tries +all packages with the required output domain, requires a unique match and +exact arity, and runs each recognizer without retaining changes to elaborator +state. It recursively reifies arguments in signature order, performs exact +expression/domain CSE, validates the resulting SSA program, and enforces +package, node, and depth limits. A separate fact parser maps propositions to a +term, domain, and fact, so interval endpoint and open/closed semantics do not +enter graph construction. Parser calls likewise retain no elaborator-state +changes. The target is reified first and is strict: an unsupported or +over-budget target fails. A parsed hypothesis is optional information; if its +term or a recursive dependency has no package or exceeds the remaining graph +budget, that whole immutable attempt is discarded. Malformed arity and +ambiguous package matches remain hard registry errors. All accepted hypotheses +narrowing the same version-zero node remain in an ordered seed recipe; later +hypotheses cannot overwrite an earlier proof dependency, while facts about +other recognized expressions may append a suffix after the target graph. The +exponential tactic currently requires only the target-reachable operation and +node prefixes, and the target fact, to match its fixed semantic/proof fixture. +Extra supported, duplicate, unsupported-real, and non-real hypotheses therefore +do not disable an otherwise applicable proof; later operation packages may +also extend the registry after the target prefix. Removing that last prefix +comparison requires package-compositional construction of the program +semantics and generic proof emission for the recorded top/assumption seed +recipes; it remains the next frontend experiment rather than an assumed +capability. 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 diff --git a/conformance/HexIntervalMathlib/ExpSignConformance.lean b/conformance/HexIntervalMathlib/ExpSignConformance.lean index 7cf459a72..8a6678e9c 100644 --- a/conformance/HexIntervalMathlib/ExpSignConformance.lean +++ b/conformance/HexIntervalMathlib/ExpSignConformance.lean @@ -5,6 +5,7 @@ Authors: Kim Morrison -/ import HexIntervalMathlib.Experiment.ExpSign +import HexInterval.Experiment.GoalFrontend import HexInterval.Experiment.ProofFrontend import Mathlib.Lean.Elab.Tactic.Meta @@ -23,7 +24,91 @@ namespace Hex.IntervalMathlib.ExpSignConformance open Lean Elab Tactic Meta open Hex.Interval.Experiment open Propagator PolicySession SemanticReplay ChronologicalReplay ProofEmitter -open Frontend FrontendEncoder ProofFrontend ProofRegistry ExpSign +open Frontend FrontendEncoder ProofFrontend ProofRegistry GoalFrontend ExpSign + +/-! ## Extensible goal reification -/ + +private def sourceSyntax : GoalFrontend.Package := + { operation := sourceOperation + recognize := fun expression => do + let type ← inferType expression + pure <| + if expression.isFVar && type == mkConst ``Real then some [] else none } + +private def expSyntax : GoalFrontend.Package := + { operation := expOperation + recognize := fun expression => + let arguments := expression.getAppArgs + pure <| + if expression.getAppFn.constName? == some ``Real.exp && + arguments.size == 1 then + some [arguments[0]!] + else + none } + +private def goalRegistry? : Except String GoalFrontend.Registry := + GoalFrontend.Registry.build + { maxPackages := 4, maxNodes := 16, maxDepth := 8 } + #[sourceSyntax, expSyntax] + +private def isZero (expression : Expr) : Bool := + let arguments := expression.getAppArgs + expression.getAppFn.constName? == some ``OfNat.ofNat && + arguments.size == 3 && + match arguments[1]! with + | .lit (.natVal 0) => true + | _ => false + +private def claimParser : GoalFrontend.Parser Bound := + { parse := fun proposition => do + let arguments := proposition.getAppArgs + if proposition.getAppFn.constName? == some ``LE.le && + arguments.size ≥ 2 then + let left := arguments[arguments.size - 2]! + let right := arguments[arguments.size - 1]! + let rightType ← inferType right + if isZero left && rightType == mkConst ``Real then + pure <| some + { expression := right + domain := real + fact := .nonnegative } + else + pure none + else + pure none } + +private meta def reifyGoal (target : Expr) : MetaM (GoalFrontend.Result Bound) := do + let registry ← + match goalRegistry? with + | .ok registry => pure registry + | .error message => + throwError "interval_exp: invalid goal registry: {message}" + let context ← getLCtx + let mut hypotheses := [] + for declaration in context do + unless declaration.isImplementationDetail do + hypotheses := hypotheses.concat + (← instantiateMVars declaration.type, mkFVar declaration.fvarId) + GoalFrontend.reify registry factDomain claimParser hypotheses target + +/-- The live proof fixture covers the target-reachable prefix. Additional +caller facts may append nodes or narrow version-zero facts without changing +the independent exponential proof. -/ +private def sameTargetGraph (input : CheckerInput Bound) : Bool := + input.baseProgram.operations.toList.take + checkerInput.baseProgram.operations.size == + checkerInput.baseProgram.operations.toList && + input.baseProgram.nodes.toList.take checkerInput.baseProgram.nodes.size == + checkerInput.baseProgram.nodes.toList && + input.target == checkerInput.target + +private def spareOperation : Operation := + { key := { name := "exp-sign.spare" }, inputs := [], output := real } + +#guard + sameTargetGraph + { checkerInput with + baseProgram := { program with operations := operations.push spareOperation } } def offer? (session : PolicySession.Session Bound) (accepts : Propagator.Policy.OfferView → Bool) : @@ -146,6 +231,9 @@ private def expTarget (x : ℝ) : Prop := 0 ≤ Real.exp x private meta def proveExp (target : Expr) : MetaM Expr := do + let reified ← reifyGoal target + unless sameTargetGraph reified.input do + throwError "interval_exp: goal reification produced an unexpected target graph" let context ← getLCtx for declaration in context do unless declaration.isImplementationDetail do @@ -180,10 +268,60 @@ syntax (name := intervalExpTac) "interval_exp" : tactic theorem tacticExp (x : ℝ) : 0 ≤ Real.exp x := by interval_exp +theorem tacticExpExtra (x y : ℝ) (_hy : 0 ≤ Real.exp y) : + 0 ≤ Real.exp x := by + interval_exp + +theorem tacticExpDuplicate (x : ℝ) (_h₁ _h₂ : 0 ≤ Real.exp x) : + 0 ≤ Real.exp x := by + interval_exp + +theorem tacticExpNat (x : ℝ) (n : Nat) (_hn : 0 ≤ n) : + 0 ≤ Real.exp x := by + interval_exp + +theorem tacticExpUnsupported (x y z : ℝ) (_h : 0 ≤ y * z) : + 0 ≤ Real.exp x := by + interval_exp + example (_x : ℝ) : True := by fail_if_success interval_exp trivial +set_option linter.unusedTactic false in +set_option linter.unusedVariables false in +example (x : ℝ) (h₁ h₂ : 0 ≤ Real.exp x) : True := by + run_tac + let context ← getLCtx + let mut target? := none + for declaration in context do + if (← claimParser.parse declaration.type).isSome then + target? := some declaration.type + let some target := target? + | throwError "interval_exp goal test: parsed hypothesis is missing" + let result ← reifyGoal target + let some seed := result.seeds[1]? + | throwError "interval_exp goal test: target seed is missing" + unless result.input.baseProgram.nodes.size == 2 && + result.terms.size == 2 && seed.assumptions.length == 2 && + result.input.initialFacts[1]? == some .nonnegative do + throwError "interval_exp goal test: CSE or assumption seeding failed" + let aliasPackage : GoalFrontend.Package := + { expSyntax with + operation := + { expOperation with key := { name := "exp-sign.exp-alias" } } } + let registry ← + match GoalFrontend.Registry.build + { maxPackages := 4, maxNodes := 16, maxDepth := 8 } + #[sourceSyntax, expSyntax, aliasPackage] with + | .ok registry => pure registry + | .error message => + throwError "interval_exp goal test: invalid alias registry: {message}" + if (← observing? <| + GoalFrontend.reify registry factDomain claimParser [] target).isSome then + throwError "interval_exp goal test: ambiguous syntax packages were accepted" + trivial + set_option linter.unusedTactic false in example : True := by run_tac diff --git a/lakefile.lean b/lakefile.lean index b71eea886..9c1dba3ba 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -314,6 +314,7 @@ lean_lib HexIntervalExperiment where `HexInterval.Experiment.Frontend, `HexInterval.Experiment.FrontendEncoder, `HexInterval.Experiment.ProofFrontend, + `HexInterval.Experiment.GoalFrontend, `HexInterval.Experiment.TraceReplay, `HexInterval.Experiment.SineSign, `HexInterval.Experiment.ExpSign] diff --git a/progress/20260811T122811Z.md b/progress/20260811T122811Z.md new file mode 100644 index 000000000..ba95aa494 --- /dev/null +++ b/progress/20260811T122811Z.md @@ -0,0 +1,30 @@ +# Extensible goal reification + +## Accomplished + +- Added a function-independent goal reifier whose packages own operation + signatures and Lean-expression recognizers. +- Added bounded recursive SSA construction, exact expression/domain CSE, + unique-match and arity checks, and final program validation. +- Separated proposition-to-fact parsing from expression construction and + retained every same-node hypothesis in an ordered version-zero seed recipe. +- Routed the live `Real.exp` tactic through reification of its actual goal and + required the derived checker input to match the existing semantic fixture. +- Added conformance checks for same-expression CSE, assumption seeding, and + rejection of overlapping syntax packages. + +## Current frontier + +The graph, initial fact array, and target can now be derived without a central +function switch. The exponential canary still compares that result with a +fixed semantics/proof fixture before planning and proof emission. + +## Next step + +Make operation packages contribute compositional semantics and teach the proof +frontend to discharge the reifier's top/assumption seed recipes, eliminating +the fixed-fixture equality gate. + +## Blockers + +None. diff --git a/progress/20260811T124002Z.md b/progress/20260811T124002Z.md new file mode 100644 index 000000000..8e6eeea10 --- /dev/null +++ b/progress/20260811T124002Z.md @@ -0,0 +1,25 @@ +# Goal frontend reconciliation + +## Accomplished + +- Reconciled the goal-derived expression graph experiment with the repaired + shared sine and exponential proof frontends. +- Preserved both the new goal reifier and the single-pass exponential proof + emitter whose diagnostics are not swallowed by backtracking. +- Removed the sine client's duplicate structural encoder through the updated + base branch. + +## Current frontier + +The exponential canary now checks a checker input derived from the actual Lean +goal before running the same generic proof frontend used by the sine canary. + +## Next step + +Rebuild the combined branch, obtain a fresh exact-head second opinion, and then +replace the remaining fixed semantic fixture with package-compositional +semantics and seed discharge. + +## Blockers + +None. diff --git a/progress/20260811T124756Z.md b/progress/20260811T124756Z.md new file mode 100644 index 000000000..0b254f797 --- /dev/null +++ b/progress/20260811T124756Z.md @@ -0,0 +1,26 @@ +# Goal reifier robustness + +## Accomplished + +- Kept the fixed exponential proof canary tied only to the target-reachable + graph prefix instead of rejecting harmless additional caller facts. +- Made proposition parsing reject non-real inequalities before graph + construction. +- Added tactic canaries for unrelated exponential facts, duplicate target + facts, and natural-number inequalities. +- Isolated each package recognizer from persistent elaborator-state changes. + +## Current frontier + +The actual-goal reifier remains package-driven and now preserves the previous +exponential tactic's applicability in richer local contexts. The fixed proof +fixture is still used only for the target prefix. + +## Next step + +Replace that final prefix comparison with package-composed semantics and proof +closure for the reified graph and its ordered seed recipes. + +## Blockers + +None. diff --git a/progress/20260811T130603Z.md b/progress/20260811T130603Z.md new file mode 100644 index 000000000..a6c764e23 --- /dev/null +++ b/progress/20260811T130603Z.md @@ -0,0 +1,25 @@ +# Optional-hypothesis reification + +## Accomplished + +- Kept target graph construction strict while making unsupported or + over-budget hypotheses optional inputs that leave the graph unchanged. +- Preserved hard errors for malformed and ambiguous package registrations. +- Compared only the target's operation and node prefixes against the temporary + exponential proof fixture, so later packages do not disable the tactic. +- Added regressions for unsupported real bounds, extended operation tables, + and two same-node seed assumptions. + +## Current frontier + +The package-driven goal frontend now remains applicable in richer local and +package contexts without weakening target validation or proof checking. + +## Next step + +Land the reviewed frontend, then discharge its node meanings and ordered seeds +through the package-composed semantics layer. + +## Blockers + +None. diff --git a/progress/20260811T162139Z.md b/progress/20260811T162139Z.md new file mode 100644 index 000000000..9fe76f8b9 --- /dev/null +++ b/progress/20260811T162139Z.md @@ -0,0 +1,28 @@ +# Accomplished + +- Reconciled package-driven goal reification with the current independent + exponential package and generic proof frontend. +- Preserved strict target reification, optional transactional hypothesis + reification, exact expression/domain sharing, ordered seed recipes, and + package/node/depth resource limits. +- Kept unsupported or over-budget hypotheses from disabling an applicable + proof while retaining hard failures for malformed or ambiguous package + registrations. +- Refreshed the exact Lake registration exemption and rebuilt the goal + frontend plus sine and exponential conformance targets successfully. + +# Current frontier + +The frontend derives an SSA target graph and seed facts from an arbitrary Lean +goal without mathematical-function cases. The exponential proof fixture still +pins the target-reachable program prefix; package-composed semantic meanings +and fully dynamic proof closure are the next layers. + +# Next step + +Push the reconciled exact head for independent review, then reconcile semantic +operation meanings and dynamic target closure. + +# Blockers + +None. diff --git a/progress/20260811T163851Z.md b/progress/20260811T163851Z.md new file mode 100644 index 000000000..5a8471564 --- /dev/null +++ b/progress/20260811T163851Z.md @@ -0,0 +1,22 @@ +# Accomplished + +- Propagated the reconciled arbitrary-function frontend, joint package + registry, selected-schema trust boundary, and guarded sine axiom report into + goal reification. +- Preserved strict target reification and transactional treatment of optional, + unrelated hypotheses. + +# Current frontier + +Supported Lean goal graphs can be reified without function cases in the proof +frontend. Unsupported hypotheses remain optional information, while the target +and every emitted replay application remain strictly checked. + +# Next step + +Finish builds and static checks, push the exact head for review, then carry the +reconciled stack into operation semantics and dynamic target closure. + +# Blockers + +None. diff --git a/scripts/bench/proof_only_runtime_exemptions.json b/scripts/bench/proof_only_runtime_exemptions.json index f91eb2d99..cd991e971 100644 --- a/scripts/bench/proof_only_runtime_exemptions.json +++ b/scripts/bench/proof_only_runtime_exemptions.json @@ -107,6 +107,12 @@ "current_blob": "b71eea88678be6aa3c8c461ce3cd130c867ed65d", "reason": "Additionally registers the shared interval frontend encoder and independent exponential-sign experiment/conformance only; the factorization service target and executable dependency graph are unchanged." }, + { + "path": "lakefile.lean", + "baseline_blob": "6dd80771ae2212333b2a9b925b52056e0037ff56", + "current_blob": "9c1dba3baec47ca1c222742abb9e0d579fe4e6b5", + "reason": "Additionally registers the generic interval goal-reification experiment only; the factorization service target and executable dependency graph are unchanged." + }, { "path": "HexBerlekamp/FactorTacticTests.lean", "baseline_blob": "4063e15934a89c671ac72d201fa60c2ef6feaf59",