def n3a

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64norm.bend:139

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/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/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

139# the normalized significand has its top bit at 52
140def n3a(+one: Nat, +h1: {one == 1n : Nat}, +ea: Nat, +fa: WU.U64, +E: Nat, +Fr: Nat, +hea: {ea == E : Nat}, +hfa: {SW.value(fa) == Fr : Nat}, +hF: {C.fits(52n, Fr) == True{} : Bool}, +hnz: {Bool.and(Nat.is_eq(E, 0n), Nat.is_eq(Fr, 0n)) == False{} : Bool}) -> {C.fits(53n, SW.value(F.norm_f(ea, fa))) == True{} : Bool}:
141  match ea:
142    case 0n:
143      +ez = ez0(E, hea)
144      +hz = L.subst(Bool, t => {Bool.and(t, Nat.is_eq(Fr, 0n)) == False{} : Bool}, Nat.is_eq(E, 0n), True{}, ez, hnz)
145      L.subst(Nat, z => {C.fits(53n, z) == True{} : Bool}, C.shift(Nat.sub(X.clz(fa), 11n), Fr), SW.value(X.shl(fa, Nat.sub(X.clz(fa), 11n))), Equal.sym(Nat, SW.value(X.shl(fa, Nat.sub(X.clz(fa), 11n))), C.shift(Nat.sub(X.clz(fa), 11n), Fr), sub_val(fa, Fr, hfa, hF, hz)), sub_fit(fa, Fr, hfa, hF, hz))
146    case 1n+ +p:
147      +hFv = L.subst(Nat, z => {C.fits(52n, z) == True{} : Bool}, Fr, SW.value(fa), Equal.sym(Nat, SW.value(fa), Fr, hfa), hF)
148      +f = WW.limbs_fit(52n, 1n, SW.value(fa), one, hFv, L.subst(Nat, z => {C.fits(1n, z) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), {==}))
149      L.subst(Nat, z => {C.fits(53n, z) == True{} : Bool}, Nat.add(SW.value(fa), C.shift(52n, one)), SW.value(X.add(fa, WU.U64{0, 1048576})), Equal.sym(Nat, SW.value(X.add(fa, WU.U64{0, 1048576})), Nat.add(SW.value(fa), C.shift(52n, one)), hid(one, h1, fa, hFv, 1048576, {==})), f)