interval: compose operation semantics from packages

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

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

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,57 +73,69 @@ 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
   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
+    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 : ℝ)

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

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,