Discharge the three C13 residual assembly axioms (issue #7)

[Th0rgal]

WIP: discharge the three C13 residual assembly axioms (issue #7)

This branch carries the in-progress proof work toward removing the residual axioms from the Verity development. Nothing here is validated end to end yet: the new modules have zero sorrys but none of them has compiled to completion on this machine, so they must be treated as unverified drafts. The main line stays clean and green without them.

Remaining axioms on main (the complete list)

There are no sorrys anywhere on main. The full trust surface, as machine-checked by the #print axioms guards at the bottom of verity/SphincsMinusVerifiers/Proofs.lean and documented in verity/SphincsMinusVerifiers/AXIOMS.md, is:

C13 (keccak) verifier: 3 residual assembly axioms

c13_refines_spec and c13_implements_spec rest on Lean's core axioms (propext, Classical.choice, Quot.sound) plus exactly these three, all declared in Proofs.lean:

1. c13_ok_beforeAuthOff_wotsPk_lightweight_chain_inputs_layer0 (Proofs.lean ~11269)
2. c13_ok_beforeAuthOff_wotsPk_lightweight_chain_cells_residual_layer1 (~11580)
3. c13_reverted_layer0_beforeAuthOff_wotsPk_lightweight_chain_cells_residual (~11987)

Each one pins an already-verified generic WOTS chain lemma (c13Layer0_copyFold43_wotsChainsEnd_cells_of_inputs and c13Layer0_copyFold43_wotsPk_keccak_of_inputs in C13WotsPkKeccak.lean / C13ChainCells.lean) to the concrete interpreter state at the beforeAuthOff lightweight WOTS public-key recomputation cutpoint inside the hypertree climb (layer 0 ok path, layer 1 ok path, and the layer 0 reverted path respectively).

What discharging each requires: proving that the five-field exact-inputs package (seed cell, message digest cell, WOTS address cell, WOTS pointer, and the calldata load) holds at the concrete state c13BeforeWotsPkLightState (c13LayerLoopState0 (mkC13State ...)). The mathematics is routine symbolic execution; the obstacle is elaboration cost. The original monolithic attempt (verity/probes/probe_inputs_layer0.lean on this branch) was OOM-killed at roughly 30 GB RSS after about 8 hours under a 32 GB cgroup cap, so the proofs do not fit as single modules on commodity hardware.

The approach on this branch: split each discharge into an Inputs module (irreducible named intermediate states, one small lemma per field of the package) and an Assembly module (assembles the per-field lemmas into the axiom statement), so each Lean worker elaborates a bounded slice and oleans act as checkpoints:

• C13ResidualLayer0Inputs.lean + C13ResidualLayer0Assembly.lean (axiom 1)
• C13ResidualLayer1Inputs.lean + C13ResidualLayer1Assembly.lean (axiom 2)
• C13ResidualRevertedLayer0Assembly.lean (axiom 3)

Once they compile, the resulting theorems must be folded into Proofs.lean: the layer-1 theorem has to be placed after c13_ok_afterMerkle_initial_wotsPk_residual_layer0 (~line 11812) and the consumers from ~line 11645 onward reordered, then the #print axioms guards and AXIOMS.md updated, with a full rebuild via verity/scripts/build.sh. After that, c13_refines_spec rests on Lean's logic alone.

SLH-DSA-SHA2-128-24 verifier: 2 axioms (not addressed by this branch)

1. slhDsaSha2_128_24_refines_byte_spec (Proofs.lean ~149): the model-to-byte-spec bridge. Discharging it requires extending the interpreter with byte-addressed memory semantics (the SHA-256 path uses overlapping sub-word mstores that the current word-keyed memory cannot represent) and a model of the SHA-256 precompile staticcall to address 0x02, then replaying the accept path the way the C13 proof does. Two slices are already proved unconditionally (the malformed-length subdomain and the length-guard pass-through).
2. slhDsaSha2_128_24_Primitives (ProofCore.lean ~25): the SHA-256-based primitive package is an opaque constant. Discharging it requires a concrete pure SHA-256 engine in the development, mirroring how c13Primitives is now the concrete KeccakEngine.keccak256.

Build caution

Do not run a bare lake build on this branch. The probe files and the residual modules are exactly the elaboration-heavy code that OOMs 32 GB machines; use verity/scripts/build.sh on a large-memory host and build one module at a time.

---

Note

High Risk
This PR changes the C13 formal verification trust boundary (axioms → theorems) for core WOTS/hypertree assembly; incorrect or uncompiled proofs would weaken c13_refines_spec, and layer-1 still leaves two axioms in the new modules.

Overview
Adds a C13Residual* module tree that proves the three former Proofs.lean assembly axioms (layer-0 WOTS exact inputs, layer-1 copied chain-end cells, reverted layer-0 chain cells) by splitting work into per-field lemmas and thin assembly theorems, then rewires those statements to theorems that call *_proved results instead of axiom.

c13BeforeWotsPkLightState and C13WotsOuterExactInputs move out of Proofs.lean into C13ResidualInterface.lean and C13WotsOuterInputs.lean. lakefile.lean lists the new modules; verity/probes/ holds standalone discharge probes documented as high-RAM WIP.

Layer-1 assembly still relies on two axioms in C13ResidualLayer1Inputs.lean (first-layer step seed slot and layer-1 currentNode = layer-0 root). SegmentLayer3MerkleFrame.lean adds stepLayer_preserves_entry_memory_zero_of_layerFrozenSite_range to support that path.

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

[Th0rgal]

@BugBot review

[cursor]

✅ Bugbot reviewed your changes and found no new issues!

Comment @cursor review or bugbot run to trigger another review on this PR

^{Reviewed by Cursor Bugbot for commit b2473f2. Configure here.}