libshrincs

Formally verified SHRINCS constructions. First construction: WOTS+C, the SHRINCS leaf one-time signature — one machine-checked theorem connecting a C implementation (VST) to game-based one-time unforgeability (SSProve), on end-to-end-lamport's single-root, single-reviewer-file architecture.

Status. Proof-of-concept first construction (WOTS+C) toward full SHRINCS; the C in src/ and its VST contracts are provisional and will change. The four public VST contracts constrain only the 9-byte ADRS anchor (tag(1) ‖ index(8)) that the C actually reads: bytes [9..22) enter as arbitrary caller bytes, because the C overwrites each of them before reading it.

The claim

proof/wots_plus_c.v is a story read top to bottom, ending in one theorem, shrincs_wots_c_correct_and_secure:

1. the scheme is not vacuous: at every leaf position of the surrounding hypertree, an honestly produced signature verifies under the matching public key;
2. the compiled C is a VERIFIED COMPONENT: the four translation units linked, with an empty Imports slot, implement the four public contracts — key generation, signing, public-key recovery, verification — against CompCert's Clight semantics;
3. forging costs breaking truncated SHA-256: ASSUMING six named hash-game bounds, no adversary wins the standard known-message valid-commit one-time experiment against WOTS+C with probability better than an eight-term sum — again at every leaf position.

Every definition the statement depends on is spelled in that file or in proof/sha256.v, the only other must-read file, plus two type declarations reproduced verbatim because a type can only be re-declared and not respelled: proof/model/address.v's five-arm adrs inductive (used in section 1) and proof/ssprove/lib/sig/scheme.v's sig_scheme record (used in section 5). proof/sha256.v answers "is the hash really SHA-256?"; wots_plus_c.v answers "is the scheme really WOTS+C at the shrincs-bip numbers, does the C really implement it, and does forging really cost what the theorem says?".

The file's own sections, in order:

1. Parameters and addresses — the shrincs-bip numbers (n = 16, w = 16, chain_count = 32, grind target constant_sum = 240) and the 22-byte ADRS wire format with its four WOTS+C smart constructors, each pinned twice: to the model tree's spelling and to the games tree's.
2. The tweakable hashes — one construction, SHA256(pk_seed ‖ 0^48 ‖ ADRS ‖ M)[:16], written directly over proof/sha256.v's sha256_bytes, plus the grinding hash's own byte layout, then the carrier-level ('fin (2^128) / 'fin (2^256)) instances the security games consume.
3. The scheme — WOTS+C's algorithms at the concrete parameter record P_c, and the round-trip theorem shrincs_wots_verify_sign: an honestly produced signature verifies.
4. The C contracts — the four VST funspecs src/wots.c's entry points are verified against, pinned by reflexivity to proof/vst/contract/public.v's.
5. What "unforgeable" means — WOTS+C with PRF-derived keys as a sig_scheme, the two-oracle COMMIT/KFORGE interface, and the known-message valid-commit game pair (shrincs_wots_kots_game) it is attacked in.
6. The assumptions — THE WHOLE TRUST SURFACE: six real-valued advantage-bound Parameters and six named Axioms saying truncated SHA-256 meets them, for the four tweakable-hash instances sections 2–3 define (chain hash F, pk-compression T_sf, grinding H_grind, the PRF). This section sits outside sections 3–5's anchor block on purpose: no assumption may mention where in the surrounding tree the keypair sits.
7. The payoff — shrincs_wots_secure_kots_sha256: the closed-form eight-term bound on forging, eps_prf + 14·eps_smud + eps_stcrp + eps_tcr_pk + eps_tcr_chain + eps_pre + 14·eps_smud + eps_prf (the two sums have w - 2 = 14 terms each), at every leaf position.
8. The theorem — the three conjuncts above, in one statement, proved by composition only: three exacts, one per conjunct.

One honesty note the file makes at length: SSProve has no resource model (an adversary is any package, with no cost attached), so a hardness assumption about a fixed function like truncated SHA-256 is formally weak however it is phrased — an exhaustive adversary is admissible, which is why the six constants stay uninterpreted Parameters rather than numerals. Conjunct (3)'s content is the reduction behind it (proof/ssprove/wots/theorem.v's eight-hop game sequence, which assumes nothing about the hash); the numeric belief (each constant near 2^-128 for truncated SHA-256 at realistic query budgets) is prose, in section 6 and here, not a theorem.

Build & verify

