law native_mask_preserves_bounded

stelliferous@0.0.2.0 · proofs/word_power_of_two.bend:162

import Base

162law native_mask_preserves_bounded:
163  for +depth: Nat
164  for +index: U32
165  {U32.is_lt(index,U32.shln(1,depth)) == True{} : Bool} -> {U32.and(index,U32.sub(U32.shln(1,depth),1)) == index : U32}