law cap_ok

lawful-bytes@0.1.1.0 · LAWS.bend:25

import Base
import lawful-bytes@0.1.1.0/defs.bend as D

25law cap_ok:
26  for b: D.Bytes
27  for d: Nat
28  for h: {D.ok(b, d) == True{} : Bool}
29  {D.cap(b) == Nat.mul(4n, Nat.pow(2n, d)) : Nat}