def operands_bounded

bendtorch-core@0.1.0.0 · src/autograd/tensor_backward_PROOF.bend:296

import Base
import bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend as Backward
import bendtorch-core@0.1.0.0/src/autograd/tensor_backward_LAWS.bend as Laws

296def operands_bounded(+node: Backward.Node, +bound: Nat) ->
297  {Backward.operands_below(node, bound) == Laws.bounded(Laws.targets(node), bound) : Bool}:
298  match node:
299    case Backward.Leaf{}:
300      {==}
301    case Backward.Add{a, b, left, right}:
302      pair_bounded(a, b, bound)
303    case Backward.Sub{a, b, left, right}:
304      pair_bounded(a, b, bound)
305    case Backward.Mul{a, b, left, right}:
306      pair_bounded(a, b, bound)
307    case Backward.Sum{a, input}:
308      Equal.sym(Bool, Bool.and(Nat.is_lt(a, bound), True{}), Nat.is_lt(a, bound), and_true(Nat.is_lt(a, bound)))
309    case Backward.SumDims{a, input, kept}:
310      Equal.sym(Bool, Bool.and(Nat.is_lt(a, bound), True{}), Nat.is_lt(a, bound), and_true(Nat.is_lt(a, bound)))
311    case Backward.Matmul{a, b, left, right}:
312      pair_bounded(a, b, bound)
313    case Backward.MatmulNT{a, b, left, right}:
314      pair_bounded(a, b, bound)
315    case Backward.Relu{a, input}:
316      Equal.sym(Bool, Bool.and(Nat.is_lt(a, bound), True{}), Nat.is_lt(a, bound), and_true(Nat.is_lt(a, bound)))
317    case Backward.MseLoss{a, b, left, right}:
318      pair_bounded(a, b, bound)
319    case Backward.CrossEntropy{a, input}:
320      Equal.sym(Bool, Bool.and(Nat.is_lt(a, bound), True{}), Nat.is_lt(a, bound), and_true(Nat.is_lt(a, bound)))
321    case Backward.BatchedMatmul{a, b, left, right}:
322      pair_bounded(a, b, bound)
323    case Backward.Slice{a, input, kept, plan}:
324      Equal.sym(Bool, Bool.and(Nat.is_lt(a, bound), True{}), Nat.is_lt(a, bound), and_true(Nat.is_lt(a, bound)))
325    case Backward.Gathered{a, input, plan, entries}:
326      Equal.sym(Bool, Bool.and(Nat.is_lt(a, bound), True{}), Nat.is_lt(a, bound), and_true(Nat.is_lt(a, bound)))
327    case Backward.Constant{}:
328      {==}
329    case Backward.Frozen{id, inner}:
330      operands_bounded(inner, bound)