Runtime Gradient Accumulation Link

This file connects the executable dense-gradient array used by the runtime tape to the typed context addition used in the proved autograd algebra. The main lemmas show that folding runtime gradient updates over indexed tensors agrees with the proof-level TorchLean.TensorPack accumulation operation.

theorem Proofs.Autograd.Algebra.Graph.foldlM_addGradAll_toIndexedShapeErasedArray_eq_add {α : Type} [TorchLean.Storage α] [Add α] (t : Runtime.Autograd.Tape α) {ss : List Spec.Shape} (pref : Array (Spec.SomeTensor α)) (seed contrib : TorchLean.TensorPack α ss) (suffix : Array (Spec.SomeTensor α)) : (∀ (i : ℕ) (hi : i < ss.length), have id := pref.size + i; ∃ (node : Runtime.Autograd.Node α), t.getNode? id = some node ∧ node.requiresGrad = true ∧ node.value.shape = seed.toShapeErasedArray[i].shape) → Array.foldlM (fun (acc2 : Array (Spec.SomeTensor α)) (x : ℕ × Spec.SomeTensor α) => match x with | (pid, pg) => t.addGradAll acc2 pid pg) (pref ++ seed.toShapeErasedArray ++ suffix) (contrib.toIndexedShapeErasedArray pref.size) = Except.ok (pref ++ (seed.add contrib).toShapeErasedArray ++ suffix)

Key accumulation lemma for the runtime dense gradient array:

Folding Tape.addGradAll over the contributions corresponding to a TorchLean.TensorPack (via toIndexedShapeErasedArray) is equivalent to pointwise addition of the typed contexts (TorchLean.TensorPack.add), embedded back into the array layout pref ++ seed ++ suffix.

This is the “runtime accumulation matches proved addition” bridge.

theorem Proofs.Autograd.Algebra.Graph.addGradAll_ok_size {α : Type} [TorchLean.Storage α] [Add α] (t : Runtime.Autograd.Tape α) {grads : Array (Spec.SomeTensor α)} {id : ℕ} {g : Spec.SomeTensor α} {grads' : Array (Spec.SomeTensor α)} (h : t.addGradAll grads id g = Except.ok grads') : grads'.size = grads.size

Tape.addGradAll never changes the size of the dense gradient array when it succeeds.

This is the structural property that lets the runtime reverse loop preserve array sizes.

theorem Proofs.Autograd.Algebra.Graph.backwardDenseFromStep_ok_size {α : Type} [TorchLean.Storage α] [Add α] (t : Runtime.Autograd.Tape α) {acc : Array (Spec.SomeTensor α)} {id : ℕ} {acc' : Array (Spec.SomeTensor α)} : t.backwardDenseFromStep acc id = Except.ok acc' → acc'.size = acc.size

If one step of the runtime dense backward loop succeeds, it preserves the accumulator array size.

This is proved by showing the internal foldlM addGradAll preserves size, then splitting on the control flow of backwardDenseFromStep.