From 885ddba5c28d625b9394a0cc4dbd1de610f9f2e7 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 11 Aug 2026 17:22:51 +0000 Subject: [PATCH 1/3] Propagate provenance honesty through branch seeds; progress 20260811T171522Z --- HexInterval/Experiment/ProofEmitter.lean | 65 +++++++++++++++++++ HexInterval/SPEC/hex-interval.md | 9 ++- .../HexInterval/ProofEmitterConformance.lean | 55 ++++++++++++++++ progress/20260811T144508Z.md | 23 +++++++ progress/20260811T145500Z.md | 24 +++++++ progress/20260811T150000Z.md | 21 ++++++ progress/20260811T165035Z.md | 21 ++++++ progress/20260811T170207Z.md | 18 +++++ 8 files changed, 234 insertions(+), 2 deletions(-) create mode 100644 progress/20260811T144508Z.md create mode 100644 progress/20260811T145500Z.md create mode 100644 progress/20260811T150000Z.md create mode 100644 progress/20260811T165035Z.md create mode 100644 progress/20260811T170207Z.md diff --git a/HexInterval/Experiment/ProofEmitter.lean b/HexInterval/Experiment/ProofEmitter.lean index 41444fc62..fdb735216 100644 --- a/HexInterval/Experiment/ProofEmitter.lean +++ b/HexInterval/Experiment/ProofEmitter.lean @@ -501,6 +501,71 @@ def replaySplit {Fact Cut : Type} {semantics : Semantics Fact} let cover <- schema.proveCover program node parent cut left right pure (installSplit cover parentSound leftSound rightSound) +/-! ## Provenance-safe branch roots -/ + +/-- An established parent fact remains established after adding one child +case assumption. -/ +def inheritSplit {Fact : Type} {semantics : Semantics Fact} + {program : Program} {base : List (NodeFact Fact)} + (side fact : NodeFact Fact) + (sound : Evidence (semantics.Entails program base fact)) : + Evidence (semantics.Entails program (side :: base) fact) := + { proof := by + intro valuation model branchHolds + apply sound.proof valuation model + intro assumption member + exact branchHolds assumption (List.mem_cons_of_mem side member) } + +/-- The exact child case is available as the sole new branch assumption. -/ +def assumeSplit {Fact : Type} {semantics : Semantics Fact} + (program : Program) (base : List (NodeFact Fact)) (side : NodeFact Fact) : + Evidence (semantics.Entails program (side :: base) side) := + assumed (by simp) + +/-- Proof table for every version-zero fact of a restarted child session. + +The exact array is runtime data, but each entry must already have an ordinary +proof under the child context. Inherited parent consequences therefore cannot +be silently reclassified as caller assumptions. -/ +structure BranchSeed {Fact : Type} (semantics : Semantics Fact) + (input : CheckerInput Fact) (base : List (NodeFact Fact)) + (side : NodeFact Fact) where + size : input.initialFacts.size = input.baseProgram.nodes.size + sound : + (node : NodeId) -> (fact : Fact) -> + input.initialFacts[node.index]? = some fact -> + Evidence + (semantics.Entails input.baseProgram (side :: base) { node, fact }) + +namespace BranchSeed + +/-- Assemble a branch root from the one new case assumption and exact proofs +of all unchanged parent facts. -/ +def make {Fact : Type} {semantics : Semantics Fact} + (input : CheckerInput Fact) {base : List (NodeFact Fact)} + (side : NodeFact Fact) + (size : input.initialFacts.size = input.baseProgram.nodes.size) + (sideAt : input.initialFacts[side.node.index]? = some side.fact) + (inherited : + (node : NodeId) -> node ≠ side.node -> (fact : Fact) -> + input.initialFacts[node.index]? = some fact -> + Evidence + (semantics.Entails input.baseProgram base { node, fact })) : + BranchSeed semantics input base side := + { size + sound := by + intro node fact found + if same : node = side.node then + subst node + have factEq : fact = side.fact := + Option.some.inj (found.symm.trans sideAt) + subst fact + exact assumeSplit input.baseProgram base side + else + exact inheritSplit side { node, fact } (inherited node same fact found) } + +end BranchSeed + /-- Close a requested fact from a stronger established fact at the same node. The independent fact-domain theorem must prove that intersecting `actual` with `requested` leaves `actual` unchanged. Runtime target detection is not used diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index cb7b144cd..487ac15ef 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -1572,8 +1572,13 @@ classify every entry as either: It must not feed all inherited derived facts to `ProofEmitter.assumed`: that would silently promote consequences of the caller's context into new caller hypotheses. The existing caller `InitialContext` is consequently not the -branch-root API. A `BranchSeed` experiment should bind the exact child -`initialFacts` array to this mixed proof table before chronological replay. +branch-root API. The transparent `ProofEmitter.BranchSeed` now binds the exact +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. The Meta frontend still needs to turn +such a `BranchSeed` into version-zero `FactProof` records before chronological +child replay. Branches may instantiate different auxiliary expressions. Each child replay therefore closes its target back to the program snapshot at the split before diff --git a/conformance/HexInterval/ProofEmitterConformance.lean b/conformance/HexInterval/ProofEmitterConformance.lean index ef944e944..352ca99ee 100644 --- a/conformance/HexInterval/ProofEmitterConformance.lean +++ b/conformance/HexInterval/ProofEmitterConformance.lean @@ -326,4 +326,59 @@ info: 'Hex.Interval.ProofEmitterConformance.splitCertifies' depends on axioms: [ #guard_msgs in #print axioms splitCertifies +def branchBase : List (NodeFact SplitFact) := + [{ node := node 1, fact := .yes }] + +def branchInitial : Array SplitFact := #[.yes, .yes, .all] + +def branchInput : CheckerInput SplitFact := + { baseProgram := program + initialFacts := branchInitial + target := splitTarget } + +def inheritedSplitFact (observed : NodeId) (different : observed ≠ splitNode) + (fact : SplitFact) (found : branchInitial[observed.index]? = some fact) : + Evidence + (splitSemantics.Entails program branchBase { node := observed, fact }) := + { proof := by + intro _ _ assumptions + cases observed with + | mk index => + cases index with + | zero => simp [splitNode, node] at different + | succ index => + cases index with + | zero => + simp [branchInitial] at found + subst fact + exact assumptions _ (by simp [branchBase, node]) + | succ index => + cases index with + | zero => + simp [branchInitial] at found + subst fact + trivial + | succ index => simp [branchInitial] at found } + +def branchSeed : + ProofEmitter.BranchSeed splitSemantics branchInput branchBase + { node := splitNode, fact := .yes } := + ProofEmitter.BranchSeed.make branchInput { node := splitNode, fact := .yes } + (by rfl) (by rfl) inheritedSplitFact + +/-- The split node is proved from the new child assumption. -/ +example : + splitSemantics.Entails program + ({ node := splitNode, fact := .yes } :: branchBase) + { node := splitNode, fact := .yes } := + (branchSeed.sound splitNode .yes (by rfl)).proof + +/-- An unchanged version-zero fact is inherited as a parent consequence under +the larger child context. -/ +example : + splitSemantics.Entails program + ({ node := splitNode, fact := .yes } :: branchBase) + { node := node 1, fact := .yes } := + (branchSeed.sound (node 1) .yes (by rfl)).proof + end Hex.Interval.ProofEmitterConformance diff --git a/progress/20260811T144508Z.md b/progress/20260811T144508Z.md new file mode 100644 index 000000000..b889c742b --- /dev/null +++ b/progress/20260811T144508Z.md @@ -0,0 +1,23 @@ +# Accomplished + +- Tightened `BranchSeed` so its program and version-zero fact array come from + one exact child `CheckerInput` rather than two independently supplied values. +- Strengthened the conformance fixture with a nonempty parent context and a + nontrivial inherited `.yes` fact at a different node. +- Rebuilt the Mathlib-free proof-emitter conformance target successfully. + +# Current frontier + +The child root now binds runtime input fidelity and proof provenance in the +same type. Its split-node fact comes from the new case assumption, while an +unchanged nontrivial fact is weakened from an established parent theorem. + +# Next step + +Have the generic Meta frontend seed its versioned evidence table from this +exact `BranchSeed`, then replay a child trace without treating inherited parent +consequences as caller assumptions. + +# Blockers + +None. diff --git a/progress/20260811T145500Z.md b/progress/20260811T145500Z.md new file mode 100644 index 000000000..b1fe7a948 --- /dev/null +++ b/progress/20260811T145500Z.md @@ -0,0 +1,24 @@ +# Accomplished + +- Added transparent weakening of inherited parent facts into a child context. +- Added the exact child case as the sole new branch assumption. +- Added `BranchSeed`, which binds every version-zero child fact and the complete + initial array length to ordinary evidence from one of those two routes. +- Added conformance coverage for the split node and an unchanged inherited + node. + +# Current frontier + +The proof-level child root is checked. The Meta frontend does not yet translate +it into version-zero `FactProof` records, and no child `PolicySession` is +started yet. + +# Next step + +Add a frontend seed fold over the exact child array, then connect it to a +restarted child session whose program snapshot is the split snapshot. + +# Blockers + +None for two target-closing children. Contradiction leaves still require the +separate refutation schema recorded in the SPEC. diff --git a/progress/20260811T150000Z.md b/progress/20260811T150000Z.md new file mode 100644 index 000000000..a9e78b2e7 --- /dev/null +++ b/progress/20260811T150000Z.md @@ -0,0 +1,21 @@ +# Accomplished + +- Bound branch version-zero proofs to the exact child `CheckerInput`. +- Made the inherited-fact route depend on a nonempty parent context rather + than a trivially true top fact. +- Completed focused conformance, repository-structure, trust, and freshness + checks; a fresh independent review approved the repaired design. + +# Current frontier + +The branch seed now distinguishes the one new split assumption from parent +facts that retain their existing proofs under the larger child context. + +# Next step + +Use this seed in the generic proof frontend to initialize exact version-zero +`FactProof` records for chronological child replay. + +# Blockers + +None. diff --git a/progress/20260811T165035Z.md b/progress/20260811T165035Z.md new file mode 100644 index 000000000..d89cacb9e --- /dev/null +++ b/progress/20260811T165035Z.md @@ -0,0 +1,21 @@ +# Accomplished + +- Reconciled authenticated branch seeding with the repaired split/join and + target-closure stack. +- Preserved exact child `CheckerInput` indexing and the distinction between + inherited parent proofs and the single conditional split assumption. + +# Current frontier + +Every child version-zero fact can be justified without promoting parent-derived +facts to caller assumptions. The seed is tied to the exact child program, +initial fact array, target, and branch side. + +# Next step + +Finish focused and static checks, push the exact head for review, then +reconcile Meta-level emission from authenticated branch seeds. + +# Blockers + +None. diff --git a/progress/20260811T170207Z.md b/progress/20260811T170207Z.md new file mode 100644 index 000000000..085dedfe0 --- /dev/null +++ b/progress/20260811T170207Z.md @@ -0,0 +1,18 @@ +# Accomplished + +- Propagated both compile-checked modeled-goal axiom reports through + authenticated branch seeding. + +# Current frontier + +Branch provenance and exact child-input binding are unchanged; inherited +goal-proof canaries retain their explicit standard-axiom checks. + +# Next step + +Push after checks, then continue through branch proof emission and live child +execution. + +# Blockers + +None. From face060f02a7935f641475112cddd757552f25ff Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 14 Aug 2026 10:42:21 +0000 Subject: [PATCH 2/3] Strengthen branch-seed provenance canary; progress 20260814T104145Z --- HexInterval/Experiment/ProofEmitter.lean | 2 +- HexInterval/SPEC/hex-interval.md | 7 ++-- .../HexInterval/ProofEmitterConformance.lean | 36 ++++++++++++++----- progress/20260814T104145Z.md | 33 +++++++++++++++++ 4 files changed, 66 insertions(+), 12 deletions(-) create mode 100644 progress/20260814T104145Z.md diff --git a/HexInterval/Experiment/ProofEmitter.lean b/HexInterval/Experiment/ProofEmitter.lean index fdb735216..ecf235968 100644 --- a/HexInterval/Experiment/ProofEmitter.lean +++ b/HexInterval/Experiment/ProofEmitter.lean @@ -540,7 +540,7 @@ structure BranchSeed {Fact : Type} (semantics : Semantics Fact) namespace BranchSeed /-- Assemble a branch root from the one new case assumption and exact proofs -of all unchanged parent facts. -/ +of all nonsplit parent consequences. -/ def make {Fact : Type} {semantics : Semantics Fact} (input : CheckerInput Fact) {base : List (NodeFact Fact)} (side : NodeFact Fact) diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index 487ac15ef..91db3656a 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -1576,9 +1576,10 @@ branch-root API. The transparent `ProofEmitter.BranchSeed` now binds the exact 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. The Meta frontend still needs to turn -such a `BranchSeed` into version-zero `FactProof` records before chronological -child replay. +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. Branches may instantiate different auxiliary expressions. Each child replay therefore closes its target back to the program snapshot at the split before diff --git a/conformance/HexInterval/ProofEmitterConformance.lean b/conformance/HexInterval/ProofEmitterConformance.lean index 352ca99ee..48d775f15 100644 --- a/conformance/HexInterval/ProofEmitterConformance.lean +++ b/conformance/HexInterval/ProofEmitterConformance.lean @@ -327,9 +327,11 @@ info: 'Hex.Interval.ProofEmitterConformance.splitCertifies' depends on axioms: [ #print axioms splitCertifies def branchBase : List (NodeFact SplitFact) := - [{ node := node 1, fact := .yes }] + [{ node := splitBaseNode, fact := .yes }] -def branchInitial : Array SplitFact := #[.yes, .yes, .all] +/-- The child carries a derived parent consequence at node one, not the +literal fact in `branchBase`. -/ +def branchInitial : Array SplitFact := #[.yes, .enabled, .all] def branchInput : CheckerInput SplitFact := { baseProgram := program @@ -341,7 +343,7 @@ def inheritedSplitFact (observed : NodeId) (different : observed ≠ splitNode) Evidence (splitSemantics.Entails program branchBase { node := observed, fact }) := { proof := by - intro _ _ assumptions + intro valuation _ assumptions cases observed with | mk index => cases index with @@ -351,7 +353,10 @@ def inheritedSplitFact (observed : NodeId) (different : observed ≠ splitNode) | zero => simp [branchInitial] at found subst fact - exact assumptions _ (by simp [branchBase, node]) + have yes := assumptions + { node := splitBaseNode, fact := .yes } + (by simp [branchBase]) + exact yes | succ index => cases index with | zero => @@ -373,12 +378,27 @@ example : { node := splitNode, fact := .yes } := (branchSeed.sound splitNode .yes (by rfl)).proof -/-- An unchanged version-zero fact is inherited as a parent consequence under -the larger child context. -/ +/-- A derived version-zero fact is inherited as a parent consequence under the +larger child context. -/ +example : + splitSemantics.Entails program + ({ node := splitNode, fact := .yes } :: branchBase) + { node := splitBaseNode, fact := .enabled } := + (branchSeed.sound splitBaseNode .enabled (by rfl)).proof + +/-- The inherited child fact above is a proved consequence, not a literal +member of the parent base-assumption list. -/ +example : + ({ node := splitBaseNode, fact := .enabled } : NodeFact SplitFact) ∉ + branchBase := by + simp [branchBase] + +/-- The unrelated version-zero top entry is also present in the exact seed +table and has its own inherited proof. -/ example : splitSemantics.Entails program ({ node := splitNode, fact := .yes } :: branchBase) - { node := node 1, fact := .yes } := - (branchSeed.sound (node 1) .yes (by rfl)).proof + { node := splitTargetNode, fact := .all } := + (branchSeed.sound splitTargetNode .all (by rfl)).proof end Hex.Interval.ProofEmitterConformance diff --git a/progress/20260814T104145Z.md b/progress/20260814T104145Z.md new file mode 100644 index 000000000..272656104 --- /dev/null +++ b/progress/20260814T104145Z.md @@ -0,0 +1,33 @@ +# Branch-seed conformance repair + +## Accomplished + +- Strengthened the Mathlib-free `BranchSeed` canary so the parent base contains + `{node 1, .yes}` while the child seed carries the genuinely derived, + non-member consequence `{node 1, .enabled}`. +- Made the inherited proof consume the parent `.yes` theorem and establish the + semantically equivalent `.enabled` fact, rather than restating a literal base + assumption. +- Exercised every entry of the exact three-node child seed: the split assumption + at node zero, the derived parent consequence at node one, and the unrelated + top fact at node two. +- Kept `BranchSeed`, `BranchSeed.make`, and all public proof APIs unchanged, and + updated only the precise SPEC/conformance description of the stronger test. +- Built `HexInterval.Experiment.ProofEmitter` and + `HexInterval.ProofEmitterConformance`; copyright, dependency-DAG, trust, + Phase 4, factor-freshness, diff, and added-line banned-mechanism checks pass. + +## Current frontier + +- The repair is complete as a local commit on the old PR #9217 head and is + ready to replay after PR #9216 merges. + +## Next step + +- Replay this commit onto the reconciled #9217 branch, rerun the focused checks, + and obtain exact-head review and CI there. + +## Blockers + +- None; the existing `SplitFact` semantics directly supports the stronger + non-member consequence. From e6436bcdaf69842beb68ce477c6da6f8cf95e584 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 14 Aug 2026 10:50:14 +0000 Subject: [PATCH 3/3] Restack branch seeds on split proof repair; progress 20260814T104936Z --- progress/20260814T104936Z.md | 36 ++++++++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) create mode 100644 progress/20260814T104936Z.md diff --git a/progress/20260814T104936Z.md b/progress/20260814T104936Z.md new file mode 100644 index 000000000..5c383caff --- /dev/null +++ b/progress/20260814T104936Z.md @@ -0,0 +1,36 @@ +# Branch-seed stack propagation + +## Accomplished + +- Replayed the exact PR #9217 feature commit onto exact post-#9216 `main` + `816b3da83788c12385e71b9c66ee0f78786c7cdc`; its second parent is reviewed + #9216 head `ce9e9143f9d5f5d43a3d0cbba31f70dca8d74868` and its tree is identical. +- Resolved the sole conformance insertion conflict by retaining #9216's direct + swapped-child rejection, noncoverage theorem, and guarded axiom report before + the new branch-seed canary. +- Replayed the stronger provenance canary while adapting it to #9216's + `.enabled`/`.certified` split semantics: a parent `.yes` theorem establishes + the distinct, non-member `.enabled` child seed. +- Pinned the split, derived, and unrelated-top entries of the exact three-node + initial array through `BranchSeed.sound`. +- Preserved the `BranchSeed` structure and constructor types; only their + builder documentation now accurately says “nonsplit parent consequences.” +- Built `HexInterval.Experiment.ProofEmitter` and + `HexInterval.ProofEmitterConformance` successfully. +- Passed copyright, dependency-DAG, published-trust-surface, Phase 4, + factor-freshness, diff-whitespace, and added-line banned-mechanism checks. + +## Current frontier + +- The reconciled stack and strengthened canary are locally verified and ready + to push for independent exact-head review and CI. + +## Next step + +- Obtain a fresh isolated Opus verdict and exact-head GitHub Actions result; + leave PR #9217 unmerged. + +## Blockers + +- None. The old `.decided` test vocabulary no longer exists after #9216, but + `.yes` to `.enabled` expresses the same non-member provenance obligation.