proofs/math/typed/f64bits.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as F64bits

15 imports

import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/f64.bend as SF
import ../../../src/math/f64.bend as F
import ../../../src/math/w64.bend as X
import ../../../src/math/u64.bend as WU
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/lemmas/spec/numeric.bend as S
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../lib/u32.bend as U
import ../../lib/u32div.bend as UD
import ../../lib/word.bend as WD
import ./width.bend as WW
import ./u32laws.bend as LW

Definitions

def v source · line 26 · raw

@+x:U32 -> Nat

def sb source · line 31 · raw

@+k:Nat -> @+x:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.scale_binary(k, x) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, x) : Nat}

def andw source · line 39 · raw

@+n:Nat -> @+k:Nat -> @+w:Word(n) -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(n, Word.and(n, w, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(n, k))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(n, w)) : Nat}

the low k bits of a word

def andm0 source · line 48 · raw

@+x:U32 -> @+k:Nat -> {v(U32.and(x, U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, k)})) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, v(x)) : Nat}

def andm source · line 55 · raw

@+x:U32 -> @+k:Nat -> @+c:U32 -> @+hc:{c == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, k)} : U32} -> {v(U32.and(x, c)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, v(x)) : Nat}

x and c for a mask constant c = 2^k - 1

def pwv source · line 59 · raw

@+k:Nat -> @+hk:{Nat.is_lt(k, 32n) == True{} : Bool} -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+c:U32 -> @+hc:{c == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, k)} : U32} -> {v(c) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, one) : Nat}

the value of a constant c = 2^k

def xstep source · line 64 · raw

@+q:Nat -> @+b:Bool -> @+t:Word(1n+q) -> @+ih:{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(1n+q, Word.xor(1n+q, t, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(1n+q, q))) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(q, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(1n+q, t)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(q, Nat.sub(1n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(q, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(1n+q, t))))) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(2n+q, Word.xor(2n+q, WCon{b, t}, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(2n+q, 1n+q))) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(1n+q, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(2n+q, WCon{b, t})), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(1n+q, Nat.sub(1n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(1n+q, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(2n+q, WCon{b, t}))))) : Nat}

flipping the top bit

def xtop source · line 91 · raw

@+p:Nat -> @+w:Word(1n+p) -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(1n+p, Word.xor(1n+p, w, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(1n+p, p))) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(p, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(1n+p, w)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(p, Nat.sub(1n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(p, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(1n+p, w))))) : Nat}

def astep source · line 107 · raw

@+q:Nat -> @+b:Bool -> @+t:Word(1n+q) -> @+ih:{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(1n+q, Word.and(1n+q, t, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(1n+q, q))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(q, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(1n+q, t))) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(2n+q, Word.and(2n+q, WCon{b, t}, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(2n+q, 1n+q))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(1n+q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(1n+q, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(2n+q, WCon{b, t}))) : Nat}

keeping only the top bit

def atop source · line 120 · raw

@+p:Nat -> @+w:Word(1n+p) -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(1n+p, Word.and(1n+p, w, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(1n+p, p))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(p, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(p, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(1n+p, w))) : Nat}

def le_nlt source · line 137 · raw

@+a:Nat -> @+b:Nat -> {Nat.is_le(a, b) == Bool.not(Nat.is_lt(b, a)) : Bool}

def le_fit source · line 149 · raw

@+k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:Nat -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, one), n) == Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, n)) : Bool}

2^k <= n exactly when n does not fit k bits

def div_sh source · line 155 · raw

@+k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:Nat -> {Nat.div(n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, one)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(k, n) : Nat}

n div 2^k

def z2 source · line 163 · raw

@+a:Nat -> @+k:Nat -> @+b:Nat -> {Nat.is_eq(Nat.add(a, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, b)), 0n) == Bool.and(Nat.is_eq(a, 0n), Nat.is_eq(b, 0n)) : Bool}

def lt_ne source · line 170 · raw

@+a:Nat -> @+m:Nat -> @+h:{Nat.is_lt(a, 1n+m) == True{} : Bool} -> {Nat.is_lt(a, m) == Bool.not(Nat.is_eq(a, m)) : Bool}

def rot3 source · line 181 · raw

@+a:Bool -> @+b:Bool -> @+c:Bool -> {Bool.and(a, Bool.and(b, c)) == Bool.and(c, Bool.and(a, b)) : Bool}

def low_split source · line 201 · raw

@+a:Nat -> @+b:Nat -> @+n:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(Nat.add(a, b), n) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(a, n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(a, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(b, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(a, n)))) : Nat}

the low a + b bits: the low a, then the next b

def ef_g source · line 213 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+h:U32 -> @+c20:U32 -> @+hc20:{c20 == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 20n)} : U32} -> @+m11:U32 -> @+hm11:{m11 == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 11n)} : U32} -> {v(U32.and(U32.div(h, c20), m11)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(11n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(20n, v(h))) : Nat}

the exponent field

def fz_g source · line 221 · raw

@+l:U32 -> @+h:U32 -> @+m20:U32 -> @+hm20:{m20 == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 20n)} : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, U32.and(h, m20)}) == Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{l, h}), 0n) : Bool}

the fraction is zero

def signbit_g source · line 230 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+l:U32 -> @+h:U32 -> @+c:U32 -> @+hc:{c == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 31n)} : U32} -> {Cmp.is_le(U32.cmp(c, h)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{l, h}) : Bool}

def signbit_value source · line 235 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.Signbit.value(x)

