Packed Floating Point Numbers

This is a test module description

structure PackedFloat (exWidth sigWidth : Nat) : Type

A packed floating point number, whose exponent and significand width are encoded at the type level.

• sign : Bool

  Sign bit.

• ex : BitVec exWidth

  Exponent of the packed float.

• sig : BitVec sigWidth

  Significand (mantissa) of the packed float.

instance instDecidableEqPackedFloat {exWidth✝ sigWidth✝ : Nat} : DecidableEq (PackedFloat exWidth✝ sigWidth✝)

Equations

• instDecidableEqPackedFloat = decEqPackedFloat✝

instance instReprPackedFloat {exWidth✝ sigWidth✝ : Nat} : Repr (PackedFloat exWidth✝ sigWidth✝)

Equations

• instReprPackedFloat = { reprPrec := reprPackedFloat✝ }

instance instReprPackedFloat_1 {exWidth sigWidth : Nat} : Repr (PackedFloat exWidth sigWidth)

Equations

• One or more equations did not get rendered due to their size.

structure FixedPoint (width exOffset : Nat) : Type

A fixed point number with specified exponent offset.

• sign : Bool
• val : BitVec width
• hExOffset : exOffset < width

instance instDecidableEqFixedPoint {width✝ exOffset✝ : Nat} : DecidableEq (FixedPoint width✝ exOffset✝)

Equations

• instDecidableEqFixedPoint = decEqFixedPoint✝

instance instReprFixedPoint {width ExOffset : Nat} : Repr (FixedPoint width ExOffset)

Equations

• One or more equations did not get rendered due to their size.

inductive State : Type

The "state" of an extended fixed-point number: either NaN, infinity, or a number.

• NaN : State
• Infinity : State
• Number : State

instance instDecidableEqState : DecidableEq State

Equations

• instDecidableEqState x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance instReprState : Repr State

Equations

• One or more equations did not get rendered due to their size.

structure EFixedPoint (width exOffset : Nat) : Type

A fixed point number extended with infinity and NaN.

• state : State
• num : FixedPoint width exOffset

instance instDecidableEqEFixedPoint {width✝ exOffset✝ : Nat} : DecidableEq (EFixedPoint width✝ exOffset✝)

Equations

• instDecidableEqEFixedPoint = decEqEFixedPoint✝

instance instReprEFixedPoint {width✝ exOffset✝ : Nat} : Repr (EFixedPoint width✝ exOffset✝)

Equations

• instReprEFixedPoint = { reprPrec := reprEFixedPoint✝ }

def FixedPoint.equal {w e : Nat} (a b : FixedPoint w e) : Bool

Equations

