law split_tail_short

bend-osdev-mode-core@0.1.0.0 · LAWS.bend:112

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M

112# the tail of a split has fewer than 16 bytes
113law split_tail_short:
114  for ys: List<&2, U32>
115  {Nat.is_lt(B.len(M.cm.split.tail(M.cm.split(B.mask(ys)))), 16n) == True{} : Bool}