law full_keys

bendtorch@1.3.0.0 · LAWS.bend:125

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

125# LAW (full_keys): FullAttention's frow reads every key 0..m, so a row's scores are 1 + m long, not 1 + i.
126law full_keys:
127  for +i: Nat
128  for +m: Nat
129  for +hd: Nat
130  for +qs: U32
131  for +qc: U32
132  for +ks: U32
133  for +kc: U32
134  for q: Array<F32>
135  for k: Array<F32>
136  {List.length(&2, F32, T.dr_row(T.frow(i, m, hd, qs, qc, ks, kc, q, k))) == 1n+m : Nat}