IEEE754.FiniteSpec

module IEEE754.FiniteSpec where

open import IEEE754.Prelude
open import IEEE754.Sign
open import IEEE754.Format
open import IEEE754.BitVec
open import IEEE754.Exact

import Cubical.Data.Int as ℤ
import Cubical.Data.Empty as ⊥
import Cubical.Data.Nat as ℕ
import Cubical.Data.NatPlusOne as ℕ₊₁
import Cubical.Data.Rationals as ℚ

one₊₁ two₊₁ : ℕ₊₁.ℕ₊₁
one₊₁ = ℕ₊₁.1+ 0
two₊₁ = ℕ₊₁.1+ 1

natℚ : ℕ → ℚ.ℚ
natℚ n = ℚ.[ ℤ.pos n / one₊₁ ]

pow2ℚ : ℤ.ℤ → ℚ.ℚ
pow2ℚ (ℤ.pos k) =
  natℚ (2 ^ k)
pow2ℚ (ℤ.negsuc k) =
  ℚ.[ ℤ.pos 1 / powerOfTwoDenominator (suc k) ]

emin : BinaryInterchangeFormat → ℤ.ℤ
emin F = ℤ._ℕ-_ 1 (exponentBias F)

unbiasedExponent :
  (F : BinaryInterchangeFormat) →
  BitVec (exponentWidth F) →
  ℤ.ℤ
unbiasedExponent F exponent =
  ℤ._ℕ-_ (bitsToℕ exponent) (exponentBias F)

fractionShift : BinaryInterchangeFormat → ℤ.ℤ
fractionShift F = ℤ.neg (trailingSignificandBits F)

fractionNumerator :
  ∀ {F} →
  BitVec (trailingSignificandBits F) →
  ℕ
fractionNumerator {F} trailing = bitsToℕ trailing

normalNumerator :
  ∀ {F} →
  BitVec (trailingSignificandBits F) →
  ℕ
normalNumerator {F} trailing = normalSignificand {F = F} trailing

natℚ-mul : (m n : ℕ) → natℚ m ℚ.· natℚ n ≡ natℚ (m · n)
natℚ-mul m n i =
  ℚ.[ sym (ℤ.pos·pos m n) i / one₊₁ ]

scaleNatByPowerOfTwo-zero :
  (n : ℕ) →
  scaleNatByPowerOfTwo n (ℤ.pos zero) ≡ natℚ n
scaleNatByPowerOfTwo-zero n i =
  ℚ.[ ℤ.pos (ℕ.·-identityʳ n i) / one₊₁ ]

double-numerator :
  (coefficient exponent : ℕ) →
  ℤ.pos coefficient ℤ.· ℤ.pos (2 ^ suc exponent) ≡
  ℤ.pos 2 ℤ.· (ℤ.pos coefficient ℤ.· ℤ.pos (2 ^ exponent))
double-numerator coefficient exponent =
  cong
    (ℤ.pos coefficient ℤ.·_)
    (ℤ.pos·pos 2 (2 ^ exponent))
  ∙ ℤ.·Assoc
      (ℤ.pos coefficient)
      (ℤ.pos 2)
      (ℤ.pos (2 ^ exponent))
  ∙ cong
      (λ q → q ℤ.· ℤ.pos (2 ^ exponent))
      (ℤ.·Comm (ℤ.pos coefficient) (ℤ.pos 2))
  ∙ sym
      (ℤ.·Assoc
        (ℤ.pos 2)
        (ℤ.pos coefficient)
        (ℤ.pos (2 ^ exponent)))

scaleNatByPowerOfTwo-product :
  (n : ℕ) →
  (e : ℤ.ℤ) →
  natℚ n ℚ.· pow2ℚ e ≡ scaleNatByPowerOfTwo n e
scaleNatByPowerOfTwo-product n (ℤ.pos k) =
  natℚ-mul n (2 ^ k)
