From 9f0b52eb6fc03823c99855de375ea8ab7173ee03 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 11 Aug 2026 17:20:03 +0000 Subject: [PATCH] Propagate provenance honesty through operation semantics; progress 20260811T171522Z --- .../Experiment/OperationSemantics.lean | 81 +++++++++++ HexInterval/SPEC/hex-interval.md | 27 ++++ HexIntervalMathlib/Experiment/ExpSign.lean | 130 +++++++++++------- .../ExpSignConformance.lean | 80 +++++++++++ lakefile.lean | 1 + progress/20260811T130144Z.md | 26 ++++ progress/20260811T130656Z.md | 22 +++ progress/20260811T132310Z.md | 22 +++ progress/20260811T162526Z.md | 26 ++++ progress/20260811T163944Z.md | 23 ++++ .../bench/proof_only_runtime_exemptions.json | 6 + 11 files changed, 396 insertions(+), 48 deletions(-) create mode 100644 HexInterval/Experiment/OperationSemantics.lean create mode 100644 progress/20260811T130144Z.md create mode 100644 progress/20260811T130656Z.md create mode 100644 progress/20260811T132310Z.md create mode 100644 progress/20260811T162526Z.md create mode 100644 progress/20260811T163944Z.md diff --git a/HexInterval/Experiment/OperationSemantics.lean b/HexInterval/Experiment/OperationSemantics.lean new file mode 100644 index 000000000..655f55861 --- /dev/null +++ b/HexInterval/Experiment/OperationSemantics.lean @@ -0,0 +1,81 @@ +/- +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.GenericInstanceReconstruction + +@[expose] public section + +/-! +# Package-composed operation semantics + +This experiment interprets an expression program without a central switch on +operation keys. Each package contributes its opaque operation signature and a +relation between argument values and the result value. A program model must +find the relation at every referenced operation index; missing meanings do not +make a node unconstrained. +-/ + +namespace Hex.Interval.Experiment.OperationSemantics + +open Propagator SemanticReplay ChronologicalReplay +open GenericInstanceReconstruction + +/-- The mathematical meaning contributed by one operation package. -/ +structure Model (Value : Type) where + operation : Operation + relation : List Value → Value → Prop + +/-- Every operation and node in a program is interpreted by the aligned model +array. The exact operation-array equality prevents a meaning from being paired +with a different opaque operation signature. -/ +def Models (models : Array (Model Value)) (program : Program) + (valuation : NodeId → Value) : Prop := + program.operations = models.map (fun model => model.operation) ∧ + ∀ node instruction, program.node? node = some instruction → + ∃ model, + models[instruction.op.index]? = some model ∧ + model.relation (instruction.args.map valuation) (valuation node) + +/-- Node-local fact semantics over a package-composed operation model. -/ +def semantics (models : Array (Model Value)) + (Contains : Fact → Value → Prop) : Semantics Fact := + { Value + models := Models models + holds := fun _ valuation fact => Contains fact.fact (valuation fact.node) } + +theorem nodeAt {before after : Program} + (step : ProgramPrefix before after) (node : NodeId) + (instruction : Node) (found : before.node? node = some instruction) : + after.node? node = some instruction := by + have within : node.index < before.nodes.size := by + by_cases inside : node.index < before.nodes.size + · exact inside + · simp [Program.node?, inside] at found + rw [Program.node?, step.nodeAt node.index within] + exact found + +/-- Node-local meanings satisfy one uniform append-only stability law. -/ +def stableLaw (models : Array (Model Value)) + (Contains : Fact → Value → Prop) : + StableLaw (semantics models Contains) := + { stable := by + intro before after _ _ step sameOperations + refine + { programPrefix := step + modelsBefore := ?_ + holdsOld := ?_ } + · intro valuation model + refine ⟨sameOperations.trans model.1, ?_⟩ + intro node instruction found + exact model.2 node instruction (nodeAt step node instruction 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] } + +end Hex.Interval.Experiment.OperationSemantics diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index 2e7f7a5f0..4256440fa 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -1395,6 +1395,33 @@ semantics and generic proof emission for the recorded top/assumption seed recipes; it remains the next frontend experiment rather than an assumed capability. +The first package-composed semantics experiment removes a second fixed-graph +assumption. An operation-meaning package supplies an opaque operation signature +and a relation from its ordered input values to its result value. The assembled +model requires the program's operation array to equal the aligned package +array and requires a successful meaning lookup for every node; an absent or +mismatched package therefore cannot make an expression unconstrained. This +makes full package alignment a proof-production obligation, not merely a +registry convenience: until the frontend supplies that equality and a meaning +proof for every node, `Models` may be uninhabited and an `Entails` theorem by +itself may be vacuous. Appending or reordering syntax packages therefore also +requires assembling the correspondingly aligned meaning array. This +node-local semantics supplies one generic append-only stability law. The +exponential companion now assembles independent source and exponential +meanings, and its positivity schema checks an arbitrary proposed node's +instruction, the exponential package's current operation slot, and unary +argument before proving the result. Key-resolved lookup replaces that +canary-specific numeric slot before packages may be reordered. A +three-node `exp (exp x)` canary obtains an ordinary theorem through that schema, +while applying it to the source node fails closed. The remaining frontend gap +is a kernel-checked link from each syntax recognizer to its operation relation, +followed by generic discharge of the reifier's top and ordered-assumption seed +recipes. A recognizer match alone is never treated as semantic evidence. +This first adapter uses one semantic value type for all domains. A later +multi-domain adapter must choose and validate a tagged universal value or a +domain-indexed valuation rather than pretending heterogeneous values have one +untyped representation. + 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 expected interleaving before it reads historical values through diff --git a/HexIntervalMathlib/Experiment/ExpSign.lean b/HexIntervalMathlib/Experiment/ExpSign.lean index 42cc55f68..f3b80e20a 100644 --- a/HexIntervalMathlib/Experiment/ExpSign.lean +++ b/HexIntervalMathlib/Experiment/ExpSign.lean @@ -9,7 +9,7 @@ module public import Mathlib.Analysis.SpecialFunctions.Exp public import HexInterval.Experiment.ExpSign public import HexInterval.Experiment.ProofRegistry -public import HexInterval.Experiment.GenericInstanceReconstruction +public import HexInterval.Experiment.OperationSemantics @[expose] public section @@ -23,21 +23,29 @@ over `ℝ` and contributes its semantic replay theorem and frontend handle. namespace Hex.Interval.Experiment.ExpSign open Propagator SemanticReplay ChronologicalReplay ProofEmitter ProofRegistry -open GenericInstanceReconstruction +open GenericInstanceReconstruction OperationSemantics 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 sourceModel : OperationSemantics.Model ℝ := + { operation := sourceOperation + relation := fun inputs _ => inputs = [] } + +def expModel : OperationSemantics.Model ℝ := + { operation := expOperation + relation := fun inputs output => + match inputs with + | [input] => output = Real.exp input + | _ => False } + +def operationModels : Array (OperationSemantics.Model ℝ) := + #[sourceModel, expModel] def semantics : Semantics Bound := - { Value := ℝ - models := Models - holds := fun _ valuation fact => Contains fact.fact (valuation fact.node) } + OperationSemantics.semantics operationModels Contains theorem containsMeet (left right : Bound) (x : ℝ) : Contains (left.meet right) x ↔ Contains left x ∧ Contains right x := by @@ -65,14 +73,35 @@ def laws : Laws semantics := 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 +theorem expEntails (graph : Program) (assumptions : List (NodeFact Bound)) + (output : NodeId) (instruction : Node) (input : NodeId) + (found : graph.node? output = some instruction) + (operation : instruction.op = { index := 1 }) + (arguments : instruction.args = [input]) : + semantics.Entails graph assumptions + { node := output, fact := .nonnegative } := by + change ∀ valuation : NodeId → ℝ, + OperationSemantics.Models operationModels graph valuation → + (∀ assumption, assumption ∈ assumptions → + Contains assumption.fact (valuation assumption.node)) → + Contains .nonnegative (valuation output) intro valuation model _ - change (0 : ℝ) ≤ valuation (node 1) - rw [model (by rfl)] + obtain ⟨meaning, meaningAt, related⟩ := + model.2 output instruction found + simp [operationModels, operation] at meaningAt + subst meaning + have outputEq : valuation output = Real.exp (valuation input) := by + simpa [expModel, arguments, List.map] using related + change (0 : ℝ) ≤ valuation output + rw [outputEq] exact (Real.exp_pos _).le +private theorem factWith {Fact : Type} (fact : NodeFact Fact) {value : Fact} + (equal : fact.fact = value) : + fact = { node := fact.node, fact := value } := by + cases fact + simp_all + def expFactSchema : PackedFactSchema semantics where rule := expRuleKey schema := 1 @@ -80,42 +109,33 @@ def expFactSchema : PackedFactSchema semantics where 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 + if proposedFact : context.proposed.fact = .nonnegative then + match found : context.program.node? context.proposed.node with + | some instruction => + if operation : instruction.op = ({ index := 1 } : OpId) then + match arguments : instruction.args with + | [input] => + some + { proof := by + have proposedEq : + context.proposed = + { node := context.proposed.node, + fact := .nonnegative } := by + exact factWith context.proposed proposedFact + rw [proposedEq] + exact + expEntails context.program context.assumptions + context.proposed.node instruction input found + operation arguments } + | _ => none + else + none + | none => 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] } + OperationSemantics.stableLaw operationModels Contains def sourceEmit : EmitPackage Lean.Name := { schemas := [] } @@ -164,9 +184,23 @@ noncomputable def valuation (x : ℝ) : NodeId → ℝ | ⟨1⟩ => Real.exp x | _ => 0 -theorem valuationModels (x : ℝ) : Models program (valuation x) := by - intro _ - rfl +theorem valuationModels (x : ℝ) : semantics.models program (valuation x) := by + refine ⟨?_, ?_⟩ + · simp [program, operations, operationModels, sourceModel, expModel] + rintro ⟨index⟩ instruction found + cases index with + | zero => + simp [Program.node?, program, sourceInstruction] at found + subst instruction + exact ⟨sourceModel, by rfl, by rfl⟩ + | succ index => + cases index with + | zero => + simp [Program.node?, program, expInstruction] at found + subst instruction + exact ⟨expModel, by rfl, by rfl⟩ + | succ index => + simp [Program.node?, program] at found /-- Turn the generic emitted evidence into the ordinary user theorem. -/ theorem closeExp (x : ℝ) diff --git a/conformance/HexIntervalMathlib/ExpSignConformance.lean b/conformance/HexIntervalMathlib/ExpSignConformance.lean index 8a6678e9c..a089925a7 100644 --- a/conformance/HexIntervalMathlib/ExpSignConformance.lean +++ b/conformance/HexIntervalMathlib/ExpSignConformance.lean @@ -184,6 +184,86 @@ def trace? : Option (Frontend.Trace Bound) := do step.event.fact == .nonnegative | _ => false +/-! ## Operation-composed semantics at an arbitrary graph node -/ + +private def nestedInstruction : Node := + { domain := real, op := { index := 1 }, args := [node 1] } + +private def nestedProgram : Program := + { operations, nodes := #[sourceInstruction, expInstruction, nestedInstruction] } + +private def nestedInput : CheckerInput Bound := + { baseProgram := nestedProgram + initialFacts := #[.all, .all, .all] + target := { node := node 2, fact := .nonnegative } } + +private def nestedAction : Action := + { serial := 0 + programVersion := 0 + application := { index := 0 } + rule := { index := 0 } + key := expRuleKey + node := node 2 + kind := .forward + effort := 0 + generation := 0 + inputs := [] + writes := [node 2] } + +private def nestedContext : RuleFactContext nestedInput nestedAction := + { program := nestedProgram + basePrefix := ProgramPrefix.refl nestedProgram + assumptions := [] + proposed := { node := node 2, fact := .nonnegative } } + +#guard (expFactSchema.replay nestedInput nestedAction nestedContext ()).isSome + +private def sourceContext : RuleFactContext nestedInput nestedAction := + { nestedContext with + proposed := { node := node 0, fact := .nonnegative } } + +#guard (expFactSchema.replay nestedInput nestedAction sourceContext ()).isNone + +private def nestedEvidence : Evidence + (semantics.Entails nestedProgram [] nestedInput.target) := + (expFactSchema.replay nestedInput nestedAction nestedContext ()).get (by rfl) + +private noncomputable def nestedValuation (x : ℝ) : NodeId → ℝ + | ⟨0⟩ => x + | ⟨1⟩ => Real.exp x + | ⟨2⟩ => Real.exp (Real.exp x) + | _ => 0 + +private theorem nestedModels (x : ℝ) : + semantics.models nestedProgram (nestedValuation x) := by + refine ⟨?_, ?_⟩ + · simp [nestedProgram, operations, operationModels, sourceModel, expModel] + rintro ⟨index⟩ instruction found + cases index with + | zero => + simp [Program.node?, nestedProgram, sourceInstruction] at found + subst instruction + exact ⟨sourceModel, by rfl, by rfl⟩ + | succ index => + cases index with + | zero => + simp [Program.node?, nestedProgram, expInstruction] at found + subst instruction + exact ⟨expModel, by rfl, by rfl⟩ + | succ index => + cases index with + | zero => + simp [Program.node?, nestedProgram, nestedInstruction] at found + subst instruction + exact ⟨expModel, by rfl, by rfl⟩ + | succ index => + simp [Program.node?, nestedProgram] at found + +theorem nestedExp (x : ℝ) : 0 ≤ Real.exp (Real.exp x) := by + have holds := nestedEvidence.proof (nestedValuation x) (nestedModels x) + (by simp) + exact holds + private def boundExpr : Bound → Expr | .all => mkConst ``Bound.all | .nonnegative => mkConst ``Bound.nonnegative diff --git a/lakefile.lean b/lakefile.lean index 9c1dba3ba..d61f146ae 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -309,6 +309,7 @@ lean_lib HexIntervalExperiment where `HexInterval.Experiment.SemanticReplay, `HexInterval.Experiment.ChronologicalReplay, `HexInterval.Experiment.GenericInstanceReconstruction, + `HexInterval.Experiment.OperationSemantics, `HexInterval.Experiment.ProofEmitter, `HexInterval.Experiment.ProofRegistry, `HexInterval.Experiment.Frontend, diff --git a/progress/20260811T130144Z.md b/progress/20260811T130144Z.md new file mode 100644 index 000000000..ee034eb0d --- /dev/null +++ b/progress/20260811T130144Z.md @@ -0,0 +1,26 @@ +# Package-composed operation semantics + +## Accomplished + +- Added a function-independent semantics whose operation meanings are supplied + as an aligned package array and whose model covers every graph node. +- Derived one generic append-only stability law for node-local facts. +- Replaced the exponential companion's fixed-node model with separate source + and exponential meanings. +- Generalized the positivity schema to inspect and prove any unary exponential + node, with a nested-exponential ordinary theorem and source-node rejection. + +## Current frontier + +The semantic replay schema no longer names the hand-written two-node graph. +The actual-goal frontend still needs kernel-checked syntax-to-relation links and +proof discharge for its ordered version-zero seed recipes. + +## Next step + +Add those package-owned syntax links, construct the node-aligned valuation, +and close the replay result against the user's original proposition. + +## Blockers + +None. diff --git a/progress/20260811T130656Z.md b/progress/20260811T130656Z.md new file mode 100644 index 000000000..c8c52cc1c --- /dev/null +++ b/progress/20260811T130656Z.md @@ -0,0 +1,22 @@ +# Operation semantics reconciliation + +## Accomplished + +- Reconciled package-composed operation semantics with the repaired + optional-hypothesis goal frontend. +- Preserved strict target validation, prefix-only fixture matching, and the + arbitrary-node exponential semantic schema. + +## Current frontier + +Goal construction and operation meaning are now separate generic layers on the +same stacked branch; kernel-checked syntax links and seed discharge remain the +bridge between them. + +## Next step + +Rebuild the combined exact head and obtain fresh second opinions for both PRs. + +## Blockers + +None. diff --git a/progress/20260811T132310Z.md b/progress/20260811T132310Z.md new file mode 100644 index 000000000..8f77994fe --- /dev/null +++ b/progress/20260811T132310Z.md @@ -0,0 +1,22 @@ +# Accomplished + +- Clarified that package-composed semantics is useful for proof production + only after the complete operation table is aligned and every reified node + has a meaning proof. +- Recorded that the current exponential schema's numeric operation slot is a + canary detail which must become key-resolved before package reordering. + +# Current frontier + +The operation semantics and arbitrary-node exponential theorem are complete; +the stacked goal-closure experiment is implementing the required alignment +and node-meaning proof bridge. + +# Next step + +Finish the generic kernel bridge from syntax packages to the aligned operation +model and use it in the live goal frontend. + +# Blockers + +None. diff --git a/progress/20260811T162526Z.md b/progress/20260811T162526Z.md new file mode 100644 index 000000000..7f2026468 --- /dev/null +++ b/progress/20260811T162526Z.md @@ -0,0 +1,26 @@ +# Accomplished + +- Reconciled package-composed operation semantics with the package-driven goal + reifier and independent exponential vertical. +- Preserved exact operation-array alignment, per-node meaning lookup, arbitrary + exponential-node replay, and the explicit warning that an unaligned model + can make semantic entailment vacuous. +- Repaired the generic node-local stability law to use whole-prefix agreement + with the established old-node bound. +- Refreshed the exact Lake registration exemption and rebuilt operation + semantics plus sine and exponential conformance targets successfully. + +# Current frontier + +Every reified operation and node can now receive an aligned package-owned +meaning, but the live goal frontend still needs to construct and kernel-check +that alignment and use it to close an arbitrary target dynamically. + +# Next step + +Push the reconciled exact head for independent review, then reconcile the +generic semantic/proof bridge and target-closing frontend. + +# Blockers + +None. diff --git a/progress/20260811T163944Z.md b/progress/20260811T163944Z.md new file mode 100644 index 000000000..384993622 --- /dev/null +++ b/progress/20260811T163944Z.md @@ -0,0 +1,23 @@ +# Accomplished + +- Propagated the reconciled goal frontend, selected-schema proof boundary, + joint package registry, and guarded sine axiom report into package-composed + operation semantics. +- Preserved whole-prefix stability and the explicit requirement that semantic + meaning arrays align with the reified operation table. + +# Current frontier + +Arbitrary supported goal graphs now have both package-driven reification and +package-composed semantic models. The SPEC remains explicit that misaligned +meaning arrays can make models empty and must never be used to obtain vacuous +proofs. + +# Next step + +Finish checks, push the exact head for review, then reconcile generic target +closure and dynamic policy execution on top of this semantic foundation. + +# Blockers + +None. diff --git a/scripts/bench/proof_only_runtime_exemptions.json b/scripts/bench/proof_only_runtime_exemptions.json index cd991e971..5e90ec9d9 100644 --- a/scripts/bench/proof_only_runtime_exemptions.json +++ b/scripts/bench/proof_only_runtime_exemptions.json @@ -113,6 +113,12 @@ "current_blob": "9c1dba3baec47ca1c222742abb9e0d579fe4e6b5", "reason": "Additionally registers the generic interval goal-reification experiment only; the factorization service target and executable dependency graph are unchanged." }, + { + "path": "lakefile.lean", + "baseline_blob": "6dd80771ae2212333b2a9b925b52056e0037ff56", + "current_blob": "d61f146ae2a77f159c2afbb1b5b3b1893186d9d5", + "reason": "Additionally registers package-composed interval operation semantics only; the factorization service target and executable dependency graph are unchanged." + }, { "path": "HexBerlekamp/FactorTacticTests.lean", "baseline_blob": "4063e15934a89c671ac72d201fa60c2ef6feaf59",