CUDA emission for custom operations

Each output element is computed independently. Inputs are immutable and only the current thread's output is written. Temporaries sequence arithmetic; branches and folds become structured CUDA control flow. Native compilation must use --fmad=false and --ftz=false, without fast math.

Scoped target blocks are allocated into named statements before rendering. Target.eval_lower certifies the scoped lowering; the named evaluator models mutable storage and control flow. Checked literal words retain the supplied bits; native-value round trips reuse FloatLib. The named allocation is certified in Cuda.Correctness. CUDA syntax interpretation, NVIDIA's compilation and device execution require separate evidence; the lowering theorems alone do not establish correctness of rendered text.

See NVIDIA's NVRTC manual and CUDA Math API for round-to-nearest arithmetic intrinsics: https://docs.nvidia.com/cuda/nvrtc/index.html https://docs.nvidia.com/cuda/cuda-math-api/index.html

inductive NN.Kernel.Cuda.Format : Type

Native Lean scalar formats; configured binary values use their complete-word emitter.

• binary32 : Format
• binary64 : Format

@[instance_reducible]

instance NN.Kernel.Cuda.instReprFormat : Repr Format

def NN.Kernel.Cuda.instReprFormat.repr : Format → ℕ → Std.Format

@[instance_reducible]

instance NN.Kernel.Cuda.instDecidableEqFormat : DecidableEq Format

@[reducible, inline]

abbrev NN.Kernel.Cuda.Format.Value : Format → Type

The native Lean scalar corresponding to a CUDA format.

inductive NN.Kernel.Cuda.Literal : Format → Type

Literal interchange words carry their width, rather than relying on a renderer-side cast.

• binary32 (bits : UInt32) : Literal Format.binary32
• binary64 (bits : UInt64) : Literal Format.binary64

def NN.Kernel.Cuda.Literal.bits {format : Format} : Literal format → UInt64

Retain the literal word in the common unsigned ABI without changing its bits.

def NN.Kernel.Cuda.Literal.value {format : Format} : Literal format → format.Value

Interpret a word in Lean's native float model, which canonicalizes NaN payloads.

def NN.Kernel.Cuda.Literal.ofBits (format : Format) (bits : UInt64) : Except String (Literal format)

Reject an oversized binary32 encoding before narrowing it to the format's word type.

def NN.Kernel.Cuda.Literal.ofValue (format : Format) : format.Value → Literal format

Obtain the exact interchange word of a native value.

theorem NN.Kernel.Cuda.Literal.bits_ofBits {format : Format} {bits : UInt64} {literal : Literal format} (h : ofBits format bits = Except.ok literal) : literal.bits = bits

Every accepted encoding retains all the supplied bits.

theorem NN.Kernel.Cuda.Literal.value_ofValue (format : Format) (value : format.Value) : (ofValue format value).value = value

Reconstructing the native value from its encoded word is exact in Lean's float model.

theorem NN.Kernel.Cuda.Literal.ofBits_ofValue (format : Format) (value : format.Value) : ofBits format (ofValue format value).bits = Except.ok (ofValue format value)

Native-value encodings always pass the word-width check.

def NN.Kernel.Cuda.Literal.render {format : Format} : Literal format → String

Render a checked word as a CUDA bit reinterpretation, never a decimal float approximation.

structure NN.Kernel.Cuda.Internal.Dialect (α : Type) : Type

Scalar spellings shared by hardware and software arithmetic emitters.

• scalar : String
• literal : α → Except String String
• binary : ScalarOp → String

def NN.Kernel.Cuda.Internal.unframe (first last text : String) : Option String

Remove an exact prefix and suffix, rejecting mismatched emitted syntax.

theorem NN.Kernel.Cuda.Internal.unframe_append (first last text : String) : unframe first last (first ++ text ++ last) = some text

theorem NN.Kernel.Cuda.Internal.unframe_eq_some {first last text middle : String} (h : unframe first last text = some middle) : text = first ++ middle ++ last

A successful parse consumes the entire framed text, not just a matching fragment.

def NN.Kernel.Cuda.Literal.parse (format : Format) : String → Option (Literal format)

