~/jendhub

def ws.gshl_hi

bend-osdev-word64@0.1.1.0 · proof_shift.bend:408

import bend-osdev-word64@0.1.1.0/proof_shift.bend as ProofShift
import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
import bend-osdev-word64@0.1.1.0/proof_value.bend as P
import bend-osdev-u32@0.1.0.0/LAWS_order.bend as UO

408# a shift left by n <= k: the high half is the low half shifted by k - n, the
409# high half's bits all carried out (and 0, if nothing overflows)
410def ws.gshl_hi(+n: Nat, +k: Nat, +hw: Word(n), +lw: Word(n), +ch: Word(n), +cl: Word(n), +h1: {Nat.is_le(n, k) == True{} : Bool}, +h: {Nat.is_le(U.U32Nat.dbl(k, P.wv.V(n, hw, lw)), P.wv.V(n, ch, cl)) == True{} : Bool}) -> {P.wv.V(n, ws.shl(n, Nat.sub(k, n), lw), Word.zero(n)) == U.U32Nat.dbl(k, P.wv.V(n, hw, lw)) : Nat}:
411  +dk1 = Equal.sym(Nat, U.U32Nat.dbl(k, 1n), U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), 1n)), ns.dnj(n, k, 1n, h1))
412  +l3a = P.wn.le_rw2(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), 1n)), U.U32Nat.dbl(k, 1n), dk1, Equal.trans(Bool, Nat.is_le(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), 1n))), Nat.is_le(1n, U.U32Nat.dbl(Nat.sub(k, n), 1n)), True{}, UL.dbl_le(n, 1n, U.U32Nat.dbl(Nat.sub(k, n), 1n)), UL.nat_le_dbl(Nat.sub(k, n), 1n)))
413  +l3 = Equal.trans(Bool, Nat.is_le(P.wv.Q(n, 1n), U.U32Nat.dbl(n, U.U32Nat.dbl(k, 1n))), Nat.is_le(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(k, 1n)), True{}, UL.dbl_le(n, U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(k, 1n)), l3a)
414  +l4 = UO.nat_lt_le_trans(U.U32Nat.dbl(n, U.U32Nat.dbl(k, Word.to_nat(n, hw))), P.wv.Q(n, 1n), U.U32Nat.dbl(n, U.U32Nat.dbl(k, 1n)), ws.hb(n, k, hw, lw, ch, cl, h), l3)
415  +l5 = Equal.trans(Bool, Nat.is_lt(U.U32Nat.dbl(k, Word.to_nat(n, hw)), U.U32Nat.dbl(k, 1n)), Nat.is_lt(U.U32Nat.dbl(n, U.U32Nat.dbl(k, Word.to_nat(n, hw))), U.U32Nat.dbl(n, U.U32Nat.dbl(k, 1n))), True{}, Equal.sym(Bool, Nat.is_lt(U.U32Nat.dbl(n, U.U32Nat.dbl(k, Word.to_nat(n, hw))), U.U32Nat.dbl(n, U.U32Nat.dbl(k, 1n))), Nat.is_lt(U.U32Nat.dbl(k, Word.to_nat(n, hw)), U.U32Nat.dbl(k, 1n)), UL.dbl_lt(n, U.U32Nat.dbl(k, Word.to_nat(n, hw)), U.U32Nat.dbl(k, 1n))), l4)
416  +l6 = Equal.trans(Bool, Nat.is_lt(Word.to_nat(n, hw), 1n), Nat.is_lt(U.U32Nat.dbl(k, Word.to_nat(n, hw)), U.U32Nat.dbl(k, 1n)), True{}, Equal.sym(Bool, Nat.is_lt(U.U32Nat.dbl(k, Word.to_nat(n, hw)), U.U32Nat.dbl(k, 1n)), Nat.is_lt(Word.to_nat(n, hw), 1n), UL.dbl_lt(k, Word.to_nat(n, hw), 1n)), l5)
417  +eh = ns.lt_one(Word.to_nat(n, hw), l6)
418  +eal = Equal.trans(Nat, P.wv.V(n, hw, lw), Nat.add(Word.to_nat(n, lw), U.U32Nat.dbl(n, 0n)), Word.to_nat(n, lw), Equal.cong(Nat, Nat, v => Nat.add(Word.to_nat(n, lw), U.U32Nat.dbl(n, v)), Word.to_nat(n, hw), 0n, eh), ns.d0(n, Word.to_nat(n, lw)))
419  +hc = P.wv.val_lt2(n, Word.to_nat(n, cl), Word.to_nat(n, ch), UL.word_value_lt(n, cl), UL.word_value_lt(n, ch))
420  +m1 = P.wn.lt_rw(U.U32Nat.dbl(k, P.wv.V(n, hw, lw)), U.U32Nat.dbl(k, Word.to_nat(n, lw)), P.wv.Q(n, 1n), Equal.cong(Nat, Nat, v => U.U32Nat.dbl(k, v), P.wv.V(n, hw, lw), Word.to_nat(n, lw), eal), UO.nat_le_lt_trans(U.U32Nat.dbl(k, P.wv.V(n, hw, lw)), P.wv.V(n, ch, cl), P.wv.Q(n, 1n), h, hc))
421  +m2 = P.wn.lt_rw(U.U32Nat.dbl(k, Word.to_nat(n, lw)), U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw))), P.wv.Q(n, 1n), ns.dnj(n, k, Word.to_nat(n, lw), h1), m1)
422  +m3 = Equal.trans(Bool, Nat.is_lt(U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw)), U.U32Nat.dbl(n, 1n)), Nat.is_lt(U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw))), U.U32Nat.dbl(n, U.U32Nat.dbl(n, 1n))), True{}, Equal.sym(Bool, Nat.is_lt(U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw))), U.U32Nat.dbl(n, U.U32Nat.dbl(n, 1n))), Nat.is_lt(U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw)), U.U32Nat.dbl(n, 1n)), UL.dbl_lt(n, U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw)), U.U32Nat.dbl(n, 1n))), m2)
423  +exj = ws.uniq(n, ws.ov(n, Nat.sub(k, n), lw), 0n, Word.to_nat(n, ws.shl(n, Nat.sub(k, n), lw)), U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw)), Equal.trans(Nat, Nat.add(Word.to_nat(n, ws.shl(n, Nat.sub(k, n), lw)), U.U32Nat.dbl(n, ws.ov(n, Nat.sub(k, n), lw))), U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw)), Nat.add(U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw)), U.U32Nat.dbl(n, 0n)), ws.shlk(n, Nat.sub(k, n), lw), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw)), U.U32Nat.dbl(n, 0n)), U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw)), ns.d0(n, U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw))))), UL.word_value_lt(n, ws.shl(n, Nat.sub(k, n), lw)), m3)
424  Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.zero(n)), U.U32Nat.dbl(n, Word.to_nat(n, ws.shl(n, Nat.sub(k, n), lw)))), Nat.add(0n, U.U32Nat.dbl(n, Word.to_nat(n, ws.shl(n, Nat.sub(k, n), lw)))), U.U32Nat.dbl(k, P.wv.V(n, hw, lw)), Equal.cong(Nat, Nat, v => Nat.add(v, U.U32Nat.dbl(n, Word.to_nat(n, ws.shl(n, Nat.sub(k, n), lw)))), Word.to_nat(n, Word.zero(n)), 0n, UL.word_zero_value(n)), Equal.trans(Nat, Nat.add(0n, U.U32Nat.dbl(n, Word.to_nat(n, ws.shl(n, Nat.sub(k, n), lw)))), U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw))), U.U32Nat.dbl(k, P.wv.V(n, hw, lw)), Equal.cong(Nat, Nat, v => U.U32Nat.dbl(n, v), Word.to_nat(n, ws.shl(n, Nat.sub(k, n), lw)), U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw)), exj), Equal.trans(Nat, U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw))), U.U32Nat.dbl(k, Word.to_nat(n, lw)), U.U32Nat.dbl(k, P.wv.V(n, hw, lw)), Equal.sym(Nat, U.U32Nat.dbl(k, Word.to_nat(n, lw)), U.U32Nat.dbl(n, U.U32Nat.dbl(Nat.sub(k, n), Word.to_nat(n, lw))), ns.dnj(n, k, Word.to_nat(n, lw), h1)), Equal.cong(Nat, Nat, v => U.U32Nat.dbl(k, v), Word.to_nat(n, lw), P.wv.V(n, hw, lw), Equal.sym(Nat, P.wv.V(n, hw, lw), Word.to_nat(n, lw), eal)))))

Uses (33)

Used by (1)