fips205-slhdsa-verified/TRUSTED-BASE.md

# TRUSTED-BASE — what the certificates do NOT cover

Eleven certificates over the extracted `verify_mono` model are now proven
(`verification/check.sh` green; the apex is
`fips205.slh_verify_128s_accepts_iff`). This file states what those
certificates deliberately do NOT establish; it is maintained as the campaign
proceeds and is part of every claim.

1. **The five verify-path hash oracles.** `h_msg, f, h, t_l, t_len`
   (SLH-DSA-SHA2-128s instantiations over SHA-256; `prf`/`prf_msg` are
   sign-side only and do not appear in the cone) are modeled as opaque
   functions with assumed functional behavior. Their correctness against
   FIPS 180-4 is NOT proven here — the same standing boundary as SHA-512
   in the ed25519 apex. A collision or misimplementation inside the hash
   layer is invisible to these certificates.
2. **Signing and key generation.** Out of extraction scope entirely. A
   verified verify path says nothing about the safety of signature or key
   production (including randomness).
3. **The transpilation pair.** Charon and Aeneas (pinned versions in the
   toolchain) are trusted to preserve semantics from Rust (MIR) to the
   Lean model. Divergence between rustc's semantics and the extracted
   model is trusted base.

   **What is now reproducible, and what is not.** Extraction is two steps:
   `Rust --charon--> SlhVerify.llbc --aeneas--> gen/SlhVerify/*.lean`. The
   `.llbc` is committed, so the SECOND step can be re-run by anyone with the
   pinned Aeneas and this repository, and on 2026-08-03 doing so reproduced
   `Types.lean` and `Funs.lean` **byte-identically**. The FIRST step still
   requires charon, which no reviewer has yet had available. So: the
   LLBC → Lean half is reproducible on demand; the Rust → LLBC half rests on
   the author's attestation alone, and continues to do so until a third party
   runs it. Do not read the first half as evidence for the second.

3b. **The correspondence check is textual, not a Lean query.** Phase 0d parses
   `FunsExternal_Template.lean` and the hand-written model as SOURCE TEXT. It
   establishes that every external the extraction names is answered by a
   declaration of the right name in the pinned model, and that the model
   declares no axiom the extraction never asked for. It does **not** ask Lean
   how those names resolve at elaboration — the four ed25519 repositories have
   a second, semantic phase for that; this one does not. All eleven externals
   here are answered by the model itself (none by the proven corpus), which is
   the narrow case where the textual answer and the semantic one coincide, but
   that is a property of today's corpus and not a guarantee of the check.
4. **The Lean kernel and its three axioms**
   (`propext, Classical.choice, Quot.sound`).