Decode the emitted bit-reinterpretation syntax, rejecting invalid or oversized words.

This recognizes literal text, not arbitrary CUDA expressions. The word is checked before any narrowing conversion, so an out-of-range decimal integer cannot silently wrap. Only canonical decimal spelling is accepted; leading zeros would give the integer an octal meaning in CUDA.

theorem NN.Kernel.Cuda.Literal.parse_render {format : Format} (literal : Literal format) : parse format literal.render = some literal

The renderer's actual text decodes to the original interchange word in either format.

theorem NN.Kernel.Cuda.Literal.value_parse_render (format : Format) (value : format.Value) : Option.map Literal.value (parse format (ofValue format value).render) = some value

Literal text preserves a native value in Lean's float model, including signed zeros.

As with value_ofValue, this concerns the model's NaN value, not native NaN payload preservation.

inductive NN.Kernel.Cuda.Unsigned (ν : Type) : Type

Unsigned CUDA expressions over already-evaluated operands.

Raw division and remainder have no defined result at a zero denominator. The lowering inserts a lazy conditional instead of relying on Lean's total unsigned operations to model that case.

• literal {ν : Type} (value : UInt64) : Unsigned ν
• var {ν : Type} (name : ν) : Unsigned ν
• binary {ν : Type} (op : IndexOp) (x y : Unsigned ν) : Unsigned ν
• ifZero {ν : Type} (test yes no : Unsigned ν) : Unsigned ν

def NN.Kernel.Cuda.Unsigned.eval {ν : Type} (values : ν → UInt64) : Unsigned ν → Option UInt64

Interpret unsigned expressions; none represents an undefined raw division or remainder.

def NN.Kernel.Cuda.Unsigned.lower {ν : Type} (op : IndexOp) (x y : ν) : Unsigned ν

Lower an index operation on named values, guarding native division and remainder.

theorem NN.Kernel.Cuda.Unsigned.eval_lower {ν : Type} (op : IndexOp) (x y : ν) (values : ν → UInt64) : eval values (lower op x y) = some (op.eval (values x) (values y))

Guarded native operations are defined and retain Lean's unsigned result for every operand.

def NN.Kernel.Cuda.Unsigned.render {ν : Type} {m : Type → Type} [Monad m] (names : ν → m String) : Unsigned ν → m String

Render the same lazy guard represented by the unsigned expression semantics.

inductive NN.Kernel.Cuda.Atom (α : Type) (ν : Ty → Type) : Ty → Type

Atomic operands with a typed address space for local variables.

• scalar {α : Type} {ν : Ty → Type} (value : α) : Atom α ν Ty.scalar
• index {α : Type} {ν : Ty → Type} (value : UInt64) : Atom α ν Ty.index
• predicate {α : Type} {ν : Ty → Type} (value : Bool) : Atom α ν Ty.predicate
• var {α : Type} {ν : Ty → Type} {t : Ty} (name : ν t) : Atom α ν t

def NN.Kernel.Cuda.Atom.eval {α : Type} {ν : Ty → Type} {t : Ty} (values : {s : Ty} → ν s → Ty.Value α s) : Atom α ν t → Ty.Value α t

Read an atomic operand from a typed local-variable valuation.

def NN.Kernel.Cuda.Atom.lower {α : Type} {Γ : List Ty} {ν : Ty → Type} {t : Ty} (names : {s : Ty} → Var Γ s → ν s) : Target.Atom α Γ t → Atom α ν t

Replace a target variable address with its assigned typed name.

theorem NN.Kernel.Cuda.Atom.eval_lower {α : Type} {Γ : List Ty} {ν : Ty → Type} {t : Ty} (names : {s : Ty} → Var Γ s → ν s) (values : {s : Ty} → ν s → Ty.Value α s) (env : Env α Γ) (h : ∀ {s : Ty} (v : Var Γ s), values (names v) = env.get v) (atom : Target.Atom α Γ t) : eval (fun {s : Ty} => values) (lower (fun {s : Ty} => names) atom) = Target.Atom.eval env atom

Assigning names preserves atomic values when the named locals represent the source scope.

