1module Model.Word32
2
3import Model.Config
4import Std.Byte
5import Std.Natural
6
7family ModelWord32ArithmeticErrorCode : Type 0
8constructor ModelWord32ModuloByZero
9
10end-family
11
12family ModelWord32ModuloResult : Type 0
13constructor ModelWord32ModuloSucceeded
14field unrestricted modelWord32ModuloValue : Nat
15constructor ModelWord32ModuloFailed
16field unrestricted modelWord32ModuloError : (family ModelWord32ArithmeticErrorCode)
17
18end-family
19
20family ModelWord32MultiplyState : Type 0
21constructor ModelWord32MultiplyStateValue
22field unrestricted modelWord32MultiplyMultiplicand : (family ModelWord32)
23field unrestricted modelWord32MultiplyMultiplier : (family ModelWord32)
24field unrestricted modelWord32MultiplyProduct : (family ModelWord32)
25
26end-family
27
28def modelWord32ArithmeticErrorCodeBytes =
29 (lambda unrestricted code : (family ModelWord32ArithmeticErrorCode) .
30 (eliminate
31 ModelWord32ArithmeticErrorCode
32 (lambda unrestricted current : (family ModelWord32ArithmeticErrorCode) . Bytes)
33 code
34 (branch ModelWord32ModuloByZero . b"ALPHA-MODEL-001")))
35
36def modelWord32Zero =
37 (constructor ModelWord32 ModelWord32Value (byte 0) (byte 0) (byte 0) (byte 0))
38
39def modelWord32NaturalOne =
40 (succ zero)
41
42def modelWord32NaturalSeven =
43 (byte-to-nat (byte 7))
44
45def modelWord32NaturalThirtyTwo =
46 (byte-to-nat (byte 32))
47
48def modelWord32Select =
49 (lambda unrestricted condition : Nat .
50 (lambda unrestricted whenTrue : (family ModelWord32) .
51 (lambda unrestricted whenFalse : (family ModelWord32) .
52 (nat-eliminate
53 (lambda unrestricted current : Nat . (family ModelWord32))
54 whenFalse
55 (lambda unrestricted predecessor : Nat .
56 (lambda unrestricted induction : (family ModelWord32) . whenTrue))
57 condition))))
58
59def modelWord32Xor =
60 (lambda unrestricted left : (family ModelWord32) .
61 (lambda unrestricted right : (family ModelWord32) .
62 (eliminate
63 ModelWord32
64 (lambda unrestricted current : (family ModelWord32) . (family ModelWord32))
65 left
66 (branch
67 ModelWord32Value
68 l0
69 l1
70 l2
71 l3
72 .
73 (eliminate
74 ModelWord32
75 (lambda unrestricted current : (family ModelWord32) . (family ModelWord32))
76 right
77 (branch
78 ModelWord32Value
79 r0
80 r1
81 r2
82 r3
83 .
84 (constructor
85 ModelWord32
86 ModelWord32Value
87 (byteXor l0 r0)
88 (byteXor l1 r1)
89 (byteXor l2 r2)
90 (byteXor l3 r3))))))))
91
92def modelWord32Add =
93 (lambda unrestricted left : (family ModelWord32) .
94 (lambda unrestricted right : (family ModelWord32) .
95 (eliminate
96 ModelWord32
97 (lambda unrestricted current : (family ModelWord32) . (family ModelWord32))
98 left
99 (branch
100 ModelWord32Value
101 l0
102 l1
103 l2
104 l3
105 .
106 (eliminate
107 ModelWord32
108 (lambda unrestricted current : (family ModelWord32) . (family ModelWord32))
109 right
110 (branch
111 ModelWord32Value
112 r0
113 r1
114 r2
115 r3
116 .
117 (eliminate
118 ByteAddResult
119 (lambda unrestricted current : (family ByteAddResult) . (family ModelWord32))
120 (byteAddWithCarry l0 r0 zero)
121 (branch
122 ByteAddResultValue
123 sum0
124 carry0
125 .
126 (eliminate
127 ByteAddResult
128 (lambda unrestricted current : (family ByteAddResult) . (family ModelWord32))
129 (byteAddWithCarry l1 r1 carry0)
130 (branch
131 ByteAddResultValue
132 sum1
133 carry1
134 .
135 (eliminate
136 ByteAddResult
137 (lambda unrestricted current : (family ByteAddResult) .
138 (family ModelWord32))
139 (byteAddWithCarry l2 r2 carry1)
140 (branch
141 ByteAddResultValue
142 sum2
143 carry2
144 .
145 (eliminate
146 ByteAddResult
147 (lambda unrestricted current : (family ByteAddResult) .
148 (family ModelWord32))
149 (byteAddWithCarry l3 r3 carry2)
150 (branch
151 ByteAddResultValue
152 sum3
153 carry3
154 .
155 (constructor ModelWord32 ModelWord32Value sum0 sum1 sum2 sum3)))))))))))))))
156
157def modelWord32ShiftRightOne =
158 (lambda unrestricted value : (family ModelWord32) .
159 (eliminate
160 ModelWord32
161 (lambda unrestricted current : (family ModelWord32) . (family ModelWord32))
162 value
163 (branch
164 ModelWord32Value
165 b0
166 b1
167 b2
168 b3
169 .
170 (constructor
171 ModelWord32
172 ModelWord32Value
173 (byteOr
174 (byteShiftRight b0 modelWord32NaturalOne)
175 (byteShiftLeftTruncated (byteAnd b1 (byte 1)) modelWord32NaturalSeven))
176 (byteOr
177 (byteShiftRight b1 modelWord32NaturalOne)
178 (byteShiftLeftTruncated (byteAnd b2 (byte 1)) modelWord32NaturalSeven))
179 (byteOr
180 (byteShiftRight b2 modelWord32NaturalOne)
181 (byteShiftLeftTruncated (byteAnd b3 (byte 1)) modelWord32NaturalSeven))
182 (byteShiftRight b3 modelWord32NaturalOne)))))
183
184def modelWord32ShiftLeftOne =
185 (lambda unrestricted value : (family ModelWord32) .
186 (eliminate
187 ModelWord32
188 (lambda unrestricted current : (family ModelWord32) . (family ModelWord32))
189 value
190 (branch
191 ModelWord32Value
192 b0
193 b1
194 b2
195 b3
196 .
197 (constructor
198 ModelWord32
199 ModelWord32Value
200 (byteShiftLeftTruncated b0 modelWord32NaturalOne)
201 (byteOr
202 (byteShiftLeftTruncated b1 modelWord32NaturalOne)
203 (byteShiftRight b0 modelWord32NaturalSeven))
204 (byteOr
205 (byteShiftLeftTruncated b2 modelWord32NaturalOne)
206 (byteShiftRight b1 modelWord32NaturalSeven))
207 (byteOr
208 (byteShiftLeftTruncated b3 modelWord32NaturalOne)
209 (byteShiftRight b2 modelWord32NaturalSeven))))))
210
211def modelWord32ToNatural =
212 (lambda unrestricted value : (family ModelWord32) .
213 (eliminate
214 ModelWord32
215 (lambda unrestricted current : (family ModelWord32) . Nat)
216 value
217 (branch
218 ModelWord32Value
219 b0
220 b1
221 b2
222 b3
223 .
224 (naturalAdd
225 (byte-to-nat b0)
226 (naturalMultiply
227 byteNaturalTwoHundredFiftySix
228 (naturalAdd
229 (byte-to-nat b1)
230 (naturalMultiply
231 byteNaturalTwoHundredFiftySix
232 (naturalAdd
233 (byte-to-nat b2)
234 (naturalMultiply byteNaturalTwoHundredFiftySix (byte-to-nat b3))))))))))
235
236-- General path: four divisions by 256 (a fold over the value each). Reached
237-- only for values of 256 and above; `modelWord32FromNaturalTruncated` takes
238-- the O(1) byte path below that (D17).
239def modelWord32FromNaturalDivided =
240 (lambda unrestricted value : Nat .
241 (app
242 (lambda unrestricted quotient1 : Nat .
243 (app
244 (lambda unrestricted quotient2 : Nat .
245 (app
246 (lambda unrestricted quotient3 : Nat .
247 (constructor
248 ModelWord32
249 ModelWord32Value
250 (nat-to-byte (naturalModuloUnchecked value byteNaturalTwoHundredFiftySix))
251 (nat-to-byte (naturalModuloUnchecked quotient1 byteNaturalTwoHundredFiftySix))
252 (nat-to-byte (naturalModuloUnchecked quotient2 byteNaturalTwoHundredFiftySix))
253 (nat-to-byte (naturalModuloUnchecked quotient3 byteNaturalTwoHundredFiftySix))))
254 (naturalDivideUnchecked quotient2 byteNaturalTwoHundredFiftySix)))
255 (naturalDivideUnchecked quotient1 byteNaturalTwoHundredFiftySix)))
256 (naturalDivideUnchecked value byteNaturalTwoHundredFiftySix)))
257
258def modelWord32FromNaturalTruncated =
259 (lambda unrestricted value : Nat .
260 (app
261 (nat-eliminate
262 (lambda unrestricted small : Nat . (pi unrestricted unit : Nat . (family ModelWord32)))
263 (lambda unrestricted unit : Nat . (modelWord32FromNaturalDivided value))
264 (lambda unrestricted predecessor : Nat .
265 (lambda unrestricted induction : (pi unrestricted unit : Nat . (family ModelWord32)) .
266 (lambda unrestricted unit : Nat .
267 (constructor
268 ModelWord32
269 ModelWord32Value
270 (nat-to-byte value)
271 (byte 0)
272 (byte 0)
273 (byte 0)))))
274 (nat-less-than value byteNaturalTwoHundredFiftySix))
275 zero))
276
277-- A logical shift is division/multiplication by 2^amount followed by the
278-- word conversion, rather than amount separate carry traversals. The width
279-- guard is lazy: amounts >= 32 return zero without computing their power.
280-- On the bounded u64 runtime lane the largest admitted multiplication is
281-- (2^32 - 1) * 2^31 < 2^63, so no host overflow precedes truncation. Keeping
282-- the one-bit operations independent also leaves a byte-lane reference for
283-- the full shift tests. The Baguette realize profile run-430189202 motivated
284-- this change; equality of emitted bytes still needs artifact qualification.
285def modelWord32ShiftRight =
286 (lambda unrestricted value : (family ModelWord32) .
287 (lambda unrestricted amount : Nat .
288 (app
289 (nat-eliminate
290 (lambda unrestricted current : Nat . (pi unrestricted unit : Nat . (family ModelWord32)))
291 (lambda unrestricted unit : Nat . modelWord32Zero)
292 (lambda unrestricted predecessor : Nat .
293 (lambda unrestricted induction : (pi unrestricted unit : Nat . (family ModelWord32)) .
294 (lambda unrestricted unit : Nat .
295 (modelWord32FromNaturalTruncated
296 (naturalDivideUnchecked (modelWord32ToNatural value) (naturalPowerOfTwo amount))))))
297 (naturalLess amount modelWord32NaturalThirtyTwo))
298 zero)))
299
300def modelWord32ShiftLeft =
301 (lambda unrestricted value : (family ModelWord32) .
302 (lambda unrestricted amount : Nat .
303 (app
304 (nat-eliminate
305 (lambda unrestricted current : Nat . (pi unrestricted unit : Nat . (family ModelWord32)))
306 (lambda unrestricted unit : Nat . modelWord32Zero)
307 (lambda unrestricted predecessor : Nat .
308 (lambda unrestricted induction : (pi unrestricted unit : Nat . (family ModelWord32)) .
309 (lambda unrestricted unit : Nat .
310 (modelWord32FromNaturalTruncated
311 (naturalMultiply (modelWord32ToNatural value) (naturalPowerOfTwo amount))))))
312 (naturalLess amount modelWord32NaturalThirtyTwo))
313 zero)))
314
315def modelWord32LeastBit =
316 (lambda unrestricted value : (family ModelWord32) .
317 (eliminate
318 ModelWord32
319 (lambda unrestricted current : (family ModelWord32) . Nat)
320 value
321 (branch ModelWord32Value b0 b1 b2 b3 . (byte-to-nat (byteAnd b0 (byte 1))))))
322
323def modelWord32MultiplyStep =
324 (lambda unrestricted state : (family ModelWord32MultiplyState) .
325 (eliminate
326 ModelWord32MultiplyState
327 (lambda unrestricted current : (family ModelWord32MultiplyState) .
328 (family ModelWord32MultiplyState))
329 state
330 (branch
331 ModelWord32MultiplyStateValue
332 multiplicand
333 multiplier
334 product
335 .
336 (constructor
337 ModelWord32MultiplyState
338 ModelWord32MultiplyStateValue
339 (modelWord32ShiftLeftOne multiplicand)
340 (modelWord32ShiftRightOne multiplier)
341 (modelWord32Select
342 (modelWord32LeastBit multiplier)
343 (modelWord32Add product multiplicand)
344 product)))))
345
346def modelWord32MultiplyStateRun =
347 (lambda unrestricted left : (family ModelWord32) .
348 (lambda unrestricted right : (family ModelWord32) .
349 (nat-eliminate
350 (lambda unrestricted current : Nat . (family ModelWord32MultiplyState))
351 (constructor
352 ModelWord32MultiplyState
353 ModelWord32MultiplyStateValue
354 left
355 right
356 modelWord32Zero)
357 (lambda unrestricted predecessor : Nat .
358 (lambda unrestricted induction : (family ModelWord32MultiplyState) .
359 (modelWord32MultiplyStep induction)))
360 modelWord32NaturalThirtyTwo)))
361
362def modelWord32Multiply =
363 (lambda unrestricted left : (family ModelWord32) .
364 (lambda unrestricted right : (family ModelWord32) .
365 (eliminate
366 ModelWord32MultiplyState
367 (lambda unrestricted current : (family ModelWord32MultiplyState) . (family ModelWord32))
368 (modelWord32MultiplyStateRun left right)
369 (branch ModelWord32MultiplyStateValue multiplicand multiplier product . product))))
370
371def modelWord32ModuloStep =
372 (lambda unrestricted remainder : Nat .
373 (lambda unrestricted value : Byte .
374 (lambda unrestricted divisor : Nat .
375 (naturalModuloUnchecked
376 (naturalAdd (naturalMultiply remainder byteNaturalTwoHundredFiftySix) (byte-to-nat value))
377 divisor))))
378
379def modelWord32ModuloUnchecked =
380 (lambda unrestricted value : (family ModelWord32) .
381 (lambda unrestricted divisor : Nat .
382 (eliminate
383 ModelWord32
384 (lambda unrestricted current : (family ModelWord32) . Nat)
385 value
386 (branch
387 ModelWord32Value
388 b0
389 b1
390 b2
391 b3
392 .
393 (modelWord32ModuloStep
394 (modelWord32ModuloStep
395 (modelWord32ModuloStep (modelWord32ModuloStep zero b3 divisor) b2 divisor)
396 b1
397 divisor)
398 b0
399 divisor)))))
400
401def modelWord32Modulo =
402 (lambda unrestricted value : (family ModelWord32) .
403 (lambda unrestricted divisor : Nat .
404 (nat-eliminate
405 (lambda unrestricted current : Nat . (family ModelWord32ModuloResult))
406 (constructor
407 ModelWord32ModuloResult
408 ModelWord32ModuloFailed
409 (constructor ModelWord32ArithmeticErrorCode ModelWord32ModuloByZero))
410 (lambda unrestricted predecessor : Nat .
411 (lambda unrestricted induction : (family ModelWord32ModuloResult) .
412 (constructor
413 ModelWord32ModuloResult
414 ModelWord32ModuloSucceeded
415 (modelWord32ModuloUnchecked value divisor))))
416 divisor)))
417
418-- Successor modulo 2^32: one carry chain, no fold over the value (D17).
419def modelWord32Increment =
420 (lambda unrestricted value : (family ModelWord32) . (modelWord32Add value modelWord32One))
421
422-- Order one byte position: 1 when left is below right, 0 when above, and the
423-- lower positions' verdict when equal (most significant position outermost).
424def modelWord32OrderByte =
425 (lambda unrestricted left : Byte .
426 (lambda unrestricted right : Byte .
427 (lambda unrestricted equalResult : Nat .
428 (nat-eliminate
429 (lambda unrestricted less : Nat . Nat)
430 (nat-eliminate
431 (lambda unrestricted greater : Nat . Nat)
432 equalResult
433 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
434 (byte-less-than right left))
435 (lambda unrestricted predecessor : Nat .
436 (lambda unrestricted induction : Nat . (succ zero)))
437 (byte-less-than left right)))))
438
439-- Unsigned order in four byte comparisons (D17).
440def modelWord32LessThan =
441 (lambda unrestricted left : (family ModelWord32) .
442 (lambda unrestricted right : (family ModelWord32) .
443 (eliminate
444 ModelWord32
445 (lambda unrestricted current : (family ModelWord32) . Nat)
446 left
447 (branch
448 ModelWord32Value
449 l0
450 l1
451 l2
452 l3
453 .
454 (eliminate
455 ModelWord32
456 (lambda unrestricted current : (family ModelWord32) . Nat)
457 right
458 (branch
459 ModelWord32Value
460 r0
461 r1
462 r2
463 r3
464 .
465 (modelWord32OrderByte
466 l3
467 r3
468 (modelWord32OrderByte
469 l2
470 r2
471 (modelWord32OrderByte l1 r1 (modelWord32OrderByte l0 r0 zero))))))))))
472
473def modelWord32Equal =
474 (lambda unrestricted left : (family ModelWord32) .
475 (lambda unrestricted right : (family ModelWord32) .
476 (naturalAnd
477 (naturalIsZero (modelWord32LessThan left right))
478 (naturalIsZero (modelWord32LessThan right left)))))
479
480-- value × 10 = (value << 3) + (value << 1), modulo 2^32.
481def modelWord32TimesTen =
482 (lambda unrestricted value : (family ModelWord32) .
483 (modelWord32Add
484 (modelWord32ShiftLeftOne (modelWord32ShiftLeftOne (modelWord32ShiftLeftOne value)))
485 (modelWord32ShiftLeftOne value)))
486
487-- The value of one ASCII decimal digit byte (0x30..0x39) as a word.
488def modelWord32DecimalDigit =
489 (lambda unrestricted digit : Byte .
490 (constructor ModelWord32 ModelWord32Value (byteAnd digit (byte 15)) (byte 0) (byte 0) (byte 0)))
491
492-- Decimal digit bytes, most significant first, to a word modulo 2^32; one
493-- step per digit. Callers check the bytes are digits and the value fits.
494def modelWord32FromDecimalDigitsTruncated =
495 (lambda unrestricted digits : Bytes .
496 (app
497 (bytes-eliminate
498 (lambda unrestricted current : Bytes .
499 (pi unrestricted accumulator : (family ModelWord32) . (family ModelWord32)))
500 (lambda unrestricted accumulator : (family ModelWord32) . accumulator)
501 (lambda unrestricted head : Byte .
502 (lambda unrestricted tail : Bytes .
503 (lambda unrestricted induction : (pi unrestricted accumulator : (family ModelWord32) . (family ModelWord32)) .
504 (lambda unrestricted accumulator : (family ModelWord32) .
505 (induction
506 (modelWord32Add (modelWord32TimesTen accumulator) (modelWord32DecimalDigit head)))))))
507 digits)
508 modelWord32Zero))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.