law read_len

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

import Base
import bend-ml-tensor-array@0.1.19.0/main.bend as TA

700# LAW (read_len): reading m + 1 numbers of an array onto acc gives m + 1 more scores.
701# PROOF: by induction on m. With 0 left it reads one number onto acc (1 + the length of acc, by the definitions);
702# with 1 + p left it reads one and recurses one index down, and len_step moves the 1 out of the sum (tensor-array's
703# leaf_len, for scores).
704law read_len:
705  for k: Array<F32>
706  for +m: Nat
707  for +idx: U32
708  for +acc: List<&2, F32>
709  for rc: Array<F32> & F32
710  {sr_len(sr_of(k, TA.read_l(m, idx, acc, rc))) == Nat.add(1n+m, List.length(&2, F32, acc)) : Nat}