inductive NN.Kernel.Cuda.Primitive (α : Type) (ν : Ty → Type) : Ty → Type

Typed CUDA primitives, including the explicit guards required by unsigned arithmetic.

Scalar operations use the supplied arithmetic contract. A read remains checked by the reader; its CUDA implementation needs a bounds-check statement, not just a right-hand-side expression.

• copy {α : Type} {ν : Ty → Type} {t : Ty} (atom : Atom α ν t) : Primitive α ν t
• load {α : Type} {ν : Ty → Type} (operand : ℕ) (index : Atom α ν Ty.index) : Primitive α ν Ty.scalar
• binary {α : Type} {ν : Ty → Type} (op : ScalarOp) (x y : Atom α ν Ty.scalar) : Primitive α ν Ty.scalar
• neg {α : Type} {ν : Ty → Type} (x : Atom α ν Ty.scalar) : Primitive α ν Ty.scalar
• unsigned {α : Type} {ν : Ty → Type} (value : Unsigned (Atom α ν Ty.index)) : Primitive α ν Ty.index
• compare {α : Type} {ν : Ty → Type} (op : Compare) (x y : Atom α ν Ty.scalar) : Primitive α ν Ty.predicate
• indexCompare {α : Type} {ν : Ty → Type} (op : Compare) (x y : Atom α ν Ty.index) : Primitive α ν Ty.predicate

def NN.Kernel.Cuda.Primitive.eval {α : Type} (arithmetic : Arithmetic α) (read : Reader α) {ν : Ty → Type} {t : Ty} (values : {s : Ty} → ν s → Ty.Value α s) : Primitive α ν t → Option (Except Error (Ty.Value α t))

Interpret a primitive; none means undefined unsigned arithmetic, not a failed input read.

def NN.Kernel.Cuda.Primitive.lower {α : Type} {Γ : List Ty} {ν : Ty → Type} {t : Ty} (names : {s : Ty} → Var Γ s → ν s) : Target.Primitive α Γ t → Primitive α ν t

Lower a target primitive, inserting native unsigned guards before rendering.

theorem NN.Kernel.Cuda.Primitive.eval_lower {α : Type} (arithmetic : Arithmetic α) (read : Reader α) {Γ : List Ty} {ν : Ty → Type} {t : Ty} (names : {s : Ty} → Var Γ s → ν s) (values : {s : Ty} → ν s → Ty.Value α s) (env : Env α Γ) (h : ∀ {s : Ty} (v : Var Γ s), values (names v) = env.get v) (operation : Target.Primitive α Γ t) : eval arithmetic read (fun {s : Ty} => values) (lower (fun {s : Ty} => names) operation) = some (Target.Primitive.eval arithmetic read env operation)

Lowering introduces no undefined operation and preserves both values and input errors.

The arithmetic contract is unchanged: this does not identify an arbitrary contract with NVIDIA's intrinsics, or prove that rendering and native compilation implement the interpreted primitive.

inductive NN.Kernel.Cuda.Name : Ty → Type

The output index and generated temporaries form the only local-variable name space.

• index : Name Ty.index
• temporary {t : Ty} (number : ℕ) : Name t

@[instance_reducible]

instance NN.Kernel.Cuda.instDecidableEqName {a✝ : Ty} : DecidableEq (Name a✝)

def NN.Kernel.Cuda.instDecidableEqName.decEq {a✝ : Ty} (x✝ x✝¹ : Name a✝) : Decidable (x✝ = x✝¹)

def NN.Kernel.Cuda.Name.render {t : Ty} : Name t → String

Render a local name without admitting arbitrary identifier text.

def NN.Kernel.Cuda.Name.parse (t : Ty) (text : String) : Option (Name t)

Decode generated local names at their declared type, without accepting arbitrary identifiers.

The output index is available only at index type. Temporary numbers use canonical decimal spelling; names with leading zeros, trailing source text or missing allocation numbers are rejected.

theorem NN.Kernel.Cuda.Name.parse_render {t : Ty} (name : Name t) : parse t name.render = some name

Decoding an emitted local name recovers the same typed address and allocation number.

