feat(libtorch): report device identity per index

NN/Kernel/Runtime.lean

@@ -18,8 +18,9 @@ bounded number of modules per process, keys them by source and context, and laun
 current stream. Input buffers and the module remain alive until the bounds record is checked.
 
 This is an explicit foreign-code boundary, not a Lean theorem about NVRTC or device execution.
-LibTorch continues to own tensor storage and its established numerical operations. CPU-only
-builds resolve the same extern symbols but report an ordinary IO error instead of executing CUDA.
+LibTorch continues to own tensor storage and its established numerical operations. Builds without
+LibTorch resolve the same extern symbols but report an ordinary IO error instead of executing CUDA,
+and so does the bridge on the host (a CPU-only SDK, or `TORCHLEAN_LIBTORCH_DEVICE=cpu`).
 -/
 
 @[expose] public section

NN/Runtime/Autograd/Engine/LibTorch.lean

@@ -14,6 +14,7 @@ public import NN.Runtime.Autograd.Engine.LibTorch.Float32Contract
 public import NN.Runtime.Autograd.Engine.LibTorch.KernelSpec
 public import NN.Runtime.Autograd.Engine.LibTorch.Kernels
 public import NN.Runtime.Autograd.Engine.LibTorch.Controls
+public import NN.Runtime.Autograd.Engine.LibTorch.DeviceInfo
 public import NN.Runtime.Autograd.Engine.LibTorch.Ops
 public import NN.Runtime.Autograd.Engine.LibTorch.Shape
 public import NN.Runtime.Autograd.Engine.LibTorch.Tape

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

@@ -11,10 +11,11 @@ public import NN.Runtime.Autograd.Engine.LibTorch.Trusted
 public import NN.Kernel.Cuda.Binary
 
 /-!
-# CUDA Buffers
+# LibTorch Buffers
 
-Low-level dtype-preserving operations for the LibTorch CUDA runtime. TorchLean retains its tape and
-selected local VJPs; native calls do not record a LibTorch autograd graph. CUDA builds use
+Low-level dtype-preserving operations for the LibTorch runtime, on a CUDA device or on the host
+(`Runtime.Autograd.LibTorch.deviceKind`). TorchLean retains its tape and selected local VJPs;
+native calls do not record a LibTorch autograd graph. `-K cuda=true` builds use
 `csrc/libtorch/torchlean.cpp`. Builds without LibTorch link `csrc/libtorch/unavailable.c`, which
 reports `.notLinked` and fails every buffer operation.
 -/
@@ -54,38 +55,58 @@ private opaque fail (message : @& String) : Buffer
 
 /-! ### Runtime Availability -/
 
-/-- What implementation sits behind the CUDA FFI symbols in the current process. -/
+/-- What implementation sits behind the buffer FFI symbols in the current process. -/
 inductive RuntimeStatus where
   /-- The default build does not link LibTorch; buffer operations fail. -/
   | notLinked
-  /-- The project was built with LibTorch CUDA and at least one CUDA device is visible. -/
+  /-- The project was built with LibTorch and the bridge selected a device: a CUDA device, or the
+  host (`Runtime.Autograd.LibTorch.deviceKind`). -/
   | nativeAvailable
-  /-- The project was built with LibTorch CUDA, but no usable CUDA device is visible. -/
+  /-- The project was built with LibTorch, but no usable device is selected: a CUDA-enabled SDK
+  with no visible CUDA device, unless `TORCHLEAN_LIBTORCH_DEVICE=cpu` selects the host. -/
   | nativeUnavailable
   deriving DecidableEq, Repr
 
 /-- Raw status word from the C layer; `runtimeStatus` decodes it. -/
 @[never_extract, extern "torchlean_cuda_runtime_status"]
 private opaque runtimeStatusRaw (token : UInt32) : UInt32
 