• a.equal b = (a.val == 0#w && b.val == 0#w || a.sign == b.sign && a.val == b.val)

theorem FixedPoint.injEq {w e : Nat} (a b : FixedPoint w e) : (a = b) = (a.sign = b.sign ∧ a.val = b.val)

theorem FixedPoint.inj {w e : Nat} (a b : FixedPoint w e) : a.sign = b.sign ∧ a.val = b.val → a = b

theorem FixedPoint.equal_refl {w e : Nat} (a : FixedPoint w e) : a.equal a = true

theorem FixedPoint.equal_comm {w e : Nat} (a b : FixedPoint w e) : a.equal b = b.equal a

def FixedPoint.expand {w e : Nat} (a : FixedPoint w e) (w' e' : Nat) (he : e' ≥ e) (hw : w' + e ≥ w + e') : FixedPoint w' e'

Equations

• a.expand w' e' he hw = { sign := a.sign, val := BitVec.setWidth' ⋯ a.val <<< (e' - e), hExOffset := ⋯ }

theorem EFixedPoint.injEq {w e : Nat} (a b : EFixedPoint w e) : (a = b) = (a.state = b.state ∧ a.num.sign = b.num.sign ∧ a.num.val = b.num.val)

theorem EFixedPoint.inj {w e : Nat} (a b : EFixedPoint w e) : a.state = b.state ∧ a.num.sign = b.num.sign ∧ a.num.val = b.num.val → a = b

def EFixedPoint.getNaN {sigWidth exWidth : Nat} (hExOffset : sigWidth < exWidth) : EFixedPoint exWidth sigWidth

Equations

• EFixedPoint.getNaN hExOffset = { state := State.NaN, num := { sign := decide False, val := 0, hExOffset := hExOffset } }

def EFixedPoint.getInfinity {sigWidth exWidth : Nat} (sign : Bool) (hExOffset : sigWidth < exWidth) : EFixedPoint exWidth sigWidth

Equations

• EFixedPoint.getInfinity sign hExOffset = { state := State.Infinity, num := { sign := sign, val := 0, hExOffset := hExOffset } }

def EFixedPoint.zero {sigWidth exWidth : Nat} (hExOffset : sigWidth < exWidth) : EFixedPoint exWidth sigWidth

Equations

• EFixedPoint.zero hExOffset = { state := State.Number, num := { sign := decide False, val := 0, hExOffset := hExOffset } }

def EFixedPoint.equal {w e : Nat} (a b : EFixedPoint w e) : Bool

Floating point equality test. Recall that NaN ≠ Nan under the floating point semantics.

Equations

• One or more equations did not get rendered due to their size.

def EFixedPoint.equal_or_nan {w e : Nat} (a b : EFixedPoint w e) : Bool

Equations

• a.equal_or_nan b = (decide (a.state = State.NaN) || decide (b.state = State.NaN) || a.equal b)

def EFixedPoint.equal_denotation {w e : Nat} (a b : EFixedPoint w e) : Bool

Floating point equality test, where we check up to denotation. So, under this definition:

• NaN = Nan iff the states are both Nan.
• +Infinity = +Infinity, -Infinity = -Infinity.
• Number equality is reflexive.

Equations

• One or more equations did not get rendered due to their size.

def EFixedPoint.isNaN {w e : Nat} (a : EFixedPoint w e) : Bool

Equations

• a.isNaN = decide (a.state = State.NaN)

def EFixedPoint.isZero {w e : Nat} (a : EFixedPoint w e) : Bool

Equations

• a.isZero = (decide (a.state = State.Number) && a.num.val == 0)

def EFixedPoint.expand {w e : Nat} (a : EFixedPoint w e) (w' e' : Nat) (he : e' ≥ e) (hw : w' + e ≥ w + e') : EFixedPoint w' e'

Equations

• a.expand w' e' he hw = { state := a.state, num := a.num.expand w' e' he hw }

def PackedFloat.getNaN (exWidth sigWidth : Nat) : PackedFloat exWidth sigWidth

Returns the "canonical" NaN for the given floating point format. For example, the canonical NaN for exWidth = 3 and sigWidth = 4 is 0.111.1000.

Equations

• PackedFloat.getNaN exWidth sigWidth = { sign := decide False, ex := BitVec.allOnes exWidth, sig := BitVec.ofNat sigWidth (2 ^ (sigWidth - 1)) }

def PackedFloat.getInfinity (exWidth sigWidth : Nat) (sign : Bool) : PackedFloat exWidth sigWidth

Returns the infinity value of the specified sign for the given floating point format.

Equations

• PackedFloat.getInfinity exWidth sigWidth sign = { sign := sign, ex := BitVec.allOnes exWidth, sig := 0 }

def PackedFloat.getZero (exWidth sigWidth : Nat) : PackedFloat exWidth sigWidth

Returns the (positive) zero value for the given floating point format.

Equations

• PackedFloat.getZero exWidth sigWidth = { sign := decide False, ex := 0, sig := 0 }

def PackedFloat.getMax (exWidth sigWidth : Nat) (sign : Bool) : PackedFloat exWidth sigWidth

Returns the maximum (magnitude) value for the given sign.

Equations

• PackedFloat.getMax exWidth sigWidth sign = { sign := sign, ex := BitVec.allOnes exWidth - 1, sig := BitVec.allOnes sigWidth }

theorem PackedFloat.injEq {e s : Nat} (a b : PackedFloat e s) : (a = b) = (a.sign = b.sign ∧ a.ex = b.ex ∧ a.sig = b.sig)

theorem PackedFloat.inj {e s : Nat} (a b : PackedFloat e s) : a.sign = b.sign ∧ a.ex = b.ex ∧ a.sig = b.sig → a = b

def PackedFloat.isInfinite {e s : Nat} (pf : PackedFloat e s) : Bool

Equations

• pf.isInfinite = (pf.ex == BitVec.allOnes e && pf.sig == 0)

def PackedFloat.isNaN {e s : Nat} (pf : PackedFloat e s) : Bool

Equations

• pf.isNaN = (pf.ex == BitVec.allOnes e && pf.sig != 0)

def PackedFloat.isNormOrSubnorm {e s : Nat} (pf : PackedFloat e s) : Bool

Equations

• pf.isNormOrSubnorm = (pf.ex != BitVec.allOnes e)

def PackedFloat.isZeroOrSubnorm {e s : Nat} (pf : PackedFloat e s) : Bool

Equations

• pf.isZeroOrSubnorm = (pf.ex == 0)

def PackedFloat.isZero {e s : Nat} (pf : PackedFloat e s) : Bool

Equations

• pf.isZero = (pf.ex == 0 && pf.sig == 0)

def PackedFloat.isNZero {e s : Nat} (pf : PackedFloat e s) : Bool

Equations

• pf.isNZero = (pf.ex == 0 && pf.sig == 0 && pf.sign)

def PackedFloat.isPZero {e s : Nat} (pf : PackedFloat e s) : Bool

Equations

• pf.isPZero = (pf.ex == 0 && pf.sig == 0 && !pf.sign)

def PackedFloat.isSignMinus {e s : Nat} (pf : PackedFloat e s) : Bool

Equations

• pf.isSignMinus = pf.sign

def PackedFloat.ofBits (e s : Nat) (b : BitVec (1 + e + s)) : PackedFloat e s

Returns the PackedFloat representation for the given BitVec.

Equations

• PackedFloat.ofBits e s b = { sign := b.msb, ex := BitVec.truncate e (b >>> s), sig := BitVec.truncate s b }

def PackedFloat.toBits {e s : Nat} (x : PackedFloat e s) : BitVec (1 + e + s)

Returns the BitVec representation for the given PackedFloat.

Equations

• x.toBits = BitVec.ofBool x.sign ++ x.ex ++ x.sig

def PackedFloat.toEFixed {e s : Nat} (pf : PackedFloat e s) : EFixedPoint (2 ^ e + s) (2 ^ (e - 1) + s - 2)

Convert from a packed float to a fixed point number.

Conversion function assumes IEEE compliance. For output FixedPoint number to have a non-degenerate exponent offset, we need two or more bits in the exponent.

NOTE: Assuming IEEE compliance, you technically only need 2^e + s - 2 bits to cover the entire range of representable values.

Equations

• One or more equations did not get rendered due to their size.

def PackedFloat.equal_denotation {e s : Nat} (a b : PackedFloat e s) : Bool

Equations

• a.equal_denotation b = (a.sign == b.sign && a.ex == b.ex && a.sig == b.sig || a.isNaN && b.isNaN)

theorem PackedFloat.isNumber_of_isNormOrSubnorm {e s : Nat} (a : PackedFloat e s) : a.isNormOrSubnorm = true → a.toEFixed.state = State.Number

def oneE5M2 : PackedFloat 5 2

E5M2 floating point representation of 1.0

Equations

• oneE5M2 = PackedFloat.ofBits 5 2 60#8

def twoE5M2 : PackedFloat 5 2

E5M2 floating point representation of 2.0

Equations

• twoE5M2 = PackedFloat.ofBits 5 2 64#8

def minNormE5M2 : PackedFloat 5 2

Smallest (positive) normal number in E5M2 floating point.

Equations

• minNormE5M2 = PackedFloat.ofBits 5 2 4#8

def minSubnormE5M2 : PackedFloat 5 2

Smallest (positive) subnormal number in E5M2 floating point.

Equations

• minSubnormE5M2 = PackedFloat.ofBits 5 2 1#8