Verifying the SPHINCS- Post-Quantum Signature Verifier

1. What is SPHINCS-?

The “minus”: smaller signatures via grinding

2. Two verifiers, one shape

We modeled two of the live verifier contracts. They share one entry point, verify(pkSeed, pkRoot, message, sig) → bool, and differ in hash, address encoding, and grinding rules.

Each contract is a single hand-written assembly block tuned for gas, exactly where a subtle masking or index bug hides.

C13 is also the first verifier in the family built on the FIPS 205 §11.2.2 uncompressed 32-byte address layout, keeping the keccak hash while aligning the ADRS encoding with the NIST reference. Concretely, every FORS hash is keyed by the position of this message in the hypertree: the digest's 22-bit index splits into a tree half and a leaf half (idxTree0 = htIdx >> 11, idxLeaf0 = htIdx & 0x7FF), and the per-level climb address folds the FORS tree number into the index word. The model and the spec are proved to agree at those real, per-message digits, not at a fixed placeholder.

The keccak verifier (C13) is fully proved against the executable model, up to three named residual assembly facts. The SHA-2 variant is modeled and specified to the same standard, but its model-to-spec step is a named assumption (its SHA-256 precompile call sits outside the pure fragment our interpreter covers), so treat its guarantees as the less settled of the two.

3. The specification, in three layers

You prove a contract correct against a specification: an independent description of what it should do. The risk is a spec so close to the code that both share one bug. We split it into three layers, each owning a different concern, and prove each layer refines the one above. Here “B refines A” just means everything B does is already allowed by A, so proving the lower layer can never contradict the upper one.

The top layer verifyBytes owns everything observable from outside the EVM and reduces a valid input to verifyParsed, the algorithm. Their combined contract is a single three-outcome function, where $\bot$ denotes a revert:

4. Six properties a correct verifier must enforce

For each property we give the rule, its spec definition, and the Solidity line that enforces it. A bug in any one is exploitable, or a denial of service against honest users. The spec is parametric over a Primitives package (hash, address encoding, signature parsing); for the keccak verifier that package is instantiated concretely, routed through the same pure Keccak function the interpreter evaluates, so nothing about the hashing is taken on faith in the implementation-correctness theorem. The spec link in each row is machine-checked; the .sol link is the Solidity line whose Lean transcription the proofs execute (section 5).

1. 1

   Signature shape

   Exactly the right components at the right sizes: the randomizer, the FORS leaves and authentication paths, and one WOTS+ block plus Merkle path per hypertree layer.

   signatureShapeOk

2. 2

   Public-key canonicality

   Both verifiers pack 16-byte hashes into 32-byte words and require the unused low bytes to be zero: pkSeed and pkRoot must each equal themselves masked by N_MASK, otherwise the contract reverts with “Invalid public key.” The C13 guard (added in review C13-V-f1, src/SPHINCs-C13Asm.sol) closes a previously silent dead branch: a non-top-aligned pkRoot can never equal the always-masked recomputed root, so every signature would quietly verify false, bricking the account. The guard fails loudly instead, and the C13 model transcribes it.

   publicKeyOkC13 .sol L60-L66

3. 3

   FORS forced-zero$\mathrm{idx}_{k-1} = 0$

   For the +C variants the verifier recomputes the last FORS tree index; a non-zero value means the signature did not pay its proof-of-work and is refused.

   forcedZeroOkC13 .sol L106

4. 4

   WOTS+C grinding target$\textstyle\sum_i a_i = T$

   The recovered chain digits must sum to the agreed target (208 for C13); a wrong sum means a forged or malformed signature and is refused. The proofs run the model's digit-sum loop and show it fails exactly when the spec-side grinding predicate fails.

   wotsGrindingFailsC13 .sol L212

5. 5

   Hypertree index arithmetic$\mathrm{leaf} = \mathrm{idx} \bmod 2^{h\prime},\;\; \mathrm{idx} \leftarrow \lfloor \mathrm{idx} / 2^{h\prime} \rfloor$

   The low bits pick the leaf in the current tree; shifting them off yields the next tree’s index. Off-by-one here silently accepts signatures from the wrong tree.

   foldHypertreeAux

6. 6

   Final acceptance$\textsf{Climb}(\dots) = \textit{pkRoot}$

   After the full climb the recovered root must equal the public root. The contract returns true exactly when they match, and only then.

   verifyParsedC13 .sol L265

5. From Solidity to a theorem

Rebuilding the assembly in Verity

Model.lean transcribes each contract's assembly block into Verity's EDSL statement by statement, keeping the same scratch-memory addresses, the same digest bit-extraction masks, the same loop bounds, the branchless Merkle swap, and the final mstore(0x00, valid); return(0x00, 0x20). Where the Solidity drops to raw Yul (revert(0, 0) and the Error(string) guards), the model uses typed unsafe-Yul fragments that carry an explicit proof obligation instead of an opaque escape hatch.