-/-- Query whether LibTorch is linked and can see a CUDA device. -/
+/-- Query whether LibTorch is linked and has a device to run on. -/
 @[no_expose] def runtimeStatus (token : UInt32 := 0) : RuntimeStatus :=
   match runtimeStatusRaw token with
   | 0 => .notLinked
   | 1 => .nativeAvailable
   | _ => .nativeUnavailable
 
-/-- Require real CUDA execution for a user-selected CUDA session. -/
+/--
+Require the LibTorch bridge with a device selected: a CUDA device, or the host. This is the check
+for a session that needs the bridge whatever its device (the CLI's `cuda` device, a CPU-only SDK
+in CI, `TORCHLEAN_REQUIRE_NATIVE=1` for the test suite); `requireCudaDevice` is the check for a
+session that needs a CUDA device.
+-/
 def requireNativeRuntime : IO Unit :=
   match runtimeStatus with
   | .nativeAvailable => pure ()
   | .notLinked =>
       throw <| IO.userError
-        "CUDA was requested, but this executable was built without LibTorch; \
+        "the LibTorch bridge was requested, but this executable was built without LibTorch; \
           rebuild and run with `-K cuda=true`"
   | .nativeUnavailable =>
       throw <| IO.userError
-        "CUDA was requested and this is a CUDA build, but no usable CUDA device is visible"
+        "the LibTorch bridge was requested and this is a LibTorch build, but no usable CUDA \
+          device is visible; TORCHLEAN_LIBTORCH_DEVICE=cpu selects the host instead"
+
+/--
+Require the LibTorch bridge on a CUDA device. `requireNativeRuntime` is satisfied by the host, so a
+check that means "a GPU ran this" has to ask for the device kind as well: this is what
+`TORCHLEAN_REQUIRE_CUDA=1` means to the test suite.
+-/
+def requireCudaDevice : IO Unit := do
+  requireNativeRuntime
+  if (← deviceKind) == .host then
+    throw <| IO.userError
+      "a CUDA device was required, but the LibTorch bridge runs on the host: the SDK is CPU-only, \
+        or TORCHLEAN_LIBTORCH_DEVICE=cpu selected the host"
 
 /-! ### Allocator Telemetry -/
 

NN/Runtime/Autograd/Engine/LibTorch/Controls.lean

@@ -7,13 +7,19 @@ Authors: TorchLean Team
 module
 
 /-!
-# LibTorch CUDA Runtime Controls
+# LibTorch Runtime Controls
 
 Effectful configuration and readback for TorchLean's LibTorch bridge. Configure these process-wide
 settings before concurrent runtime work. They are runtime requests, not numerical proof evidence:
 IEEE precision and strict determinism do not establish a reference reduction order, correct
 rounding of every operation, or FloatLib bit agreement.
 
+The bridge selects its device once, at its first call: a visible CUDA device when the SDK was
+built with CUDA support, or the host when the SDK is CPU-only. `TORCHLEAN_LIBTORCH_DEVICE=cpu`
+selects the host on any SDK and `TORCHLEAN_LIBTORCH_DEVICE=cuda` insists on a CUDA device; a CUDA
+SDK without a visible device never falls back to the host silently. `deviceKind` reports the
+choice; the CUDA-only controls below say what they do on the host.
+
 TorchLean owns its tape and selected local VJPs. These controls never enable LibTorch autograd.
 Native tensors retain their supported hardware dtypes; this API does not select arbitrary FloatLib
 formats. `version` reports the linked native build rather than a version assumed by Lean.
@@ -41,6 +47,9 @@ private opaque deviceCountRaw (token : UInt32) : UInt32
 @[never_extract, extern "torchlean_libtorch_get_device"]
 private opaque getDeviceRaw (token : UInt32) : UInt32
 
+@[never_extract, extern "torchlean_libtorch_device_kind"]
+private opaque deviceKindRaw (token : UInt32) : UInt32
+
 @[never_extract, extern "torchlean_libtorch_set_device"]
 private opaque setDeviceRaw (device : UInt32) : IO Unit
 
