source: src/ASM/Fetch.ma @ 1946

Last change on this file since 1946 was 1946, checked in by sacerdot, 9 years ago

\snd half_add => add everywhere

File size: 23.5 KB
Line 
1include "ASM/BitVectorTrie.ma".
2include "ASM/Arithmetic.ma".
3include "ASM/ASM.ma".
4include "basics/russell.ma".
5
6definition bitvector_max_nat ≝
7  λlength: nat.
8    2^length.
9
10definition code_memory_size ≝ bitvector_max_nat 16.
11
12include alias "ASM/BitVectorTrie.ma".
13
14definition next: BitVectorTrie Byte 16 → ∀program_counter: Word. Word × Byte ≝
15  λpmem: BitVectorTrie Byte 16.
16  λpc: Word.
17    〈add … pc (bitvector_of_nat 16 1), lookup … pc pmem (zero …)〉.
18
19lemma Prod_inv_rect_Type0:
20 ∀A,B. ∀P: A × B → Type[0].∀ab.
21  (∀a,b. ab = 〈a,b〉 → P 〈a,b〉) → P ab.
22 #A #B #P * /2/
23qed.
24
25notation > "hvbox('let' 〈ident x,ident y〉 {ident H} ≝ t 'in' s)"
26 with precedence 10
27for @{ Prod_inv_rect_Type0 ??? $t (λ${ident x}.λ${ident y}.λ${ident H}.$s) }.
28
29notation < "hvbox('let' 〈ident x,ident y〉 {ident H} ≝ t 'in' s)"
30 with precedence 10
31for @{ Prod_inv_rect_Type0 $z $w $r $t (λ${ident x}:$X.λ${ident y}:$Y.λ${ident H}:$h.$s) }.
32
33lemma breakup_pair' : ∀A,B,C:Type[0].∀x. ∀R:C → Prop. ∀P:∀a:A.∀b:B. x=〈a,b〉 → C.
34  R (P (\fst x) (\snd x) ?) → R (let 〈a,b〉 {H} ≝ x in P a b H).
35[2: // ]
36#A #B #C *; normalize /2/
37qed.
38
39(* timings taken from SIEMENS *)
40
41definition fetch0: ∀code_memory: BitVectorTrie Byte 16.
42    ∀program_counter: Word. Byte → instruction × Word × nat ≝
43  λpmem.
44  λpc.
45  λv.
46   let 〈b,v〉 ≝ head … v in if b then
47    let 〈b,v〉 ≝ head … v in if b then
48     let 〈b,v〉 ≝ head … v in if b then
49      let 〈b,v〉 ≝ head … v in if b then
50       let 〈b,v〉 ≝ head … v in if b then
51        〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,ACC_A〉)))))), pc〉, 1〉
52       else
53        let 〈b,v〉≝  head … v in if b then
54         let 〈b,v〉≝  head … v in if b then
55          〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),ACC_A〉)))))), pc〉, 1〉
56         else
57          let 〈b,v〉≝  head … v in if b then
58           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉))))), pc〉, 1〉
59          else
60           〈〈RealInstruction (CPL … ACC_A), pc〉, 1〉
61        else
62         let 〈b,v〉≝  head … v in if b then
63          〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT (from_singl … v),ACC_A〉)), pc〉, 2〉
64         else
65          let 〈b,v〉≝  head … v in if b then
66           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
67          else
68           〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT_DPTR,ACC_A〉)), pc〉, 2〉
69      else
70       let 〈b,v〉≝  head … v in if b then
71        〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,REGISTER v〉)))))), pc〉, 1〉
72       else
73        let 〈b,v〉≝  head … v in if b then
74         let 〈b,v〉≝  head … v in if b then
75          〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)))))), pc〉, 1〉
76         else
77          let 〈b,v〉≝  head … v in if b then
78           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉)))))), pc〉, 1〉
79          else
80           〈〈RealInstruction (CLR … ACC_A), pc〉, 1〉
81        else
82         let 〈b,v〉≝  head … v in if b then
83          〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT (from_singl … v)〉)), pc〉, 2〉
84         else
85          let 〈b,v〉≝  head … v in if b then
86           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
87          else
88           〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT_DPTR〉)), pc〉, 2〉
89     else
90      let 〈b,v〉≝  head … v in if b then
91       let 〈b,v〉≝  head … v in if b then
92        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉
93       else
94        let 〈b,v〉≝  head … v in if b then
95         let 〈b,v〉≝  head … v in if b then
96          〈〈RealInstruction (XCHD … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
97         else
98          let 〈b,v〉≝  head … v in if b then
99           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉
100          else
101           〈〈RealInstruction (DA … ACC_A), pc〉, 1〉
102        else
103         let 〈b,v〉≝  head … v in if b then
104          let 〈b,v〉≝  head … v in if b then
105           〈〈RealInstruction (SETB … CARRY), pc〉, 1〉
106          else
107           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SETB … (BIT_ADDR b1)), pc〉, 1〉
108         else
109          let 〈b,v〉≝  head … v in if b then
110           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
111          else
112           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (POP … (DIRECT b1)), pc〉, 2〉
113      else
114       let 〈b,v〉≝  head … v in if b then
115        〈〈RealInstruction (XCH … ACC_A (REGISTER v)), pc〉, 1〉
116       else
117        let 〈b,v〉≝  head … v in if b then
118         let 〈b,v〉≝  head … v in if b then
119          〈〈RealInstruction (XCH … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
120         else
121          let 〈b,v〉≝  head … v in if b then
122           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XCH … ACC_A (DIRECT b1)), pc〉, 1〉
123          else
124           〈〈RealInstruction (SWAP … ACC_A), pc〉, 1〉
125        else
126         let 〈b,v〉≝  head … v in if b then
127          let 〈b,v〉≝  head … v in if b then
128           〈〈RealInstruction (CLR … CARRY), pc〉, 1〉
129          else
130           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (CLR … (BIT_ADDR b1)), pc〉, 1〉
131         else
132          let 〈b,v〉≝  head … v in if b then
133           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
134          else
135           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (PUSH … (DIRECT b1)), pc〉, 2〉
136    else
137     let 〈b,v〉≝  head … v in if b then
138      let 〈b,v〉≝  head … v in if b then
139       let 〈b,v〉≝  head … v in if b then
140        let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (CJNE …  (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
141       else
142        let 〈b,v〉≝  head … v in if b then
143         let 〈b,v〉≝  head … v in if b then
144          let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉
145         else
146          let 〈b,v〉≝  head … v in if b then
147           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (CJNE …  (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉
148          else
149           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
150        else
151         let 〈b,v〉≝  head … v in if b then
152          let 〈b,v〉≝  head … v in if b then
153           〈〈RealInstruction (CPL … CARRY), pc〉, 1〉
154          else
155           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (CPL … (BIT_ADDR b1)), pc〉, 1〉
156         else
157          let 〈b,v〉≝  head … v in if b then
158           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
159          else
160           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
161      else
162       let 〈b,v〉≝  head … v in if b then
163        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉)))))), pc〉, 2〉
164       else
165        let 〈b,v〉≝  head … v in if b then
166         let 〈b,v〉≝  head … v in if b then
167          let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉)))))), pc〉, 2〉
168         else
169          〈〈RealInstruction (MUL … ACC_A ACC_B), pc〉, 4〉
170        else
171         let 〈b,v〉≝  head … v in if b then
172          let 〈b,v〉≝  head … v in if b then
173           〈〈RealInstruction (INC … DPTR), pc〉, 2〉
174          else
175           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉))), pc〉, 1〉
176         else
177          let 〈b,v〉≝  head … v in if b then
178           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
179          else
180           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
181     else
182      let 〈b,v〉≝  head … v in if b then
183       let 〈b,v〉≝  head … v in if b then
184        〈〈RealInstruction (SUBB … ACC_A (REGISTER v)), pc〉, 1〉
185       else
186        let 〈b,v〉≝  head … v in if b then
187         let 〈b,v〉≝  head … v in if b then
188          〈〈RealInstruction (SUBB … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
189         else
190          let 〈b,v〉≝  head … v in if b then
191           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DIRECT b1)), pc〉, 1〉
192          else
193           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DATA b1)), pc〉, 1〉
194        else
195         let 〈b,v〉≝  head … v in if b then
196          let 〈b,v〉≝  head … v in if b then
197           〈〈MOVC … ACC_A (ACC_DPTR), pc〉, 2〉
198          else
199           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inr … 〈BIT_ADDR b1,CARRY〉)), pc〉, 2〉
200         else
201          let 〈b,v〉≝  head … v in if b then
202           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
203          else
204           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉)))), pc〉, 2〉
205      else
206       let 〈b,v〉≝  head … v in if b then
207        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉))))), pc〉, 2〉
208       else
209        let 〈b,v〉≝  head … v in if b then
210         let 〈b,v〉≝  head … v in if b then
211          let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉))))), pc〉, 2〉
212         else
213          let 〈b,v〉≝  head … v in if b then
214           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉))))), pc〉, 2〉
215          else
216           〈〈RealInstruction (DIV … ACC_A ACC_B), pc〉, 4〉
217        else
218         let 〈b,v〉≝  head … v in if b then
219          let 〈b,v〉≝  head … v in if b then
220           〈〈MOVC … ACC_A (ACC_PC), pc〉, 2〉
221          else
222           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
223         else
224          let 〈b,v〉≝  head … v in if b then
225           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
226          else
227           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈SJMP … (RELATIVE b1), pc〉, 2〉
228   else
229    let 〈b,v〉≝  head … v in if b then
230     let 〈b,v〉≝  head … v in if b then
231      let 〈b,v〉≝  head … v in if b then
232       let 〈b,v〉≝  head … v in if b then
233        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉)))))), pc〉, 1〉
234       else
235        let 〈b,v〉≝  head … v in if b then
236         let 〈b,v〉≝  head … v in if b then
237          let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉)))))), pc〉, 1〉
238         else
239          let 〈b,v〉≝  head … v in if b then
240           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉))))), pc〉, 3〉
241          else
242           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉
243        else
244         let 〈b,v〉≝  head … v in if b then
245          let 〈b,v〉≝  head … v in if b then
246           〈〈JMP … INDIRECT_DPTR, pc〉, 2〉
247          else
248           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
249         else
250          let 〈b,v〉≝  head … v in if b then
251           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
252          else
253           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JNZ … (RELATIVE b1)), pc〉, 2〉
254      else
255       let 〈b,v〉≝  head … v in if b then
256        〈〈RealInstruction (XRL … (inl … 〈ACC_A,REGISTER v〉)), pc〉, 1〉
257       else
258        let 〈b,v〉≝  head … v in if b then
259         let 〈b,v〉≝  head … v in if b then
260          〈〈RealInstruction (XRL … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, 1〉
261         else
262          let 〈b,v〉≝  head … v in if b then
263           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉
264          else
265           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉
266        else
267         let 〈b,v〉≝  head … v in if b then
268          let 〈b,v〉≝  head … v in if b then
269           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉
270          else
271           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉
272         else
273          let 〈b,v〉≝  head … v in if b then
274           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
275          else
276           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JZ … (RELATIVE b1)), pc〉, 2〉
277     else
278      let 〈b,v〉≝  head … v in if b then
279       let 〈b,v〉≝  head … v in if b then
280        〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,REGISTER v〉))), pc〉, 1〉
281       else
282        let 〈b,v〉≝  head … v in if b then
283         let 〈b,v〉≝  head … v in if b then
284          〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))), pc〉, 1〉
285         else
286          let 〈b,v〉≝  head … v in if b then
287           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
288          else
289           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
290        else
291         let 〈b,v〉≝  head … v in if b then
292          let 〈b,v〉≝  head … v in if b then
293           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
294          else
295           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
296         else
297          let 〈b,v〉≝  head … v in if b then
298           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
299          else
300           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JNC … (RELATIVE b1)), pc〉, 2〉
301      else
302       let 〈b,v〉≝  head … v in if b then
303        〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,REGISTER v〉))), pc〉, 1〉
304       else
305        let 〈b,v〉≝  head … v in if b then
306         let 〈b,v〉≝  head … v in if b then
307          〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))), pc〉, 1〉
308         else
309          let 〈b,v〉≝  head … v in if b then
310           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
311          else
312           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
313        else
314         let 〈b,v〉≝  head … v in if b then
315          let 〈b,v〉≝  head … v in if b then
316           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
317          else
318           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
319         else
320          let 〈b,v〉≝  head … v in if b then
321           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
322          else
323           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JC … (RELATIVE b1)), pc〉, 2〉
324    else
325     let 〈b,v〉≝  head … v in if b then
326      let 〈b,v〉≝  head … v in if b then
327       let 〈b,v〉≝  head … v in if b then
328        〈〈RealInstruction (ADDC … ACC_A (REGISTER v)), pc〉, 1〉
329       else
330        let 〈b,v〉≝  head … v in if b then
331         let 〈b,v〉≝  head … v in if b then
332          〈〈RealInstruction (ADDC … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
333         else
334          let 〈b,v〉≝  head … v in if b then
335           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DIRECT b1)), pc〉, 1〉
336          else
337           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DATA b1)), pc〉, 1〉
338        else
339         let 〈b,v〉≝  head … v in if b then
340          let 〈b,v〉≝  head … v in if b then
341           〈〈RealInstruction (RLC … ACC_A), pc〉, 1〉
342          else
343           〈〈RealInstruction (RETI …), pc〉, 2〉
344         else
345          let 〈b,v〉≝  head … v in if b then
346           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
347          else
348           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
349      else
350       let 〈b,v〉≝  head … v in if b then
351        〈〈RealInstruction (ADD … ACC_A (REGISTER v)), pc〉, 1〉
352       else
353        let 〈b,v〉≝  head … v in if b then
354         let 〈b,v〉≝  head … v in if b then
355          〈〈RealInstruction (ADD … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
356         else
357          let 〈b,v〉≝  head … v in if b then
358           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DIRECT b1)), pc〉, 1〉
359          else
360           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DATA b1)), pc〉, 1〉
361        else
362         let 〈b,v〉≝  head … v in if b then
363          let 〈b,v〉≝  head … v in if b then
364           〈〈RealInstruction (RL … ACC_A), pc〉, 1〉
365          else
366           〈〈RealInstruction (RET …), pc〉, 2〉
367         else
368          let 〈b,v〉≝  head … v in if b then
369           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
370          else
371           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
372     else
373      let 〈b,v〉≝  head … v in if b then
374       let 〈b,v〉≝  head … v in if b then
375        〈〈RealInstruction (DEC … (REGISTER v)), pc〉, 1〉
376       else
377        let 〈b,v〉≝  head … v in if b then
378         let 〈b,v〉≝  head … v in if b then
379          〈〈RealInstruction (DEC … (INDIRECT (from_singl … v))), pc〉, 1〉
380         else
381          let 〈b,v〉≝  head … v in if b then
382           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (DEC … (DIRECT b1)), pc〉, 1〉
383          else
384           〈〈RealInstruction (DEC … ACC_A), pc〉, 1〉
385        else
386         let 〈b,v〉≝  head … v in if b then
387          let 〈b,v〉≝  head … v in if b then
388           〈〈RealInstruction (RRC … ACC_A), pc〉, 1〉
389          else
390           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉
391         else
392          let 〈b,v〉≝  head … v in if b then
393           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
394          else
395           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
396      else
397       let 〈b,v〉≝  head … v in if b then
398        〈〈RealInstruction (INC … (REGISTER v)), pc〉, 1〉
399       else
400        let 〈b,v〉≝  head … v in if b then
401         let 〈b,v〉≝  head … v in if b then
402          〈〈RealInstruction (INC … (INDIRECT (from_singl … v))), pc〉, 1〉
403         else
404          let 〈b,v〉≝  head … v in if b then
405           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (INC … (DIRECT b1)), pc〉, 1〉
406          else
407           〈〈RealInstruction (INC … ACC_A), pc〉, 1〉
408        else
409         let 〈b,v〉≝  head … v in if b then
410          let 〈b,v〉≝  head … v in if b then
411           〈〈RealInstruction (RR … ACC_A), pc〉, 1〉
412          else
413           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉
414         else
415          let 〈b,v〉≝  head … v in if b then
416           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
417          else
418           〈〈RealInstruction (NOP …), pc〉, 1〉.
419  %
420qed.
421
422definition fetch: ∀code_memory: BitVectorTrie Byte 16.
423    ∀program_counter: Word. instruction × Word × nat ≝
424  λpmem: BitVectorTrie Byte 16.
425  λpc: Word.
426  let 〈word, byte〉 ≝ next pmem pc in
427    fetch0 pmem word byte.
Note: See TracBrowser for help on using the repository browser.