law causal

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

import Base

735# LAW (causal): attention at position t scores exactly t + 1 keys, the positions 0..t: one score per position
736# written, none for a position not yet computed.
737# PROOF: the gemm's result has one constructor, so matching it opens it without computing the product
738# (sr_len_g); read_len counts the 1 + t numbers read back.
739law causal:
740  for +hd: Nat
741  for +t: Nat
742  for k: Array<F32>
743  for +q: List<&2, F32>
744  {sr_len(scores(hd, t, k, q)) == 1n+t : Nat}