interval: seed proofs for child branch replay

HexInterval/Experiment/FrontendEncoder.lean

@@ -28,6 +28,7 @@ open Propagator PayloadArena SemanticReplay ProofEmitter
 /-- Reification boundary for a frontend's concrete fact representation. -/
 structure Encoder (Fact : Type) where
   program : Program → MetaM Expr
+  input : CheckerInput Fact → MetaM Expr
   nodeId : NodeId → MetaM Expr
   node : Node → MetaM Expr
   fact : Fact → MetaM Expr
@@ -181,6 +182,13 @@ def nodeFactExpr (factExpr : Fact → MetaM Expr) (fact : NodeFact Fact) :
     MetaM Expr :=
   do mkAppM ``NodeFact.mk #[← nodeIdExpr fact.node, ← factExpr fact.fact]
 
+def checkerInputExpr (factType : Expr) (factExpr : Fact → MetaM Expr)
+    (input : CheckerInput Fact) : MetaM Expr := do
+  mkAppM ``CheckerInput.mk
+    #[← programExpr input.baseProgram,
+      ← arrayExpr factType (← input.initialFacts.toList.mapM factExpr),
+      ← nodeFactExpr factExpr input.target]
+
 def edgeExpr (edge : EqualityEdge) : MetaM Expr := do
   mkAppM ``EqualityEdge.mk
     #[← nodeIdExpr edge.left,
@@ -242,6 +250,7 @@ def transportStepExpr (factType : Expr) (factExpr : Fact → MetaM Expr)
 /-- Build the complete generic encoder from one fact-value encoder. -/
 def make (factType : Expr) (factExpr : Fact → MetaM Expr) : Encoder Fact :=
   { program := programExpr
+    input := checkerInputExpr factType factExpr
     nodeId := nodeIdExpr
     node := nodeExpr
     fact := factExpr

HexInterval/Experiment/ProofEmitter.lean

@@ -539,6 +539,18 @@ structure BranchSeed {Fact : Type} (semantics : Semantics Fact)
 
 namespace BranchSeed
 
+/-- Select one child-root fact while explicitly pinning the exact checker
+input and complete child assumption list used by the frontend. -/
+def get {Fact : Type} (semantics : Semantics Fact) (input : CheckerInput Fact)
+    (childBase : List (NodeFact Fact)) {base : List (NodeFact Fact)}
+    {side : NodeFact Fact} (seed : BranchSeed semantics input base side)
+    (same : childBase = side :: base) (node : NodeId) (fact : Fact)
+    (found : input.initialFacts[node.index]? = some fact) :
+    Evidence
+      (semantics.Entails input.baseProgram childBase { node, fact }) := by
+  subst childBase
+  exact seed.sound node fact found
+
 /-- Assemble a branch root from the one new case assumption and exact proofs
 of all nonsplit parent consequences. -/
 def make {Fact : Type} {semantics : Semantics Fact}

HexInterval/Experiment/ProofFrontend.lean

@@ -184,6 +184,47 @@ def seedBase (context : Context Fact Handle) (program : Expr) (basePrefix : Expr
         proof }
   pure known
 
+/-- Seed every version-zero fact of a restarted child from its exact branch
+proof table.  The runtime input only selects concrete array entries; applying
+`BranchSeed.get` forces the supplied Lean expression to describe that same
+input and child context. -/
+def seedBranch (encoder : Encoder Fact) (semantics input childBase : Expr)
+    (inputValue : CheckerInput Fact) (seed : Expr) :
+    MetaM (List (FactProof Fact)) := do
+  unless inputValue.initialFacts.size == inputValue.baseProgram.nodes.size do
+    throwError "interval frontend: branch facts do not cover the child graph"
+  unless ← isDefEq (← encoder.input inputValue) input do
+    throwError "interval frontend: branch proof uses a different checker input"
+  let program ← encoder.program inputValue.baseProgram
+  let mut known := []
+  for index in [0:inputValue.initialFacts.size] do
+    let node : NodeId := { index }
+    let some fact := inputValue.initialFacts[index]?
+      | throwError "interval frontend: branch fact index escaped its table"
+    let some instruction := inputValue.baseProgram.nodes[index]?
+      | throwError "interval frontend: branch node index escaped its program"
+    let nodeTerm ← encoder.nodeId node
+    let factTerm ← encoder.fact fact
+    let someFact ← mkAppM ``Option.some #[factTerm]
+    let factFound ← mkAppM ``Eq.refl #[someFact]
+    let sameBase ← mkAppM ``Eq.refl #[childBase]
+    let proof ←
+      mkAppM ``ProofEmitter.BranchSeed.get
+        #[semantics, input, childBase, seed, sameBase,
+          nodeTerm, factTerm, factFound]
+    let instructionTerm ← encoder.node instruction
+    let someInstruction ← mkAppM ``Option.some #[instructionTerm]
+    let nodeFound ← mkAppM ``Eq.refl #[someInstruction]
+    let within ←
+      mkAppM ``ProofEmitter.nodeWithin
+        #[program, nodeTerm, instructionTerm, nodeFound]
+    known ← insertProof known
+      { seen := { node, version := 0 }
+        fact
+        within
+        proof }
+  pure known
+
 /-- Seed domain-top evidence for exactly one instance's fresh-node suffix. -/
 def seedNew [BEq Fact] (context : Context Fact Handle) (programValue : Program)
     (program : Expr) (newNodes : List NodeId) (known : List (FactProof Fact)) :
