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 modelWord32ShiftRight =
212 (lambda unrestricted value : (family ModelWord32) .
213 (lambda unrestricted amount : Nat .
214 (nat-eliminate
215 (lambda unrestricted current : Nat . (family ModelWord32))
216 value
217 (lambda unrestricted predecessor : Nat .
218 (lambda unrestricted induction : (family ModelWord32) .
219 (modelWord32ShiftRightOne induction)))
220 amount)))
221
222def modelWord32ShiftLeft =
223 (lambda unrestricted value : (family ModelWord32) .
224 (lambda unrestricted amount : Nat .
225 (nat-eliminate
226 (lambda unrestricted current : Nat . (family ModelWord32))
227 value
228 (lambda unrestricted predecessor : Nat .
229 (lambda unrestricted induction : (family ModelWord32) .
230 (modelWord32ShiftLeftOne induction)))
231 amount)))
232
233def modelWord32LeastBit =
234 (lambda unrestricted value : (family ModelWord32) .
235 (eliminate
236 ModelWord32
237 (lambda unrestricted current : (family ModelWord32) . Nat)
238 value
239 (branch ModelWord32Value b0 b1 b2 b3 . (byte-to-nat (byteAnd b0 (byte 1))))))
240
241def modelWord32MultiplyStep =
242 (lambda unrestricted state : (family ModelWord32MultiplyState) .
243 (eliminate
244 ModelWord32MultiplyState
245 (lambda unrestricted current : (family ModelWord32MultiplyState) .
246 (family ModelWord32MultiplyState))
247 state
248 (branch
249 ModelWord32MultiplyStateValue
250 multiplicand
251 multiplier
252 product
253 .
254 (constructor
255 ModelWord32MultiplyState
256 ModelWord32MultiplyStateValue
257 (modelWord32ShiftLeftOne multiplicand)
258 (modelWord32ShiftRightOne multiplier)
259 (modelWord32Select
260 (modelWord32LeastBit multiplier)
261 (modelWord32Add product multiplicand)
262 product)))))
263
264def modelWord32MultiplyStateRun =
265 (lambda unrestricted left : (family ModelWord32) .
266 (lambda unrestricted right : (family ModelWord32) .
267 (nat-eliminate
268 (lambda unrestricted current : Nat . (family ModelWord32MultiplyState))
269 (constructor
270 ModelWord32MultiplyState
271 ModelWord32MultiplyStateValue
272 left
273 right
274 modelWord32Zero)
275 (lambda unrestricted predecessor : Nat .
276 (lambda unrestricted induction : (family ModelWord32MultiplyState) .
277 (modelWord32MultiplyStep induction)))
278 modelWord32NaturalThirtyTwo)))
279
280def modelWord32Multiply =
281 (lambda unrestricted left : (family ModelWord32) .
282 (lambda unrestricted right : (family ModelWord32) .
283 (eliminate
284 ModelWord32MultiplyState
285 (lambda unrestricted current : (family ModelWord32MultiplyState) . (family ModelWord32))
286 (modelWord32MultiplyStateRun left right)
287 (branch ModelWord32MultiplyStateValue multiplicand multiplier product . product))))
288
289def modelWord32ModuloStep =
290 (lambda unrestricted remainder : Nat .
291 (lambda unrestricted value : Byte .
292 (lambda unrestricted divisor : Nat .
293 (naturalModuloUnchecked
294 (naturalAdd (naturalMultiply remainder byteNaturalTwoHundredFiftySix) (byte-to-nat value))
295 divisor))))
296
297def modelWord32ModuloUnchecked =
298 (lambda unrestricted value : (family ModelWord32) .
299 (lambda unrestricted divisor : Nat .
300 (eliminate
301 ModelWord32
302 (lambda unrestricted current : (family ModelWord32) . Nat)
303 value
304 (branch
305 ModelWord32Value
306 b0
307 b1
308 b2
309 b3
310 .
311 (modelWord32ModuloStep
312 (modelWord32ModuloStep
313 (modelWord32ModuloStep (modelWord32ModuloStep zero b3 divisor) b2 divisor)
314 b1
315 divisor)
316 b0
317 divisor)))))
318
319def modelWord32Modulo =
320 (lambda unrestricted value : (family ModelWord32) .
321 (lambda unrestricted divisor : Nat .
322 (nat-eliminate
323 (lambda unrestricted current : Nat . (family ModelWord32ModuloResult))
324 (constructor
325 ModelWord32ModuloResult
326 ModelWord32ModuloFailed
327 (constructor ModelWord32ArithmeticErrorCode ModelWord32ModuloByZero))
328 (lambda unrestricted predecessor : Nat .
329 (lambda unrestricted induction : (family ModelWord32ModuloResult) .
330 (constructor
331 ModelWord32ModuloResult
332 ModelWord32ModuloSucceeded
333 (modelWord32ModuloUnchecked value divisor))))
334 divisor)))
335
336def modelWord32ToNatural =
337 (lambda unrestricted value : (family ModelWord32) .
338 (eliminate
339 ModelWord32
340 (lambda unrestricted current : (family ModelWord32) . Nat)
341 value
342 (branch
343 ModelWord32Value
344 b0
345 b1
346 b2
347 b3
348 .
349 (naturalAdd
350 (byte-to-nat b0)
351 (naturalMultiply
352 byteNaturalTwoHundredFiftySix
353 (naturalAdd
354 (byte-to-nat b1)
355 (naturalMultiply
356 byteNaturalTwoHundredFiftySix
357 (naturalAdd
358 (byte-to-nat b2)
359 (naturalMultiply byteNaturalTwoHundredFiftySix (byte-to-nat b3))))))))))
360
361-- General path: four divisions by 256 (a fold over the value each). Reached
362-- only for values of 256 and above; `modelWord32FromNaturalTruncated` takes
363-- the O(1) byte path below that (D17).
364def modelWord32FromNaturalDivided =
365 (lambda unrestricted value : Nat .
366 (app
367 (lambda unrestricted quotient1 : Nat .
368 (app
369 (lambda unrestricted quotient2 : Nat .
370 (app
371 (lambda unrestricted quotient3 : Nat .
372 (constructor
373 ModelWord32
374 ModelWord32Value
375 (nat-to-byte (naturalModuloUnchecked value byteNaturalTwoHundredFiftySix))
376 (nat-to-byte (naturalModuloUnchecked quotient1 byteNaturalTwoHundredFiftySix))
377 (nat-to-byte (naturalModuloUnchecked quotient2 byteNaturalTwoHundredFiftySix))
378 (nat-to-byte (naturalModuloUnchecked quotient3 byteNaturalTwoHundredFiftySix))))
379 (naturalDivideUnchecked quotient2 byteNaturalTwoHundredFiftySix)))
380 (naturalDivideUnchecked quotient1 byteNaturalTwoHundredFiftySix)))
381 (naturalDivideUnchecked value byteNaturalTwoHundredFiftySix)))
382
383def modelWord32FromNaturalTruncated =
384 (lambda unrestricted value : Nat .
385 (app
386 (nat-eliminate
387 (lambda unrestricted small : Nat . (pi unrestricted unit : Nat . (family ModelWord32)))
388 (lambda unrestricted unit : Nat . (modelWord32FromNaturalDivided value))
389 (lambda unrestricted predecessor : Nat .
390 (lambda unrestricted induction : (pi unrestricted unit : Nat . (family ModelWord32)) .
391 (lambda unrestricted unit : Nat .
392 (constructor
393 ModelWord32
394 ModelWord32Value
395 (nat-to-byte value)
396 (byte 0)
397 (byte 0)
398 (byte 0)))))
399 (nat-less-than value byteNaturalTwoHundredFiftySix))
400 zero))
401
402-- Successor modulo 2^32: one carry chain, no fold over the value (D17).
403def modelWord32Increment =
404 (lambda unrestricted value : (family ModelWord32) . (modelWord32Add value modelWord32One))
405
406-- Order one byte position: 1 when left is below right, 0 when above, and the
407-- lower positions' verdict when equal (most significant position outermost).
408def modelWord32OrderByte =
409 (lambda unrestricted left : Byte .
410 (lambda unrestricted right : Byte .
411 (lambda unrestricted equalResult : Nat .
412 (nat-eliminate
413 (lambda unrestricted less : Nat . Nat)
414 (nat-eliminate
415 (lambda unrestricted greater : Nat . Nat)
416 equalResult
417 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
418 (byte-less-than right left))
419 (lambda unrestricted predecessor : Nat .
420 (lambda unrestricted induction : Nat . (succ zero)))
421 (byte-less-than left right)))))
422
423-- Unsigned order in four byte comparisons (D17).
424def modelWord32LessThan =
425 (lambda unrestricted left : (family ModelWord32) .
426 (lambda unrestricted right : (family ModelWord32) .
427 (eliminate
428 ModelWord32
429 (lambda unrestricted current : (family ModelWord32) . Nat)
430 left
431 (branch
432 ModelWord32Value
433 l0
434 l1
435 l2
436 l3
437 .
438 (eliminate
439 ModelWord32
440 (lambda unrestricted current : (family ModelWord32) . Nat)
441 right
442 (branch
443 ModelWord32Value
444 r0
445 r1
446 r2
447 r3
448 .
449 (modelWord32OrderByte
450 l3
451 r3
452 (modelWord32OrderByte
453 l2
454 r2
455 (modelWord32OrderByte l1 r1 (modelWord32OrderByte l0 r0 zero))))))))))
456
457def modelWord32Equal =
458 (lambda unrestricted left : (family ModelWord32) .
459 (lambda unrestricted right : (family ModelWord32) .
460 (naturalAnd
461 (naturalIsZero (modelWord32LessThan left right))
462 (naturalIsZero (modelWord32LessThan right left)))))
463
464-- value × 10 = (value << 3) + (value << 1), modulo 2^32.
465def modelWord32TimesTen =
466 (lambda unrestricted value : (family ModelWord32) .
467 (modelWord32Add
468 (modelWord32ShiftLeftOne (modelWord32ShiftLeftOne (modelWord32ShiftLeftOne value)))
469 (modelWord32ShiftLeftOne value)))
470
471-- The value of one ASCII decimal digit byte (0x30..0x39) as a word.
472def modelWord32DecimalDigit =
473 (lambda unrestricted digit : Byte .
474 (constructor ModelWord32 ModelWord32Value (byteAnd digit (byte 15)) (byte 0) (byte 0) (byte 0)))
475
476-- Decimal digit bytes, most significant first, to a word modulo 2^32; one
477-- step per digit. Callers check the bytes are digits and the value fits.
478def modelWord32FromDecimalDigitsTruncated =
479 (lambda unrestricted digits : Bytes .
480 (app
481 (bytes-eliminate
482 (lambda unrestricted current : Bytes .
483 (pi unrestricted accumulator : (family ModelWord32) . (family ModelWord32)))
484 (lambda unrestricted accumulator : (family ModelWord32) . accumulator)
485 (lambda unrestricted head : Byte .
486 (lambda unrestricted tail : Bytes .
487 (lambda unrestricted induction : (pi unrestricted accumulator : (family ModelWord32) . (family ModelWord32)) .
488 (lambda unrestricted accumulator : (family ModelWord32) .
489 (induction
490 (modelWord32Add (modelWord32TimesTen accumulator) (modelWord32DecimalDigit head)))))))
491 digits)
492 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.