law read_len

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

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

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