From fc346668030aa5c66b6b77eb08690846b18762df Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 11 Aug 2026 17:18:46 +0000 Subject: [PATCH] Propagate provenance honesty through exponential vertical; progress 20260811T171522Z --- HexInterval/Experiment/ExpSign.lean | 181 +++++++++++++ HexInterval/Experiment/FrontendEncoder.lean | 253 ++++++++++++++++++ HexInterval/Experiment/ProofFrontend.lean | 17 +- HexInterval/SPEC/hex-interval.md | 17 +- HexIntervalMathlib/Experiment/ExpSign.lean | 183 +++++++++++++ .../ExpSignConformance.lean | 203 ++++++++++++++ .../SineTacticConformance.lean | 231 +--------------- lakefile.lean | 9 +- progress/20260811T120328Z.md | 31 +++ progress/20260811T121755Z.md | 23 ++ progress/20260811T123329Z.md | 26 ++ progress/20260811T161940Z.md | 26 ++ progress/20260811T163751Z.md | 22 ++ .../bench/proof_only_runtime_exemptions.json | 6 + 14 files changed, 987 insertions(+), 241 deletions(-) create mode 100644 HexInterval/Experiment/ExpSign.lean create mode 100644 HexInterval/Experiment/FrontendEncoder.lean create mode 100644 HexIntervalMathlib/Experiment/ExpSign.lean create mode 100644 conformance/HexIntervalMathlib/ExpSignConformance.lean create mode 100644 progress/20260811T120328Z.md create mode 100644 progress/20260811T121755Z.md create mode 100644 progress/20260811T123329Z.md create mode 100644 progress/20260811T161940Z.md create mode 100644 progress/20260811T163751Z.md diff --git a/HexInterval/Experiment/ExpSign.lean b/HexInterval/Experiment/ExpSign.lean new file mode 100644 index 000000000..cba9c92d7 --- /dev/null +++ b/HexInterval/Experiment/ExpSign.lean @@ -0,0 +1,181 @@ +/- +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.PolicySession + +@[expose] public section + +/-! +# Mathlib-free exponential-sign propagator + +This second arbitrary-function vertical is intentionally unrelated to rational +arithmetic and to sine's oddness instantiation. A standalone package declares +an opaque exponential operation and an unconditional positivity propagator. +Its Mathlib companion supplies the real interpretation and proof schema. +-/ + +namespace Hex.Interval.Experiment.ExpSign + +open Propagator PayloadArena + +/-- Minimal fact lattice for exponential positivity. -/ +inductive Bound where + | all + | nonnegative + | empty + deriving DecidableEq, Repr + +namespace Bound + +def meet : Bound → Bound → Bound + | .empty, _ | _, .empty => .empty + | .all, right => right + | left, .all => left + | .nonnegative, .nonnegative => .nonnegative + +def code : Bound → Nat + | .all => 0 + | .nonnegative => 1 + | .empty => 2 + +def ofCode? : Nat → Option Bound + | 0 => some .all + | 1 => some .nonnegative + | 2 => some .empty + | _ => none + +end Bound + +def factDomain : FactDomain Bound where + top _ := .all + narrow _ current proposed := + let installed := current.meet proposed + if installed == current then .noChange + else if installed == .empty then .contradiction installed + else .improved installed + +def real : DomainId := { index := 0 } + +def sourceKey : OpKey := { name := "exp-sign.source" } +def expKey : OpKey := { name := "exp-sign.exp" } +def expRuleKey : RuleKey := { name := "exp-sign.exp.nonnegative" } + +def sourceOperation : Operation := + { key := sourceKey, inputs := [], output := real } + +def expOperation : Operation := + { key := expKey, inputs := [real], output := real } + +def operations : Array Operation := #[sourceOperation, expOperation] + +def node (index : Nat) : NodeId := { index } +def payload (index : Nat) : PayloadId := { index } + +def sourceInstruction : Node := + { domain := real, op := { index := 0 }, args := [] } + +def expInstruction : Node := + { domain := real, op := { index := 1 }, args := [node 0] } + +/-- Caller graph for `exp x`. -/ +def program : Program := + { operations, nodes := #[sourceInstruction, expInstruction] } + +def expRule : Registration := + { key := expRuleKey + head := expKey + kind := .forward + watches := [.argument 0] + writes := [.result] } + +def factFormat : ReplayFormat := + { role := .fact + schema := 1 + validateBody := fun body => + match body with + | [code] => (Bound.ofCode? code).isSome + | _ => false } + +/-- Exponential positivity is independent of the input interval. -/ +def expPlan (request : RuleRequest Bound) : Plan Bound := + match request.inputs, request.writes with + | [_], [target] => + { outcome := + .success + [{ node := target, fact := .nonnegative, payload := payload 0 }] + [] {} + drafts := + [{ label := payload 0 + role := .fact + schema := 1 + body := [Bound.nonnegative.code] }] } + | _, _ => { outcome := .failed 1, drafts := [] } + +def sourcePackage : Package Bound := + { Cache := Unit + cache := () + operations := #[sourceOperation] + handlers := #[] } + +def expPackage : Package Bound := + { Cache := Unit + cache := () + operations := #[expOperation] + handlers := #[Handler.statelessPlanned expRule expPlan #[factFormat]] } + +def packages : Array (Package Bound) := #[sourcePackage, expPackage] + +def engineLimits : Propagator.Limits := + { maxOperations := 3 + maxNodes := 5 + maxRules := 3 + maxRegistryEntries := 16 + maxReplayFormats := 4 + maxArity := 1 + maxScopeNodes := 1 + maxApplications := 7 + maxQueueEntries := 24 + maxActions := 16 + maxMatcherVisits := 8 + matcherBatchSize := 8 + maxAcceptedFacts := 8 + maxRetainedSuggestions := 2 + maxEffort := 1 + maxObservationValue := 16 + maxDiagnosticValue := 300 + maxOutcomeCandidates := 1 + maxOutcomeSuggestions := 1 + maxProposalItems := 4 + maxInstances := 1 + maxGeneration := 1 + maxNodeDepth := 4 + maxEqualities := 1 + splitEndpointLimit := + { maxEndpointHeight := 8, maxAlignmentShift := 4 } } + +def policyLimits : Propagator.Policy.Limits := + { maxDecisions := 24 + maxTraversal := 256 + maxLiveOffers := 24 } + +def arenaLimits : PayloadArena.Limits := + { maxEntries := 16 + maxBodyCells := 32 + maxDrafts := 8 + maxDraftCells := 8 + maxAtom := 32 + maxSchema := 1 + maxUses := 8 } + +def limits : PolicySession.Limits := + { engine := engineLimits, policy := policyLimits, arena := arenaLimits } + +def start : Except PolicySession.StartError (PolicySession.Session Bound) := + PolicySession.Session.start factDomain program packages #[.all, .all] limits + +end Hex.Interval.Experiment.ExpSign diff --git a/HexInterval/Experiment/FrontendEncoder.lean b/HexInterval/Experiment/FrontendEncoder.lean new file mode 100644 index 000000000..7569d54d3 --- /dev/null +++ b/HexInterval/Experiment/FrontendEncoder.lean @@ -0,0 +1,253 @@ +/- +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 + +@[expose] public section + +/-! +# Shared Lean encoder for interval proof frontends + +The search engine returns ordinary data. A tactic must quote that data as +Lean expressions before applying transparent replay theorems. This module +encodes every function-independent program and trace structure once; a fact +domain contributes only its fact type expression and fact-value encoder. +-/ + +namespace Hex.Interval.Experiment.FrontendEncoder + +open Lean Meta +open Propagator PayloadArena SemanticReplay ProofEmitter + +/-- Reification boundary for a frontend's concrete fact representation. -/ +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 + +def listExpr (type : Expr) (items : List Expr) : Expr := + items.foldr + (fun item tail => mkApp3 (mkConst ``List.cons [Level.zero]) type item tail) + (mkApp (mkConst ``List.nil [Level.zero]) type) + +def natOptionExpr : Option Nat → Expr + | none => mkApp (mkConst ``Option.none [Level.zero]) (mkConst ``Nat) + | some value => + mkApp2 (mkConst ``Option.some [Level.zero]) (mkConst ``Nat) + (mkNatLit value) + +def nodeIdExpr (node : NodeId) : MetaM Expr := + mkAppM ``NodeId.mk #[mkNatLit node.index] + +def domainExpr (domain : DomainId) : MetaM Expr := + mkAppM ``DomainId.mk #[mkNatLit domain.index] + +def opExpr (operation : OpId) : MetaM Expr := + mkAppM ``OpId.mk #[mkNatLit operation.index] + +def opKeyExpr (key : OpKey) : MetaM Expr := + mkAppM ``OpKey.mk #[toExpr key.name, mkNatLit key.version] + +def operationExpr (operation : Operation) : MetaM Expr := do + mkAppM ``Operation.mk + #[← opKeyExpr operation.key, + listExpr (mkConst ``DomainId) (← operation.inputs.mapM domainExpr), + ← domainExpr operation.output] + +def nodeExpr (instruction : Node) : MetaM Expr := do + mkAppM ``Node.mk + #[← domainExpr instruction.domain, + ← opExpr instruction.op, + listExpr (mkConst ``NodeId) (← instruction.args.mapM nodeIdExpr)] + +def arrayExpr (type : Expr) (items : List Expr) : MetaM Expr := + mkAppM ``Array.mk #[listExpr type items] + +def programExpr (program : Program) : MetaM Expr := do + mkAppM ``Program.mk + #[← arrayExpr (mkConst ``Operation) + (← program.operations.toList.mapM operationExpr), + ← arrayExpr (mkConst ``Node) (← program.nodes.toList.mapM nodeExpr)] + +def ruleKeyExpr (key : RuleKey) : MetaM Expr := + mkAppM ``RuleKey.mk #[toExpr key.name, mkNatLit key.schema] + +def ruleIdExpr (rule : RuleId) : MetaM Expr := + mkAppM ``RuleId.mk #[mkNatLit rule.index] + +def applicationExpr (application : ApplicationId) : MetaM Expr := + mkAppM ``ApplicationId.mk #[mkNatLit application.index] + +def equalityExpr (equality : EqualityId) : MetaM Expr := + mkAppM ``EqualityId.mk #[mkNatLit equality.index] + +def payloadExpr (payload : PayloadId) : MetaM Expr := + mkAppM ``PayloadId.mk #[mkNatLit payload.index] + +def actionKindExpr : ActionKind → Expr + | .forward => mkConst ``ActionKind.forward + | .backward => mkConst ``ActionKind.backward + | .improve => mkConst ``ActionKind.improve + | .shave => mkConst ``ActionKind.shave + | .instantiate => mkConst ``ActionKind.instantiate + | .rewrite => mkConst ``ActionKind.rewrite + | .regularize => mkConst ``ActionKind.regularize + | .split => mkConst ``ActionKind.split + +def seenExpr (seen : SeenVersion) : MetaM Expr := + do mkAppM ``SeenVersion.mk #[← nodeIdExpr seen.node, mkNatLit seen.version] + +def structuralKeyExpr : StructuralKey → MetaM Expr + | .node node => do mkAppM ``StructuralKey.node #[← nodeIdExpr node] + | .equality equality => do + mkAppM ``StructuralKey.equality #[← equalityExpr equality] + | .application application => do + mkAppM ``StructuralKey.application #[← applicationExpr application] + +def structuralInputExpr (input : StructuralInput) : MetaM Expr := + do + mkAppM ``StructuralInput.mk + #[← structuralKeyExpr input.key, mkNatLit input.generation] + +def scopeExpr (binding : ScopeBinding) : MetaM Expr := + do + mkAppM ``ScopeBinding.mk + #[← ruleKeyExpr binding.rule, + ← nodeIdExpr binding.anchor, + listExpr (mkConst ``NodeId) (← binding.watches.mapM nodeIdExpr), + listExpr (mkConst ``NodeId) (← binding.writes.mapM nodeIdExpr)] + +def actionExpr (action : Action) : MetaM Expr := do + mkAppM ``Action.mk + #[mkNatLit action.serial, + mkNatLit action.programVersion, + ← applicationExpr action.application, + ← ruleIdExpr action.rule, + ← ruleKeyExpr action.key, + ← nodeIdExpr action.node, + actionKindExpr action.kind, + mkNatLit action.effort, + mkNatLit action.generation, + listExpr (mkConst ``SeenVersion) (← action.inputs.mapM seenExpr), + listExpr (mkConst ``NodeId) (← action.writes.mapM nodeIdExpr), + listExpr (mkConst ``StructuralInput) + (← action.structuralInputs.mapM structuralInputExpr), + natOptionExpr action.matcherEpoch] + +def roleExpr : Role → Expr + | .fact => mkConst ``Role.fact + | .instance => mkConst ``Role.instance + | .equality => mkConst ``Role.equality + +def entryExpr (entry : Entry) : MetaM Expr := do + mkAppM ``Entry.mk + #[← actionExpr entry.origin, + roleExpr entry.role, + mkNatLit entry.schema, + listExpr (mkConst ``Nat) (entry.body.map mkNatLit)] + +def factCauseExpr (factType : Expr) (factExpr : Fact → MetaM Expr) : + FactCause Fact → MetaM Expr + | .rule action proposed payload => + do + mkAppM ``FactCause.rule + #[← actionExpr action, ← factExpr proposed, ← payloadExpr payload] + | .transport equality source => do + pure <| mkApp3 (mkConst ``FactCause.transport) factType + (← equalityExpr equality) (← seenExpr source) + +def factEventExpr (factType : Expr) (factExpr : Fact → MetaM Expr) + (event : FactEvent Fact) : MetaM Expr := do + mkAppM ``FactEvent.mk + #[mkNatLit event.programVersion, + ← nodeIdExpr event.node, + ← seenExpr event.previous, + ← factExpr event.fact, + mkNatLit event.version, + ← factCauseExpr factType factExpr event.cause] + +def nodeFactExpr (factExpr : Fact → MetaM Expr) (fact : NodeFact Fact) : + MetaM Expr := + do mkAppM ``NodeFact.mk #[← nodeIdExpr fact.node, ← factExpr fact.fact] + +def edgeExpr (edge : EqualityEdge) : MetaM Expr := do + mkAppM ``EqualityEdge.mk + #[← nodeIdExpr edge.left, + ← nodeIdExpr edge.right, + mkNatLit edge.generation, + ← actionExpr edge.origin, + ← payloadExpr edge.payload] + +def instanceEventExpr (event : InstanceEvent) : MetaM Expr := do + mkAppM ``InstanceEvent.mk + #[mkNatLit event.programVersion, + ← actionExpr event.origin, + mkNatLit event.family, + listExpr (mkConst ``NodeId) (← event.substitution.mapM nodeIdExpr), + listExpr (mkConst ``NodeId) (← event.products.mapM nodeIdExpr), + listExpr (mkConst ``NodeId) (← event.newNodes.mapM nodeIdExpr), + listExpr (mkConst ``ScopeBinding) (← event.bindings.mapM scopeExpr), + listExpr (mkConst ``ScopeBinding) (← event.newBindings.mapM scopeExpr), + listExpr (mkConst ``ApplicationId) + (← event.applications.mapM applicationExpr), + listExpr (mkConst ``ApplicationId) + (← event.newApplications.mapM applicationExpr), + mkNatLit event.generation, + listExpr (mkConst ``EqualityId) (← event.equalities.mapM equalityExpr), + listExpr (mkConst ``EqualityId) + (← event.newEqualities.mapM equalityExpr), + ← payloadExpr event.payload] + +def instanceQuoteExpr (quote : InstanceQuote) : MetaM Expr := + do + mkAppM ``InstanceQuote.mk + #[← instanceEventExpr quote.event, + ← payloadExpr quote.payload, + ← entryExpr quote.entry] + +def ruleStepExpr (factType : Expr) (factExpr : Fact → MetaM Expr) + (step : RuleStep Fact) : MetaM Expr := do + let nodeFactType ← mkAppM ``NodeFact #[factType] + mkAppM ``RuleStep.mk + #[← factEventExpr factType factExpr step.event, + ← payloadExpr step.payload, + ← entryExpr step.entry, + listExpr nodeFactType (← step.assumptions.mapM (nodeFactExpr factExpr)), + ← factExpr step.previous] + +def transportStepExpr (factType : Expr) (factExpr : Fact → MetaM Expr) + (step : TransportStep Fact) : MetaM Expr := do + let nodeFactType ← mkAppM ``NodeFact #[factType] + mkAppM ``TransportStep.mk + #[← factEventExpr factType factExpr step.event, + ← equalityExpr step.equality, + ← edgeExpr step.edge, + ← payloadExpr step.payload, + ← entryExpr step.entry, + listExpr nodeFactType (← step.assumptions.mapM (nodeFactExpr factExpr)), + ← factExpr step.previous, + ← factExpr step.sourceFact] + +/-- Build the complete generic encoder from one fact-value encoder. -/ +def make (factType : Expr) (factExpr : Fact → MetaM Expr) : Encoder Fact := + { program := programExpr + nodeId := nodeIdExpr + node := nodeExpr + fact := factExpr + nodeFact := nodeFactExpr factExpr + instanceQuote := instanceQuoteExpr + ruleStep := ruleStepExpr factType factExpr + transportStep := transportStepExpr factType factExpr } + +end Hex.Interval.Experiment.FrontendEncoder diff --git a/HexInterval/Experiment/ProofFrontend.lean b/HexInterval/Experiment/ProofFrontend.lean index daa4246aa..4f757e7ca 100644 --- a/HexInterval/Experiment/ProofFrontend.lean +++ b/HexInterval/Experiment/ProofFrontend.lean @@ -6,8 +6,7 @@ Authors: Kim Morrison module -public import Lean -public import HexInterval.Experiment.Frontend +public import HexInterval.Experiment.FrontendEncoder public import HexInterval.Experiment.GenericInstanceReconstruction @[expose] public section @@ -32,19 +31,7 @@ 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 +open FrontendEncoder /-- Kernel constants and runtime values needed by the generic fold. diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index 6f48bb912..f9accc618 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -1349,10 +1349,19 @@ 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. 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. +fixed base graph, base list, semantic bridge, and final target. + +A second live vertical validates this separation with `Real.exp`. Its +Mathlib-free package uses a distinct three-element fact lattice, contributes +one unconditional nonnegativity propagator, and has neither instantiation nor +equality transport. Its Mathlib companion contributes only real semantics and +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. 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/HexIntervalMathlib/Experiment/ExpSign.lean b/HexIntervalMathlib/Experiment/ExpSign.lean new file mode 100644 index 000000000..42cc55f68 --- /dev/null +++ b/HexIntervalMathlib/Experiment/ExpSign.lean @@ -0,0 +1,183 @@ +/- +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 Mathlib.Analysis.SpecialFunctions.Exp +public import HexInterval.Experiment.ExpSign +public import HexInterval.Experiment.ProofRegistry +public import HexInterval.Experiment.GenericInstanceReconstruction + +@[expose] public section + +/-! +# Real semantics for exponential-sign propagation + +This companion interprets the independent Mathlib-free exponential package +over `ℝ` and contributes its semantic replay theorem and frontend handle. +-/ + +namespace Hex.Interval.Experiment.ExpSign + +open Propagator SemanticReplay ChronologicalReplay ProofEmitter ProofRegistry +open GenericInstanceReconstruction + +def Contains : Bound → ℝ → Prop + | .all, _ => True + | .nonnegative, x => 0 ≤ x + | .empty, _ => False + +def Models (graph : Program) (valuation : NodeId → ℝ) : Prop := + graph.node? (node 1) = some expInstruction → + valuation (node 1) = Real.exp (valuation (node 0)) + +def semantics : Semantics Bound := + { Value := ℝ + models := Models + holds := fun _ valuation fact => Contains fact.fact (valuation fact.node) } + +theorem containsMeet (left right : Bound) (x : ℝ) : + Contains (left.meet right) x ↔ Contains left x ∧ Contains right x := by + cases left <;> cases right <;> + simp_all [Bound.meet, Contains] + +def boundSchema : FactDomainSchema semantics := + { top := fun _ => .all + topSound := by + intro _ _ _ _ _ _ + trivial + proveMeet := fun _ _ previous proposed installed => + if exact : installed = previous.meet proposed then + some + { proof := by + subst installed + intro valuation _ + exact containsMeet previous proposed (valuation _) } + else + none } + +def laws : Laws semantics := + { holdsEq := by + intro _ valuation left right fact _ _ values + change Contains fact (valuation left) ↔ Contains fact (valuation right) + rw [values] } + +theorem expEntails (assumptions : List (NodeFact Bound)) : + semantics.Entails program assumptions + { node := node 1, fact := .nonnegative } := by + intro valuation model _ + change (0 : ℝ) ≤ valuation (node 1) + rw [model (by rfl)] + exact (Real.exp_pos _).le + +def expFactSchema : PackedFactSchema semantics where + rule := expRuleKey + schema := 1 + Certificate := Unit + decode := fun body => + if body == [Bound.nonnegative.code] then some () else none + replay := fun _ _ context _ => + if graphEq : context.program = program then + if proposedEq : context.proposed = + ({ node := node 1, fact := .nonnegative } : NodeFact Bound) then + some + { proof := by + simpa only [graphEq, proposedEq] using + expEntails context.assumptions } + else + none + else + none + +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 + simp [Program.node?, outside] at found + rw [Program.node?, stepPrefix.nodeAt target.index within] + exact found + +def stableLaw : StableLaw semantics := + { stable := by + intro before after _ _ stepPrefix _ + refine + { programPrefix := stepPrefix + modelsBefore := ?_ + holdsOld := ?_ } + · intro valuation model found + exact model (nodeAtPrefix stepPrefix _ _ found) + · intro oldValue newValue fact within _ _ agreement + change Contains fact.fact (oldValue fact.node) ↔ + Contains fact.fact (newValue fact.node) + rw [agreement fact.node within] } + +def sourceEmit : EmitPackage Lean.Name := { schemas := [] } + +def expEmit : EmitPackage Lean.Name := + { schemas := + [{ key := expFactSchema.key + handle := ``expFactSchema }] } + +def sourceProof : ProofRegistry.Package semantics Lean.Name := + { semantic := { factSchemas := #[] } + emit := sourceEmit } + +def expProof : ProofRegistry.Package semantics Lean.Name := + { semantic := { factSchemas := #[expFactSchema] } + emit := expEmit } + +def proofPackages : Array (ProofRegistry.Package semantics Lean.Name) := + #[sourceProof, expProof] + +def semanticPackages : Array (SemanticReplay.Package semantics) := + proofPackages.map (fun package => package.semantic) + +def baseFacts : List (NodeFact Bound) := + [{ node := node 0, fact := .all }, { node := node 1, fact := .all }] + +def checkerInput : CheckerInput Bound := + { baseProgram := program + initialFacts := #[.all, .all] + target := { node := node 1, fact := .nonnegative } } + +theorem baseWithin : FactsWithin program baseFacts := by + intro fact member + simp only [baseFacts, List.mem_cons, List.not_mem_nil, or_false] at member + rcases member with rfl | rfl <;> simp [program, node] + +theorem basePrefix : ProgramPrefix program program := + ProgramPrefix.refl program + +theorem sameOperations : program.operations = program.operations := rfl + +def initialExtension : Evidence (semantics.Extends program program) := + extendRefl semantics program + +noncomputable def valuation (x : ℝ) : NodeId → ℝ + | ⟨0⟩ => x + | ⟨1⟩ => Real.exp x + | _ => 0 + +theorem valuationModels (x : ℝ) : Models program (valuation x) := by + intro _ + rfl + +/-- Turn the generic emitted evidence into the ordinary user theorem. -/ +theorem closeExp (x : ℝ) + (result : Evidence + (semantics.Entails program baseFacts checkerInput.target)) : + 0 ≤ Real.exp x := by + have holds := result.proof (valuation x) (valuationModels x) + (by + intro fact member + simp only [baseFacts, List.mem_cons, List.not_mem_nil, or_false] at member + rcases member with rfl | rfl <;> trivial) + exact holds + +end Hex.Interval.Experiment.ExpSign diff --git a/conformance/HexIntervalMathlib/ExpSignConformance.lean b/conformance/HexIntervalMathlib/ExpSignConformance.lean new file mode 100644 index 000000000..7cf459a72 --- /dev/null +++ b/conformance/HexIntervalMathlib/ExpSignConformance.lean @@ -0,0 +1,203 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ + +import HexIntervalMathlib.Experiment.ExpSign +import HexInterval.Experiment.ProofFrontend +import Mathlib.Lean.Elab.Tactic.Meta + +/-! +# Exponential package and generic frontend conformance + +This is the second mathematical-function client of the interval framework. +It uses a different fact type, no instantiation, no equality transport, and an +unconditional `Real.exp` propagator. The same joint package registry, +chronology quotation, structural encoder, and dependent proof fold produce an +ordinary kernel-checked theorem. +-/ + +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 + +def offer? (session : PolicySession.Session Bound) + (accepts : Propagator.Policy.OfferView → Bool) : + Option + (Propagator.Policy.OfferView × Propagator.Policy.Selection × + PolicySession.Session Bound) := + match session.view with + | .ready view viewed => + match view.offers.toList.find? accepts with + | none => none + | some offer => + some + (offer, + { scope := view.scope + serial := view.serial + programVersion := view.programVersion + id := offer.id + expected := offer.key }, + viewed) + | .resource _ _ | .contradiction _ | .invalidSession _ => none + +def invokesExp (offer : Propagator.Policy.OfferView) : Bool := + match offer.key with + | .invoke invocation => + invocation.rule == expRuleKey && invocation.anchor == node 1 + | _ => false + +def contracted? : Option (PolicySession.Session Bound) := do + let .ok session := start | none + let (_, selection, viewed) ← offer? session invokesExp + match viewed.choose (.select selection) with + | .rule _ observation next => + if observation.outcome == .success then some next else none + | _ => none + +#guard + contracted?.any fun session => + session.live && !session.droppedWork && + session.state.engine.program == program && + session.state.engine.facts[1]? == some .nonnegative && + session.state.engine.history.size == 1 && + session.state.engine.instanceHistory.isEmpty && + session.state.engine.equalities.isEmpty && + session.state.engine.chronology == #[.fact 0] + +structure Fixture where + session : PolicySession.Session Bound + registry : ProofRegistry.Registry semantics Lean.Name + +def fixture? : Option Fixture := do + let session ← contracted? + match ProofRegistry.build session.registry proofPackages with + | .ok registry => some { session, registry } + | .error _ => none + +#guard + fixture?.any fun fixture => + fixture.registry.emit.find? expFactSchema.key == some ``expFactSchema + +def trace? : Option (Frontend.Trace Bound) := do + match fixture? with + | none => none + | some fixture => + Frontend.trace? fixture.session.state.engine fixture.session.arena + +#guard + trace?.any fun trace => + trace.program == program && + match trace.events with + | [.rule step] => + step.entry.replayKey == expFactSchema.key && + step.event.node == node 1 && + step.event.fact == .nonnegative + | _ => false + +private def boundExpr : Bound → Expr + | .all => mkConst ``Bound.all + | .nonnegative => mkConst ``Bound.nonnegative + | .empty => mkConst ``Bound.empty + +private def seedAssumed (graph : Program) (base : List (NodeFact Bound)) + (index : Nat) (fact : NodeFact Bound) (found : base[index]? = some fact) : + Evidence (semantics.Entails graph base fact) := + ProofEmitter.assumedAt graph base index fact found + +private def frontendContext : ProofFrontend.Context Bound Name := + { encoder := FrontendEncoder.make (mkConst ``Bound) + (fun fact => pure (boundExpr fact)) + resolveSchema := pure + semantics := mkConst ``semantics + domain := mkConst ``boundSchema + laws := mkConst ``laws + stableLaw := mkConst ``stableLaw + input := mkConst ``checkerInput + assumed := ``seedAssumed + baseFacts + baseFactsTerm := mkConst ``baseFacts + baseProgram := program + baseProgramTerm := mkConst ``program + basePrefix := mkConst ``basePrefix + baseWithin := mkConst ``baseWithin + initialExtension := mkConst ``initialExtension + finalPrefix := mkConst ``basePrefix + sameOperations := mkConst ``sameOperations + top := boundSchema.top } + +private meta def emitEvidence : MetaM Expr := do + let some fixture := fixture? + | throwError "interval_exp: compiled search or proof registry failed" + let some trace := Frontend.trace? fixture.session.state.engine fixture.session.arena + | throwError "interval_exp: chronology quotation failed" + let state ← ProofFrontend.emitTrace frontendContext trace.program trace.events + fixture.registry.emit + let target := { node := node 1, version := 1 : SeenVersion } + let some proof := ProofFrontend.findProof? state.known target .nonnegative + | throwError "interval_exp: target fact was not emitted" + pure proof + +private def expTarget (x : ℝ) : Prop := + 0 ≤ Real.exp x + +private meta def proveExp (target : Expr) : MetaM Expr := do + let context ← getLCtx + for declaration in context do + unless declaration.isImplementationDetail do + let saved ← saveState + let candidate? ← observing? <| + mkAppM ``expTarget #[mkFVar declaration.fvarId] + match candidate? with + | some candidate => + if ← isDefEq candidate target then + let evidence ← emitEvidence + let proof ← + mkAppM ``closeExp #[mkFVar declaration.fvarId, evidence] + unless ← isDefEq (← inferType proof) target do + throwError "interval_exp: emitted replay has the wrong target" + return (← instantiateMVars proof) + saved.restore + | none => saved.restore + throwError "interval_exp: expected a goal definitionally equal to `0 ≤ Real.exp x`" + +syntax (name := intervalExpTac) "interval_exp" : tactic + +@[tactic intervalExpTac] meta def evalIntervalExp : Tactic := fun stx => do + match stx with + | `(tactic| interval_exp) => + let goal ← getMainGoal + goal.withContext do + let proof ← proveExp (← instantiateMVars (← goal.getType)) + goal.assign proof + replaceMainGoal [] + | _ => throwUnsupportedSyntax + +theorem tacticExp (x : ℝ) : 0 ≤ Real.exp x := by + interval_exp + +example (_x : ℝ) : True := by + fail_if_success interval_exp + trivial + +set_option linter.unusedTactic false in +example : True := by + run_tac + let some fixture := fixture? + | throwError "interval_exp test: missing live fixture" + let some trace := Frontend.trace? fixture.session.state.engine fixture.session.arena + | throwError "interval_exp test: missing trace" + let [.rule step] := trace.events + | throwError "interval_exp test: wrong event shape" + let stale : RuleStep Bound := + { step with event := { step.event with programVersion := 1 } } + if (← observing? (ProofFrontend.emitTrace frontendContext program + [.rule stale] fixture.registry.emit)).isSome then + throwError "interval_exp test: stale rule version was accepted" + trivial + +end Hex.IntervalMathlib.ExpSignConformance diff --git a/conformance/HexIntervalMathlib/SineTacticConformance.lean b/conformance/HexIntervalMathlib/SineTacticConformance.lean index e6126a94c..6d145fae3 100644 --- a/conformance/HexIntervalMathlib/SineTacticConformance.lean +++ b/conformance/HexIntervalMathlib/SineTacticConformance.lean @@ -126,130 +126,6 @@ private def liveQuotes? : Option LiveQuotes := do (Frontend.quote? engine session.arena [.instance 0, .fact 0, .fact 1] 0 0).isNone -private def listExpr (type : Expr) (items : List Expr) : Expr := - items.foldr - (fun item tail => - mkApp3 (mkConst ``List.cons [Level.zero]) type item tail) - (mkApp (mkConst ``List.nil [Level.zero]) type) - -private def natOptionExpr : Option Nat -> Expr - | none => mkApp (mkConst ``Option.none [Level.zero]) (mkConst ``Nat) - | some value => - mkApp2 (mkConst ``Option.some [Level.zero]) (mkConst ``Nat) (mkNatLit value) - -private meta def nodeExpr (node : NodeId) : MetaM Expr := - do mkAppM ``NodeId.mk #[mkNatLit node.index] - -private meta def domainExpr (domain : DomainId) : MetaM Expr := - do mkAppM ``DomainId.mk #[mkNatLit domain.index] - -private meta def opExpr (operation : OpId) : MetaM Expr := - do mkAppM ``OpId.mk #[mkNatLit operation.index] - -private meta def opKeyExpr (key : OpKey) : MetaM Expr := - do mkAppM ``OpKey.mk #[toExpr key.name, mkNatLit key.version] - -private meta def operationExpr (operation : Operation) : MetaM Expr := do - mkAppM ``Operation.mk - #[← opKeyExpr operation.key, - listExpr (mkConst ``DomainId) (← operation.inputs.mapM domainExpr), - ← domainExpr operation.output] - -private meta def instructionExpr (instruction : Node) : MetaM Expr := do - mkAppM ``Node.mk - #[← domainExpr instruction.domain, - ← opExpr instruction.op, - listExpr (mkConst ``NodeId) (← instruction.args.mapM nodeExpr)] - -private meta def arrayExpr (type : Expr) (items : List Expr) : MetaM Expr := - mkAppM ``Array.mk #[listExpr type items] - -private meta def programExpr (program : Program) : MetaM Expr := do - mkAppM ``Program.mk - #[← arrayExpr (mkConst ``Operation) - (← program.operations.toList.mapM operationExpr), - ← arrayExpr (mkConst ``Node) - (← program.nodes.toList.mapM instructionExpr)] - -private meta def ruleKeyExpr (key : RuleKey) : MetaM Expr := - do mkAppM ``RuleKey.mk #[toExpr key.name, mkNatLit key.schema] - -private meta def ruleExpr (rule : RuleId) : MetaM Expr := - do mkAppM ``RuleId.mk #[mkNatLit rule.index] - -private meta def applicationExpr (application : ApplicationId) : MetaM Expr := - do mkAppM ``ApplicationId.mk #[mkNatLit application.index] - -private meta def equalityExpr (equality : EqualityId) : MetaM Expr := - do mkAppM ``EqualityId.mk #[mkNatLit equality.index] - -private meta def payloadExpr (payload : PayloadId) : MetaM Expr := - do mkAppM ``PayloadId.mk #[mkNatLit payload.index] - -private def actionKindExpr : ActionKind -> Expr - | .forward => mkConst ``ActionKind.forward - | .backward => mkConst ``ActionKind.backward - | .improve => mkConst ``ActionKind.improve - | .shave => mkConst ``ActionKind.shave - | .instantiate => mkConst ``ActionKind.instantiate - | .rewrite => mkConst ``ActionKind.rewrite - | .regularize => mkConst ``ActionKind.regularize - | .split => mkConst ``ActionKind.split - -private meta def seenExpr (seen : SeenVersion) : MetaM Expr := - do mkAppM ``SeenVersion.mk #[← nodeExpr seen.node, mkNatLit seen.version] - -private meta def structuralKeyExpr : StructuralKey -> MetaM Expr - | .node node => do mkAppM ``StructuralKey.node #[← nodeExpr node] - | .equality equality => - do mkAppM ``StructuralKey.equality #[← equalityExpr equality] - | .application application => - do mkAppM ``StructuralKey.application #[← applicationExpr application] - -private meta def structuralInputExpr (input : StructuralInput) : MetaM Expr := - do - mkAppM ``StructuralInput.mk - #[← structuralKeyExpr input.key, mkNatLit input.generation] - -private meta def scopeExpr (binding : ScopeBinding) : MetaM Expr := - do - mkAppM ``ScopeBinding.mk - #[← ruleKeyExpr binding.rule, - ← nodeExpr binding.anchor, - listExpr (mkConst ``NodeId) (← binding.watches.mapM nodeExpr), - listExpr (mkConst ``NodeId) (← binding.writes.mapM nodeExpr)] - -private meta def actionExpr (action : Action) : MetaM Expr := - do - mkAppM ``Action.mk - #[mkNatLit action.serial, - mkNatLit action.programVersion, - ← applicationExpr action.application, - ← ruleExpr action.rule, - ← ruleKeyExpr action.key, - ← nodeExpr action.node, - actionKindExpr action.kind, - mkNatLit action.effort, - mkNatLit action.generation, - listExpr (mkConst ``SeenVersion) (← action.inputs.mapM seenExpr), - listExpr (mkConst ``NodeId) (← action.writes.mapM nodeExpr), - listExpr (mkConst ``StructuralInput) - (← action.structuralInputs.mapM structuralInputExpr), - natOptionExpr action.matcherEpoch] - -private def roleExpr : Role -> Expr - | .fact => mkConst ``Role.fact - | .instance => mkConst ``Role.instance - | .equality => mkConst ``Role.equality - -private meta def entryExpr (entry : Entry) : MetaM Expr := - do - mkAppM ``Entry.mk - #[← actionExpr entry.origin, - roleExpr entry.role, - mkNatLit entry.schema, - listExpr (mkConst ``Nat) (entry.body.map mkNatLit)] - private def rangeExpr : Range -> Expr | .all => mkConst ``Range.all | .unit => mkConst ``Range.unit @@ -258,88 +134,10 @@ private def rangeExpr : Range -> Expr | .zero => mkConst ``Range.zero | .empty => mkConst ``Range.empty -private meta def factCauseExpr : FactCause Range -> MetaM Expr - | .rule action proposed payload => - do - mkAppM ``FactCause.rule - #[← actionExpr action, rangeExpr proposed, ← payloadExpr payload] - | .transport equality source => - do - let equalityTerm <- equalityExpr equality - let sourceTerm <- seenExpr source - pure <| - mkApp3 (mkConst ``FactCause.transport) (mkConst ``Range) - equalityTerm sourceTerm - -private meta def factEventExpr (event : FactEvent Range) : MetaM Expr := - do - mkAppM ``FactEvent.mk - #[mkNatLit event.programVersion, - ← nodeExpr event.node, - ← seenExpr event.previous, - rangeExpr event.fact, - mkNatLit event.version, - ← factCauseExpr event.cause] - -private meta def nodeFactExpr (fact : NodeFact Range) : MetaM Expr := - do mkAppM ``NodeFact.mk #[← nodeExpr fact.node, rangeExpr fact.fact] - -private meta def edgeExpr (edge : EqualityEdge) : MetaM Expr := - do - mkAppM ``EqualityEdge.mk - #[← nodeExpr edge.left, - ← nodeExpr edge.right, - mkNatLit edge.generation, - ← actionExpr edge.origin, - ← payloadExpr edge.payload] - -private meta def instanceEventExpr (event : InstanceEvent) : MetaM Expr := - do - mkAppM ``InstanceEvent.mk - #[mkNatLit event.programVersion, - ← actionExpr event.origin, - mkNatLit event.family, - listExpr (mkConst ``NodeId) (← event.substitution.mapM nodeExpr), - listExpr (mkConst ``NodeId) (← event.products.mapM nodeExpr), - listExpr (mkConst ``NodeId) (← event.newNodes.mapM nodeExpr), - listExpr (mkConst ``ScopeBinding) (← event.bindings.mapM scopeExpr), - listExpr (mkConst ``ScopeBinding) (← event.newBindings.mapM scopeExpr), - listExpr (mkConst ``ApplicationId) (← event.applications.mapM applicationExpr), - listExpr (mkConst ``ApplicationId) (← event.newApplications.mapM applicationExpr), - mkNatLit event.generation, - listExpr (mkConst ``EqualityId) (← event.equalities.mapM equalityExpr), - listExpr (mkConst ``EqualityId) (← event.newEqualities.mapM equalityExpr), - ← payloadExpr event.payload] - -private meta def instanceQuoteExpr (quote : InstanceQuote) : MetaM Expr := - do - mkAppM ``InstanceQuote.mk - #[← instanceEventExpr quote.event, - ← payloadExpr quote.payload, - ← entryExpr quote.entry] - -private meta def ruleStepExpr (step : RuleStep Range) : MetaM Expr := - do - let factType <- mkAppM ``NodeFact #[mkConst ``Range] - mkAppM ``RuleStep.mk - #[← factEventExpr step.event, - ← payloadExpr step.payload, - ← entryExpr step.entry, - listExpr factType (← step.assumptions.mapM nodeFactExpr), - rangeExpr step.previous] - -private meta def transportStepExpr (step : TransportStep Range) : MetaM Expr := - do - let factType <- mkAppM ``NodeFact #[mkConst ``Range] - mkAppM ``TransportStep.mk - #[← factEventExpr step.event, - ← equalityExpr step.equality, - ← edgeExpr step.edge, - ← payloadExpr step.payload, - ← entryExpr step.entry, - listExpr factType (← step.assumptions.mapM nodeFactExpr), - rangeExpr step.previous, - rangeExpr step.sourceFact] +/-- The one structural encoder used by both quotation regression and proof +emission. -/ +private def frontendEncoder : FrontendEncoder.Encoder Range := + FrontendEncoder.make (mkConst ``Range) (fun fact => pure (rangeExpr fact)) private meta def checkQuote (label : String) (actual expected : Expr) : MetaM Unit := do unless <- isDefEq actual expected do @@ -367,12 +165,15 @@ private meta def checkQuoteData (quote : LiveQuotes) : MetaM Unit := do checkSchema table "negation rule" quote.negation.entry ``negationFactSchema checkSchema table "equality transport" quote.transport.entry ``oddnessEqualitySchema - checkQuote "instantiation" (← instanceQuoteExpr quote.instantiation) + checkQuote "instantiation" + (← frontendEncoder.instanceQuote quote.instantiation) (mkConst ``instanceQuote) - checkQuote "sine rule" (← ruleStepExpr quote.sine) (mkConst ``sineStep) - checkQuote "negation rule" (← ruleStepExpr quote.negation) + checkQuote "sine rule" (← frontendEncoder.ruleStep quote.sine) + (mkConst ``sineStep) + checkQuote "negation rule" (← frontendEncoder.ruleStep quote.negation) (mkConst ``negationStep) - checkQuote "equality transport" (← transportStepExpr quote.transport) + checkQuote "equality transport" + (← frontendEncoder.transportStep quote.transport) (mkConst ``transportStep) /-- Specialize generic caller-assumption seeding to this semantics adapter; @@ -384,15 +185,7 @@ private def seedAssumed (program : Program) (base : List (NodeFact Range)) /-- 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 } + { encoder := frontendEncoder resolveSchema := pure semantics := mkConst ``semantics domain := mkConst ``rangeSchema diff --git a/lakefile.lean b/lakefile.lean index ad632dd23..b71eea886 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -312,13 +312,16 @@ lean_lib HexIntervalExperiment where `HexInterval.Experiment.ProofEmitter, `HexInterval.Experiment.ProofRegistry, `HexInterval.Experiment.Frontend, + `HexInterval.Experiment.FrontendEncoder, `HexInterval.Experiment.ProofFrontend, `HexInterval.Experiment.TraceReplay, - `HexInterval.Experiment.SineSign] + `HexInterval.Experiment.SineSign, + `HexInterval.Experiment.ExpSign] lean_lib HexIntervalMathlibExperiment where globs := #[`HexIntervalMathlib.Experiment.Center, - `HexIntervalMathlib.Experiment.SineSign] + `HexIntervalMathlib.Experiment.SineSign, + `HexIntervalMathlib.Experiment.ExpSign] lean_lib HexIntervalReplayProbe where srcDir := "bench" @@ -382,7 +385,7 @@ lean_lib HexRCFProofProbeScientific where -- `*_emit_fixtures` exes below, carrying `srcDir := "conformance"`. lean_lib HexConformance where srcDir := "conformance" - globs := #[`HexArith.Conformance, `HexArith.CrossCheck, `HexBerlekamp.Conformance, `HexBerlekampZassenhaus.Conformance, `HexBerlekampZassenhaus.CrossCheck, `HexConway.Conformance, `HexGF2.Conformance, `HexGF2.CrossCheck, `HexGF2.FastCheck, `HexGFq.Conformance, `HexGFq.CrossCheck, `HexGFqField.Conformance, `HexGFqRing.Conformance, `HexGramSchmidt.Conformance, `HexHensel.Conformance, `HexHensel.CrossCheck, `HexInterval.Conformance, `HexInterval.CenterConformance, `HexInterval.ScaleConformance, `HexInterval.PropagatorConformance, `HexInterval.ScopeConformance, `HexInterval.StructuralMatcherConformance, `HexInterval.MatcherSchedulerConformance, `HexInterval.StructureViewConformance, `HexInterval.PolicyConformance, `HexInterval.PolicyFrontierConformance, `HexInterval.PolicyDriverConformance, `HexInterval.PackageRegistryConformance, `HexInterval.DyadicIntervalConformance, `HexInterval.DyadicRulesConformance, `HexInterval.PayloadArenaConformance, `HexInterval.PayloadSessionConformance, `HexInterval.PolicySessionConformance, `HexInterval.PolicyFunctionConformance, `HexInterval.SemanticReplayConformance, `HexInterval.ChronologicalReplayConformance, `HexInterval.GenericInstanceReconstructionConformance, `HexInterval.ProofEmitterConformance, `HexInterval.TraceReplayConformance, `HexIntervalMathlib.SineSignConformance, `HexIntervalMathlib.SineProofConformance, `HexIntervalMathlib.SineTacticConformance, `HexIntervalMathlib.ProofRegistryConformance, `HexLLL.Conformance, `HexMatrix.Conformance, `HexMvPolyFixtures, `HexMvPoly.Conformance, `HexMvPolyMathlib.Conformance, `HexRowReduce.Conformance, `HexDeterminant.Conformance, `HexBareiss.Conformance, `HexModArith.Conformance, `HexModArith.FastCheck, `HexNumberField.Conformance, `HexNumberFieldTower.Conformance, `HexPoly.Conformance, `HexPolyFp.Conformance, `HexPolyZ.Conformance, `HexRCF.Conformance, `HexRealRoots.Conformance, `HexRealRootsMathlib.Conformance, `HexResultant.Conformance, `HexRoots.Conformance].map Glob.one + globs := #[`HexArith.Conformance, `HexArith.CrossCheck, `HexBerlekamp.Conformance, `HexBerlekampZassenhaus.Conformance, `HexBerlekampZassenhaus.CrossCheck, `HexConway.Conformance, `HexGF2.Conformance, `HexGF2.CrossCheck, `HexGF2.FastCheck, `HexGFq.Conformance, `HexGFq.CrossCheck, `HexGFqField.Conformance, `HexGFqRing.Conformance, `HexGramSchmidt.Conformance, `HexHensel.Conformance, `HexHensel.CrossCheck, `HexInterval.Conformance, `HexInterval.CenterConformance, `HexInterval.ScaleConformance, `HexInterval.PropagatorConformance, `HexInterval.ScopeConformance, `HexInterval.StructuralMatcherConformance, `HexInterval.MatcherSchedulerConformance, `HexInterval.StructureViewConformance, `HexInterval.PolicyConformance, `HexInterval.PolicyFrontierConformance, `HexInterval.PolicyDriverConformance, `HexInterval.PackageRegistryConformance, `HexInterval.DyadicIntervalConformance, `HexInterval.DyadicRulesConformance, `HexInterval.PayloadArenaConformance, `HexInterval.PayloadSessionConformance, `HexInterval.PolicySessionConformance, `HexInterval.PolicyFunctionConformance, `HexInterval.SemanticReplayConformance, `HexInterval.ChronologicalReplayConformance, `HexInterval.GenericInstanceReconstructionConformance, `HexInterval.ProofEmitterConformance, `HexInterval.TraceReplayConformance, `HexIntervalMathlib.SineSignConformance, `HexIntervalMathlib.SineProofConformance, `HexIntervalMathlib.SineTacticConformance, `HexIntervalMathlib.ProofRegistryConformance, `HexIntervalMathlib.ExpSignConformance, `HexLLL.Conformance, `HexMatrix.Conformance, `HexMvPolyFixtures, `HexMvPoly.Conformance, `HexMvPolyMathlib.Conformance, `HexRowReduce.Conformance, `HexDeterminant.Conformance, `HexBareiss.Conformance, `HexModArith.Conformance, `HexModArith.FastCheck, `HexNumberField.Conformance, `HexNumberFieldTower.Conformance, `HexPoly.Conformance, `HexPolyFp.Conformance, `HexPolyZ.Conformance, `HexRCF.Conformance, `HexRealRoots.Conformance, `HexRealRootsMathlib.Conformance, `HexResultant.Conformance, `HexRoots.Conformance].map Glob.one -- Public umbrellas intentionally contain only the supported API. Executable -- examples and regression tests are compiled through this separate target so diff --git a/progress/20260811T120328Z.md b/progress/20260811T120328Z.md new file mode 100644 index 000000000..b86b39014 --- /dev/null +++ b/progress/20260811T120328Z.md @@ -0,0 +1,31 @@ +# Accomplished + +- Extracted a shared Mathlib-free Lean encoder for all structural program, + action, payload, and proof-event data; fact domains now supply only their + fact-value encoding. +- Added an independent Mathlib-free exponential package with a distinct fact + lattice and unconditional nonnegativity propagator. +- Added the real `Real.exp` semantics, semantic replay schema, and joint proof + package in the Mathlib companion. +- Ran the live exponential rule through the policy session, chronology + quotation, shared encoder, and generic evidence fold to produce the ordinary + theorem `0 ≤ Real.exp x`. +- Added runtime chronology/package checks and a stale-version rejection test. +- Updated the SPEC and passed the focused 1,964-target build and all structural + checks. + +# Current frontier + +Two materially different functions now use the same package-driven frontend: +sine exercises matcher-triggered graph growth, independent propagators, and +equality transport; exponential exercises a different fact representation and +a single unconditional rule. + +# Next step + +Construct the caller program, initial facts, semantic adapter selection, and +target from the tactic goal instead of supplying fixed canary constants. + +# Blockers + +None. diff --git a/progress/20260811T121755Z.md b/progress/20260811T121755Z.md new file mode 100644 index 000000000..4eb504263 --- /dev/null +++ b/progress/20260811T121755Z.md @@ -0,0 +1,23 @@ +# Exponential vertical frontend reconciliation + +## Accomplished + +- Merged the Handle-polymorphic generic proof frontend into the independent + `Real.exp` validation branch. +- Kept sine and exponential frontends on the shared structural encoder while + resolving their schema handles at the Mathlib elaboration boundary. +- Rebuilt both the real-sine tactic and real-exponential conformance targets. + +## Current frontier + +The same function-independent chronology and evidence fold now serves two +unrelated mathematical packages and two fact representations. + +## Next step + +Push the reconciled exponential PR and obtain a fresh exact-head review after +its updated stacked base is green. + +## Blockers + +None. diff --git a/progress/20260811T123329Z.md b/progress/20260811T123329Z.md new file mode 100644 index 000000000..4c1a4e0c7 --- /dev/null +++ b/progress/20260811T123329Z.md @@ -0,0 +1,26 @@ +# Real-function frontend review repairs + +## Accomplished + +- Routed the sine literal-quotation regression and live proof emitter through + the same shared structural encoder. +- Changed the exponential tactic to perform its cheap goal-shape probe first, + then run search and proof emission exactly once outside error-suppressing + backtracking. +- Derived the exponential frontend top value from its fact-domain schema and + narrowed the semantic companion imports to its actual dependencies. + +## Current frontier + +The independent sine and exponential clients now exercise one encoder and +propagate planner/schema diagnostics instead of relabeling them as goal-shape +failures. + +## Next step + +Push the repaired exact PR head, obtain a fresh second opinion, and merge the +repair into the stacked goal-reification experiment. + +## Blockers + +None. diff --git a/progress/20260811T161940Z.md b/progress/20260811T161940Z.md new file mode 100644 index 000000000..4a062918d --- /dev/null +++ b/progress/20260811T161940Z.md @@ -0,0 +1,26 @@ +# Accomplished + +- Reconciled the independent exponential-function vertical with the current + generic frontend, joint package registry, and repeated-instantiation stack. +- Preserved a distinct Mathlib-free fact lattice and propagator plus its + package-owned real semantic replay theorem, with no exponential case in the + shared frontend. +- Repaired the exponential semantics adapter to use the strengthened + whole-prefix agreement law, matching the sine adapter. +- Refreshed the exact Lake registration exemption and rebuilt both the sine + and exponential tactic conformance targets successfully. + +# Current frontier + +Two structurally different real functions now use the same generic package, +quotation, evidence-fold, and kernel proof-emission APIs. Caller expression +reification and dynamic target closure remain the next generalization. + +# Next step + +Push the reconciled exact head for independent review, then reconcile the +generic goal reifier and dynamic goal-closing layers. + +# Blockers + +None. diff --git a/progress/20260811T163751Z.md b/progress/20260811T163751Z.md new file mode 100644 index 000000000..44c03f4a5 --- /dev/null +++ b/progress/20260811T163751Z.md @@ -0,0 +1,22 @@ +# Accomplished + +- Propagated the reconciled generic frontend, selected-schema trust wording, + joint registry invariant, and guarded sine axiom report into the independent + `Real.exp` vertical. +- Preserved separate exponential runtime and semantic packages using the same + function-agnostic frontend as sine. + +# Current frontier + +Sine and exponential propagation exercise one common proof frontend. Their +function-specific content remains confined to package-owned operations, +propagators, semantic schemas, and theorems. + +# Next step + +Finish focused and static checks, push this exact head for review, then +propagate the stack into reification of arbitrary supported Lean goal graphs. + +# Blockers + +None. diff --git a/scripts/bench/proof_only_runtime_exemptions.json b/scripts/bench/proof_only_runtime_exemptions.json index 327ec7c0e..f91eb2d99 100644 --- a/scripts/bench/proof_only_runtime_exemptions.json +++ b/scripts/bench/proof_only_runtime_exemptions.json @@ -101,6 +101,12 @@ "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": "lakefile.lean", + "baseline_blob": "6dd80771ae2212333b2a9b925b52056e0037ff56", + "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": "HexBerlekamp/FactorTacticTests.lean", "baseline_blob": "4063e15934a89c671ac72d201fa60c2ef6feaf59",