chore(abi): remove the idrisiser tree (owner decision; it never typechecked)

.machine_readable/bot_directives/gitbot-fleet.a2ml

@@ -22,12 +22,11 @@ ci-green-before-merge = true
 never-touch = [
   ".claude/CLAUDE.md",
   "src/abi/",
-  "generated/idrisiser/",
   ".machine_readable/threat-model.a2ml",
   ".machine_readable/contractiles/Trustfile.a2ml",
   "LICENSE",
 ]
-never-touch-notes = "src/abi/ (one tree: src/abi/januskey-abi.ipkg + JanusKey/ABI/*.idr, invariants in scripts/check-abi-tree.sh) + generated/idrisiser/ are the Idris2 ABI proof surface (changes require proof re-verification); threat-model.a2ml awaits human sign-off; the Trustfile may never be widened by an agent (see its self-integrity rule)."
+never-touch-notes = "src/abi/ (one tree: src/abi/januskey-abi.ipkg + JanusKey/ABI/*.idr, invariants in scripts/check-abi-tree.sh) is the Idris2 ABI proof surface (changes require proof re-verification); threat-model.a2ml awaits human sign-off; the Trustfile may never be widened by an agent (see its self-integrity rule)."
 
 [per-bot.sustainabot]
 allow = ["Cargo.toml", "Cargo.lock", ".github/workflows (SHA bumps via grouped dependabot PRs only)"]

.machine_readable/contractiles/Mustfile.a2ml

@@ -108,7 +108,7 @@ trust level: even maximal-trust agents cannot violate MUST constraints.
 
 ### no-dangerous-proof-escapes
 - description: No believe_me / assert_total in Idris2 proof code
-- run: "! grep -rnE 'believe_me|assert_total' src/abi/ generated/idrisiser/ 2>/dev/null | head -1 | grep -q ."
+- run: "! grep -rnE 'believe_me|assert_total' src/abi/ 2>/dev/null | head -1 | grep -q ."
 - severity: critical
 
 ### no-unsafe-without-comment
@@ -150,11 +150,6 @@ trust level: even maximal-trust agents cannot violate MUST constraints.
 - run: test -f src/abi/JanusKey/ABI/Types.idr && test -f src/abi/JanusKey/ABI/Proofs.idr && test -f src/abi/JanusKey/ABI/Foreign.idr && test -f src/abi/januskey-abi.ipkg
 - severity: critical
 
-### generated-code-in-generated
-- description: Generated code lives in generated/ only
-- run: test -d generated
-- severity: warning
-
 ### tests-not-deleted
 - description: Test directories must not be deleted or emptied
 - run: test -d tests && test -d crates/januskey-cli/tests

PROOF-NEEDS.adoc

@@ -31,9 +31,9 @@ commits, not this one:
   `+Handle Locked+`, linear variables used twice or not at all, and
   `+oblitMostExpensive (S k) = Oh+` on an open `+k+`).
 
-`+generated/idrisiser/+` is unchanged and outside the gate; whether it is
-regenerated with capitalised module names or removed is an owner decision
-(JNK-01, open question).
+`+generated/idrisiser/+` was left outside the gate here; the owner decided
+(2026-10-14) to remove it, with its `+idrisiser/*.tsig+` inputs and
+`+idrisiser.toml+`. `+scripts/check-abi-tree.sh+` now fails if any of them returns.
 
 ==== Same day, three commits later: the package typechecks
 
@@ -103,11 +103,9 @@ single tree; ABI bullet re-verified 2026-10-13._
 and `+dashboard-check+`). The tautological placeholders are gone (list
 above). What it proves are ABI and model lemmas (ledger rows A-*, C-*),
 NOT the security proofs listed below.
-* **generated/idrisiser/idris2/Januskey/Verified/*.idr**: **DO NOT
-typecheck** — `+idris2 --check+` fails ("`Expected a capitalised
-identifier, got: key`") because the generated module names are
-lowercase. Despite the `+Verified/+` name, nothing there is currently
-verified.
+* **generated/idrisiser/**: removed 2026-10-14 (owner decision). It never
+typechecked (lowercase generated module names), so nothing in it was
+verified; no ledger row depended on it.
 * *Dangerous patterns*: *265* `+unwrap()+` calls across the Rust
 codebase.
 * *LOC*: ~12,200 (Rust)

README.adoc

@@ -142,7 +142,7 @@ Reversibility is the default. Secure obliteration (`jk shred`) is the deliberate
 
 [CAUTION]
 ====
-**Formal proofs are pending.** The claim "data loss is architecturally impossible" is an engineering intent supported by the inversion-metadata mechanism. It is not yet a mechanically verified theorem. The `src/abi/` package typechecks (gate: `just test-proofs`) and discharges the ABI obligations listed in PROOF-NEEDS.adoc; it does not discharge "data loss is architecturally impossible", and `generated/idrisiser/` is outside the gate.
+**Formal proofs are pending.** The claim "data loss is architecturally impossible" is an engineering intent supported by the inversion-metadata mechanism. It is not yet a mechanically verified theorem. The `src/abi/` package typechecks (gate: `just test-proofs`) and discharges the ABI obligations listed in PROOF-NEEDS.adoc; it does not discharge "data loss is architecturally impossible". (The former `generated/idrisiser/` tree, which never typechecked, was removed.)
 ====
 
 [CAUTION]