def AP.mask_lm

bend-osdev-array@0.1.0.1 · PROOF.bend:484

import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF

import Base

484def AP.mask_lm(+d: Nat) -> {U32.sub(U32.shln(1, d), 1) == U32{AP.lm(32n, d)} : U32}:
485  %AP.pw_shln(d) : {U32.sub(_, 1) == U32{AP.lm(32n, d)} : U32}
486  AP.u32_cong(Word.sub(32n, AP.pw(32n, d), AP.pw(32n, 0n)), AP.lm(32n, d), AP.sub_one(32n, d))

Uses (10)

Used by (4)