Indexed tensor lookup and an array context shared by forward graphs and algebraic tapes. The correspondence certificate is erased at runtime; reads select tensors without traversing a linked pack. Conversion to a pack happens at an explicit typed boundary.

structure Proofs.Autograd.Algebra.TensorLookup (α : Type) [TorchLean.Storage α] (shapes : List Spec.Shape) : Type

Tensor selection without committing a node to a linked pack representation.

• read {shape : Spec.Shape} : Idx shapes shape → TorchLean.Tensor α shape

  Select the tensor with the shape certified by its index.

theorem Proofs.Autograd.Algebra.TensorLookup.ext_iff {α : Type} {inst✝ : TorchLean.Storage α} {shapes : List Spec.Shape} {x y : TensorLookup α shapes} : x = y ↔ @read α inst✝ shapes x = @read α inst✝ shapes y

theorem Proofs.Autograd.Algebra.TensorLookup.ext {α : Type} {inst✝ : TorchLean.Storage α} {shapes : List Spec.Shape} {x y : TensorLookup α shapes} (read : @read α inst✝ shapes x = @read α inst✝ shapes y) : x = y

def Proofs.Autograd.Algebra.TensorLookup.ofPack {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} (xs : TorchLean.TensorPack α shapes) : TensorLookup α shapes

Present a linked tensor pack through the selection interface.

@[instance_reducible]

instance Proofs.Autograd.Algebra.instCoeTensorPackTensorLookup {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} : Coe (TorchLean.TensorPack α shapes) (TensorLookup α shapes)

Typed packs can supply a node's lookup without changing tensor values.

@[simp]

theorem Proofs.Autograd.Algebra.TensorLookup.read_ofPack {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} (xs : TorchLean.TensorPack α shapes) {shape : Spec.Shape} (idx : Idx shapes shape) : (ofPack xs).read idx = getIdx xs idx

Reading a pack through the lookup agrees with its typed selection.

def Proofs.Autograd.Algebra.TensorLookup.toPack {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} : TensorLookup α shapes → TorchLean.TensorPack α shapes

Materialize a reader at an explicit typed boundary.

@[simp]

theorem Proofs.Autograd.Algebra.TensorLookup.getIdx_toPack {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} (lookup : TensorLookup α shapes) {shape : Spec.Shape} (idx : Idx shapes shape) : getIdx lookup.toPack idx = lookup.read idx

@[simp]

theorem Proofs.Autograd.Algebra.TensorLookup.toPack_ofPack {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} (xs : TorchLean.TensorPack α shapes) : (ofPack xs).toPack = xs

@[simp]

theorem Proofs.Autograd.Algebra.TensorLookup.ofPack_toPack {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} (lookup : TensorLookup α shapes) : ofPack lookup.toPack = lookup

theorem Proofs.Autograd.Algebra.TensorLookup.shape_eq_of_index_eq {shapes : List Spec.Shape} {source target : Spec.Shape} (left : Idx shapes source) (right : Idx shapes target) (same : ↑left.i = ↑right.i) : source = target

Equal context positions certify equal tensor shapes.

def Proofs.Autograd.Algebra.TensorLookup.set {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} (lookup : TensorLookup α shapes) {shape : Spec.Shape} (idx : Idx shapes shape) (value : TorchLean.Tensor α shape) : TensorLookup α shapes

Replace one typed entry of a reader.

@[simp]

theorem Proofs.Autograd.Algebra.TensorLookup.read_set_self {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} (lookup : TensorLookup α shapes) {shape : Spec.Shape} (idx : Idx shapes shape) (value : TorchLean.Tensor α shape) : (lookup.set idx value).read idx = value

@[simp]

theorem Proofs.Autograd.Algebra.TensorLookup.read_set_other {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} (lookup : TensorLookup α shapes) {shape otherShape : Spec.Shape} (idx : Idx shapes shape) (value : TorchLean.Tensor α shape) (other : Idx shapes otherShape) (different : ↑idx.i ≠ ↑other.i) : (lookup.set idx value).read other = lookup.read other

theorem Proofs.Autograd.Algebra.TensorLookup.ofTensor_read_set {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} (lookup : TensorLookup α shapes) {shape otherShape : Spec.Shape} (idx : Idx shapes shape) (value : TorchLean.Tensor α shape) (other : Idx shapes otherShape) : Spec.SomeTensor.ofTensor ((lookup.set idx value).read other) = if ↑idx.i = ↑other.i then Spec.SomeTensor.ofTensor value else Spec.SomeTensor.ofTensor (lookup.read other)

Erasing shapes removes the transport in a reader update.

theorem Proofs.Autograd.Algebra.TensorLookup.read_set_from {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} (lookup source : TensorLookup α shapes) {shape otherShape : Spec.Shape} (idx : Idx shapes shape) (other : Idx shapes otherShape) : (lookup.set idx (source.read idx)).read other = if ↑other.i = ↑idx.i then source.read other else lookup.read other

Updating from another reader copies exactly that reader's value at the selected position.

structure Proofs.Autograd.Algebra.TensorContext (α : Type) [TorchLean.Storage α] (shapes : List Spec.Shape) : Type

Runtime tensor references with an erased certificate of their shapes and order.

• values : Array (Spec.SomeTensor α)

  Inputs followed by node values in evaluation order.

• valid : ∃ (xs : TorchLean.TensorPack α shapes), self.values = xs.toShapeErasedArray

  Every runtime entry has the shape at the same position in the typed context.

theorem Proofs.Autograd.Algebra.TensorContext.ext_iff {α : Type} {inst✝ : TorchLean.Storage α} {shapes : List Spec.Shape} {x y : TensorContext α shapes} : x = y ↔ x.values = y.values

