WordPowerOfTwo.native_word_mask: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/word_power_of_two.bend as WordPowerOfTwo
Lines 155-160 of stelliferous@0.0.2.0/proofs/word_power_of_two.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/word_power_of_two.bend&start_line=155&end_line=160

import Base

def native_word_mask(+depth: Nat,+word: Word(32n),bound: {Cmp.is_lt(Word.cmp(32n,word,power(32n,
        depth))) == True{} : Bool}) -> {U32.and(U32{word},U32.sub(U32{power(32n,depth)},1)) == U32{word} : U32}:
  %Equal.sym(Word(32n),Word.sub(32n,power(32n,depth),power(32n,0n)),mask(32n,depth),Equal.trans(Word(32n),Word.sub(32n,power(32n,depth),
        power(32n,0n)),Word.adc(32n,power(32n,depth),Word.zero(32n),True{},False{}),mask(32n,depth),subtract_one(32n,power(32n,depth)),
      decrement_power(32n,depth))) : {U32{Word.and(32n,word,_)} == U32{word} : U32}
  Equal.cong(Word(32n),U32,w => U32{w},Word.and(32n,word,mask(32n,depth)),word,mask_preserves_bounded(32n,depth,word,bound))

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.adc
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.zero
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_power_of_two.bend&name=decrement_power
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_power_of_two.bend&name=mask
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_power_of_two.bend&name=mask_preserves_bounded
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_power_of_two.bend&name=power
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_power_of_two.bend&name=subtract_one