type KV

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

import Base

472# One pair of arrays per key/value head: the keys (after RoPE) and the values of positions 0..t-1, position p at
473# [p·head, p·head + head). The type indexes are the capacity cap (the positions the arrays have room for, set by
474# KV.empty) and t, the number of positions written. KV.push asks for a proof that t < cap, so a cache is never
475# written past its room (kv_room says why that is enough).
476type KV<-cap: Nat, -t: Nat> is Type:
477  KV{ks: List<&1, Array<F32>>, vs: List<&1, Array<F32>>}