module BinaryFloatModel

import FloatLiteralSpec

-- Exact binary floating arithmetic for the reference lane. A format owns its
-- exponent/fraction widths, bias and rational scale. The operations round once
-- through the maintained literal-rounding specification, preserving subnormals
-- and signed zero. NaN selection is the reference policy (quiet first operand,
-- negative quiet NaN for invalid operations); it is not a hardware attestation.
-- This module is never part of a production device execution path.
-- The admitted reference formats are binary32Format and binary64Format;
-- new widths need their own rational-exponent bound and known-answer rows.
family BinaryFloatFormat : Type 0
constructor BinaryFloatFormatOf
field unrestricted binaryFloatExponentWidth : Nat
field unrestricted binaryFloatFractionWidth : Nat
field unrestricted binaryFloatExponentBias : Nat

end-family

family ModelSigned : Type 0
constructor ModelSignedOf
field unrestricted modelSignedSign : Nat
field unrestricted modelSignedMagnitude : Nat

end-family

def binary32Format =
  (constructor BinaryFloatFormat BinaryFloatFormatOf 8 23 127)

def binary64Format =
  (constructor BinaryFloatFormat BinaryFloatFormatOf 11 52 1023)

def binaryFloatExponentBits =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (eliminate
      BinaryFloatFormat
      (lambda unrestricted value : (family BinaryFloatFormat) . Nat)
      format
      (branch BinaryFloatFormatOf e f b . e)))

def binaryFloatFractionBits =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (eliminate
      BinaryFloatFormat
      (lambda unrestricted value : (family BinaryFloatFormat) . Nat)
      format
      (branch BinaryFloatFormatOf e f b . f)))

def binaryFloatBias =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (eliminate
      BinaryFloatFormat
      (lambda unrestricted value : (family BinaryFloatFormat) . Nat)
      format
      (branch BinaryFloatFormatOf e f b . b)))

def binaryFloatFractionBase =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (specPow2 (binaryFloatFractionBits format)))

def binaryFloatSignBase =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (specPow2 (nat-add (binaryFloatExponentBits format) (binaryFloatFractionBits format))))

def binaryFloatExponentBase =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (specPow2 (binaryFloatExponentBits format)))

def binaryFloatExponentMask =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (nat-subtract (binaryFloatExponentBase format) 1))

def binaryFloatQuietBit =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (nat-divide (binaryFloatFractionBase format) 2))

def binaryFloatInfinityBits =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (nat-multiply (binaryFloatExponentMask format) (binaryFloatFractionBase format)))

def binaryFloatDefaultNaN =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (nat-add
      (binaryFloatSignBase format)
      (nat-add (binaryFloatInfinityBits format) (binaryFloatQuietBit format))))

def binaryFloatDenominator =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (specPow2 (nat-add (binaryFloatBias format) (binaryFloatFractionBits format))))

def binaryFloatProductDenominator =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (nat-multiply (binaryFloatDenominator format) (binaryFloatDenominator format)))

-- A finite significand scaled to this denominator has at most fractionBits
-- + exponentMask bits; an exact product has at most twice that. Include one
-- complete chunk beyond integer division, before the residual bit scan.
def binaryFloatRoundingChunks =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (nat-add
      1
      (nat-divide
        (nat-multiply 2 (nat-add (binaryFloatFractionBits format) (binaryFloatExponentMask format)))
        64)))

-- Signed exact magnitudes are independent of any floating format.
def modelOr =
  (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (specSelect a 1 b)))

def modelAnd =
  (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (specSelect a b 0)))

def modelXor =
  (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (specSelect a (specNot b) b)))

def modelSelectSigned =
  (lambda unrestricted condition : Nat .
    (lambda unrestricted whenTrue : (family ModelSigned) .
      (lambda unrestricted whenFalse : (family ModelSigned) .
        (nat-eliminate
          (lambda unrestricted current : Nat . (family ModelSigned))
          whenFalse
          (lambda unrestricted predecessor : Nat .
            (lambda unrestricted induction : (family ModelSigned) . whenTrue))
          condition))))

