fix(abi): close last Tier2 assert_total via fuel recursion + FP classifications

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"))
+)

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