scaleNatByPowerOfTwo-product n (ℤ.negsuc k) =
  (λ i →
    ℚ.[ ℤ.·Comm (ℤ.pos n) (ℤ.pos 1) i
      / ℕ₊₁.1+ 0 ℕ₊₁.·₊₁ powerOfTwoDenominator (suc k) ])
  ∙ ℚ.·CancelL
      {a = ℤ.pos n}
      {b = powerOfTwoDenominator (suc k)}
      (ℕ₊₁.1+ 0)

pow2ℚ-negative-+ :
  (m n : ℕ) →
  pow2ℚ (ℤ.neg m) ℚ.· pow2ℚ (ℤ.neg n) ≡
  pow2ℚ (ℤ.neg (m + n))
pow2ℚ-negative-+ zero n =
  ℚ.·IdL (pow2ℚ (ℤ.neg n))
pow2ℚ-negative-+ (suc m) zero =
  ℚ.·IdR (pow2ℚ (ℤ.neg (suc m)))
  ∙ (λ i → pow2ℚ (ℤ.neg (sym (ℕ.+-zero (suc m)) i)))
pow2ℚ-negative-+ (suc m) (suc n) i =
  ℚ.[ ℤ.·IdR (ℤ.pos 1) i
    / sym (powerOfTwoDenominator-+ (suc m) (suc n)) i ]

scaleNatByPowerOfTwo-negative-+ :
  (coefficient m n : ℕ) →
  scaleNatByPowerOfTwo coefficient (ℤ.neg m) ℚ.· pow2ℚ (ℤ.neg n) ≡
  scaleNatByPowerOfTwo coefficient (ℤ.neg (m + n))
scaleNatByPowerOfTwo-negative-+ coefficient zero n =
  cong
    (λ q → q ℚ.· pow2ℚ (ℤ.neg n))
    (scaleNatByPowerOfTwo-zero coefficient)
  ∙ scaleNatByPowerOfTwo-product coefficient (ℤ.neg n)
scaleNatByPowerOfTwo-negative-+ coefficient (suc m) zero =
  ℚ.·IdR (scaleNatByPowerOfTwo coefficient (ℤ.neg (suc m)))
  ∙ (λ i →
      scaleNatByPowerOfTwo
        coefficient
        (ℤ.neg (sym (ℕ.+-zero (suc m)) i)))
scaleNatByPowerOfTwo-negative-+ coefficient (suc m) (suc n) i =
  ℚ.[ ℤ.·IdR (ℤ.pos coefficient) i
    / sym (powerOfTwoDenominator-+ (suc m) (suc n)) i ]

scaleNatByPowerOfTwo-cancel-suc-step :
  (coefficient trailingExponent unbiasedExponent : ℕ) →
  scaleNatByPowerOfTwo coefficient (ℤ.neg (suc trailingExponent)) ℚ.·
  pow2ℚ (ℤ.pos (suc unbiasedExponent))
  ≡
  ℚ.[
    ℤ.pos coefficient ℤ.· ℤ.pos (2 ^ unbiasedExponent) /
    powerOfTwoDenominator trailingExponent ℕ₊₁.·₊₁ one₊₁
  ]
scaleNatByPowerOfTwo-cancel-suc-step coefficient trailingExponent unbiasedExponent =
  (λ i →
    ℚ.[ double-numerator coefficient unbiasedExponent i
      / sym
          (ℕ₊₁.·₊₁-assoc
            two₊₁
            (powerOfTwoDenominator trailingExponent)
            one₊₁) i ])
  ∙ ℚ.·CancelL
      {a = ℤ.pos coefficient ℤ.· ℤ.pos (2 ^ unbiasedExponent)}
      {b = powerOfTwoDenominator trailingExponent ℕ₊₁.·₊₁ one₊₁}
      two₊₁

scaleNatByPowerOfTwo-cancel-suc :
  (coefficient trailingExponent unbiasedExponent : ℕ) →
  scaleNatByPowerOfTwo coefficient (ℤ.neg (suc trailingExponent)) ℚ.·
  pow2ℚ (ℤ.pos (suc unbiasedExponent))
  ≡
  scaleNatByPowerOfTwo coefficient (ℤ.neg trailingExponent) ℚ.·
  pow2ℚ (ℤ.pos unbiasedExponent)
