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 64-bit chunks (at most 20 for the widest KAT
87-- magnitude), then single bits (at most 64); each step is O(digits)
88def specChunk : Nat = 18446744073709551616
89def specChunkStep =
90 (lambda unrestricted state : (family SpecBitState) .
91 (eliminate SpecBitState (lambda unrestricted current : (family SpecBitState) . (family SpecBitState)) state
92 (branch SpecBitStateOf remaining count .
93 (nat-eliminate (lambda unrestricted current : Nat . (family SpecBitState))
94 (constructor SpecBitState SpecBitStateOf (nat-divide remaining specChunk) (nat-add count 64))
95 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecBitState) .
96 (constructor SpecBitState SpecBitStateOf remaining count)))
97 (nat-less-than remaining specChunk)))))
98
99def specBitStep =
100 (lambda unrestricted state : (family SpecBitState) .
101 (eliminate SpecBitState (lambda unrestricted current : (family SpecBitState) . (family SpecBitState)) state
102 (branch SpecBitStateOf remaining count .
103 (nat-eliminate (lambda unrestricted current : Nat . (family SpecBitState))
104 (constructor SpecBitState SpecBitStateOf (nat-divide remaining 2) (nat-add count 1))
105 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecBitState) .
106 (constructor SpecBitState SpecBitStateOf remaining count)))
107 (specIsZero remaining)))))
108
109def specBitLength =
110 (lambda unrestricted value : Nat .
111 (eliminate SpecBitState (lambda unrestricted current : (family SpecBitState) . Nat)
112 (nat-eliminate (lambda unrestricted current : Nat . (family SpecBitState))
113 (nat-eliminate (lambda unrestricted current : Nat . (family SpecBitState))
114 (constructor SpecBitState SpecBitStateOf value 0)
115 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecBitState) . (specChunkStep induction)))
116 20)
117 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecBitState) . (specBitStep induction)))
118 64)
119 (branch SpecBitStateOf remaining count . count)))
120
121-- the exact value as a fraction
122
123def specFraction =
124 (lambda unrestricted digits : Nat . (lambda unrestricted exponent : Nat . (lambda unrestricted exponentNegative : Nat .
125 (nat-eliminate (lambda unrestricted current : Nat . (family SpecFraction))
126 (constructor SpecFraction SpecFractionOf (nat-multiply digits (specPow10 exponent)) 1)
127 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecFraction) .
128 (constructor SpecFraction SpecFractionOf digits (specPow10 exponent))))
129 exponentNegative))))
130
131-- is 2^e <= N/M ? with e = eOffset - specOffset (either sign)
132
133def specPowerFits =
134 (lambda unrestricted numerator : Nat . (lambda unrestricted denominator : Nat . (lambda unrestricted eOffset : Nat .
135 (nat-eliminate (lambda unrestricted current : Nat . Nat)
136 (specLessOrEqual denominator (nat-multiply numerator (specPow2 (nat-subtract specOffset eOffset))))
137 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat .
138 (specLessOrEqual (nat-multiply denominator (specPow2 (nat-subtract eOffset specOffset))) numerator)))
139 (specLessOrEqual specOffset eOffset)))))
140
141-- the binade: e with 2^e <= N/M < 2^(e+1), as an offset exponent; the bit-length
142-- guess g = bitlen(N) - bitlen(M) is e or e + 1
143
144def specBinadeOffset =
145 (lambda unrestricted numerator : Nat . (lambda unrestricted denominator : Nat .
146 (nat-eliminate (lambda unrestricted current : Nat . Nat)
147 (nat-subtract (nat-add (specBitLength numerator) specOffset) (nat-add (specBitLength denominator) 1))
148 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat .
149 (nat-subtract (nat-add (specBitLength numerator) specOffset) (specBitLength denominator))))
150 (specPowerFits numerator denominator (nat-subtract (nat-add (specBitLength numerator) specOffset) (specBitLength denominator))))))
151
152-- floor(N / M / 2^s) with the remainder tie test, s = sOffset - specOffset (either sign):
153-- q = floor(num'/den'), round up when 2r > den' or (2r == den' and q odd)
154
155def specRoundQuotient =
156 (lambda unrestricted numerator : Nat . (lambda unrestricted denominator : Nat .
157 (nat-add (nat-divide numerator denominator)
158 (specSelect
159 (nat-less-than denominator (nat-multiply 2 (nat-modulo numerator denominator)))
160 1
161 (specSelect
162 (specNot (nat-less-than (nat-multiply 2 (nat-modulo numerator denominator)) denominator))
163 (nat-modulo (nat-divide numerator denominator) 2)
164 0)))))
165
166-- the format: exponent bits, fraction bits, bias
167
168def specRoundScaled =
169 (lambda unrestricted numerator : Nat . (lambda unrestricted denominator : Nat . (lambda unrestricted sOffset : Nat .
170 (nat-eliminate (lambda unrestricted current : Nat . Nat)
171 (specRoundQuotient (nat-multiply numerator (specPow2 (nat-subtract specOffset sOffset))) denominator)
172 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat .
173 (specRoundQuotient numerator (nat-multiply denominator (specPow2 (nat-subtract sOffset specOffset))))))
174 (specLessOrEqual specOffset sOffset)))))
175
176def specAssembleField =
177 (lambda unrestricted exponentBits : Nat . (lambda unrestricted fractionBits : Nat . (lambda unrestricted negative : Nat .
178 (lambda unrestricted q : Nat . (lambda unrestricted expField : Nat .
179 (nat-eliminate (lambda unrestricted current : Nat . (family SpecResult))
180 (constructor SpecResult SpecBits
181 (nat-add (nat-multiply negative (specPow2 (nat-add exponentBits fractionBits)))
182 (nat-add (nat-multiply expField (specPow2 fractionBits)) (nat-subtract q (specPow2 fractionBits)))))
183 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecResult) .
184 (constructor SpecResult SpecOverflow)))
185 (nat-less-than (nat-subtract (specPow2 exponentBits) 2) expField)))))))
186
187def specAssembleNormal =
188 (lambda unrestricted exponentBits : Nat . (lambda unrestricted fractionBits : Nat . (lambda unrestricted bias : Nat . (lambda unrestricted negative : Nat .
189 (lambda unrestricted q : Nat . (lambda unrestricted eOffset : Nat .
190 (specAssembleField exponentBits fractionBits negative
191 (specSelect (specEqual q (specPow2 (nat-add fractionBits 1))) (nat-divide q 2) q)
192 (nat-subtract (nat-add (specSelect (specEqual q (specPow2 (nat-add fractionBits 1))) (nat-add eOffset 1) eOffset) bias) specOffset))))))))
193
194def specAssemble =
195 (lambda unrestricted exponentBits : Nat . (lambda unrestricted fractionBits : Nat . (lambda unrestricted bias : Nat . (lambda unrestricted negative : Nat .
196 (lambda unrestricted rounded : (family SpecRounded) .
197 (eliminate SpecRounded (lambda unrestricted current : (family SpecRounded) . (family SpecResult)) rounded
198 (branch SpecRoundedOf q eOffset subnormal .
199 (nat-eliminate (lambda unrestricted current : Nat . (family SpecResult))
200 (specAssembleNormal exponentBits fractionBits bias negative q eOffset)
201 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecResult) .
202 (constructor SpecResult SpecBits (nat-add (nat-multiply negative (specPow2 (nat-add exponentBits fractionBits))) q))))
203 subnormal))))))))
204-- normal: a significand that rounded up to 2^(fractionBits+1) moves to the next binade;
205-- the exponent field is e + bias = (eOffset + bias) - specOffset, added BEFORE the offset is
206-- removed (a negative e would otherwise saturate to 0 and give the wrong binade: 0.1 read as 1.6);
207-- beyond 2^exponentBits - 2 it is overflow
208
209def specRound =
210 (lambda unrestricted fractionBits : Nat . (lambda unrestricted bias : Nat . (lambda unrestricted numerator : Nat . (lambda unrestricted denominator : Nat .
211 (nat-eliminate (lambda unrestricted current : Nat . (family SpecRounded))
212 (constructor SpecRounded SpecRoundedOf
213 (specRoundScaled numerator denominator (nat-subtract (specBinadeOffset numerator denominator) fractionBits))
214 (specBinadeOffset numerator denominator)
215 0)
216 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecRounded) .
217 (constructor SpecRounded SpecRoundedOf
218 (specRoundScaled numerator denominator (nat-subtract (nat-subtract (nat-add specOffset 1) bias) fractionBits))
219 (nat-subtract (nat-add specOffset 1) bias)
220 1)))
221 (nat-less-than (specBinadeOffset numerator denominator) (nat-subtract (nat-add specOffset 1) bias)))))))
222
223-- assemble the bits, or overflow
224
225def specConvert =
226 (lambda unrestricted exponentBits : Nat . (lambda unrestricted fractionBits : Nat . (lambda unrestricted bias : Nat .
227 (lambda unrestricted negative : Nat . (lambda unrestricted digits : Nat . (lambda unrestricted exponent : Nat . (lambda unrestricted exponentNegative : Nat .
228 (nat-eliminate (lambda unrestricted current : Nat . (family SpecResult))
229 (constructor SpecResult SpecBits (nat-multiply negative (specPow2 (nat-add exponentBits fractionBits))))
230 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SpecResult) .
231 (eliminate SpecFraction (lambda unrestricted current : (family SpecFraction) . (family SpecResult))
232 (specFraction digits exponent exponentNegative)
233 (branch SpecFractionOf numerator denominator .
234 (specAssemble exponentBits fractionBits bias negative
235 (specRound fractionBits bias numerator denominator))))))
236 (specNot (specIsZero digits))))))))))
237
238-- round to the format: subnormal below the minimum normal exponent (fixed scale)
239
240def specConvertF32 = (specConvert 8 23 127)
241
242def specConvertF64 = (specConvert 11 52 1023)
243The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.