def modelSignedScale =
  (lambda unrestricted value : (family ModelSigned) .
    (lambda unrestricted factor : Nat .
      (eliminate
        ModelSigned
        (lambda unrestricted current : (family ModelSigned) . (family ModelSigned))
        value
        (branch
          ModelSignedOf
          sign
          magnitude
          .
          (constructor ModelSigned ModelSignedOf sign (nat-multiply magnitude factor))))))

def modelSumSignedValues =
  (lambda unrestricted a : (family ModelSigned) .
    (lambda unrestricted b : (family ModelSigned) .
      (eliminate
        ModelSigned
        (lambda unrestricted current : (family ModelSigned) . (family ModelSigned))
        a
        (branch
          ModelSignedOf
          signA
          magnitudeA
          .
          (eliminate
            ModelSigned
            (lambda unrestricted current : (family ModelSigned) . (family ModelSigned))
            b
            (branch
              ModelSignedOf
              signB
              magnitudeB
              .
              (modelSelectSigned
                (specEqual signA signB)
                (constructor ModelSigned ModelSignedOf signA (nat-add magnitudeA magnitudeB))
                (modelSelectSigned
                  (nat-less-than magnitudeA magnitudeB)
                  (constructor ModelSigned ModelSignedOf signB (nat-subtract magnitudeB magnitudeA))
                  (constructor
                    ModelSigned
                    ModelSignedOf
                    (specSelect (nat-less-than magnitudeB magnitudeA) signA 0)
                    (nat-subtract magnitudeA magnitudeB))))))))))

def binaryFloatSign =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (lambda unrestricted bits : Nat . (nat-divide bits (binaryFloatSignBase format))))

def binaryFloatExponent =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (lambda unrestricted bits : Nat .
      (nat-modulo
        (nat-divide bits (binaryFloatFractionBase format))
        (binaryFloatExponentBase format))))

def binaryFloatFraction =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (lambda unrestricted bits : Nat . (nat-modulo bits (binaryFloatFractionBase format))))

def binaryFloatMagnitudeBits =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (lambda unrestricted bits : Nat . (nat-modulo bits (binaryFloatSignBase format))))

def binaryFloatExponentAllOnes =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (lambda unrestricted bits : Nat .
      (specEqual (binaryFloatExponent format bits) (binaryFloatExponentMask format))))

def binaryFloatIsNaN =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (lambda unrestricted bits : Nat .
      (modelAnd
        (binaryFloatExponentAllOnes format bits)
        (specNot (specIsZero (binaryFloatFraction format bits))))))

def binaryFloatIsInfinite =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (lambda unrestricted bits : Nat .
      (modelAnd
        (binaryFloatExponentAllOnes format bits)
        (specIsZero (binaryFloatFraction format bits)))))

def binaryFloatIsZero =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (lambda unrestricted bits : Nat . (specIsZero (binaryFloatMagnitudeBits format bits))))

def binaryFloatIsSignalling =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (lambda unrestricted bits : Nat .
      (modelAnd
        (binaryFloatIsNaN format bits)
        (nat-less-than (binaryFloatFraction format bits) (binaryFloatQuietBit format)))))

def binaryFloatZeroOf =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (lambda unrestricted sign : Nat . (nat-multiply sign (binaryFloatSignBase format))))

def binaryFloatInfinityOf =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (lambda unrestricted sign : Nat .
      (nat-add (nat-multiply sign (binaryFloatSignBase format)) (binaryFloatInfinityBits format))))

def binaryFloatQuiet =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (lambda unrestricted bits : Nat .
      (specSelect
        (nat-less-than (binaryFloatFraction format bits) (binaryFloatQuietBit format))
        (nat-add bits (binaryFloatQuietBit format))
        bits)))

def binaryFloatNegate =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (lambda unrestricted bits : Nat .
      (specSelect
        (binaryFloatSign format bits)
        (nat-subtract bits (binaryFloatSignBase format))
        (nat-add bits (binaryFloatSignBase format)))))

def binaryFloatNaNResult =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (lambda unrestricted a : Nat .
      (lambda unrestricted b : Nat .
        (specSelect
          (binaryFloatIsNaN format a)
          (binaryFloatQuiet format a)
          (binaryFloatQuiet format b)))))

