Phase 1: clean extraction + type-checking SLH-DSA-SHA2-128s model

The gate-0 fn-pointer blocker is cleared. This commits the phase-1
deliverable:

- verification/extract.sh: re-pointed at the monomorphic root
  crate::verify_mono::slh_verify_128s with crate::verify_mono::oracle as
  the opaque SHA-2 boundary (against fips205-source @ 2d89ee3).
- verification/gen/SlhVerify: the extracted Lean model — 62 defs, the
  full verify cone (chain -> wots -> xmss -> ht -> fors ->
  slh_verify_internal) up to the apex verify_mono.slh_verify_128s. No
  sorry, no admit.
- verification/gen/SlhVerify/FunsExternal.lean + TypesExternal.lean:
  hand-maintained externals with the two-class justification header —
  (1) the five SHA-2 hash oracles = the deliberate cryptographic
  boundary (the only axioms the apex certificate will carry beyond
  Lean's three); (2) transpiler plumbing (try_from, is_err, iterator
  Step/Take, zeroize) adopted as axioms for the phase-1 type-check, to
  be discharged in the proof phase.
- verification/check.sh: real Phase-1 button — compiles the model under
  lean-guard (memory-capped, serialized). GREEN. Still says NOTHING
  PROVEN: a well-formed model is not a correct one.

Zero certificates. Proof layers (chain semantics -> ... -> acceptance
equation) are the next task.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

.gitignore

@@ -1,3 +1,5 @@
 *.olean
 target/
 .lake/
+*_Template.lean
+SlhVerify.llbc

README.md

@@ -5,12 +5,26 @@ 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
+## STATUS: MODEL EXTRACTED & TYPE-CHECKS — NOTHING PROVEN YET
 
-There are **zero certificates** in this repository. `verification/check.sh`
+There are still **zero certificates** in this repository. What phase 1
-exits non-green and says so. Every claim in this README below the line
+established (2026-07-22):
-"What will be claimed" is a *plan*, not a result. (Honesty invariant H5:
+
-an honest gap outranks a hollow certificate.)
+- the Aeneas-compat patch landed in the snapshot (an additive monomorphic
+  SHA2-128s verify module reached through a named hash-oracle boundary);
+- **charon and aeneas both exit 0** on the full verify cone — the gate-0
+  fn-pointer blocker is gone;
+- the extracted Lean model (`verification/gen/SlhVerify`, 62 defs, apex
+  `verify_mono.slh_verify_128s`) **type-checks under lean-guard**
+  (`verification/check.sh` Phase 1 is green);
+- fidelity of the monomorphic path is pinned by a differential test in the
+  snapshot that agrees with the deployed verifier on valid / corrupted /
+  wrong-message signatures.
+
+A green Phase-1 compile proves the model is **well-formed**, NOT that the
+verifier is correct. No operation theorem has been stated or proven. Every
+claim under "What will be claimed" remains a *plan* (H5: an honest gap
+outranks a hollow certificate).
 
 ## Subject
 
@@ -61,12 +75,18 @@ this repository was created:
   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
+- **Phase 1 — DONE (2026-07-22)**: the Aeneas-compat patch landed in
-  `fips205-source` will replace the fn-pointer struct with named opaque
+  `fips205-source` (snapshot `2d89ee3`): an additive monomorphic SHA2-128s
-  free functions on the verify path — the same pattern as the
+  verify module (`src/verify_mono.rs`) whose hash suite is reached through
-  `sha512_new/update/finalize` shims in `curve25519-dalek-source`'s
+  named free functions in `verify_mono::oracle` (marked opaque at the
-  verify glue. Until that patch lands, `verification/extract.sh`
+  Charon boundary) — the `sha512_*`-shim pattern. Two further compat
-  documents intent and produces a partial model.
+  refinements: the message-digest input M' passes as a single `&[u8]`
+  (nested `&[&[u8]]` is untranslatable), and one `let-else` became the
+  `is_err`/`unwrap` idiom. `verification/extract.sh` now re-derives the
+  model from the mono root; charon + aeneas both exit 0, and
+  `verification/check.sh` compiles the result. The generic paths and all
+  twelve parameter sets are untouched (the only change to existing code is
+  two lines wiring the module).
 
 ## What will be claimed (when the button is green, not before)
 

