From f45612f26753ddccf75e0c61e69deb4b37e76472 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 11 Aug 2026 17:44:01 +0000 Subject: [PATCH 1/5] feat(interval): emit proofs from retained branch trees --- HexInterval/Experiment/BranchProof.lean | 139 ++++ HexInterval/SPEC/hex-interval.md | 27 +- .../ExpSignConformance.lean | 581 +------------ .../HexIntervalMathlib/ReluConformance.lean | 772 ++++++++++++++++++ lakefile.lean | 3 +- progress/20260811T174347Z.md | 28 + .../bench/proof_only_runtime_exemptions.json | 6 + 7 files changed, 968 insertions(+), 588 deletions(-) create mode 100644 HexInterval/Experiment/BranchProof.lean create mode 100644 conformance/HexIntervalMathlib/ReluConformance.lean create mode 100644 progress/20260811T174347Z.md diff --git a/HexInterval/Experiment/BranchProof.lean b/HexInterval/Experiment/BranchProof.lean new file mode 100644 index 000000000..2d08cebc7 --- /dev/null +++ b/HexInterval/Experiment/BranchProof.lean @@ -0,0 +1,139 @@ +/- +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.BranchTree +public import HexInterval.Experiment.ProofFrontend + +@[expose] public section + +/-! +# Generic branch-tree proof emission + +This frontend folds a settled retained branch tree from its leaves to its root. +It knows no fact representation, mathematical function, proof schema, or +branch policy. Client callbacks replay an exact closed leaf and join an exact +split; the generic fold validates tree shape, total coverage, and the final +Lean type. + +Runtime tree data remains untrusted. Every callback result is an ordinary +`Expr`, and later callback applications plus the final type check force the +kernel-facing theorem structure. Pending, blocked, failed, unreachable, +duplicated, or cyclic nodes are rejected before a root term is returned. +-/ + +namespace Hex.Interval.Experiment.BranchProof + +open Lean Meta +open BranchTree + +/-- Structural traversal resources, independent of search resources already +charged by `BranchTree`. -/ +structure Limits where + maxNodes : Nat + maxDepth : Nat + deriving DecidableEq, Repr + +/-- Proof-producing operations for one semantics adapter and package set. -/ +structure Emitter (Fact PolicyState : Type) where + leaf : BranchTree.Leaf Fact PolicyState -> + TargetRun.Result Fact PolicyState -> MetaM Expr + split : BranchTree.Leaf Fact PolicyState -> + TargetRun.Result Fact PolicyState -> BranchStart.Children Fact -> + Expr -> Expr -> MetaM Expr + +structure Output (Fact PolicyState : Type) where + proof : Expr + seen : List Nat + source : BranchTree.Leaf Fact PolicyState + +def overlap (left right : List Nat) : Bool := + left.any right.contains + +def sameInput [DecidableEq Fact] + (left right : SemanticReplay.CheckerInput Fact) : Bool := + left.baseProgram == right.baseProgram && + left.initialFacts == right.initialFacts && left.target == right.target + +def sameChild [DecidableEq Fact] + (scope : Propagator.Policy.ScopeId) (depth : Nat) + (input : SemanticReplay.CheckerInput Fact) + (source : BranchTree.Leaf Fact PolicyState) : Bool := + source.scope == scope && source.depth == depth && sameInput source.input input + +partial def emitAt [DecidableEq Fact] + (limits : Limits) (emitter : Emitter Fact PolicyState) + (tree : BranchTree.State Fact PolicyState) (depth : Nat) + (id : BranchTree.TreeId) : MetaM (Output Fact PolicyState) := do + if depth > limits.maxDepth then + throwError "interval branch proof: traversal depth exhausted" + let some node := tree.nodes[id.index]? + | throwError "interval branch proof: missing node {id.index}" + match node with + | .pending _ => + throwError "interval branch proof: pending node {id.index} is not closed" + | .leaf source ending => + match ending with + | .result run => + unless BranchStart.sameInput source.scope source.input run do + throwError "interval branch proof: leaf input does not match its run" + pure + { proof := ← emitter.leaf source run + seen := [id.index] + source } + | .blocked _ _ => + throwError "interval branch proof: blocked node {id.index} is not closed" + | .startError _ => + throwError "interval branch proof: failed node {id.index} is not closed" + | .split source run children left right => + if left.index <= id.index || right.index <= id.index then + throwError "interval branch proof: child does not follow its parent" + if left.index == right.index then + throwError "interval branch proof: split reuses one child" + let leftOutput ← emitAt limits emitter tree (depth + 1) left + let rightOutput ← emitAt limits emitter tree (depth + 1) right + unless BranchStart.sameInput source.scope source.input run do + throwError "interval branch proof: split input does not match its run" + unless sameInput source.input children.parent do + throwError "interval branch proof: split parent input changed" + unless sameChild children.leftScope children.depth children.left + leftOutput.source do + throwError "interval branch proof: left child input changed" + unless sameChild children.rightScope children.depth children.right + rightOutput.source do + throwError "interval branch proof: right child input changed" + if overlap leftOutput.seen rightOutput.seen then + throwError "interval branch proof: subtrees share a node" + let proof ← emitter.split source run children + leftOutput.proof rightOutput.proof + pure + { proof + seen := id.index :: (leftOutput.seen ++ rightOutput.seen) + source } + +/-- Emit one root theorem only from a settled, totally covered tree. + +`expected` is normally the current goal type. The final check is deliberately +inside the generic frontend, so even a single-leaf tree cannot return an +unrelated callback term. -/ +def emit [DecidableEq Fact] (limits : Limits) (emitter : Emitter Fact PolicyState) + (tree : BranchTree.State Fact PolicyState) (expected : Expr) : MetaM Expr := do + if !tree.frontier.isEmpty then + throwError "interval branch proof: tree still has pending work" + if tree.nodes.isEmpty then + throwError "interval branch proof: tree has no root" + if tree.nodes.size > limits.maxNodes then + throwError "interval branch proof: node budget exhausted" + let output ← emitAt limits emitter tree 0 { index := 0 } + if output.seen.length != tree.nodes.size then + throwError "interval branch proof: tree contains unreachable nodes" + let proof ← instantiateMVars output.proof + unless ← isDefEq (← inferType proof) expected do + throwError "interval branch proof: emitted root has the wrong type" + pure proof + +end Hex.Interval.Experiment.BranchProof diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index b4fd83917..c1379e426 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -1711,13 +1711,26 @@ runs the arbitrary exponential propagator in each, and retains two target leaves. Separate guards show that one global step leaves both children pending, and that zero split or one-leaf budgets retain an explicitly blocked root. -This runtime tree contains no proof evidence. The existing two-child proof -canary separately demonstrates how exact retained child runs can be replayed -and joined, but the manager does not yet emit that term. The proof-tree layer -must emit a theorem only when every coverage child is closed by replay or a -checked refutation. For best-bound mode, unfinished leaves must contribute -their inherited parent fact to the global hull; they never inherit a tighter -sibling fact. +This runtime tree contains no proof evidence. The separate generic +`BranchProof` frontend now folds a settled retained tree bottom-up. It first +binds every leaf and split result back to its exact scope, base program, +initial fact array, and target; checks that each child is the exact child input +stored by its parent; rejects pending, blocked, failed, dangling, shared, +cyclic, or unreachable nodes; then asks client callbacks to replay each closed +leaf and apply each package-owned split join. The final emitted expression must +have the requested Lean type. A callback can therefore cause rejection or +choose a different kernel-checkable proof, but tree data itself cannot become +evidence. + +The useful ReLU canary now runs through this generic path. Its retained root +has two exact live target children; the leaf callback invokes the unchanged +generic chronology emitter with the side-specific proof registry, and the +split callback applies `replaySplit`. The resulting expression is assigned to +an ordinary declaration and its axiom report is compile-checked. Separate +negative tests reject the delivered fuel-limited partial tree, a fork whose +two edges share one child, and an otherwise valid but unreachable extra node. +For best-bound mode, unfinished leaves must contribute their inherited parent +fact to the global hull; they never inherit a tighter sibling fact. Several operational choices deliberately remain experimental: diff --git a/conformance/HexIntervalMathlib/ExpSignConformance.lean b/conformance/HexIntervalMathlib/ExpSignConformance.lean index f94f12760..8468f91e9 100644 --- a/conformance/HexIntervalMathlib/ExpSignConformance.lean +++ b/conformance/HexIntervalMathlib/ExpSignConformance.lean @@ -11,6 +11,7 @@ import HexInterval.Experiment.ProofFrontend import HexInterval.Experiment.TargetRun import HexInterval.Experiment.BranchStart import HexInterval.Experiment.BranchTree +import HexInterval.Experiment.BranchProof import Mathlib.Lean.Elab.Tactic.Meta /-! @@ -1563,584 +1564,4 @@ example : True := by throwError "interval_exp_refute test: stale bottom version was accepted" trivial -/-! ## Branch-dependent ReLU propagation - -Unlike exponential positivity, these two propagators are intentionally -conditional. The nonnegative-side rule proves the output fact by rewriting -with `max x 0 = x` from `0 <= x`; the negative-side rule does so by rewriting -with `max x 0 = 0` from `x < 0`. This conditionality is a package-test design -choice for an unconditional final theorem. The runtime and proof packages -know those two function-specific facts, while branch creation, branch seeding, -chronology replay, and the two-proof join stay generic. -/ - -private def reluKey : OpKey := { name := "relu-sign.max-zero" } - -private def reluNonnegativeKey : RuleKey := - { name := "relu-sign.max-zero.nonnegative" } - -private def reluNegativeKey : RuleKey := - { name := "relu-sign.max-zero.negative" } - -private def reluOperation : Operation := - { key := reluKey, inputs := [real], output := real } - -private def reluOperations : Array Operation := #[sourceOperation, reluOperation] - -private def reluInstruction : Node := - { domain := real, op := { index := 1 }, args := [node 0] } - -private def reluProgram : Program := - { operations := reluOperations, nodes := #[sourceInstruction, reluInstruction] } - -private def reluNonnegativeRule : Registration := - { key := reluNonnegativeKey - head := reluKey - kind := .forward - watches := [.argument 0] - writes := [.result] } - -private def reluNegativeRule : Registration := - { key := reluNegativeKey - head := reluKey - kind := .forward - watches := [.argument 0] - writes := [.result] } - -private def reluFormat (side : Bound) : ReplayFormat := - { role := .fact - schema := 1 - validateBody := fun body => body == [side.code] } - -private def reluPlan (side : Bound) (request : RuleRequest Bound) : Plan Bound := - match request.inputs, request.writes with - | [source], [target] => - if source.fact == side then - { outcome := - .success - [{ node := target, fact := .nonnegative, payload := payload 0 }] - [] {} - drafts := - [{ label := payload 0 - role := .fact - schema := 1 - body := [side.code] }] } - else - { outcome := .failed 10, drafts := [] } - | _, _ => { outcome := .failed 11, drafts := [] } - -private def reluPackage : Package Bound := - { Cache := Unit - cache := () - operations := #[reluOperation] - handlers := - #[Handler.statelessPlanned reluNonnegativeRule - (reluPlan .nonnegative) #[reluFormat .nonnegative], - Handler.statelessPlanned reluNegativeRule - (reluPlan .negative) #[reluFormat .negative]] } - -private def reluPackages : Array (Package Bound) := #[sourcePackage, reluPackage] - -private def reluSplitPackages : Array (Package Bound) := - #[sourcePackage, reluPackage, splitPackage] - -private def reluModel : OperationSemantics.Model ℝ := - { operation := reluOperation - relation := fun inputs output => - match inputs with - | [input] => output = max input 0 - | _ => False } - -private def reluModels : Array (OperationSemantics.Model ℝ) := - #[sourceModel, reluModel] - -private def reluSemantics : Semantics Bound := - OperationSemantics.semantics reluModels Contains - -private def reluBoundSchema : FactDomainSchema reluSemantics := - { 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 } - -private def reluLaws : Laws reluSemantics := - { holdsEq := by - intro _ valuation left right fact _ _ values - change Contains fact (valuation left) ↔ Contains fact (valuation right) - rw [values] } - -private def reluStableLaw : GenericInstanceReconstruction.StableLaw reluSemantics := - OperationSemantics.stableLaw reluModels Contains - -private def reluSplitSchema : SplitSchema reluSemantics Unit where - proveCover := fun _ _ parent _ left right => - if shape : parent = .all ∧ left = .nonnegative ∧ right = .negative then - some - { proof := by - rcases shape with ⟨rfl, rfl, rfl⟩ - intro valuation _ _ - change NodeId → ℝ at valuation - change (0 : ℝ) ≤ valuation _ ∨ valuation _ < 0 - exact le_or_gt 0 (valuation _) } - else - none - -private theorem reluSideEntails (side : Bound) - (accepted : side = .nonnegative ∨ side = .negative) - (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]) - (exactAssumptions : assumptions = [{ node := input, fact := side }]) : - reluSemantics.Entails graph assumptions - { node := output, fact := .nonnegative } := by - change ∀ valuation : NodeId → ℝ, - OperationSemantics.Models reluModels graph valuation → - (∀ assumption, assumption ∈ assumptions → - Contains assumption.fact (valuation assumption.node)) → - Contains .nonnegative (valuation output) - intro valuation model holds - obtain ⟨meaning, meaningAt, related⟩ := - model.2 output instruction found - simp [reluModels, operation] at meaningAt - subst meaning - have outputEq : valuation output = max (valuation input) 0 := by - simpa [reluModel, arguments, List.map] using related - have inputH : Contains side (valuation input) := - holds { node := input, fact := side } (by simp [exactAssumptions]) - rcases accepted with rfl | rfl - · change (0 : ℝ) ≤ valuation output - rw [outputEq, max_eq_left inputH] - exact inputH - · change (0 : ℝ) ≤ valuation output - change valuation input < 0 at inputH - rw [outputEq, max_eq_right inputH.le] - -private theorem reluFactWith (fact : NodeFact Bound) {value : Bound} - (equal : fact.fact = value) : - fact = { node := fact.node, fact := value } := by - cases fact - simp_all - -private def reluFactSchema (key : RuleKey) (side : Bound) - (accepted : side = .nonnegative ∨ side = .negative) : - PackedFactSchema reluSemantics where - rule := key - schema := 1 - Certificate := Unit - decode := fun body => if body == [side.code] then some () else none - replay := fun _ _ context _ => - 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] => - if exactAssumptions : - context.assumptions = [{ node := input, fact := side }] then - some - { proof := by - have proposedEq : - context.proposed = - { node := context.proposed.node, - fact := .nonnegative } := - reluFactWith context.proposed proposedFact - rw [proposedEq] - exact - reluSideEntails side accepted context.program - context.assumptions context.proposed.node instruction - input found operation arguments exactAssumptions } - else - none - | _ => none - else - none - | none => none - else - none - -private def reluNonnegativeSchema : PackedFactSchema reluSemantics := - reluFactSchema reluNonnegativeKey .nonnegative (Or.inl rfl) - -private def reluNegativeSchema : PackedFactSchema reluSemantics := - reluFactSchema reluNegativeKey .negative (Or.inr rfl) - -private def reluSourceProof : ProofRegistry.Package reluSemantics Name := - { semantic := { factSchemas := #[] } - emit := { schemas := [] } } - -private def reluProof : ProofRegistry.Package reluSemantics Name := - { semantic := - { factSchemas := #[reluNonnegativeSchema, reluNegativeSchema] } - emit := - { schemas := - [{ key := reluNonnegativeSchema.key, - handle := ``reluNonnegativeSchema }, - { key := reluNegativeSchema.key, - handle := ``reluNegativeSchema }] } } - -private def reluProofPackages : - Array (ProofRegistry.Package reluSemantics Name) := - #[reluSourceProof, reluProof] - -private def reluBaseFacts : List (NodeFact Bound) := - [{ node := node 0, fact := .all }, { node := node 1, fact := .all }] - -private def reluInput : CheckerInput Bound := - { baseProgram := reluProgram - initialFacts := #[.all, .all] - target := { node := node 1, fact := .nonnegative } } - -private theorem reluBaseWithin : FactsWithin reluProgram reluBaseFacts := by - intro fact member - simp only [reluBaseFacts, List.mem_cons, List.not_mem_nil, or_false] at member - rcases member with rfl | rfl <;> simp [reluProgram, node] - -private theorem reluBasePrefix : ProgramPrefix reluProgram reluProgram := - ProgramPrefix.refl reluProgram - -private theorem reluSameOperations : - reluProgram.operations = reluProgram.operations := rfl - -private def reluInitialExtension : - Evidence (reluSemantics.Extends reluProgram reluProgram) := - extendRefl reluSemantics reluProgram - -private noncomputable def reluValuation (x : ℝ) : NodeId → ℝ - | ⟨0⟩ => x - | ⟨1⟩ => max x 0 - | _ => 0 - -private theorem reluValuationModels (x : ℝ) : - reluSemantics.models reluProgram (reluValuation x) := by - refine ⟨?_, ?_⟩ - · simp [reluProgram, reluOperations, reluModels, sourceModel, reluModel] - rintro ⟨index⟩ instruction found - cases index with - | zero => - simp [Program.node?, reluProgram, sourceInstruction] at found - subst instruction - exact ⟨sourceModel, by rfl, by rfl⟩ - | succ index => - cases index with - | zero => - simp [Program.node?, reluProgram, reluInstruction] at found - subst instruction - exact ⟨reluModel, by rfl, by rfl⟩ - | succ index => - simp [Program.node?, reluProgram] at found - -private theorem closeRelu (x : ℝ) - (result : Evidence - (reluSemantics.Entails reluProgram reluBaseFacts reluInput.target)) : - 0 ≤ max x 0 := by - have holds := result.proof (reluValuation x) (reluValuationModels x) - (by - intro fact member - simp only [reluBaseFacts, List.mem_cons, List.not_mem_nil, or_false] at member - rcases member with rfl | rfl <;> trivial) - exact holds - -private def reluOffer? (key : RuleKey) (view : Propagator.Policy.View Bound) : - Option Propagator.Policy.OfferView := - view.offers.toList.find? fun offer => - match offer.key with - | .invoke invocation => invocation.rule == key - | _ => false - -private def reluRulePolicy (key : RuleKey) : - TargetRun.Controller Bound Unit := - { update := fun state _ => state - choose := fun state view => - match reluOffer? key view with - | some offer => .select offer state - | none => .stop state } - -private def reluRunWith? (runtimePackages : Array (Package Bound)) - (input : CheckerInput Bound) (controller : TargetRun.Controller Bound Unit) - (scope : Propagator.Policy.ScopeId := { index := 0 }) : - Option (TargetRun.Result Bound Unit) := do - let .ok session := PolicySession.Session.start factDomain - input.baseProgram runtimePackages input.initialFacts limits scope - | none - some (TargetRun.drive factDomain input.target.node input.target.fact controller - limits.policy.maxDecisions session ()) - -private def reluPrepared? : - Option (ULift.{1, 0} (BranchStart.Children Bound)) := - match reluRunWith? reluSplitPackages reluInput splitPolicy with - | none => none - | some result => - match result.stop with - | .split plan => - match BranchStart.prepare branchLimits - (BranchStart.State.start result.session) result.session plan - reluInput.target signSplitter with - | .ok (_, children) => some (ULift.up children) - | .error _ => none - | _ => none - -private def reluBranchFact (side : Bound) : NodeFact Bound := - { node := node 0, fact := side } - -private def reluBranchFacts (side : Bound) : List (NodeFact Bound) := - reluBranchFact side :: reluBaseFacts - -private def reluBranchInput (side : Bound) : CheckerInput Bound := - { baseProgram := reluProgram - initialFacts := #[side, .all] - target := reluInput.target } - -private def reluInherit (side : Bound) (observed : NodeId) - (different : observed ≠ node 0) (fact : Bound) - (found : (reluBranchInput side).initialFacts[observed.index]? = some fact) : - Evidence - (reluSemantics.Entails reluProgram reluBaseFacts { node := observed, fact }) := - { proof := by - intro _ _ assumptions - cases observed with - | mk index => - cases index with - | zero => simp [node] at different - | succ index => - cases index with - | zero => - simp [reluBranchInput] at found - subst fact - exact assumptions _ (by simp [reluBaseFacts, node]) - | succ index => simp [reluBranchInput] at found } - -private def reluLeftInput : CheckerInput Bound := - reluBranchInput .nonnegative - -private def reluRightInput : CheckerInput Bound := - reluBranchInput .negative - -private def reluLeftFacts : List (NodeFact Bound) := - reluBranchFacts .nonnegative - -private def reluRightFacts : List (NodeFact Bound) := - reluBranchFacts .negative - -private def reluLeftSeed : - ProofEmitter.BranchSeed reluSemantics reluLeftInput reluBaseFacts - (reluBranchFact .nonnegative) := - ProofEmitter.BranchSeed.make reluLeftInput (reluBranchFact .nonnegative) - (by rfl) (by rfl) (reluInherit .nonnegative) - -private def reluRightSeed : - ProofEmitter.BranchSeed reluSemantics reluRightInput reluBaseFacts - (reluBranchFact .negative) := - ProofEmitter.BranchSeed.make reluRightInput (reluBranchFact .negative) - (by rfl) (by rfl) (reluInherit .negative) - -private structure ReluRun where - session : PolicySession.Session Bound - registry : ProofRegistry.Registry reluSemantics Name - reached : TargetRun.Reached Bound - -private def reluRunChild? (side : Bound) (input : CheckerInput Bound) - (scope : Propagator.Policy.ScopeId) : Option ReluRun := do - let key := if side == .nonnegative then reluNonnegativeKey else reluNegativeKey - let result ← reluRunWith? reluPackages input (reluRulePolicy key) scope - let .target reached := result.stop | none - let .ok registry := ProofRegistry.build result.session.registry reluProofPackages - | none - some { session := result.session, registry, reached } - -#guard - reluPrepared?.any fun lifted => - let children := lifted.down - children.depth == 1 && sameChecker children.parent reluInput && - children.leftScope == ({ index := 1 } : Propagator.Policy.ScopeId) && - children.rightScope == ({ index := 2 } : Propagator.Policy.ScopeId) && - sameChecker children.left reluLeftInput && - sameChecker children.right reluRightInput - -private def reluTraceUses? (side : Bound) (input : CheckerInput Bound) - (scope : Propagator.Policy.ScopeId) : Bool := - match reluRunChild? side input scope with - | none => false - | some run => - match Frontend.trace? run.session.state.engine run.session.arena with - | some trace => - match trace.events with - | [.rule step] => - trace.program == input.baseProgram && - run.reached.seen == - ({ node := node 1, version := 1 } : SeenVersion) && - run.reached.fact == .nonnegative && - run.session.state.engine.facts == #[side, .nonnegative] && - run.session.state.engine.versions == #[0, 1] && - step.assumptions == [reluBranchFact side] && - step.event.programVersion == 0 && step.event.node == node 1 && - step.event.previous == - ({ node := node 1, version := 0 } : SeenVersion) && - step.event.fact == .nonnegative && - step.event.version == 1 && step.previous == .all && - step.entry.replayKey == - (if side == .nonnegative then reluNonnegativeSchema.key - else reluNegativeSchema.key) - | _ => false - | none => false - -#guard reluTraceUses? .nonnegative reluLeftInput { index := 1 } -#guard reluTraceUses? .negative reluRightInput { index := 2 } - -private def reluRejectsUnsplit? (key : RuleKey) : Bool := - reluRunWith? reluPackages reluInput (reluRulePolicy key) |>.any fun result => - (match result.stop with | .target _ => false | _ => true) && - result.session.state.engine.facts == #[.all, .all] && - result.session.state.engine.history.isEmpty - -#guard reluRejectsUnsplit? reluNonnegativeKey -#guard reluRejectsUnsplit? reluNegativeKey - -private theorem reluBranchWithin (side : Bound) : - FactsWithin reluProgram (reluBranchFacts side) := by - intro fact member - simp only [reluBranchFacts, reluBranchFact, reluBaseFacts, List.mem_cons, - List.not_mem_nil, or_false] at member - rcases member with rfl | rfl | rfl <;> simp [reluProgram, node] - -private def reluSeedAssumed (graph : Program) (base : List (NodeFact Bound)) - (index : Nat) (fact : NodeFact Bound) (found : base[index]? = some fact) : - Evidence (reluSemantics.Entails graph base fact) := - ProofEmitter.assumedAt graph base index fact found - -private def reluContext (input facts within : Expr) - (factValues : List (NodeFact Bound)) : ProofFrontend.Context Bound Name := - { encoder := boundEncoder - resolveSchema := pure - semantics := mkConst ``reluSemantics - domain := mkConst ``reluBoundSchema - laws := mkConst ``reluLaws - stableLaw := mkConst ``reluStableLaw - input - assumed := ``reluSeedAssumed - baseFacts := factValues - baseFactsTerm := facts - baseProgram := reluProgram - baseProgramTerm := mkConst ``reluProgram - basePrefix := mkConst ``reluBasePrefix - baseWithin := within - initialExtension := mkConst ``reluInitialExtension - finalPrefix := mkConst ``reluBasePrefix - sameOperations := mkConst ``reluSameOperations - top := reluBoundSchema.top } - -private def reluLeftContext : ProofFrontend.Context Bound Name := - reluContext (mkConst ``reluLeftInput) (mkConst ``reluLeftFacts) - (mkApp (mkConst ``reluBranchWithin) (mkConst ``Bound.nonnegative)) - reluLeftFacts - -private def reluRightContext : ProofFrontend.Context Bound Name := - reluContext (mkConst ``reluRightInput) (mkConst ``reluRightFacts) - (mkApp (mkConst ``reluBranchWithin) (mkConst ``Bound.negative)) - reluRightFacts - -private def reluParent : Evidence - (reluSemantics.Entails reluProgram reluBaseFacts (reluBranchFact .all)) := - ProofEmitter.assumed (by simp [reluBaseFacts, reluBranchFact, node]) - -private meta def emitReluChild (context : ProofFrontend.Context Bound Name) - (side : Bound) (input : CheckerInput Bound) - (scope : Propagator.Policy.ScopeId) (seed : Expr) : MetaM Expr := do - let some run := reluRunChild? side input scope - | throwError "interval_relu_split: child search failed" - let some trace := Frontend.trace? run.session.state.engine run.session.arena - | throwError "interval_relu_split: child chronology quotation failed" - let [.rule step] := trace.events - | throwError "interval_relu_split: child trace is not exactly one rule" - let expectedKey := - if side == .nonnegative then reluNonnegativeSchema.key - else reluNegativeSchema.key - unless trace.program == input.baseProgram && - run.reached.seen == ({ node := node 1, version := 1 } : SeenVersion) && - run.reached.fact == .nonnegative && - run.session.state.engine.facts == #[side, .nonnegative] && - run.session.state.engine.versions == #[0, 1] && - step.assumptions == [reluBranchFact side] && - step.event.programVersion == 0 && step.event.node == node 1 && - step.event.previous == ({ node := node 1, version := 0 } : SeenVersion) && - step.event.fact == .nonnegative && step.event.version == 1 && - step.previous == .all && step.entry.replayKey == expectedKey do - throwError "interval_relu_split: child result or quoted rule trace drifted" - let state ← ProofFrontend.emitBranch context input seed trace.program - trace.events run.registry.emit - ProofFrontend.closeTarget context state run.reached.seen run.reached.fact input.target - -private meta def emitReluSplit : MetaM Expr := do - let some lifted := reluPrepared? - | throwError "interval_relu_split: branch preparation failed" - let children := lifted.down - let left ← emitReluChild reluLeftContext .nonnegative children.left - children.leftScope (mkConst ``reluLeftSeed) - let right ← emitReluChild reluRightContext .negative children.right - children.rightScope (mkConst ``reluRightSeed) - let result ← - mkAppM ``ProofEmitter.replaySplit - #[mkConst ``reluSplitSchema, mkConst ``reluProgram, - mkConst ``reluBaseFacts, ← boundEncoder.nodeId (node 0), - ← boundEncoder.fact .all, mkConst ``Unit.unit, - ← boundEncoder.fact .nonnegative, ← boundEncoder.fact .negative, - ← boundEncoder.nodeFact reluInput.target, - mkConst ``reluParent, left, right] - ProofFrontend.replayResult result - -/-- The emitted term contains both live child replays and the checked generic -split join. Assigning that term to this declaration makes the ordinary kernel, -not the Meta evaluator, validate the complete proof. -/ -private def reluJoined : Evidence - (reluSemantics.Entails reluProgram reluBaseFacts reluInput.target) := by - run_tac - let goal ← getMainGoal - goal.assign (← emitReluSplit) - -/-- An arbitrary-function vertical whose child proofs consume distinct split -assumptions by construction: neither ReLU propagator fires before the zero -split. The final theorem is unconditional; conditionality here tests the -branch proof plumbing rather than mathematical necessity. -/ -theorem reluSplit (x : ℝ) : 0 ≤ max x 0 := - closeRelu x reluJoined - -/-- -info: 'Hex.IntervalMathlib.ExpSignConformance.reluSplit' depends on axioms: [propext, Classical.choice, Quot.sound] --/ -#guard_msgs in -#print axioms reluSplit - -set_option linter.unusedTactic false in -example : True := by - run_tac - let checkMutation (context : ProofFrontend.Context Bound Name) - (side wrong : Bound) (input : CheckerInput Bound) - (scope : Propagator.Policy.ScopeId) (seed : Expr) : MetaM Unit := do - let some run := reluRunChild? side input scope - | throwError "interval_relu_split mutation: child search failed" - let some trace := Frontend.trace? run.session.state.engine run.session.arena - | throwError "interval_relu_split mutation: trace missing" - let [.rule step] := trace.events - | throwError "interval_relu_split mutation: wrong trace shape" - let mutated : RuleStep Bound := - { step with assumptions := [reluBranchFact wrong] } - if (← observing? <| ProofFrontend.emitBranch context input seed trace.program - [.rule mutated] run.registry.emit).isSome then - throwError - "interval_relu_split mutation: opposite split assumption was accepted" - checkMutation reluLeftContext .nonnegative .negative reluLeftInput - { index := 1 } (mkConst ``reluLeftSeed) - checkMutation reluRightContext .negative .nonnegative reluRightInput - { index := 2 } (mkConst ``reluRightSeed) - trivial - end Hex.IntervalMathlib.ExpSignConformance diff --git a/conformance/HexIntervalMathlib/ReluConformance.lean b/conformance/HexIntervalMathlib/ReluConformance.lean new file mode 100644 index 000000000..dffae4ccd --- /dev/null +++ b/conformance/HexIntervalMathlib/ReluConformance.lean @@ -0,0 +1,772 @@ +/- +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.ExpSignConformance +import HexInterval.Experiment.BranchProof + +/-! +# Branch-dependent function propagation conformance + +This module checks that a retained split tree whose children use different +function-specific propagators can be folded into one kernel-checked proof. +-/ + +namespace Hex.IntervalMathlib.ReluConformance + +open Lean Elab Tactic Meta +open Hex.Interval.Experiment +open Propagator PolicySession SemanticReplay ChronologicalReplay ProofEmitter +open Frontend FrontendEncoder ProofFrontend ProofRegistry GoalFrontend ExpSign +open GoalClosure BranchStart +open Hex.IntervalMathlib.ExpSignConformance + +private def splitOffer? (view : Propagator.Policy.View Bound) : + Option Propagator.Policy.OfferView := + view.offers.toList.find? fun offer => + match offer.key with + | .invoke invocation => invocation.rule == splitRuleKey + | .split _ _ _ _ => true + | _ => false + +private def splitPolicy : TargetRun.Controller Bound Unit := + { update := fun state _ => state + choose := fun state view => + match splitOffer? view with + | some offer => .select offer state + | none => .stop state } + +private def signSplitter : BranchStart.Splitter Bound := + { split := fun graph target instruction parent point => + if graph.node? target == some instruction && instruction.domain == real && + parent == .all && point == 0 then + some (.nonnegative, .negative) + else + none } + +private def branchLimits : BranchStart.Limits := + { maxDepth := 4, maxScopes := 8 } + +private def treeLimits (maxSteps := 3) (maxSplits := 1) + (maxLeaves := 2) : BranchTree.Limits := + { branch := branchLimits + maxSteps + maxSplits + maxLeaves + leafFuel := limits.policy.maxDecisions } + +private def boundExpr : Bound → Expr + | .all => mkConst ``Bound.all + | .nonnegative => mkConst ``Bound.nonnegative + | .negative => mkConst ``Bound.negative + | .empty => mkConst ``Bound.empty + +private def boundEncoder : FrontendEncoder.Encoder Bound := + FrontendEncoder.make (mkConst ``Bound) (fun fact => pure (boundExpr fact)) + +/-! ## Branch-dependent ReLU propagation + +Unlike exponential positivity, these two propagators are intentionally +conditional. The nonnegative-side rule proves `max x 0 = x` from `0 <= x`; +the negative-side rule proves `max x 0 = 0` from `x < 0`. The runtime and +proof packages know those two function-specific facts, while branch creation, +branch seeding, chronology replay, and the two-proof join stay generic. -/ + +private def reluKey : OpKey := { name := "relu-sign.max-zero" } + +private def reluNonnegativeKey : RuleKey := + { name := "relu-sign.max-zero.nonnegative" } + +private def reluNegativeKey : RuleKey := + { name := "relu-sign.max-zero.negative" } + +private def reluOperation : Operation := + { key := reluKey, inputs := [real], output := real } + +private def reluOperations : Array Operation := #[sourceOperation, reluOperation] + +private def reluInstruction : Node := + { domain := real, op := { index := 1 }, args := [node 0] } + +private def reluProgram : Program := + { operations := reluOperations, nodes := #[sourceInstruction, reluInstruction] } + +private def reluNonnegativeRule : Registration := + { key := reluNonnegativeKey + head := reluKey + kind := .forward + watches := [.argument 0] + writes := [.result] } + +private def reluNegativeRule : Registration := + { key := reluNegativeKey + head := reluKey + kind := .forward + watches := [.argument 0] + writes := [.result] } + +private def reluFormat (side : Bound) : ReplayFormat := + { role := .fact + schema := 1 + validateBody := fun body => body == [side.code] } + +private def reluPlan (side : Bound) (request : RuleRequest Bound) : Plan Bound := + match request.inputs, request.writes with + | [source], [target] => + if source.fact == side then + { outcome := + .success + [{ node := target, fact := .nonnegative, payload := payload 0 }] + [] {} + drafts := + [{ label := payload 0 + role := .fact + schema := 1 + body := [side.code] }] } + else + { outcome := .failed 10, drafts := [] } + | _, _ => { outcome := .failed 11, drafts := [] } + +private def reluPackage : Package Bound := + { Cache := Unit + cache := () + operations := #[reluOperation] + handlers := + #[Handler.statelessPlanned reluNonnegativeRule + (reluPlan .nonnegative) #[reluFormat .nonnegative], + Handler.statelessPlanned reluNegativeRule + (reluPlan .negative) #[reluFormat .negative]] } + +private def reluPackages : Array (Package Bound) := #[sourcePackage, reluPackage] + +private def reluSplitPackages : Array (Package Bound) := + #[sourcePackage, reluPackage, splitPackage] + +private def reluModel : OperationSemantics.Model ℝ := + { operation := reluOperation + relation := fun inputs output => + match inputs with + | [input] => output = max input 0 + | _ => False } + +private def reluModels : Array (OperationSemantics.Model ℝ) := + #[sourceModel, reluModel] + +private def reluSemantics : Semantics Bound := + OperationSemantics.semantics reluModels Contains + +private def reluBoundSchema : FactDomainSchema reluSemantics := + { 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 } + +private def reluLaws : Laws reluSemantics := + { holdsEq := by + intro _ valuation left right fact _ _ values + change Contains fact (valuation left) ↔ Contains fact (valuation right) + rw [values] } + +private def reluStableLaw : GenericInstanceReconstruction.StableLaw reluSemantics := + OperationSemantics.stableLaw reluModels Contains + +private def reluSplitSchema : SplitSchema reluSemantics Unit where + proveCover := fun _ _ parent _ left right => + if shape : parent = .all ∧ left = .nonnegative ∧ right = .negative then + some + { proof := by + rcases shape with ⟨rfl, rfl, rfl⟩ + intro valuation _ _ + change NodeId → ℝ at valuation + change (0 : ℝ) ≤ valuation _ ∨ valuation _ < 0 + exact le_or_gt 0 (valuation _) } + else + none + +private theorem reluSideEntails (side : Bound) + (accepted : side = .nonnegative ∨ side = .negative) + (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]) + (exactAssumptions : assumptions = [{ node := input, fact := side }]) : + reluSemantics.Entails graph assumptions + { node := output, fact := .nonnegative } := by + change ∀ valuation : NodeId → ℝ, + OperationSemantics.Models reluModels graph valuation → + (∀ assumption, assumption ∈ assumptions → + Contains assumption.fact (valuation assumption.node)) → + Contains .nonnegative (valuation output) + intro valuation model holds + obtain ⟨meaning, meaningAt, related⟩ := + model.2 output instruction found + simp [reluModels, operation] at meaningAt + subst meaning + have outputEq : valuation output = max (valuation input) 0 := by + simpa [reluModel, arguments, List.map] using related + have inputH : Contains side (valuation input) := + holds { node := input, fact := side } (by simp [exactAssumptions]) + rcases accepted with rfl | rfl + · change (0 : ℝ) ≤ valuation output + rw [outputEq, max_eq_left inputH] + exact inputH + · change (0 : ℝ) ≤ valuation output + change valuation input < 0 at inputH + rw [outputEq, max_eq_right inputH.le] + +private theorem reluFactWith (fact : NodeFact Bound) {value : Bound} + (equal : fact.fact = value) : + fact = { node := fact.node, fact := value } := by + cases fact + simp_all + +private def reluFactSchema (key : RuleKey) (side : Bound) + (accepted : side = .nonnegative ∨ side = .negative) : + PackedFactSchema reluSemantics where + rule := key + schema := 1 + Certificate := Unit + decode := fun body => if body == [side.code] then some () else none + replay := fun _ _ context _ => + 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] => + if exactAssumptions : + context.assumptions = [{ node := input, fact := side }] then + some + { proof := by + have proposedEq : + context.proposed = + { node := context.proposed.node, + fact := .nonnegative } := + reluFactWith context.proposed proposedFact + rw [proposedEq] + exact + reluSideEntails side accepted context.program + context.assumptions context.proposed.node instruction + input found operation arguments exactAssumptions } + else + none + | _ => none + else + none + | none => none + else + none + +private def reluNonnegativeSchema : PackedFactSchema reluSemantics := + reluFactSchema reluNonnegativeKey .nonnegative (Or.inl rfl) + +private def reluNegativeSchema : PackedFactSchema reluSemantics := + reluFactSchema reluNegativeKey .negative (Or.inr rfl) + +private def reluSourceProof : ProofRegistry.Package reluSemantics Name := + { semantic := { factSchemas := #[] } + emit := { schemas := [] } } + +private def reluProof : ProofRegistry.Package reluSemantics Name := + { semantic := + { factSchemas := #[reluNonnegativeSchema, reluNegativeSchema] } + emit := + { schemas := + [{ key := reluNonnegativeSchema.key, + handle := ``reluNonnegativeSchema }, + { key := reluNegativeSchema.key, + handle := ``reluNegativeSchema }] } } + +private def reluProofPackages : + Array (ProofRegistry.Package reluSemantics Name) := + #[reluSourceProof, reluProof] + +private def reluSplitProof : ProofRegistry.Package reluSemantics Name := + { semantic := { factSchemas := #[] } + emit := { schemas := [] } } + +private def reluSplitProofPackages : + Array (ProofRegistry.Package reluSemantics Name) := + #[reluSourceProof, reluProof, reluSplitProof] + +private def reluBaseFacts : List (NodeFact Bound) := + [{ node := node 0, fact := .all }, { node := node 1, fact := .all }] + +private def reluInput : CheckerInput Bound := + { baseProgram := reluProgram + initialFacts := #[.all, .all] + target := { node := node 1, fact := .nonnegative } } + +private theorem reluBaseWithin : FactsWithin reluProgram reluBaseFacts := by + intro fact member + simp only [reluBaseFacts, List.mem_cons, List.not_mem_nil, or_false] at member + rcases member with rfl | rfl <;> simp [reluProgram, node] + +private theorem reluBasePrefix : ProgramPrefix reluProgram reluProgram := + ProgramPrefix.refl reluProgram + +private theorem reluSameOperations : + reluProgram.operations = reluProgram.operations := rfl + +private def reluInitialExtension : + Evidence (reluSemantics.Extends reluProgram reluProgram) := + extendRefl reluSemantics reluProgram + +private noncomputable def reluValuation (x : ℝ) : NodeId → ℝ + | ⟨0⟩ => x + | ⟨1⟩ => max x 0 + | _ => 0 + +private theorem reluValuationModels (x : ℝ) : + reluSemantics.models reluProgram (reluValuation x) := by + refine ⟨?_, ?_⟩ + · simp [reluProgram, reluOperations, reluModels, sourceModel, reluModel] + rintro ⟨index⟩ instruction found + cases index with + | zero => + simp [Program.node?, reluProgram, sourceInstruction] at found + subst instruction + exact ⟨sourceModel, by rfl, by rfl⟩ + | succ index => + cases index with + | zero => + simp [Program.node?, reluProgram, reluInstruction] at found + subst instruction + exact ⟨reluModel, by rfl, by rfl⟩ + | succ index => + simp [Program.node?, reluProgram] at found + +private theorem closeRelu (x : ℝ) + (result : Evidence + (reluSemantics.Entails reluProgram reluBaseFacts reluInput.target)) : + 0 ≤ max x 0 := by + have holds := result.proof (reluValuation x) (reluValuationModels x) + (by + intro fact member + simp only [reluBaseFacts, List.mem_cons, List.not_mem_nil, or_false] at member + rcases member with rfl | rfl <;> trivial) + exact holds + +private def reluOffer? (key : RuleKey) (view : Propagator.Policy.View Bound) : + Option Propagator.Policy.OfferView := + view.offers.toList.find? fun offer => + match offer.key with + | .invoke invocation => invocation.rule == key + | _ => false + +private def reluRulePolicy (key : RuleKey) : + TargetRun.Controller Bound Unit := + { update := fun state _ => state + choose := fun state view => + match reluOffer? key view with + | some offer => .select offer state + | none => .stop state } + +private def reluRunWith? (runtimePackages : Array (Package Bound)) + (input : CheckerInput Bound) (controller : TargetRun.Controller Bound Unit) + (scope : Propagator.Policy.ScopeId := { index := 0 }) : + Option (TargetRun.Result Bound Unit) := do + let .ok session := PolicySession.Session.start factDomain + input.baseProgram runtimePackages input.initialFacts limits scope + | none + some (TargetRun.drive factDomain input.target.node input.target.fact controller + limits.policy.maxDecisions session ()) + +private def reluPrepared? : + Option (ULift.{1, 0} (BranchStart.Children Bound)) := + match reluRunWith? reluSplitPackages reluInput splitPolicy with + | none => none + | some result => + match result.stop with + | .split plan => + match BranchStart.prepare branchLimits + (BranchStart.State.start { index := 0 }) 0 result.session plan + reluInput.target signSplitter with + | .ok (_, children) => some (ULift.up children) + | .error _ => none + | _ => none + +private def reluBranchFact (side : Bound) : NodeFact Bound := + { node := node 0, fact := side } + +private def reluBranchFacts (side : Bound) : List (NodeFact Bound) := + reluBranchFact side :: reluBaseFacts + +private def reluBranchInput (side : Bound) : CheckerInput Bound := + { baseProgram := reluProgram + initialFacts := #[side, .all] + target := reluInput.target } + +private def reluInherit (side : Bound) (observed : NodeId) + (different : observed ≠ node 0) (fact : Bound) + (found : (reluBranchInput side).initialFacts[observed.index]? = some fact) : + Evidence + (reluSemantics.Entails reluProgram reluBaseFacts { node := observed, fact }) := + { proof := by + intro _ _ assumptions + cases observed with + | mk index => + cases index with + | zero => simp [node] at different + | succ index => + cases index with + | zero => + simp [reluBranchInput] at found + subst fact + exact assumptions _ (by simp [reluBaseFacts, node]) + | succ index => simp [reluBranchInput] at found } + +private def reluLeftInput : CheckerInput Bound := + reluBranchInput .nonnegative + +private def reluRightInput : CheckerInput Bound := + reluBranchInput .negative + +private def reluLeftFacts : List (NodeFact Bound) := + reluBranchFacts .nonnegative + +private def reluRightFacts : List (NodeFact Bound) := + reluBranchFacts .negative + +private def reluLeftSeed : + ProofEmitter.BranchSeed reluSemantics reluLeftInput reluBaseFacts + (reluBranchFact .nonnegative) := + ProofEmitter.BranchSeed.make reluLeftInput (reluBranchFact .nonnegative) + (by rfl) (by rfl) (reluInherit .nonnegative) + +private def reluRightSeed : + ProofEmitter.BranchSeed reluSemantics reluRightInput reluBaseFacts + (reluBranchFact .negative) := + ProofEmitter.BranchSeed.make reluRightInput (reluBranchFact .negative) + (by rfl) (by rfl) (reluInherit .negative) + +private structure ReluRun where + session : PolicySession.Session Bound + registry : ProofRegistry.Registry reluSemantics Name + reached : TargetRun.Reached Bound + +private def reluRunChild? (side : Bound) (input : CheckerInput Bound) + (scope : Propagator.Policy.ScopeId) : Option ReluRun := do + let key := if side == .nonnegative then reluNonnegativeKey else reluNegativeKey + let result ← reluRunWith? reluPackages input (reluRulePolicy key) scope + let .target reached := result.stop | none + let .ok registry := ProofRegistry.build result.session.registry reluProofPackages + | none + some { session := result.session, registry, reached } + +private def reluTreePolicy : TargetRun.Controller Bound Unit := + { update := fun state _ => state + choose := fun state view => + let selected := + if view.scope.index == 0 then splitOffer? view + else if view.scope.index == 1 then reluOffer? reluNonnegativeKey view + else if view.scope.index == 2 then reluOffer? reluNegativeKey view + else none + match selected with + | some offer => .select offer state + | none => .stop state } + +private def reluTreeConfig (resources : BranchTree.Limits) : + BranchTree.Config Bound Unit := + { factDomain + packages := reluSplitPackages + sessionLimits := limits + controller := reluTreePolicy + splitter := signSplitter + forkPolicy := fun state _ => state + order := .depthFirst + limits := resources } + +private def reluTree? (resources : BranchTree.Limits := treeLimits) : + Option (BranchTree.State Bound Unit) := do + let .ok state := BranchTree.start (reluTreeConfig resources) { index := 0 } + reluInput () | none + let .ok state := BranchTree.run (reluTreeConfig resources) state | none + some state + +#guard + reluTree?.any fun state => + state.settled && state.nodes.size == 3 && state.steps == 3 && + state.splits == 1 && state.leaves == 2 && + match state.nodes[1]?, state.nodes[2]? with + | some (BranchTree.Node.leaf left (BranchTree.LeafEnd.result leftRun)), + some (BranchTree.Node.leaf right (BranchTree.LeafEnd.result rightRun)) => + left.scope.index == 1 && left.input.initialFacts == #[.nonnegative, .all] && + right.scope.index == 2 && right.input.initialFacts == #[.negative, .all] && + (match leftRun.stop with | .target _ => true | _ => false) && + (match rightRun.stop with | .target _ => true | _ => false) + | _, _ => false + +#guard + reluPrepared?.any fun lifted => + let children := lifted.down + children.leftScope == ({ index := 1 } : Propagator.Policy.ScopeId) && + children.rightScope == ({ index := 2 } : Propagator.Policy.ScopeId) && + children.left.baseProgram == reluLeftInput.baseProgram && + children.left.initialFacts == reluLeftInput.initialFacts && + children.left.target == reluLeftInput.target && + children.right.baseProgram == reluRightInput.baseProgram && + children.right.initialFacts == reluRightInput.initialFacts && + children.right.target == reluRightInput.target + +private def reluTraceUses? (side : Bound) (input : CheckerInput Bound) + (scope : Propagator.Policy.ScopeId) : Bool := + match reluRunChild? side input scope with + | none => false + | some run => + match Frontend.trace? run.session.state.engine run.session.arena with + | some trace => + match trace.events with + | [.rule step] => + step.assumptions == [reluBranchFact side] && + step.event.fact == .nonnegative && + step.entry.replayKey == + (if side == .nonnegative then reluNonnegativeSchema.key + else reluNegativeSchema.key) + | _ => false + | none => false + +#guard reluTraceUses? .nonnegative reluLeftInput { index := 1 } +#guard reluTraceUses? .negative reluRightInput { index := 2 } + +private def reluRejectsUnsplit? (key : RuleKey) : Bool := + reluRunWith? reluPackages reluInput (reluRulePolicy key) |>.any fun result => + (match result.stop with | .target _ => false | _ => true) && + result.session.state.engine.facts == #[.all, .all] && + result.session.state.engine.history.isEmpty + +#guard reluRejectsUnsplit? reluNonnegativeKey +#guard reluRejectsUnsplit? reluNegativeKey + +private theorem reluBranchWithin (side : Bound) : + FactsWithin reluProgram (reluBranchFacts side) := by + intro fact member + simp only [reluBranchFacts, reluBranchFact, reluBaseFacts, List.mem_cons, + List.not_mem_nil, or_false] at member + rcases member with rfl | rfl | rfl <;> simp [reluProgram, node] + +private def reluSeedAssumed (graph : Program) (base : List (NodeFact Bound)) + (index : Nat) (fact : NodeFact Bound) (found : base[index]? = some fact) : + Evidence (reluSemantics.Entails graph base fact) := + ProofEmitter.assumedAt graph base index fact found + +private def reluContext (input facts within : Expr) + (factValues : List (NodeFact Bound)) : ProofFrontend.Context Bound Name := + { encoder := boundEncoder + resolveSchema := pure + semantics := mkConst ``reluSemantics + domain := mkConst ``reluBoundSchema + laws := mkConst ``reluLaws + stableLaw := mkConst ``reluStableLaw + input + assumed := ``reluSeedAssumed + baseFacts := factValues + baseFactsTerm := facts + baseProgram := reluProgram + baseProgramTerm := mkConst ``reluProgram + basePrefix := mkConst ``reluBasePrefix + baseWithin := within + initialExtension := mkConst ``reluInitialExtension + finalPrefix := mkConst ``reluBasePrefix + sameOperations := mkConst ``reluSameOperations + top := reluBoundSchema.top } + +private def reluLeftContext : ProofFrontend.Context Bound Name := + reluContext (mkConst ``reluLeftInput) (mkConst ``reluLeftFacts) + (mkApp (mkConst ``reluBranchWithin) (mkConst ``Bound.nonnegative)) + reluLeftFacts + +private def reluRightContext : ProofFrontend.Context Bound Name := + reluContext (mkConst ``reluRightInput) (mkConst ``reluRightFacts) + (mkApp (mkConst ``reluBranchWithin) (mkConst ``Bound.negative)) + reluRightFacts + +private def reluParent : Evidence + (reluSemantics.Entails reluProgram reluBaseFacts (reluBranchFact .all)) := + ProofEmitter.assumed (by simp [reluBaseFacts, reluBranchFact, node]) + +private meta def emitReluChild (context : ProofFrontend.Context Bound Name) + (side : Bound) (input : CheckerInput Bound) + (scope : Propagator.Policy.ScopeId) (seed : Expr) : MetaM Expr := do + let some run := reluRunChild? side input scope + | throwError "interval_relu_split: child search failed" + let some trace := Frontend.trace? run.session.state.engine run.session.arena + | throwError "interval_relu_split: child chronology quotation failed" + let state ← ProofFrontend.emitBranch context input seed trace.program + trace.events run.registry.emit + ProofFrontend.closeTarget context state run.reached.seen run.reached.fact input.target + +private meta def emitReluSplit : MetaM Expr := do + let some lifted := reluPrepared? + | throwError "interval_relu_split: branch preparation failed" + let children := lifted.down + let left ← emitReluChild reluLeftContext .nonnegative children.left + children.leftScope (mkConst ``reluLeftSeed) + let right ← emitReluChild reluRightContext .negative children.right + children.rightScope (mkConst ``reluRightSeed) + let result ← + mkAppM ``ProofEmitter.replaySplit + #[mkConst ``reluSplitSchema, mkConst ``reluProgram, + mkConst ``reluBaseFacts, ← boundEncoder.nodeId (node 0), + ← boundEncoder.fact .all, mkConst ``Unit.unit, + ← boundEncoder.fact .nonnegative, ← boundEncoder.fact .negative, + ← boundEncoder.nodeFact reluInput.target, + mkConst ``reluParent, left, right] + ProofFrontend.replayResult result + +/-- The emitted term contains both live child replays and the checked generic +split join. Assigning that term to this declaration makes the ordinary kernel, +not the Meta evaluator, validate the complete proof. -/ +private def reluJoined : Evidence + (reluSemantics.Entails reluProgram reluBaseFacts reluInput.target) := by + run_tac + let goal ← getMainGoal + goal.assign (← emitReluSplit) + +/-- A genuinely branch-dependent arbitrary-function vertical: neither ReLU +propagator fires before the zero split, and each child proof consumes its own +strictly narrower source fact before the generic join closes the theorem. -/ +theorem tacticReluSplit (x : ℝ) : 0 ≤ max x 0 := + closeRelu x reluJoined + +private meta def emitReluTreeLeaf (source : BranchTree.Leaf Bound Unit) + (run : TargetRun.Result Bound Unit) : MetaM Expr := do + let .target reached := run.stop + | throwError "interval_relu_tree: leaf did not reach its target" + let .ok registry := ProofRegistry.build run.session.registry reluSplitProofPackages + | throwError "interval_relu_tree: child proof registry failed" + let some trace := Frontend.trace? run.session.state.engine run.session.arena + | throwError "interval_relu_tree: child chronology quotation failed" + let (context, seed) ← + match source.input.initialFacts[0]? with + | some .nonnegative => + unless source.scope.index == 1 do + throwError "interval_relu_tree: left child has the wrong scope" + pure (reluLeftContext, mkConst ``reluLeftSeed) + | some .negative => + unless source.scope.index == 2 do + throwError "interval_relu_tree: right child has the wrong scope" + pure (reluRightContext, mkConst ``reluRightSeed) + | _ => throwError "interval_relu_tree: leaf has no split-side fact" + let state ← ProofFrontend.emitBranch context source.input seed trace.program + trace.events registry.emit + ProofFrontend.closeTarget context state reached.seen reached.fact source.input.target + +private meta def emitReluTreeSplit (source : BranchTree.Leaf Bound Unit) + (run : TargetRun.Result Bound Unit) (children : BranchStart.Children Bound) + (left right : Expr) : MetaM Expr := do + let .split plan := run.stop + | throwError "interval_relu_tree: internal node did not retain a split" + unless source.scope.index == 0 && + BranchProof.sameInput source.input reluInput && + BranchProof.sameInput children.parent reluInput && + BranchProof.sameInput children.left reluLeftInput && + BranchProof.sameInput children.right reluRightInput && + children.leftScope.index == 1 && children.rightScope.index == 2 && + plan.node == node 0 && plan.fact == .all && plan.point == 0 do + throwError "interval_relu_tree: retained split does not match the proof adapter" + let result ← + mkAppM ``ProofEmitter.replaySplit + #[mkConst ``reluSplitSchema, mkConst ``reluProgram, + mkConst ``reluBaseFacts, ← boundEncoder.nodeId (node 0), + ← boundEncoder.fact .all, mkConst ``Unit.unit, + ← boundEncoder.fact .nonnegative, ← boundEncoder.fact .negative, + ← boundEncoder.nodeFact reluInput.target, + mkConst ``reluParent, left, right] + ProofFrontend.replayResult result + +private def reluTreeEmitter : BranchProof.Emitter Bound Unit := + { leaf := emitReluTreeLeaf + split := emitReluTreeSplit } + +private def reluProofLimits : BranchProof.Limits := + { maxNodes := 16, maxDepth := 8 } + +/-- Unlike `reluJoined`, this ordinary proof term is produced by folding the +generic retained tree rather than by a fixed two-child orchestration. -/ +private def reluTreeJoined : Evidence + (reluSemantics.Entails reluProgram reluBaseFacts reluInput.target) := by + run_tac + let some tree := reluTree? + | throwError "interval_relu_tree: runtime tree failed" + let goal ← getMainGoal + goal.assign (← BranchProof.emit reluProofLimits reluTreeEmitter tree + (← goal.getType)) + +theorem tacticReluTree (x : ℝ) : 0 ≤ max x 0 := + closeRelu x reluTreeJoined + +/-- +info: 'Hex.IntervalMathlib.ReluConformance.tacticReluTree' depends on axioms: [propext, Classical.choice, Quot.sound] +-/ +#guard_msgs in +#print axioms tacticReluTree + +set_option linter.unusedTactic false in +example : True := by + run_tac + let expected ← inferType (mkConst ``reluJoined) + let partialResources := treeLimits (maxSteps := 1) + let some partialTree := reluTree? partialResources + | throwError "interval_relu_tree test: partial tree failed" + if (← observing? <| BranchProof.emit reluProofLimits reluTreeEmitter partialTree + expected).isSome then + throwError "interval_relu_tree test: pending children produced a proof" + let some tree := reluTree? + | throwError "interval_relu_tree test: complete tree failed" + let some root := tree.nodes[0]? + | throwError "interval_relu_tree test: root is missing" + let BranchTree.Node.split source run children left _ := root + | throwError "interval_relu_tree test: root is not a split" + let shared := + { tree with + nodes := tree.nodes.set! 0 + (BranchTree.Node.split source run children left left) } + if (← observing? <| BranchProof.emit reluProofLimits reluTreeEmitter shared + expected).isSome then + throwError "interval_relu_tree test: a shared sibling produced a proof" + let some extra := tree.nodes[1]? + | throwError "interval_relu_tree test: child is missing" + let unreachable := { tree with nodes := tree.nodes.push extra } + if (← observing? <| BranchProof.emit reluProofLimits reluTreeEmitter unreachable + expected).isSome then + throwError "interval_relu_tree test: an unreachable node produced a proof" + trivial + +set_option linter.unusedTactic false in +example : True := by + run_tac + let checkMutation (context : ProofFrontend.Context Bound Name) + (side wrong : Bound) (input : CheckerInput Bound) + (scope : Propagator.Policy.ScopeId) (seed : Expr) : MetaM Unit := do + let some run := reluRunChild? side input scope + | throwError "interval_relu_split mutation: child search failed" + let some trace := Frontend.trace? run.session.state.engine run.session.arena + | throwError "interval_relu_split mutation: trace missing" + let [.rule step] := trace.events + | throwError "interval_relu_split mutation: wrong trace shape" + let mutated : RuleStep Bound := + { step with assumptions := [reluBranchFact wrong] } + if (← observing? <| ProofFrontend.emitBranch context input seed trace.program + [.rule mutated] run.registry.emit).isSome then + throwError + "interval_relu_split mutation: opposite split assumption was accepted" + checkMutation reluLeftContext .nonnegative .negative reluLeftInput + { index := 1 } (mkConst ``reluLeftSeed) + checkMutation reluRightContext .negative .nonnegative reluRightInput + { index := 2 } (mkConst ``reluRightSeed) + trivial + +end Hex.IntervalMathlib.ReluConformance diff --git a/lakefile.lean b/lakefile.lean index 85f3a799b..7b6aaa8aa 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -309,6 +309,7 @@ lean_lib HexIntervalExperiment where `HexInterval.Experiment.TargetRun, `HexInterval.Experiment.BranchStart, `HexInterval.Experiment.BranchTree, + `HexInterval.Experiment.BranchProof, `HexInterval.Experiment.SemanticReplay, `HexInterval.Experiment.ChronologicalReplay, `HexInterval.Experiment.GenericInstanceReconstruction, @@ -399,7 +400,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, `HexInterval.SinTenIntervalConformance, `HexIntervalMathlib.SineSignConformance, `HexIntervalMathlib.SineProofConformance, `HexIntervalMathlib.SineTacticConformance, `HexIntervalMathlib.ProofRegistryConformance, `HexIntervalMathlib.ExpSignConformance, `HexIntervalMathlib.RefuteConformance, `HexIntervalMathlib.PntLogTableConformance, `HexIntervalMathlib.PntNestedLogConformance, `HexIntervalMathlib.SinTenConformance, `HexIntervalMathlib.SinTenIntervalConformance, `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, `HexInterval.SinTenIntervalConformance, `HexIntervalMathlib.SineSignConformance, `HexIntervalMathlib.SineProofConformance, `HexIntervalMathlib.SineTacticConformance, `HexIntervalMathlib.ProofRegistryConformance, `HexIntervalMathlib.ExpSignConformance, `HexIntervalMathlib.ReluConformance, `HexIntervalMathlib.RefuteConformance, `HexIntervalMathlib.PntLogTableConformance, `HexIntervalMathlib.PntNestedLogConformance, `HexIntervalMathlib.SinTenConformance, `HexIntervalMathlib.SinTenIntervalConformance, `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/20260811T174347Z.md b/progress/20260811T174347Z.md new file mode 100644 index 000000000..560c509d3 --- /dev/null +++ b/progress/20260811T174347Z.md @@ -0,0 +1,28 @@ +# Accomplished + +- Added a function-independent bottom-up emitter for settled retained branch + trees, with exact child-input checks and rejection of unfinished, shared, + cyclic, dangling, and unreachable nodes. +- Routed the branch-dependent `max x 0` example through that generic emitter: + both live child sessions replay their own function rule, and the root uses + the package-owned split theorem to produce one ordinary Lean theorem. +- Split the ReLU client into its own conformance module so both conformance + files remain within the repository line limits. +- Added negative checks for partial trees, shared children, and unreachable + nodes, plus a compile-checked axiom report for the emitted theorem. + +# Current frontier + +The retained two-child tree now produces a kernel-checked proof without any +function cases in the generic tree fold. Scheduling is still tested only on a +single split, so depth-first and breadth-first behavior coincide. + +# Next step + +Add a nested live split with a side-sensitive policy. Use it to exercise both +frontier orders and then begin replacing the finite sign facts with an actual +open/closed/unbounded interval domain. + +# Blockers + +None. diff --git a/scripts/bench/proof_only_runtime_exemptions.json b/scripts/bench/proof_only_runtime_exemptions.json index 68ea6a1ee..c04061403 100644 --- a/scripts/bench/proof_only_runtime_exemptions.json +++ b/scripts/bench/proof_only_runtime_exemptions.json @@ -173,6 +173,12 @@ "current_blob": "85f3a799be1661b7624e63b28aa1f6996763d4e8", "reason": "Additionally registers the Mathlib-free nested-log chronology experiment, its proof-only real-semantics companion, and conformance module; the factorization service target and executable dependency graph are unchanged." }, + { + "path": "lakefile.lean", + "baseline_blob": "6dd80771ae2212333b2a9b925b52056e0037ff56", + "current_blob": "7b6aaa8aa8a5af86fb3de13fc11606499863c170", + "reason": "Additionally registers the isolated Mathlib-free HexInterval branch-proof experiment and its ReLU conformance module only; the factorization service target and executable dependency graph are unchanged." + }, { "path": "HexBerlekamp/FactorTacticTests.lean", "baseline_blob": "4063e15934a89c671ac72d201fa60c2ef6feaf59", From a2d1212a273a5d83532a78713c02e9f5fd8eea6f Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 11 Aug 2026 18:25:24 +0000 Subject: [PATCH 2/5] Tighten branch proof conformance dependencies --- HexInterval/SPEC/hex-interval.md | 22 ++++++++++------ .../HexIntervalMathlib/ReluConformance.lean | 10 ++++++-- progress/20260811T182509Z.md | 25 +++++++++++++++++++ 3 files changed, 47 insertions(+), 10 deletions(-) create mode 100644 progress/20260811T182509Z.md diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index c1379e426..6f59028ca 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -1713,14 +1713,20 @@ and that zero split or one-leaf budgets retain an explicitly blocked root. This runtime tree contains no proof evidence. The separate generic `BranchProof` frontend now folds a settled retained tree bottom-up. It first -binds every leaf and split result back to its exact scope, base program, -initial fact array, and target; checks that each child is the exact child input -stored by its parent; rejects pending, blocked, failed, dangling, shared, -cyclic, or unreachable nodes; then asks client callbacks to replay each closed -leaf and apply each package-owned split join. The final emitted expression must -have the requested Lean type. A callback can therefore cause rejection or -choose a different kernel-checkable proof, but tree data itself cannot become -evidence. +binds every leaf and split result back to its exact scope, base program, and +initial fact array. Each child is checked against the exact child input stored +by its parent, including that input's target. Pending, blocked, failed, +dangling, shared, cyclic, and unreachable nodes are rejected. Client callbacks +then replay each closed leaf and apply each package-owned split join; the final +emitted expression must have the requested Lean target type. A callback can +therefore cause rejection or choose a different kernel-checkable proof, but +tree data itself cannot become evidence. + +Every child admitted by a split's coverage theorem must eventually close by +replaying a proof of its target or by deriving a package-checked refutation. +A retained runtime result is not by itself a proof of closure: the leaf +callback must turn it into the corresponding kernel-checked evidence before +the bottom-up join can accept it. The useful ReLU canary now runs through this generic path. Its retained root has two exact live target children; the leaf callback invokes the unchanged diff --git a/conformance/HexIntervalMathlib/ReluConformance.lean b/conformance/HexIntervalMathlib/ReluConformance.lean index dffae4ccd..0df56122f 100644 --- a/conformance/HexIntervalMathlib/ReluConformance.lean +++ b/conformance/HexIntervalMathlib/ReluConformance.lean @@ -4,8 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ -import HexIntervalMathlib.ExpSignConformance +import HexIntervalMathlib.Experiment.ExpSign +import HexInterval.Experiment.GoalFrontend +import HexInterval.Experiment.GoalClosure +import HexInterval.Experiment.ProofFrontend +import HexInterval.Experiment.TargetRun +import HexInterval.Experiment.BranchStart +import HexInterval.Experiment.BranchTree import HexInterval.Experiment.BranchProof +import Mathlib.Lean.Elab.Tactic.Meta /-! # Branch-dependent function propagation conformance @@ -21,7 +28,6 @@ open Hex.Interval.Experiment open Propagator PolicySession SemanticReplay ChronologicalReplay ProofEmitter open Frontend FrontendEncoder ProofFrontend ProofRegistry GoalFrontend ExpSign open GoalClosure BranchStart -open Hex.IntervalMathlib.ExpSignConformance private def splitOffer? (view : Propagator.Policy.View Bound) : Option Propagator.Policy.OfferView := diff --git a/progress/20260811T182509Z.md b/progress/20260811T182509Z.md new file mode 100644 index 000000000..a7db1162d --- /dev/null +++ b/progress/20260811T182509Z.md @@ -0,0 +1,25 @@ +# Accomplished + +- Replaced the ReLU branch-proof conformance module's import of the complete + exponential conformance suite with the direct experiment and frontend + modules it actually uses. +- Made the retained-tree binding claim precise: runtime results bind scope, + program, and initial facts; exact child inputs bind targets; the final + emitted expression is checked against the requested target type. +- Restored the normative requirement that every covered child closes through + replayed target evidence or a package-checked refutation. +- Rebuilt the ReLU branch-proof conformance target successfully. + +# Current frontier + +The generic bottom-up tree fold and its branch-dependent ReLU client are ready +for exact-head review after these documentation and dependency repairs. + +# Next step + +Propagate this repaired base through the nested-tree and interval-domain stack, +then continue the arbitrary centered-function contractor. + +# Blockers + +None. From 9e72238f174c172c166624d1ef0e3c1186178a2c Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 14 Aug 2026 18:42:09 +0000 Subject: [PATCH 3/5] fix(interval): preserve branch proof fidelity --- HexInterval/SPEC/hex-interval.md | 8 +- .../HexIntervalMathlib/ReluConformance.lean | 78 +++++++++++++------ progress/20260811T174347Z.md | 2 +- progress/20260811T182509Z.md | 4 +- progress/20260814T184123Z.md | 33 ++++++++ 5 files changed, 96 insertions(+), 29 deletions(-) create mode 100644 progress/20260814T184123Z.md diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index 6f59028ca..5d388aab0 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -1728,12 +1728,12 @@ A retained runtime result is not by itself a proof of closure: the leaf callback must turn it into the corresponding kernel-checked evidence before the bottom-up join can accept it. -The useful ReLU canary now runs through this generic path. Its retained root -has two exact live target children; the leaf callback invokes the unchanged -generic chronology emitter with the side-specific proof registry, and the +The distinct-assumption ReLU canary now runs through this generic path. Its +retained root has two exact live target children; the leaf callback invokes the +unchanged generic chronology emitter with the side-specific proof registry, and the split callback applies `replaySplit`. The resulting expression is assigned to an ordinary declaration and its axiom report is compile-checked. Separate -negative tests reject the delivered fuel-limited partial tree, a fork whose +negative tests reject the delivered step-limited partial tree, a fork whose two edges share one child, and an otherwise valid but unreachable extra node. For best-bound mode, unfinished leaves must contribute their inherited parent fact to the global hull; they never inherit a tighter sibling fact. diff --git a/conformance/HexIntervalMathlib/ReluConformance.lean b/conformance/HexIntervalMathlib/ReluConformance.lean index 0df56122f..89ae1b614 100644 --- a/conformance/HexIntervalMathlib/ReluConformance.lean +++ b/conformance/HexIntervalMathlib/ReluConformance.lean @@ -15,10 +15,12 @@ import HexInterval.Experiment.BranchProof import Mathlib.Lean.Elab.Tactic.Meta /-! -# Branch-dependent function propagation conformance +# Distinct-assumption function propagation conformance This module checks that a retained split tree whose children use different -function-specific propagators can be folded into one kernel-checked proof. +function-specific propagators can be folded into one kernel-checked proof. The +conditional rules deliberately test branch-proof plumbing; the final ReLU +theorem is unconditional and does not mathematically require branching. -/ namespace Hex.IntervalMathlib.ReluConformance @@ -75,10 +77,12 @@ private def boundEncoder : FrontendEncoder.Encoder Bound := /-! ## Branch-dependent ReLU propagation Unlike exponential positivity, these two propagators are intentionally -conditional. The nonnegative-side rule proves `max x 0 = x` from `0 <= x`; -the negative-side rule proves `max x 0 = 0` from `x < 0`. The runtime and -proof packages know those two function-specific facts, while branch creation, -branch seeding, chronology replay, and the two-proof join stay generic. -/ +conditional. The nonnegative-side rule proves the output fact by rewriting +with `max x 0 = x` from `0 <= x`; the negative-side rule does so by rewriting +with `max x 0 = 0` from `x < 0`. This conditionality is a package-test design +choice for an unconditional final theorem. The runtime and proof packages +know those two function-specific facts, while branch creation, branch seeding, +chronology replay, and the two-proof join stay generic. -/ private def reluKey : OpKey := { name := "relu-sign.max-zero" } @@ -398,7 +402,7 @@ private def reluPrepared? : match result.stop with | .split plan => match BranchStart.prepare branchLimits - (BranchStart.State.start { index := 0 }) 0 result.session plan + (BranchStart.State.start result.session) result.session plan reluInput.target signSplitter with | .ok (_, children) => some (ULift.up children) | .error _ => none @@ -518,14 +522,11 @@ private def reluTree? (resources : BranchTree.Limits := treeLimits) : #guard reluPrepared?.any fun lifted => let children := lifted.down - children.leftScope == ({ index := 1 } : Propagator.Policy.ScopeId) && + children.depth == 1 && BranchProof.sameInput children.parent reluInput && + children.leftScope == ({ index := 1 } : Propagator.Policy.ScopeId) && children.rightScope == ({ index := 2 } : Propagator.Policy.ScopeId) && - children.left.baseProgram == reluLeftInput.baseProgram && - children.left.initialFacts == reluLeftInput.initialFacts && - children.left.target == reluLeftInput.target && - children.right.baseProgram == reluRightInput.baseProgram && - children.right.initialFacts == reluRightInput.initialFacts && - children.right.target == reluRightInput.target + BranchProof.sameInput children.left reluLeftInput && + BranchProof.sameInput children.right reluRightInput private def reluTraceUses? (side : Bound) (input : CheckerInput Bound) (scope : Propagator.Policy.ScopeId) : Bool := @@ -536,8 +537,18 @@ private def reluTraceUses? (side : Bound) (input : CheckerInput Bound) | some trace => match trace.events with | [.rule step] => - step.assumptions == [reluBranchFact side] && + trace.program == input.baseProgram && + run.reached.seen == + ({ node := node 1, version := 1 } : SeenVersion) && + run.reached.fact == .nonnegative && + run.session.state.engine.facts == #[side, .nonnegative] && + run.session.state.engine.versions == #[0, 1] && + step.assumptions == [reluBranchFact side] && + step.event.programVersion == 0 && step.event.node == node 1 && + step.event.previous == + ({ node := node 1, version := 0 } : SeenVersion) && step.event.fact == .nonnegative && + step.event.version == 1 && step.previous == .all && step.entry.replayKey == (if side == .nonnegative then reluNonnegativeSchema.key else reluNegativeSchema.key) @@ -610,6 +621,22 @@ private meta def emitReluChild (context : ProofFrontend.Context Bound Name) | throwError "interval_relu_split: child search failed" let some trace := Frontend.trace? run.session.state.engine run.session.arena | throwError "interval_relu_split: child chronology quotation failed" + let [.rule step] := trace.events + | throwError "interval_relu_split: child trace is not exactly one rule" + let expectedKey := + if side == .nonnegative then reluNonnegativeSchema.key + else reluNegativeSchema.key + unless trace.program == input.baseProgram && + run.reached.seen == ({ node := node 1, version := 1 } : SeenVersion) && + run.reached.fact == .nonnegative && + run.session.state.engine.facts == #[side, .nonnegative] && + run.session.state.engine.versions == #[0, 1] && + step.assumptions == [reluBranchFact side] && + step.event.programVersion == 0 && step.event.node == node 1 && + step.event.previous == ({ node := node 1, version := 0 } : SeenVersion) && + step.event.fact == .nonnegative && step.event.version == 1 && + step.previous == .all && step.entry.replayKey == expectedKey do + throwError "interval_relu_split: child result or quoted rule trace drifted" let state ← ProofFrontend.emitBranch context input seed trace.program trace.events run.registry.emit ProofFrontend.closeTarget context state run.reached.seen run.reached.fact input.target @@ -641,12 +668,19 @@ private def reluJoined : Evidence let goal ← getMainGoal goal.assign (← emitReluSplit) -/-- A genuinely branch-dependent arbitrary-function vertical: neither ReLU -propagator fires before the zero split, and each child proof consumes its own -strictly narrower source fact before the generic join closes the theorem. -/ -theorem tacticReluSplit (x : ℝ) : 0 ≤ max x 0 := +/-- An arbitrary-function vertical whose child proofs consume distinct split +assumptions by construction: neither ReLU propagator fires before the zero +split. The final theorem is unconditional; conditionality here tests the +branch proof plumbing rather than mathematical necessity. -/ +theorem reluSplit (x : ℝ) : 0 ≤ max x 0 := closeRelu x reluJoined +/-- +info: 'Hex.IntervalMathlib.ReluConformance.reluSplit' depends on axioms: [propext, Classical.choice, Quot.sound] +-/ +#guard_msgs in +#print axioms reluSplit + private meta def emitReluTreeLeaf (source : BranchTree.Leaf Bound Unit) (run : TargetRun.Result Bound Unit) : MetaM Expr := do let .target reached := run.stop @@ -711,14 +745,14 @@ private def reluTreeJoined : Evidence goal.assign (← BranchProof.emit reluProofLimits reluTreeEmitter tree (← goal.getType)) -theorem tacticReluTree (x : ℝ) : 0 ≤ max x 0 := +theorem reluTree (x : ℝ) : 0 ≤ max x 0 := closeRelu x reluTreeJoined /-- -info: 'Hex.IntervalMathlib.ReluConformance.tacticReluTree' depends on axioms: [propext, Classical.choice, Quot.sound] +info: 'Hex.IntervalMathlib.ReluConformance.reluTree' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in -#print axioms tacticReluTree +#print axioms reluTree set_option linter.unusedTactic false in example : True := by diff --git a/progress/20260811T174347Z.md b/progress/20260811T174347Z.md index 560c509d3..62a711d78 100644 --- a/progress/20260811T174347Z.md +++ b/progress/20260811T174347Z.md @@ -3,7 +3,7 @@ - Added a function-independent bottom-up emitter for settled retained branch trees, with exact child-input checks and rejection of unfinished, shared, cyclic, dangling, and unreachable nodes. -- Routed the branch-dependent `max x 0` example through that generic emitter: +- Routed the distinct-assumption `max x 0` example through that generic emitter: both live child sessions replay their own function rule, and the root uses the package-owned split theorem to produce one ordinary Lean theorem. - Split the ReLU client into its own conformance module so both conformance diff --git a/progress/20260811T182509Z.md b/progress/20260811T182509Z.md index a7db1162d..b2b8e1893 100644 --- a/progress/20260811T182509Z.md +++ b/progress/20260811T182509Z.md @@ -12,8 +12,8 @@ # Current frontier -The generic bottom-up tree fold and its branch-dependent ReLU client are ready -for exact-head review after these documentation and dependency repairs. +The generic bottom-up tree fold and its distinct-assumption ReLU client are +ready for exact-head review after these documentation and dependency repairs. # Next step diff --git a/progress/20260814T184123Z.md b/progress/20260814T184123Z.md new file mode 100644 index 000000000..ca0945cbc --- /dev/null +++ b/progress/20260814T184123Z.md @@ -0,0 +1,33 @@ +# PR #9225 local preparation + +## Accomplished + +- Replayed only the generic bottom-up branch-proof feature onto exact merged + #9224 main `22d293dd6f2e6a29ba49961ea40496cd7194fce5`. +- Preserved current refutation, PNT-log, Machin, endpoint-sine, and retained + runtime-tree content while moving the ReLU client into its own conformance + module. +- Updated the extracted ReLU client to the sealed session-owned branch-start + API and restored the exact parent, child, scope, chronology, rule-key, + version, and installed-fact guards from the merged ReLU vertical. +- Kept both ordinary ReLU theorems honestly named and documented as + distinct-assumption plumbing for an unconditional result, with guarded axiom + reports. +- Audited the generic fold's shape checks, traversal bounds, source/run and + child-input binding, callback trust boundary, and final kernel type check. +- Refreshed the exact lakefile freshness exemption for registering only the + Mathlib-free branch-proof module and its ReLU conformance client. + +## Current frontier + +- The local feature candidate builds its focused modules. It is intentionally + unpushed while #9260 prepares the final upstream base. + +## Next step + +- Rebase once onto the final post-#9260 main, rerun focused/static checks, then + push and obtain fresh exact-head review and CI. + +## Blockers + +- None. From 99c058f69c9835809bcfed5d773f0c221e4fe744 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 14 Aug 2026 19:07:09 +0000 Subject: [PATCH 4/5] docs(interval): record final branch proof reconciliation --- progress/20260814T190655Z.md | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 progress/20260814T190655Z.md diff --git a/progress/20260814T190655Z.md b/progress/20260814T190655Z.md new file mode 100644 index 000000000..78be2b421 --- /dev/null +++ b/progress/20260814T190655Z.md @@ -0,0 +1,28 @@ +# PR #9225 final reconciliation + +## Accomplished + +- Rebased the prepared branch-proof feature onto exact post-#9260 main + `b083ed96f8ad05fa38d97f0f47d32981c1c5910a`. +- Preserved the merged nested-log registrations and all earlier interval, + PNT-log, Machin, and endpoint-sine content while retaining the audited + generic proof fold and ReLU conformance repairs. +- Recomputed the proof-only Lake freshness exemption against exact resolved + blob `7b6aaa8aa8a5af86fb3de13fc11606499863c170`. +- Rebuilt the focused branch-proof, ReLU, PNT nested-log, and sine targets and + reran the static, trust-surface, freshness, inventory, diff, and banned-term + checks successfully. + +## Current frontier + +- The exact reconciled candidate is ready to push for a fresh independent + review and exact-head CI. + +## Next step + +- Push and retarget PR #9225 to `main`, then require both fresh exact-head Opus + approval and exact-head CI success before marking it merge-ready. + +## Blockers + +- None. From 8c1633850c240531944958a32fd7181d324a6ce2 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 14 Aug 2026 19:17:57 +0000 Subject: [PATCH 5/5] docs(interval): remove delivered branch proof test from backlog --- HexInterval/SPEC/hex-interval.md | 3 +-- progress/20260814T190655Z.md | 11 +++++++---- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index 5d388aab0..945cef0a1 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -1773,8 +1773,7 @@ runtime and Mathlib semantic companion. Remaining acceptance tests include a theorem whose proof mathematically requires branching, a nested split, a child-local instantiation, a sibling-reference attack, a non-interior repeated split, -per-leaf fuel exhaustion with no theorem emitted, and proof emission refusing -the delivered step-limited partial tree. +and per-leaf fuel exhaustion with no theorem emitted. ### Proof-producing frontend diff --git a/progress/20260814T190655Z.md b/progress/20260814T190655Z.md index 78be2b421..fa6159a8a 100644 --- a/progress/20260814T190655Z.md +++ b/progress/20260814T190655Z.md @@ -12,16 +12,19 @@ - Rebuilt the focused branch-proof, ReLU, PNT nested-log, and sine targets and reran the static, trust-surface, freshness, inventory, diff, and banned-term checks successfully. +- Removed the stale remaining-acceptance-test entry for the already delivered + step-limited partial-tree rejection after the fresh review identified the + contradictory SPEC wording. ## Current frontier -- The exact reconciled candidate is ready to push for a fresh independent - review and exact-head CI. +- The reconciled candidate includes only the narrow SPEC honesty repair after + the reviewed code head. ## Next step -- Push and retarget PR #9225 to `main`, then require both fresh exact-head Opus - approval and exact-head CI success before marking it merge-ready. +- Require fresh exact-head Opus approval and superseding exact-head CI success + before marking PR #9225 merge-ready. ## Blockers