source: src/ASM/Fetch.ma @ 2222

Last change on this file since 2222 was 2124, checked in by sacerdot, 7 years ago

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