diff --git a/verification/PROVENANCE.json b/verification/PROVENANCE.json
index a58bcb6..aa14396 100644
--- a/verification/PROVENANCE.json
+++ b/verification/PROVENANCE.json
@@ -48,12 +48,15 @@
   "harness_integrity_sha256": {
     "_comment": "The harness is part of the trusted computing base and its membership is now SELF-DERIVING: check.sh requires every executable file in verification/ to appear here (round-8 review \u2014 a hardcoded list was itself a second thing to keep in sync), plus Proofs/Audit.lean, which is not executable but computes the digest it is judged by. check.sh itself is excluded: it cannot pin itself, and is disclosed as trusted-unbound in TRUSTED-BASE.md item 11. Pinning check-selftest.sh matters beyond the button: it is the only artifact demonstrating the gates work, and its assertions have been defective in four consecutive rounds, so weakening it is now a reviewable pin rotation rather than an unnoticed edit.",
     "lean-guard": "690d861cfd81b327604ffd5ef85599ee01b2bcd943907f5b71b8b6f99bad418f",
-    "Proofs/Audit.lean": "6108b97d75a8a8e8e0b9bef642ba887ea1ae8b17ba5b7c11d66400bfd2847d9e",
+    "Proofs/Audit.lean": "3a1540187622c47ee2de4bf1dd2379fbbabf4a3d6ec902f2b602dcf486731691",
     "check-selftest.sh": "c6811482e25ae6e1fffa6ca50e60541e8e609a70c951db6bec4d2d39a4849e9a",
     "drill.sh": "915cf9310fa168c14ca5d76a1b84fd3b19acdfef9dfd0b03b01b19883548719e",
     "extract.sh": "01cff43c350ed8eaac0e65ccd7599b68fef47c9434cdb5ad01c92d2127a3bbe9",
     "model-correspondence.py": "1942177f13d6ae229d87a3b0b33f7fbb4b2ae20fe1059cc83010e73f6a156427",
-    "MODEL-CORRESPONDENCE.txt": "77bd374a60152689edcb3350c2a2547c6aaad192629e39e86d8548d2bad3f748"
+    "MODEL-CORRESPONDENCE.txt": "77bd374a60152689edcb3350c2a2547c6aaad192629e39e86d8548d2bad3f748",
+    "inventory_gate.sh": "3ebc8027f14c9e037f36322ef4119183c33214658efcc1a7bc985a98a9c32e4e",
+    "inventory-allowlist.txt": "6b27fb410f61d0d6e0d17f9089a5dc1f53027bec507c6c7c180554c5c8f40ede",
+    "driver-allowlist.txt": "5f9a4167068407ae5e31ec0c7c55d78af455a7ed7f1913b79912f6ae50c13686"
   },
   "audit_gate": "verification/Proofs/Audit.lean \u2014 in-Lean audit (round 5). Per certificate: exact cone equality (collectAxioms) + elaborated-statement check. Enumeration: EVERY declaration kind (def/theorem/opaque/axiom \u2014 round 4 matched theorems only, so a `def : False` passed) in the eight certificate modules AND in Audit.lean itself (the auditor is not exempt). Binding digest: check.sh binds to the SHA-256 of a canonical AUDIT-MANIFEST block covering the POLICY constants (allowedBoundary + certModules \u2014 round-5 NEW-1: widening allowedBoundary previously re-opened the False-proof with the fingerprint byte-identical), every certificate's fully-elaborated statement, and every reachable specification definition's fully-elaborated BODY (round-5 NEW-2: redefining a reference fold to *be* the extracted loop previously left cone and fingerprint intact while the certificate degenerated to `loop = loop`). The 32-bit Expr.hash is retained only as a per-certificate diagnostic, not as the binding. Fail-closed; adversarially exercised by check-selftest.sh. check.sh Phase 0 additionally purges stale .olean files, forbids stray .lean outside gen/ and Proofs/, and pins model + harness bytes."
 }
\ No newline at end of file
diff --git a/verification/Proofs/Audit.lean b/verification/Proofs/Audit.lean
index 748a55b..7c713d6 100644
--- a/verification/Proofs/Audit.lean
+++ b/verification/Proofs/Audit.lean
@@ -93,6 +93,21 @@ def manifest : List (Name × List Name × UInt64) :=
     (`fips205.base2b_outer_loop_eq,        kernel3,                                           324621577),
     (`fips205.slh_verify_128s_accepts_iff, kernel3 ++ [oracleF, oracleH, oracleTL, oracleTLen, oracleHMsg], 2489587792) ]
 
+/-- Declaration kind, in the vocabulary the estate's allowlists already use.
+    A KIND is part of the record because "the name is still there" and "the
+    thing behind the name is still the same kind of thing" are different
+    facts: a theorem quietly replaced by a `def` keeps its name and loses its
+    meaning. -/
+def kindOf : ConstantInfo → String
+  | .axiomInfo _  => "axiom"
+  | .thmInfo _    => "theorem"
+  | .opaqueInfo _ => "opaque"
+  | .defnInfo _   => "def"
+  | .quotInfo _   => "quot"
+  | .inductInfo _ => "inductive"
+  | .ctorInfo _   => "ctor"
+  | .recInfo _    => "rec"
+
 /-- Deterministic name ordering for the canonical serialization. -/
 def sortNames (l : List Name) : List Name :=
   ((l.map toString).toArray.qsort (· < ·)).toList.map (·.toName)
@@ -172,18 +187,39 @@ elab "auditCones" : command => do
   let manifestNames := manifest.map (·.1)
   let mut nEnum := 0
   let mut certsSeen : Array Name := #[]
