Certified native tensor construction

This module lifts the operation-independent native array builder to shaped tensors. Generated kernels fill one contiguous buffer with a USize loop, while the correctness theorem exposes the ordinary Rep.ofFlatFn semantics used throughout the library.

@[inline]

def TorchLean.Tensor.Internal.Elab.Impl.nativeTensorOfFlatFn {α : Type u} [storage : Storage α] {shape : Shape} (bound : USize) (hBound : bound.toNat = shape.size) (nativeValues : (index : USize) → index.toNat < shape.size → α) (values : Fin shape.size → α) (_hValues : ∀ (index : USize) (hIndex : index.toNat < shape.size), nativeValues index hIndex = values ⟨index.toNat, hIndex⟩) : Rep α shape

Build a tensor with one native row-major output loop.

The shape-size equality and callback bound proofs erase during code generation.

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeTensorOfFlatFn_correct {α : Type u} [storage : Storage α] {shape : Shape} (bound : USize) (hBound : bound.toNat = shape.size) (nativeValues : (index : USize) → index.toNat < shape.size → α) (values : Fin shape.size → α) (hValues : ∀ (index : USize) (hIndex : index.toNat < shape.size), nativeValues index hIndex = values ⟨index.toNat, hIndex⟩) : nativeTensorOfFlatFn bound hBound nativeValues values hValues = Rep.ofFlatFn values

The native tensor builder equals Rep.ofFlatFn whenever its callback agrees pointwise with the semantic finite-index function.

@[inline]

def TorchLean.Tensor.Internal.Elab.Impl.nativeTensorGather {α : Type u} [storage : Storage α] {sourceShape outputShape : Shape} (source : Rep α sourceShape) (bound : USize) (hBound : bound.toNat = outputShape.size) (sourceIndices : (index : USize) → index.toNat < outputShape.size → USize) (hSourceIndices : ∀ (index : USize) (hIndex : index.toNat < outputShape.size), (sourceIndices index hIndex).toNat < sourceShape.size) (values : Fin outputShape.size → α) (_hValues : ∀ (index : USize) (hIndex : index.toNat < outputShape.size), source.getFlatUSize (sourceIndices index hIndex) ⋯ = values ⟨index.toNat, hIndex⟩) : Rep α outputShape

Build a tensor by copying physical entries from an existing tensor.

The source-index callback returns only native indices. Generic array storage can therefore transfer existing boxed objects directly, while specialized storage performs raw scalar-buffer reads and writes.

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeTensorGather_correct {α : Type u} [storage : Storage α] {sourceShape outputShape : Shape} (source : Rep α sourceShape) (bound : USize) (hBound : bound.toNat = outputShape.size) (sourceIndices : (index : USize) → index.toNat < outputShape.size → USize) (hSourceIndices : ∀ (index : USize) (hIndex : index.toNat < outputShape.size), (sourceIndices index hIndex).toNat < sourceShape.size) (values : Fin outputShape.size → α) (hValues : ∀ (index : USize) (hIndex : index.toNat < outputShape.size), source.getFlatUSize (sourceIndices index hIndex) ⋯ = values ⟨index.toNat, hIndex⟩) : nativeTensorGather source bound hBound sourceIndices hSourceIndices values hValues = Rep.ofFlatFn values

A physical tensor gather equals its coordinate-level flat function.

@[inline]

def TorchLean.Tensor.Internal.Elab.Impl.nativeTensorCopyAt {α : Type u} [storage : Storage α] {shape : Shape} (source : Rep α shape) (index : USize) (hIndex : index.toNat < shape.size) (output : Storage.Buffer α) : Storage.Buffer α

Copy one native flat tensor entry into an output physical buffer.

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeTensorCopyAt_eq_push_of_getFlatUSize_eq {α : Type u} [storage : Storage α] {shape : Shape} (source : Rep α shape) (index : USize) (hIndex : index.toNat < shape.size) (output : Storage.Buffer α) (value : α) (hValue : source.getFlatUSize index hIndex = value) : nativeTensorCopyAt source index hIndex output = Storage.push output value

Copying a tensor entry is the same physical update as pushing its observed native flat value.