@@ -80,16 +89,30 @@ private opaque emptyCacheRaw (token : UInt32) : IO Unit
 @[no_expose] def version : IO String :=
   IO.lazyPure fun _ => versionRaw 0
 
-/-- Number of CUDA devices visible to the linked runtime; zero without LibTorch. -/
+/-- Number of CUDA devices visible to the linked runtime; zero without LibTorch and zero on a
+CPU-only SDK. A visible device is not necessarily the selected one: see `deviceKind`. -/
 @[no_expose] def deviceCount : IO UInt32 :=
   IO.lazyPure fun _ => deviceCountRaw 0
 
-/-- Device index selected by the bridge. This read alone does not establish availability. -/
+/-- The device the bridge runs on, as selected at its first call. -/
+inductive DeviceKind where
+  /-- A CUDA device. `Buffer.runtimeStatus` says whether one is usable. -/
+  | cuda
+  /-- The host: a CPU-only SDK, or `TORCHLEAN_LIBTORCH_DEVICE=cpu`. -/
+  | host
+  deriving DecidableEq, Repr
+
+/-- Which device the bridge selected. Meaningful only when LibTorch is linked: a build without it
+reads `.cuda` and `Buffer.runtimeStatus` reads `.notLinked`. -/
+@[no_expose] def deviceKind : IO DeviceKind :=
+  IO.lazyPure fun _ => if deviceKindRaw 0 == 0 then .host else .cuda
+
+/-- CUDA device index selected by the bridge. This read alone does not establish availability. -/
 @[no_expose] def getDevice : IO UInt32 :=
   IO.lazyPure fun _ => getDeviceRaw 0
 
 /--
-Select the device for subsequent bridge work.
+Select the CUDA device for subsequent bridge work; the host has no index and rejects the call.
 
 The native setter rejects changes while any buffer wrappers remain live, including released or
 empty wrappers. Retire those owners before switching devices; the call does not migrate tensors.
@@ -196,7 +219,7 @@ eligible choices causes a native execution error. Configure them before recordin
 Read the selected device's allocator memory fraction.
 
 This is a native allocator limit, not the fraction of memory currently free or a cache-only budget.
-Returns zero when LibTorch is not linked.
+Returns zero when LibTorch is not linked, and zero on the host, which has no such limit.
 -/
 @[no_expose] def getMemoryFraction : IO Float := do
   let fraction ← getMemoryFractionRaw 0
@@ -209,13 +232,15 @@ Set the selected device's allocator memory fraction to a finite value in `(0, 1]
 
 This configures native allocation policy; it does not release live tensors or reserve memory against
 other processes. Read back with `getMemoryFraction`; byte granularity may affect the observed limit.
+The host has no such limit and rejects the request.
 -/
 @[no_expose] def setMemoryFraction (fraction : Float) : IO Unit := do
   unless fraction.isFinite && 0.0 < fraction && fraction ≤ 1.0 do
     throw <| IO.userError "LibTorch: memory fraction must be finite and lie in (0, 1]"
   setMemoryFractionRaw fraction
 
-/-- Wait for the selected CUDA device's work, propagating native errors through `IO`. -/
+/-- Wait for the selected CUDA device's work, propagating native errors through `IO`. Host work
+is synchronous, so this returns at once there. -/
 @[no_expose] def synchronize : IO Unit :=
   synchronizeRaw 0
 
@@ -225,6 +250,7 @@ Release unused native allocator cache blocks.
 Live tensors, saved forward state, and library workspaces remain allocated. A cuBLAS workspace can
 outlive every TorchLean buffer, so both allocated and reserved bytes may remain after this call.
 Use the buffer ownership counters to distinguish those allocations from retained TorchLean owners.
+The host has no native cache, so this returns at once there.
 -/
 @[no_expose] def emptyCache : IO Unit :=
   emptyCacheRaw 0

NN/Runtime/Autograd/Engine/LibTorch/DeviceInfo.lean