verification/check.sh

@@ -1,12 +1,44 @@
 #!/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.
+# PHASE 1 (current): compiles the extracted Lean model (gen/SlhVerify) under
+# lean-guard. Green here means the monomorphic SHA2-128s verify cone
+# translated and TYPE-CHECKS — it does NOT yet mean anything is proven. There
+# are zero certificates; the proof layers come next. This script grows a
+# Phase-2 (proofs) and Phase-3 (axiom audit) section as the pyramid rises,
+# exactly like the ed25519 check.sh.
 set -euo pipefail
 
-echo "fips205-slhdsa-verified — check"
+HERE="$(cd "$(dirname "$0")" && pwd)"
-echo "================================"
+source ~/aeneas-toolchain/env.sh
-echo "SKELETON: 0 certificates. NOTHING PROVEN YET."
+AENEAS_LEAN="$AENEAS_HOME/backends/lean"
-echo "Campaign phase 1 (Aeneas-compat patch + clean extraction) has not"
+TIMEOUT="${LEAN_TIMEOUT:-300}"
-echo "landed. See README.md 'Gate-0 record' and TRUSTED-BASE.md."
+CORES="${LEAN_MAX_CORES:-4}"
-exit 1
+
+# Import order (each depends on the previous).
+GEN_MODULES=(
+  "SlhVerify/TypesExternal"
+  "SlhVerify/Types"
+  "SlhVerify/FunsExternal"
+  "SlhVerify/Funs"
+)
+
+echo "fips205-slhdsa-verified — check (PHASE 1: model compile only)"
+echo "============================================================"
+echo "NOTE: 0 certificates. A green compile proves the extracted model is"
+echo "well-formed; it does NOT prove the verifier correct. See README.md."
+echo
+
+LOG=$(mktemp /tmp/fips205-check-XXXX.log)
+cd "$AENEAS_LEAN"
+lake env bash -c "
+  set -euo pipefail
+  cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
+  compile() {
+    echo \"  · \$1\"
+    LEAN_TIMEOUT=$TIMEOUT LEAN_MAX_CORES=$CORES '$HERE/lean-guard' \"\${1}.lean\" 2>&1 | tee -a '$LOG' || { echo \"FAIL: \$1\"; exit 1; }
+  }
+  for m in ${GEN_MODULES[*]}; do compile \"\$m\"; done
+"
+echo
+echo "PHASE 1 GREEN: gen/SlhVerify model type-checks. Proofs are the next layer."

verification/extract.sh

@@ -25,20 +25,17 @@ 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)"
+echo "[1/2] charon: Rust -> LLBC (monomorphic SHA2-128s verify cone;"
+echo "        crate::verify_mono::oracle is the opaque SHA-2 boundary)"
 cd "$CRATE"
+# Single extraction root: the monomorphic entry. The five hash primitives
+# are reached through crate::verify_mono::oracle, marked opaque here — this
+# is the deliberate SHA-2 trust boundary (documented in TRUSTED-BASE.md).
+# The generic Hashers fn-pointer path is NOT in this cone by construction.
 charon cargo --preset=aeneas \
-  --start-from 'crate::slh::slh_verify' \
+  --start-from 'crate::verify_mono::slh_verify_128s' \
-  --start-from 'crate::slh::slh_verify_internal' \
+  --opaque 'crate::verify_mono::oracle' \
-  --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

verification/gen/SlhVerify/FunsExternal.lean

