def shl_exact_k

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/u32.bend:70

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_shift.bend as WS

70def shl_exact_k(+n: Nat, +k: Nat, +w: Word(n), +hk: {Nat.is_le(k, n) == True{} : Bool}, +h: {Nat.is_lt(Nat.double(S.unsigned(n, w)), SC.pow2(k)) == True{} : Bool}) -> {S.unsigned(n, Word.shl(n, w)) == Nat.double(S.unsigned(n, w)) : Nat}:
71  WS.exact(n, w, N.lt_le_trans(Nat.double(S.unsigned(n, w)), SC.pow2(k), S.scale_binary(n, 1n), h, pow2_le_scale(n, k, hk)))