scaleNatByPowerOfTwo-cancel-suc coefficient zero unbiasedExponent =
  scaleNatByPowerOfTwo-cancel-suc-step
    coefficient
    zero
    unbiasedExponent
  ∙ sym
      (cong
        (λ q → q ℚ.· pow2ℚ (ℤ.pos unbiasedExponent))
        (scaleNatByPowerOfTwo-zero coefficient))
scaleNatByPowerOfTwo-cancel-suc coefficient (suc trailingExponent) unbiasedExponent =
  scaleNatByPowerOfTwo-cancel-suc-step
    coefficient
    (suc trailingExponent)
    unbiasedExponent

scaleNatByPowerOfTwo-negative-positive :
  (coefficient trailingExponent unbiasedExponent : ℕ) →
  scaleNatByPowerOfTwo coefficient (ℤ.neg trailingExponent) ℚ.·
  pow2ℚ (ℤ.pos unbiasedExponent)
  ≡
  scaleNatByPowerOfTwo coefficient (ℤ._ℕ-_ unbiasedExponent trailingExponent)
scaleNatByPowerOfTwo-negative-positive coefficient zero unbiasedExponent =
  cong
    (λ q → q ℚ.· pow2ℚ (ℤ.pos unbiasedExponent))
    (scaleNatByPowerOfTwo-zero coefficient)
  ∙ scaleNatByPowerOfTwo-product coefficient (ℤ.pos unbiasedExponent)
scaleNatByPowerOfTwo-negative-positive coefficient (suc trailingExponent) zero =
  ℚ.·IdR (scaleNatByPowerOfTwo coefficient (ℤ.neg (suc trailingExponent)))
scaleNatByPowerOfTwo-negative-positive
  coefficient
  (suc trailingExponent)
  (suc unbiasedExponent) =
  scaleNatByPowerOfTwo-cancel-suc
    coefficient
    trailingExponent
    unbiasedExponent
  ∙ scaleNatByPowerOfTwo-negative-positive
      coefficient
      trailingExponent
      unbiasedExponent

zeroℕ-≡neg : (n : ℕ) → ℤ._ℕ-_ 0 n ≡ ℤ.neg n
zeroℕ-≡neg zero = refl
zeroℕ-≡neg (suc n) = refl

abs-zeroℕ- : (n : ℕ) → ℤ.abs (ℤ._ℕ-_ 0 n) ≡ n
abs-zeroℕ- zero = refl
abs-zeroℕ- (suc n) = refl

abs-neg : (n : ℕ) → ℤ.abs (ℤ.neg n) ≡ n
abs-neg zero = refl
abs-neg (suc n) = refl

positive≢neg :
  (n m : ℕ) →
  ℤ.pos (suc n) ≡ ℤ.neg m →
  ⊥.⊥
positive≢neg n zero pos≡neg =
  ℕ.snotz (ℤ.injPos pos≡neg)
positive≢neg n (suc m) pos≡neg =
  ℤ.posNotnegsuc (suc n) m pos≡neg

neg≢pos :
  (n m : ℕ) →
  ℤ.neg n ≡ ℤ.pos (suc m) →
  ⊥.⊥
neg≢pos zero m neg≡pos =
  ℕ.snotz (sym (ℤ.injPos neg≡pos))
neg≢pos (suc n) m neg≡pos =
  ℤ.negsucNotpos n (suc m) neg≡pos

nℕ-n≡0 : (n : ℕ) → ℤ._ℕ-_ n n ≡ ℤ.pos zero
nℕ-n≡0 zero = refl
nℕ-n≡0 (suc n) = nℕ-n≡0 n

nℕ-n+k≡neg : (n k : ℕ) → ℤ._ℕ-_ n (n + k) ≡ ℤ.neg k
nℕ-n+k≡neg zero k = zeroℕ-≡neg k
nℕ-n+k≡neg (suc n) k = nℕ-n+k≡neg n k

