verity: C13 public-key guard in the model, legacy model removal, accurate verification scope

[Th0rgal]

Summary

This PR makes the Verity tree and the repo documentation match the live production verifier set, and brings the C13 model up to date with the current Solidity.

C13 model catches up with the Solidity public-key guard (review C13-V-f1)

• c13VerifyBody in verity/SphincsMinusVerifiers/Model.lean now runs the public-key canonicality guard (pkSeed/pkRoot must equal themselves masked by N_MASK, otherwise revert with Invalid public key) right after the length guard, matching src/SPHINCs-C13Asm.sol.
• The refinement proofs discharge the guard with real lemmas: wordOfHash16_land_nmask (SegmentS2R.lean) and mkC13State_pkSeed_canonical / mkC13State_pkRoot_canonical (SegmentRejectSpec.lean).
• Spec.lean keeps fullPkSeed/fullPkRoot := true for c13 on purpose: the byte spec builds the state with wordOfHash16, whose low 128 bits are always zero, so a non-canonical public-key word is not observable at that boundary. The guard is a model-level fact, proved as such.

Legacy scope removal

The repo's live verifiers are C7, C9, C13, and SLH-DSA-SHA2-128-24; C12 Solidity moved to legacy/ upstream. Accordingly this removes:

• the C12 Verity model (C12Concrete.lean, C12BridgePrep.lean, C12Segment*.lean) and its lakefile roots,
• the older SphincsC6* and SphincsKernel trees, verity/artifacts/, and verity/scripts/compile_merkle_kernel.py,
• test/MerkleKernelVerityTest.t.sol, the only Foundry test that replayed a Verity artifact (the small Merkle kernel). With it gone, no Verity artifact is exercised by Foundry, and the docs now say so explicitly.

The lake package is renamed SphincsC6Verity -> SphincsVerity.

Documentation accuracy

• Top-level README.md, CLAUDE.md, verity/README.md, and the SphincsMinusVerifiers/*.md set now state precisely: only the C13 keccak verifier and the SLH-DSA-SHA2-128-24 verifier are modeled; live C7/C9 are not modeled; the Lean models are hand-transcribed from the assembly and are not compiled into contracts, not deployed, and not replayed in Foundry.
• verity/SphincsMinusVerifiers/AXIOMS.md is rewritten as an exact axiom inventory (see verification below).

Verification

• Full lake build (via verity/scripts/build.sh) is green: no errors, no sorry, no warnings.
• #print axioms confirms the exact trust surface:
  • c13_refines_spec / c13_implements_spec: Lean core axioms (propext, Classical.choice, Quot.sound) plus exactly the three named residual assembly axioms (c13_ok_beforeAuthOff_wotsPk_lightweight_chain_inputs_layer0, ..._cells_residual_layer1, c13_reverted_layer0_..._cells_residual). Discharging these is issue verity: discharge the 4 remaining residual assembly axioms #7, addressed by a follow-up PR.
  • slhDsaSha2_128_24_refines_spec: Lean core axioms plus slhDsaSha2_128_24_refines_byte_spec (MODEL-EXEC-BRIDGE) and the opaque slhDsaSha2_128_24_Primitives.
  • The C13 primitives are concrete (C13Concrete.c13PrimitivesConcrete, same pure Keccak as the interpreter), so no keccak axiom remains; collision resistance / EUF-CMA are out-of-scope cryptographic assumptions, not Lean axioms.
• forge build passes; the default forge test path never referenced the removed Lean trees.

Test plan

• CI: forge build / forge test
• Reviewer spot-check: verity/SphincsMinusVerifiers/AXIOMS.md against #print axioms output at the bottom of Proofs.lean
• Reviewer spot-check: guard transcription in Model.lean against src/SPHINCs-C13Asm.sol

Verification status

Verifier	Live Solidity	Verity model	Bridge theorem	Bridge status	Remaining axioms / sorry	Build (lake, jobs=1, HEAD b6028c7)	Known limitations	AXIOMS.md
C13 keccak	src/SPHINCs-C13Asm.sol	verity/SphincsMinusVerifiers/Model.lean (SphincsC13Asm_VerityModel)	c13_refines_byte_spec -> c13_refines_spec / c13_implements_spec (Proofs.lean)	Proved theorem	3 residual assembly axioms (c13_ok_beforeAuthOff_wotsPk_lightweight_chain_inputs_layer0, ..._cells_residual_layer1, c13_reverted_layer0_..._cells_residual); 0 sorry	Green	Residual lightweight-chain cutpoint obligations (issue #7, follow-up PR in progress); source-to-model transcription is human-reviewed, not machine-checked	C13 (keccak)
SLH-DSA-SHA2-128-24	src/SLH-DSA-SHA2-128-24verifier.sol	verity/SphincsMinusVerifiers/Model.lean (SLH_DSA_SHA2_128_24_VerityModel)	slhDsaSha2_128_24_refines_byte_spec -> slhDsaSha2_128_24_refines_spec (Proofs.lean)	Axiom (MODEL-EXEC-BRIDGE)	Bridge axiom + opaque slhDsaSha2_128_24_Primitives (ProofCore.lean); 0 sorry	Green	SHA-256 precompile unmodeled (evalExpr_staticcall = none); linear_memory_aliasing: overlapping sub-word mstores vs the word-keyed memory model block accept-path replay. Malformed-length and length-guard slices are proved without the axiom	SLH-DSA-SHA2-128-24

Why axiomatized. The three C13 residual axioms pin already-proved generic WOTS chain lemmas (C13WotsPkKeccak.lean, C13ChainCells.lean) to concrete interpreter states at the lightweight cutpoint; the concrete instantiation needs more elaboration memory than prior hosts allowed, so it was taken as a named obligation rather than proved or sorry-ed. See the AXIOMS.md "Residual Assembly Axioms" inventory and the docstrings in Proofs.lean (file header, lines ~25-60, and the per-axiom ASSEMBLY OBLIGATION comments around lines 11255/11570/11978). The SHA2 bridge axiom rationale is in the same file header. C13's primitives carry no axiom: hashing is the interpreter's concrete pure Keccak.

---

Note

Low Risk
Changes are documentation and deletion of unused Verity/Foundry artifacts; production Solidity verifiers in src/ are not modified in this diff.

Overview
Scope and honesty. Top-level and verity/ docs now state that only SPHINCs-C13Asm and SLH-DSA-SHA2-128-24verifier are modeled; live C7/C9 are explicitly unverified in Lean. Models are described as hand-transcribed, not compiled into contracts, not deployed, and not replayed in Foundry (no EVM regression against Lean).

Legacy removal. Drops the old Verity trees (SphincsC6*, SphincsC6Full, SphincsC6V, SphincsKernel), C12Concrete.lean, related Spec.lean c12 variant wiring, and test/MerkleKernelVerityTest.t.sol (~490 lines) plus its FFI compile path. The Lean package is renamed SphincsC6Verity → SphincsVerity.

Trust surface docs. AXIOMS.md and AUDIT.md are rewritten to match the slimmer inventory: C13 top-level theorems rest on Lean core plus three named residual WOTS-PK assembly axioms; SHA-2 keeps MODEL-EXEC-BRIDGE and opaque SHA-256 primitives. publicKeyOk_c13 drops out of the C13Concrete axiom print list as docs clarify byte-spec vs model-level PK handling.

README polish. Minor prose/formatting fixes (punctuation, n/a vs em dashes) alongside the formal verification section expansion in root README.md.

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