5. **Build correspondence.** No reproducible-builds claim: the proof is
   about the pinned source, not about any particular compiled binary
   (the estate's R5 gap, stated everywhere it matters).
6. **Parameter-set scope.** Claims will bind SLH-DSA-SHA2-128s only;
   other parameter sets are unverified until separately extracted and
   proven (R2).
7. **Aeneas-compat + de-plumbing patch surface.** The fn-pointer-to-named-
   oracle rewrite in `fips205-source` (phase 1) and the two de-plumbing
   rounds (index-loop rewrites of the iterator adapters on the verify path,
   de-plumbing round 2 at `bea1051`; current snapshot head `a3ce8e8`) are
   part of the verified surface: the
   certificates cover the *patched* verify path, and the patch commits are
   the auditable delta from upstream `30bac08`. Each rewrite's equivalence
   to upstream is argued in its commit and checked, for SHA2-128s, by the
   snapshot differential test — it is not itself machine-checked.
8. **The `base_2b` inner loop.** `helpers.base_2b_loop0_loop0` (which
   determines the FORS indices and WOTS digits) is threaded opaquely and
   has no certificate; a defect there could change the recomputed root while
   all eleven theorems still hold.
9. **The deployed generic verifier.** The proved subject is the private
   `verify_mono` facade. The bridge to upstream's generic `pk.verify()` is a
   finite differential test, **not** a machine-checked refinement — no theorem
   here says the two agree; the evidence is empirical and its size is stated so
   a reader can judge it (external review, rounds 4–6, correctly objected that
   "finite" without a number is not a disclosure):
   - **137 evaluated input/verdict cases on the proved path** (was 9 until
     2026-07-28: three rounds from one fixed seed, corrupting one fixed byte of a
     7856-byte signature). The breakdown, which a reviewer can recount from
     `src/verify_mono.rs`:
     | source | cases |
     |---|---:|
     | retained original differential test (3 rounds × valid/corrupt/wrong-message) | 9 |
     | randomized differential bridge (12 rounds × valid + 6 corruptions + wrong-key + wrong-context) | 108 |
     | NIST ACVP `internal` group — M′ fed straight into `slh_verify_128s` | 10 |
     | NIST ACVP `external pure` group — mono vs deployed vs NIST | 10 |
     | **total** | **137** |
   - **20 of those are NIST known-answer tests against the proved path** (the
     two NIST rows above). NIST's negatives sit at structurally distinct sites —
     modified R, SIGFORS, SIGHT, modified message — rather than one arbitrary
     byte. The external-pure ten carry real contexts, 9 of them non-empty and one
     at the FIPS-205 maximum length of 255, which is the only empirical check of
     the domain-separator byte and context-length prefix that item 10 declares
     outside every proof.
   - **127 of the 137 compare mono against the deployed verifier** (all but the
     ten `internal` NIST cases, which compare mono against NIST directly).
   - Separately and **not** counted in the 137: **3 deployed-only prehash cases**
     (NIST `external preHash`), which exercise `hash_verify` rather than the
     proved path. Only two SHA2-512 vectors and one SHAKE-256 vector are
     executable — NIST's remaining prehash vectors use functions this crate does
     not implement — so this is *not* NIST coverage of all four supported prehash
     variants.
   - Corruption in the randomized bridge covers **72 distinct positions in the
     range 11..=7779**, not literally every byte of the signature.
   Still **not** covered by any of it: agreement on inputs nobody generated, and
   the prehash variant against the mono path (see item 10). A passing
   differential test is evidence, not a proof.
10. **Everything above the extraction root.** The root is
    `verify_mono::slh_verify_128s = slh_verify_internal_free(M′, sig, pk)`,
    which takes the message-digest input **M′ as an argument**. The code in
    `slh_verify`/`verify` (`src/lib.rs`) that runs *before* this root is NOT
    covered by any certificate: the assembly of M′; the pure-vs-prehash
    **domain-separator byte** (`0u8` for `verify` vs `1u8` for `hash_verify`
    — the whole cross-variant domain separation); the FIPS-205 `ctx.len() >
    255` bound; and signature/public-key deserialization. The certificates
    say nothing about this input handling — a defect there (e.g. a wrong
    separator byte) would be outside every proof.
    **Concretely, so the consequence is not left to the reader:** that byte is
    the *only* thing separating the pure and prehash variants. If it were wrong
    or dropped, a signature issued over the pure M′ would verify as a prehash
    signature and vice versa — cross-variant signature confusion, a forgery
    primitive. No certificate in this repository would change.
11. **The verification harness itself.** The certificates are statements
    checked by the Lean kernel, but the *button* that reports them is a shell
    script. Round-5 review demonstrated that stubbing `verification/lean-guard`
    alone — one repo-tracked file, without touching `check.sh`, the manifest, or
    the proofs — yields ALL GREEN in 3.6 seconds over deliberately destroyed
    proofs. `lean-guard` is therefore **sha256-pinned** by check.sh Phase 0
    (`PROVENANCE.json → harness_integrity_sha256`); it is kept rather than
    removed because it is the memory cap and machine-wide lock that protect the
    build machine (a Lean elaboration once reached 12.2 GB and took the host
    down).
    **`verification/Proofs/Audit.lean` is pinned the same way, and for a sharper
    reason** (round-6 NEW-7): the digest it emits binds the audit's *data* — the
    policy constants, the statements, the specification bodies — but nothing can
    make a program hash the correctness of its own logic. Flipping this file's
    two fail-closed guards to `unless true` disabled every in-Lean check while
    the digest stayed BYTE-IDENTICAL, and a repository proving `False` passed
    ALL GREEN. The byte pin converts that from a silent green into a build
    failure; a legitimate change to the audit is now a reviewable pin rotation.
    Note the residue honestly: an author who edits the logic *and* rotates its
    pin in the same commit is not stopped by anything mechanical — that case is
    caught only by reading the diff at the pin.
    **`PROVENANCE.json` is itself load-bearing and unpinned.** It supplies the
    values for every byte pin, and round-7 review demonstrated that deleting one
    key from it silently removed both harness pins with no diagnostic, after
    which the logic mutation above ran to ALL GREEN. The *policy* — which files
    must be pinned — now lives hardcoded in `check.sh` and a missing entry is a
    build failure, so the map can no longer be quietly shortened; but the map's
    own bytes are still not pinned by anything, and could not be without moving
    the root of trust somewhere else.
    Still trusted, and NOT bound by anything the button can check:
    `check.sh` itself, `~/aeneas-toolchain/env.sh`, the `$AENEAS_HOME` tree
    (i.e. *which* Aeneas/Lean library the proofs are checked against), `python3`,
    and the Lean toolchain. An audit executed by a harness cannot defend against
    an author who edits that harness; the consumer defense is the pinned commit,
    reviewed at the pin.
12. **Composition.** The apex does **not** compose the ten loop-fidelity
    theorems — it is a structural factorization of the extracted verifier around
    its final equality check and references none of them (it would remain
    provable if one were deleted). The ten are independent, individually
    human-reviewed lemmas. Round-5 review makes this worth stating here rather
    than only in the README: each of the ten is individually meaningful only to
    the extent a human has read its reference fold against FIPS 205.