Subnormal Floating-Point Representations

This module defines SubnormRep, the sign/mantissa representation of subnormal floating-point numbers, its rational interpretation, rounding to subnormals, and the validity and error properties of subnormal rounding.

structure SubnormRep (C : FloatCfg) : Type

A sign/mantissa representation of a subnormal floating-point number.

• s : Bool

  The sign bit (true for negative).

• m : ℕ

  The subnormal mantissa.

def SubnormRep.neg {C : FloatCfg} (f : SubnormRep C) : SubnormRep C

Negate a subnormal representation by flipping its sign bit.

Equations

• f.neg = { s := decide ¬f.s = true, m := f.m }

theorem neg_subnorm_involutive {C : FloatCfg} : Function.Involutive SubnormRep.neg

def SubnormRep.nonzero {C : FloatCfg} (f : SubnormRep C) : Prop

A subnormal representation is nonzero when its mantissa is nonzero.

Equations

• f.nonzero = (f.m ≠ 0)

theorem subnorm_neg_nonzero {C : FloatCfg} {f : SubnormRep C} (h : f.nonzero) : f.neg.nonzero

def subnormalToQ {C : FloatCfg} : SubnormRep C → ℚ

The rational value represented by a subnormal representation.

Equations

• subnormalToQ { s := b, m := m } = (if b = true then -1 else 1) * (↑m / ↑C.prec) * 2 ^ C.emin

theorem subnormal_to_q_neg {C : FloatCfg} (s : SubnormRep C) : subnormalToQ s.neg = -subnormalToQ s

theorem subnormal_to_q_nonzero {C : FloatCfg} (s : SubnormRep C) : subnormalToQ s ≠ 0 ↔ s.nonzero

def subnormalRound {C : FloatCfg} (r : IntRounder) (q : ℚ) : SubnormRep C

Round a rational to a subnormal representation using the rounder r.

Equations

• subnormalRound r q = { s := decide (q < 0), m := r (decide (q < 0)) (|q| * 2 ^ (-C.emin) * ↑C.prec) }

theorem neg_subnormal_round {C : FloatCfg} (r : IntRounder) {q : ℚ} (h : q ≠ 0) : subnormalRound r.neg (-q) = (subnormalRound r q).neg

def subnormalRoundDown {C : FloatCfg} (q : ℚ) : SubnormRep C

Round a rational down to a subnormal representation.

Equations

• subnormalRoundDown q = subnormalRound round0 q

theorem subnormal_round_coe {C : FloatCfg} (r : IntRounder) [rh : ValidRounder r] {s : SubnormRep C} (h : s.nonzero) : subnormalRound r (subnormalToQ s) = s

theorem subnormal_round_down_coe {C : FloatCfg} (s : SubnormRep C) (h : s.nonzero) : subnormalRoundDown (subnormalToQ s) = s

theorem subnormal_round_le_of_le {C : FloatCfg} (r : IntRounder) [rh : ValidRounder r] (q1 q2 : ℚ) (h : q1 ≤ q2) : subnormalToQ (subnormalRound r q1) ≤ subnormalToQ (subnormalRound r q2)

theorem subnormal_exp_small {C : FloatCfg} {q : ℚ} (q_nonneg : q ≠ 0) (h : Int.log 2 |q| < C.emin) : |q| * 2 ^ (-C.emin) < 1

def ValidSubnormalRounding {C : FloatCfg} (f : ℚ → SubnormRep C) : Prop

A subnormal rounding map is valid if it never overflows the precision on inputs below the smallest normal magnitude.

Equations

• ValidSubnormalRounding f = ∀ (q : ℚ), q ≠ 0 → Int.log 2 |q| < C.emin → (f q).m ≤ C.prec

theorem subnormal_round_valid {C : FloatCfg} (r : IntRounder) [rh : ValidRounder r] : ValidSubnormalRounding (subnormalRound r)

theorem subnorm_zero {C : FloatCfg} {s : Bool} : subnormalToQ { s := s, m := 0 } = 0

theorem roundsub_zero {C : FloatCfg} (r : IntRounder) [rh : ValidRounder r] : subnormalToQ (subnormalRound r 0) = 0

theorem rounddownsub_le {C : FloatCfg} (q : ℚ) : subnormalToQ (subnormalRound rounddown q) ≤ q

theorem le_roundupsub {C : FloatCfg} (q : ℚ) : q ≤ subnormalToQ (subnormalRound roundup q)

theorem subnormal_up_minus_down {C : FloatCfg} (q : ℚ) : subnormalToQ (subnormalRound roundup q) - subnormalToQ (subnormalRound rounddown q) ≤ 2 ^ C.emin * (↑C.prec)⁻¹

theorem subnormal_round_neg {C : FloatCfg} (r : IntRounder) {q : ℚ} (h : q ≠ 0) : subnormalRound r.neg (-q) = (subnormalRound r q).neg

theorem subnormal_round_eq_up_down {C : FloatCfg} (r : IntRounder) [rh : ValidRounder r] (q : ℚ) : subnormalRound r q = subnormalRound rounddown q ∨ subnormalRound r q = subnormalRound roundup q

theorem subnormal_round_close {C : FloatCfg} (r : IntRounder) [rh : ValidRounder r] (q : ℚ) : |q - subnormalToQ (subnormalRound r q)| ≤ 2 ^ C.emin / ↑C.prec

theorem subnormal_near_close {C : FloatCfg} (q : ℚ) : |q - subnormalToQ (subnormalRound roundnearest q)| ≤ 2 ^ (C.emin - 1) / ↑C.prec