law backward_dangling

bendtorch-core@0.1.0.0 · src/autograd/backward_LAWS.bend:386

import Base
import bendtorch-core@0.1.0.0/src/autograd/backward.bend as Backward

386# A tape with a node that refers to itself, to a newer node or to a missing
387# node is refused with DanglingOperand.
388law backward_dangling:
389  for +entries: List<&2, Backward.Entry>
390  for +output: Nat
391  for inside: {Nat.is_lt(output, List.length(&2, Backward.Entry, entries)) == True{} : Bool}
392  for unsound: {Backward.wired(Backward.nodes(entries), List.length(&2, Backward.Entry, entries)) == False{} : Bool}
393  {Backward.backward(Backward.Tape{entries}, output) == Fail{Backward.DanglingOperand{}} : Result<&2, &2, Backward.Error, Backward.Tape>}