theorem NN.Kernel.Cuda.Name.render_parse {t : Ty} {text : String} {name : Name t} (h : parse t text = some name) : name.render = text

Accepted identifier text is exactly the canonical spelling of the decoded name.

theorem NN.Kernel.Cuda.Name.temporary_render_inj {s t : Ty} {m n : ℕ} : (temporary m).render = (temporary n).render ↔ m = n

Distinct allocation numbers have distinct CUDA spellings, even across scalar types.

theorem NN.Kernel.Cuda.Name.index_ne_temporary {t : Ty} (n : ℕ) : index.render ≠ (temporary n).render

Generated temporaries cannot shadow the output index.

def NN.Kernel.Cuda.Name.Before {t : Ty} (next : ℕ) : Name t → Prop

A local is the output index or was allocated before the next temporary number.

@[reducible, inline]

abbrev NN.Kernel.Cuda.Locals (α : Type) : Type

A typed valuation of named locals; values outside the current scope are unconstrained.

def NN.Kernel.Cuda.Locals.get {α : Type} (locals : Locals α) {t : Ty} (name : Name t) : Ty.Value α t

Read a named local at its declared type.

def NN.Kernel.Cuda.Locals.set {α : Type} (locals : Locals α) {t : Ty} (name : Name t) (value : Ty.Value α t) : Locals α

Replace one local value using mathlib's dependent function update.

theorem NN.Kernel.Cuda.Locals.get_set {α : Type} (locals : Locals α) {t : Ty} (name : Name t) (value : Ty.Value α t) : (locals.set name value).get name = value

A write returns the assigned value when read at the same typed address.

theorem NN.Kernel.Cuda.Locals.get_set_of_ne {α : Type} (locals : Locals α) {s t : Ty} (name : Name t) (value : Ty.Value α t) (other : Name s) (h : other.render ≠ name.render) : (locals.set name value).get other = locals.get other

A write cannot change a local with a different CUDA spelling, regardless of its type.

theorem NN.Kernel.Cuda.Locals.get_set_before {α : Type} (locals : Locals α) {s t : Ty} (next : ℕ) (value : Ty.Value α t) (other : Name s) (h : Name.Before next other) : (locals.set (Name.temporary next) value).get other = locals.get other

Allocating the next temporary leaves every earlier local unchanged.

structure NN.Kernel.Cuda.Assignment (α : Type) (t : Ty) : Type

One named assignment, including the checked read of a primitive's inputs.

• name : Name t
• operation : Primitive α Name t

def NN.Kernel.Cuda.Assignment.eval {α : Type} {t : Ty} (assignment : Assignment α t) (arithmetic : Arithmetic α) (read : Reader α) (locals : Locals α) : Option (Except Error (Locals α))

Execute the assignment in its local valuation. Failed reads never supply a stored value.

theorem NN.Kernel.Cuda.Assignment.eval_lower {α : Type} {Γ : List Ty} {t : Ty} (names : {s : Ty} → Var Γ s → Name s) (locals : Locals α) (env : Env α Γ) (h : ∀ {s : Ty} (v : Var Γ s), locals.get (names v) = env.get v) (name : Name t) (operation : Target.Primitive α Γ t) (arithmetic : Arithmetic α) (read : Reader α) : { name := name, operation := Primitive.lower (fun {s : Ty} => names) operation }.eval arithmetic read locals = some (Except.map (fun (value : Ty.Value α t) => locals.set name value) (Target.Primitive.eval arithmetic read env operation))

A lowered primitive writes exactly its source result and retains the source read errors.

theorem NN.Kernel.Cuda.Assignment.eval_preserves_scope {α : Type} {Γ : List Ty} {t : Ty} (assignment : Assignment α t) (names : {s : Ty} → Var Γ s → Name s) (locals after : Locals α) (env : Env α Γ) (hScope : ∀ {s : Ty} (v : Var Γ s), locals.get (names v) = env.get v) (hFresh : ∀ {s : Ty} (v : Var Γ s), (names v).render ≠ assignment.name.render) (arithmetic : Arithmetic α) (read : Reader α) (hResult : assignment.eval arithmetic read locals = some (Except.ok after)) {s : Ty} (v : Var Γ s) : after.get (names v) = env.get v

