Structured kernel target

Primitive operands are values, not computations. Bindings therefore fix the order of reads and arithmetic before CUDA rendering. Branches and loops retain their own blocks, so lowering cannot hoist a failing read out of a branch or reassociate a sequential accumulation.

The target evaluator specifies these blocks independently of the source evaluator. Its lowering theorem is about this representation, not NVIDIA's compiler or execution of rendered text.

theorem NN.Kernel.Target.Internal.increment_toNat {i count : UInt64} (h : i < count) : (i + 1).toNat = i.toNat + 1

Incrementing below an unsigned loop bound cannot wrap, even at the largest bound.

@[irreducible]

def NN.Kernel.Target.loop {α : Type} (step : UInt64 → α → Except Error α) (count i : UInt64) (acc : α) : Except Error α

An unsigned counter loop, stopping before count and at the first failed step.

The strict guard ensures that incrementing the counter cannot wrap, even when count is the largest representable index. Starting at or beyond the bound leaves the accumulator unchanged.

theorem NN.Kernel.Target.loop_eq_iterate {α : Type} (step : UInt64 → α → Except Error α) (count i : UInt64) (acc : α) : loop step count i acc = iterate step (count.toNat - i.toNat) i acc

The unsigned guard executes exactly the remaining sequential steps, including their errors.

inductive NN.Kernel.Target.Atom (α : Type) : List Ty → Ty → Type

Constants and typed local variables, with no effects or arithmetic.

• scalar {α : Type} {Γ : List Ty} (value : α) : Atom α Γ Ty.scalar
• index {α : Type} {Γ : List Ty} (value : UInt64) : Atom α Γ Ty.index
• predicate {α : Type} {Γ : List Ty} (value : Bool) : Atom α Γ Ty.predicate
• var {α : Type} {Γ : List Ty} {t : Ty} (v : Var Γ t) : Atom α Γ t

inductive NN.Kernel.Target.Primitive (α : Type) : List Ty → Ty → Type

One primitive operation whose operands have already been evaluated.

• load {α : Type} {Γ : List Ty} (operand : Nat) (index : Atom α Γ Ty.index) : Primitive α Γ Ty.scalar
• binary {α : Type} {Γ : List Ty} (op : ScalarOp) (x y : Atom α Γ Ty.scalar) : Primitive α Γ Ty.scalar
• neg {α : Type} {Γ : List Ty} (x : Atom α Γ Ty.scalar) : Primitive α Γ Ty.scalar
• indexBinary {α : Type} {Γ : List Ty} (op : IndexOp) (x y : Atom α Γ Ty.index) : Primitive α Γ Ty.index
• compare {α : Type} {Γ : List Ty} (op : Compare) (x y : Atom α Γ Ty.scalar) : Primitive α Γ Ty.predicate
• indexCompare {α : Type} {Γ : List Ty} (op : Compare) (x y : Atom α Γ Ty.index) : Primitive α Γ Ty.predicate

inductive NN.Kernel.Target.Block (α : Type) : List Ty → Ty → Type

Scoped statement blocks. A binding finishes its value block before entering its body.

• result {α : Type} {Γ : List Ty} {t : Ty} (value : Atom α Γ t) : Block α Γ t
• compute {α : Type} {Γ : List Ty} {t : Ty} (operation : Primitive α Γ t) : Block α Γ t
• bind {α : Type} {Γ : List Ty} {s t : Ty} (value : Block α Γ s) (body : Block α (s :: Γ) t) : Block α Γ t
• branch {α : Type} {Γ : List Ty} {t : Ty} (p : Atom α Γ Ty.predicate) (yes no : Block α Γ t) : Block α Γ t
• loop {α : Type} {Γ : List Ty} (count : Atom α Γ Ty.index) (initial : Atom α Γ Ty.scalar) (body : Block α (Ty.scalar :: Ty.index :: Γ) Ty.scalar) : Block α Γ Ty.scalar

def NN.Kernel.Target.Atom.eval {α : Type} {Γ : List Ty} {t : Ty} (env : Env α Γ) : Atom α Γ t → Ty.Value α t

Read an atomic value from the current environment.

def NN.Kernel.Target.Primitive.eval {α : Type} (arithmetic : Arithmetic α) (read : Reader α) {Γ : List Ty} {t : Ty} (env : Env α Γ) : Primitive α Γ t → Except Error (Ty.Value α t)

Perform one operation, retaining the reader's error rather than supplying a default value.

def NN.Kernel.Target.Block.eval {α : Type} (arithmetic : Arithmetic α) (read : Reader α) {Γ : List Ty} {t : Ty} (env : Env α Γ) : Block α Γ t → Except Error (Ty.Value α t)

Sequential block semantics, with lazy branches and increasing-index loop accumulation.

def NN.Kernel.Target.Atom.rename {α : Type} {Γ Δ : List Ty} {t : Ty} (ρ : Renaming Γ Δ) : Atom α Γ t → Atom α Δ t

Move an atom's variable addresses under a new scope.

def NN.Kernel.Target.Primitive.rename {α : Type} {Γ Δ : List Ty} {t : Ty} (ρ : Renaming Γ Δ) : Primitive α Γ t → Primitive α Δ t

Rename only the already-evaluated operands of a primitive.

def NN.Kernel.Target.Block.rename {α : Type} {Γ Δ : List Ty} {t : Ty} (ρ : Renaming Γ Δ) : Block α Γ t → Block α Δ t

Rename a block without changing its sequencing or control-flow regions.

theorem NN.Kernel.Target.Atom.eval_rename {α : Type} {Γ Δ : List Ty} {t : Ty} (value : Atom α Γ t) (ρ : Renaming Γ Δ) (env : Env α Δ) : eval env (rename (fun {t : Ty} => ρ) value) = eval (Env.pull (fun {t : Ty} => ρ) env) value

Renaming an atom is equivalent to looking up its original address in a pulled environment.

theorem NN.Kernel.Target.Primitive.eval_rename {α : Type} {Γ Δ : List Ty} {t : Ty} (operation : Primitive α Γ t) (arithmetic : Arithmetic α) (read : Reader α) (ρ : Renaming Γ Δ) (env : Env α Δ) : eval arithmetic read env (rename (fun {t : Ty} => ρ) operation) = eval arithmetic read (Env.pull (fun {t : Ty} => ρ) env) operation

Renaming cannot change primitive results or failed reads.

theorem NN.Kernel.Target.Block.eval_rename {α : Type} {Γ : List Ty} {t : Ty} (block : Block α Γ t) (arithmetic : Arithmetic α) (read : Reader α) {Δ : List Ty} (ρ : Renaming Γ Δ) (env : Env α Δ) : eval arithmetic read env (rename (fun {t : Ty} => ρ) block) = eval arithmetic read (Env.pull (fun {t : Ty} => ρ) env) block

Renaming scoped statements preserves both values and errors.

def NN.Kernel.Target.lower {α : Type} {Γ : List Ty} {t : Ty} : Expr α Γ t → Block α Γ t

Lower source expressions to blocks with atomic primitive operands.

theorem NN.Kernel.Target.eval_lower {α : Type} {Γ : List Ty} {t : Ty} (expr : Expr α Γ t) (arithmetic : Arithmetic α) (read : Reader α) (env : Env α Γ) : Block.eval arithmetic read env (lower expr) = Expr.eval arithmetic read env expr

Lowering preserves results and failures without scalar associativity or field assumptions.