def mul_p2

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64sh.bend:121

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW

121# x 2^k on a word: low(32, shift(k, x))
122def mul_p2(+x: U32, +k: Nat, +hk: {Nat.is_lt(k, 32n) == True{} : Bool}) -> {v(U32.mul(x, X.pow2(k))) == C.low(32n, C.shift(k, v(x))) : Nat}:
123  +e = Equal.trans(Nat, Nat.mul(v(x), v(X.pow2(k))), Nat.mul(v(x), C.shift(k, 1n)), C.shift(k, v(x)), Equal.cong(Nat, Nat, t => Nat.mul(v(x), t), v(X.pow2(k)), C.shift(k, 1n), Equal.trans(Nat, v(X.pow2(k)), C.pow2(k), C.shift(k, 1n), p2v(k, hk), Equal.sym(Nat, C.shift(k, 1n), C.pow2(k), WW.shift_one(k)))), Equal.sym(Nat, C.shift(k, v(x)), Nat.mul(v(x), C.shift(k, 1n)), WW.shift_mul(k, v(x))))
124  Equal.trans(Nat, v(U32.mul(x, X.pow2(k))), C.low(32n, Nat.mul(v(x), v(X.pow2(k)))), C.low(32n, C.shift(k, v(x))), mul_low(x, X.pow2(k)), Equal.cong(Nat, Nat, t => C.low(32n, t), Nat.mul(v(x), v(X.pow2(k))), C.shift(k, v(x)), e))