For the keccak verifier the transcription is not decoration: the proofs execute it. Verity ships a small interpreter for its statement language, and the theorems run c13VerifyBody through it, statement by statement, on a symbolic input. To keep that tractable the body is cut at natural seams, the digest computation, the index split, the FORS reconstruction, the hypertree climb, and each segment is pinned to the body by a definitional equation (a rfl that Lean checks by computing). Edit one opcode of the transcription and those equations stop type-checking: a transcription bug breaks the build.

Inside each segment, loop invariants carry the spec values through every iteration: the 19-level FORS climbs, the 43 WOTS chains, the two hypertree layers. And because the spec's hash package is instantiated with the same pure Keccak function the interpreter calls, “the model's keccak” and “the spec's keccak” are literally one definition; there is no axiom asserting they agree.

What is proved, and what is assumed

Everything from the raw bytes up to the algorithm is machine-checked, resting only on Lean's core logic. For C13 the step below that, the model computes exactly verifyBytes, is a theorem too, established by running the transcribed body through the interpreter. Its proof leans on three named residual assembly facts, each a small, local statement documented in place; the SHA-2 variant keeps its bridge as an explicit assumption. The exact axioms are listed in the trust-surface disclosure below.

The full build contains no sorry, though that alone proves little: what matters is which axioms each theorem rests on, and Lean prints that list exactly. The three residual facts are statements of the same kind as hundreds of lemmas the build does check: that the WOTS chain loop's entry bindings hold at a named cutpoint state of the layer climb, and the same for its layer-1 and revert-branch twins. Each is recorded in place and none hides a new mathematical idea. Work-in-progress proofs discharging them live on the wip/axiom-discharge branch (PR #9); they have not yet compiled to completion (the monolithic attempt exceeded a 32 GB memory cap), so the three declarations remain axioms on main.

c13_refines_spec depends on axioms:
  [propext, Classical.choice, Quot.sound,             -- Lean logic
   c13_ok_..._lightweight_chain_inputs_layer0,         -- WOTS loop entry facts
   c13_ok_..._lightweight_chain_cells_residual_layer1, -- layer-1 twin
   c13_reverted_..._lightweight_chain_cells_residual]  -- revert-branch twin

slhDsaSha2_128_24_refines_spec depends on axioms:
  [propext, Quot.sound,
   slhDsaSha2_128_24_Primitives,                       -- opaque SHA-2 semantics
   slhDsaSha2_128_24_refines_byte_spec]                -- named bridge assumption

Assumptions

The entire trust surface is small and named. These are the only things a reader must take on faith.

• keccak / SHA-2 collision resistancestandard hash assumption, security only

  every hash-based scheme

  Cryptographic security reduces to the hash being hard to invert and collision-resistant; this is what SPHINCS+ itself is built on. It is not needed for the implementation-correctness theorems above: those say the contract computes the algorithm, whatever the hash's strength.

• Residual assembly facts (C13: 3)accepted obligations, documented in place

  verity/SphincsMinusVerifiers/Proofs.lean

  Three named axioms in Proofs.lean: c13_ok_beforeAuthOff_wotsPk_lightweight_chain_inputs_layer0, c13_ok_beforeAuthOff_wotsPk_lightweight_chain_cells_residual_layer1, and c13_reverted_layer0_beforeAuthOff_wotsPk_lightweight_chain_cells_residual. Each pins the WOTS chain loop's entry bindings at a named cutpoint state of the layer climb (layer 0, layer 1, and the revert branch). All higher-level facts that used to be assumed are theorems composed from these. Discharge is in progress on the wip/axiom-discharge branch (PR #9). The proof is per-variant: it covers C13's concrete parameters, not a generic parameterized family.

• Source-to-model transcription fidelitymanual review assumption, all variants

  verity/SphincsMinusVerifiers/Model.lean

  The models are hand-transcribed from the Solidity assembly and are never compiled into the contracts or replayed by Foundry, so correspondence rests on review. One divergence is known: on a failed grinding check (forced-zero index or WOTS digit sum) the model and spec revert, while the live contract, after a later review pass (C13-V-f2), returns false for caller uniformity. Both behaviors refuse the signature; no input is accepted by one and not the other, but the revert-versus-reject boundary proved about the model does not match the deployed source on those two branches until the transcription is re-aligned.

• slhDsaSha2_128_24_refines_byte_spec (+ its Primitives)SHA-2 variant only, named bridge assumption

  verity/SphincsMinusVerifiers/Proofs.lean

  The SHA-2 verifier's model-to-bytes step and its opaque SHA-256/parse semantics remain explicit assumptions: its hashing goes through the SHA-256 precompile, which sits outside the pure fragment the interpreter covers. The keccak verifiers carry neither assumption.

Reproduce it

The proof is checked by Lean 4's kernel. If any step had a gap, the build would fail.

git clone https://github.com/lfglabs-dev/SPHINCS-
cd SPHINCS-/verity
git checkout e62d833a3ad70740ef6d3669b37aace6cc652f2a
./scripts/build.sh SphincsMinusVerifiers   # caps Lean at 2 workers; ~16 GB RAM suffices

Learn more

New to this? What is a formal proof? explains the idea in two minutes. The reusable layered spec also required a small addition to Verity itself (typed unsafe-Yul fragments), landed upstream in verity#1942.