subtract-add-from-negative :
  (minuend subtrahend extra deficit : ℕ) →
  ℤ._ℕ-_ minuend subtrahend ≡ ℤ.neg deficit →
  ℤ._ℕ-_ minuend (subtrahend + extra) ≡ ℤ.neg (deficit + extra)
subtract-add-from-negative zero subtrahend extra deficit diff≡neg =
  let
    subtrahend≡deficit =
      sym (abs-zeroℕ- subtrahend)
      ∙ cong ℤ.abs diff≡neg
      ∙ abs-neg deficit
  in
  zeroℕ-≡neg (subtrahend + extra)
  ∙ cong (λ n → ℤ.neg (n + extra)) subtrahend≡deficit
subtract-add-from-negative (suc minuend) zero extra deficit diff≡neg =
  ⊥.rec (positive≢neg minuend deficit diff≡neg)
subtract-add-from-negative
  (suc minuend)
  (suc subtrahend)
  extra
  deficit
  diff≡neg =
  subtract-add-from-negative minuend subtrahend extra deficit diff≡neg

subtract-add-from-positive :
  (minuend subtrahend extra excess : ℕ) →
  ℤ._ℕ-_ minuend subtrahend ≡ ℤ.pos excess →
  ℤ._ℕ-_ minuend (subtrahend + extra) ≡ ℤ._ℕ-_ excess extra
subtract-add-from-positive zero zero extra zero diff≡pos = refl
subtract-add-from-positive zero zero extra (suc excess) diff≡pos =
  ⊥.rec (ℕ.snotz (sym (ℤ.injPos diff≡pos)))
subtract-add-from-positive zero (suc subtrahend) extra zero diff≡pos =
  ⊥.rec (ℤ.negsucNotpos subtrahend 0 diff≡pos)
subtract-add-from-positive zero (suc subtrahend) extra (suc excess) diff≡pos =
  ⊥.rec (neg≢pos (suc subtrahend) excess diff≡pos)
subtract-add-from-positive (suc minuend) zero extra excess diff≡pos =
  let minuend≡excess = ℤ.injPos diff≡pos in
  (λ i → ℤ._ℕ-_ (minuend≡excess i) extra)
subtract-add-from-positive
  (suc minuend)
  (suc subtrahend)
  extra
  excess
  diff≡pos =
  subtract-add-from-positive minuend subtrahend extra excess diff≡pos

subnormalTextbookShift : BinaryInterchangeFormat → ℤ.ℤ
subnormalTextbookShift F =
  ℤ._ℕ-_ 1 (exponentBias F + trailingSignificandBits F)

normalTextbookShift :
  (F : BinaryInterchangeFormat) →
  BitVec (exponentWidth F) →
  ℤ.ℤ
normalTextbookShift F exponent =
  ℤ._ℕ-_ (bitsToℕ exponent)
          (exponentBias F + trailingSignificandBits F)

subnormalTextbookMagnitude :
  ∀ {F} →
  BitVec (trailingSignificandBits F) →
  ℚ.ℚ
subnormalTextbookMagnitude {F} trailing =
  scaleNatByPowerOfTwo
    (fractionNumerator {F = F} trailing)
    (subnormalTextbookShift F)

normalTextbookMagnitude :
  ∀ {F} →
  BitVec (exponentWidth F) →
  BitVec (trailingSignificandBits F) →
  ℚ.ℚ
normalTextbookMagnitude {F} exponent trailing =
  scaleNatByPowerOfTwo
    (normalNumerator {F = F} trailing)
    (normalTextbookShift F exponent)

normalNumerator-is-hidden-bit-plus-fraction :
  ∀ {F} →
  (trailing : BitVec (trailingSignificandBits F)) →
  normalNumerator {F = F} trailing ≡
  (2 ^ trailingSignificandBits F) + fractionNumerator {F = F} trailing
normalNumerator-is-hidden-bit-plus-fraction trailing = refl

trailingFraction :
  ∀ {F} →
  BitVec (trailingSignificandBits F) →
  ℚ.ℚ
trailingFraction {F} trailing =
  natℚ (fractionNumerator {F = F} trailing) ℚ.· pow2ℚ (fractionShift F)

