law kv_room

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

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

561# LAW (kv_room): KV.empty(c, cap) gives each key/value head arrays of 2^cap_depth(cap·head) slots, and KV.push at
562# position t writes head numbers from t·head. For a position below the capacity (t < cap) they all fall inside the
563# slots: (1 + t)·head <= 2^cap_depth(cap·head), so a push never wraps around onto position 0. (What stays trusted is
564# tensor-array's: Array.new allocates 2^d slots.) KV.push takes a proof that t < cap, so a push at t >= cap does not
565# compile (tests/bad_cap.bend).
566law kv_room:
567  for +cap: Nat
568  for +h: Nat
569  for +t: Nat
570  for e: {True{} == TA.leb(1n+t, cap) : Bool}
571  {True{} == TA.leb(Nat.mul(1n+t, h), TA.pow2(TA.cap_depth(Nat.mul(cap, h)))) : Bool}