nix develop      # the one devshell (forked Rocq/VST/SSProve toolchain)
make test        # C self-consistency / tamper tests + SHA-256 KATs/CAVS
make prove       # both proof trees (vst-prove + ssprove-prove)
make audit       # prove + the six-gate honesty layer; ends in the TRUST SURFACE table
make check       # full CI gate: static analysis, sanitizers, CompCert, ctgrind,
                 #               extract, prove, audit

make alone builds only build/libwots.a. make extract runs clightgen; make vst-prove / make ssprove-prove build one proof tree at a time; make check-ct runs the constant-time gate (below) under gcc, clang and CompCert; CC=ccomp builds the C with CompCert instead of gcc. make clean also runs make -C proof clean, wiping the whole proof .vo tree, so a routine C-only rebuild should use rm -rf build && make instead.

The devshell builds Rocq, VST and SSProve from forks (branches pinned in flake.nix) — the same three end-to-end-lamport's toolchain uses. wots_plus_c.v needs floyd (VST), the mathcomp/SSProve surface, and the model tree in one file, which is exactly the interop problem that proving ground exists to solve first. None of the three forks touches a logical rule, a proof, or a soundness-relevant check:

• SSProve (remix7531/ssprove, interop-vst) exposes a universe-small machine-word carrier, so the security games can be typed in the same mathcomp-word type the C contracts use, and keeps the nominal layer's notations and rewrite-order flags from leaking into a file that also imports floyd.
• VST (remix7531/VST, interop-mathcomp-2.16) moves floyd's print-only ==/!= notations to level 70, where ssreflect's parsing notations already sit — Rocq's notation-level table is global, so without this any file importing floyd after mathcomp fails hard.
• Rocq (remix7531/rocq, only-printing-no-level-clash-9.0) backports three commits from an upstream PR to v9.0 that stop only printing notations from having to match the grammar level — the general fix for the clash the VST commit works around locally.

Trust surface

make audit runs proof/audit/check.sh's six gates (0–5): every .v in _RocqProject is built and current; no Admitted/admit./give_up. anywhere under proof/ outside audit/ itself; no Axiom/Parameter/Hypothesis declared anywhere except proof/wots_plus_c.v (two narrow, discharged carve-outs documented at the gate); the two theorem names are literally probed, so neither can be silently renamed or swapped for a weaker namesake; the probed Print Assumptions cone is a subset of proof/audit/allowed.txt; and a hand-pasted copy of the headline theorem's statement (proof/audit/statement.v) type-checks against the live theorem, so a dropped conjunct or a weakened bound is a build failure rather than a diff nobody notices.

What is plainly not assumed any more: SHA-256 is a definition — proof/sha256.v is the FIPS 180-4 transcription, section by section, pinned by vm_compute-checked known-answer tests — and src/sha256.c's body is proved against it (proof/vst/sha256/, packaged as the Verified Software Unit sha256_c_correct). Nothing named SHA256/sha256 is a Parameter or an Axiom anywhere in this repository, and Print Assumptions on the model tree's own ground-truth round-trip theorem (proof/model/correct/wots.v's wots_correct) prints the closed-under-the-global-context empty cone.

proof/audit/allowed.txt is 25 names, in three groups:

• The repository's own trust surface (12 names) — six real-valued advantage-bound Parameters (eps_prf, eps_smud, eps_stcrp, eps_tcr_pk, eps_tcr_chain, eps_pre) and six named Axioms saying truncated SHA-256 meets them (sha256_prf_secure, sha256_smud_secure, sha256_stcrp_secure, sha256_tcr_pk_secure, sha256_tcr_chain_secure, sha256_pre_secure), both declared only in proof/wots_plus_c.v section 6.
• One library gap — realsum.__admitted__interchange_psum, a Tonelli/Fubini-style psum-interchange fact left Admitted inside mathcomp-analysis's own realsum.v (not authored here, reached through SSProve's probability semantics). It is proved in that library's development version.
• Twelve classical baselines the two toolchains come with — SSProve's abstract real carrier and proof-irrelevance axiom, mathcomp-analysis's boolp classical axioms, and CompCert/Coq-stdlib's excluded middle, choice, functional/propositional extensionality and UIP — asserted by none of this repository's own files.

What the caller must guarantee

The theorem is about a byte-level model and a Clight program under CompCert's semantics. Several things stand between that and a running system, none of them checkable by the C API:

