From b6332b89134523cd7543cd8a4769db7eb8b41845 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Thu, 11 Jun 2026 22:25:37 +0000
Subject: [PATCH] fix(abi): close last Tier2 assert_total via fuel recursion +
 FP classifications

bufferToList now recurses structurally on a remaining-byte Nat fuel
instead of asserting totality on an increasing Int index. Semantics
unchanged (n <= 0 yields [], bytes read [0, n) in order); the totality
checker accepts it directly, restoring the proof-corpus zero
proof-escape contract that #52's merge gate promised.

audits/assail-classifications.a2ml records the audited FFI residuals
from a fresh panic-attack 2.5.5 scan: the documented unsafe blocks in
recompute-wasm and attest (both files carry in-file UNSAFE POLICY
sections and deny(clippy::undocumented_unsafe_blocks)) and the Zig
C-ABI bridge cast. The assert_total finding is fixed, not classified.

vcl-ut also gains scan coverage for the first time: it had NO entry in
verisimdb-data/scans at all (coverage gap fixed estate-wide by
hypatia's new estate-rescan workflow).
---
 audits/assail-classifications.a2ml | 35 ++++++++++++++++++++++++++++++
 src/interface/abi/Tier2.idr        | 19 +++++++++-------
 2 files changed, 46 insertions(+), 8 deletions(-)
 create mode 100644 audits/assail-classifications.a2ml

diff --git a/audits/assail-classifications.a2ml b/audits/assail-classifications.a2ml
new file mode 100644
index 0000000..3eab8d6
--- /dev/null
+++ b/audits/assail-classifications.a2ml
@@ -0,0 +1,35 @@
+;; SPDX-License-Identifier: MPL-2.0
+;; assail-classifications.a2ml — audited panic-attack findings for vcl-ut.
+;;
+;; Read by panic-attack >= 2.5.5 (load_user_classifications): findings
+;; matching (file, category) flip to suppressed = true after the kanren
+;; structural pass. Entries are AUDITED-SOUND residuals with rationale;
+;; the registry lives apart from the source so a code edit cannot
+;; self-suppress (panic-attack CLAUDE.md, User-Classification Registry).
+;;
+;; Audit trail: 2026-06-11 estate-loop session — fresh panic-attack
+;; 2.5.5 scan; every entry inspected at source. The Tier2.idr
+;; assert_total finding from the same scan was FIXED at source (fuel
+;; recursion), not classified — classification is only for sound
+;; residuals that cannot reasonably be removed.
+
+(assail-classifications
+  ;; ── FFI boundary unsafe: required by the C ABI, reviewed ─────────
+  ;; Mirrors the reference pattern in hyperpolymath/007
+  ;; audits/assail-classifications.a2ml (zig_bridge.rs UnsafeCode).
+  (classification
+    (file "src/interface/recompute-wasm/src/lib.rs")
+    (category "UnsafeCode")
+    (audit "in-file UNSAFE POLICY (lib.rs:40-46) + deny(clippy::undocumented_unsafe_blocks)")
+    (rationale "only unsafe is the documented host/guest memory-ABI block (alloc/dealloc pair); all decision logic lives in the forbid(unsafe_code) vcltotal-parse crate"))
+  (classification
+    (file "src/interface/attest/src/lib.rs")
+    (category "UnsafeCode")
+    (audit "in-file UNSAFE POLICY (lib.rs:38-42) + deny(clippy::undocumented_unsafe_blocks)")
+    (rationale "single documented C-ABI block in vclut_rs_verify with null/len checks and fail-closed -1 returns; decode logic in forbid(unsafe_code) crate"))
+  (classification
+    (file "ffi/zig/src/lib.zig")
+    (category "UnsafeCode")
+    (audit "Zig C-ABI bridge — single pointer cast at the exported boundary")
+    (rationale "the cast is the FFI contract itself; callee validates length before use"))
+)
diff --git a/src/interface/abi/Tier2.idr b/src/interface/abi/Tier2.idr
index 70c0d15..5b89454 100644
--- a/src/interface/abi/Tier2.idr
+++ b/src/interface/abi/Tier2.idr
@@ -139,15 +139,18 @@ listToBuffer xs = do
 ||| a `List Bits8`. Reads bytes `[0, n)` in order.
 private
 bufferToList : Buffer -> Int -> IO (List Bits8)
-bufferToList buf n = go 0 []
+bufferToList buf n = go (integerToNat (cast n)) 0 []
   where
-    go : Int -> List Bits8 -> IO (List Bits8)
-    go i acc =
-      if i >= n
-        then pure (reverse acc)
-        else do
-          b <- getBits8 buf i
-          assert_total (go (i + 1) (b :: acc))
+    -- Structural recursion on the remaining-byte fuel: the totality
+    -- checker accepts this directly, closing the last assert_total in
+    -- the Tier-2 ABI (proof-corpus gate: zero proof-escape). For n <= 0
+    -- the fuel is Z and we return [] — same semantics as the previous
+    -- `i >= n` guard.
+    go : Nat -> Int -> List Bits8 -> IO (List Bits8)
+    go Z     _ acc = pure (reverse acc)
+    go (S k) i acc = do
+      b <- getBits8 buf i
+      go k (i + 1) (b :: acc)
 
 -- ═══════════════════════════════════════════════════════════════════════
 -- Safe public wrapper