def t32_c

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

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/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/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW

202def t32_c(+l: U32, +h: U32, +c: Bool, +hc: {U32.is_zero(h) == c : Bool}) -> {SF.rv32(F.tu32_w(WU.U64{l, h}, c)) == SF.pick(Result<&2, &2, NE.NumError, Nat>, c, Done{SW.value(WU.U64{l, h})}, Fail{NE.Overflow{}}) : Result<&2, &2, NE.NumError, Nat>}:
203  match c:
204    case True{}:
205      +h0 = N.eq_from_is_eq(v(h), 0n, Equal.trans(Bool, Nat.is_eq(v(h), 0n), U32.is_zero(h), True{}, Equal.sym(Bool, U32.is_zero(h), Nat.is_eq(v(h), 0n), LW.zero_nat(h)), hc))
206      +e1 = Equal.cong(Nat, Nat, t => Nat.add(v(l), C.shift(32n, t)), v(h), 0n, h0)
207      +e2 = Equal.trans(Nat, SW.value(WU.U64{l, h}), Nat.add(v(l), 0n), v(l), Equal.trans(Nat, SW.value(WU.U64{l, h}), Nat.add(v(l), C.shift(32n, 0n)), Nat.add(v(l), 0n), e1, {==}), N.add_zero(v(l)))
208      Equal.cong(Nat, Result<&2, &2, NE.NumError, Nat>, t => Done{t}, v(l), SW.value(WU.U64{l, h}), Equal.sym(Nat, SW.value(WU.U64{l, h}), v(l), e2))
209    case False{}:
210      {==}