law causal

bend-ml-llama@0.2.0.0 · main.bend:733

import Base

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