normalCoefficient :
  ∀ {F} →
  BitVec (trailingSignificandBits F) →
  ℚ.ℚ
normalCoefficient {F} trailing =
  natℚ (normalNumerator {F = F} trailing) ℚ.· pow2ℚ (fractionShift F)

record PositiveExponentBias (F : BinaryInterchangeFormat) : Type₀ where
  constructor positive-exponent-bias
  field
    biasTail : ℕ
    bias≡suc : exponentBias F ≡ suc biasTail

positiveBias-emin :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  emin F ≡ ℤ.neg (PositiveExponentBias.biasTail bias)
positiveBias-emin (positive-exponent-bias biasTail bias≡suc) =
  (λ i → ℤ._ℕ-_ 1 (bias≡suc i))
  ∙ zeroℕ-≡neg biasTail

positiveBias-subnormalShift :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  subnormalShift F ≡
  ℤ.neg
    (PositiveExponentBias.biasTail bias + trailingSignificandBits F)
positiveBias-subnormalShift {F} (positive-exponent-bias biasTail bias≡suc) =
  (λ i → ℤ._ℕ-_ 1 (bias≡suc i + trailingSignificandBits F))
  ∙ zeroℕ-≡neg (biasTail + trailingSignificandBits F)

trailingFraction-canonical :
  ∀ {F} →
  (trailing : BitVec (trailingSignificandBits F)) →
  trailingFraction {F = F} trailing ≡
  scaleNatByPowerOfTwo
    (fractionNumerator {F = F} trailing)
    (fractionShift F)
trailingFraction-canonical {F} trailing =
  scaleNatByPowerOfTwo-product
    (fractionNumerator {F = F} trailing)
    (fractionShift F)

normalCoefficient-canonical :
  ∀ {F} →
  (trailing : BitVec (trailingSignificandBits F)) →
  normalCoefficient {F = F} trailing ≡
  scaleNatByPowerOfTwo
    (normalNumerator {F = F} trailing)
    (fractionShift F)
normalCoefficient-canonical {F} trailing =
  scaleNatByPowerOfTwo-product
    (normalNumerator {F = F} trailing)
    (fractionShift F)

unbiasedExponent-zero :
  ∀ {F} →
  {exponent : BitVec (exponentWidth F)} →
  bitsToℕ exponent ≡ exponentBias F →
  unbiasedExponent F exponent ≡ ℤ.pos zero
unbiasedExponent-zero {F} {exponent} exponent≡bias =
  (λ i → ℤ._ℕ-_ (exponent≡bias i) (exponentBias F))
  ∙ nℕ-n≡0 (exponentBias F)

normalShift-zeroUnbiased :
  ∀ {F} →
  {exponent : BitVec (exponentWidth F)} →
  bitsToℕ exponent ≡ exponentBias F →
  normalShift F exponent ≡ ℤ.neg (trailingSignificandBits F)
normalShift-zeroUnbiased {F} {exponent} exponent≡bias =
  (λ i →
    ℤ._ℕ-_
      (exponent≡bias i)
      (exponentBias F + trailingSignificandBits F))
  ∙ nℕ-n+k≡neg (exponentBias F) (trailingSignificandBits F)

normalShift-negativeUnbiased :
  ∀ {F} →
  {exponent : BitVec (exponentWidth F)} →
  (deficit : ℕ) →
  unbiasedExponent F exponent ≡ ℤ.neg deficit →
  normalShift F exponent ≡
  ℤ.neg (deficit + trailingSignificandBits F)
normalShift-negativeUnbiased {F} {exponent} deficit unbiased≡neg =
  subtract-add-from-negative
    (bitsToℕ exponent)
    (exponentBias F)
    (trailingSignificandBits F)
    deficit
    unbiased≡neg

normalShift-positiveUnbiased :
  ∀ {F} →
  {exponent : BitVec (exponentWidth F)} →
  (excess : ℕ) →
  unbiasedExponent F exponent ≡ ℤ.pos excess →
  normalShift F exponent ≡
  ℤ._ℕ-_ excess (trailingSignificandBits F)
