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 TList accumulation operation.

theorem Proofs.Autograd.Algebra.Graph.foldlM_addGradAll_toIndexedAnyList_eq_add {α : Type} [Add α] [DecidableEq Spec.Shape] (t : Runtime.Autograd.Tape α) {ss : List Spec.Shape} (pref : Array (Runtime.AnyTensor α)) (seed contrib : TList α ss) (suffix : Array (Runtime.AnyTensor α)) : (∀ (i : ℕ) (hi : i < ss.length), have id := pref.size + i; ∃ (node : Runtime.Autograd.Node α), t.getNode? id = some node ∧ node.requires_grad = true ∧ node.value.s = seed.toAnyArray[i].s) → List.foldlM (fun (acc2 : Array (Runtime.AnyTensor α)) (x : ℕ × Runtime.AnyTensor α) => match x with | (pid, pg) => t.addGradAll acc2 pid pg) (pref ++ seed.toAnyArray ++ suffix) (contrib.toIndexedAnyList pref.size) = Except.ok (pref ++ (seed.add contrib).toAnyArray ++ suffix)

Key accumulation lemma for the runtime dense gradient array:

Folding Tape.addGradAll over the contributions corresponding to a TList (via toIndexedAnyList) is equivalent to pointwise addition of the typed contexts (TList.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_size_preserved {α : Type} [Add α] [DecidableEq Spec.Shape] (t : Runtime.Autograd.Tape α) (grads : Array (Runtime.AnyTensor α)) (id : ℕ) (g : Runtime.AnyTensor α) : match t.addGradAll grads id g with | Except.ok grads' => grads'.size = grads.size | Except.error a => True

Tape.addGradAll never changes the size of the dense gradient array in the .ok case.

This is a structural property needed to show the runtime reverse loop preserves array sizes.

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

If addGradAll returns .ok grads', then grads'.size = grads.size.

theorem Proofs.Autograd.Algebra.Graph.backwardDenseFromStep_ok_size {α : Type} [Add α] [DecidableEq Spec.Shape] (t : Runtime.Autograd.Tape α) {acc : Array (Runtime.AnyTensor α)} {id : ℕ} {acc' : Array (Runtime.AnyTensor α)} : 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.