source: src/ASM/Fetch.ma @ 1941

Last change on this file since 1941 was 1941, checked in by mulligan, 8 years ago

Changes to the AssemblyProof? with a few more (large) axioms closed.

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