1module Model.Word64
2
3import Model.Parameter
4import Std.Byte
5import Std.Natural
6import Std.Flag
7
8family ModelWord64ArithmeticErrorCode : Type 0
9constructor ModelWord64AdditionOverflow
10constructor ModelWord64SubtractionUnderflow
11
12end-family
13
14family ModelWord64AddResult : Type 0
15constructor ModelWord64AddResultValue
16field unrestricted modelWord64AddValue : (family ModelWord64)
17field unrestricted modelWord64AddCarry : Nat
18
19end-family
20
21family ModelWord64CheckedResult : Type 0
22constructor ModelWord64CheckedSucceeded
23field unrestricted modelWord64CheckedValue : (family ModelWord64)
24constructor ModelWord64CheckedFailed
25field unrestricted modelWord64CheckedError : (family ModelWord64ArithmeticErrorCode)
26
27end-family
28
29family ModelWord64MultiplyState : Type 0
30constructor ModelWord64MultiplyStateValue
31field unrestricted modelWord64MultiplyMultiplicand : (family ModelWord64)
32field unrestricted modelWord64MultiplyMultiplier : (family ModelWord64)
33field unrestricted modelWord64MultiplyProduct : (family ModelWord64)
34field unrestricted modelWord64MultiplyOverflow : Nat
35
36end-family
37
38family ModelWord64MultiplyCheckedResult : Type 0
39constructor ModelWord64MultiplySucceeded
40field unrestricted modelWord64MultiplyValue : (family ModelWord64)
41constructor ModelWord64MultiplyOverflow
42
43end-family
44
45def modelWord64ArithmeticErrorCodeBytes =
46 (lambda unrestricted code : (family ModelWord64ArithmeticErrorCode) .
47 (eliminate
48 ModelWord64ArithmeticErrorCode
49 (lambda unrestricted current : (family ModelWord64ArithmeticErrorCode) . Bytes)
50 code
51 (branch ModelWord64AdditionOverflow . b"ALPHA-MODEL-W64-001")
52 (branch ModelWord64SubtractionUnderflow . b"ALPHA-MODEL-W64-002")))
53
54def modelWord64Zero =
55 (constructor
56 ModelWord64
57 ModelWord64Value
58 (byte 0)
59 (byte 0)
60 (byte 0)
61 (byte 0)
62 (byte 0)
63 (byte 0)
64 (byte 0)
65 (byte 0))
66
67def modelWord64One =
68 (constructor
69 ModelWord64
70 ModelWord64Value
71 (byte 1)
72 (byte 0)
73 (byte 0)
74 (byte 0)
75 (byte 0)
76 (byte 0)
77 (byte 0)
78 (byte 0))
79
80-- Delegates to the one owner (Std.Flag), which this file already had a
81-- byte-for-byte copy of before `alpha-ast duplicates` found it (L24d).
82def modelWord64FlagAnd =
83 inferenceFlagAnd
84
85def modelWord64Select =
86 (lambda unrestricted condition : Nat .
87 (lambda unrestricted whenTrue : (family ModelWord64) .
88 (lambda unrestricted whenFalse : (family ModelWord64) .
89 (nat-eliminate
90 (lambda unrestricted current : Nat . (family ModelWord64))
91 whenFalse
92 (lambda unrestricted predecessor : Nat .
93 (lambda unrestricted induction : (family ModelWord64) . whenTrue))
94 condition))))
95
96def modelWord64And =
97 (lambda unrestricted left : (family ModelWord64) .
98 (lambda unrestricted right : (family ModelWord64) .
99 (eliminate
100 ModelWord64
101 (lambda unrestricted current : (family ModelWord64) . (family ModelWord64))
102 left
103 (branch
104 ModelWord64Value
105 l0
106 l1
107 l2
108 l3
109 l4
110 l5
111 l6
112 l7
113 .
114 (eliminate
115 ModelWord64
116 (lambda unrestricted current : (family ModelWord64) . (family ModelWord64))
117 right
118 (branch
119 ModelWord64Value
120 r0
121 r1
122 r2
123 r3
124 r4
125 r5
126 r6
127 r7
128 .
129 (constructor
130 ModelWord64
131 ModelWord64Value
132 (byteAnd l0 r0)
133 (byteAnd l1 r1)
134 (byteAnd l2 r2)
135 (byteAnd l3 r3)
136 (byteAnd l4 r4)
137 (byteAnd l5 r5)
138 (byteAnd l6 r6)
139 (byteAnd l7 r7))))))))
140
141def modelWord64Xor =
142 (lambda unrestricted left : (family ModelWord64) .
143 (lambda unrestricted right : (family ModelWord64) .
144 (eliminate
145 ModelWord64
146 (lambda unrestricted current : (family ModelWord64) . (family ModelWord64))
147 left
148 (branch
149 ModelWord64Value
150 l0
151 l1
152 l2
153 l3
154 l4
155 l5
156 l6
157 l7
158 .
159 (eliminate
160 ModelWord64
161 (lambda unrestricted current : (family ModelWord64) . (family ModelWord64))
162 right
163 (branch
164 ModelWord64Value
165 r0
166 r1
167 r2
168 r3
169 r4
170 r5
171 r6
172 r7
173 .
174 (constructor
175 ModelWord64
176 ModelWord64Value
177 (byteXor l0 r0)
178 (byteXor l1 r1)
179 (byteXor l2 r2)
180 (byteXor l3 r3)
181 (byteXor l4 r4)
182 (byteXor l5 r5)
183 (byteXor l6 r6)
184 (byteXor l7 r7))))))))
185
186def modelWord64Complement =
187 (lambda unrestricted value : (family ModelWord64) .
188 (eliminate
189 ModelWord64
190 (lambda unrestricted current : (family ModelWord64) . (family ModelWord64))
191 value
192 (branch
193 ModelWord64Value
194 b0
195 b1
196 b2
197 b3
198 b4
199 b5
200 b6
201 b7
202 .
203 (constructor
204 ModelWord64
205 ModelWord64Value
206 (byteXor b0 (byte 255))
207 (byteXor b1 (byte 255))
208 (byteXor b2 (byte 255))
209 (byteXor b3 (byte 255))
210 (byteXor b4 (byte 255))
211 (byteXor b5 (byte 255))
212 (byteXor b6 (byte 255))
213 (byteXor b7 (byte 255))))))
214
215def modelWord64IsZero =
216 (lambda unrestricted value : (family ModelWord64) .
217 (eliminate
218 ModelWord64
219 (lambda unrestricted current : (family ModelWord64) . Nat)
220 value
221 (branch
222 ModelWord64Value
223 b0
224 b1
225 b2
226 b3
227 b4
228 b5
229 b6
230 b7
231 .
232 (modelWord64FlagAnd
233 (byte-equal b0 (byte 0))
234 (modelWord64FlagAnd
235 (byte-equal b1 (byte 0))
236 (modelWord64FlagAnd
237 (byte-equal b2 (byte 0))
238 (modelWord64FlagAnd
239 (byte-equal b3 (byte 0))
240 (modelWord64FlagAnd
241 (byte-equal b4 (byte 0))
242 (modelWord64FlagAnd
243 (byte-equal b5 (byte 0))
244 (modelWord64FlagAnd (byte-equal b6 (byte 0)) (byte-equal b7 (byte 0))))))))))))
245
246def modelWord64Equal =
247 (lambda unrestricted left : (family ModelWord64) .
248 (lambda unrestricted right : (family ModelWord64) .
249 (modelWord64IsZero (modelWord64Xor left right))))
250
251def modelWord64OrderByte =
252 (lambda unrestricted left : Byte .
253 (lambda unrestricted right : Byte .
254 (lambda unrestricted equalResult : Nat .
255 (nat-eliminate
256 (lambda unrestricted less : Nat . Nat)
257 (nat-eliminate
258 (lambda unrestricted greater : Nat . Nat)
259 equalResult
260 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
261 (byte-less-than right left))
262 (lambda unrestricted predecessor : Nat .
263 (lambda unrestricted induction : Nat . (succ zero)))
264 (byte-less-than left right)))))
265
266def modelWord64LessThan =
267 (lambda unrestricted left : (family ModelWord64) .
268 (lambda unrestricted right : (family ModelWord64) .
269 (eliminate
270 ModelWord64
271 (lambda unrestricted current : (family ModelWord64) . Nat)
272 left
273 (branch
274 ModelWord64Value
275 l0
276 l1
277 l2
278 l3
279 l4
280 l5
281 l6
282 l7
283 .
284 (eliminate
285 ModelWord64
286 (lambda unrestricted current : (family ModelWord64) . Nat)
287 right
288 (branch
289 ModelWord64Value
290 r0
291 r1
292 r2
293 r3
294 r4
295 r5
296 r6
297 r7
298 .
299 (modelWord64OrderByte
300 l7
301 r7
302 (modelWord64OrderByte
303 l6
304 r6
305 (modelWord64OrderByte
306 l5
307 r5
308 (modelWord64OrderByte
309 l4
310 r4
311 (modelWord64OrderByte
312 l3
313 r3
314 (modelWord64OrderByte
315 l2
316 r2
317 (modelWord64OrderByte l1 r1 (modelWord64OrderByte l0 r0 zero))))))))))))))
318
319def modelWord64AddWithCarry =
320 (lambda unrestricted left : (family ModelWord64) .
321 (lambda unrestricted right : (family ModelWord64) .
322 (eliminate
323 ModelWord64
324 (lambda unrestricted current : (family ModelWord64) . (family ModelWord64AddResult))
325 left
326 (branch
327 ModelWord64Value
328 l0
329 l1
330 l2
331 l3
332 l4
333 l5
334 l6
335 l7
336 .
337 (eliminate
338 ModelWord64
339 (lambda unrestricted current : (family ModelWord64) . (family ModelWord64AddResult))
340 right
341 (branch
342 ModelWord64Value
343 r0
344 r1
345 r2
346 r3
347 r4
348 r5
349 r6
350 r7
351 .
352 (eliminate
353 ByteAddResult
354 (lambda unrestricted current : (family ByteAddResult) .
355 (family ModelWord64AddResult))
356 (byteAddWithCarry l0 r0 zero)
357 (branch
358 ByteAddResultValue
359 s0
360 c0
361 .
362 (eliminate
363 ByteAddResult
364 (lambda unrestricted current : (family ByteAddResult) .
365 (family ModelWord64AddResult))
366 (byteAddWithCarry l1 r1 c0)
367 (branch
368 ByteAddResultValue
369 s1
370 c1
371 .
372 (eliminate
373 ByteAddResult
374 (lambda unrestricted current : (family ByteAddResult) .
375 (family ModelWord64AddResult))
376 (byteAddWithCarry l2 r2 c1)
377 (branch
378 ByteAddResultValue
379 s2
380 c2
381 .
382 (eliminate
383 ByteAddResult
384 (lambda unrestricted current : (family ByteAddResult) .
385 (family ModelWord64AddResult))
386 (byteAddWithCarry l3 r3 c2)
387 (branch
388 ByteAddResultValue
389 s3
390 c3
391 .
392 (eliminate
393 ByteAddResult
394 (lambda unrestricted current : (family ByteAddResult) .
395 (family ModelWord64AddResult))
396 (byteAddWithCarry l4 r4 c3)
397 (branch
398 ByteAddResultValue
399 s4
400 c4
401 .
402 (eliminate
403 ByteAddResult
404 (lambda unrestricted current : (family ByteAddResult) .
405 (family ModelWord64AddResult))
406 (byteAddWithCarry l5 r5 c4)
407 (branch
408 ByteAddResultValue
409 s5
410 c5
411 .
412 (eliminate
413 ByteAddResult
414 (lambda unrestricted current : (family ByteAddResult) .
415 (family ModelWord64AddResult))
416 (byteAddWithCarry l6 r6 c5)
417 (branch
418 ByteAddResultValue
419 s6
420 c6
421 .
422 (eliminate
423 ByteAddResult
424 (lambda unrestricted current : (family ByteAddResult) .
425 (family ModelWord64AddResult))
426 (byteAddWithCarry l7 r7 c6)
427 (branch
428 ByteAddResultValue
429 s7
430 c7
431 .
432 (constructor
433 ModelWord64AddResult
434 ModelWord64AddResultValue
435 (constructor
436 ModelWord64
437 ModelWord64Value
438 s0
439 s1
440 s2
441 s3
442 s4
443 s5
444 s6
445 s7)
446 c7)))))))))))))))))))))))
447
448def modelWord64Add =
449 (lambda unrestricted left : (family ModelWord64) .
450 (lambda unrestricted right : (family ModelWord64) .
451 (eliminate
452 ModelWord64AddResult
453 (lambda unrestricted result : (family ModelWord64AddResult) . (family ModelWord64))
454 (modelWord64AddWithCarry left right)
455 (branch ModelWord64AddResultValue value carry . value))))
456
457def modelWord64AddChecked =
458 (lambda unrestricted left : (family ModelWord64) .
459 (lambda unrestricted right : (family ModelWord64) .
460 (eliminate
461 ModelWord64AddResult
462 (lambda unrestricted result : (family ModelWord64AddResult) .
463 (family ModelWord64CheckedResult))
464 (modelWord64AddWithCarry left right)
465 (branch
466 ModelWord64AddResultValue
467 value
468 carry
469 .
470 (nat-eliminate
471 (lambda unrestricted current : Nat . (family ModelWord64CheckedResult))
472 (constructor ModelWord64CheckedResult ModelWord64CheckedSucceeded value)
473 (lambda unrestricted predecessor : Nat .
474 (lambda unrestricted induction : (family ModelWord64CheckedResult) .
475 (constructor
476 ModelWord64CheckedResult
477 ModelWord64CheckedFailed
478 (constructor ModelWord64ArithmeticErrorCode ModelWord64AdditionOverflow))))
479 carry)))))
480
481def modelWord64Subtract =
482 (lambda unrestricted left : (family ModelWord64) .
483 (lambda unrestricted right : (family ModelWord64) .
484 (modelWord64Add left (modelWord64Add (modelWord64Complement right) modelWord64One))))
485
486def modelWord64SubtractChecked =
487 (lambda unrestricted left : (family ModelWord64) .
488 (lambda unrestricted right : (family ModelWord64) .
489 (nat-eliminate
490 (lambda unrestricted current : Nat . (family ModelWord64CheckedResult))
491 (constructor
492 ModelWord64CheckedResult
493 ModelWord64CheckedSucceeded
494 (modelWord64Subtract left right))
495 (lambda unrestricted predecessor : Nat .
496 (lambda unrestricted induction : (family ModelWord64CheckedResult) .
497 (constructor
498 ModelWord64CheckedResult
499 ModelWord64CheckedFailed
500 (constructor ModelWord64ArithmeticErrorCode ModelWord64SubtractionUnderflow))))
501 (modelWord64LessThan left right))))
502
503-- Delegates to the one owner (Std.Flag): this body is alpha-equivalent to
504-- Std.Flag.inferenceFlagNot (binder renamed value<->flag, otherwise
505-- identical) -- missed by `alpha-ast duplicates`' exact (binder-name-
506-- sensitive) shape digest, found by manual inspection after that tool
507-- grouped it with Std.Natural.naturalIsZero instead (also alpha-equivalent
508-- to inferenceFlagNot, coincidentally under the same binder name "value").
509def modelWord64FlagNot =
510 inferenceFlagNot
511
512-- Delegates to the one owner (Std.Flag), which this file already had a
513-- byte-for-byte copy of before `alpha-ast duplicates` found it (L24d).
514def modelWord64FlagOr =
515 inferenceFlagOr
516
517def modelWord64NaturalOne =
518 (succ zero)
519
520def modelWord64NaturalSeven =
521 (byte-to-nat (byte 7))
522
523def modelWord64NaturalSixtyFour =
524 (byte-to-nat (byte 64))
525
526def modelWord64ShiftRightOne =
527 (lambda unrestricted value : (family ModelWord64) .
528 (eliminate
529 ModelWord64
530 (lambda unrestricted current : (family ModelWord64) . (family ModelWord64))
531 value
532 (branch
533 ModelWord64Value
534 b0
535 b1
536 b2
537 b3
538 b4
539 b5
540 b6
541 b7
542 .
543 (constructor
544 ModelWord64
545 ModelWord64Value
546 (byteOr
547 (byteShiftRight b0 modelWord64NaturalOne)
548 (byteShiftLeftTruncated (byteAnd b1 (byte 1)) modelWord64NaturalSeven))
549 (byteOr
550 (byteShiftRight b1 modelWord64NaturalOne)
551 (byteShiftLeftTruncated (byteAnd b2 (byte 1)) modelWord64NaturalSeven))
552 (byteOr
553 (byteShiftRight b2 modelWord64NaturalOne)
554 (byteShiftLeftTruncated (byteAnd b3 (byte 1)) modelWord64NaturalSeven))
555 (byteOr
556 (byteShiftRight b3 modelWord64NaturalOne)
557 (byteShiftLeftTruncated (byteAnd b4 (byte 1)) modelWord64NaturalSeven))
558 (byteOr
559 (byteShiftRight b4 modelWord64NaturalOne)
560 (byteShiftLeftTruncated (byteAnd b5 (byte 1)) modelWord64NaturalSeven))
561 (byteOr
562 (byteShiftRight b5 modelWord64NaturalOne)
563 (byteShiftLeftTruncated (byteAnd b6 (byte 1)) modelWord64NaturalSeven))
564 (byteOr
565 (byteShiftRight b6 modelWord64NaturalOne)
566 (byteShiftLeftTruncated (byteAnd b7 (byte 1)) modelWord64NaturalSeven))
567 (byteShiftRight b7 modelWord64NaturalOne)))))
568
569def modelWord64ShiftLeftOne =
570 (lambda unrestricted value : (family ModelWord64) .
571 (eliminate
572 ModelWord64
573 (lambda unrestricted current : (family ModelWord64) . (family ModelWord64))
574 value
575 (branch
576 ModelWord64Value
577 b0
578 b1
579 b2
580 b3
581 b4
582 b5
583 b6
584 b7
585 .
586 (constructor
587 ModelWord64
588 ModelWord64Value
589 (byteShiftLeftTruncated b0 modelWord64NaturalOne)
590 (byteOr
591 (byteShiftLeftTruncated b1 modelWord64NaturalOne)
592 (byteShiftRight b0 modelWord64NaturalSeven))
593 (byteOr
594 (byteShiftLeftTruncated b2 modelWord64NaturalOne)
595 (byteShiftRight b1 modelWord64NaturalSeven))
596 (byteOr
597 (byteShiftLeftTruncated b3 modelWord64NaturalOne)
598 (byteShiftRight b2 modelWord64NaturalSeven))
599 (byteOr
600 (byteShiftLeftTruncated b4 modelWord64NaturalOne)
601 (byteShiftRight b3 modelWord64NaturalSeven))
602 (byteOr
603 (byteShiftLeftTruncated b5 modelWord64NaturalOne)
604 (byteShiftRight b4 modelWord64NaturalSeven))
605 (byteOr
606 (byteShiftLeftTruncated b6 modelWord64NaturalOne)
607 (byteShiftRight b5 modelWord64NaturalSeven))
608 (byteOr
609 (byteShiftLeftTruncated b7 modelWord64NaturalOne)
610 (byteShiftRight b6 modelWord64NaturalSeven))))))
611
612def modelWord64LeastBit =
613 (lambda unrestricted value : (family ModelWord64) .
614 (eliminate
615 ModelWord64
616 (lambda unrestricted current : (family ModelWord64) . Nat)
617 value
618 (branch ModelWord64Value b0 b1 b2 b3 b4 b5 b6 b7 . (byte-to-nat (byteAnd b0 (byte 1))))))
619
620def modelWord64HighBit =
621 (lambda unrestricted value : (family ModelWord64) .
622 (eliminate
623 ModelWord64
624 (lambda unrestricted current : (family ModelWord64) . Nat)
625 value
626 (branch ModelWord64Value b0 b1 b2 b3 b4 b5 b6 b7 . (byte-less-than (byte 127) b7))))
627
628def modelWord64MultiplyStep =
629 (lambda unrestricted state : (family ModelWord64MultiplyState) .
630 (eliminate
631 ModelWord64MultiplyState
632 (lambda unrestricted current : (family ModelWord64MultiplyState) .
633 (family ModelWord64MultiplyState))
634 state
635 (branch
636 ModelWord64MultiplyStateValue
637 multiplicand
638 multiplier
639 product
640 overflow
641 .
642 (app
643 (lambda unrestricted leastBit : Nat .
644 (app
645 (lambda unrestricted nextMultiplier : (family ModelWord64) .
646 (eliminate
647 ModelWord64AddResult
648 (lambda unrestricted result : (family ModelWord64AddResult) .
649 (family ModelWord64MultiplyState))
650 (modelWord64AddWithCarry product multiplicand)
651 (branch
652 ModelWord64AddResultValue
653 sum
654 carry
655 .
656 (constructor
657 ModelWord64MultiplyState
658 ModelWord64MultiplyStateValue
659 (modelWord64ShiftLeftOne multiplicand)
660 nextMultiplier
661 (modelWord64Select leastBit sum product)
662 (modelWord64FlagOr
663 overflow
664 (modelWord64FlagOr
665 (modelWord64FlagAnd leastBit carry)
666 (modelWord64FlagAnd
667 (modelWord64HighBit multiplicand)
668 (modelWord64FlagNot (modelWord64IsZero nextMultiplier)))))))))
669 (modelWord64ShiftRightOne multiplier)))
670 (modelWord64LeastBit multiplier)))))
671
672def modelWord64MultiplyStateRun =
673 (lambda unrestricted left : (family ModelWord64) .
674 (lambda unrestricted right : (family ModelWord64) .
675 (nat-eliminate
676 (lambda unrestricted current : Nat . (family ModelWord64MultiplyState))
677 (constructor
678 ModelWord64MultiplyState
679 ModelWord64MultiplyStateValue
680 left
681 right
682 modelWord64Zero
683 zero)
684 (lambda unrestricted predecessor : Nat .
685 (lambda unrestricted induction : (family ModelWord64MultiplyState) .
686 (modelWord64MultiplyStep induction)))
687 modelWord64NaturalSixtyFour)))
688
689def modelWord64MultiplyChecked =
690 (lambda unrestricted left : (family ModelWord64) .
691 (lambda unrestricted right : (family ModelWord64) .
692 (eliminate
693 ModelWord64MultiplyState
694 (lambda unrestricted current : (family ModelWord64MultiplyState) .
695 (family ModelWord64MultiplyCheckedResult))
696 (modelWord64MultiplyStateRun left right)
697 (branch
698 ModelWord64MultiplyStateValue
699 multiplicand
700 multiplier
701 product
702 overflow
703 .
704 (nat-eliminate
705 (lambda unrestricted current : Nat . (family ModelWord64MultiplyCheckedResult))
706 (constructor ModelWord64MultiplyCheckedResult ModelWord64MultiplySucceeded product)
707 (lambda unrestricted predecessor : Nat .
708 (lambda unrestricted induction : (family ModelWord64MultiplyCheckedResult) .
709 (constructor ModelWord64MultiplyCheckedResult ModelWord64MultiplyOverflow)))
710 overflow)))))
711
712def modelWord64FromNaturalTruncated =
713 (lambda unrestricted value : Nat .
714 (app
715 (lambda unrestricted quotient1 : Nat .
716 (app
717 (lambda unrestricted quotient2 : Nat .
718 (app
719 (lambda unrestricted quotient3 : Nat .
720 (app
721 (lambda unrestricted quotient4 : Nat .
722 (app
723 (lambda unrestricted quotient5 : Nat .
724 (app
725 (lambda unrestricted quotient6 : Nat .
726 (app
727 (lambda unrestricted quotient7 : Nat .
728 (constructor
729 ModelWord64
730 ModelWord64Value
731 (nat-to-byte
732 (naturalModuloUnchecked value byteNaturalTwoHundredFiftySix))
733 (nat-to-byte
734 (naturalModuloUnchecked quotient1 byteNaturalTwoHundredFiftySix))
735 (nat-to-byte
736 (naturalModuloUnchecked quotient2 byteNaturalTwoHundredFiftySix))
737 (nat-to-byte
738 (naturalModuloUnchecked quotient3 byteNaturalTwoHundredFiftySix))
739 (nat-to-byte
740 (naturalModuloUnchecked quotient4 byteNaturalTwoHundredFiftySix))
741 (nat-to-byte
742 (naturalModuloUnchecked quotient5 byteNaturalTwoHundredFiftySix))
743 (nat-to-byte
744 (naturalModuloUnchecked quotient6 byteNaturalTwoHundredFiftySix))
745 (nat-to-byte
746 (naturalModuloUnchecked quotient7 byteNaturalTwoHundredFiftySix))))
747 (naturalDivideUnchecked quotient6 byteNaturalTwoHundredFiftySix)))
748 (naturalDivideUnchecked quotient5 byteNaturalTwoHundredFiftySix)))
749 (naturalDivideUnchecked quotient4 byteNaturalTwoHundredFiftySix)))
750 (naturalDivideUnchecked quotient3 byteNaturalTwoHundredFiftySix)))
751 (naturalDivideUnchecked quotient2 byteNaturalTwoHundredFiftySix)))
752 (naturalDivideUnchecked quotient1 byteNaturalTwoHundredFiftySix)))
753 (naturalDivideUnchecked value byteNaturalTwoHundredFiftySix)))
754
755-- the natural a word holds (its bytes little-endian); below 2^64, so it is
756-- a word of the build's naturals too
757def modelWord64Natural =
758 (lambda unrestricted value : (family ModelWord64) .
759 (eliminate
760 ModelWord64
761 (lambda unrestricted current : (family ModelWord64) . Nat)
762 value
763 (branch
764 ModelWord64Value
765 b0
766 b1
767 b2
768 b3
769 b4
770 b5
771 b6
772 b7
773 .
774 (naturalAdd
775 (byte-to-nat b0)
776 (naturalMultiply
777 256
778 (naturalAdd
779 (byte-to-nat b1)
780 (naturalMultiply
781 256
782 (naturalAdd
783 (byte-to-nat b2)
784 (naturalMultiply
785 256
786 (naturalAdd
787 (byte-to-nat b3)
788 (naturalMultiply
789 256
790 (naturalAdd
791 (byte-to-nat b4)
792 (naturalMultiply
793 256
794 (naturalAdd
795 (byte-to-nat b5)
796 (naturalMultiply
797 256
798 (naturalAdd (byte-to-nat b6) (naturalMultiply 256 (byte-to-nat b7))))))))))))))))))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.