def wq.shr_le.go

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

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/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

229def wq.shr_le.go(z: Bool, l32: Bool, l64: Bool, +k: Nat, +hw: Word(32n), +lw: 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}) -> {Nat.is_le(U.U32Nat.dbl(k, W.W64.to_nat(W.W64.shr.pick(z, l32, l64, k, W.W64{U32{hw}, U32{lw}}))), W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) == True{} : Bool}:
230  match z l32 l64:
231    case True{} _ _:
232      %Equal.sym(Nat, k, 0n, PS.ns.eq_zero(k, ez)) : {Nat.is_le(U.U32Nat.dbl(_, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})), W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) == True{} : Bool}
233      UL.nat_le_refl(W.W64.to_nat(W.W64{U32{hw}, U32{lw}}))
234    case False{} True{} _:
235      %Equal.sym(U32, U32.shrn(U32{hw}, k), U32{PS.ws.shr(32n, k, hw)}, wq.shrn(hw, k)) : {Nat.is_le(U.U32Nat.dbl(k, W.W64.to_nat(W.W64{_, U32.or(U32.shrn(U32{lw}, k), U32.shln(U32{hw}, Nat.sub(32n, k)))})), W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) == True{} : Bool}
236      %Equal.sym(U32, U32.shrn(U32{lw}, k), U32{PS.ws.shr(32n, k, lw)}, wq.shrn(lw, k)) : {Nat.is_le(U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{PS.ws.shr(32n, k, hw)}, U32.or(_, U32.shln(U32{hw}, Nat.sub(32n, k)))})), W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) == True{} : Bool}
237      %Equal.sym(U32, U32.shln(U32{hw}, Nat.sub(32n, k)), U32{PS.ws.shl(32n, Nat.sub(32n, k), hw)}, wq.shln(hw, Nat.sub(32n, k))) : {Nat.is_le(U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{PS.ws.shr(32n, k, hw)}, U32.or(U32{PS.ws.shr(32n, k, lw)}, _)})), W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) == True{} : Bool}
238      PS.ws.gshr_lo_le(32n, k, hw, lw, e32)
239    case False{} False{} True{}:
240      %Equal.sym(U32, U32.shrn(U32{hw}, Nat.sub(k, 32n)), U32{PS.ws.shr(32n, Nat.sub(k, 32n), hw)}, wq.shrn(hw, Nat.sub(k, 32n))) : {Nat.is_le(U.U32Nat.dbl(k, W.W64.to_nat(W.W64{0, _})), W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) == True{} : Bool}
241      PS.ws.gshr_hi_le(32n, k, hw, lw, PS.ns.le_of_not_lt(k, 32n, e32))
242    case False{} False{} False{}:
243      Empty.absurd({Nat.is_le(U.U32Nat.dbl(k, W.W64.to_nat(W.W64.shr.pick(False{}, False{}, False{}, k, W.W64{U32{hw}, U32{lw}}))), W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) == True{} : Bool}, P.wn.ft(Equal.trans(Bool, False{}, Nat.is_lt(k, 64n), True{}, Equal.sym(Bool, Nat.is_lt(k, 64n), False{}, e64), hk)))