@@ -348,15 +389,23 @@ def emitEvents [BEq Fact] (context : Context Fact Handle) (finalValue : Program)
       let state ← emitTransport context state table step
       emitEvents context finalValue finalProgram table rest state
 
-/-- Emit the complete generic state for one final program and chronology. -/
-def emitTrace [BEq Fact] (context : Context Fact Handle) (programValue : Program)
-    (events : List (Frontend.Event Fact)) (table : SchemaTable Handle) :
-    MetaM (State Fact) := do
+/-- Low-level fold from an already authenticated version-zero proof table.
+
+Every entry in `known` must contain a proof over `context.baseProgramTerm` and
+`context.baseFactsTerm`, with a node bound for that same program.  This helper
+does not establish that precondition; public callers should normally use
+`emitTrace` or `emitBranch`, which construct the table through the appropriate
+checked root.  A malformed raw table cannot create a kernel proof, because
+each stored expression is typechecked when a replay step or target consumes
+it. -/
+def emitSeeded [BEq Fact] (context : Context Fact Handle)
+    (programValue : Program)
+    (events : List (Frontend.Event Fact)) (table : SchemaTable Handle)
+    (known : List (FactProof Fact)) : MetaM (State Fact) := do
   unless programValue.check do
     throwError "interval frontend: final expression program is not checked"
   let finalProgram ← context.encoder.program programValue
   let snapshot ← initialSnapshot context finalProgram
