def wq.shl.go

bend-osdev-word64@0.1.1.0 · PROOF.bend:209

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-word64@0.1.1.0/word64.bend as W
import bend-osdev-word64@0.1.1.0/proof_value.bend as P
import bend-osdev-word64@0.1.1.0/proof_shift.bend as PS

209def wq.shl.go(z: Bool, l32: Bool, l64: Bool, +k: Nat, +hw: Word(32n), +lw: Word(32n), +chw: Word(32n), +clw: Word(32n), ez: {Nat.is_eq(k, 0n) == z : Bool}, e32: {Nat.is_lt(k, 32n) == l32 : Bool}, e64: {Nat.is_lt(k, 64n) == l64 : Bool}, hk: {Nat.is_lt(k, 64n) == True{} : Bool}, +h: {Nat.is_le(U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})), W.W64.to_nat(W.W64{U32{chw}, U32{clw}})) == True{} : Bool}) -> {W.W64.to_nat(W.W64.shl.pick(z, l32, l64, k, W.W64{U32{hw}, U32{lw}})) == U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) : Nat}:
210  match z l32 l64:
211    case True{} _ _:
212      Equal.sym(Nat, U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})), W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), Equal.cong(Nat, Nat, v => U.U32Nat.dbl(v, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})), k, 0n, PS.ns.eq_zero(k, ez)))
213    case False{} True{} _:
214      %Equal.sym(U32, U32.shln(U32{hw}, k), U32{PS.ws.shl(32n, k, hw)}, wq.shln(hw, k)) : {W.W64.to_nat(W.W64{U32.or(_, U32.shrn(U32{lw}, Nat.sub(32n, k))), U32.shln(U32{lw}, k)}) == U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) : Nat}
215      %Equal.sym(U32, U32.shrn(U32{lw}, Nat.sub(32n, k)), U32{PS.ws.shr(32n, Nat.sub(32n, k), lw)}, wq.shrn(lw, Nat.sub(32n, k))) : {W.W64.to_nat(W.W64{U32.or(U32{PS.ws.shl(32n, k, hw)}, _), U32.shln(U32{lw}, k)}) == U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) : Nat}
216      %Equal.sym(U32, U32.shln(U32{lw}, k), U32{PS.ws.shl(32n, k, lw)}, wq.shln(lw, k)) : {W.W64.to_nat(W.W64{U32.or(U32{PS.ws.shl(32n, k, hw)}, U32{PS.ws.shr(32n, Nat.sub(32n, k), lw)}), _}) == U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) : Nat}
217      PS.ws.gshl_lo(32n, k, hw, lw, chw, clw, e32, h)
218    case False{} False{} True{}:
219      %Equal.sym(U32, U32.shln(U32{lw}, Nat.sub(k, 32n)), U32{PS.ws.shl(32n, Nat.sub(k, 32n), lw)}, wq.shln(lw, Nat.sub(k, 32n))) : {W.W64.to_nat(W.W64{_, 0}) == U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) : Nat}
220      PS.ws.gshl_hi(32n, k, hw, lw, chw, clw, PS.ns.le_of_not_lt(k, 32n, e32), h)
221    case False{} False{} False{}:
222      Empty.absurd({W.W64.to_nat(W.W64.shl.pick(False{}, False{}, False{}, k, W.W64{U32{hw}, U32{lw}})) == U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) : Nat}, P.wn.ft(Equal.trans(Bool, False{}, Nat.is_lt(k, 64n), True{}, Equal.sym(Bool, Nat.is_lt(k, 64n), False{}, e64), hk)))