source: src/ASM/Fetch.ma @ 2119

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

load_code_memory moved to Fetch.ma and proved correct w.r.t. next
(fetching) using Russell

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