bendtorch-core

Releases (1):
  0.1.0.0  0x1689e5deb278c16abd3bd45eac101ef3  indexed  https://jend.leeeet.dev/files.txt?path=bendtorch-core@0.1.0.0

Definitions (5204, 1 to 100 shown):
  Backward.Error (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=Error)
   type Error is Data:
     UnknownNode{}
     DanglingOperand{}
  Backward.Node (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=Node)
   type Node is Data:
     Leaf{}
     Add{a: Nat, b: Nat}
     Sub{a: Nat, b: Nat}
     Mul{a: Nat, b: Nat, left: F32, right: F32}
     Neg{a: Nat}
  Backward.Entry (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=Entry)
   type Entry is Data:
     Entry{node: Node, value: F32, grad: Maybe<&2, F32>}
  Backward.Tape (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=Tape)
   type Tape is Data:
     Tape{entries: List<&2, Entry>}
  Backward.Contribution (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=Contribution)
   type Contribution is Data:
     Contribution{target: Nat, value: F32}
  Backward.Binary (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=Binary)
   type Binary is Data:
     Plus{}
     Minus{}
     Times{}
  Backward.empty (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=empty)
   def empty() -> Tape:
  Backward.size (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=size)
   def size(tape: Tape) -> Nat:
  Backward.picked (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=picked)
   def picked(-A: Data, head: A, rec: Unit -> Maybe<&2, A>, same: Bool) -> Maybe<&2, A>:
  Backward.find (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=find)
   # The element with id `id` in a newest-first list of count elements: the head
   # has id count - 1, and the walk counts down from it.
   def find(-A: Data, xs: List<&2, A>, +count: Nat, +id: Nat) -> Maybe<&2, A>:
  Backward.lookup (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=lookup)
   def lookup(-A: Data, +xs: List<&2, A>, +id: Nat) -> Maybe<&2, A>:
  Backward.accumulate (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=accumulate)
   def accumulate(total: Maybe<&2, F32>, contribution: Maybe<&2, F32>) -> Maybe<&2, F32>:
  Backward.bumped (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=bumped)
   def bumped(slot: Maybe<&2, F32>, +rest: List<&2, Maybe<&2, F32>>, +contribution: F32,
     rec: Unit -> List<&2, Maybe<&2, F32>>, same: Bool) -> List<&2, Maybe<&2, F32>>:
  Backward.bump (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=bump)
   def bump(slots: List<&2, Maybe<&2, F32>>, +count: Nat, +target: Nat, +contribution: F32) -> List<&2, Maybe<&2, F32>>:
  Backward.vjp (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=vjp)
   # The vector-Jacobian product of one node: the contribution each operand
   # receives when the node's gradient is g, in operand order.
   def vjp(node: Node, +g: F32) -> List<&2, Contribution>:
  Backward.deliver (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=deliver)
   def deliver(contributions: List<&2, Contribution>, +count: Nat, slots: List<&2, Maybe<&2, F32>>) -> List<&2, Maybe<&2, F32>>:
  Backward.contribute (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=contribute)
   def contribute(node: Node, gradient: Maybe<&2, F32>, +count: Nat, slots: List<&2, Maybe<&2, F32>>) -> List<&2, Maybe<&2, F32>>:
  Backward.sweep (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=sweep)
   def sweep(nodes: List<&2, Node>, gradients: List<&2, Maybe<&2, F32>>, +count: Nat) -> List<&2, Maybe<&2, F32>>:
  Backward.nones (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=nones)
   def nones(count: Nat) -> List<&2, Maybe<&2, F32>>:
  Backward.chosen (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=chosen)
   def chosen(node: Node, +rest: List<&2, Node>, +below: Nat, rec: Unit -> List<&2, Maybe<&2, F32>>, selected: Bool) ->
     List<&2, Maybe<&2, F32>>:
  Backward.pass (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=pass)
   # The gradient of output with respect to each of count nodes, newest first:
   # None for the nodes newer than output and for every node output does not
   # reach.
   def pass(nodes: List<&2, Node>, +count: Nat, +output: Nat) -> List<&2, Maybe<&2, F32>>:
  Backward.operands_below (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=operands_below)
   def operands_below(node: Node, +bound: Nat) -> Bool:
  Backward.wired (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=wired)
   def wired(nodes: List<&2, Node>, +count: Nat) -> Bool:
  Backward.nodes (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=nodes)
   def nodes(entries: List<&2, Entry>) -> List<&2, Node>:
  Backward.checked (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=checked)
   def checked(+graph: List<&2, Node>, +count: Nat, +output: Nat, known: Bool, sound: Bool) ->
     Result<&2, &2, Error, List<&2, Maybe<&2, F32>>>:
  Backward.planned (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=planned)
   def planned(+graph: List<&2, Node>, +output: Nat) -> Result<&2, &2, Error, List<&2, Maybe<&2, F32>>>:
  Backward.gradients (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=gradients)
   # The gradients of one backward of output, newest first, read from the nodes
   # alone. An output the tape does not hold is refused with UnknownNode; a tape
   # with a node that refers to itself or to a newer or missing node is refused
   # with DanglingOperand.
   def gradients(tape: Tape, +output: Nat) -> Result<&2, &2, Error, List<&2, Maybe<&2, F32>>>:
  Backward.merge (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=merge)
   def merge(entries: List<&2, Entry>, gradients: List<&2, Maybe<&2, F32>>) -> List<&2, Entry>:
  Backward.merged (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=merged)
   def merged(entries: List<&2, Entry>, result: Result<&2, &2, Error, List<&2, Maybe<&2, F32>>>) -> Result<&2, &2, Error, Tape>:
  Backward.backward (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=backward)
   # Runs one backward of output and accumulates its gradients into the slots.
   def backward(tape: Tape, +output: Nat) -> Result<&2, &2, Error, Tape>:
  Backward.cleared (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=cleared)
   def cleared(entries: List<&2, Entry>) -> List<&2, Entry>:
  Backward.zero_grad (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=zero_grad)
   # Empties every gradient slot, like PyTorch's zero_grad(set_to_none=True).
   def zero_grad(tape: Tape) -> Tape:
  Backward.entry_value (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=entry_value)
   def entry_value(found: Maybe<&2, Entry>) -> Result<&2, &2, Error, F32>:
  Backward.entry_grad (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=entry_grad)
   def entry_grad(found: Maybe<&2, Entry>) -> Result<&2, &2, Error, Maybe<&2, F32>>:
  Backward.value (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=value)
   def value(tape: Tape, +id: Nat) -> Result<&2, &2, Error, F32>:
  Backward.grad (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=grad)
   # The gradient slot of node id: None until a backward reaches it.
   def grad(tape: Tape, +id: Nat) -> Result<&2, &2, Error, Maybe<&2, F32>>:
  Backward.leaf (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=leaf)
   # Records a leaf; its id is the number of entries before it.
   def leaf(tape: Tape, value: F32) -> Tape & Nat:
  Backward.forward (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=forward)
   def forward(kind: Binary, +a: Nat, +b: Nat, +left: F32, +right: F32) -> Entry:
  Backward.operands (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=operands)
   def operands(+entries: List<&2, Entry>, kind: Binary, +a: Nat, +b: Nat,
     left: Result<&2, &2, Error, F32>, right: Result<&2, &2, Error, F32>) -> Tape & Result<&2, &2, Error, Nat>:
  Backward.binary (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=binary)
   # Records `a op b`. An operand id the tape does not hold is refused with
   # UnknownNode, and the tape comes back unchanged.
   def binary(tape: Tape, kind: Binary, +a: Nat, +b: Nat) -> Tape & Result<&2, &2, Error, Nat>:
  Backward.add (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=add)
   def add(tape: Tape, +a: Nat, +b: Nat) -> Tape & Result<&2, &2, Error, Nat>:
  Backward.sub (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=sub)
   def sub(tape: Tape, +a: Nat, +b: Nat) -> Tape & Result<&2, &2, Error, Nat>:
  Backward.mul (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=mul)
   def mul(tape: Tape, +a: Nat, +b: Nat) -> Tape & Result<&2, &2, Error, Nat>:
  Backward.negated (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=negated)
   def negated(+entries: List<&2, Entry>, +a: Nat, operand: Result<&2, &2, Error, F32>) -> Tape & Result<&2, &2, Error, Nat>:
  Backward.neg (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=neg)
   # Records -a, with the same refusal as binary.
   def neg(tape: Tape, +a: Nat) -> Tape & Result<&2, &2, Error, Nat>:
  Backward.error_code (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=error_code)
   def error_code(error: Error) -> U32:
  BackwardLAWS.marked (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=marked)
   def marked(flag: Bool, +rest: List<&2, Bool>, rec: Unit -> List<&2, Bool>, same: Bool) -> List<&2, Bool>:
  BackwardLAWS.mark (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=mark)
   def mark(flags: List<&2, Bool>, +count: Nat, +target: Nat) -> List<&2, Bool>:
  BackwardLAWS.targets (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=targets)
   def targets(node: Backward.Node) -> List<&2, Nat>:
  BackwardLAWS.mark_all (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=mark_all)
   def mark_all(ids: List<&2, Nat>, +count: Nat, flags: List<&2, Bool>) -> List<&2, Bool>:
  BackwardLAWS.spread (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=spread)
   def spread(node: Backward.Node, flag: Bool, +count: Nat, flags: List<&2, Bool>) -> List<&2, Bool>:
  BackwardLAWS.reach (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=reach)
   def reach(nodes: List<&2, Backward.Node>, flags: List<&2, Bool>, +count: Nat) -> List<&2, Bool>:
  BackwardLAWS.falses (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=falses)
   def falses(count: Nat) -> List<&2, Bool>:
  BackwardLAWS.reached_chosen (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=reached_chosen)
   def reached_chosen(node: Backward.Node, +rest: List<&2, Backward.Node>, +below: Nat, rec: Unit -> List<&2, Bool>, selected: Bool) ->
     List<&2, Bool>:
  BackwardLAWS.reached (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=reached)
   def reached(nodes: List<&2, Backward.Node>, +count: Nat, +output: Nat) -> List<&2, Bool>:
  BackwardLAWS.bounded (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=bounded)
   # Operand bounds, stated without the engine's validator: a node may name only
   # nodes older than itself, so each operand id must be below the number of
   # older nodes. An operand that is the node itself, a newer node or a missing
   # node fails this bound.
   def bounded(ids: List<&2, Nat>, +bound: Nat) -> Bool:
  BackwardLAWS.well_formed (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=well_formed)
   def well_formed(nodes: List<&2, Backward.Node>) -> Bool:
  BackwardLAWS.entry_node (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=entry_node)
   def entry_node(entry: Backward.Entry) -> Backward.Node:
  BackwardLAWS.somes (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=somes)
   def somes(gradients: List<&2, Maybe<&2, F32>>) -> List<&2, Bool>:
  BackwardLAWS.nodes_of (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=nodes_of)
   def nodes_of(tape: Backward.Tape) -> List<&2, Backward.Node>:
  BackwardLAWS.slots (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=slots)
   def slots(entries: List<&2, Backward.Entry>) -> List<&2, Maybe<&2, F32>>:
  BackwardLAWS.tape_slots (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=tape_slots)
   def tape_slots(tape: Backward.Tape) -> List<&2, Maybe<&2, F32>>:
  BackwardLAWS.slots_after (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=slots_after)
   def slots_after(result: Result<&2, &2, Backward.Error, Backward.Tape>) -> Result<&2, &2, Backward.Error, List<&2, Maybe<&2, F32>>>:
  BackwardLAWS.grad_after (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=grad_after)
   def grad_after(result: Result<&2, &2, Backward.Error, Backward.Tape>, +id: Nat) -> Result<&2, &2, Backward.Error, Maybe<&2, F32>>:
  BackwardLAWS.again (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=again)
   def again(result: Result<&2, &2, Backward.Error, Backward.Tape>, +output: Nat) -> Result<&2, &2, Backward.Error, Backward.Tape>:
  BackwardLAWS.observe (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=observe)
   def observe(+tape: Backward.Tape, +output: Nat) ->
     Result<&2, &2, Backward.Error, F32> & Result<&2, &2, Backward.Error, List<&2, Maybe<&2, F32>>>:
  BackwardLAWS.tape_of (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=tape_of)
   def tape_of(pair: Backward.Tape & Nat) -> Backward.Tape:
  BackwardLAWS.recorded (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=recorded)
   def recorded(pair: Backward.Tape & Result<&2, &2, Backward.Error, Nat>) -> Backward.Tape:
  BackwardLAWS.program_binary (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=program_binary)
   def program_binary(kind: Backward.Binary, x: F32, y: F32) -> Backward.Tape:
  BackwardLAWS.program_neg (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=program_neg)
   def program_neg(x: F32) -> Backward.Tape:
  BackwardLAWS.program_unused (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=program_unused)
   # x = 0, y = 1, z = 2, x * y = 3, z + z = 4. Node 4 is newer than the output
   # 3 and uses z twice; z is not used by 3.
   def program_unused(x: F32, y: F32, z: F32) -> Backward.Tape:
  BackwardLAWS.program_fan_out (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=program_fan_out)
   # x = 0, a = 1, b = 2, c = 3, p = x * a = 4, q = x * b = 5, r = x * c = 6,
   # s = p + q = 7, t = s + r = 8. x has three consumers.
   def program_fan_out(x: F32, a: F32, b: F32, c: F32) -> Backward.Tape:
  BackwardLAWS.vjp_leaf (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=vjp_leaf)
   law vjp_leaf:
     for +g: F32
     {Backward.vjp(Backward.Leaf{}, g) == [] : List<&2, Backward.Contribution>}
  BackwardLAWS.vjp_add (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=vjp_add)
   law vjp_add:
     for +a: Nat
     for +b: Nat
     for +g: F32
     {Backward.vjp(Backward.Add{a, b}, g) == [Backward.Contribution{a, g}, Backward.Contribution{b, g}] : List<&2, Backward.Contribution>}
  BackwardLAWS.vjp_sub (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=vjp_sub)
   law vjp_sub:
     for +a: Nat
     for +b: Nat
     for +g: F32
     {Backward.vjp(Backward.Sub{a, b}, g) == [Backward.Contribution{a, g}, Backward.Contribution{b, F32.neg(g)}] : List<&2, Backward.Contribution>}
  BackwardLAWS.vjp_mul (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=vjp_mul)
   # d(a*b)/da = b and d(a*b)/db = a, with the operand values saved at record
   # time: the first operand receives g * right, the second g * left.
   law vjp_mul:
     for +a: Nat
     for +b: Nat
     for +left: F32
     for +right: F32
     for +g: F32
     {Backward.vjp(Backward.Mul{a, b, left, right}, g) ==
       [Backward.Contribution{a, F32.mul(g, right)}, Backward.Contribution{b, F32.mul(g, left)}] : List<&2, Backward.Contribution>}
  BackwardLAWS.vjp_neg (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=vjp_neg)
   law vjp_neg:
     for +a: Nat
     for +g: F32
     {Backward.vjp(Backward.Neg{a}, g) == [Backward.Contribution{a, F32.neg(g)}] : List<&2, Backward.Contribution>}
  BackwardLAWS.backward_add (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=backward_add)
   law backward_add:
     for +x: F32
     for +y: F32
     {observe(program_binary(Backward.Plus{}, x, y), 2n) ==
       (Done{F32.add(x, y)}, Done{[Some{1.0}, Some{1.0}, Some{1.0}]}) :
       Result<&2, &2, Backward.Error, F32> & Result<&2, &2, Backward.Error, List<&2, Maybe<&2, F32>>>}
  BackwardLAWS.backward_sub (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=backward_sub)
   law backward_sub:
     for +x: F32
     for +y: F32
     {observe(program_binary(Backward.Minus{}, x, y), 2n) ==
       (Done{F32.sub(x, y)}, Done{[Some{1.0}, Some{F32.neg(1.0)}, Some{1.0}]}) :
       Result<&2, &2, Backward.Error, F32> & Result<&2, &2, Backward.Error, List<&2, Maybe<&2, F32>>>}
  BackwardLAWS.backward_mul (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=backward_mul)
   law backward_mul:
     for +x: F32
     for +y: F32
     {observe(program_binary(Backward.Times{}, x, y), 2n) ==
       (Done{F32.mul(x, y)}, Done{[Some{1.0}, Some{F32.mul(1.0, x)}, Some{F32.mul(1.0, y)}]}) :
       Result<&2, &2, Backward.Error, F32> & Result<&2, &2, Backward.Error, List<&2, Maybe<&2, F32>>>}
  BackwardLAWS.backward_neg (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=backward_neg)
   law backward_neg:
     for +x: F32
     {observe(program_neg(x), 1n) ==
       (Done{F32.neg(x)}, Done{[Some{1.0}, Some{F32.neg(1.0)}]}) :
       Result<&2, &2, Backward.Error, F32> & Result<&2, &2, Backward.Error, List<&2, Maybe<&2, F32>>>}
  BackwardLAWS.seed_selected_output (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=seed_selected_output)
   # The seed is the selected output (C1). For any graph, the nodes newer than
   # the output get None, the output gets exactly 1.0, and the older nodes get
   # what the sweep sends from the output's VJP, whatever the newer nodes are.
   law seed_selected_output:
     for +newer: List<&2, Backward.Node>
     for +node: Backward.Node
     for +rest: List<&2, Backward.Node>
     {Backward.pass(List.append(&2, Backward.Node, newer, node <> rest),
         List.length(&2, Backward.Node, List.append(&2, Backward.Node, newer, node <> rest)), List.length(&2, Backward.Node, rest)) ==
       List.append(&2, Maybe<&2, F32>, Backward.nones(List.length(&2, Backward.Node, newer)),
         Some{1.0} <> Backward.sweep(rest,
     …
  BackwardLAWS.reached_exactly (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=reached_exactly)
   # Only the reachable graph: a node has a gradient exactly when the selected
   # output reaches it. Every other node, newer or unused, reads None.
   law reached_exactly:
     for +graph: List<&2, Backward.Node>
     for +output: Nat
     {somes(Backward.pass(graph, List.length(&2, Backward.Node, graph), output)) ==
       reached(graph, List.length(&2, Backward.Node, graph), output) : List<&2, Bool>}
  BackwardLAWS.unused_leaf_none (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=unused_leaf_none)
   # With x, y and z recorded and z only used by a node newer than the output
   # x * y, backward of x * y seeds the output, leaves z and the newer node None,
   # and gives x and y their VJP.
   law unused_leaf_none:
     for +x: F32
     for +y: F32
     for +z: F32
     {slots_after(Backward.backward(program_unused(x, y, z), 3n)) ==
       Done{[None{}, Some{1.0}, None{}, Some{F32.mul(1.0, x)}, Some{F32.mul(1.0, y)}]} :
       Result<&2, &2, Backward.Error, List<&2, Maybe<&2, F32>>>}
  BackwardLAWS.accumulate_moves_in (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=accumulate_moves_in)
   # Fan-out: a node's first contribution moves in, and each later one is added
   # to the held total with one F32 add, total first.
   law accumulate_moves_in:
     for contribution: Maybe<&2, F32>
     {Backward.accumulate(None{}, contribution) == contribution : Maybe<&2, F32>}
  BackwardLAWS.accumulate_adds_total_first (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=accumulate_adds_total_first)
   law accumulate_adds_total_first:
     for +held: F32
     for +value: F32
     {Backward.accumulate(Some{held}, Some{value}) == Some{F32.add(held, value)} : Maybe<&2, F32>}
  BackwardLAWS.accumulate_keeps_without_contribution (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=accumulate_keeps_without_contribution)
   law accumulate_keeps_without_contribution:
     for +held: F32
     {Backward.accumulate(Some{held}, None{}) == Some{held} : Maybe<&2, F32>}
  BackwardLAWS.bump_target (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=bump_target)
   # A contribution to node target reaches exactly the slot of that node and no
   # other, for any list of slots.
   law bump_target:
     for +newer: List<&2, Maybe<&2, F32>>
     for +slot: Maybe<&2, F32>
     for +rest: List<&2, Maybe<&2, F32>>
     for +value: F32
     {Backward.bump(List.append(&2, Maybe<&2, F32>, newer, slot <> rest),
         List.length(&2, Maybe<&2, F32>, List.append(&2, Maybe<&2, F32>, newer, slot <> rest)), List.length(&2, Maybe<&2, F32>, rest), value) ==
       List.append(&2, Maybe<&2, F32>, newer, Backward.accumulate(slot, Some{value}) <> rest) : List<&2, Maybe<&2, F32>>}
  BackwardLAWS.fan_out_arrival_order (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=fan_out_arrival_order)
   # The contributions of x's three consumers arrive newest consumer first, and
   # each is added to the held total.
   law fan_out_arrival_order:
     for +x: F32
     for +a: F32
     for +b: F32
     for +c: F32
     {grad_after(Backward.backward(program_fan_out(x, a, b, c), 8n), 0n) ==
       Done{Some{F32.add(F32.add(F32.mul(1.0, c), F32.mul(1.0, b)), F32.mul(1.0, a))}} :
       Result<&2, &2, Backward.Error, Maybe<&2, F32>>}
  BackwardLAWS.lookup_exact (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=lookup_exact)
   # Ids (C2): id k reads exactly the element with k older elements, and an id
   # the list does not hold reads None, never another element.
   law lookup_exact:
     for -A: Data
     for +newer: List<&2, A>
     for +item: A
     for +rest: List<&2, A>
     {Backward.lookup(A, List.append(&2, A, newer, item <> rest), List.length(&2, A, rest)) == Some{item} : Maybe<&2, A>}
  BackwardLAWS.lookup_unknown (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=lookup_unknown)
   law lookup_unknown:
     for -A: Data
     for +items: List<&2, A>
     for +id: Nat
     for outside: {Nat.is_lt(id, List.length(&2, A, items)) == False{} : Bool}
     {Backward.lookup(A, items, id) == None{} : Maybe<&2, A>}
  BackwardLAWS.bump_unknown (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=bump_unknown)
   law bump_unknown:
     for +gradients: List<&2, Maybe<&2, F32>>
     for +target: Nat
     for +value: F32
     for +outside: {Nat.is_lt(target, List.length(&2, Maybe<&2, F32>, gradients)) == False{} : Bool}
     {Backward.bump(gradients, List.length(&2, Maybe<&2, F32>, gradients), target, value) == gradients : List<&2, Maybe<&2, F32>>}
  BackwardLAWS.value_unknown (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=value_unknown)
   law value_unknown:
     for +entries: List<&2, Backward.Entry>
     for +id: Nat
     for outside: {Nat.is_lt(id, List.length(&2, Backward.Entry, entries)) == False{} : Bool}
     {Backward.value(Backward.Tape{entries}, id) == Fail{Backward.UnknownNode{}} : Result<&2, &2, Backward.Error, F32>}
  BackwardLAWS.grad_unknown (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=grad_unknown)
   law grad_unknown:
     for +entries: List<&2, Backward.Entry>
     for +id: Nat
     for outside: {Nat.is_lt(id, List.length(&2, Backward.Entry, entries)) == False{} : Bool}
     {Backward.grad(Backward.Tape{entries}, id) == Fail{Backward.UnknownNode{}} : Result<&2, &2, Backward.Error, Maybe<&2, F32>>}
  BackwardLAWS.record_unknown_left (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=record_unknown_left)
   # Recording with an operand id the tape does not hold is refused with
   # UnknownNode, and the tape comes back unchanged.
   law record_unknown_left:
     for +entries: List<&2, Backward.Entry>
     for kind: Backward.Binary
     for +a: Nat
     for +b: Nat
     for outside: {Nat.is_lt(a, List.length(&2, Backward.Entry, entries)) == False{} : Bool}
     {Backward.binary(Backward.Tape{entries}, kind, a, b) == (Backward.Tape{entries}, Fail{Backward.UnknownNode{}}) :
       Backward.Tape & Result<&2, &2, Backward.Error, Nat>}
  BackwardLAWS.record_unknown_right (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=record_unknown_right)
   law record_unknown_right:
     for +entries: List<&2, Backward.Entry>
     for kind: Backward.Binary
     for +a: Nat
     for +b: Nat
     for outside: {Nat.is_lt(b, List.length(&2, Backward.Entry, entries)) == False{} : Bool}
     {Backward.binary(Backward.Tape{entries}, kind, a, b) == (Backward.Tape{entries}, Fail{Backward.UnknownNode{}}) :
       Backward.Tape & Result<&2, &2, Backward.Error, Nat>}
  BackwardLAWS.neg_unknown (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=neg_unknown)
   law neg_unknown:
     for +entries: List<&2, Backward.Entry>
     for +a: Nat
     for outside: {Nat.is_lt(a, List.length(&2, Backward.Entry, entries)) == False{} : Bool}
     {Backward.neg(Backward.Tape{entries}, a) == (Backward.Tape{entries}, Fail{Backward.UnknownNode{}}) :
       Backward.Tape & Result<&2, &2, Backward.Error, Nat>}
  BackwardLAWS.backward_unknown (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=backward_unknown)
   # backward of an output the tape does not hold is refused with UnknownNode.
   law backward_unknown:
     for +entries: List<&2, Backward.Entry>
     for +output: Nat
     for outside: {Nat.is_lt(output, List.length(&2, Backward.Entry, entries)) == False{} : Bool}
     {Backward.backward(Backward.Tape{entries}, output) == Fail{Backward.UnknownNode{}} : Result<&2, &2, Backward.Error, Backward.Tape>}
  BackwardLAWS.backward_dangling (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=backward_dangling)
   # A tape with a node that refers to itself, to a newer node or to a missing
   # node is refused with DanglingOperand.
   law backward_dangling:
     for +entries: List<&2, Backward.Entry>
     for +output: Nat
     for inside: {Nat.is_lt(output, List.length(&2, Backward.Entry, entries)) == True{} : Bool}
     for unsound: {Backward.wired(Backward.nodes(entries), List.length(&2, Backward.Entry, entries)) == False{} : Bool}
     {Backward.backward(Backward.Tape{entries}, output) == Fail{Backward.DanglingOperand{}} : Result<&2, &2, Backward.Error, Backward.Tape>}
  BackwardLAWS.wired_matches_operand_bounds (https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=wired_matches_operand_bounds)
   # The engine's wiring check is exactly the operand-bound specification above.
   law wired_matches_operand_bounds:
     for +graph: List<&2, Backward.Node>
     {Backward.wired(graph, List.length(&2, Backward.Node, graph)) == well_formed(graph) : Bool}
More: https://jend.leeeet.dev/packages/bendtorch-core.txt?definitions_offset=100