verity: C13 accept-path climb-correspondence workbench#3

Draft

Th0rgal wants to merge 98 commits into

mainfrom

verity-sphincs-minus-model

Commits on Jun 1, 2026

verity: C13 accept-path climb correspondence workbench
Th0rgal
committed
Prove blocker #20: masked sig read = wordOfHash16 (16-aligned)
Th0rgal
committed
Prove general-offset masked sibling read = wordOfHash16
Th0rgal
committed
Wire general masked-read lemma into Merkle climb data obligation
Th0rgal
committed
Add hauth: parseSignatureC13 auth-path byte-offset indexing lemmas
Th0rgal
committed
C13: add hcd + whole-loop XMSS climb-data range suppliers
Th0rgal
committed
C13: add fors_climb_data_range (FORS inner-climb range supplier)
Th0rgal
committed
C13: STEP-2 climb-loop lift (MerkleClimbRel <-> specFold/xmssClimb)
Th0rgal
committed
C13: Blocker A — accept_path_returns_verifyParsed_bool_linked (pin spec inputs to bytes)
Th0rgal
committed
C13: Blocker B — h1 frame fact (merkle_sibling_read_frozen) + calldataloadWord bound
Th0rgal
committed
STEP 1: define MerkleClimbFrame frame-carrying climb invariant + toRel projection
Th0rgal
committed
STEP 2a: frame world-preservation bricks for stepMerkle
Th0rgal
committed
STEP 2b: add evalExpr_bitXor_bounded combinator
Th0rgal
committed
STEP 2c: per-fact evalExpr discharges for the climb body
Th0rgal
committed
STEP 2d: MerkleClimbFrame self-preservation by one stepMerkle step
Th0rgal
committed
STEP 3: frame-carrying climb loop lift threading MerkleClimbFrame
Th0rgal
committed
STEP 3: MerkleClimbFrame_hstep per-step builder for the frame loop lift
Th0rgal
committed
Advance C13 hCmp bridge scaffolding
Th0rgal
committed
Advance C13 accept bridge obligations
Th0rgal
committed
Reduce FORS hLeaf/hmRlo data obligations to standalone bricks
Th0rgal
committed
Discharge FORS hLeaf unconditionally via bound-free stepMerkle seed frame
Th0rgal
committed

Commits on Jun 2, 2026

Commits on Jun 3, 2026

Add memory-capped Lean runner
Th0rgal
committed

Commits on Jun 4, 2026