normalShift-positiveUnbiased {F} {exponent} excess unbiased≡pos =
  subtract-add-from-positive
    (bitsToℕ exponent)
    (exponentBias F)
    (trailingSignificandBits F)
    excess
    unbiased≡pos

normalMagnitude-positiveUnbiased-textbook-product :
  ∀ {F} →
  (excess : ℕ) →
  (exponent : BitVec (exponentWidth F)) →
  (trailing : BitVec (trailingSignificandBits F)) →
  unbiasedExponent F exponent ≡ ℤ.pos excess →
  normalMagnitude {F = F} exponent trailing ≡
  normalCoefficient {F = F} trailing ℚ.·
  pow2ℚ (unbiasedExponent F exponent)
normalMagnitude-positiveUnbiased-textbook-product
  {F}
  excess
  exponent
  trailing
  unbiased≡pos =
  let
    coefficient = normalNumerator {F = F} trailing
    trailingBits = trailingSignificandBits F
  in
  cong
    (scaleNatByPowerOfTwo coefficient)
    (normalShift-positiveUnbiased
      {F = F}
      {exponent = exponent}
      excess
      unbiased≡pos)
  ∙ sym
      (scaleNatByPowerOfTwo-negative-positive
        coefficient
        trailingBits
        excess)
  ∙ sym
      (cong
        (λ q → q ℚ.· pow2ℚ (ℤ.pos excess))
        (normalCoefficient-canonical {F = F} trailing))
  ∙ cong
      (λ q → normalCoefficient {F = F} trailing ℚ.· q)
      (cong pow2ℚ (sym unbiased≡pos))

normalMagnitude-negativeUnbiased-textbook-product :
  ∀ {F} →
  (deficit : ℕ) →
  (exponent : BitVec (exponentWidth F)) →
  (trailing : BitVec (trailingSignificandBits F)) →
  unbiasedExponent F exponent ≡ ℤ.neg deficit →
  normalMagnitude {F = F} exponent trailing ≡
  normalCoefficient {F = F} trailing ℚ.·
  pow2ℚ (unbiasedExponent F exponent)
normalMagnitude-negativeUnbiased-textbook-product
  {F}
  deficit
  exponent
  trailing
  unbiased≡neg =
  let
    coefficient = normalNumerator {F = F} trailing
    trailingBits = trailingSignificandBits F
  in
  cong
    (scaleNatByPowerOfTwo coefficient)
    (normalShift-negativeUnbiased
      {F = F}
      {exponent = exponent}
      deficit
      unbiased≡neg)
  ∙ cong
      (λ e → scaleNatByPowerOfTwo coefficient (ℤ.neg e))
      (ℕ.+-comm deficit trailingBits)
  ∙ sym
      (scaleNatByPowerOfTwo-negative-+
        coefficient
        trailingBits
        deficit)
  ∙ sym
      (cong
        (λ q → q ℚ.· pow2ℚ (ℤ.neg deficit))
        (normalCoefficient-canonical {F = F} trailing))
  ∙ cong
      (λ q → normalCoefficient {F = F} trailing ℚ.· q)
      (cong pow2ℚ (sym unbiased≡neg))

normalMagnitude-zeroUnbiased-textbook-product :
  ∀ {F} →
  (exponent : BitVec (exponentWidth F)) →
  (trailing : BitVec (trailingSignificandBits F)) →
  bitsToℕ exponent ≡ exponentBias F →
  normalMagnitude {F = F} exponent trailing ≡
  normalCoefficient {F = F} trailing ℚ.·
  pow2ℚ (unbiasedExponent F exponent)
normalMagnitude-zeroUnbiased-textbook-product {F} exponent trailing exponent≡bias =
  let coefficient = normalNumerator {F = F} trailing in
  cong
    (scaleNatByPowerOfTwo coefficient)
    (normalShift-zeroUnbiased {F = F} {exponent = exponent} exponent≡bias)
  ∙ sym (normalCoefficient-canonical {F = F} trailing)
  ∙ sym (ℚ.·IdR (normalCoefficient {F = F} trailing))
  ∙ cong
      (λ q → normalCoefficient {F = F} trailing ℚ.· q)
      (cong
        pow2ℚ
        (sym
          (unbiasedExponent-zero
            {F = F}
            {exponent = exponent}
            exponent≡bias)))

