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

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

# LAW (causal_keys): T.Attention reads keys only through T.qrow, and the scores it builds for the query at position i
# come from keys 0..i, one per key: exactly i + 1 of them. So no key after position i is read, and T.causal_row (law
# causal) gets the i + 1 scores its condition asks for: past them, the row of probabilities is zeros.
law causal_keys:
  for +i: Nat
  for +hd: Nat
  for +qs: U32
  for +qc: U32
  for +ks: U32
  for +kc: U32
  for q: Array<F32>
  for k: Array<F32>
  {List.length(&2, F32, T.dr_row(T.qrow(i, hd, qs, qc, ks, kc, q, k))) == 1n+i : Nat}

Uses (16):
  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=List.length
  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=len_drow
  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=dr_row
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=qrow