@@ -0,0 +1,145 @@
+/-
+Copyright (c) 2026 TorchLean
+Released under MIT license as described in the file LICENSE.
+Authors: TorchLean Team
+-/
+
+module
+
+public import NN.Runtime.Autograd.Engine.LibTorch.Controls
+
+/-!
+# LibTorch CUDA Device Identity
+
+Readback of the CUDA device the bridge runs on. A measurement that cannot name the device it was
+taken on produces a number nobody can file beside another one. `Buffer.memory` answers how
+much device memory there is; this module answers which device.
+
+Every query takes an explicit device index and reads that device's properties through the SDK's
+own per-device cache, so the answer never depends on which device was selected earlier, and a
+multi-GPU host never combines fields from two cards in one record. The queries describe the
+visible CUDA devices, not the one the bridge selected: a CUDA-enabled SDK answers them even while
+the bridge runs on the host (`TORCHLEAN_LIBTORCH_DEVICE=cpu`). Without LibTorch linked, and on a
+CPU-only SDK, every query fails through `IO` like the other runtime controls.
+
+Two things this record does not say, which are separate questions. The SDK's packaged GPU
+architectures, the `sm_XY` targets its own kernels were compiled for: ATen's C++ API does not
+expose the list the Python package reads back, and it is a property of the SDK build rather than
+of the device, so whether the packaged kernels cover a device is settled by comparing
+`capability` against that list by other means. And the kernels TorchLean compiles at run time,
+the generated operations of `NN.Kernel`: NVRTC compiles those for the compute capability of the
+device they run on, whatever the SDK was packaged for, so their coverage is a question for NVRTC,
+not for this readback.
+-/
+
+@[expose] public section
+
+namespace Runtime
+namespace Autograd
+namespace LibTorch
+
+@[never_extract, extern "torchlean_libtorch_device_name"]
+private opaque deviceNameRaw (index : UInt32) : IO String
+
+@[never_extract, extern "torchlean_libtorch_device_capability"]
+private opaque deviceCapabilityRaw (index : UInt32) : IO UInt32
+
+@[never_extract, extern "torchlean_libtorch_device_sm_count"]
+private opaque deviceSmCountRaw (index : UInt32) : IO UInt32
+
+@[never_extract, extern "torchlean_libtorch_device_clock_khz"]
+private opaque deviceClockKhzRaw (index : UInt32) : IO UInt32
+
+@[never_extract, extern "torchlean_libtorch_device_mem_clock_khz"]
+private opaque deviceMemClockKhzRaw (index : UInt32) : IO UInt32
+
+@[never_extract, extern "torchlean_libtorch_device_mem_bus_width"]
+private opaque deviceMemBusWidthRaw (index : UInt32) : IO UInt32
+
+@[never_extract, extern "torchlean_libtorch_device_total_bytes"]
+private opaque deviceTotalBytesRaw (index : UInt32) : IO UInt64
+
+@[never_extract, extern "torchlean_libtorch_driver_version"]
+private opaque driverVersionRaw (token : UInt32) : IO UInt32
+
+@[never_extract, extern "torchlean_libtorch_runtime_version"]
+private opaque runtimeVersionRaw (token : UInt32) : IO UInt32
+
+/--
+Identity of one CUDA device, as the linked SDK reports it.
+
+The device fields come from the SDK's cached `cudaDeviceProp` for that index and from
+`cudaDeviceGetAttribute`; the two version fields from `cudaDriverGetVersion` and
+`cudaRuntimeGetVersion`. `capability` is `major * 10 + minor`, so it reads the way an `sm_XY`
+target is spelled.
+-/
+structure DeviceInfo where
+  /-- The index this record was read for. -/
+  index : UInt32
+  /-- The device name, for example `NVIDIA RTX A4500`. -/
+  name : String
+  /-- `major * 10 + minor`: `86` is `sm_86`, `120` is `sm_120`. -/
+  capability : UInt32
+  /-- Streaming multiprocessor count. -/
+  smCount : UInt32
+  /-- Core clock in kHz. -/
+  clockKhz : UInt32
+  /-- Memory clock in kHz. -/
+  memClockKhz : UInt32
+  /-- Global memory bus width in bits. -/
+  memBusWidthBits : UInt32
+  /-- Total global memory in bytes. -/
+  totalBytes : UInt64
+  /-- `cudaDriverGetVersion`, for example `13000` for 13.0. -/
+  driverVersion : UInt32
+  /-- `cudaRuntimeGetVersion` of the SDK's runtime, for example `12080` for 12.8. -/
+  runtimeVersion : UInt32
+  deriving Repr
+
+/--
+Read the properties of device `index`.
+
+Fails through `IO` when the index is outside the visible device count or LibTorch is not linked.
+Reading by explicit index is what keeps the answer independent of the selected device.
+-/
+@[no_expose] def deviceInfo (index : UInt32) : IO DeviceInfo := do
+  let name ← deviceNameRaw index
+  let capability ← deviceCapabilityRaw index
+  let smCount ← deviceSmCountRaw index
+  let clockKhz ← deviceClockKhzRaw index
+  let memClockKhz ← deviceMemClockKhzRaw index
+  let memBusWidthBits ← deviceMemBusWidthRaw index
+  let totalBytes ← deviceTotalBytesRaw index
+  let driverVersion ← driverVersionRaw 0
+  let runtimeVersion ← runtimeVersionRaw 0
+  pure { index, name, capability, smCount, clockKhz, memClockKhz, memBusWidthBits, totalBytes,
+         driverVersion, runtimeVersion }
+
+/-- The device the bridge currently selects, as `getDevice` reports it. -/
+@[no_expose] def currentDeviceInfo : IO DeviceInfo := do
+  deviceInfo (← getDevice)
+
+/-- A CUDA version integer (`12080`) as it is written (`12.8`). -/
+def versionString (v : UInt32) : String :=
+  let n := v.toNat
+  s!"{n / 1000}.{(n % 1000) / 10}"
+
+/--
+Peak theoretical memory bandwidth in GB/s from the memory clock and bus width, so a row reporting
+achieved GB/s can be read as a fraction of the roofline without looking the card up. Double data
+rate is assumed.
+-/
+def DeviceInfo.peakBandwidthGBs (d : DeviceInfo) : Float :=
+  (Float.ofNat d.memClockKhz.toNat) * 1.0e3 * 2.0 *
+    (Float.ofNat d.memBusWidthBits.toNat / 8.0) / 1.0e9
+
+/-- One-line device identity for a benchmark header. -/
+def DeviceInfo.format (d : DeviceInfo) : String :=
+  s!"{d.name} (device {d.index}, sm_{d.capability}, {d.smCount} SMs, " ++
+  s!"{(Float.ofNat d.totalBytes.toNat) / (1024.0 * 1024.0 * 1024.0)} GiB, " ++
+  s!"~{d.peakBandwidthGBs} GB/s peak, " ++
+  s!"driver {versionString d.driverVersion}, runtime {versionString d.runtimeVersion})"
+
+end LibTorch
+end Autograd
+end Runtime

NN/Runtime/Autograd/Engine/LibTorch/Trusted.lean

@@ -89,8 +89,9 @@ def Dtype.bytes : Dtype → Nat
   | .encoded => 0
 
 /--
-Opaque handle to a contiguous, dtype-carrying CUDA buffer in `csrc/libtorch/torchlean.cpp`.
-Builds without `-K cuda=true` cannot create one.
+Opaque handle to a contiguous, dtype-carrying buffer on the bridge's device (a CUDA device, or
+the host), implemented in `csrc/libtorch/torchlean.cpp`. Builds without `-K cuda=true` cannot
+create one.
 -/
 opaque BufferImpl : NonemptyType.{0}