def small_nat

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

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/w64sh.bend as SH
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as FL
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR

69def small_nat(+s: Bool, +w: WU.U64, +k: Nat) -> {SF.rv64(F.tu_int(s, X.shr(w, k))) == TN(s, C.high(k, SW.value(w))) : Result<&2, &2, NE.NumError, Nat>}:
70  +V = SW.value(w)
71  +H = C.high(k, V)
72  +e1 = tuint_v(s, X.shr(w, k))
73  +e2 = Equal.cong(Nat, Result<&2, &2, NE.NumError, Nat>, n => TS(s, n), SW.value(X.shr(w, k)), H, SH.shr_value(w, k))
74  +hf = Equal.trans(Bool, C.fits(64n, H), C.fits(Nat.add(k, 64n), V), True{}, Equal.sym(Bool, C.fits(Nat.add(k, 64n), V), C.fits(64n, H), FR.fits_hc(k, 64n, V)), SH.fits_mono(64n, Nat.add(k, 64n), V, le_k64(k), FL.vb64(w)))
75  Equal.trans(Result<&2, &2, NE.NumError, Nat>, SF.rv64(F.tu_int(s, X.shr(w, k))), TS(s, SW.value(X.shr(w, k))), TN(s, H), e1, Equal.trans(Result<&2, &2, NE.NumError, Nat>, TS(s, SW.value(X.shr(w, k))), TS(s, H), TN(s, H), e2, tn_fit(s, H, hf)))