LAWS.causal_grad: law of bendtorch@1.3.0.0
Import: import bendtorch@1.3.0.0/LAWS.bend as LAWS
Lines 169-187 of bendtorch@1.3.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch@1.3.0.0/LAWS.bend&start_line=169&end_line=187

import Base
import bendtorch@1.3.0.0/main.bend as T

# LAW (causal_grad): in T.Attention's backward pass, row i of a head's G (the gradient of its scores) is computed over
# exactly i + 1 positions. T.grow reads dP's row against values 0..i only (as qrow reads keys 0..i), writes it from the
# start of its row and runs the softmax's backward pass over as many positions as it wrote; this law says that count is
# i + 1. G starts as zeros and nothing else writes the row, so its other t - (i + 1) positions stay 0: no gradient
# reaches a key or a value after the query's position.
law causal_grad:
  for +i: Nat
  for +t: Nat
  for +hd: Nat
  for +sc: F32
  for +ds: U32
  for +dc: U32
  for +vs: U32
  for +vc: U32
  for d: Array<F32>
  for v: Array<F32>
  for p: Array<F32>
  for g: Array<F32>
  {T.gr_n(T.grow(i, t, hd, sc, ds, dc, vs, vc, d, v, p, g)) == 1n+i : Nat}

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mul
  https://jend.leeeet.dev/definition.txt?path=bend-ml-nat-lemmas@0.1.2.0/main.bend&name=add_zero
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=cnt_gdrow
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=dot0
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=gr_n
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=grow