Std.Byte

1module Std.Byte
2
3import Std.Natural
4
5family ByteAddResult : Type 0
6constructor ByteAddResultValue
7field unrestricted byteAddLow : Byte
8field unrestricted byteAddCarry : Nat
9
10end-family
11
12family ByteMultiplyResult : Type 0
13constructor ByteMultiplyResultValue
14field unrestricted byteMultiplyLow : Byte
15field unrestricted byteMultiplyHigh : Byte
16
17end-family
18
19def byteNaturalTwo =
20  (succ (succ zero))
21
22def byteNaturalEight =
23  (byte-to-nat (byte 8))
24
25def byteNaturalTwoHundredFiftySix =
26  (succ (byte-to-nat (byte 255)))
27
28def byteAdd =
29  (lambda unrestricted left : Byte .
30    (lambda unrestricted right : Byte .
31      (app
32        (lambda unrestricted total : Nat .
33          (constructor
34            ByteAddResult
35            ByteAddResultValue
36            -- total is in 0..510. The primitive conversion keeps its low
37            -- eight bits, and its high part is exactly the flag total > 255.
38            -- Avoid general unary division/modulo in this bounded operation.
39            (nat-to-byte total)
40            (nat-less-than (byte-to-nat (byte 255)) total)))
41        (naturalAdd (byte-to-nat left) (byte-to-nat right)))))
42
43def byteMultiply =
44  (lambda unrestricted left : Byte .
45    (lambda unrestricted right : Byte .
46      (app
47        (lambda unrestricted product : Nat .
48          (constructor
49            ByteMultiplyResult
50            ByteMultiplyResultValue
51            (nat-to-byte (naturalModuloUnchecked product byteNaturalTwoHundredFiftySix))
52            (nat-to-byte (naturalDivideUnchecked product byteNaturalTwoHundredFiftySix))))
53        (naturalMultiply (byte-to-nat left) (byte-to-nat right)))))
54
55-- The bit operations are the L21 byte primitives (one machine operation on
56-- every lane). A shift amount is a Nat here, as it always was: an amount of
57-- eight or more yields zero, decided by the primitive comparison so that
58-- `nat-to-byte` never truncates an amount of 256 or more into a small one.
59def byteAnd =
60  (lambda unrestricted left : Byte . (lambda unrestricted right : Byte . (byte-and left right)))
61
62def byteOr =
63  (lambda unrestricted left : Byte . (lambda unrestricted right : Byte . (byte-or left right)))
64
65def byteXor =
66  (lambda unrestricted left : Byte . (lambda unrestricted right : Byte . (byte-xor left right)))
67
68def byteShiftRight =
69  (lambda unrestricted value : Byte .
70    (lambda unrestricted amount : Nat .
71      (nat-eliminate
72        (lambda unrestricted current : Nat . Byte)
73        (byte 0)
74        (lambda unrestricted predecessor : Nat .
75          (lambda unrestricted induction : Byte . (byte-shift-right value (nat-to-byte amount))))
76        (nat-less-than amount byteNaturalEight))))
77
78def byteShiftLeftTruncated =
79  (lambda unrestricted value : Byte .
80    (lambda unrestricted amount : Nat .
81      (nat-eliminate
82        (lambda unrestricted current : Nat . Byte)
83        (byte 0)
84        (lambda unrestricted predecessor : Nat .
85          (lambda unrestricted induction : Byte . (byte-shift-left value (nat-to-byte amount))))
86        (nat-less-than amount byteNaturalEight))))
87
88def byteAddWithCarry =
89  (lambda unrestricted left : Byte .
90    (lambda unrestricted right : Byte .
91      (lambda unrestricted carry : Nat .
92        (eliminate
93          ByteAddResult
94          (lambda unrestricted current : (family ByteAddResult) . (family ByteAddResult))
95          (byteAdd left right)
96          (branch
97            ByteAddResultValue
98            firstLow
99            firstCarry
100            .
101            (eliminate
102              ByteAddResult
103              (lambda unrestricted current : (family ByteAddResult) . (family ByteAddResult))
104              (byteAdd firstLow (nat-to-byte carry))
105              (branch
106                ByteAddResultValue
107                secondLow
108                secondCarry
109                .
110                (constructor
111                  ByteAddResult
112                  ByteAddResultValue
113                  secondLow
114                  (naturalAdd firstCarry secondCarry)))))))))