+  let mut invRows : Array String := #[]
+  let mut drvRows : Array String := #[]
   for (nm, ci) in env.constants.toList do
     let scope : Option String :=
       match env.getModuleIdxFor? nm with
       | some idx =>
           let m := env.header.moduleNames[idx.toNat]!
           if certModules.contains m then some (toString m) else none
-      | none => if nm.isInternal then none else some "Proofs.Audit (this file)"
+      -- INTERNAL NAMES ARE NO LONGER EXEMPT. They were skipped here, which
+      -- was harmless while nothing compared this walk against the kernel's
+      -- view — and became a hole the moment it did: Phase 3b reads the object
+      -- files, which contain the compiler's auxiliaries, so exempting them
+      -- here would leave the accounting identity permanently short and force
+      -- it to be "explained" by a constant. A residual that has to be
+      -- explained away is the shape of the fudge term four-fork data refuted
+      -- in the ed25519 repos.
+      | none => some "Proofs.Audit"
     match scope with
     | none => pure ()
     | some where_ =>
       nEnum := nEnum + 1
       if manifestNames.contains nm then certsSeen := certsSeen.push nm
+      -- THE ROW. Same shape as the corpus walks in the ed25519 repositories:
+      -- module, name, kind, cone. The originating module is part of the record
+      -- because two modules may legitimately declare the same name, and keyed
+      -- on name alone one would be covered by the other's entry.
+      let rowCone := (← collectAxioms nm).toList
+      let rowKind := kindOf ci
+      let rowStr := s!"{where_}|{nm}|{rowKind}|{String.intercalate "," ((sortNames rowCone).map toString)}"
+      if where_ == "Proofs.Audit" then
+        drvRows := drvRows.push s!"DRV|{rowStr}"
+      else
+        invRows := invRows.push s!"INV|{rowStr}"
       match ci with
       | .axiomInfo _ =>
           -- the five oracle axioms live in gen/ (Phase-0 pinned); an axiom
@@ -232,6 +268,13 @@ elab "auditCones" : command => do
   -- check.sh prints the certificate list it gets from HERE, not from a hand-kept
   -- bash array (drill finding: the one authoritative claim string was the one
   -- thing nothing bound — adding a name to it printed a cert that never existed).
+  -- The two walks, emitted for check.sh to diff against committed allowlists in
+  -- BOTH directions. A trailer per walk, so a truncated or crashed emission can
+  -- never pass as an empty diff.
+  for r in invRows.qsort (· < ·) do IO.println r
+  IO.println s!"INV-COUNT|{invRows.size}"
+  for r in drvRows.qsort (· < ·) do IO.println r
+  IO.println s!"DRV-COUNT|{drvRows.size}"
   logInfo s!"CERTIFICATES: {String.intercalate " " (manifestNames.map toString)}"
   logInfo s!"exact-cone audit PASSED: {manifest.length} certificates (cones + statements), {specs.toList.length} specification constants pinned, {nEnum} declarations enumerated clean"
 
diff --git a/verification/check.sh b/verification/check.sh
index 1057974..ff02a4d 100755
--- a/verification/check.sh
+++ b/verification/check.sh
@@ -270,6 +270,8 @@ fi
 echo "  ✓ $(grep -oF 'exact-cone audit PASSED' <<<"$AUD_OUT" | head -1)"
 echo "  ✓ audit-manifest digest matches (sha256 ${EXPECTED_AUDIT_SHA256:0:16}…)"
 
+
+
 # ── Phase 3b: kernel-side axiom-declaration gate ────────────────────────────
 # WHY A SECOND GATE ON THE SAME PROPERTY. Phase 3's audit runs INSIDE Lean and
 # reads `env.constants` after the imports — an ELABORATION-TIME view. That view
@@ -320,6 +322,12 @@ run_cmd do
     let (mod, _) ← readModuleData p
     for ci in mod.constants do
       nConst := nConst + 1
+      -- The kernel's OWN list of names, for the accounting identity in check.sh:
+      -- every constant the kernel holds must be accounted for by one of the two
+      -- environment walks. Emitted rather than counted, because a count cannot
+      -- say WHICH constant is unaccounted for — the residual would then have to
+      -- be "explained", which is how a fudge term gets born.
+      IO.println s!"KERNEL-NAME|{ci.name}"
       if ci matches .axiomInfo _ then
         errs := errs.push s!"  {name}: {ci.name}"
   unless errs.isEmpty do
@@ -336,18 +344,65 @@ GATE_RC=0
 # The temp source AND its artifact are removed on BOTH paths: under `set -e` a
 # bare rm after the call never runs when the gate goes red, which is how the
 # ed25519 repos once accumulated 101 orphan .olean files.
