pub proof fn lemma_low_bits_mask_values()
Expand description
ensures
low_bits_mask(0) == 0x0,
low_bits_mask(1) == 0x1,
low_bits_mask(2) == 0x3,
low_bits_mask(3) == 0x7,
low_bits_mask(4) == 0xf,
low_bits_mask(5) == 0x1f,
low_bits_mask(6) == 0x3f,
low_bits_mask(7) == 0x7f,
low_bits_mask(8) == 0xff,
low_bits_mask(9) == 0x1ff,
low_bits_mask(10) == 0x3ff,
low_bits_mask(11) == 0x7ff,
low_bits_mask(12) == 0xfff,
low_bits_mask(13) == 0x1fff,
low_bits_mask(14) == 0x3fff,
low_bits_mask(15) == 0x7fff,
low_bits_mask(16) == 0xffff,
low_bits_mask(17) == 0x1ffff,
low_bits_mask(18) == 0x3ffff,
low_bits_mask(19) == 0x7ffff,
low_bits_mask(20) == 0xfffff,
low_bits_mask(21) == 0x1fffff,
low_bits_mask(22) == 0x3fffff,
low_bits_mask(23) == 0x7fffff,
low_bits_mask(24) == 0xffffff,
low_bits_mask(25) == 0x1ffffff,
low_bits_mask(26) == 0x3ffffff,
low_bits_mask(27) == 0x7ffffff,
low_bits_mask(28) == 0xfffffff,
low_bits_mask(29) == 0x1fffffff,
low_bits_mask(30) == 0x3fffffff,
low_bits_mask(31) == 0x7fffffff,
low_bits_mask(32) == 0xffffffff,
low_bits_mask(64) == 0xffffffffffffffff,

Proof establishing the concrete values of all masks of bit sizes from 0 to 32, and 64.