def isqrt_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64isq.bend:152

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/w64.bend as SW
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/natural.bend as M
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/w64sqrt.bend as W64S
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

152def isqrt_c(+l: U32, +h: U32, +z: Bool, +hz: {U32.is_zero(h) == z : Bool}) -> {SW.value(X.isqrt_pick(WU.U64{l, h}, z)) == M.isqrt(SW.value(WU.U64{l, h})) : Nat}:
153  match z:
154    case True{}:
155      +e0 = 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)), hz))
156      +ev = Equal.trans(Nat, SW.value(WU.U64{l, h}), Nat.add(v(l), C.shift(32n, 0n)), v(l), Equal.cong(Nat, Nat, t => Nat.add(v(l), C.shift(32n, t)), v(h), 0n, e0), Equal.trans(Nat, Nat.add(v(l), C.shift(32n, 0n)), Nat.add(v(l), 0n), v(l), Equal.cong(Nat, Nat, t => Nat.add(v(l), t), C.shift(32n, 0n), 0n, WW.shift_zero(32n)), N.add_zero(v(l))))
157      Equal.trans(Nat, SW.value(WU.U64{X.isqrt32(l), 0}), v(X.isqrt32(l)), M.isqrt(SW.value(WU.U64{l, h})), val0(X.isqrt32(l)), Equal.trans(Nat, v(X.isqrt32(l)), M.isqrt(v(l)), M.isqrt(SW.value(WU.U64{l, h})), W64S.isqrt32_value(l), Equal.cong(Nat, Nat, t => M.isqrt(t), v(l), SW.value(WU.U64{l, h}), Equal.sym(Nat, SW.value(WU.U64{l, h}), v(l), ev))))
158    case False{}:
159      big_v(l, h, X.isqrt_est(F32.sqrt(F32.add(F32.mul(U32.to_f32(h), 4294967296.0), U32.to_f32(l)))))