inductive RoundingMode : Type

Rounding modes used in floating-point calculations.

Available modes:

• RNA: Round to nearest, tiebreak away from zero.
• RNE: Round to nearest, tiebreak to even significand.
• RTN: Round towards negative infinity.
• RTP: Round towards positive infinity.
• RTZ: Round towards zero.

• RNA : RoundingMode
• RNE : RoundingMode
• RTN : RoundingMode
• RTP : RoundingMode
• RTZ : RoundingMode

instance instDecidableEqRoundingMode : DecidableEq RoundingMode

Equations

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

instance instReprRoundingMode : Repr RoundingMode

Equations

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

def fls' {n : Nat} (m : Nat) (b : BitVec n) (hm : n ≤ m) : BitVec m

Equations

• fls' m b_2 hm_2 = 0
• fls' m b_2 hm_2 = if b_2.msb = true then ↑n'.succ else fls' m (BitVec.truncate n' b_2) ⋯

@[irreducible]

def fls_log {n : Nat} (m : Nat) (b : BitVec n) : BitVec n

Equations

• fls_log m b = if m = 0 then 0 else if (b >>> m == 0) = true then fls_log (m / 2) b else BitVec.ofNat n m ||| fls_log (m / 2) (b >>> m)

def fls {n : Nat} (b : BitVec n) : BitVec n

Find the position of the last (most significant) set bit in a BitVec.

Returns zero if BitVec is zero. Otherwise, returns the index starting from 1.

Implemented naively using a fold with $O(n)$ steps.

Equations

• fls b = fls' n b ⋯

def flsLog {n : Nat} (b : BitVec n) : BitVec n

Find the position of the last (most significant) set bit in a BitVec.

Returns zero if BitVec is zero. Otherwise, returns the index starting from 1.

Equations

• flsLog b = if (b == 0) = true then 0 else 1#n + fls_log (lastPowerOfTwo n) b

theorem flsIter_eq_fls (b : BitVec 8) : flsLog b = fls b

flsLog and fls implement the same function.

def truncateRight {n : Nat} (w : Nat) (v : BitVec n) : BitVec w

Gets the first w bits of the bitvector v.

Equations

• truncateRight w v = if hw : n ≤ w then let_fun h := ⋯; h.mp (v ++ 0#(w - n)) else BitVec.truncate w (v >>> (n - w))

def shouldRoundAway {n : Nat} (m : RoundingMode) (sign odd : Bool) (v : BitVec n) : Bool

Equations

• shouldRoundAway RoundingMode.RNE sign odd v = decide (v.msb = true ∧ (BitVec.truncate (n - 1) v ≠ 0 ∨ odd = true))
• shouldRoundAway RoundingMode.RNA sign odd v = v.msb
• shouldRoundAway RoundingMode.RTP sign odd v = decide ((v.msb = true ∨ BitVec.truncate (n - 1) v ≠ 0) ∧ ¬sign = true)
• shouldRoundAway RoundingMode.RTN sign odd v = decide ((v.msb = true ∨ BitVec.truncate (n - 1) v ≠ 0) ∧ sign = true)
• shouldRoundAway RoundingMode.RTZ sign odd v = decide False

def round {width exOffset : Nat} (exWidth sigWidth : Nat) (mode : RoundingMode) (x : EFixedPoint width exOffset) : PackedFloat exWidth sigWidth

Round an extended fixed-point number to its nearest floating point number of the specified format, with the specified rounding mode.

Equations

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

def isExactFloat {width exOffset : Nat} (exWidth sigWidth : Nat) (x : EFixedPoint width exOffset) : Bool

Determine if a fixed-point number has an exact representation in the specified floating-point format.

Equations

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

def roundToInt {e s : Nat} (mode : RoundingMode) (x : PackedFloat e s) : PackedFloat e s

Equations

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

def PackedFloat.ofRat (e s : Nat) (mode : RoundingMode) (num : Int) (den : Nat) : PackedFloat e s

Equations

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

theorem ofRat_one_is_oneE5M2 : PackedFloat.ofRat 5 2 RoundingMode.RNE 1 1 = oneE5M2

theorem ofRat_two_is_twoE5M2 : PackedFloat.ofRat 5 2 RoundingMode.RNE 2 1 = twoE5M2