Assigning a fresh local preserves every previously represented source variable.

inductive NN.Kernel.Cuda.Statement (α : Type) : Type

Named statements used by both the CUDA renderer and the mutable-local evaluator.

Branch results are copied into their destination only after the selected arm finishes. Loop bodies read the current counter and accumulator, then copy their result back into the accumulator.

• skip {α : Type} : Statement α
• assign {α : Type} {t : Ty} (assignment : Assignment α t) : Statement α
• seq {α : Type} (first second : Statement α) : Statement α
• branch {α : Type} {t : Ty} (name : Name t) (condition : Atom α Name Ty.predicate) (yes : Statement α) (yesResult : Name t) (no : Statement α) (noResult : Name t) : Statement α
• loop {α : Type} (acc : Name Ty.scalar) (counter : Name Ty.index) (count : Atom α Name Ty.index) (initial : Atom α Name Ty.scalar) (body : Statement α) (next : Name Ty.scalar) : Statement α

def NN.Kernel.Cuda.Statement.Internal.steps {α : Type} (body : Locals α → ExceptT Error Option (Locals α)) (acc : Name Ty.scalar) (counter : Name Ty.index) (next : Name Ty.scalar) (count : UInt64) : ℕ → UInt64 → Locals α → ExceptT Error Option (Locals α)

Execute at most the remaining bounded steps, stopping on the unsigned guard or an error.

theorem NN.Kernel.Cuda.Statement.Internal.steps_eq_iterate {α : Type} (body : Locals α → ExceptT Error Option (Locals α)) (step : Locals α → Except Error (Locals α)) (hBody : ∀ (locals : Locals α), (body locals).run = some (step locals)) (acc : Name Ty.scalar) (counter : Name Ty.index) (next : Name Ty.scalar) (count : UInt64) (n : ℕ) (i : UInt64) (locals : Locals α) (hBound : n + i.toNat ≤ count.toNat) : (steps body acc counter next count n i locals).run = some (iterate (fun (i : UInt64) (locals : Locals α) => Except.map (fun (after : Locals α) => after.set acc (after.get next)) (step (locals.set counter i))) n i locals)

A defined body gives exactly the remaining source iterations, including their errors.

def NN.Kernel.Cuda.Statement.eval {α : Type} (arithmetic : Arithmetic α) (read : Reader α) : Statement α → Locals α → ExceptT Error Option (Locals α)

Evaluate the same named assignments and control flow that the renderer consumes.

none denotes undefined raw unsigned arithmetic; checked input failures remain Except.error. The loop's fuel is its unsigned bound, so it cannot truncate an increasing counter from zero.

theorem NN.Kernel.Cuda.Statement.eval_loop_eq {α : Type} (arithmetic : Arithmetic α) (read : Reader α) (acc : Name Ty.scalar) (counter : Name Ty.index) (count : Atom α Name Ty.index) (initial : Atom α Name Ty.scalar) (body : Statement α) (next : Name Ty.scalar) (step : Locals α → Except Error (Locals α)) (hBody : ∀ (locals : Locals α), (eval arithmetic read body locals).run = some (step locals)) (locals : Locals α) : (eval arithmetic read (loop acc counter count initial body next) locals).run = some (Target.loop (fun (i : UInt64) (locals : Locals α) => Except.map (fun (after : Locals α) => after.set acc (after.get next)) (step (locals.set counter i))) (Atom.eval (fun {s : Ty} => locals.get) count) 0 (locals.set acc (Atom.eval (fun {s : Ty} => locals.get) initial)))

A named loop agrees with the unsigned guarded loop when its body has defined semantics.

The step may fail with a checked error. The hypothesis excludes only undefined raw arithmetic, not failed input reads; each successful step copies its result into the mutable accumulator.

structure NN.Kernel.Cuda.Source : Type

Generated CUDA source and its checked input signature. Compilation fixes the FP policy.

• format : Format
• inputs : ℕ
• text : String

def NN.Kernel.Cuda.instReprSource.repr : Source → ℕ → Std.Format

