Configured binary CUDA emission

Configured binary formats share one device implementation, with native operations selected by the complete format and GPU architecture and integer-limb arithmetic otherwise. Expression lowering is the same as for native arithmetic; device arithmetic itself is an explicit foreign-code trust boundary. The descriptor selects exceptional-value and overflow conventions. Device arithmetic is bundled with the native bridge in csrc/libtorch/binary.h, not generated from FloatLib proofs.

def NN.Kernel.Cuda.binarySource {α : Type} (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) (encode : α → ℕ) (inputs : ℕ) (expr : Expr α [Ty.index] Ty.scalar) : Except String String

Emit exact byte literals and configured nearest-even arithmetic using the shared renderer.