source: src/ASM/Fetch.ma @ 1591

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

work from today

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