ProofShift.ws.gshl_hi: def of bend-osdev-word64@0.1.1.0 Import: import bend-osdev-word64@0.1.1.0/proof_shift.bend as ProofShift Lines 408-424 of bend-osdev-word64@0.1.1.0/proof_shift.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-word64@0.1.1.0/proof_shift.bend&start_line=408&end_line=424 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 # a shift left by n <= k: the high half is the low half shifted by k - n, the # high half's bits all carried out (and 0, if nothing overflows) def 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}: +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)) +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))) +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) +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) +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) +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) +eh = ns.lt_one(Word.to_nat(n, hw), l6) +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))) +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)) +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)) +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) +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) +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) 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): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.to_nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.zero https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=dbl_le https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=dbl_lt https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_le_dbl https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_value_lt https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_zero_value https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS_order.bend&name=nat_le_lt_trans https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS_order.bend&name=nat_lt_le_trans https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.dbl https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_shift.bend&name=ns.d0 https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_shift.bend&name=ns.dnj https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_shift.bend&name=ns.lt_one https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_shift.bend&name=ws.hb https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_shift.bend&name=ws.ov https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_shift.bend&name=ws.shl https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_shift.bend&name=ws.shlk https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_shift.bend&name=ws.uniq https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_value.bend&name=wn.le_rw2 https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_value.bend&name=wn.lt_rw https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_value.bend&name=wv.Q https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_value.bend&name=wv.V https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_value.bend&name=wv.val_lt2