def shr_big

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

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/shrn.bend as SR

173# 32 <= k < 64: the high word shifted by k - 32
174def shr_big(+l: U32, +h: U32, +k: Nat, +hge: {Nat.is_le(32n, k) == True{} : Bool}, +hlt: {Nat.is_lt(k, 64n) == True{} : Bool}) -> {SW.value(WU.U64{U32.shrn(h, Nat.sub(k, 32n)), 0}) == C.high(k, val(l, h)) : Nat}:
175  +d = Nat.sub(k, 32n)
176  +ek = N.sub_add(k, 32n, hge)
177  +hd = L.subst(Nat, z => {Nat.is_lt(d, z) == True{} : Bool}, Nat.sub(64n, 32n), 32n, {==}, WW.sub_lt_sub(k, 64n, 32n, hlt, hge))
178  +e1 = Equal.trans(Nat, C.high(k, val(l, h)), C.high(Nat.add(32n, d), val(l, h)), C.high(d, C.high(32n, val(l, h))), Equal.cong(Nat, Nat, z => C.high(z, val(l, h)), k, Nat.add(32n, d), Equal.sym(Nat, Nat.add(32n, d), k, ek)), WW.high_comp(d, 32n, val(l, h)))
179  +e2 = Equal.trans(Nat, C.high(k, val(l, h)), C.high(d, C.high(32n, val(l, h))), C.high(d, v(h)), e1, Equal.cong(Nat, Nat, z => C.high(d, z), C.high(32n, val(l, h)), v(h), WW.high_u(32n, v(l), v(h), vb(l))))
180  Equal.trans(Nat, SW.value(WU.U64{U32.shrn(h, d), 0}), v(U32.shrn(h, d)), C.high(k, val(l, h)), val0(U32.shrn(h, d)), Equal.trans(Nat, v(U32.shrn(h, d)), C.high(d, v(h)), C.high(k, val(l, h)), SR.shrn_high(h, d), Equal.sym(Nat, C.high(k, val(l, h)), C.high(d, v(h)), e2)))