normalMagnitude-textbook-product :
  ∀ {F} →
  (exponent : BitVec (exponentWidth F)) →
  (trailing : BitVec (trailingSignificandBits F)) →
  normalMagnitude {F = F} exponent trailing ≡
  normalCoefficient {F = F} trailing ℚ.·
  pow2ℚ (unbiasedExponent F exponent)
normalMagnitude-textbook-product {F} exponent trailing
  with unbiasedExponent F exponent UsingEq
... | ℤ.pos excess , unbiased≡pos =
  normalMagnitude-positiveUnbiased-textbook-product
    {F = F}
    excess
    exponent
    trailing
    unbiased≡pos
... | ℤ.negsuc deficit , unbiased≡neg =
  normalMagnitude-negativeUnbiased-textbook-product
    {F = F}
    (suc deficit)
    exponent
    trailing
    unbiased≡neg

subnormalMagnitude-textbook-product :
  ∀ {F} →
  (bias : PositiveExponentBias F) →
  (trailing : BitVec (trailingSignificandBits F)) →
  subnormalMagnitude {F = F} trailing ≡
  trailingFraction {F = F} trailing ℚ.· pow2ℚ (emin F)
subnormalMagnitude-textbook-product {F} bias trailing =
  let
    coefficient = fractionNumerator {F = F} trailing
    trailingBits = trailingSignificandBits F
    biasTail = PositiveExponentBias.biasTail bias
  in
  cong
    (scaleNatByPowerOfTwo coefficient)
    (positiveBias-subnormalShift bias)
  ∙ cong
      (λ e → scaleNatByPowerOfTwo coefficient (ℤ.neg e))
      (ℕ.+-comm biasTail trailingBits)
  ∙ sym
      (scaleNatByPowerOfTwo-negative-+
        coefficient
        trailingBits
        biasTail)
  ∙ sym
      (cong
        (λ q → q ℚ.· pow2ℚ (ℤ.neg biasTail))
        (trailingFraction-canonical {F = F} trailing))
  ∙ cong
      (λ q → trailingFraction {F = F} trailing ℚ.· q)
      (cong pow2ℚ (sym (positiveBias-emin bias)))

binary16-positiveExponentBias : PositiveExponentBias binary16
binary16-positiveExponentBias = positive-exponent-bias 14 refl

binary32-positiveExponentBias : PositiveExponentBias binary32
binary32-positiveExponentBias = positive-exponent-bias 126 refl

binary64-positiveExponentBias : PositiveExponentBias binary64
binary64-positiveExponentBias = positive-exponent-bias 1022 refl

binary128-positiveExponentBias : PositiveExponentBias binary128
binary128-positiveExponentBias = positive-exponent-bias 16382 refl

subnormalTextbookShift-agrees :
  (F : BinaryInterchangeFormat) →
  subnormalTextbookShift F ≡ subnormalShift F
subnormalTextbookShift-agrees F = refl

normalTextbookShift-agrees :
  (F : BinaryInterchangeFormat) →
  (exponent : BitVec (exponentWidth F)) →
  normalTextbookShift F exponent ≡ normalShift F exponent
normalTextbookShift-agrees F exponent = refl

subnormalMagnitude-textbook :
  ∀ {F} →
  (trailing : BitVec (trailingSignificandBits F)) →
  subnormalMagnitude {F = F} trailing ≡
  subnormalTextbookMagnitude {F = F} trailing
subnormalMagnitude-textbook trailing = refl

normalMagnitude-textbook :
  ∀ {F} →
  (exponent : BitVec (exponentWidth F)) →
  (trailing : BitVec (trailingSignificandBits F)) →
  normalMagnitude {F = F} exponent trailing ≡
  normalTextbookMagnitude {F = F} exponent trailing
normalMagnitude-textbook exponent trailing = refl