Skip to content

interval: seed proofs for child branch replay - #9218

Merged
kim-em merged 2 commits into
mainfrom
agent/interval-branch-frontend-v2
Aug 14, 2026
Merged

interval: seed proofs for child branch replay#9218
kim-em merged 2 commits into
mainfrom
agent/interval-branch-frontend-v2

Conversation

@kim-em

@kim-em kim-em commented Aug 11, 2026

Copy link
Copy Markdown
Owner

Summary

  • quote and definitionally validate the complete child CheckerInput in the generic frontend encoder
  • convert a provenance-safe BranchSeed into one version-zero FactProof for every child graph node
  • add a generic emitBranch entry point using the existing arbitrary-event fold
  • reject checker-input, child-assumption, runtime base-program, and quoted base-program drift
  • preserve the interval: seed proof branches safely #9217 derived-nonmember inheritance canary and pin the split, inherited, and unrelated-top entries through the public bridge
  • document the authenticated-table precondition of the low-level emitSeeded fold

Verification

  • lake build HexInterval.ProofEmitterConformance HexIntervalMathlib.SineTacticConformance HexIntervalMathlib.ExpSignConformance (1970 jobs)
  • git diff --check 6ccdf8aeb0c152b4e75ae81b50a3e853d1f8b04e
  • copyright-header and DAG checks
  • trust-surface, Phase 4, factor-freshness, and banned-proof-mechanism checks

Restacked directly on merged #9217 / exact main 6ccdf8aeb0c152b4e75ae81b50a3e853d1f8b04e.

@kim-em
kim-em force-pushed the agent/interval-branch-seed branch from 314f804 to 22f1fa5 Compare August 11, 2026 19:37
@kim-em
kim-em force-pushed the agent/interval-branch-frontend-v2 branch from 25439bc to b8c1064 Compare August 11, 2026 19:38
@kim-em
kim-em force-pushed the agent/interval-branch-seed branch 3 times, most recently from e5e1d44 to e6436bc Compare August 14, 2026 11:17
@kim-em
kim-em force-pushed the agent/interval-branch-frontend-v2 branch from b8c1064 to 6067839 Compare August 14, 2026 12:01
@kim-em
kim-em changed the base branch from agent/interval-branch-seed to main August 14, 2026 12:01
@kim-em
kim-em merged commit 3967aa7 into main Aug 14, 2026
1 of 2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant