module FloatLiteralSpec

-- The N5 SPECIFICATION of decimal -> IEEE-754 conversion as an .alpha algorithm
-- over compact naturals (Language & Testing Evolution L12c, PRD 08 N5, NUM-002,
-- REG-021). Every arithmetic step is one of the L12k compile-time heads
-- (nat-add / nat-multiply / nat-subtract / nat-divide / nat-modulo) or the core
-- nat-less-than, so on closed inputs the reference evaluator folds it in
-- O(digits) per step. This module is a REFERENCE (never in a package root and
-- never built): a definition holding compile-time arithmetic with open operands
-- is refused at erasure by design, and this module holds nothing else. It is
-- evaluated under the draft edition alpha-2027 by debug/float-spec-check.py,
-- which compares it row by row with reference/numeric/float-literal-kat.tsv
-- (the exact-rational authority) and with the bootstrap's literal elaboration.
--
-- Inputs are naturals only: (negative flag, significand digits, exponent
-- magnitude, exponent-negative flag) = (-1)^negative x digits x 10^(+-exponent).
-- Signed binary exponents are carried with the offset specOffset (= 4096) so
-- every intermediate stays a natural.

-- numerator / denominator of the exact value
family SpecFraction : Type 0
constructor SpecFractionOf
field unrestricted specNumerator : Nat
field unrestricted specDenominator : Nat
end-family

-- a counting loop state: the value still being halved, and how many halvings
family SpecBitState : Type 0
constructor SpecBitStateOf
field unrestricted specBitRemaining : Nat
field unrestricted specBitCount : Nat
end-family

-- the rounding result: an integer significand and the (offset) exponent
family SpecRounded : Type 0
constructor SpecRoundedOf
field unrestricted specRoundedSignificand : Nat
field unrestricted specRoundedExponentOffset : Nat
field unrestricted specRoundedSubnormal : Nat
end-family

-- the outcome: the bit pattern as a natural, or finite overflow
family SpecResult : Type 0
constructor SpecBits
field unrestricted specBits : Nat
constructor SpecOverflow
end-family

def specOffset : Nat = 4096

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

def specNot =
  (lambda unrestricted flag : Nat .
    (nat-eliminate (lambda unrestricted current : Nat . Nat) 1
      (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . 0)) flag))

-- zero test in O(digits): the eliminator steps a compact literal O(n) by design
-- (L9), so a big literal is never a nat-eliminate scrutinee here
def specIsZero =
  (lambda unrestricted value : Nat . (nat-less-than value 1))
-- a <= b  as a flag (not (b < a))

def specLessOrEqual =
  (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (specNot (nat-less-than b a))))

-- a == b as a flag (neither is less), O(digits)
def specEqual =
  (lambda unrestricted a : Nat . (lambda unrestricted b : Nat .
    (specSelect (nat-less-than a b) 0 (specNot (nat-less-than b a)))))

-- base^k by k multiplications

def specPower =
  (lambda unrestricted base : Nat . (lambda unrestricted k : Nat .
    (nat-eliminate (lambda unrestricted current : Nat . Nat) 1
      (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . (nat-multiply induction base))) k)))

def specPow2 = (specPower 2)

def specPow10 = (specPower 10)

-- bit length in two levels: strip 64-bit chunks (at most 20 for the widest KAT
-- magnitude), then single bits (at most 64); each step is O(digits)
def specChunk : Nat = 18446744073709551616
def specChunkStep =
  (lambda unrestricted state : (family SpecBitState) .
    (eliminate SpecBitState (lambda unrestricted current : (family SpecBitState) . (family SpecBitState)) state
      (branch SpecBitStateOf remaining count .
        (nat-eliminate (lambda unrestricted current : Nat . (family SpecBitState))
          (constructor SpecBitState SpecBitStateOf (nat-divide remaining specChunk) (nat-add count 64))
          (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecBitState) .
            (constructor SpecBitState SpecBitStateOf remaining count)))
          (nat-less-than remaining specChunk)))))

def specBitStep =
  (lambda unrestricted state : (family SpecBitState) .
    (eliminate SpecBitState (lambda unrestricted current : (family SpecBitState) . (family SpecBitState)) state
      (branch SpecBitStateOf remaining count .
        (nat-eliminate (lambda unrestricted current : Nat . (family SpecBitState))
          (constructor SpecBitState SpecBitStateOf (nat-divide remaining 2) (nat-add count 1))
          (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecBitState) .
            (constructor SpecBitState SpecBitStateOf remaining count)))
          (specIsZero remaining)))))

def specBitLength =
  (lambda unrestricted value : Nat .
    (eliminate SpecBitState (lambda unrestricted current : (family SpecBitState) . Nat)
      (nat-eliminate (lambda unrestricted current : Nat . (family SpecBitState))
        (nat-eliminate (lambda unrestricted current : Nat . (family SpecBitState))
          (constructor SpecBitState SpecBitStateOf value 0)
          (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecBitState) . (specChunkStep induction)))
          20)
        (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecBitState) . (specBitStep induction)))
        64)
      (branch SpecBitStateOf remaining count . count)))

-- the exact value as a fraction

def specFraction =
  (lambda unrestricted digits : Nat . (lambda unrestricted exponent : Nat . (lambda unrestricted exponentNegative : Nat .
    (nat-eliminate (lambda unrestricted current : Nat . (family SpecFraction))
      (constructor SpecFraction SpecFractionOf (nat-multiply digits (specPow10 exponent)) 1)
      (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecFraction) .
        (constructor SpecFraction SpecFractionOf digits (specPow10 exponent))))
      exponentNegative))))

-- is 2^e <= N/M ?  with e = eOffset - specOffset (either sign)

def specPowerFits =
  (lambda unrestricted numerator : Nat . (lambda unrestricted denominator : Nat . (lambda unrestricted eOffset : Nat .
    (nat-eliminate (lambda unrestricted current : Nat . Nat)
      (specLessOrEqual denominator (nat-multiply numerator (specPow2 (nat-subtract specOffset eOffset))))
      (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat .
        (specLessOrEqual (nat-multiply denominator (specPow2 (nat-subtract eOffset specOffset))) numerator)))
      (specLessOrEqual specOffset eOffset)))))

-- the binade: e with 2^e <= N/M < 2^(e+1), as an offset exponent; the bit-length
-- guess g = bitlen(N) - bitlen(M) is e or e + 1

def specBinadeOffset =
  (lambda unrestricted numerator : Nat . (lambda unrestricted denominator : Nat .
    (nat-eliminate (lambda unrestricted current : Nat . Nat)
      (nat-subtract (nat-add (specBitLength numerator) specOffset) (nat-add (specBitLength denominator) 1))
      (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat .
        (nat-subtract (nat-add (specBitLength numerator) specOffset) (specBitLength denominator))))
      (specPowerFits numerator denominator (nat-subtract (nat-add (specBitLength numerator) specOffset) (specBitLength denominator))))))

-- floor(N / M / 2^s) with the remainder tie test, s = sOffset - specOffset (either sign):
-- q = floor(num'/den'), round up when 2r > den' or (2r == den' and q odd)

def specRoundQuotient =
  (lambda unrestricted numerator : Nat . (lambda unrestricted denominator : Nat .
    (nat-add (nat-divide numerator denominator)
      (specSelect
        (nat-less-than denominator (nat-multiply 2 (nat-modulo numerator denominator)))
        1
        (specSelect
          (specNot (nat-less-than (nat-multiply 2 (nat-modulo numerator denominator)) denominator))
          (nat-modulo (nat-divide numerator denominator) 2)
          0)))))

-- the format: exponent bits, fraction bits, bias

def specRoundScaled =
  (lambda unrestricted numerator : Nat . (lambda unrestricted denominator : Nat . (lambda unrestricted sOffset : Nat .
    (nat-eliminate (lambda unrestricted current : Nat . Nat)
      (specRoundQuotient (nat-multiply numerator (specPow2 (nat-subtract specOffset sOffset))) denominator)
      (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat .
        (specRoundQuotient numerator (nat-multiply denominator (specPow2 (nat-subtract sOffset specOffset))))))
      (specLessOrEqual specOffset sOffset)))))

def specAssembleField =
  (lambda unrestricted exponentBits : Nat . (lambda unrestricted fractionBits : Nat . (lambda unrestricted negative : Nat .
    (lambda unrestricted q : Nat . (lambda unrestricted expField : Nat .
      (nat-eliminate (lambda unrestricted current : Nat . (family SpecResult))
        (constructor SpecResult SpecBits
          (nat-add (nat-multiply negative (specPow2 (nat-add exponentBits fractionBits)))
            (nat-add (nat-multiply expField (specPow2 fractionBits)) (nat-subtract q (specPow2 fractionBits)))))
        (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecResult) .
          (constructor SpecResult SpecOverflow)))
        (nat-less-than (nat-subtract (specPow2 exponentBits) 2) expField)))))))

def specAssembleNormal =
  (lambda unrestricted exponentBits : Nat . (lambda unrestricted fractionBits : Nat . (lambda unrestricted bias : Nat . (lambda unrestricted negative : Nat .
    (lambda unrestricted q : Nat . (lambda unrestricted eOffset : Nat .
      (specAssembleField exponentBits fractionBits negative
        (specSelect (specEqual q (specPow2 (nat-add fractionBits 1))) (nat-divide q 2) q)
        (nat-subtract (nat-add (specSelect (specEqual q (specPow2 (nat-add fractionBits 1))) (nat-add eOffset 1) eOffset) bias) specOffset))))))))

def specAssemble =
  (lambda unrestricted exponentBits : Nat . (lambda unrestricted fractionBits : Nat . (lambda unrestricted bias : Nat . (lambda unrestricted negative : Nat .
    (lambda unrestricted rounded : (family SpecRounded) .
      (eliminate SpecRounded (lambda unrestricted current : (family SpecRounded) . (family SpecResult)) rounded
        (branch SpecRoundedOf q eOffset subnormal .
          (nat-eliminate (lambda unrestricted current : Nat . (family SpecResult))
            (specAssembleNormal exponentBits fractionBits bias negative q eOffset)
            (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecResult) .
              (constructor SpecResult SpecBits (nat-add (nat-multiply negative (specPow2 (nat-add exponentBits fractionBits))) q))))
            subnormal))))))))
-- normal: a significand that rounded up to 2^(fractionBits+1) moves to the next binade;
-- the exponent field is e + bias = (eOffset + bias) - specOffset, added BEFORE the offset is
-- removed (a negative e would otherwise saturate to 0 and give the wrong binade: 0.1 read as 1.6);
-- beyond 2^exponentBits - 2 it is overflow

def specRound =
  (lambda unrestricted fractionBits : Nat . (lambda unrestricted bias : Nat . (lambda unrestricted numerator : Nat . (lambda unrestricted denominator : Nat .
    (nat-eliminate (lambda unrestricted current : Nat . (family SpecRounded))
      (constructor SpecRounded SpecRoundedOf
        (specRoundScaled numerator denominator (nat-subtract (specBinadeOffset numerator denominator) fractionBits))
        (specBinadeOffset numerator denominator)
        0)
      (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecRounded) .
        (constructor SpecRounded SpecRoundedOf
          (specRoundScaled numerator denominator (nat-subtract (nat-subtract (nat-add specOffset 1) bias) fractionBits))
          (nat-subtract (nat-add specOffset 1) bias)
          1)))
      (nat-less-than (specBinadeOffset numerator denominator) (nat-subtract (nat-add specOffset 1) bias)))))))

-- assemble the bits, or overflow

def specConvert =
  (lambda unrestricted exponentBits : Nat . (lambda unrestricted fractionBits : Nat . (lambda unrestricted bias : Nat .
    (lambda unrestricted negative : Nat . (lambda unrestricted digits : Nat . (lambda unrestricted exponent : Nat . (lambda unrestricted exponentNegative : Nat .
      (nat-eliminate (lambda unrestricted current : Nat . (family SpecResult))
        (constructor SpecResult SpecBits (nat-multiply negative (specPow2 (nat-add exponentBits fractionBits))))
        (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecResult) .
          (eliminate SpecFraction (lambda unrestricted current : (family SpecFraction) . (family SpecResult))
            (specFraction digits exponent exponentNegative)
            (branch SpecFractionOf numerator denominator .
              (specAssemble exponentBits fractionBits bias negative
                (specRound fractionBits bias numerator denominator))))))
        (specNot (specIsZero digits))))))))))

-- round to the format: subnormal below the minimum normal exponent (fixed scale)

def specConvertF32 = (specConvert 8 23 127)

def specConvertF64 = (specConvert 11 52 1023)