@[instance_reducible]

instance NN.Kernel.Cuda.instReprSource : Repr Source

def NN.Kernel.Cuda.Internal.Format.name : Format → String

def NN.Kernel.Cuda.Internal.typeName (format : Format) : Ty → String

def NN.Kernel.Cuda.Internal.Format.binary (format : Format) (op : ScalarOp) : String

def NN.Kernel.Cuda.Internal.comparison : Compare → String

structure NN.Kernel.Cuda.Internal.Names (Γ : List Ty) : Type

• get {t : Ty} : Var Γ t → Name t

def NN.Kernel.Cuda.Internal.Names.push {Γ : List Ty} {t : Ty} (name : Name t) (names : Names Γ) : Names (t :: Γ)

def NN.Kernel.Cuda.Internal.Names.output : Names [Ty.index]

Bind the sole free output coordinate to the kernel entry point's index local.

@[reducible, inline]

abbrev NN.Kernel.Cuda.Internal.Allocate (α : Type) : Type

def NN.Kernel.Cuda.Internal.fresh (t : Ty) : Allocate (Name t)

@[reducible]

def NN.Kernel.Cuda.Internal.atomWith {α : Type} (dialect : Dialect α) {t : Ty} : Atom α Name t → Except String String

@[reducible, inline]

abbrev NN.Kernel.Cuda.Internal.native {α : Type} (format : Format) (bits : α → UInt64) : Dialect α

@[reducible, inline]

abbrev NN.Kernel.Cuda.Internal.atom {α : Type} (format : Format) (bits : α → UInt64) {t : Ty} (value : Atom α Name t) : Except String String

@[reducible]

def NN.Kernel.Cuda.Internal.expressionWith {α : Type} (dialect : Dialect α) {t : Ty} : Primitive α Name t → Except String String

Emit a primitive expression. Loads require a separate bounds-check statement.

@[reducible, inline]

abbrev NN.Kernel.Cuda.Internal.expression {α : Type} (format : Format) (bits : α → UInt64) {t : Ty} (value : Primitive α Name t) : Except String String

@[reducible]

def NN.Kernel.Cuda.Internal.Dialect.typeName {α : Type} (dialect : Dialect α) : Ty → String

theorem NN.Kernel.Cuda.Internal.typeName_native {α : Type} (format : Format) (bits : α → UInt64) (t : Ty) : (native format bits).typeName t = typeName format t

@[reducible]

def NN.Kernel.Cuda.Internal.assignmentWith {α : Type} (dialect : Dialect α) (inputs : ℕ) {t : Ty} (statement : Assignment α t) : Except String String

@[reducible, inline]

abbrev NN.Kernel.Cuda.Internal.assignment {α : Type} (format : Format) (bits : α → UInt64) (inputs : ℕ) {t : Ty} (value : Assignment α t) : Except String String

def NN.Kernel.Cuda.Internal.lower {α : Type} {Γ : List Ty} {t : Ty} (names : Names Γ) : Target.Block α Γ t → Allocate (Statement α × Name t)

@[reducible]

def NN.Kernel.Cuda.Internal.renderWith {α : Type} (dialect : Dialect α) (inputs : ℕ) : Statement α → Except String String

@[reducible, inline]

abbrev NN.Kernel.Cuda.Internal.render {α : Type} (format : Format) (bits : α → UInt64) (inputs : ℕ) (statement : Statement α) : Except String String

def NN.Kernel.Cuda.Internal.entrypoint (scalar : String) (inputs : ℕ) (body : String) (result : Name Ty.scalar) : String

Shared signature, output guard and write for native and configured scalar arithmetic.

def NN.Kernel.Cuda.source {α : Type} (format : Format) (bits : α → UInt64) (inputs : ℕ) (expr : Expr α [Ty.index] Ty.scalar) : Except String Source

Emit one independent output calculation with exact bit-pattern scalar literals.

The expression's sole free variable is its row-major output index. Each input has its own pointer and length argument. A four-word error record reports an observed invalid read; callers must check it after execution before exposing the output. No caller-provided text enters the source.