def cshl

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fix32.bend:219

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/generic.bend as SG
import bend-collections-laws-math@1.0.0.0/spec/math/fixed.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/fixed.bend as F
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixgen.bend as G

219def cshl(+a: U32, +s: U32, +ok: Bool, +hok: {Nat.is_lt(vs(s), 32n) == ok : Bool}) -> {SF.mval(~U32, ~SG.u32_val, F.opt(U32, Bool.not(U32.is_lt(s, 32)), U32.mul(a, X.pow2(U32.to_nat(U32.and(s, 31)))))) == SF.keep(ok, C.low(32n, C.shift(vs(s), SG.u32_val(a)))) : Maybe<&2, Nat>}:
220  match ok:
221    case True{}:
222      +hb = Equal.trans(Bool, U32.is_lt(s, 32), Nat.is_lt(vs(s), 32n), True{}, lt32(s), hok)
223      +ev = Equal.trans(Nat, SG.u32_val(U32.mul(a, X.pow2(U32.to_nat(U32.and(s, 31))))), SG.u32_val(U32.mul(a, X.pow2(vs(s)))), C.low(32n, C.shift(vs(s), SG.u32_val(a))), Equal.cong(Nat, Nat, t => SG.u32_val(U32.mul(a, X.pow2(t))), U32.to_nat(U32.and(s, 31)), vs(s), am_small(s, hok)), SH.mul_p2(a, vs(s), hok))
224      G.some_of(~U32, ~SG.u32_val, Bool.not(U32.is_lt(s, 32)), G.bnot_eq(U32.is_lt(s, 32), True{}, hb), U32.mul(a, X.pow2(U32.to_nat(U32.and(s, 31)))), C.low(32n, C.shift(vs(s), SG.u32_val(a))), ev)
225    case False{}:
226      +hb = Equal.trans(Bool, U32.is_lt(s, 32), Nat.is_lt(vs(s), 32n), False{}, lt32(s), hok)
227      G.none_of(~U32, ~SG.u32_val, Bool.not(U32.is_lt(s, 32)), G.bnot_eq(U32.is_lt(s, 32), False{}, hb), U32.mul(a, X.pow2(U32.to_nat(U32.and(s, 31)))))