def AP.shr_shln

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

import Base

425# halving 2^(d+1) gives 2^d (below 2^32)
426def AP.shr_shln(+d: Nat, h: {Nat.is_lt(1n+d, 32n) == True{} : Bool}) -> {U32.shr(U32.shln(1, 1n+d)) == U32.shln(1, d) : U32}:
427  %AP.pw_shln(1n+d) : {U32.shr(_) == U32.shln(1, d) : U32}
428  %AP.pw_shln(d) : {U32.shr(U32{AP.pw(32n, 1n+d)}) == _ : U32}
429  AP.u32_cong(Word.shr(32n, AP.pw(32n, 1n+d)), AP.pw(32n, d), AP.shr_pw(32n, d, h))