Correctness of named kernel lowering

CUDA rendering uses numbered temporaries and mutable loop locals. Allocation must keep earlier source bindings live, including across branch-result copies and repeated loop updates. The proofs here establish that names advance monotonically and generated destinations cannot overwrite the older allocation prefix. eval_lower then proves result agreement, including checked read errors, for every scoped block. Scalar arithmetic is supplied without reassociation laws.

These are statements about the named evaluator. They do not establish correctness of CUDA text, NVRTC compilation or GPU execution.

def NN.Kernel.Cuda.Internal.writesAfter {α : Type} (first : ℕ) : Statement α → Prop

Every destination is outside the local names allocated before first.

theorem NN.Kernel.Cuda.Internal.before_mono {t : Ty} {m n : ℕ} (name : Name t) (h : m ≤ n) (hName : Name.Before m name) : Name.Before n name

Increasing the allocation bound retains every name already in scope.

theorem NN.Kernel.Cuda.Internal.writesAfter_mono {α : Type} {m n : ℕ} (statement : Statement α) (h : m ≤ n) (hWrites : writesAfter n statement) : writesAfter m statement

A block that only writes newer locals also leaves an earlier prefix untouched.

theorem NN.Kernel.Cuda.Internal.lower_bounds {α : Type} {Γ : List Ty} {t : Ty} (block : Target.Block α Γ t) (names : Names Γ) (first : ℕ) (hNames : ∀ {s : Ty} (v : Var Γ s), Name.Before first (names.get v)) : match StateT.run (lower names block) first with | ((statement, result), finish) => first ≤ finish ∧ Name.Before finish result ∧ writesAfter first statement

Allocation advances monotonically, returns an in-scope name and only writes fresh locals.

theorem NN.Kernel.Cuda.Internal.before_ne {s t : Ty} {first : ℕ} (earlier : Name s) (later : Name t) (hBefore : Name.Before first earlier) (hAfter : ¬Name.Before first later) : earlier.render ≠ later.render

An older local and a fresh destination have different CUDA spellings.

theorem NN.Kernel.Cuda.Internal.get_set_fresh {α : Type} {s t : Ty} {first : ℕ} (locals : Locals α) (name : Name t) (value : Ty.Value α t) (other : Name s) (hBefore : Name.Before first other) (hAfter : ¬Name.Before first name) : (locals.set name value).get other = locals.get other

Writing outside an allocation prefix leaves every name in that prefix unchanged.

def NN.Kernel.Cuda.Internal.frame {α : Type} (first : ℕ) (before after : Locals α) : Prop

Two local valuations agree on every name allocated before first.

theorem NN.Kernel.Cuda.Internal.frame_trans {α : Type} {first : ℕ} {a b c : Locals α} (hAB : frame first a b) (hBC : frame first b c) : frame first a c

Agreement on an allocation prefix composes across successive blocks.

theorem NN.Kernel.Cuda.Internal.steps_frame {α : Type} (first : ℕ) (body : Locals α → ExceptT Error Option (Locals α)) (hBody : ∀ (before after : Locals α), (body before).run = some (Except.ok after) → frame first before after) (acc : Name Ty.scalar) (counter : Name Ty.index) (next : Name Ty.scalar) (count : UInt64) (hAcc : ¬Name.Before first acc) (hCounter : ¬Name.Before first counter) (n : ℕ) (i : UInt64) (locals after : Locals α) (hResult : (Statement.Internal.steps body acc counter next count n i locals).run = some (Except.ok after)) : frame first locals after

Counter writes, body execution and accumulator copies retain every older local.

theorem NN.Kernel.Cuda.Internal.eval_frame {α : Type} (arithmetic : Arithmetic α) (read : Reader α) (statement : Statement α) (first : ℕ) (hWrites : writesAfter first statement) (locals after : Locals α) (hResult : (Statement.eval arithmetic read statement locals).run = some (Except.ok after)) : frame first locals after

Successfully executing a block with fresh destinations preserves the earlier valuation.

theorem NN.Kernel.Cuda.Internal.mapped_ok {α β : Type} (value : Option (Except Error α)) (f : α → β) (y : β) (h : Option.map (fun (x : Except Error α) => Except.map f x) value = some (Except.ok y)) : ∃ (x : α), value = some (Except.ok x) ∧ f x = y

A successful projected result comes from a successful unprojected valuation.

theorem NN.Kernel.Cuda.Internal.mapped_error {α β : Type} (value : Option (Except Error α)) (f : α → β) (error : Error) (h : Option.map (fun (x : Except Error α) => Except.map f x) value = some (Except.error error)) : value = some (Except.error error)

Projecting successful values cannot create or change a checked error.

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

A body simulation and preserved invariant compose over the exact bounded step order.

theorem NN.Kernel.Cuda.Internal.branch_result {α : Type} {t : Ty} (arithmetic : Arithmetic α) (read : Reader α) (name : Name t) (condition : Atom α Name Ty.predicate) (yes no : Statement α) (y n : Name t) (locals : Locals α) : Option.map (fun (x : Except Error (Locals α)) => Except.map (fun (x : Locals α) => x.get name) x) (Statement.eval arithmetic read (Statement.branch name condition yes y no n) locals).run = if Atom.eval (fun {s : Ty} => locals.get) condition = true then Option.map (fun (x : Except Error (Locals α)) => Except.map (fun (x : Locals α) => x.get y) x) (Statement.eval arithmetic read yes locals).run else Option.map (fun (x : Except Error (Locals α)) => Except.map (fun (x : Locals α) => x.get n) x) (Statement.eval arithmetic read no locals).run

Copying the selected branch result retains its value and its read failures.

theorem NN.Kernel.Cuda.lower_preserves_local {α : Type} {Γ : List Ty} {s t : Ty} (block : Target.Block α Γ t) (names : Internal.Names Γ) (first : ℕ) (hNames : ∀ {u : Ty} (v : Var Γ u), Name.Before first (names.get v)) (arithmetic : Arithmetic α) (read : Reader α) (locals after : Locals α) (other : Name s) (hBefore : Name.Before first other) (hResult : (Statement.eval arithmetic read (StateT.run (Internal.lower names block) first).1.1 locals).run = some (Except.ok after)) : after.get other = locals.get other

Running an allocated block leaves every previously allocated local unchanged.

The initial source names must lie before the allocation counter. This theorem applies to a successful run; failed reads do not produce an output valuation.

theorem NN.Kernel.Cuda.eval_lower {α : Type} {Γ : List Ty} {t : Ty} (block : Target.Block α Γ t) (names : Internal.Names Γ) (first : ℕ) (locals : Locals α) (env : Env α Γ) (hNames : ∀ {s : Ty} (v : Var Γ s), Name.Before first (names.get v)) (hScope : ∀ {s : Ty} (v : Var Γ s), locals.get (names.get v) = env.get v) (arithmetic : Arithmetic α) (read : Reader α) : match StateT.run (Internal.lower names block) first with | ((statement, result), snd) => Option.map (fun (x : Except Error (Locals α)) => Except.map (fun (x : Locals α) => x.get result) x) (Statement.eval arithmetic read statement locals).run = some (Target.Block.eval arithmetic read env block)

Allocating scoped blocks into named statements preserves their result and checked errors.

The initial named valuation must represent the source scope, whose names lie below the allocation counter. Other initial local values are arbitrary. Arithmetic is supplied without algebraic laws: the theorem preserves the specified operation and accumulation order, not a reassociated formula. It concerns named semantics, not execution of rendered CUDA by NVIDIA's compiler and device.