law kv_of_group

bendtorch@1.3.0.0 · LAWS.bend:231

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

231# LAW (kv_of_group): T.kv_of, the function both passes of T.Attention use to pick the key/value head of query head hi,
232# gives j for every head of group j: query heads j·g + 0 .. j·g + g - 1 (g = 1 + i + k, i < g) all read key/value head j.
233law kv_of_group:
234  for +j: Nat
235  for +i: Nat
236  for +k: Nat
237  {T.kv_of(Nat.add(Nat.mul(j, 1n+Nat.add(i, k)), i), 1n+Nat.add(i, k)) == j : Nat}