Runtime-to-tape autograd link proofs.

These modules connect executable runtime graph bookkeeping to the proof-oriented autograd tape semantics used by correctness theorems.