Runtime link: compileAux + Tape.backwardDenseFrom

compileAux produces a runtime tape whose node ids correspond to positions in the proof context Γ ++ ss, and bakes the proved vjp into each node’s runtime backward closure.

The theorem backwardDenseFrom_compileAux_eq_backpropAllCtx states that executing the runtime reverse-mode loop on this compiled tape matches the proved backpropAllCtx.

theorem Proofs.Autograd.Algebra.Graph.compileAuxData_all_requires_grad_true {α Δ : Type} [DecidableEq Spec.Shape] {Γ ss : List Spec.Shape} (g : GraphData α Δ Γ ss) (x : TList α Γ) (d : Δ) : ((compileAuxData g x d).1.nodes.all fun (n : Runtime.Autograd.Node α) => n.requires_grad) = true

All nodes produced by compileAuxData have requires_grad = true.

This is a simplifying invariant: the compiled tape is meant for correctness proofs, so we mark every node as eligible for gradient accumulation (including leaves for inputs).

theorem Proofs.Autograd.Algebra.Graph.compileAuxData_requires_grad_true {α Δ : Type} [DecidableEq Spec.Shape] {Γ ss : List Spec.Shape} (g : GraphData α Δ Γ ss) (x : TList α Γ) (d : Δ) : have t := (compileAuxData g x d).1; ∀ (i : ℕ) (hi : i < t.nodes.size), t.nodes[i].requires_grad = true

Pointwise form of compileAuxData_all_requires_grad_true: every node index is requires_grad = true.

This is often more convenient than the .all formulation when reasoning about array indexing.

theorem Proofs.Autograd.Algebra.Graph.compileAuxData_backward_pids_lt_id {α Δ : Type} [DecidableEq Spec.Shape] {Γ ss : List Spec.Shape} (g : GraphData α Δ Γ ss) (x : TList α Γ) (d0 : Δ) (id : ℕ) (n : Runtime.Autograd.Node α) : (compileAuxData g x d0).1.getNode? id = some n → ∀ (d : Runtime.AnyTensor α) (contribs : List (ℕ × Runtime.AnyTensor α)), n.backward d = Except.ok contribs → ∀ {pid : ℕ} {pg : Runtime.AnyTensor α}, (pid, pg) ∈ contribs → pid < id

Backward closure safety for compileAuxData: parent ids produced by any node are strictly smaller than the node id.

This is the “edges point backwards” invariant required by the runtime reverse loop: when processing node id, every contribution targets an earlier node (pid < id), so accumulation is well-founded.

theorem Proofs.Autograd.Algebra.Graph.compileAux_all_requires_grad_true {α Δ : Type} [DecidableEq Spec.Shape] [CommSemiring α] {Γ ss : List Spec.Shape} (g : Graph Δ Γ ss) (x : TList α Γ) (d0 : Δ) : ((g.compileAux x d0).1.nodes.all fun (n : Runtime.Autograd.Node α) => n.requires_grad) = true

All nodes produced by compileAux have requires_grad = true.

This mirrors compileAuxData_all_requires_grad_true for the Graph interface.

theorem Proofs.Autograd.Algebra.Graph.compileAux_requires_grad_true {α Δ : Type} [DecidableEq Spec.Shape] [CommSemiring α] {Γ ss : List Spec.Shape} (g : Graph Δ Γ ss) (x : TList α Γ) (d0 : Δ) : have t := (g.compileAux x d0).1; ∀ (i : ℕ) (hi : i < t.nodes.size), t.nodes[i].requires_grad = true

Pointwise form of compileAux_all_requires_grad_true.

theorem Proofs.Autograd.Algebra.Graph.compileAux_backward_pids_lt_id {α Δ : Type} [DecidableEq Spec.Shape] [CommSemiring α] {Γ ss : List Spec.Shape} (g : Graph Δ Γ ss) (x : TList α Γ) (d0 : Δ) (id : ℕ) (n : Runtime.Autograd.Node α) : (g.compileAux x d0).1.getNode? id = some n → ∀ (d : Runtime.AnyTensor α) (contribs : List (ℕ × Runtime.AnyTensor α)), n.backward d = Except.ok contribs → ∀ {pid : ℕ} {pg : Runtime.AnyTensor α}, (pid, pg) ∈ contribs → pid < id

Backward closure safety for compileAux: parent ids produced by any node are strictly smaller than the node id.

This mirrors compileAuxData_backward_pids_lt_id for the Graph interface.