Accelerator.SM86.ControlEncoding

1module Accelerator.SM86.ControlEncoding
2
3import Accelerator.SM86.Control
4
5family SM86ControlEncodingResult : Type 0
6constructor SM86ControlEncoded
7field unrestricted encodedSM86ControlBytes : Bytes
8constructor SM86ControlEncodingFailed
9field unrestricted sm86ControlEncodingFailureCode : Nat
10
11end-family
12
13def sm86NaturalAdd =
14  (lambda unrestricted left : Nat .
15    (lambda unrestricted right : Nat .
16      (nat-eliminate
17        (lambda unrestricted current : Nat . Nat)
18        left
19        (lambda unrestricted predecessor : Nat .
20          (lambda unrestricted induction : Nat . (succ induction)))
21        right)))
22
23def sm86NaturalDouble =
24  (lambda unrestricted value : Nat . (sm86NaturalAdd value value))
25
26def sm86NaturalTimesEight =
27  (lambda unrestricted value : Nat .
28    (sm86NaturalDouble (sm86NaturalDouble (sm86NaturalDouble value))))
29
30def sm86NaturalTimesSixteen =
31  (lambda unrestricted value : Nat . (sm86NaturalDouble (sm86NaturalTimesEight value)))
32
33def sm86NaturalTimesThirtyTwo =
34  (lambda unrestricted value : Nat . (sm86NaturalDouble (sm86NaturalTimesSixteen value)))
35
36def sm86NaturalPredecessor =
37  (lambda unrestricted value : Nat .
38    (nat-eliminate
39      (lambda unrestricted current : Nat . Nat)
40      zero
41      (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . predecessor))
42      value))
43
44def sm86NaturalSubtract =
45  (lambda unrestricted left : Nat .
46    (lambda unrestricted right : Nat .
47      (nat-eliminate
48        (lambda unrestricted current : Nat . Nat)
49        left
50        (lambda unrestricted predecessor : Nat .
51          (lambda unrestricted induction : Nat . (sm86NaturalPredecessor induction)))
52        right)))
53
54def sm86NaturalSelect =
55  (lambda unrestricted condition : Nat .
56    (lambda unrestricted whenTrue : Nat .
57      (lambda unrestricted whenFalse : Nat .
58        (nat-eliminate
59          (lambda unrestricted current : Nat . Nat)
60          whenFalse
61          (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . whenTrue))
62          condition))))
63
64def sm86YieldBit =
65  (lambda unrestricted yieldMode : (family SM86YieldMode) .
66    (eliminate
67      SM86YieldMode
68      (lambda unrestricted value : (family SM86YieldMode) . Nat)
69      yieldMode
70      (branch SM86Continue . zero)
71      (branch SM86Yield . (succ zero))))
72
73def sm86BarrierCode =
74  (lambda unrestricted barrier : (family SM86Barrier) .
75    (eliminate
76      SM86Barrier
77      (lambda unrestricted value : (family SM86Barrier) . Nat)
78      barrier
79      (branch SM86Barrier0 . (byte-to-nat (byte 0)))
80      (branch SM86Barrier1 . (byte-to-nat (byte 1)))
81      (branch SM86Barrier2 . (byte-to-nat (byte 2)))
82      (branch SM86Barrier3 . (byte-to-nat (byte 3)))
83      (branch SM86Barrier4 . (byte-to-nat (byte 4)))
84      (branch SM86Barrier5 . (byte-to-nat (byte 5)))
85      (branch SM86Barrier6 . (byte-to-nat (byte 6)))
86      (branch SM86BarrierNone . (byte-to-nat (byte 7)))))
87
88def encodeValidatedSM86ControlLE =
89  (lambda unrestricted control : (family SM86Control) .
90    (eliminate
91      SM86Control
92      (lambda unrestricted value : (family SM86Control) . Bytes)
93      control
94      (branch
95        SM86ControlValue
96        stall
97        yieldMode
98        writeBarrier
99        readBarrier
100        waitMask
101        reuseMask
102        .
103        (app
104          (lambda unrestricted stallNatural : Nat .
105            (lambda unrestricted yieldNatural : Nat .
106              (lambda unrestricted writeNatural : Nat .
107                (lambda unrestricted readNatural : Nat .
108                  (lambda unrestricted waitNatural : Nat .
109                    (lambda unrestricted reuseNatural : Nat .
110                      (app
111                        (lambda unrestricted waitHigh : Nat .
112                          (lambda unrestricted waitLow : Nat .
113                            (bytes
114                              (nat-to-byte
115                                (sm86NaturalAdd
116                                  stallNatural
117                                  (sm86NaturalAdd
118                                    (sm86NaturalTimesSixteen yieldNatural)
119                                    (sm86NaturalTimesThirtyTwo writeNatural))))
120                              (nat-to-byte
121                                (sm86NaturalAdd readNatural (sm86NaturalTimesEight waitLow)))
122                              (nat-to-byte
123                                (sm86NaturalAdd waitHigh (sm86NaturalDouble reuseNatural)))
124                              (byte 0))))
125                        (nat-less-than (byte-to-nat (byte 31)) waitNatural)
126                        (sm86NaturalSelect
127                          (nat-less-than (byte-to-nat (byte 31)) waitNatural)
128                          (sm86NaturalSubtract waitNatural (byte-to-nat (byte 32)))
129                          waitNatural))))))))
130          (byte-to-nat stall)
131          (sm86YieldBit yieldMode)
132          (sm86BarrierCode writeBarrier)
133          (sm86BarrierCode readBarrier)
134          (byte-to-nat waitMask)
135          (byte-to-nat reuseMask)))))
136
137def encodeSM86ControlLE =
138  (lambda unrestricted control : (family SM86Control) .
139    (eliminate
140      SM86Control
141      (lambda unrestricted value : (family SM86Control) . (family SM86ControlEncodingResult))
142      control
143      (branch
144        SM86ControlValue
145        stall
146        yieldMode
147        writeBarrier
148        readBarrier
149        waitMask
150        reuseMask
151        .
152        (eliminate
153          SM86ControlResult
154          (lambda unrestricted result : (family SM86ControlResult) .
155            (family SM86ControlEncodingResult))
156          (makeSM86Control stall yieldMode writeBarrier readBarrier waitMask reuseMask)
157          (branch
158            SM86ControlValidated
159            validated
160            .
161            (constructor
162              SM86ControlEncodingResult
163              SM86ControlEncoded
164              (encodeValidatedSM86ControlLE validated)))
165          (branch
166            SM86ControlFailed
167            code
168            .
169            (constructor SM86ControlEncodingResult SM86ControlEncodingFailed code))))))