law causal

bendtorch@1.3.0.0 · LAWS.bend:102

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

102# LAW (causal): in T.Attention, row i of a head's probabilities is a softmax over exactly i + 1 positions. T.prow
103# writes the query's scores from the start of its row and runs the softmax over as many positions as it wrote; the count
104# is the one the softmax's own division loop reports (T.psmc), and this law says it is i + 1, the keys 0..i of
105# causal_keys. P starts as zeros and nothing else writes the row, so its other t - (i + 1) positions stay 0: no
106# probability lands on a later position.
107law causal:
108  for +i: Nat
109  for +t: Nat
110  for +hd: Nat
111  for +sc: F32
112  for +qs: U32
113  for +qc: U32
114  for +ks: U32
115  for +kc: U32
116  for q: Array<F32>
117  for k: Array<F32>
118  for p: Array<F32>
119  {T.pr_n(T.prow(i, t, hd, sc, qs, qc, ks, kc, q, k, p)) == 1n+i : Nat}