law causal_keys

bendtorch@1.3.0.0 · LAWS.bend:88

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

88# LAW (causal_keys): T.Attention reads keys only through T.qrow, and the scores it builds for the query at position i
89# 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
90# causal) gets the i + 1 scores its condition asks for: past them, the row of probabilities is zeros.
91law causal_keys:
92  for +i: Nat
93  for +hd: Nat
94  for +qs: U32
95  for +qc: U32
96  for +ks: U32
97  for +kc: U32
98  for q: Array<F32>
99  for k: Array<F32>
100  {List.length(&2, F32, T.dr_row(T.qrow(i, hd, qs, qc, ks, kc, q, k))) == 1n+i : Nat}