@[inline]

def TorchLean.Tensor.Internal.Elab.Impl.nativeTensorOfCopyFn {α : Type u} [storage : Storage α] {shape : Shape} (bound : USize) (hBound : bound.toNat = shape.size) (nativeStep : Storage.Buffer α → (index : USize) → index.toNat < shape.size → Storage.Buffer α) (values : Fin shape.size → α) (hStep : ∀ (output : Storage.Buffer α) (index : USize) (hIndex : index.toNat < shape.size), nativeStep output index hIndex = Storage.push output (values ⟨index.toNat, hIndex⟩)) : Rep α shape

Build a tensor with a physical-buffer update callback.

This is the movement-oriented counterpart of nativeTensorOfFlatFn: the callback copies or appends physical entries directly instead of returning an α value.

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeTensorOfCopyFn_correct {α : Type u} [storage : Storage α] {shape : Shape} (bound : USize) (hBound : bound.toNat = shape.size) (nativeStep : Storage.Buffer α → (index : USize) → index.toNat < shape.size → Storage.Buffer α) (values : Fin shape.size → α) (hStep : ∀ (output : Storage.Buffer α) (index : USize) (hIndex : index.toNat < shape.size), nativeStep output index hIndex = Storage.push output (values ⟨index.toNat, hIndex⟩)) : nativeTensorOfCopyFn bound hBound nativeStep values hStep = Rep.ofFlatFn values

A physical-update tensor fill equals its coordinate-level flat function.

@[inline]

def TorchLean.Tensor.Internal.Elab.Impl.certifiedNativeTensor {α : Type u} [Storage α] {shape : Shape} (implementation : Rep α shape) {reference : Rep α shape} (_hImplementation : implementation = reference) : Rep α shape

Return a native tensor whose semantic reference is carried only by an erased correctness certificate.

Unlike nativeTensorKernel, this boundary has no ordinary reference value or compiled value argument. It is useful when constructing either reference would duplicate a large dependent plan or perform avoidable strict runtime work.

theorem TorchLean.Tensor.Internal.Elab.Impl.certifiedNativeTensor_correct {α : Type u} [Storage α] {shape : Shape} (implementation reference : Rep α shape) (hImplementation : implementation = reference) : certifiedNativeTensor implementation hImplementation = reference

A tensor returned through an erased certificate equals its reference.

@[noinline]

def TorchLean.Tensor.Internal.Elab.Impl.nativeStage {α : Type u} {β : Type v} (value : α) (next : α → β) : β

Evaluate a staged value before entering the consumer that uses it.

Lean is strict, and @[noinline] prevents native code generation from sinking value into a consumer closure. The transformation scheduler uses this boundary when materializing an intermediate tensor is cheaper than composing another flat-index program.

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeStage_eq {α : Type u} {β : Type v} (value : α) (next : α → β) : nativeStage value next = next value

Staging changes evaluation placement, not the returned value.

@[inline]

def TorchLean.Tensor.Internal.Elab.Impl.nativeTensorKernel {α : Type u} [Storage α] {shape : Shape} (reference compiled implementation : Rep α shape) (_hCompiled : compiled = reference) (_hImplementation : implementation = compiled) : Rep α shape

Execute a native tensor implementation while retaining semantic and compiled references.

Both equality proofs erase during code generation. Standalone reasoning uses the independent semantic reference, while a downstream compiler may consume the compiled reference without recovering executable callbacks or repeating the compilation proof.

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeTensorKernel_eq_compiled {α : Type u} [Storage α] {shape : Shape} (reference compiled implementation : Rep α shape) (hCompiled : compiled = reference) (hImplementation : implementation = compiled) : nativeTensorKernel reference compiled implementation hCompiled hImplementation = compiled

A native tensor implementation equals its compact compiled reference.

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeTensorKernel_correct {α : Type u} [Storage α] {shape : Shape} (reference compiled implementation : Rep α shape) (hCompiled : compiled = reference) (hImplementation : implementation = compiled) : nativeTensorKernel reference compiled implementation hCompiled hImplementation = reference

A certified native tensor implementation equals its compact reference.