law kv_heads

bend-ml-llama@0.2.1.0 · main.bend:526

import Base

526# LAW (kv_heads): an empty cache holds one array of keys (and one of values) per key/value head, so key/value head j
527# of the model reads column j and no other.
528law kv_heads:
529  for +c: Cfg
530  for +cap: Nat
531  {kv_count(cap, 0n, KV.empty(c, cap)) == Cfg.kv(c) : Nat}