def binaryFloatScaledMagnitude =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (lambda unrestricted bits : Nat .
      (specSelect
        (specIsZero (binaryFloatExponent format bits))
        (nat-multiply 2 (binaryFloatFraction format bits))
        (nat-multiply
          (nat-add (binaryFloatFractionBase format) (binaryFloatFraction format bits))
          (specPow2 (binaryFloatExponent format bits))))))

def binaryFloatRoundBitsWithLimit =
  (lambda unrestricted chunks : Nat .
    (lambda unrestricted format : (family BinaryFloatFormat) .
      (lambda unrestricted sign : Nat .
        (lambda unrestricted numerator : Nat .
          (lambda unrestricted denominator : Nat .
            (specSelect
              (specIsZero numerator)
              (binaryFloatZeroOf format sign)
              (eliminate
                SpecResult
                (lambda unrestricted current : (family SpecResult) . Nat)
                (specAssemble
                  (binaryFloatExponentBits format)
                  (binaryFloatFractionBits format)
                  (binaryFloatBias format)
                  sign
                  (specRoundWithLimit
                    chunks
                    (binaryFloatFractionBits format)
                    (binaryFloatBias format)
                    numerator
                    denominator))
                (branch SpecBits n . n)
                (branch SpecOverflow . (binaryFloatInfinityOf format sign)))))))))

def binaryFloatRoundBits =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (binaryFloatRoundBitsWithLimit (binaryFloatRoundingChunks format) format))

def binaryFloatSumSigned =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (lambda unrestricted a : Nat .
      (lambda unrestricted b : Nat .
        (modelSelectSigned
          (specEqual (binaryFloatSign format a) (binaryFloatSign format b))
          (constructor
            ModelSigned
            ModelSignedOf
            (binaryFloatSign format a)
            (nat-add (binaryFloatScaledMagnitude format a) (binaryFloatScaledMagnitude format b)))
          (modelSelectSigned
            (nat-less-than
              (binaryFloatScaledMagnitude format a)
              (binaryFloatScaledMagnitude format b))
            (constructor
              ModelSigned
              ModelSignedOf
              (binaryFloatSign format b)
              (nat-subtract
                (binaryFloatScaledMagnitude format b)
                (binaryFloatScaledMagnitude format a)))
            (constructor
              ModelSigned
              ModelSignedOf
              (specSelect
                (nat-less-than
                  (binaryFloatScaledMagnitude format b)
                  (binaryFloatScaledMagnitude format a))
                (binaryFloatSign format a)
                0)
              (nat-subtract
                (binaryFloatScaledMagnitude format a)
                (binaryFloatScaledMagnitude format b))))))))

def binaryFloatAddFinite =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (lambda unrestricted a : Nat .
      (lambda unrestricted b : Nat .
        (specSelect
          (modelAnd (binaryFloatIsZero format a) (binaryFloatIsZero format b))
          (binaryFloatZeroOf
            format
            (modelAnd (binaryFloatSign format a) (binaryFloatSign format b)))
          (eliminate
            ModelSigned
            (lambda unrestricted current : (family ModelSigned) . Nat)
            (binaryFloatSumSigned format a b)
            (branch
              ModelSignedOf
              sign
              magnitude
              .
              (binaryFloatRoundBits format sign magnitude (binaryFloatDenominator format))))))))

def binaryFloatAdd =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (lambda unrestricted a : Nat .
      (lambda unrestricted b : Nat .
        (specSelect
          (modelOr (binaryFloatIsNaN format a) (binaryFloatIsNaN format b))
          (binaryFloatNaNResult format a b)
          (specSelect
            (binaryFloatIsInfinite format a)
            (specSelect
              (modelAnd
                (binaryFloatIsInfinite format b)
                (specNot (specEqual (binaryFloatSign format a) (binaryFloatSign format b))))
              (binaryFloatDefaultNaN format)
              a)
            (specSelect (binaryFloatIsInfinite format b) b (binaryFloatAddFinite format a b)))))))