theorem Proofs.Autograd.Algebra.TensorContext.ext {α : Type} {inst✝ : TorchLean.Storage α} {shapes : List Spec.Shape} {x y : TensorContext α shapes} (values : x.values = y.values) : x = y

def Proofs.Autograd.Algebra.TensorContext.ofPack {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} (xs : TorchLean.TensorPack α shapes) : TensorContext α shapes

Convert input tensors once, before traversing the graph.

theorem Proofs.Autograd.Algebra.TensorContext.size_values {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} (ctx : TensorContext α shapes) : ctx.values.size = shapes.length

Runtime and typed contexts have the same number of entries.

def Proofs.Autograd.Algebra.TensorContext.lookup {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} (ctx : TensorContext α shapes) : TensorLookup α shapes

Read a previously checked position in constant time.

@[simp]

theorem Proofs.Autograd.Algebra.TensorContext.lookup_ofPack {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} (xs : TorchLean.TensorPack α shapes) : (ofPack xs).lookup = TensorLookup.ofPack xs

Array lookup agrees with the original typed pack lookup.

@[simp]

theorem Proofs.Autograd.Algebra.TensorContext.ofTensor_lookup {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} (ctx : TensorContext α shapes) {shape : Spec.Shape} (idx : Idx shapes shape) : Spec.SomeTensor.ofTensor (ctx.lookup.read idx) = ctx.values[↑idx.i]

def Proofs.Autograd.Algebra.TensorContext.set {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} (ctx : TensorContext α shapes) {shape : Spec.Shape} (idx : Idx shapes shape) (value : TorchLean.Tensor α shape) : TensorContext α shapes

Update one tensor reference without copying the context when it is uniquely owned.

@[simp]

theorem Proofs.Autograd.Algebra.TensorContext.lookup_set {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} (ctx : TensorContext α shapes) {shape : Spec.Shape} (idx : Idx shapes shape) (value : TorchLean.Tensor α shape) : (ctx.set idx value).lookup = ctx.lookup.set idx value

def Proofs.Autograd.Algebra.TensorContext.cast {α : Type} [TorchLean.Storage α] {shapes other : List Spec.Shape} (h : shapes = other) (ctx : TensorContext α shapes) : TensorContext α other

Transport the type index without changing the runtime array.

@[simp]

theorem Proofs.Autograd.Algebra.TensorContext.cast_ofPack {α : Type} [TorchLean.Storage α] {shapes other : List Spec.Shape} (h : shapes = other) (xs : TorchLean.TensorPack α shapes) : cast h (ofPack xs) = ofPack (TorchLean.TensorPack.cast h xs)

def Proofs.Autograd.Algebra.TensorContext.push {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} {shape : Spec.Shape} (ctx : TensorContext α shapes) (x : TorchLean.Tensor α shape) : TensorContext α (shapes ++ [shape])

Append a tensor reference, amortized constant time when the context is uniquely owned.

Retaining a previous context or its lookup can make this append copy the shared array.

@[simp]

theorem Proofs.Autograd.Algebra.TensorContext.push_ofPack {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} {shape : Spec.Shape} (xs : TorchLean.TensorPack α shapes) (x : TorchLean.Tensor α shape) : (ofPack xs).push x = ofPack (xs.snoc x)

def Proofs.Autograd.Algebra.TensorContext.pop {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} {shape : Spec.Shape} (ctx : TensorContext α (shapes ++ [shape])) : TensorContext α shapes × TorchLean.Tensor α shape

Remove the last reference in constant time, preserving the typed prefix.

@[simp]

theorem Proofs.Autograd.Algebra.TensorContext.pop_ofPack_snoc {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} {shape : Spec.Shape} (xs : TorchLean.TensorPack α shapes) (value : TorchLean.Tensor α shape) : (ofPack (xs.snoc value)).pop = (ofPack xs, value)

@[simp]

theorem Proofs.Autograd.Algebra.TensorContext.pop_ofPack {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} {shape : Spec.Shape} (xs : TorchLean.TensorPack α (shapes ++ [shape])) : (ofPack xs).pop = (ofPack xs.unsnoc.1, xs.unsnoc.2)

def Proofs.Autograd.Algebra.TensorContext.toPack {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} (ctx : TensorContext α shapes) : TorchLean.TensorPack α shapes

Recover the public typed result once at the execution boundary.

@[simp]

theorem Proofs.Autograd.Algebra.TensorContext.toPack_ofPack {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} (xs : TorchLean.TensorPack α shapes) : (ofPack xs).toPack = xs

@[simp]

theorem Proofs.Autograd.Algebra.TensorContext.ofPack_toPack {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} (ctx : TensorContext α shapes) : ofPack ctx.toPack = ctx

@[simp]

theorem Proofs.Autograd.Algebra.TensorContext.lookup_toPack {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} (ctx : TensorContext α shapes) : TensorLookup.ofPack ctx.toPack = ctx.lookup

@[simp]

theorem Proofs.Autograd.Algebra.TensorContext.toPack_pop {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} {shape : Spec.Shape} (ctx : TensorContext α (shapes ++ [shape])) : (ctx.pop.1.toPack, ctx.pop.2) = ctx.toPack.unsnoc

@[simp]

theorem Proofs.Autograd.Algebra.TensorContext.toPack_cast {α : Type} [TorchLean.Storage α] {shapes other : List Spec.Shape} (same : shapes = other) (ctx : TensorContext α shapes) : (cast same ctx).toPack = TorchLean.TensorPack.cast same ctx.toPack

@[simp]

theorem Proofs.Autograd.Algebra.TensorContext.toPack_push {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} {shape : Spec.Shape} (ctx : TensorContext α shapes) (value : TorchLean.Tensor α shape) : (ctx.push value).toPack = ctx.toPack.snoc value