feat(cuda): bound the device block reuse cache with an env byte cap

NN/Runtime/Autograd/Engine/Cuda/Buffer.lean

@@ -87,13 +87,20 @@ opaque allocatorDeviceFreeBytesRaw (u : UInt32) : UInt64
 @[extern "torchlean_cuda_allocator_device_total_bytes"]
 opaque allocatorDeviceTotalBytesRaw (u : UInt32) : UInt64
 
+@[extern "torchlean_cuda_allocator_cache_bytes"]
+opaque allocatorCacheBytesRaw (u : UInt32) : UInt64
+
 /--
 Snapshot of the CUDA buffer allocator.
 
 `liveBytes`/`peakBytes` count TorchLean buffers created by this runtime layer. `deviceFreeBytes`
 and `deviceTotalBytes` come from `cudaMemGetInfo` in the CUDA build and are `0` in the CPU stub.
 Together they let long-running examples distinguish a TorchLean lifetime leak from broader CUDA
 memory pressure or fragmentation.
+
+`cacheBytes` is the device memory held in the buffer reuse cache — dropped buffers awaiting reuse,
+which are *not* counted in `liveBytes`. `TORCHLEAN_CUDA_CACHE_CAP_BYTES` bounds it; it is always `0`
+in the CPU stub, which keeps no cache.
 -/
 structure AllocatorStats where
   liveBytes : UInt64
@@ -102,6 +109,7 @@ structure AllocatorStats where
   freeCount : UInt64
   deviceFreeBytes : UInt64
   deviceTotalBytes : UInt64
+  cacheBytes : UInt64
 deriving Repr
 
 /--
@@ -118,7 +126,8 @@ def allocatorStatsWithToken (token : UInt32) : IO AllocatorStats := do
       allocCount := allocatorAllocCountRaw token
       freeCount := allocatorFreeCountRaw token
       deviceFreeBytes := allocatorDeviceFreeBytesRaw token
-      deviceTotalBytes := allocatorDeviceTotalBytesRaw token }
+      deviceTotalBytes := allocatorDeviceTotalBytesRaw token
+      cacheBytes := allocatorCacheBytesRaw token }
 
 /-- Read the current CUDA allocator counters. Prefer `allocatorStatsWithToken` in repeated loops. -/
 def allocatorStats : IO AllocatorStats :=
@@ -136,7 +145,8 @@ def AllocatorStats.format (s : AllocatorStats) : String :=
   " allocs=" ++ toString s.allocCount ++
   " frees=" ++ toString s.freeCount ++
   " cuda_free=" ++ mibString s.deviceFreeBytes ++
-  " cuda_total=" ++ mibString s.deviceTotalBytes
+  " cuda_total=" ++ mibString s.deviceTotalBytes ++
+  " cache=" ++ mibString s.cacheBytes
 
 /--
 Create a device buffer by copying from a host `FloatArray` (casts each element to float32).
@@ -239,6 +249,49 @@ opaque collectAllocatorRaw (force : UInt32) : UInt32
 def collectAllocator (force : Bool := true) : UInt32 :=
   collectAllocatorRaw (if force then 1 else 0)
 
+/-!
+### Scoped device-memory arena (`withCudaArena`)
+
+A long *pure* eager loop — a `foldl` of `Buffer → Buffer` ops with no IO sequencing — keeps every
+intermediate `Buffer` GC-*reachable* until the final readback, so the finalizers that would free the
+device memory never run and the working set grows with the loop length. Explicit `release` cannot
+reach those buffers: a pure carrier has no IO point at which to call it.
+
+A scoped arena fixes this. `arenaEnter` opens an allocation epoch; every device buffer allocated while
+it is open is tracked. `arenaExit keep` frees the device data of *all* of them — reachable or not —
+except the `keep` results, which survive: promoted to an enclosing arena if there is one, or left to
+ordinary reference-counted finalization at the outermost level. This matches a training loop's natural
+phase boundary (one LM step / one fold).
+
+**Contract.** Every buffer that must outlive the scope MUST appear in `keep` (or be reachable only
+through a kept buffer). Touching any other in-scope buffer after `arenaExit` is a use-after-free, the
+same hazard as reading a buffer after `release`.
+-/
+
+@[extern "torchlean_cuda_arena_enter"]
+opaque arenaEnter : IO Unit
+
+@[extern "torchlean_cuda_arena_exit"]
+opaque arenaExit (keep : @& Array Buffer) : IO Unit
+
+/--
+Run `body` inside a fresh device-memory arena, then reclaim every buffer it allocated except those
+named by `keep result`.
+
+`keep` extracts the buffers that must survive the scope (typically the step's result parameters). If
+`body` raises, the arena is still closed and every in-scope buffer is reclaimed before the exception
+propagates.
+-/
+def withCudaArena {α : Type} (keep : α → Array Buffer) (body : IO α) : IO α := do
+  arenaEnter
+  try
+    let r ← body
+    arenaExit (keep r)
+    return r
+  catch e =>
+    arenaExit #[]
+    throw e
+
 /-- Allocate a length-`n` buffer filled with zeros. -/
 @[extern "torchlean_cuda_buffer_zeros"]
 opaque zeros (n : UInt32) : Buffer