1module FloatLiteralSpec
2
3-- The N5 SPECIFICATION of decimal -> IEEE-754 conversion as an .alpha algorithm
4-- over compact naturals (Language & Testing Evolution L12c, PRD 08 N5, NUM-002,
5-- REG-021). Every arithmetic step is one of the L12k compile-time heads
6-- (nat-add / nat-multiply / nat-subtract / nat-divide / nat-modulo) or the core
7-- nat-less-than, so on closed inputs the reference evaluator folds it in
8-- O(digits) per step. This module is a REFERENCE (never in a package root and
9-- never built): a definition holding compile-time arithmetic with open operands
10-- is refused at erasure by design, and this module holds nothing else. It is
11-- evaluated under the draft edition alpha-2027 by debug/float-spec-check.py,
12-- which compares it row by row with reference/numeric/float-literal-kat.tsv
13-- (the exact-rational authority) and with the bootstrap's literal elaboration.
14--
15-- Inputs are naturals only: (negative flag, significand digits, exponent
16-- magnitude, exponent-negative flag) = (-1)^negative x digits x 10^(+-exponent).
17-- Signed binary exponents are carried with the offset specOffset (= 4096) so
18-- every intermediate stays a natural.
19
20-- numerator / denominator of the exact value
21family SpecFraction : Type 0
22constructor SpecFractionOf
23field unrestricted specNumerator : Nat
24field unrestricted specDenominator : Nat
25end-family
26
27-- a counting loop state: the value still being halved, and how many halvings
28family SpecBitState : Type 0
29constructor SpecBitStateOf
30field unrestricted specBitRemaining : Nat
31field unrestricted specBitCount : Nat
32end-family
33
34-- the rounding result: an integer significand and the (offset) exponent
35family SpecRounded : Type 0
36constructor SpecRoundedOf
37field unrestricted specRoundedSignificand : Nat
38field unrestricted specRoundedExponentOffset : Nat
39field unrestricted specRoundedSubnormal : Nat
40end-family
41
42-- the outcome: the bit pattern as a natural, or finite overflow
43family SpecResult : Type 0
44constructor SpecBits
45field unrestricted specBits : Nat
46constructor SpecOverflow
47end-family
48
49def specOffset : Nat = 4096
50
51def specSelect =
52 (lambda unrestricted condition : Nat . (lambda unrestricted whenTrue : Nat . (lambda unrestricted whenFalse : Nat .
53 (nat-eliminate (lambda unrestricted current : Nat . Nat) whenFalse
54 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . whenTrue)) condition))))
55
56def specNot =
57 (lambda unrestricted flag : Nat .
58 (nat-eliminate (lambda unrestricted current : Nat . Nat) 1
59 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . 0)) flag))
60
61-- zero test in O(digits): the eliminator steps a compact literal O(n) by design
62-- (L9), so a big literal is never a nat-eliminate scrutinee here
63def specIsZero =
64 (lambda unrestricted value : Nat . (nat-less-than value 1))
65-- a <= b as a flag (not (b < a))
66
67def specLessOrEqual =
68 (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (specNot (nat-less-than b a))))
69
70-- a == b as a flag (neither is less), O(digits)
71def specEqual =
72 (lambda unrestricted a : Nat . (lambda unrestricted b : Nat .
73 (specSelect (nat-less-than a b) 0 (specNot (nat-less-than b a)))))
74
75-- base^k by k multiplications
76
77def specPower =
78 (lambda unrestricted base : Nat . (lambda unrestricted k : Nat .
79 (nat-eliminate (lambda unrestricted current : Nat . Nat) 1
80 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . (nat-multiply induction base))) k)))
81
82def specPow2 = (specPower 2)
83
84def specPow10 = (specPower 10)
85
86-- Bit length in two levels: strip caller-bounded 64-bit chunks, then at most
87-- 64 single bits. Literal KATs need 20 chunks; exact binary64 products need
88-- a larger, format-derived bound. Each step is O(digits).
89def specChunk : Nat = 18446744073709551616
90def specChunkStep =
91 (lambda unrestricted state : (family SpecBitState) .
92 (eliminate SpecBitState (lambda unrestricted current : (family SpecBitState) . (family SpecBitState)) state
93 (branch SpecBitStateOf remaining count .
94 (nat-eliminate (lambda unrestricted current : Nat . (family SpecBitState))
95 (constructor SpecBitState SpecBitStateOf (nat-divide remaining specChunk) (nat-add count 64))
96 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecBitState) .
97 (constructor SpecBitState SpecBitStateOf remaining count)))
98 (nat-less-than remaining specChunk)))))
99
100def specBitStep =
101 (lambda unrestricted state : (family SpecBitState) .
102 (eliminate SpecBitState (lambda unrestricted current : (family SpecBitState) . (family SpecBitState)) state
103 (branch SpecBitStateOf remaining count .
104 (nat-eliminate (lambda unrestricted current : Nat . (family SpecBitState))
105 (constructor SpecBitState SpecBitStateOf (nat-divide remaining 2) (nat-add count 1))
106 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecBitState) .
107 (constructor SpecBitState SpecBitStateOf remaining count)))
108 (specIsZero remaining)))))
109
110def specBitLengthWithLimit =
111 (lambda unrestricted chunks : Nat . (lambda unrestricted value : Nat .
112 (eliminate SpecBitState (lambda unrestricted current : (family SpecBitState) . Nat)
113 (nat-eliminate (lambda unrestricted current : Nat . (family SpecBitState))
114 (nat-eliminate (lambda unrestricted current : Nat . (family SpecBitState))
115 (constructor SpecBitState SpecBitStateOf value 0)
116 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecBitState) . (specChunkStep induction)))
117 chunks)
118 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecBitState) . (specBitStep induction)))
119 64)
120 (branch SpecBitStateOf remaining count . count))))
121
122def specBitLength = (specBitLengthWithLimit 20)
123
124-- the exact value as a fraction
125
126def specFraction =
127 (lambda unrestricted digits : Nat . (lambda unrestricted exponent : Nat . (lambda unrestricted exponentNegative : Nat .
128 (nat-eliminate (lambda unrestricted current : Nat . (family SpecFraction))
129 (constructor SpecFraction SpecFractionOf (nat-multiply digits (specPow10 exponent)) 1)
130 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecFraction) .
131 (constructor SpecFraction SpecFractionOf digits (specPow10 exponent))))
132 exponentNegative))))
133
134-- is 2^e <= N/M ? with e = eOffset - specOffset (either sign)
135
136def specPowerFits =
137 (lambda unrestricted numerator : Nat . (lambda unrestricted denominator : Nat . (lambda unrestricted eOffset : Nat .
138 (nat-eliminate (lambda unrestricted current : Nat . Nat)
139 (specLessOrEqual denominator (nat-multiply numerator (specPow2 (nat-subtract specOffset eOffset))))
140 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat .
141 (specLessOrEqual (nat-multiply denominator (specPow2 (nat-subtract eOffset specOffset))) numerator)))
142 (specLessOrEqual specOffset eOffset)))))
143
144-- the binade: e with 2^e <= N/M < 2^(e+1), as an offset exponent; the bit-length
145-- guess g = bitlen(N) - bitlen(M) is e or e + 1
146
147def specBinadeOffsetWithLimit =
148 (lambda unrestricted chunks : Nat . (lambda unrestricted numerator : Nat . (lambda unrestricted denominator : Nat .
149 (nat-eliminate (lambda unrestricted current : Nat . Nat)
150 (nat-subtract (nat-add (specBitLengthWithLimit chunks numerator) specOffset) (nat-add (specBitLengthWithLimit chunks denominator) 1))
151 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat .
152 (nat-subtract (nat-add (specBitLengthWithLimit chunks numerator) specOffset) (specBitLengthWithLimit chunks denominator))))
153 (specPowerFits numerator denominator (nat-subtract (nat-add (specBitLengthWithLimit chunks numerator) specOffset) (specBitLengthWithLimit chunks denominator)))))))
154
155def specBinadeOffset = (specBinadeOffsetWithLimit 20)
156
157-- floor(N / M / 2^s) with the remainder tie test, s = sOffset - specOffset (either sign):
158-- q = floor(num'/den'), round up when 2r > den' or (2r == den' and q odd)
159
160def specRoundQuotient =
161 (lambda unrestricted numerator : Nat . (lambda unrestricted denominator : Nat .
162 (nat-add (nat-divide numerator denominator)
163 (specSelect
164 (nat-less-than denominator (nat-multiply 2 (nat-modulo numerator denominator)))
165 1
166 (specSelect
167 (specNot (nat-less-than (nat-multiply 2 (nat-modulo numerator denominator)) denominator))
168 (nat-modulo (nat-divide numerator denominator) 2)
169 0)))))
170
171-- the format: exponent bits, fraction bits, bias
172
173def specRoundScaled =
174 (lambda unrestricted numerator : Nat . (lambda unrestricted denominator : Nat . (lambda unrestricted sOffset : Nat .
175 (nat-eliminate (lambda unrestricted current : Nat . Nat)
176 (specRoundQuotient (nat-multiply numerator (specPow2 (nat-subtract specOffset sOffset))) denominator)
177 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat .
178 (specRoundQuotient numerator (nat-multiply denominator (specPow2 (nat-subtract sOffset specOffset))))))
179 (specLessOrEqual specOffset sOffset)))))
180
181def specAssembleField =
182 (lambda unrestricted exponentBits : Nat . (lambda unrestricted fractionBits : Nat . (lambda unrestricted negative : Nat .
183 (lambda unrestricted q : Nat . (lambda unrestricted expField : Nat .
184 (nat-eliminate (lambda unrestricted current : Nat . (family SpecResult))
185 (constructor SpecResult SpecBits
186 (nat-add (nat-multiply negative (specPow2 (nat-add exponentBits fractionBits)))
187 (nat-add (nat-multiply expField (specPow2 fractionBits)) (nat-subtract q (specPow2 fractionBits)))))
188 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecResult) .
189 (constructor SpecResult SpecOverflow)))
190 (nat-less-than (nat-subtract (specPow2 exponentBits) 2) expField)))))))
191
192def specAssembleNormal =
193 (lambda unrestricted exponentBits : Nat . (lambda unrestricted fractionBits : Nat . (lambda unrestricted bias : Nat . (lambda unrestricted negative : Nat .
194 (lambda unrestricted q : Nat . (lambda unrestricted eOffset : Nat .
195 (specAssembleField exponentBits fractionBits negative
196 (specSelect (specEqual q (specPow2 (nat-add fractionBits 1))) (nat-divide q 2) q)
197 (nat-subtract (nat-add (specSelect (specEqual q (specPow2 (nat-add fractionBits 1))) (nat-add eOffset 1) eOffset) bias) specOffset))))))))
198
199def specAssemble =
200 (lambda unrestricted exponentBits : Nat . (lambda unrestricted fractionBits : Nat . (lambda unrestricted bias : Nat . (lambda unrestricted negative : Nat .
201 (lambda unrestricted rounded : (family SpecRounded) .
202 (eliminate SpecRounded (lambda unrestricted current : (family SpecRounded) . (family SpecResult)) rounded
203 (branch SpecRoundedOf q eOffset subnormal .
204 (nat-eliminate (lambda unrestricted current : Nat . (family SpecResult))
205 (specAssembleNormal exponentBits fractionBits bias negative q eOffset)
206 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecResult) .
207 (constructor SpecResult SpecBits (nat-add (nat-multiply negative (specPow2 (nat-add exponentBits fractionBits))) q))))
208 subnormal))))))))
209-- normal: a significand that rounded up to 2^(fractionBits+1) moves to the next binade;
210-- the exponent field is e + bias = (eOffset + bias) - specOffset, added BEFORE the offset is
211-- removed (a negative e would otherwise saturate to 0 and give the wrong binade: 0.1 read as 1.6);
212-- beyond 2^exponentBits - 2 it is overflow
213
214def specRoundWithLimit =
215 (lambda unrestricted chunks : Nat . (lambda unrestricted fractionBits : Nat . (lambda unrestricted bias : Nat . (lambda unrestricted numerator : Nat . (lambda unrestricted denominator : Nat .
216 (nat-eliminate (lambda unrestricted current : Nat . (family SpecRounded))
217 (constructor SpecRounded SpecRoundedOf
218 (specRoundScaled numerator denominator (nat-subtract (specBinadeOffsetWithLimit chunks numerator denominator) fractionBits))
219 (specBinadeOffsetWithLimit chunks numerator denominator)
220 0)
221 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecRounded) .
222 (constructor SpecRounded SpecRoundedOf
223 (specRoundScaled numerator denominator (nat-subtract (nat-subtract (nat-add specOffset 1) bias) fractionBits))
224 (nat-subtract (nat-add specOffset 1) bias)
225 1)))
226 (nat-less-than (specBinadeOffsetWithLimit chunks numerator denominator) (nat-subtract (nat-add specOffset 1) bias))))))))
227
228def specRound = (specRoundWithLimit 20)
229
230-- assemble the bits, or overflow
231
232def specConvert =
233 (lambda unrestricted exponentBits : Nat . (lambda unrestricted fractionBits : Nat . (lambda unrestricted bias : Nat .
234 (lambda unrestricted negative : Nat . (lambda unrestricted digits : Nat . (lambda unrestricted exponent : Nat . (lambda unrestricted exponentNegative : Nat .
235 (nat-eliminate (lambda unrestricted current : Nat . (family SpecResult))
236 (constructor SpecResult SpecBits (nat-multiply negative (specPow2 (nat-add exponentBits fractionBits))))
237 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecResult) .
238 (eliminate SpecFraction (lambda unrestricted current : (family SpecFraction) . (family SpecResult))
239 (specFraction digits exponent exponentNegative)
240 (branch SpecFractionOf numerator denominator .
241 (specAssemble exponentBits fractionBits bias negative
242 (specRound fractionBits bias numerator denominator))))))
243 (specNot (specIsZero digits))))))))))
244
245-- round to the format: subnormal below the minimum normal exponent (fixed scale)
246
247def specConvertF32 = (specConvert 8 23 127)
248
249def specConvertF64 = (specConvert 11 52 1023)
250The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.