Function vstd::bits::lemma_low_bits_mask_values
source · 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.