law full

bendtorch@1.3.0.0 · LAWS.bend:138

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

138# LAW (full): row i of a head's probabilities in FullAttention is a softmax over all t positions.
139law full:
140  for +i: Nat
141  for +m: Nat
142  for +hd: Nat
143  for +sc: F32
144  for +qs: U32
145  for +qc: U32
146  for +ks: U32
147  for +kc: U32
148  for q: Array<F32>
149  for k: Array<F32>
150  for pa: Array<F32>
151  {T.pr_n(T.fprow(i, m, hd, sc, qs, qc, ks, kc, q, k, pa)) == 1n+m : Nat}