1. sk_seed and pk_seed are CSPRNG output. Section 5's game samples both uniformly (dK/dPP); there is no key generation in this library, by design. A key derived from a low-entropy seed is outside the theorem.
2. One shrincs_wots_sign call per (sk_seed, pk_seed, addr) triple (include/wots.h's own header comment). WOTS+C is a one-time signature: signing a second message under the same keypair is outside every conjunct of the theorem, and nothing in the API keeps state to stop it.
3. The buffers do not overlap. Every pointer parameter is restrict (include/wots.h, include/sha256.h, include/thash.h); the funspecs say the same thing via the separating conjunction between their data_at clauses. CompCert drops restrict during elaboration, so the C-side qualifier is documentation and the funspec is where the requirement bites.
4. The ADRS buffer's anchor is the caller's; everything else is not. A caller prefills addr[0..9) (1-byte node height, 8-byte big-endian node index) before every call; the four contracts constrain only those nine bytes on the way in (see the Status note above) — bytes [9..22) enter as opaque junk because the C stamps the type byte and clobbers the three payload words before anything reads them. Reusing an anchor across two different keypairs breaks the "one leaf position, one keypair" reading the one-time security game depends on.
5. Compile with CompCert if you want conjunct (2) to apply to your binary. The proof is about the Clight AST clightgen derives from src/*.c under CompCert's semantics; make defaults to gcc -O2. make CC=ccomp is the configuration the guarantee transfers to.
6. Side channels are checked, not proved. make check-ct runs shrincs_wots_pubkey_gen and shrincs_wots_sign — the two functions that touch sk_seed — under valgrind/ctgrind with sk_seed marked uninitialized, across gcc, clang and CompCert builds, and fails on any branch or memory address that depends on it. That rules out secret-dependent control/memory flow on the paths exercised; it is not part of the Rocq theorem and not a proof.

Layout

See proof/README.md for a guided tour of the three proof trees below proof/ and how they relate to wots_plus_c.v.

src/ include/        the C: wots.c (the scheme), thash.c (the shared
                      tweakable hash + ADRS writer), sha256.c (FIPS 180-4),
                      util.c (memcpy/memset/ct_memcmp/panic libc shims).
                      Four translation units, four Verified Software
                      Units, linked with an empty Imports slot in
                      proof/vst/link.v
test/                 C self-consistency/tamper tests, SHA-256 KATs/CAVS,
                      the WOTS+C KAT (test/wots/vectors/, regenerable
                      against the shrincs-bip Python reference), the
                      ctgrind constant-time harness (test/ctgrind/)
proof/wots_plus_c.v   MUST READ. The claim (see above); the only file
                      allowed to declare an Axiom or a Parameter
proof/sha256.v        MUST READ. SHA-256 as FIPS 180-4 orders it, the
                      known-answer tests, and the one C contract
                      src/sha256.c satisfies
proof/model/          the shared, framework-neutral ground: machine.v /
                      fin.v / byte.v / bytes.v (the representation
                      atlas), address.v (the 5-arm adrs union), wots.v
                      (the byte-level WOTS+C scheme -- the VST tree's
                      ground truth), sha256.v (derived facts over
                      proof/sha256.v), iteration.v, math/ (pure
                      combinatorics the SSProve tree imports directly),
                      theory/ (derived facts), correct/wots.v (the
                      model-only round-trip theorem, assumption-free)
proof/vst/            functional correctness of the C, VST/CompCert:
                      base.v / settings.v (the floyd + CompSpecs root),
                      repr/ (word/seqlist/int32 codec bridges), sha256/
                      (clone.v + sync.v: a private clone of
                      proof/sha256.v plus the kernel-checked gate that
                      it IS the original; contract.v, verif/, vsu.v,
                      correct.v), model/wots.v (a re-export shim onto
                      proof/model/wots.v), contract/ (the four public
                      funspecs and their C-representation bridges),
                      verif/ (one semax_body per C function), vsu/ (the
                      other three components), link.v (all four linked)
proof/ssprove/        one-time security, SSProve/MathComp: lib/ (the
                      generic hash-based-signature substrate -- games/,
                      sig/, chain/, toolkit/), addressing.v / bridge.v
                      (the tweak encoding and the games<->model.wots
                      bridge), wots/ (the WOTS+C scheme, one reduction
                      per assumption under hop/, the assembled
                      theorem.v, instantiation.v, model_bridge.v,
                      kots_link.v), axioms.v (the concrete SHA-256
                      instantiation the six axioms in wots_plus_c.v are
                      about)
proof/audit/          the honesty gate: check.sh (6 gates), allowed.txt
                      (the 25-entry allowlist), probe.v / statement.v
                      (the two standalone pins)
proof/clight/         clightgen output, regenerated by every build,
                      never committed
proof/STYLE.md        the proof style guide

License

MIT; see LICENSE. Copyright (c) 2026 remix7531 remix7531@mailbox.org. proof/sha256.v is ported from end-to-end-lamport's Lamport.sha256 (same author and licence).