law replay_size

bendtorch-core@0.1.0.0 · src/storage/LAWS.bend:191

import Base

191law replay_size:
192  for +n: U32
193  for +value: F32
194  for +ops: List<&2, Op>
195  for +fits: {U32.is_le(n, 1048576) == True{} : Bool}
196  {size(replay(ops, created(n, value))) == U32.to_nat(n) : Nat}