-  let known ← seedBase context context.baseProgramTerm context.basePrefix
   let initial : State Fact :=
     { version := 0
       programValue := context.baseProgram
@@ -371,4 +420,27 @@ def emitTrace [BEq Fact] (context : Context Fact Handle) (programValue : Program
     throwError "interval frontend: trace did not consume the complete final program"
   pure state
 
+/-- Emit the complete generic state for one caller-rooted chronology. -/
+def emitTrace [BEq Fact] (context : Context Fact Handle) (programValue : Program)
+    (events : List (Frontend.Event Fact)) (table : SchemaTable Handle) :
+    MetaM (State Fact) := do
+  let known ← seedBase context context.baseProgramTerm context.basePrefix
+  emitSeeded context programValue events table known
+
+/-- Emit a restarted child chronology without reclassifying inherited parent
+consequences as caller assumptions. -/
+def emitBranch [BEq Fact] (context : Context Fact Handle)
+    (inputValue : CheckerInput Fact) (seed : Expr) (programValue : Program)
+    (events : List (Frontend.Event Fact)) (table : SchemaTable Handle) :
+    MetaM (State Fact) := do
+  unless inputValue.baseProgram == context.baseProgram do
+    throwError "interval frontend: branch seed uses a different base program"
+  unless ← isDefEq (← context.encoder.program inputValue.baseProgram)
+      context.baseProgramTerm do
+    throwError "interval frontend: branch context quotes a different base program"
+  let known ←
+    seedBranch context.encoder context.semantics context.input
+      context.baseFactsTerm inputValue seed
+  emitSeeded context programValue events table known
+
 end Hex.Interval.Experiment.ProofFrontend

HexInterval/SPEC/hex-interval.md

@@ -1577,9 +1577,18 @@ child `initialFacts` array and its length to this mixed proof table. Its checked
 builder obtains the split-node entry only from the new child assumption and
 requires an inherited parent theorem for every other array entry; the
 Mathlib-free canary checks both routes, including an inherited derived fact
-which is not a literal parent base member and an unrelated top entry. The Meta
-frontend still needs to turn such a `BranchSeed` into version-zero `FactProof`
-records before chronological child replay.
+which is not a literal parent base member and an unrelated top entry. The
+generic Meta frontend now quotes
+the complete child `CheckerInput`, rejects any mismatch in its program, fact
+array, or target, pins the full child assumption list, and turns the seed into
+exact version-zero `FactProof` records. Its branch entry point then uses the
+unchanged function-independent chronology fold. A live child session and a
+nonempty child event trace remain the next end-to-end branch experiment.
+The shared `emitSeeded` fold is a low-level Meta helper: its raw proof table
+must already refer to the context's quoted base program and child assumptions.
+The caller-root and branch-root entry points establish that precondition via
+`seedBase` and `seedBranch`; later replay use sites still typecheck every
+stored proof expression and fail closed on a mismatch.
 
 Branches may instantiate different auxiliary expressions. Each child replay
 therefore closes its target back to the program snapshot at the split before

conformance/HexInterval/ProofEmitterConformance.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 
-import HexInterval.Experiment.ProofEmitter
+import HexInterval.Experiment.ProofFrontend
 import HexInterval.PolicyFunctionConformance
 
 /-!
@@ -18,6 +18,7 @@ namespace Hex.Interval.ProofEmitterConformance
 
 open Experiment Propagator PayloadArena SemanticReplay ChronologicalReplay
 open PolicyFunctionConformance
+open Lean Meta
 
 def base : List (NodeFact Rank) :=
   [{ node := node 0, fact := 0 }]
@@ -333,6 +334,9 @@ def branchBase : List (NodeFact SplitFact) :=
 literal fact in `branchBase`. -/
 def branchInitial : Array SplitFact := #[.yes, .enabled, .all]
 
+def branchFacts : List (NodeFact SplitFact) :=
+  { node := splitNode, fact := .yes } :: branchBase
+
 def branchInput : CheckerInput SplitFact :=
   { baseProgram := program
     initialFacts := branchInitial
@@ -372,19 +376,29 @@ def branchSeed :
     (by rfl) (by rfl) inheritedSplitFact
 
 /-- The split node is proved from the new child assumption. -/
+def branchSide : Evidence
+    (splitSemantics.Entails program branchFacts
+      { node := splitNode, fact := .yes }) :=
+  branchSeed.sound splitNode .yes (by rfl)
+
 example :
     splitSemantics.Entails program
       ({ node := splitNode, fact := .yes } :: branchBase)
       { node := splitNode, fact := .yes } :=
-  (branchSeed.sound splitNode .yes (by rfl)).proof
+  branchSide.proof
 
 /-- A derived version-zero fact is inherited as a parent consequence under the
 larger child context. -/
+def branchInherited : Evidence
+    (splitSemantics.Entails program branchFacts
+      { node := splitBaseNode, fact := .enabled }) :=
+  branchSeed.sound splitBaseNode .enabled (by rfl)
+
 example :
     splitSemantics.Entails program
       ({ node := splitNode, fact := .yes } :: branchBase)
       { node := splitBaseNode, fact := .enabled } :=
-  (branchSeed.sound splitBaseNode .enabled (by rfl)).proof
+  branchInherited.proof
 
 /-- The inherited child fact above is a proved consequence, not a literal
 member of the parent base-assumption list. -/
@@ -401,4 +415,97 @@ example :
       { node := splitTargetNode, fact := .all } :=
   (branchSeed.sound splitTargetNode .all (by rfl)).proof
 
+private def splitFactExpr : SplitFact → Expr
+  | .all => mkConst ``SplitFact.all
+  | .yes => mkConst ``SplitFact.yes
+  | .no => mkConst ``SplitFact.no
+  | .enabled => mkConst ``SplitFact.enabled
+  | .certified => mkConst ``SplitFact.certified
+
+private def splitEncoder : FrontendEncoder.Encoder SplitFact :=
+  FrontendEncoder.make (mkConst ``SplitFact)
+    (fun fact => pure (splitFactExpr fact))
+
+private theorem branchPrefix : ProgramPrefix program program :=
+  ProgramPrefix.refl program
+
+private theorem branchSameOperations : program.operations = program.operations :=
+  rfl
+
+/-- The Meta frontend obtains the branch assumption and every inherited entry
+from the exact child-input-indexed proof table. -/
+example : True := by
+  run_tac
+    let inputTerm ← splitEncoder.input branchInput
+    unless ← isDefEq inputTerm (mkConst ``branchInput) do
+      throwError "branch seed test: checker-input quotation is not canonical"
+    let known ←
+      ProofFrontend.seedBranch splitEncoder (mkConst ``splitSemantics)
+        (mkConst ``branchInput) (mkConst ``branchFacts) branchInput
+        (mkConst ``branchSeed)
+    let some side :=
+        ProofFrontend.findFact? known { node := splitNode, version := 0 } .yes
+      | throwError "branch seed test: split assumption is missing"
+    let some inherited :=
+        ProofFrontend.findFact? known { node := splitBaseNode, version := 0 } .enabled
+      | throwError "branch seed test: inherited parent fact is missing"
+    let some top :=
+        ProofFrontend.findFact? known { node := splitTargetNode, version := 0 } .all
+      | throwError "branch seed test: unrelated top fact is missing"
+    unless ← isDefEq (← inferType side.proof) (← inferType (mkConst ``branchSide)) do
+      throwError "branch seed test: split proof has the wrong proposition"
+    unless ← isDefEq (← inferType inherited.proof)
+        (← inferType (mkConst ``branchInherited)) do
+      throwError "branch seed test: inherited proof has the wrong proposition"
+    unless top.seen.node == splitTargetNode && top.fact == .all do
+      throwError "branch seed test: unrelated top fact has the wrong identity"
+    let wrongInput : CheckerInput SplitFact :=
+      { branchInput with target := { node := node 1, fact := .yes } }
+    if (← observing? <| ProofFrontend.seedBranch splitEncoder
+        (mkConst ``splitSemantics) (mkConst ``branchInput)
+        (mkConst ``branchFacts) wrongInput (mkConst ``branchSeed)).isSome then
+      throwError "branch seed test: mismatched checker input was accepted"
+    if (← observing? <| ProofFrontend.seedBranch splitEncoder
+        (mkConst ``splitSemantics) (mkConst ``branchInput)
+        (mkConst ``branchBase) branchInput (mkConst ``branchSeed)).isSome then
+      throwError "branch seed test: mismatched child assumptions were accepted"
+    let context : ProofFrontend.Context SplitFact Unit :=
+      { encoder := splitEncoder
+        resolveSchema := fun _ => throwError "branch seed test: unexpected schema lookup"
+        semantics := mkConst ``splitSemantics
+        domain := mkConst ``True
+        laws := mkConst ``True
+        stableLaw := mkConst ``True
+        input := mkConst ``branchInput
+        assumed := ``ProofEmitter.assumedAt
+        baseFacts := branchFacts
+        baseFactsTerm := mkConst ``branchFacts
+        baseProgram := program
+        baseProgramTerm := mkConst ``program
+        basePrefix := mkConst ``branchPrefix
+        baseWithin := mkConst ``True.intro
+        initialExtension := mkConst ``True.intro
+        finalPrefix := mkConst ``branchPrefix
+        sameOperations := mkConst ``branchSameOperations
+        top := fun _ => .all }
+    let emptyTable : ProofEmitter.SchemaTable Unit :=
+      { entries := [], unique := by rfl }
+    let state ← ProofFrontend.emitBranch context branchInput
+      (mkConst ``branchSeed) program [] emptyTable
+    unless state.known.length == branchInitial.size do
+      throwError "branch emitter test: not every seed entry reached the replay state"
+    unless (ProofFrontend.findFact? state.known
+        { node := splitNode, version := 0 } .yes).isSome &&
+      (ProofFrontend.findFact? state.known
+        { node := splitBaseNode, version := 0 } .enabled).isSome &&
+      (ProofFrontend.findFact? state.known
+        { node := splitTargetNode, version := 0 } .all).isSome do
+      throwError "branch emitter test: the public bridge dropped a seed entry"
+    let wrongProgramContext :=
+      { context with baseProgramTerm := mkConst ``extendedProgram }
+    if (← observing? <| ProofFrontend.emitBranch wrongProgramContext branchInput
+        (mkConst ``branchSeed) program [] emptyTable).isSome then
+      throwError "branch emitter test: mismatched base-program term was accepted"
+  trivial
+
 end Hex.Interval.ProofEmitterConformance

progress/20260811T150500Z.md

@@ -0,0 +1,28 @@
+# Accomplished
+
+- Added exact `CheckerInput` quotation to the shared function-independent
+  frontend encoder.
+- Added branch-root seeding which converts every authenticated child
+  version-zero fact into the ordinary proof table used by chronological replay.
+- Pinned both the complete child input and the complete child assumption list
+  before any inherited proof is accepted; negative tests reject drift in
+  either value.
+- Added `emitBranch`, which feeds the branch proof table into the unchanged
+  generic event fold without treating inherited consequences as assumptions.
+- Rebuilt the Mathlib-free proof-emitter conformance and both sine and
+  exponential frontend conformance targets successfully.
+
+# Current frontier
+
+The proof frontend can now initialize a child chronology soundly. It has not
+yet run a live child engine session or replayed a nonempty child event list.
+
+# Next step
+
+Restart or fork a checked policy session from one branch input, run an
+arbitrary function propagator in that child, replay the child trace with
+`emitBranch`, and join the two child target proofs through `replaySplit`.
+
+# Blockers
+
+None.

progress/20260811T151000Z.md

@@ -0,0 +1,21 @@
+# Accomplished
+
+- Rebuilt the branch frontend through both arbitrary-function tactic
+  conformance targets.
+- Corrected the shared seeded-fold helper's module visibility so the public
+  caller-rooted and branch-rooted entry points compile under Lean's module
+  system.
+
+# Current frontier
+
+Exact child input and assumption validation, branch evidence seeding, and the
+generic child replay entry point all compile together.
+
+# Next step
+
+Exercise the entry point on a live child session with a nonempty arbitrary
+function trace and join both child results through the split schema.
+
+# Blockers
+
+None.