Factor climb engines toward generic from Verity (thin instantiation, least on Verity)

[Th0rgal]

Summary

This PR (together with the companion minimal Verity PR #1983) begins the factoring of the reusable climb / frame machinery so that:

• Verity owns the generic "preserve without forcing huge terms" combinators.
• SPHINCS- (and future consumers) only supply the concrete step spec + the range / data supplier for their specific climbs.

Changes in this PR (kept deliberately small on the Verity side)

• Copy the new Compiler/Proofs/Frames.lean (from Verity PR #1983) into the local vendored verity/ so the workspace builds.
• Add short notes in BindingFrame.lean and StateFrame.lean pointing at the generic versions.
• Add a section to STRATEGY.md documenting the intended split and the target thin top-level claim.

The "additive concrete" modelling in SphincsMinusVerifierSpec/ (C13Concrete, hMsgC13, the pure index lemmas, etc.) is completely untouched.

Motivation (from previous agent work)

Agents repeatedly hit RAM blowups when trying to close the remaining bridge axioms (c13_refines_byte_spec, Layer-3 compose, atomic execC13 flip) with monolithic simp / aesop strategies over the full state + long climb traces.

The successful commits were the ones that decomposed into frames + preservation bricks + data obligations reduced to pure-spec facts + range suppliers. This PR externalises the most reusable pieces of that decomposition.

Desired end state (documented in STRATEGY.md)

• Verity: generic Frames (and in follow-ups: generic ClimbEngine taking step, specStep, DataSupplier, and frame-preservation proofs).
• SPHINCS-: thin instantiation files that supply the SPHINCS- stepMerkle / guarded runBody, the merkleSpecStep, the xmss_climb_data_range / fors_climb_data_range (from hauth + frozen calldata), and the C13-specific memory layout.
• Top-level claim becomes the thin observable one: the model returns success and the observed final root cell matches the spec root computed from pk iff the byte spec accepts and rootMatchesPk holds. No full trace equivalence.

Test plan / verification

• The changes are mostly comments + one vendored copy + docs.
• lake build (or equivalent in the harness) should still pass for the spec side.
• The factoring direction is now explicit and the two PRs are linked.

Companion Verity PR: lfglabs-dev/verity#1983

This implements the "least possible on the verity side" version of the refactoring discussed for the C13 accept-path climb correspondence work.

---

Note

Low Risk
Additive proof scaffolding, comments, and strategy docs; no changes to verifier specs, axioms, or runtime behavior.

Overview
Vendors Compiler/Proofs/Frames.lean (from Verity PR #1983) into the local verity/ tree so the workspace can build against the shared climb/frame lemmas. That module adds generic PreservesBindingsExcept / PreservesSelectorCalldata and keccak-free letVar / mstore preservation theorems for reuse in climb proofs.

BindingFrame.lean gains an import of Compiler.Proofs.Frames plus a short note that SPHINCS-specific lemmas sit on top of the generic engine; existing SPHINCS frame proofs are unchanged. StateFrame.lean only adds a cross-reference to the generic selector/calldata lemmas.

STRATEGY.md documents the June 2026 climb engine factoring: Verity owns generic frames (and later a generic climb lift); SPHINCS- keeps concrete step specs, range suppliers, and memory layout—aimed at avoiding RAM blowups from monolithic bridge proofs.

^{Reviewed by Cursor Bugbot for commit f4cd500. Bugbot is set up for automated code reviews on this repo. Configure here.}