def binaryFloatSubtract =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (lambda unrestricted a : Nat .
      (lambda unrestricted b : Nat .
        (specSelect
          (modelOr (binaryFloatIsNaN format a) (binaryFloatIsNaN format b))
          (binaryFloatNaNResult format a b)
          (binaryFloatAdd format a (binaryFloatNegate format b))))))

def binaryFloatMultiply =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (lambda unrestricted a : Nat .
      (lambda unrestricted b : Nat .
        (specSelect
          (modelOr (binaryFloatIsNaN format a) (binaryFloatIsNaN format b))
          (binaryFloatNaNResult format a b)
          (specSelect
            (modelOr
              (modelAnd (binaryFloatIsInfinite format a) (binaryFloatIsZero format b))
              (modelAnd (binaryFloatIsZero format a) (binaryFloatIsInfinite format b)))
            (binaryFloatDefaultNaN format)
            (specSelect
              (modelOr (binaryFloatIsInfinite format a) (binaryFloatIsInfinite format b))
              (binaryFloatInfinityOf
                format
                (modelXor (binaryFloatSign format a) (binaryFloatSign format b)))
              (specSelect
                (modelOr (binaryFloatIsZero format a) (binaryFloatIsZero format b))
                (binaryFloatZeroOf
                  format
                  (modelXor (binaryFloatSign format a) (binaryFloatSign format b)))
                (binaryFloatRoundBits
                  format
                  (modelXor (binaryFloatSign format a) (binaryFloatSign format b))
                  (nat-multiply
                    (binaryFloatScaledMagnitude format a)
                    (binaryFloatScaledMagnitude format b))
                  (binaryFloatProductDenominator format)))))))))

def binaryFloatDivide =
  (lambda unrestricted format : (family BinaryFloatFormat) .
    (lambda unrestricted a : Nat .
      (lambda unrestricted b : Nat .
        (specSelect
          (modelOr (binaryFloatIsNaN format a) (binaryFloatIsNaN format b))
          (binaryFloatNaNResult format a b)
          (specSelect
            (modelOr
              (modelAnd (binaryFloatIsInfinite format a) (binaryFloatIsInfinite format b))
              (modelAnd (binaryFloatIsZero format a) (binaryFloatIsZero format b)))
            (binaryFloatDefaultNaN format)
            (specSelect
              (modelOr (binaryFloatIsInfinite format a) (binaryFloatIsZero format b))
              (binaryFloatInfinityOf
                format
                (modelXor (binaryFloatSign format a) (binaryFloatSign format b)))
              (specSelect
                (modelOr (binaryFloatIsInfinite format b) (binaryFloatIsZero format a))
                (binaryFloatZeroOf
                  format
                  (modelXor (binaryFloatSign format a) (binaryFloatSign format b)))
                (binaryFloatRoundBits
                  format
                  (modelXor (binaryFloatSign format a) (binaryFloatSign format b))
                  (binaryFloatScaledMagnitude format a)
                  (binaryFloatScaledMagnitude format b)))))))))

-- Conversion rounds the exact source rational once. Its scan bound comes from
-- the SOURCE width: using the destination's binary32 bound for a binary64
-- numerator silently loses large exponents. NaN payload mapping is a reference
-- policy; finite device conversion must be qualified separately on silicon.
def binaryFloatConvert =
  (lambda unrestricted source : (family BinaryFloatFormat) .
    (lambda unrestricted destination : (family BinaryFloatFormat) .
      (lambda unrestricted bits : Nat .
        (let unrestricted sign =
          (binaryFloatSign source bits)
          in
          (specSelect
            (binaryFloatIsNaN source bits)
            (binaryFloatQuiet
              destination
              (nat-add
                (binaryFloatInfinityOf destination sign)
                (nat-divide
                  (nat-multiply
                    (binaryFloatFraction source bits)
                    (binaryFloatFractionBase destination))
                  (binaryFloatFractionBase source))))
            (specSelect
              (binaryFloatIsInfinite source bits)
              (binaryFloatInfinityOf destination sign)
              (binaryFloatRoundBitsWithLimit
                (binaryFloatRoundingChunks source)
                destination
                sign
                (binaryFloatScaledMagnitude source bits)
                (binaryFloatDenominator source))))))))