@@ -0,0 +1,200 @@
+/- ──────────────────────────────────────────────────────────────────────────────
+   gen/SlhVerify/FunsExternal.lean — hand-maintained external functions.
+
+   TWO CLASSES of external, per honesty invariants H4/H5:
+
+   (1) THE CRYPTOGRAPHIC BOUNDARY — the deliberate opaque axioms.
+       The five SLH-DSA-SHA2-128s hash primitives, reached by name from the
+       monomorphic verify path (verify_mono::oracle):
+         · verify_mono.oracle.f      — F  (chain / FORS leaf)
+         · verify_mono.oracle.h      — H  (Merkle node)
+         · verify_mono.oracle.t_l    — T_len (WOTS+ pk compression)
+         · verify_mono.oracle.t_len  — T_k   (FORS root compression)
+         · verify_mono.oracle.h_msg  — H_msg (message digest)
+       These are SHA-256-based; their correctness against FIPS 180-4 is the
+       standing hash-oracle boundary (see TRUSTED-BASE.md). The apex
+       certificate will carry EXACTLY these five beyond Lean's three kernel
+       axioms — nothing else.
+
+   (2) TRANSPILER PLUMBING — core-library externals Aeneas emits for this
+       extraction config (u32::try_from, Result::is_err, the iterator Step /
+       Take machinery driving `for` ranges, the zeroize blanket impls, the
+       TryFromIntError Debug impl). These carry NO cryptographic content.
+       They are adopted here as axioms so the model type-checks at phase 1
+       (no certificates exist yet, so H4's cone requirement is vacuous). The
+       proof phase will discharge each from Aeneas.Std / real definitions and
+       the #print axioms audit will then confirm only class (1) survives in
+       any certificate cone. Tracked as the phase-2 de-plumbing item.
+   ────────────────────────────────────────────────────────────────────────────── -/
+-- This is a template file: rename it to "FunsExternal.lean" and fill the holes.
+import Aeneas
+import SlhVerify.Types
+open Aeneas Aeneas.Std Result ControlFlow Error
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+/- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/
+set_option maxHeartbeats 1000000
+
+/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
+set_option maxRecDepth 2048
+open fips205
+
+/-- [core::convert::num::ptr_try_from_impls::{impl core::convert::TryFrom<usize, core::num::error::TryFromIntError> for u32}::try_from]:
+    Source: '/rustc/library/core/src/convert/num.rs', lines 300:12-300:64
+    Name pattern: [core::convert::num::ptr_try_from_impls::{core::convert::TryFrom<u32, usize, core::num::error::TryFromIntError>}::try_from]
+    Visibility: public -/
+@[rust_fun
+  "core::convert::num::ptr_try_from_impls::{core::convert::TryFrom<u32, usize, core::num::error::TryFromIntError>}::try_from"]
+axiom U32.Insts.CoreConvertTryFromUsizeTryFromIntError.try_from
+  :
+  Std.Usize → Result (core.result.Result Std.U32
+    core.num.error.TryFromIntError)
+
+/-- [core::convert::num::{impl core::convert::TryFrom<u64, core::num::error::TryFromIntError> for u32}::try_from]:
+    Source: '/rustc/library/core/src/convert/num.rs', lines 300:12-300:64
+    Name pattern: [core::convert::num::{core::convert::TryFrom<u32, u64, core::num::error::TryFromIntError>}::try_from]
+    Visibility: public -/
+@[rust_fun
+  "core::convert::num::{core::convert::TryFrom<u32, u64, core::num::error::TryFromIntError>}::try_from"]
+axiom U32.Insts.CoreConvertTryFromU64TryFromIntError.try_from
+  :
+  Std.U64 → Result (core.result.Result Std.U32
+    core.num.error.TryFromIntError)
+
+/-- [core::ops::arith::{impl core::ops::arith::Sub<&'_0 u32, u32> for u32}::sub]:
+    Source: '/rustc/library/core/src/internal_macros.rs', lines 38:12-38:68
+    Name pattern: [core::ops::arith::{core::ops::arith::Sub<u32, &'0 u32, u32>}::sub]
+    Visibility: public -/
+@[rust_fun "core::ops::arith::{core::ops::arith::Sub<u32, &'0 u32, u32>}::sub"]
+axiom U32.Insts.CoreOpsArithSubShared0U32U32.sub
+  : Std.U32 → Std.U32 → Result Std.U32
+
+/-- [core::iter::adapters::take::{impl core::iter::traits::iterator::Iterator<Clause0_Item> for core::iter::adapters::take::Take<I>}::next]:
+    Source: '/rustc/library/core/src/iter/adapters/take.rs', lines 36:4-36:55
+    Name pattern: [core::iter::adapters::take::{core::iter::traits::iterator::Iterator<core::iter::adapters::take::Take<@I>, @Clause0_Item>}::next]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::adapters::take::{core::iter::traits::iterator::Iterator<core::iter::adapters::take::Take<@I>, @Clause0_Item>}::next"]
+axiom core.iter.adapters.take.Take.Insts.CoreIterTraitsIteratorIterator.next
+  {I : Type} {Clause0_Item : Type} (traitsiteratorIteratorInst :
+  core.iter.traits.iterator.Iterator I Clause0_Item) :
+  core.iter.adapters.take.Take I → Result ((Option Clause0_Item) ×
+    (core.iter.adapters.take.Take I))
+
+/-- [core::iter::range::{impl core::iter::range::Step for u32}::backward_checked]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 290:16-290:74
+    Name pattern: [core::iter::range::{core::iter::range::Step<u32>}::backward_checked]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<u32>}::backward_checked"]
+axiom U32.Insts.CoreIterRangeStep.backward_checked
+  : Std.U32 → Std.Usize → Result (Option Std.U32)
+
+/-- [core::iter::range::{impl core::iter::range::Step for u32}::forward_checked]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 282:16-282:73
+    Name pattern: [core::iter::range::{core::iter::range::Step<u32>}::forward_checked]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<u32>}::forward_checked"]
+axiom U32.Insts.CoreIterRangeStep.forward_checked
+  : Std.U32 → Std.Usize → Result (Option Std.U32)
+
+/-- [core::iter::range::{impl core::iter::range::Step for u32}::steps_between]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 271:16-271:84
+    Name pattern: [core::iter::range::{core::iter::range::Step<u32>}::steps_between]
+    Visibility: public -/
+@[rust_fun "core::iter::range::{core::iter::range::Step<u32>}::steps_between"]
+axiom U32.Insts.CoreIterRangeStep.steps_between
+  : Std.U32 → Std.U32 → Result (Std.Usize × (Option Std.Usize))
+
+/-- [core::iter::traits::iterator::Iterator::take]:
+    Source: '/rustc/library/core/src/iter/traits/iterator.rs', lines 1447:4-1449:20
+    Name pattern: [core::iter::traits::iterator::Iterator::take]
+    Visibility: public -/
+@[rust_fun "core::iter::traits::iterator::Iterator::take"]
+axiom core.iter.traits.iterator.Iterator.take.default
+  {Self : Type} {Clause0_Item : Type} (IteratorInst :
+  core.iter.traits.iterator.Iterator Self Clause0_Item) :
+  Self → Std.Usize → Result (core.iter.adapters.take.Take Self)
+
+/-- [core::num::error::{impl core::fmt::Debug for core::num::error::TryFromIntError}::fmt]:
+    Source: '/rustc/library/core/src/num/error.rs', lines 9:9-9:14
+    Name pattern: [core::num::error::{core::fmt::Debug<core::num::error::TryFromIntError>}::fmt]
+    Visibility: public -/
+@[rust_fun
+  "core::num::error::{core::fmt::Debug<core::num::error::TryFromIntError>}::fmt"]
+axiom core.num.error.TryFromIntError.Insts.CoreFmtDebug.fmt
+  :
+  core.num.error.TryFromIntError → core.fmt.Formatter → Result
+    ((core.result.Result Unit core.fmt.Error) × core.fmt.Formatter)
+
+/-- [core::result::{core::result::Result<T, E>}::is_err]:
+    Source: '/rustc/library/core/src/result.rs', lines 646:4-646:38
+    Name pattern: [core::result::{core::result::Result<@T, @E>}::is_err]
+    Visibility: public -/
+@[rust_fun "core::result::{core::result::Result<@T, @E>}::is_err"]
+axiom core.result.Result.is_err
+  {T : Type} {E : Type} : core.result.Result T E → Result Bool
+
+/-- [zeroize::{impl zeroize::Zeroize for Z}::zeroize]:
+    Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/zeroize-1.9.0/src/lib.rs', lines 274:4-274:25
+    Name pattern: [zeroize::{zeroize::Zeroize<@Z>}::zeroize]
+    Visibility: public -/
+@[rust_fun "zeroize::{zeroize::Zeroize<@Z>}::zeroize"]
+axiom zeroize.Zeroize.Blanket.zeroize
+  {Z : Type} (DefaultIsZeroesInst : zeroize.DefaultIsZeroes Z) : Z → Result Z
+
+/-- [zeroize::{impl zeroize::Zeroize for [Z; N]}::zeroize]:
+    Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/zeroize-1.9.0/src/lib.rs', lines 346:4-346:25
+    Name pattern: [zeroize::{zeroize::Zeroize<[@Z; @N]>}::zeroize]
+    Visibility: public -/
+@[rust_fun "zeroize::{zeroize::Zeroize<[@Z; @N]>}::zeroize"]
+axiom Array.Insts.ZeroizeZeroize.zeroize
+  {Z : Type} {N : Std.Usize} (ZeroizeInst : zeroize.Zeroize Z) :
+  Array Z N → Result (Array Z N)
+
+/-- [zeroize::__internal::{impl zeroize::__internal::AssertZeroize for T}::zeroize_or_on_drop]:
+    Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/zeroize-1.9.0/src/lib.rs', lines 846:8-846:40
+    Name pattern: [zeroize::__internal::{zeroize::__internal::AssertZeroize<@T>}::zeroize_or_on_drop]
+    Visibility: public -/
+@[rust_fun
+  "zeroize::__internal::{zeroize::__internal::AssertZeroize<@T>}::zeroize_or_on_drop"]
+axiom zeroize.__internal.AssertZeroize.Blanket.zeroize_or_on_drop
+  {T : Type} (ZeroizeInst : zeroize.Zeroize T) : T → Result T
+
+/-- [fips205::verify_mono::oracle::f]:
+    Source: 'src/verify_mono.rs', lines 49:4-51:5 -/
+axiom verify_mono.oracle.f
+  (N : Std.Usize) :
+  Slice Std.U8 → types.Adrs → Slice Std.U8 → Result (Array Std.U8 N)
+
+/-- [fips205::verify_mono::oracle::h]:
+    Source: 'src/verify_mono.rs', lines 54:4-56:5 -/
+axiom verify_mono.oracle.h
+  (N : Std.Usize) :
+  Slice Std.U8 → types.Adrs → Slice Std.U8 → Slice Std.U8 → Result
+    (Array Std.U8 N)
+
+/-- [fips205::verify_mono::oracle::t_l]:
+    Source: 'src/verify_mono.rs', lines 60:4-64:5 -/
+axiom verify_mono.oracle.t_l
+  {X : Std.Usize} {N : Std.Usize} :
+  Slice Std.U8 → types.Adrs → Array (Array Std.U8 N) X → Result (Array
+    Std.U8 N)
+
+/-- [fips205::verify_mono::oracle::t_len]:
+    Source: 'src/verify_mono.rs', lines 69:4-73:5 -/
+axiom verify_mono.oracle.t_len
+  {X : Std.Usize} {N : Std.Usize} :
+  Slice Std.U8 → types.Adrs → Array (Array Std.U8 N) X → Result (Array
+    Std.U8 N)
+
+/-- [fips205::verify_mono::oracle::h_msg]:
+    Source: 'src/verify_mono.rs', lines 81:4-85:5 -/
+axiom verify_mono.oracle.h_msg
+  (M : Std.Usize) :
+  Slice Std.U8 → Slice Std.U8 → Slice Std.U8 → Slice Std.U8 → Result
+    (Array Std.U8 M)
+

verification/gen/SlhVerify/Types.lean

@@ -0,0 +1,101 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [fips205]: type definitions
+import Aeneas
+import SlhVerify.TypesExternal
+open Aeneas Aeneas.Std Result ControlFlow Error
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+/- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/
+set_option maxHeartbeats 1000000
+
+/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
+set_option maxRecDepth 2048
+
+namespace fips205
+
+/-- Trait declaration: [zeroize::Zeroize]
+    Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/zeroize-1.9.0/src/lib.rs', lines 245:0-245:17
+    Name pattern: [zeroize::Zeroize]
+    Visibility: public -/
+@[rust_trait "zeroize::Zeroize"]
+structure zeroize.Zeroize (Self : Type) where
+  zeroize : Self → Result Self
+
+/-- Trait declaration: [zeroize::DefaultIsZeroes]
+    Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/zeroize-1.9.0/src/lib.rs', lines 255:0-255:49
+    Name pattern: [zeroize::DefaultIsZeroes]
+    Visibility: public -/
+@[rust_trait "zeroize::DefaultIsZeroes"
+  (parentClauses := ["coremarkerCopyInst", "coredefaultDefaultInst"])]
+structure zeroize.DefaultIsZeroes (Self : Type) where
+  coremarkerCopyInst : core.marker.Copy Self
+  coredefaultDefaultInst : core.default.Default Self
+
+/-- [fips205::types::Adrs]
+    Source: 'src/types.rs', lines 116:0-132:1 -/
+structure types.Adrs where
+  f0 : Array Std.U8 4#usize
+  f1 : Array Std.U8 4#usize
+  f2 : Array Std.U8 4#usize
+  f3 : Array Std.U8 4#usize
+  f4 : Array Std.U8 4#usize
+  f5 : Array Std.U8 4#usize
+  f6 : Array Std.U8 4#usize
+  f7 : Array Std.U8 4#usize
+
+/-- [fips205::types::WotsSig]
+    Source: 'src/types.rs', lines 80:0-82:1 -/
+structure types.WotsSig (LEN : Std.Usize) (N : Std.Usize) where
+  data : Array (Array Std.U8 N) LEN
+
+/-- [fips205::types::XmssSig]
+    Source: 'src/types.rs', lines 91:0-94:1 -/
+structure types.XmssSig (HP : Std.Usize) (LEN : Std.Usize) (N : Std.Usize)
+  where
+  sig_wots : types.WotsSig LEN N
+  auth : Array (Array Std.U8 N) HP
+
+/-- [fips205::types::HtSig]
+    Source: 'src/types.rs', lines 73:0-75:1 -/
+structure types.HtSig (D : Std.Usize) (HP : Std.Usize) (LEN : Std.Usize) (N :
+  Std.Usize) where
+  xmss_sigs : Array (types.XmssSig HP LEN N) D
+
+/-- [fips205::types::Auth]
+    Source: 'src/types.rs', lines 66:0-68:1 -/
+structure types.Auth (A : Std.Usize) (N : Std.Usize) where
+  tree : Array (Array Std.U8 N) A
+
+/-- [fips205::types::ForsSig]
+    Source: 'src/types.rs', lines 53:0-56:1 -/
+structure types.ForsSig (A : Std.Usize) (K : Std.Usize) (N : Std.Usize) where
+  private_key_value : Array (Array Std.U8 N) K
+  auth : Array (types.Auth A N) K
+
+/-- [fips205::types::SlhDsaSig]
+    Source: 'src/types.rs', lines 19:0-30:1 -/
+structure types.SlhDsaSig (A : Std.Usize) (D : Std.Usize) (HP : Std.Usize) (K :
+  Std.Usize) (LEN : Std.Usize) (N : Std.Usize) where
+  randomness : Array Std.U8 N
+  fors_sig : types.ForsSig A K N
+  ht_sig : types.HtSig D HP LEN N
+
+/-- [fips205::types::SlhPublicKey]
+    Source: 'src/types.rs', lines 35:0-38:1 -/
+structure types.SlhPublicKey (N : Std.Usize) where
+  pk_seed : Array Std.U8 N
+  pk_root : Array Std.U8 N
+
+/-- [fips205::types::ForsPk]
+    Source: 'src/types.rs', lines 60:0-62:1 -/
+structure types.ForsPk (N : Std.Usize) where
+  key : Array Std.U8 N
+
+/-- [fips205::types::WotsPk]
+    Source: 'src/types.rs', lines 86:0-86:61 -/
+@[reducible]
+def types.WotsPk (N : Std.Usize) := Array Std.U8 N
+
+end fips205

verification/gen/SlhVerify/TypesExternal.lean

@@ -0,0 +1,23 @@
+/- gen/SlhVerify/TypesExternal.lean — hand-maintained external types.
+   The single external type is a core-library error type introduced by
+   u32::try_from; it carries no cryptographic content. -/
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes.
+import Aeneas
+open Aeneas Aeneas.Std Result ControlFlow Error
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+/- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/
+set_option maxHeartbeats 1000000
+
+/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
+set_option maxRecDepth 2048
+
+/-- [core::num::error::TryFromIntError]
+    Source: '/rustc/library/core/src/num/error.rs', lines 10:0-10:26
+    Name pattern: [core::num::error::TryFromIntError]
+    Visibility: public -/
+@[rust_type "core::num::error::TryFromIntError"]
+axiom core.num.error.TryFromIntError : Type
+