proofs/math/typed/f64addv.bend checks

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

12 imports

import Base
import ./f64round.bend as FR
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 ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ./width.bend as WW
import ./natcmp.bend as NC
import ./f64bits.bend as FB
import ./f64addf.bend as AF

Definitions

def v source · line 18 · raw

@+x:U32 -> Nat

def spec_g source · line 22 · raw

@+a1:Bool -> @+z1:Bool -> @+a2:Bool -> @+z2:Bool -> @+sx:Bool -> @+sy:Bool -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+fin:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

the spec's add with the classification of both operands as Booleans

def pick_same source · line 25 · raw

@+b:Bool -> @+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, b, r, r) == r : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def ff source · line 32 · raw

@+z1:Bool -> @+z2:Bool -> @+sx:Bool -> @+sy:Bool -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+fin:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {spec_g(False{}, z1, False{}, z2, sx, sy, x, y, fin) == fin : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def tf source · line 35 · raw

@+z1:Bool -> @+z2:Bool -> @+sx:Bool -> @+sy:Bool -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+fin:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.nan_or(x, Bool.not(z1)) == spec_g(True{}, z1, False{}, z2, sx, sy, x, y, fin) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def ft source · line 42 · raw

@+z1:Bool -> @+z2:Bool -> @+sx:Bool -> @+sy:Bool -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+fin:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.nan_or(y, Bool.not(z2)) == spec_g(False{}, z1, True{}, z2, sx, sy, x, y, fin) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def tt source · line 49 · raw

@+z1:Bool -> @+z2:Bool -> @+sx:Bool -> @+sy:Bool -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+fin:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Bool.not(Bool.xor(sx, sy)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.nan_or(x, Bool.or(Bool.not(z1), Bool.not(z2))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.nan) == spec_g(True{}, z1, True{}, z2, sx, sy, x, y, fin) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def spec_c source · line 85 · raw

@+xl:U32 -> @+xh:U32 -> @+yl:U32 -> @+yh:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}) == spec_g(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 2047n), Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0n), Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 2047n), Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.add_fin(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh})) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

the spec's add, classified

def lt11 source · line 88 · raw

@+xl:U32 -> @+xh:U32 -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 2047n) == Bool.not(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 2047n)) : Bool}

def ltf source · line 91 · raw

@+xl:U32 -> @+xh:U32 -> @+h:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 2047n) == False{} : Bool} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 2047n) == True{} : Bool}

def add_g source · line 95 · raw

@+xl:U32 -> @+xh:U32 -> @+yl:U32 -> @+yh:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Bool.not(Bool.xor(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.am_case(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), Nat.cmp(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sm_case(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), Nat.cmp(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh})))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

F.add as the SoftFloat case split on the spec's fields

def top_c source · line 103 · raw

@+xl:U32 -> @+xh:U32 -> @+yl:U32 -> @+yh:U32 -> @+a1:Bool -> @+ha1:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 2047n) == a1 : Bool} -> @+a2:Bool -> @+ha2:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 2047n) == a2 : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def add_value source · line 151 · raw

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

def sub_value source · line 156 · raw

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