LibTorch CUDA 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.

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.

The raw ABI uses setting IDs 0–8: TF32 matmul, TF32 cuDNN convolution, strict determinism, cuDNN benchmarking, flash SDP, efficient SDP, math SDP, cuDNN SDP, and cuDNN enablement. Public callers use the typed operations below. Setting and memory-fraction reads, like configuration requests, return native failures through IO. Boolean settings are read back to detect a rejected request. Without LibTorch linked, reads return zero and configuration requests fail; raw setting reads also reject unknown IDs.

def Runtime.Autograd.LibTorch.version : IO String

Native build identification; "unavailable" when LibTorch is not linked.

def Runtime.Autograd.LibTorch.deviceCount : IO UInt32

Number of CUDA devices visible to the linked runtime; zero without LibTorch.

def Runtime.Autograd.LibTorch.getDevice : IO UInt32

Device index selected by the bridge. This read alone does not establish availability.

def Runtime.Autograd.LibTorch.setDevice (device : UInt32) : IO Unit

Select the device for subsequent bridge work.

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.

inductive Runtime.Autograd.LibTorch.Float32Precision : Type

Float32 input precision for matrix multiplication or cuDNN convolution.

• ieee : Float32Precision

  Disable the corresponding TF32 permission. This is not a correct-rounding theorem.

• tf32 : Float32Precision

  Permit TF32; the runtime still selects an eligible implementation.

@[instance_reducible]

instance Runtime.Autograd.LibTorch.instDecidableEqFloat32Precision : DecidableEq Float32Precision

@[instance_reducible]

instance Runtime.Autograd.LibTorch.instReprFloat32Precision : Repr Float32Precision

def Runtime.Autograd.LibTorch.instReprFloat32Precision.repr : Float32Precision → Nat → Std.Format

def Runtime.Autograd.LibTorch.getMatmulPrecision : IO Float32Precision

Read the float32 matrix multiplication precision policy.

def Runtime.Autograd.LibTorch.setMatmulPrecision (precision : Float32Precision) : IO Unit

Set the float32 matrix multiplication precision policy and check its readback.

def Runtime.Autograd.LibTorch.getConvPrecision : IO Float32Precision

Read the float32 cuDNN convolution precision policy.

def Runtime.Autograd.LibTorch.setConvPrecision (precision : Float32Precision) : IO Unit

Set the float32 cuDNN convolution precision policy and check its readback.

def Runtime.Autograd.LibTorch.getDeterministic : IO Bool

Read whether strict deterministic algorithms are enabled, with warning-only mode disabled.

def Runtime.Autograd.LibTorch.setDeterministic (enabled : Bool) : IO Unit

Request strict deterministic execution, or disable that request.

Enabling this requires native errors for unsupported deterministic operations, not warnings, and disables cuDNN benchmarking. It does not fix a particular reduction tree or promise agreement across builds or devices. Keep it stable between an attention forward call and its backward call.

def Runtime.Autograd.LibTorch.getCuDNNBenchmark : IO Bool

Read whether cuDNN convolution algorithm benchmarking is enabled.

def Runtime.Autograd.LibTorch.setCuDNNBenchmark (enabled : Bool) : IO Unit

Enable or disable cuDNN convolution benchmarking; enabling is rejected in deterministic mode.

inductive Runtime.Autograd.LibTorch.SDPBackend : Type

Native scaled-dot-product-attention implementations whose eligibility can be configured.

• flash : SDPBackend
• efficient : SDPBackend
• math : SDPBackend
• cuDNN : SDPBackend

@[instance_reducible]

instance Runtime.Autograd.LibTorch.instDecidableEqSDPBackend : DecidableEq SDPBackend

@[instance_reducible]

instance Runtime.Autograd.LibTorch.instReprSDPBackend : Repr SDPBackend

def Runtime.Autograd.LibTorch.instReprSDPBackend.repr : SDPBackend → Nat → Std.Format

def Runtime.Autograd.LibTorch.getSDPEnabled (backend : SDPBackend) : IO Bool

Read whether the selected native SDP implementation is permitted.

def Runtime.Autograd.LibTorch.setSDPEnabled (backend : SDPBackend) (enabled : Bool) : IO Unit

Permit or disable an SDP implementation.

Permission does not guarantee support for a shape, dtype, device, or mask. These choices apply to the native SDP route. Disabling all eligible choices causes a native execution error. Configure them before recording attention work.

def Runtime.Autograd.LibTorch.getCuDNNEnabled : IO Bool

Read whether cuDNN is enabled in the native context.

def Runtime.Autograd.LibTorch.setCuDNNEnabled (enabled : Bool) : IO Unit

Enable or disable cuDNN in the native context.

def Runtime.Autograd.LibTorch.getMemoryFraction : IO Float

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.

def Runtime.Autograd.LibTorch.setMemoryFraction (fraction : Float) : IO Unit

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.

def Runtime.Autograd.LibTorch.synchronize : IO Unit

Wait for the selected CUDA device's work, propagating native errors through IO.

def Runtime.Autograd.LibTorch.emptyCache : IO Unit

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.