SLH-DSA (FIPS 205) campaign skeleton: honest zero-certificate state

Subject pinned: integritychain/fips205 @ 30bac08 via saymrwulf/fips205-source @ 5dca0db. Parameter set SLH-DSA-SHA2-128s. Scope: verify path only (slh_verify -> ... -> chain); six SHA-2 hash oracles opaque per the standing boundary. Gate-0 record (2026-07-22): charon clean on the full verify cone; aeneas translates everything except the Hashers fn-pointer struct (3 unique errors, the sole obstruction) -> phase 1 = named-opaque- free-function compat patch in the snapshot repo, the established dalek sha512-shim pattern. check.sh exits non-green and says NOTHING PROVEN YET (H5, R3). lean-guard copied; every future compile runs under it (S1, S2). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-09-03 19:53:49 +00:00 · 2026-07-22 21:00:57 +02:00 · 2026-07-22 21:00:57 +02:00 · 31f00fe756
commit 31f00fe756
7 changed files with 372 additions and 0 deletions
--- a/.gitignore
+++ b/.gitignore
@ -0,0 +1,3 @@
+*.olean
+target/
+.lake/
--- a/README.md
+++ b/README.md
@ -0,0 +1,86 @@
+# fips205-slhdsa-verified
+
+Machine-checked verification campaign for the **SLH-DSA (FIPS 205) verify
+path**, extracted from a pure-Rust implementation into Lean 4 via
+Charon/Aeneas — the same pipeline, discipline, and honesty rules as the
+four ed25519 campaigns (`dalek/anza/risc0/betrusted-ed25519-verified`).
+
+## STATUS: SKELETON — NOTHING PROVEN YET
+
+There are **zero certificates** in this repository. `verification/check.sh`
+exits non-green and says so. Every claim in this README below the line
+"What will be claimed" is a *plan*, not a result. (Honesty invariant H5:
+an honest gap outranks a hollow certificate.)
+
+## Subject
+
+- Upstream: `integritychain/fips205` — pure-Rust FIPS 205 (final standard,
+  2024-08-13), zero `unsafe`, `no_std`, const-generic parameterization,
+  modules mirroring the FIPS 205 algorithm structure.
+- Pinned at upstream commit `30bac08580aa61f653e5436d1bbacb5ffac446c4`
+  (2025-09-01), snapshotted with full history at
+  `saymrwulf/fips205-source` (snapshot head `5dca0db`, whose single
+  deviation from verbatim is the removal of upstream CI workflows,
+  documented in that commit). Aeneas-compat patches will land in the
+  snapshot repo as transparent, individually-justified commits — never
+  upstream. **No affiliation with, and no changes proposed to, the
+  upstream project.**
+- Parameter set: **SLH-DSA-SHA2-128s** first (the small-signature profile
+  deployed in the firmware/code-signing lane). The architecture
+  generalizes; each further parameter set is a separate claim (rigor
+  invariant R2).
+
+## Scope
+
+**Verify path only.** The extraction cone, mirroring FIPS 205's own
+algorithm tree:
+
+```
+slh_verify -> slh_verify_internal
+  -> fors_pk_from_sig
+  -> ht_verify -> xmss_pk_from_sig -> wots_pk_from_sig -> chain
+```
+
+Key generation and signing are out of scope (trusted base), exactly as
+ed25519 signing was. The six hash oracles (`h_msg, prf, f, h, t_l,
+t_len` — SHA-2 instantiations) are opaque external models with written
+justifications, kept outside every certificate's dependency cone
+(honesty invariant H4); their semantics are the standing SHA-2 oracle
+boundary documented in [TRUSTED-BASE.md](TRUSTED-BASE.md).
+
+## Gate-0 record (2026-07-22)
+
+Per TARGETS.md ("re-verify before use"), the subject was probed before
+this repository was created:
+
+- **Charon**: clean (`charon cargo --preset=aeneas`, roots at the verify
+  cone, `sha2/sha3/zeroize/rand_core` opaque, features
+  `slh_dsa_sha2_128s`) — LLBC produced, exit 0.
+- **Aeneas**: translated the entire const-generic verify cone to Lean
+  definitions (`wots.chain` … `slh.slh_verify_internal` all generated),
+  with exactly **one obstruction class** (3 unique errors): the
+  `crate::hashers::Hashers` struct of plain **function pointers** cannot
+  be translated.
+- **Consequence (campaign phase 1)**: an Aeneas-compat patch in
+  `fips205-source` will replace the fn-pointer struct with named opaque
+  free functions on the verify path — the same pattern as the
+  `sha512_new/update/finalize` shims in `curve25519-dalek-source`'s
+  verify glue. Until that patch lands, `verification/extract.sh`
+  documents intent and produces a partial model.
+
+## What will be claimed (when the button is green, not before)
+
+One theorem per layer, each a statement about the **extracted** functions
+(H3), compiled by `verification/check.sh` with `#print axioms` reporting
+exactly `[propext, Classical.choice, Quot.sound]` (H1): chain semantics,
+WOTS+ pk recomputation, XMSS path recomputation, hypertree acceptance,
+FORS pk recomputation, and the apex — `slh_verify_internal` accepts iff
+the recomputed hypertree root equals the pinned public-key root, under
+the stated oracle boundary.
+
+## Discipline
+
+Every Lean compile in this repository runs under `verification/lean-guard`
+(memory-capped, machine-wide serialized). Extraction is reproducible from
+the committed `extract.sh` against the pinned snapshot (R1). What cannot
+be proven is named in [TRUSTED-BASE.md](TRUSTED-BASE.md), not hidden (H5).
--- a/TRUSTED-BASE.md
+++ b/TRUSTED-BASE.md
@ -0,0 +1,30 @@
+# TRUSTED-BASE — what the certificates will NOT cover
+
+Initial statement, written at skeleton time (nothing proven yet); this
+file is maintained as the campaign proceeds and is part of every claim.
+
+1. **The six hash oracles.** `h_msg, prf, f, h, t_l, t_len`
+   (SLH-DSA-SHA2-128s instantiations over SHA-256) 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.
+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 patch surface.** The fn-pointer-to-named-oracle
+   rewrite in `fips205-source` (phase 1) is part of the verified surface:
+   the certificate covers the patched verify path, and the patch commits
+   are the auditable delta from upstream `30bac08`.
--- a/verification/Proofs/.gitkeep
+++ b/verification/Proofs/.gitkeep
--- a/verification/check.sh
+++ b/verification/check.sh
@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+# The one-button claim for this repository (rigor invariant R3).
+# Green output == the full claim. This script is the ONLY source of the
+# word "proven" for this repo.
+set -euo pipefail
+
+echo "fips205-slhdsa-verified — check"
+echo "================================"
+echo "SKELETON: 0 certificates. NOTHING PROVEN YET."
+echo "Campaign phase 1 (Aeneas-compat patch + clean extraction) has not"
+echo "landed. See README.md 'Gate-0 record' and TRUSTED-BASE.md."
+exit 1
--- a/verification/extract.sh
+++ b/verification/extract.sh
@ -0,0 +1,52 @@
+#!/usr/bin/env bash
+# Regenerate the Lean model in gen/ from the pinned fips205 snapshot.
+#
+# SCOPE: the SLH-DSA verify path, parameter set SLH-DSA-SHA2-128s
+#   roots: slh_verify(_internal), fors_pk_from_sig, ht_verify,
+#          xmss_pk_from_sig, wots_pk_from_sig, chain
+#   (sign/keygen are out of scope; the six hash oracles are opaque —
+#    see TRUSTED-BASE.md.)
+#
+#   Rust --charon--> SlhVerify.llbc --aeneas--> gen/SlhVerify/*.lean
+#
+# PHASE-1 PRECONDITION (gate-0 finding, 2026-07-22): upstream models the
+# hash family as `crate::hashers::Hashers`, a struct of plain function
+# pointers, which Aeneas cannot translate (3 unique errors, the only
+# obstruction in the whole cone). Until the Aeneas-compat patch in
+# fips205-source replaces that struct with named opaque free functions
+# on the verify path (the curve25519-dalek-source sha512-shim pattern),
+# this script produces a PARTIAL model. Do not build proofs on a partial
+# model; check.sh stays non-green until extraction is clean.
+#
+# Usage:  ./extract.sh
+set -euo pipefail
+
+source ~/aeneas-toolchain/env.sh
+HERE="$(cd "$(dirname "$0")" && pwd)"
+CRATE=~/GitClone/FormalVerification/sources/fips205-source
+
+echo "[1/2] charon: Rust -> LLBC (verify cone, SHA2-128s, hash oracles opaque)"
+cd "$CRATE"
+charon cargo --preset=aeneas \
+  --start-from 'crate::slh::slh_verify' \
+  --start-from 'crate::slh::slh_verify_internal' \
+  --start-from 'crate::fors::fors_pk_from_sig' \
+  --start-from 'crate::hypertree::ht_verify' \
+  --start-from 'crate::xmss::xmss_pk_from_sig' \
+  --start-from 'crate::wots::wots_pk_from_sig' \
+  --start-from 'crate::wots::chain' \
+  --opaque 'sha2' --opaque 'sha3' --opaque 'zeroize' --opaque 'rand_core' \
+  --opaque 'crate::hashers::sha2_cat_1' \
+  --opaque 'crate::hashers::sha2_cat_3_5' \
+  --opaque 'crate::hashers::shake' \
+  --hide-marker-traits \
+  --dest-file "$HERE/SlhVerify.llbc" \
+  -- --no-default-features --features slh_dsa_sha2_128s
+
+echo "[2/2] aeneas: LLBC -> Lean (split files, SlhVerify.* modules;"
+echo "        hand-maintained TypesExternal.lean / FunsExternal.lean are"
+echo "        NOT overwritten once they exist)"
+cd "$HERE"
+aeneas -backend lean -split-files -subdir SlhVerify -dest gen SlhVerify.llbc
+
+echo "Done. Now run ./check.sh (expect non-green until phase 1 lands)."
--- a/verification/lean-guard
+++ b/verification/lean-guard
@ -0,0 +1,189 @@
+#!/usr/bin/env bash
+# ────────────────────────────────────────────────────────────────────────────
+# lean-guard — HARD-CAPPED Lean compiler wrapper.
+#
+# Successor to lean-safe after the 2026-07-02 OOM incident: a single `lean`
+# elaboration (tactic-search blowup: simp[*]/scalar_tac over a ~60-hypothesis
+# context with 2^256-scale literals) grew to 12.2GB RSS and was killed by the
+# GLOBAL kernel OOM killer, taking the driving session down with it.
+# lean-safe's guards (timeout + affinity + PREFLIGHT headroom) cannot stop
+# that: the process passes preflight, then balloons inside its timeout.
+#
+# NEW GUARDS (in addition to all lean-safe guards):
+#   A. lean -M <MB>                  — Lean's internal cap: elaboration aborts
+#                                      with a clean "maximum memory exceeded"
+#                                      error. First line of defense; graceful.
+#   B. systemd-run --user --scope
+#        -p MemoryMax / MemorySwapMax — kernel cgroup cap around the process:
+#                                      if Lean's own accounting misses (C-level
+#                                      allocations), the cgroup kills ONLY this
+#                                      lean, never the session, never the box.
+#   C. flock on /tmp/lean-guard.lock — machine-wide single-flight: at most ONE
+#                                      lean compile at a time, regardless of
+#                                      how many agents/scripts are active.
+#
+# Env knobs (defaults for this 14GB / 8-core ThinkPad):
+#   LEAN_TIMEOUT      per-file wall clock seconds        (default 400)
+#   LEAN_MEM_MB       lean -M internal cap, MB           (default 4096)
+#   LEAN_CGROUP_MB    cgroup MemoryMax, MB               (default LEAN_MEM_MB+1024)
+#   LEAN_MAX_CORES    taskset core range                 (default 0-3)
+#   LEAN_MIN_FREE_MB  preflight available-RAM floor      (default 3072)
+#   LEAN_LOCK_WAIT    max seconds to wait for the lock   (default 7200)
+#
+# Usage:  lean-guard <file.lean> [extra lean args...]
+# The .olean output path is always computed as ${file%.lean}.olean.
+# Requires: lean on PATH (caller sources the toolchain env; typically run
+# inside `lake env` so LEAN_PATH is set — this wrapper does NOT clobber env).
+# ────────────────────────────────────────────────────────────────────────────
+set -uo pipefail
+
+# No core dumps: hitting the memory cap makes lean (and uutils `timeout`) abort;
+# those aborts are EXPECTED and their core dumps only trigger Ubuntu apport
+# popups and fill /var/crash. ulimit applies to this shell and every child.
+ulimit -c 0 2>/dev/null || true
+
+TIMEOUT_SEC=${LEAN_TIMEOUT:-400}
+MEM_MB=${LEAN_MEM_MB:-4096}
+CGROUP_MB=${LEAN_CGROUP_MB:-$((MEM_MB + 1024))}
+CORES=${LEAN_MAX_CORES:-0-3}
+MIN_FREE_MB=${LEAN_MIN_FREE_MB:-3072}
+LOCK_WAIT=${LEAN_LOCK_WAIT:-7200}
+LOCK_FILE=/tmp/lean-guard.lock
+LOG_FILE="${HOME}/.lean-guard.log"
+
+if ! command -v lean &>/dev/null; then
+    echo "FATAL: lean not on PATH — source ~/aeneas-toolchain/env.sh (and run inside lake env)"
+    exit 1
+fi
+if [ $# -eq 0 ]; then
+    echo "Usage: lean-guard <file.lean> [lean args...]"
+    exit 1
+fi
+
+LEAN_FILE="$1"; shift || true
+
+# ── Guard 1: source integrity (anti olean-clobber) ──────────────────────────
+if [ ! -f "$LEAN_FILE" ]; then
+    echo "MISSING: $LEAN_FILE"; exit 1
+fi
+if ! grep -qE '^[[:space:]]*(/-|import |namespace |theorem |def |open |set_option |--)' "$LEAN_FILE" 2>/dev/null; then
+    echo "FATAL: $LEAN_FILE is not Lean source (binary/olean data?)."
+    echo "  Restore: git checkout HEAD -- $LEAN_FILE"
+    exit 1
+fi
+
+# ── Guard 2: output path ─────────────────────────────────────────────────────
+case "$LEAN_FILE" in
+  *.lean) ;;
+  *) echo "FATAL: input lacks .lean extension"; exit 1 ;;
+esac
+OLEAN_FILE="${LEAN_FILE%.lean}.olean"
+[ "$OLEAN_FILE" = "$LEAN_FILE" ] && { echo "FATAL: output would clobber source"; exit 1; }
+
+# ── Guard C: machine-wide single-flight ─────────────────────────────────────
+exec 9>"$LOCK_FILE"
+if ! flock -w "$LOCK_WAIT" 9; then
+    echo "FATAL: could not acquire lean-guard lock within ${LOCK_WAIT}s (another compile stuck?)"
+    exit 1
+fi
+
+# ── Guard 3: preflight headroom (after lock: serialized measurement) ────────
+AVAIL_MB=$(free -m | awk '/Mem:/{print $7}')
+if [ "$AVAIL_MB" -lt "$MIN_FREE_MB" ]; then
+    echo "FATAL: only ${AVAIL_MB}MB available (< ${MIN_FREE_MB}MB floor) — refusing to compile"
+    exit 1
+fi
+
+
+# ── Guard 3b: global-headroom clamp (2026-07-03 swap-pressure incident) ─────
+# A cap is a PROMISE of memory to lean; never promise more than the machine
+# can afford right now. Requested caps that exceed (available − floor) are
+# clamped, so raising LEAN_MEM_MB can no longer starve the rest of the system
+# into swap even when lean itself stays within its cap. Clamp, don't fail:
+# most compiles peak far below their cap (measure before raising — the
+# incident's 9G scopes served a file whose true peak was 753MB).
+REQ_MEM_MB=$MEM_MB
+WAS_CLAMPED=0
+MAX_AFFORD_MB=$(( AVAIL_MB - MIN_FREE_MB ))
+if [ "$MEM_MB" -gt "$MAX_AFFORD_MB" ]; then
+    echo "lean-guard: clamping -M ${MEM_MB} -> ${MAX_AFFORD_MB}MB (avail=${AVAIL_MB}MB, floor=${MIN_FREE_MB}MB)"
+    MEM_MB=$MAX_AFFORD_MB
+    CGROUP_MB=$(( MEM_MB + 1024 ))
+    WAS_CLAMPED=1
+fi
+if [ "$MEM_MB" -lt 1024 ]; then
+    echo "FATAL: headroom clamp would leave lean < 1024MB — machine too loaded to compile safely"
+    exit 1
+fi
+
+echo "[$(date -u +%F' '%T)] $LEAN_FILE (t=${TIMEOUT_SEC}s M=${MEM_MB}MB cg=${CGROUP_MB}MB cores=$CORES avail=${AVAIL_MB}MB)" >> "$LOG_FILE"
+
+# ── Compile under both caps ──────────────────────────────────────────────────
+run_leancmd() {
+    taskset -c "$CORES" \
+      timeout --signal=TERM --kill-after=15 "$TIMEOUT_SEC" \
+      lean -M "$MEM_MB" -o "$OLEAN_FILE" "$LEAN_FILE" "$@"
+}
+do_compile() {
+    if systemd-run --user --scope -p MemoryMax=10M --quiet -- /bin/true 2>/dev/null; then
+        # --scope runs the command as a child of THIS shell (env inherited),
+        # merely placing it in a fresh cgroup with the hard caps below.
+        systemd-run --user --scope --quiet \
+            -p MemoryMax="${CGROUP_MB}M" -p MemorySwapMax=256M \
+            -- taskset -c "$CORES" \
+               timeout --signal=TERM --kill-after=15 "$TIMEOUT_SEC" \
+               lean -M "$MEM_MB" -o "$OLEAN_FILE" "$LEAN_FILE" "$@"
+    else
+        echo "  (systemd-run unavailable — falling back to lean -M only)" >> "$LOG_FILE"
+        run_leancmd "$@"
+    fi
+}
+do_compile "$@"
+EXIT_CODE=$?
+
+# ── Guard 3a: lazy wait-and-retry after a clamped memory abort (pass 3) ─────
+# The clamp above protects the host, but under ambient memory pressure it
+# can cut a KNOWN-NEEDED cap (ReduceSpec peaks ~6.5G) and guarantee an
+# interpreter abort that reads like a proof regression. Lazy semantics keep
+# light files free: only when a CLAMPED run dies on memory (134 abort /
+# 137 cgroup kill) and LEAN_MEM_WAIT_SEC>0, wait — still under the
+# single-flight lock — until the ORIGINAL request is affordable, then retry
+# once at full cap. Default 0: behavior unchanged.
+MEM_WAIT_SEC=${LEAN_MEM_WAIT_SEC:-0}
+if [ "$WAS_CLAMPED" -eq 1 ] && [ "$MEM_WAIT_SEC" -gt 0 ]; then
+    WAITED=0
+    # Retry ladder: whenever headroom improves MATERIALLY (>= +1536MB over
+    # the cap that just died, or reaches the full request), retry at the
+    # new clamp. The full request may never be affordable on a loaded host
+    # even though the true peak is — climbing the ladder finds the passing
+    # clamp without knowing the peak. Monotone caps + deadline => bounded.
+    while { [ "$EXIT_CODE" -eq 134 ] || [ "$EXIT_CODE" -eq 137 ]; } \
+          && [ "$WAITED" -lt "$MEM_WAIT_SEC" ] && [ "$MEM_MB" -lt "$REQ_MEM_MB" ]; do
+        sleep 20; WAITED=$(( WAITED + 20 ))
+        AVAIL_MB=$(free -m | awk '/Mem:/{print $7}')
+        NEW_AFFORD=$(( AVAIL_MB - MIN_FREE_MB ))
+        if [ "$NEW_AFFORD" -ge "$REQ_MEM_MB" ] || [ "$NEW_AFFORD" -ge $(( MEM_MB + 1536 )) ]; then
+            MEM_MB=$(( NEW_AFFORD < REQ_MEM_MB ? NEW_AFFORD : REQ_MEM_MB ))
+            CGROUP_MB=$(( MEM_MB + 1024 ))
+            echo "lean-guard: clamped run died (rc=$EXIT_CODE); retrying at -M ${MEM_MB}MB after ${WAITED}s (avail=${AVAIL_MB}MB, request=${REQ_MEM_MB}MB)"
+            echo "[$(date -u +%F' '%T)] RETRY $LEAN_FILE (M=${MEM_MB}MB cg=${CGROUP_MB}MB avail=${AVAIL_MB}MB after ${WAITED}s)" >> "$LOG_FILE"
+            do_compile "$@"
+            EXIT_CODE=$?
+        fi
+    done
+    if [ "$EXIT_CODE" -eq 134 ] || [ "$EXIT_CODE" -eq 137 ]; then
+        echo "lean-guard: memory-death persists after ${WAITED}s of ladder retries (last -M ${MEM_MB}MB, request ${REQ_MEM_MB}MB) — keeping the failure"
+    fi
+fi
+
+case $EXIT_CODE in
+  0)   echo "  OK" >> "$LOG_FILE" ;;
+  124) echo "  TIMEOUT ${TIMEOUT_SEC}s" >> "$LOG_FILE"
+       echo "TIMEOUT: $LEAN_FILE exceeded ${TIMEOUT_SEC}s" ;;
+  137) echo "  KILLED (cgroup MemoryMax ${CGROUP_MB}MB hit)" >> "$LOG_FILE"
+       echo "KILLED: $LEAN_FILE hit the ${CGROUP_MB}MB cgroup cap (contained — machine unharmed)" ;;
+  *)   echo "  FAILED exit $EXIT_CODE (lean error, possibly '-M ${MEM_MB}MB exceeded')" >> "$LOG_FILE" ;;
+esac
+# stale partial olean from a failed compile must not poison later imports
+[ $EXIT_CODE -ne 0 ] && rm -f "$OLEAN_FILE"
+exit $EXIT_CODE