Certified custom-operation programs

A program retains the Lean function supplied to the frontend and a proof that its typed expression has the same result, including failed reads. The certificate concerns Lean semantics. Native CUDA emission, compilation and execution have the separate trust boundary described in Runtime.

def NN.Kernel.Env.output {α : Type} (index : UInt64) : Env α [Ty.index]

Bind the single free variable to the row-major output index.

def NN.Kernel.evaluate {α : Type} (arithmetic : Arithmetic α) (expr : Expr α [Ty.index] Ty.scalar) (read : Reader α) (index : UInt64) : Except Error α

Evaluate one output element using a supplied arithmetic implementation and input reader.

structure NN.Kernel.Program (α : Type) : Type

A frontend result with its original Lean function and checked semantic correspondence.

• scalar : Scalar α
• arithmetic : Arithmetic α
• reference : Reader α → UInt64 → Except Error α
• expression : Expr α [Ty.index] Ty.scalar
• correct (read : Reader α) (index : UInt64) : evaluate self.arithmetic self.expression read index = self.reference read index
• native : self.arithmetic = Scalar.arithmetic

  The source certificate uses the arithmetic selected for device execution.

structure NN.Kernel.Elementwise {α : Type} (f : α → α) : Type

An elementwise program whose reference calculation is the supplied scalar function.

• program : Program α
• reference_eq (read : Reader α) (index : UInt64) : self.program.reference read index = do let x ← read 0 index pure (f x)

structure NN.Kernel.Zip {α : Type} (f : α → α → α) : Type

A binary scalar function compiled with left-to-right reads of its two tensor inputs.

• program : Program α
• reference_eq (read : Reader α) (index : UInt64) : self.program.reference read index = do let x ← read 0 index let y ← read 1 index pure (f x y)

theorem NN.Kernel.Program.lower_correct {α : Type} (program : Program α) (read : Reader α) (index : UInt64) : Target.Block.eval program.arithmetic read (Env.output index) (Target.lower program.expression) = program.reference read index

The scoped target before CUDA name allocation preserves the original source function.

theorem NN.Kernel.Program.named_correct {α : Type} (program : Program α) (read : Reader α) (index : UInt64) (locals : Cuda.Locals α) (hIndex : locals.get Cuda.Name.index = index) : match StateT.run (Cuda.Internal.lower Cuda.Internal.Names.output (Target.lower program.expression)) 0 with | ((statement, result), snd) => Option.map (fun (x : Except Error (Cuda.Locals α)) => Except.map (fun (x : Cuda.Locals α) => x.get result) x) (Cuda.Statement.eval program.arithmetic read statement locals).run = some (program.reference read index)

The named statements consumed by CUDA rendering preserve the original Lean function.

Only the output index must be initialized. Other local values may be arbitrary; the allocation proof ensures that none can affect the result. Read failures are retained, and scalar arithmetic follows the supplied operation order. Rendering, NVRTC and GPU execution are separate boundaries.