Model.Word32Logic

1module Model.Word32Logic
2
3import Model.Config
4import Model.Word32
5import Std.Byte
6import Std.Natural
7
8def modelWord32And =
9  (lambda unrestricted left : (family ModelWord32) .
10    (lambda unrestricted right : (family ModelWord32) .
11      (eliminate
12        ModelWord32
13        (lambda unrestricted current : (family ModelWord32) . (family ModelWord32))
14        left
15        (branch
16          ModelWord32Value
17          l0
18          l1
19          l2
20          l3
21          .
22          (eliminate
23            ModelWord32
24            (lambda unrestricted current : (family ModelWord32) . (family ModelWord32))
25            right
26            (branch
27              ModelWord32Value
28              r0
29              r1
30              r2
31              r3
32              .
33              (constructor
34                ModelWord32
35                ModelWord32Value
36                (byteAnd l0 r0)
37                (byteAnd l1 r1)
38                (byteAnd l2 r2)
39                (byteAnd l3 r3))))))))
40
41def modelWord32Or =
42  (lambda unrestricted left : (family ModelWord32) .
43    (lambda unrestricted right : (family ModelWord32) .
44      (eliminate
45        ModelWord32
46        (lambda unrestricted current : (family ModelWord32) . (family ModelWord32))
47        left
48        (branch
49          ModelWord32Value
50          l0
51          l1
52          l2
53          l3
54          .
55          (eliminate
56            ModelWord32
57            (lambda unrestricted current : (family ModelWord32) . (family ModelWord32))
58            right
59            (branch
60              ModelWord32Value
61              r0
62              r1
63              r2
64              r3
65              .
66              (constructor
67                ModelWord32
68                ModelWord32Value
69                (byteOr l0 r0)
70                (byteOr l1 r1)
71                (byteOr l2 r2)
72                (byteOr l3 r3))))))))
73
74def modelWord32Not =
75  (lambda unrestricted value : (family ModelWord32) .
76    (eliminate
77      ModelWord32
78      (lambda unrestricted current : (family ModelWord32) . (family ModelWord32))
79      value
80      (branch
81        ModelWord32Value
82        b0
83        b1
84        b2
85        b3
86        .
87        (constructor
88          ModelWord32
89          ModelWord32Value
90          (byteXor b0 (byte 255))
91          (byteXor b1 (byte 255))
92          (byteXor b2 (byte 255))
93          (byteXor b3 (byte 255))))))
94
95def modelWord32RotateRight =
96  (lambda unrestricted value : (family ModelWord32) .
97    (lambda unrestricted amount : Nat .
98      (app
99        (lambda unrestricted normalized : Nat .
100          (modelWord32Or
101            (modelWord32ShiftRight value normalized)
102            (modelWord32ShiftLeft
103              value
104              (naturalSaturatingSubtract modelWord32NaturalThirtyTwo normalized))))
105        (naturalModuloUnchecked amount modelWord32NaturalThirtyTwo))))
106
107def modelWord32Choose =
108  (lambda unrestricted choose : (family ModelWord32) .
109    (lambda unrestricted whenSet : (family ModelWord32) .
110      (lambda unrestricted whenClear : (family ModelWord32) .
111        (modelWord32Xor
112          (modelWord32And choose whenSet)
113          (modelWord32And (modelWord32Not choose) whenClear)))))
114
115def modelWord32Majority =
116  (lambda unrestricted first : (family ModelWord32) .
117    (lambda unrestricted second : (family ModelWord32) .
118      (lambda unrestricted third : (family ModelWord32) .
119        (modelWord32Xor
120          (modelWord32Xor (modelWord32And first second) (modelWord32And first third))
121          (modelWord32And second third)))))
122
123def modelWord32AddThree =
124  (lambda unrestricted first : (family ModelWord32) .
125    (lambda unrestricted second : (family ModelWord32) .
126      (lambda unrestricted third : (family ModelWord32) .
127        (modelWord32Add (modelWord32Add first second) third))))
128
129def modelWord32AddFour =
130  (lambda unrestricted first : (family ModelWord32) .
131    (lambda unrestricted second : (family ModelWord32) .
132      (lambda unrestricted third : (family ModelWord32) .
133        (lambda unrestricted fourth : (family ModelWord32) .
134          (modelWord32Add (modelWord32AddThree first second third) fourth)))))
135
136def modelWord32AddFive =
137  (lambda unrestricted first : (family ModelWord32) .
138    (lambda unrestricted second : (family ModelWord32) .
139      (lambda unrestricted third : (family ModelWord32) .
140        (lambda unrestricted fourth : (family ModelWord32) .
141          (lambda unrestricted fifth : (family ModelWord32) .
142            (modelWord32Add (modelWord32AddFour first second third fourth) fifth))))))