def isnan_g source · line 240 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+l:U32 -> @+h:U32 -> @+c20:U32 -> @+hc20:{c20 == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 20n)} : U32} -> @+m11:U32 -> @+hm11:{m11 == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 11n)} : U32} -> @+m20:U32 -> @+hm20:{m20 == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 20n)} : U32} -> {Bool.and(Nat.is_eq(v(U32.and(U32.div(h, c20), m11)), 2047n), Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, U32.and(h, m20)}))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{l, h}) : Bool}

def is_nan_value source · line 247 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.IsNan.value(x)

def isinf_g source · line 252 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+l:U32 -> @+h:U32 -> @+c20:U32 -> @+hc20:{c20 == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 20n)} : U32} -> @+m11:U32 -> @+hm11:{m11 == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 11n)} : U32} -> @+m20:U32 -> @+hm20:{m20 == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 20n)} : U32} -> {Bool.and(Nat.is_eq(v(U32.and(U32.div(h, c20), m11)), 2047n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, U32.and(h, m20)})) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_inf(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{l, h}) : Bool}

def is_inf_value source · line 259 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.IsInf.value(x)

def isfin_g source · line 264 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+l:U32 -> @+h:U32 -> @+c20:U32 -> @+hc20:{c20 == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 20n)} : U32} -> @+m11:U32 -> @+hm11:{m11 == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 11n)} : U32} -> {Nat.is_lt(v(U32.and(U32.div(h, c20), m11)), 2047n) == Bool.not(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{l, h}), 2047n)) : Bool}

def is_finite_value source · line 269 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.IsFinite.value(x)

def iszero_g source · line 274 · raw

@+l:U32 -> @+h:U32 -> @+m31:U32 -> @+hm31:{m31 == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 31n)} : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, U32.and(h, m31)}) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{l, h}) : Bool}

def is_zero_value source · line 286 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.IsZero.value(x)

def xorv0 source · line 293 · raw

@+h:U32 -> {v(U32.xor(h, U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 31n)})) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(31n, v(h)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(31n, Nat.sub(1n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(31n, v(h))))) : Nat}

def xorv source · line 300 · raw

@+h:U32 -> @+c:U32 -> @+hc:{c == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 31n)} : U32} -> {v(U32.xor(h, c)) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(31n, v(h)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(31n, Nat.sub(1n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(31n, v(h))))) : Nat}

def andv0 source · line 303 · raw

@+h:U32 -> {v(U32.and(h, U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 31n)})) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(31n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(31n, v(h))) : Nat}

def andv source · line 310 · raw

@+h:U32 -> @+c:U32 -> @+hc:{c == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 31n)} : U32} -> {v(U32.and(h, c)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(31n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(31n, v(h))) : Nat}

def addv source · line 314 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:U32 -> @+b:U32 -> @+h:{Nat.is_lt(Nat.add(v(a), v(b)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one)) == True{} : Bool} -> {v(U32.add(a, b)) == Nat.add(v(a), v(b)) : Nat}

an addition below 2^32 is exact

def half0 source · line 326 · raw

@+h:U32 -> {Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(31n, v(h))), 0n) == True{} : Bool}

the sign bit c of a 32-bit word is 0 or 1

def bit_c source · line 329 · raw

@+c:Nat -> @+h2:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(c), 0n) == True{} : Bool} -> {c == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(Nat.is_eq(c, 0n))) : Nat}

def nbit_c source · line 338 · raw

@+c:Nat -> @+h2:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(c), 0n) == True{} : Bool} -> {Nat.sub(1n, c) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(Bool.not(Nat.is_eq(c, 0n)))) : Nat}

def fold source · line 348 · raw

@+f:Nat -> @+E:Nat -> @+t:Nat -> {Nat.add(Nat.add(f, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(20n, E)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(31n, t)) == Nat.add(f, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(20n, Nat.add(E, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(11n, t)))) : Nat}

f + 2^20 E + 2^31 t is f + 2^20 (E + 2^11 t)

def enc_g source · line 355 · raw

@+l:U32 -> @+h:U32 -> @+s:Bool -> @+y:U32 -> @+hy:{v(y) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(20n, v(h)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(20n, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(11n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(20n, v(h))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(11n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(s))))) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{l, y} == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.encode(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{l, h}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{l, h})) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

a pattern with the fraction and exponent of x and sign s is encode(s, ...)

def neg_g source · line 365 · raw

@+l:U32 -> @+h:U32 -> @+c:U32 -> @+hc:{c == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 31n)} : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{l, U32.xor(h, c)} == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.neg(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{l, h}) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def neg_value source · line 376 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.Neg.value(x)

def abs_g source · line 381 · raw

@+l:U32 -> @+h:U32 -> @+m31:U32 -> @+hm31:{m31 == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 31n)} : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{l, U32.and(h, m31)} == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.encode(False{}, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{l, h}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{l, h})) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def abs_value source · line 389 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.Abs.value(x)

def cs_g source · line 394 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+l:U32 -> @+h:U32 -> @+l2:U32 -> @+h2:U32 -> @+m31:U32 -> @+hm31:{m31 == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 31n)} : U32} -> @+c:U32 -> @+hc:{c == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 31n)} : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{l, U32.add(U32.and(h, m31), U32.and(h2, c))} == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.encode(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{l2, h2}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{l, h}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{l, h})) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def copysign_value source · line 413 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.Copysign.value(x, y)