def t32w

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64conv.bend:212

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/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
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/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NE
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW

212def t32w(+w: WU.U64) -> {SF.rv32(F.tu32_w(w, U32.is_zero(X.hi(w)))) == SF.pick(Result<&2, &2, NE.NumError, Nat>, C.fits(32n, SW.value(w)), Done{SW.value(w)}, Fail{NE.Overflow{}}) : Result<&2, &2, NE.NumError, Nat>}:
213  match w:
214    case WU.U64{+l, +h}:
215      +ef = Equal.trans(Bool, U32.is_zero(h), Nat.is_eq(v(h), 0n), C.fits(32n, SW.value(WU.U64{l, h})), LW.zero_nat(h), Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), v(h), C.high(32n, SW.value(WU.U64{l, h})), Equal.sym(Nat, C.high(32n, SW.value(WU.U64{l, h})), v(h), WW.high_u(32n, v(l), v(h), LW.vb(l)))))
216      +e1 = t32_c(l, h, U32.is_zero(h), {==})
217      +e2 = Equal.cong(Bool, Result<&2, &2, NE.NumError, Nat>, b => SF.pick(Result<&2, &2, NE.NumError, Nat>, b, Done{SW.value(WU.U64{l, h})}, Fail{NE.Overflow{}}), U32.is_zero(h), C.fits(32n, SW.value(WU.U64{l, h})), ef)
218      Equal.trans(Result<&2, &2, NE.NumError, Nat>, SF.rv32(F.tu32_w(WU.U64{l, h}, U32.is_zero(h))), SF.pick(Result<&2, &2, NE.NumError, Nat>, U32.is_zero(h), Done{SW.value(WU.U64{l, h})}, Fail{NE.Overflow{}}), SF.pick(Result<&2, &2, NE.NumError, Nat>, C.fits(32n, SW.value(WU.U64{l, h})), Done{SW.value(WU.U64{l, h})}, Fail{NE.Overflow{}}), e1, e2)