+GATELOG=$(mktemp /tmp/slh-kernlog-XXXX.log)
 ( cd "$AENEAS_LEAN" && lake env bash -c "
   set -euo pipefail
   cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
   cd '$HERE'
   LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=$MEM '$HERE/lean-guard' '$GATE'
-" ) || GATE_RC=$?
+" ) 2>&1 | tee "$GATELOG" || GATE_RC=${PIPESTATUS[0]}
 rm -f "$GATE" "${GATE%.lean}.olean"
 if [ "$GATE_RC" -ne 0 ]; then
   echo "AXIOM SMUGGLING GATE FAILED (kernel-side) — see the error above."
   exit 1
 fi
 
+# ── Phase 3c: declaration coverage, both walks, both directions ─────────────
+# Phase 3 proves each certificate's cone is exact and that no declaration in
+# scope carries a disallowed axiom. It does NOT pin WHICH declarations exist:
+# a new one that happens to be clean, or a silently vanished one, both pass it.
+# These two gates diff the walks against committed allowlists in both
+# directions — UNCLASSIFIED for something in the environment and not the list,
+# STALE for the reverse — using the same implementation the ed25519 repositories
+# use for their corpus, with a tag for each surface.
+AUDROWS=$(mktemp /tmp/slh-audrows-XXXX.log)
+printf '%s\n' "$AUD_OUT" > "$AUDROWS"
+COVFAIL=0
+"$HERE/inventory_gate.sh" "$AUDROWS" "$HERE/inventory-allowlist.txt" INV || COVFAIL=1
+"$HERE/inventory_gate.sh" "$AUDROWS" "$HERE/driver-allowlist.txt"    DRV || COVFAIL=1
+
+# ── THE ACCOUNTING IDENTITY ─────────────────────────────────────────────────
+# Round-8 review (Claude, `accounting-certifies-enumeration`). The two walks
+# above are ENVIRONMENT views, taken while Audit.lean elaborates. Phase 3b reads
+# the OBJECT FILES. Every constant the kernel holds must be accounted for by one
+# of the two walks — otherwise a declaration exists that the button compiled,
+# the kernel sees, and no allowlist describes.
+#
+# SET CONTAINMENT, never arithmetic. An earlier version of this identity in the
+# ed25519 repositories carried a "+ N_DRIVERS" correction term fitted from one
+# repository; four-fork data refuted it (the residual was 2 regardless of driver
+# count). A residual that has to be explained is a fudge term waiting to absorb
+# the next real finding, so this compares NAMES and prints the ones missing.
+KERN=$(mktemp /tmp/slh-kern-XXXX.txt); ACCT=$(mktemp /tmp/slh-acct-XXXX.txt)
+LC_ALL=C grep '^KERNEL-NAME|' "$GATELOG" | cut -d'|' -f2 | LC_ALL=C sort -u > "$KERN"
+{ LC_ALL=C awk -F'|' '/^INV\|/{print $3}' "$HERE/inventory-allowlist.txt"
+  LC_ALL=C awk -F'|' '/^DRV\|/{print $3}' "$HERE/driver-allowlist.txt"
+} | LC_ALL=C sort -u > "$ACCT"
+UNACCOUNTED=$(LC_ALL=C comm -23 "$KERN" "$ACCT")
+if [ ! -s "$KERN" ]; then
+  echo "  ACCOUNTING FAILED: the kernel gate reported no names — the scan was vacuous"
+  COVFAIL=1
+elif [ -n "$UNACCOUNTED" ]; then
+  echo "  ACCOUNTING FAILED: the kernel holds constants that neither walk accounts for:"
+  printf '%s\n' "$UNACCOUNTED" | head -20 | sed 's/^/    /'
+  COVFAIL=1
+else
+  echo "  accounting: every one of $(wc -l < "$KERN") kernel constants is covered by the corpus inventory or the instrument surface"
+fi
+rm -f "$AUDROWS" "$KERN" "$ACCT"
+[ "$COVFAIL" = 0 ] || { echo "COVERAGE FAILED"; exit 1; }
+rm -f "$GATELOG"
+
 
 echo
 echo "ALL GREEN — model compiles, proofs compile, and every certificate cone"
diff --git a/verification/driver-allowlist.txt b/verification/driver-allowlist.txt
new file mode 100644
index 0000000..48a8f37
--- /dev/null
+++ b/verification/driver-allowlist.txt
@@ -0,0 +1,39 @@
+# driver-allowlist.txt — the AUDIT INSTRUMENT's own declaration surface,
+# with cones, gated by the same implementation that gates the corpus.
+# Round-8 review (Claude): enumeration is not audit. Rows carrying no cone,
+# covered by no allowlist, are counted and then examined by nothing.
+DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1._sparseCasesOn_3|def|propext
+DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1._sparseCasesOn_6|def|propext
+DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_11|def|
+DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_13|def|propext
+DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_15|def|
+DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_17|def|
+DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_19|def|Classical.choice,Quot.sound,propext
+DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_1|def|
+DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_21|def|
+DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_3|def|propext
+DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_6|def|propext
+DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_9|def|
+DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1|def|Classical.choice,Quot.sound,propext
+DRV|Proofs.Audit|SlhVerify.Audit.allowedBoundary|def|
+DRV|Proofs.Audit|SlhVerify.Audit.certModules|def|
+DRV|Proofs.Audit|SlhVerify.Audit.closureOf._sparseCasesOn_1|def|propext
+DRV|Proofs.Audit|SlhVerify.Audit.closureOf._unsafe_rec|def|Classical.choice,Quot.sound,propext
+DRV|Proofs.Audit|SlhVerify.Audit.closureOf.match_1|def|propext
+DRV|Proofs.Audit|SlhVerify.Audit.closureOf.match_4|def|
+DRV|Proofs.Audit|SlhVerify.Audit.closureOf|opaque|Classical.choice,Quot.sound,propext
+DRV|Proofs.Audit|SlhVerify.Audit.commandAuditCones|def|
+DRV|Proofs.Audit|SlhVerify.Audit.isSpecConst.match_1|def|
+DRV|Proofs.Audit|SlhVerify.Audit.isSpecConst|def|Classical.choice,Quot.sound,propext
+DRV|Proofs.Audit|SlhVerify.Audit.kernel3|def|
+DRV|Proofs.Audit|SlhVerify.Audit.kindOf.match_1|def|
+DRV|Proofs.Audit|SlhVerify.Audit.kindOf|def|
+DRV|Proofs.Audit|SlhVerify.Audit.manifest|def|
+DRV|Proofs.Audit|SlhVerify.Audit.normWs|def|Classical.choice,Quot.sound,propext
+DRV|Proofs.Audit|SlhVerify.Audit.oracleF|def|
+DRV|Proofs.Audit|SlhVerify.Audit.oracleHMsg|def|
+DRV|Proofs.Audit|SlhVerify.Audit.oracleH|def|
+DRV|Proofs.Audit|SlhVerify.Audit.oracleTLen|def|
+DRV|Proofs.Audit|SlhVerify.Audit.oracleTL|def|
+DRV|Proofs.Audit|SlhVerify.Audit.ppAll|def|Classical.choice,Quot.sound,propext
+DRV|Proofs.Audit|SlhVerify.Audit.sortNames|def|Classical.choice,Quot.sound,propext
diff --git a/verification/inventory-allowlist.txt b/verification/inventory-allowlist.txt
new file mode 100644
index 0000000..873ddc6
--- /dev/null
+++ b/verification/inventory-allowlist.txt
@@ -0,0 +1,270 @@
+# inventory-allowlist.txt — the audited corpus, one row per declaration:
+#   INV|module|name|kind|cone
+# Diffed in BOTH directions by inventory_gate.sh. A row here that is not in
+# the environment is STALE; a declaration not here is UNCLASSIFIED. Neither
+# passes. Regenerate deliberately and read the diff.
+INV|Proofs.ApexSpec|List.allM.eq_1|theorem|
+INV|Proofs.ApexSpec|List.allM.eq_2|theorem|
+INV|Proofs.ApexSpec|List.allM.eq_def|theorem|
+INV|Proofs.ApexSpec|_private.Proofs.ApexSpec.0.List.anyM.match_1.eq_1|theorem|
+INV|Proofs.ApexSpec|_private.Proofs.ApexSpec.0.List.anyM.match_1.eq_2|theorem|
+INV|Proofs.ApexSpec|_private.Proofs.ApexSpec.0.List.anyM.match_1.splitter|def|
+INV|Proofs.ApexSpec|_private.Proofs.ApexSpec.0.List.mapA.match_1.eq_1|theorem|
+INV|Proofs.ApexSpec|_private.Proofs.ApexSpec.0.List.mapA.match_1.eq_2|theorem|
+INV|Proofs.ApexSpec|_private.Proofs.ApexSpec.0.List.mapA.match_1.splitter|def|
+INV|Proofs.ApexSpec|fips205.allM_byteEq._proof_1_1|theorem|Quot.sound,propext
+INV|Proofs.ApexSpec|fips205.allM_byteEq|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.ApexSpec|fips205.arrayEqU8_spec|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.ApexSpec|fips205.byteEq|theorem|
+INV|Proofs.ApexSpec|fips205.htVerifyRoot._proof_1|theorem|propext
+INV|Proofs.ApexSpec|fips205.htVerifyRoot._proof_2|theorem|propext
+INV|Proofs.ApexSpec|fips205.htVerifyRoot|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l
+INV|Proofs.ApexSpec|fips205.ht_verify_free_split|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l
+INV|Proofs.ApexSpec|fips205.slhVerifyRoot._proof_1|theorem|propext
+INV|Proofs.ApexSpec|fips205.slhVerifyRoot._proof_2|theorem|propext
+INV|Proofs.ApexSpec|fips205.slhVerifyRoot._proof_3|theorem|propext
+INV|Proofs.ApexSpec|fips205.slhVerifyRoot._proof_4|theorem|propext
+INV|Proofs.ApexSpec|fips205.slhVerifyRoot._proof_5|theorem|propext
+INV|Proofs.ApexSpec|fips205.slhVerifyRoot._proof_6|theorem|propext
+INV|Proofs.ApexSpec|fips205.slhVerifyRoot|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.h_msg,verify_mono.oracle.t_l,verify_mono.oracle.t_len
+INV|Proofs.ApexSpec|fips205.slh_verify_128s_accepts_iff|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.h_msg,verify_mono.oracle.t_l,verify_mono.oracle.t_len
+INV|Proofs.ApexSpec|fips205.slh_verify_internal_accepts_iff|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.h_msg,verify_mono.oracle.t_l,verify_mono.oracle.t_len
+INV|Proofs.ChainSpec|Aeneas.Std.core.cmp.impls.PartialOrdU32.lt.eq_1|theorem|
+INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem|
+INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem|
+INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def|
+INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.fips205.chainFoldN.match_1.eq_1|theorem|
+INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.fips205.chainFoldN.match_1.eq_2|theorem|
+INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.fips205.chainFoldN.match_1.splitter|def|
+INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_1|theorem|
+INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_2|theorem|
+INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.fips205.helpers.to_byte_loop.body.match_1.splitter|def|
+INV|Proofs.ChainSpec|fips205.chainFoldN._f|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
+INV|Proofs.ChainSpec|fips205.chainFoldN._proof_1|theorem|propext
+INV|Proofs.ChainSpec|fips205.chainFoldN._sunfold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
+INV|Proofs.ChainSpec|fips205.chainFoldN.eq_def|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
+INV|Proofs.ChainSpec|fips205.chainFoldN.match_1|def|
+INV|Proofs.ChainSpec|fips205.chainFoldN|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
+INV|Proofs.ChainSpec|fips205.chain_free_loop_eq._proof_1_1|theorem|Quot.sound,propext
+INV|Proofs.ChainSpec|fips205.chain_free_loop_eq._proof_1_6|theorem|Quot.sound,propext
+INV|Proofs.ChainSpec|fips205.chain_free_loop_eq._proof_1_7|theorem|Quot.sound,propext
+INV|Proofs.ChainSpec|fips205.chain_free_loop_eq._proof_1_8|theorem|Quot.sound,propext
+INV|Proofs.ChainSpec|fips205.chain_free_loop_eq._proof_1_9|theorem|Quot.sound,propext
+INV|Proofs.ChainSpec|fips205.chain_free_loop_eq|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
+INV|Proofs.ChainSpec|fips205.chain_step|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
+INV|Proofs.ChainSpec|fips205.fwd_succ|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.ChainSpec|fips205.hbody|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
+INV|Proofs.ChainSpec|fips205.hnext|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.ChainSpec|fips205.loop_unfold_bind|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.ChainSpec|fips205.u32_succ._proof_1_1|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.ChainSpec|fips205.u32_succ._proof_1_2|theorem|Quot.sound,propext
+INV|Proofs.ChainSpec|fips205.u32_succ|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem|
+INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem|
+INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def|
+INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.fips205.forsInnerFold.match_1.eq_1|theorem|
+INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.fips205.forsInnerFold.match_1.eq_2|theorem|
+INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.fips205.forsInnerFold.match_1.splitter|def|
+INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_1|theorem|
+INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_2|theorem|
+INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.fips205.helpers.to_byte_loop.body.match_1.splitter|def|
+INV|Proofs.ForsInnerSpec|fips205.forsInnerFold._f|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
+INV|Proofs.ForsInnerSpec|fips205.forsInnerFold._proof_1|theorem|propext
+INV|Proofs.ForsInnerSpec|fips205.forsInnerFold._proof_2|theorem|propext
+INV|Proofs.ForsInnerSpec|fips205.forsInnerFold._proof_3|theorem|propext
+INV|Proofs.ForsInnerSpec|fips205.forsInnerFold._sunfold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
+INV|Proofs.ForsInnerSpec|fips205.forsInnerFold.eq_def|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
+INV|Proofs.ForsInnerSpec|fips205.forsInnerFold.match_1|def|
+INV|Proofs.ForsInnerSpec|fips205.forsInnerFold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
+INV|Proofs.ForsInnerSpec|fips205.fors_inner_loop_eq._proof_1_1|theorem|Quot.sound,propext
+INV|Proofs.ForsInnerSpec|fips205.fors_inner_loop_eq._proof_1_5|theorem|Quot.sound,propext
+INV|Proofs.ForsInnerSpec|fips205.fors_inner_loop_eq._proof_1_6|theorem|Quot.sound,propext
+INV|Proofs.ForsInnerSpec|fips205.fors_inner_loop_eq._proof_1_7|theorem|Quot.sound,propext
+INV|Proofs.ForsInnerSpec|fips205.fors_inner_loop_eq._proof_1_8|theorem|Quot.sound,propext
+INV|Proofs.ForsInnerSpec|fips205.fors_inner_loop_eq|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
+INV|Proofs.ForsInnerSpec|fips205.fors_inner_step|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
+INV|Proofs.ForsInnerSpec|fips205.hbody_fi|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
+INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem|
+INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem|
+INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def|
+INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.fips205.forsOuterFold.match_1.eq_1|theorem|
+INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.fips205.forsOuterFold.match_1.eq_2|theorem|
+INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.fips205.forsOuterFold.match_1.splitter|def|
+INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_1|theorem|
+INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_2|theorem|
+INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.fips205.helpers.to_byte_loop.body.match_1.splitter|def|
+INV|Proofs.ForsOuterSpec|fips205.forsOuterFold._f|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h
+INV|Proofs.ForsOuterSpec|fips205.forsOuterFold._proof_1|theorem|propext
+INV|Proofs.ForsOuterSpec|fips205.forsOuterFold._proof_2|theorem|propext
+INV|Proofs.ForsOuterSpec|fips205.forsOuterFold._sunfold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h
+INV|Proofs.ForsOuterSpec|fips205.forsOuterFold.eq_def|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h
+INV|Proofs.ForsOuterSpec|fips205.forsOuterFold.match_1|def|
+INV|Proofs.ForsOuterSpec|fips205.forsOuterFold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h
+INV|Proofs.ForsOuterSpec|fips205.fors_outer_loop_eq._proof_1_1|theorem|Quot.sound,propext
+INV|Proofs.ForsOuterSpec|fips205.fors_outer_loop_eq._proof_1_5|theorem|Quot.sound,propext
+INV|Proofs.ForsOuterSpec|fips205.fors_outer_loop_eq._proof_1_6|theorem|Quot.sound,propext
+INV|Proofs.ForsOuterSpec|fips205.fors_outer_loop_eq._proof_1_7|theorem|Quot.sound,propext
+INV|Proofs.ForsOuterSpec|fips205.fors_outer_loop_eq._proof_1_8|theorem|Quot.sound,propext
+INV|Proofs.ForsOuterSpec|fips205.fors_outer_loop_eq|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h
+INV|Proofs.ForsOuterSpec|fips205.fors_outer_step|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h
+INV|Proofs.ForsOuterSpec|fips205.hbody_fo|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h
+INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem|
+INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem|
+INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def|
+INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_1|theorem|
+INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_2|theorem|
+INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.fips205.helpers.to_byte_loop.body.match_1.splitter|def|
+INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.fips205.htFoldN.match_1.eq_1|theorem|
+INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.fips205.htFoldN.match_1.eq_2|theorem|
+INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.fips205.htFoldN.match_1.splitter|def|
+INV|Proofs.HtSpec|fips205.hbody_ht|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l
+INV|Proofs.HtSpec|fips205.htFoldN._f|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l
+INV|Proofs.HtSpec|fips205.htFoldN._proof_1|theorem|propext
+INV|Proofs.HtSpec|fips205.htFoldN._proof_2|theorem|propext
+INV|Proofs.HtSpec|fips205.htFoldN._sunfold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l
+INV|Proofs.HtSpec|fips205.htFoldN.eq_def|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l
+INV|Proofs.HtSpec|fips205.htFoldN.match_1|def|
+INV|Proofs.HtSpec|fips205.htFoldN|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l
+INV|Proofs.HtSpec|fips205.ht_loop_eq._proof_1_1|theorem|Quot.sound,propext
+INV|Proofs.HtSpec|fips205.ht_loop_eq._proof_1_5|theorem|Quot.sound,propext
+INV|Proofs.HtSpec|fips205.ht_loop_eq._proof_1_6|theorem|Quot.sound,propext
+INV|Proofs.HtSpec|fips205.ht_loop_eq._proof_1_7|theorem|Quot.sound,propext
+INV|Proofs.HtSpec|fips205.ht_loop_eq._proof_1_8|theorem|Quot.sound,propext
+INV|Proofs.HtSpec|fips205.ht_loop_eq|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l
+INV|Proofs.HtSpec|fips205.ht_loop_step|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l
+INV|Proofs.InputPrepSpec|Aeneas.Std.I32.ofInt.congr_simp|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem|
+INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem|
+INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def|
+INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.base2bOuterFold.match_1.eq_1|theorem|propext
+INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.base2bOuterFold.match_1.eq_2|theorem|propext
+INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.base2bOuterFold.match_1.splitter|def|propext
+INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_1|theorem|
+INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_2|theorem|
+INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.helpers.to_byte_loop.body.match_1.splitter|def|
+INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.helpers.to_int_loop.body.match_1.eq_1|theorem|
+INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.helpers.to_int_loop.body.match_1.eq_2|theorem|
+INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.helpers.to_int_loop.body.match_1.splitter|def|
+INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.toByteFold.match_1.eq_1|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.toByteFold.match_1.eq_2|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.toByteFold.match_1.splitter|def|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.toIntFold.match_1.eq_1|theorem|
+INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.toIntFold.match_1.eq_2|theorem|
+INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.toIntFold.match_1.splitter|def|
+INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.wotsCsumFold.match_1.eq_1|theorem|
+INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.wotsCsumFold.match_1.eq_2|theorem|
+INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.wotsCsumFold.match_1.splitter|def|
+INV|Proofs.InputPrepSpec|fips205.base2bOuterFold._f|def|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.base2bOuterFold._proof_1|theorem|propext
+INV|Proofs.InputPrepSpec|fips205.base2bOuterFold._sunfold|def|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.base2bOuterFold.eq_def|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.base2bOuterFold.match_1|def|propext
+INV|Proofs.InputPrepSpec|fips205.base2bOuterFold|def|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.base2b_outer_loop_eq._proof_1_1|theorem|Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.base2b_outer_loop_eq._proof_1_5|theorem|Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.base2b_outer_loop_eq._proof_1_6|theorem|Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.base2b_outer_loop_eq._proof_1_7|theorem|Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.base2b_outer_loop_eq._proof_1_8|theorem|Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.base2b_outer_loop_eq|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.base2b_outer_step|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.hbody_b2|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.hbody_cs|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.hbody_tb|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.hbody_ti|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.toByteFold._f|def|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.toByteFold._proof_1|theorem|propext
+INV|Proofs.InputPrepSpec|fips205.toByteFold._proof_2|theorem|propext
+INV|Proofs.InputPrepSpec|fips205.toByteFold._proof_3|theorem|propext
+INV|Proofs.InputPrepSpec|fips205.toByteFold._proof_4|theorem|propext
+INV|Proofs.InputPrepSpec|fips205.toByteFold._sunfold|def|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.toByteFold.eq_def|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.toByteFold.match_1|def|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.toByteFold|def|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.toIntFold._f|def|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.toIntFold._proof_1|theorem|propext
+INV|Proofs.InputPrepSpec|fips205.toIntFold._proof_2|theorem|propext
+INV|Proofs.InputPrepSpec|fips205.toIntFold._sunfold|def|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.toIntFold.eq_def|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.toIntFold.match_1|def|
+INV|Proofs.InputPrepSpec|fips205.toIntFold|def|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.to_byte_loop_eq._proof_1_1|theorem|Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.to_byte_loop_eq._proof_1_5|theorem|Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.to_byte_loop_eq._proof_1_6|theorem|Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.to_byte_loop_eq._proof_1_7|theorem|Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.to_byte_loop_eq._proof_1_8|theorem|Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.to_byte_loop_eq|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.to_byte_step|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.to_int_loop_eq._proof_1_1|theorem|Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.to_int_loop_eq._proof_1_5|theorem|Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.to_int_loop_eq._proof_1_6|theorem|Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.to_int_loop_eq._proof_1_7|theorem|Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.to_int_loop_eq._proof_1_8|theorem|Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.to_int_loop_eq|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.to_int_step|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.wotsCsumFold._f|def|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.wotsCsumFold._sunfold|def|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.wotsCsumFold.eq_def|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.wotsCsumFold.match_1|def|
+INV|Proofs.InputPrepSpec|fips205.wotsCsumFold|def|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.wots_csum_loop_eq._proof_1_1|theorem|Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.wots_csum_loop_eq._proof_1_5|theorem|Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.wots_csum_loop_eq._proof_1_6|theorem|Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.wots_csum_loop_eq._proof_1_7|theorem|Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.wots_csum_loop_eq._proof_1_8|theorem|Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.wots_csum_loop_eq|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.InputPrepSpec|fips205.wots_csum_step|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.WotsSpec|Aeneas.Std.core.cmp.impls.PartialOrdUsize.lt.eq_1|theorem|
+INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem|
+INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem|
+INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def|
+INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.fips205.helpers.to_int_loop.body.match_1.eq_1|theorem|
+INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.fips205.helpers.to_int_loop.body.match_1.eq_2|theorem|
+INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.fips205.helpers.to_int_loop.body.match_1.splitter|def|
+INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.fips205.wotsChainFold.match_1.eq_1|theorem|
+INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.fips205.wotsChainFold.match_1.eq_2|theorem|
+INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.fips205.wotsChainFold.match_1.splitter|def|
+INV|Proofs.WotsSpec|fips205.fwd_succ_usize|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.WotsSpec|fips205.hbody1|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
+INV|Proofs.WotsSpec|fips205.hnext_usize|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.WotsSpec|fips205.usize_succ._proof_1_1|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.WotsSpec|fips205.usize_succ._proof_1_2|theorem|Quot.sound,propext
+INV|Proofs.WotsSpec|fips205.usize_succ|theorem|Classical.choice,Quot.sound,propext
+INV|Proofs.WotsSpec|fips205.wotsChainFold._f|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
+INV|Proofs.WotsSpec|fips205.wotsChainFold._proof_1|theorem|propext
+INV|Proofs.WotsSpec|fips205.wotsChainFold._proof_2|theorem|propext
+INV|Proofs.WotsSpec|fips205.wotsChainFold._sunfold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
+INV|Proofs.WotsSpec|fips205.wotsChainFold.eq_def|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
+INV|Proofs.WotsSpec|fips205.wotsChainFold.match_1|def|
+INV|Proofs.WotsSpec|fips205.wotsChainFold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
+INV|Proofs.WotsSpec|fips205.wots_loop1_eq._proof_1_1|theorem|Quot.sound,propext
+INV|Proofs.WotsSpec|fips205.wots_loop1_eq._proof_1_6|theorem|Quot.sound,propext
+INV|Proofs.WotsSpec|fips205.wots_loop1_eq._proof_1_7|theorem|Quot.sound,propext
+INV|Proofs.WotsSpec|fips205.wots_loop1_eq._proof_1_8|theorem|Quot.sound,propext
+INV|Proofs.WotsSpec|fips205.wots_loop1_eq._proof_1_9|theorem|Quot.sound,propext
+INV|Proofs.WotsSpec|fips205.wots_loop1_eq|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
+INV|Proofs.WotsSpec|fips205.wots_loop1_step|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
+INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem|
+INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem|
+INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def|
+INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_1|theorem|
+INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_2|theorem|
+INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.fips205.helpers.to_byte_loop.body.match_1.splitter|def|
+INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.fips205.xmssFoldN.match_1.eq_1|theorem|
+INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.fips205.xmssFoldN.match_1.eq_2|theorem|
+INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.fips205.xmssFoldN.match_1.splitter|def|
+INV|Proofs.XmssSpec|fips205.hbody_x|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
+INV|Proofs.XmssSpec|fips205.xmssFoldN._f|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
+INV|Proofs.XmssSpec|fips205.xmssFoldN._proof_1|theorem|propext
+INV|Proofs.XmssSpec|fips205.xmssFoldN._proof_2|theorem|propext
+INV|Proofs.XmssSpec|fips205.xmssFoldN._proof_3|theorem|propext
+INV|Proofs.XmssSpec|fips205.xmssFoldN._sunfold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
+INV|Proofs.XmssSpec|fips205.xmssFoldN.eq_def|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
+INV|Proofs.XmssSpec|fips205.xmssFoldN.match_1|def|
+INV|Proofs.XmssSpec|fips205.xmssFoldN|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
+INV|Proofs.XmssSpec|fips205.xmss_loop_eq._proof_1_1|theorem|Quot.sound,propext
+INV|Proofs.XmssSpec|fips205.xmss_loop_eq._proof_1_5|theorem|Quot.sound,propext
+INV|Proofs.XmssSpec|fips205.xmss_loop_eq._proof_1_6|theorem|Quot.sound,propext
+INV|Proofs.XmssSpec|fips205.xmss_loop_eq._proof_1_7|theorem|Quot.sound,propext
+INV|Proofs.XmssSpec|fips205.xmss_loop_eq._proof_1_8|theorem|Quot.sound,propext
+INV|Proofs.XmssSpec|fips205.xmss_loop_eq|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
+INV|Proofs.XmssSpec|fips205.xmss_loop_step|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
diff --git a/verification/inventory_gate.sh b/verification/inventory_gate.sh
new file mode 100755
index 0000000..b0de821
--- /dev/null
+++ b/verification/inventory_gate.sh
@@ -0,0 +1,116 @@
+#!/usr/bin/env bash
+# ─────────────────────────────────────────────────────────────────────────────
+# inventory_gate.sh — diff an observed environment inventory against the
+# pinned allowlist. PORTED VERBATIM from ltl-accumulator-verified apart from
+# the axiom-surface assertion, which is repo-specific: there the corpus admits
+# exactly one sanctioned axiom, here it admits none.
+#
+# This is THE production coverage gate: check.sh Phase 2c calls it, and the
+# self-test exercises this exact script — the tested logic IS the shipping
+# logic.
+#
+# Usage: inventory_gate.sh <observed-lean-output> <allowlist-file> [<tag>]
+#
+# <tag> defaults to INV — the CORPUS walk. Pass DRV to gate the INSTRUMENTS'
+# OWN SURFACE with this same implementation.
+#
+# WHY THE TAG EXISTS — round-8 review (Claude, register keys
+# `drv-surface-no-cones`, `accounting-certifies-enumeration`).
+#
+# The accounting identity added in round 7 proved every constant the kernel
+# sees is ENUMERATED by one of the two walks. The reviewer showed that
+# enumeration is not audit: a claim planted in an instrument WAS enumerated —
+# `DRV|LTLAccAudit.bait.smuggled|theorem` — and then nothing looked at it,
+# because DRV rows carried name and kind and NO CONE, and no allowlist covered
+# them. In their words, the identity "converted 36 declarations nobody
+# enumerated into 36 declarations nobody examined. That is progress of one
+# step, not two."
+#
+# The second step is here: DRV rows now carry their axiom cone and are pinned
+# in a committed allowlist, by THIS gate, in both directions — exactly as the
+# corpus is. One implementation, not two, because a second copy of a coverage
+# gate is a second thing to drift.
+#
+# It also retires a heuristic. The driver-surface rule permits a theorem whose
+# name extends a constant declared alongside it, since that is what the
+# elaborator generates for a definition; the reviewer showed it "breaks in one
+# line" — declare `def bait`, then `theorem bait.smuggled` passes. That rule is
+# kept as a fast, readable first line of defence, but it is NO LONGER
+# LOAD-BEARING: a planted claim now has to appear in the pinned allowlist, and
+# a new row fails closed whatever it is named.
+#
+# Fail-closed in BOTH directions:
+#   UNCLASSIFIED — constant in the environment, absent from the allowlist
+#                  (new/renamed decl, changed kind, or changed axiom cone)
+#   STALE        — allowlist entry absent from the environment
+# plus an output-integrity check: the INV-COUNT trailer emitted by
+# Proofs/Inventory.lean must equal the number of INV lines actually seen,
+# so a truncated or crashed run can never pass as an empty diff.
+# ─────────────────────────────────────────────────────────────────────────────
+set -uo pipefail
+export LC_ALL=C   # byte-order collation: sort/comm must agree with Lean's String order
+obs_file="$1"; allow_file="$2"; TAG="${3:-INV}"
+case "$TAG" in
+  INV) WHAT="the audited corpus"; TRAILER_TAG="INV-COUNT"; LABEL="inventory gate"; TRUNCLABEL="INVENTORY TRUNCATED" ;;
+  DRV) WHAT="the audit instruments"; TRAILER_TAG="DRV-COUNT"; LABEL="driver-surface gate"; TRUNCLABEL="DRIVER SURFACE TRUNCATED" ;;
+  *)   echo "  GATE MISUSE: unknown tag '$TAG' (expected INV or DRV)"; exit 1 ;;
+esac
+
+# The trailer is an OUTPUT-INTEGRITY check: it must equal the number of rows
+# the driver(s) actually emitted, BEFORE de-duplication. Comparing it to the
+# de-duplicated count conflates "a run was truncated" with "two rows were
+# identical", and the second is a record-format defect that must be fixed at
+# the source, not absorbed here. (It was: DRV rows now carry their driver.)
+N_RAW=$(grep -c "^$TAG|" "$obs_file" || true)
+OBS=$(grep "^$TAG|" "$obs_file" | sort -u)
+N_OBS=$(printf '%s' "$OBS" | grep -c "^$TAG|" || true)
+if [ "$N_RAW" -ne "$N_OBS" ]; then
+  echo "  DUPLICATE $TAG RECORDS: $N_RAW rows collapse to $N_OBS distinct ones."
+  echo "  Two declarations share a record, so one is covered by the other's entry:"
+  grep "^$TAG|" "$obs_file" | sort | uniq -d | head -5 | sed 's/^/    /'
+  exit 1
+fi
+# Each driver emits its own trailer, so DRV trailers are SUMMED; the corpus
+# walk emits one and the last is taken. Either way a truncated or crashed run
+# must never pass as an empty diff.
+if [ "$TAG" = DRV ]; then
+  TRAILER=$(grep "^$TRAILER_TAG|" "$obs_file" | cut -d'|' -f2 | paste -sd+ - | bc)
+else
+  TRAILER=$(grep "^$TRAILER_TAG|" "$obs_file" | tail -1 | cut -d'|' -f2)
+fi
+if [ -z "$TRAILER" ] || [ "$TRAILER" != "$N_RAW" ]; then
+  echo "  $TRUNCLABEL: trailer=${TRAILER:-absent}, observed $N_RAW lines"
+  exit 1
+fi
+
+ALLOW=$(grep "^$TAG|" "$allow_file" | sort -u)
+FAILGATE=0
+UNCLASS=$(comm -23 <(printf '%s\n' "$OBS") <(printf '%s\n' "$ALLOW"))
+STALE=$(comm -13 <(printf '%s\n' "$OBS") <(printf '%s\n' "$ALLOW"))
+if [ -n "$UNCLASS" ]; then
+  printf '%s\n' "$UNCLASS" | sed 's/^/  UNCLASSIFIED (in environment, not allowlisted): /'
+  FAILGATE=1
+fi
+if [ -n "$STALE" ]; then
+  printf '%s\n' "$STALE" | sed 's/^/  STALE (allowlisted, not in environment): /'
+  FAILGATE=1
+fi
+
+# The audited corpus admits NO axiom declarations at all: the sanctioned
+# external models live in gen/, outside every module these drivers cover, and
+# are byte-pinned by Phase 0b. An axiom appearing here would be a declaration
+# smuggled into the proof corpus, which Phase 2b also catches kernel-side —
+# two independent gates on the same property, deliberately.
+AXLINES=$(printf '%s\n' "$OBS" | grep '|axiom|' || true)
+if [ -n "$AXLINES" ]; then
+  echo "  AXIOM SURFACE DRIFT: $WHAT must declare no axioms; observed:"
+  printf '%s\n' "$AXLINES" | sed 's/^/    /'
+  FAILGATE=1
+fi
+
+# The message must describe what was actually checked. It said "single
+# sanctioned axiom" when ported, which is the accumulator's policy; here the
+# audited corpus permits NONE, and a success line describing a different rule
+# is how an assertion quietly stops meaning anything.
+[ "$FAILGATE" = 0 ] && echo "  $LABEL: $N_OBS constants, environment == allowlist, zero axioms declared in $WHAT"
+exit "$FAILGATE"