source: src/ASM/Fetch.ma @ 3033

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

code_memory added to labelled_object_code to avoid recomputing it every time.
This gives a major speed up in the semantics of the extracted code.

File size: 30.2 KB
Line 
1(*include "ASM/BitVectorTrie.ma".*)
2include "ASM/Arithmetic.ma".
3include "ASM/ASM.ma". (* includes "ASM/BitVectorTrie.ma". *)
4include "basics/russell.ma".
5
6(***** Pseudo-code ******)
7
8definition inefficient_address_of_word_labels_code_mem ≝
9  λcode_mem : list labelled_instruction.
10  λid: Identifier.
11    bitvector_of_nat 16 (index_of ? (instruction_matches_identifier ?? id) code_mem).
12
13lemma inefficient_address_of_word_labels_None: ∀i,id,instr_list.
14 occurs_exactly_once ?? id (instr_list@[〈None …,i〉]) →
15  inefficient_address_of_word_labels_code_mem instr_list id =
16  inefficient_address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
17 #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
18 >(index_of_internal_None ?????? H) %
19qed.
20
21lemma inefficient_address_of_word_labels_Some_miss: ∀i,id,id',instr_list.
22 eq_identifier ? id' id = false →
23  occurs_exactly_once ?? id (instr_list@[〈Some ? id',i〉]) →
24   inefficient_address_of_word_labels_code_mem instr_list id =
25   inefficient_address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.
26 #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
27 >(index_of_internal_Some_miss ???????? H) [ @refl | // ]
28qed.
29
30lemma inefficient_address_of_word_labels_Some_hit: ∀i,id,instr_list.
31  occurs_exactly_once ?? id (instr_list@[〈Some ? id,i〉]) →
32   inefficient_address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id
33   = bitvector_of_nat … (|instr_list|).
34 #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)?);
35 >(index_of_internal_Some_hit ?????? H) <plus_n_O @refl
36qed.
37
38(* label_map: identifier ↦ pseudo program counter *)
39definition label_map ≝ identifier_map ASMTag ℕ.
40
41(* The function that creates the label-to-address map *)
42definition create_label_cost_map0: ∀program:list labelled_instruction.
43  (Σlabels_costs:label_map × (BitVectorTrie costlabel 16). (* Both on ppcs *)
44    let labels ≝ \fst labels_costs in
45    (∀l.occurs_exactly_once ?? l program →
46      bitvector_of_nat ? (lookup_def ?? labels l 0) =
47       inefficient_address_of_word_labels_code_mem program l) ∧
48    (∀l.occurs_exactly_once ?? l program →lookup_def ?? labels l 0 < |program|)
49  ) ≝
50  λprogram.
51  \fst (pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)
52  (λprefix.Σlabels_costs_ppc:label_map × (BitVectorTrie costlabel 16) × ℕ.
53    let 〈labels,costs,ppc〉 ≝ labels_costs_ppc in
54    ppc = |prefix| ∧
55    ((∀l.occurs_exactly_once ?? l prefix →
56      bitvector_of_nat ? (lookup_def ?? labels l 0) =
57       inefficient_address_of_word_labels_code_mem prefix l) ∧
58    (∀l.occurs_exactly_once ?? l prefix → lookup_def ?? labels l 0 < |program|)))
59  program
60  (λprefix.λx.λtl.λprf.λlabels_costs_ppc.
61   let 〈labels,costs,ppc〉 ≝ pi1 ?? labels_costs_ppc in
62   let 〈label,instr〉 ≝ x in
63   let labels ≝
64     match label with
65     [ None   ⇒ labels
66     | Some l ⇒ add … labels l ppc
67     ] in
68   let costs ≝
69     match instr with
70     [ Cost cost ⇒ insert … (bitvector_of_nat ? ppc) cost costs
71     | _ ⇒ costs ] in
72      〈labels,costs,S ppc〉
73   ) 〈(empty_map …),(Stub ??),0〉)).
74[ normalize nodelta lapply (pi2 … labels_costs_ppc) >p >p1 normalize nodelta *
75  #IH1 * #IH2 #IH3 -labels_costs_ppc % [>IH1 >length_append <plus_n_Sm <plus_n_O %]
76 inversion label [#EQ | #l #EQ]
77 [ % #lbl
78   [ #Hocc <inefficient_address_of_word_labels_None [2: @Hocc] normalize nodelta
79     >occurs_exactly_once_None in Hocc; @IH2
80   | #Hocc normalize nodelta >occurs_exactly_once_None in Hocc; @IH3 ]
81 | %
82   #lbl normalize nodelta inversion (eq_identifier ? lbl l)
83    [1,3: #Heq #Hocc >(eq_identifier_eq … Heq)
84     [ >inefficient_address_of_word_labels_Some_hit
85       [ >IH1 >lookup_def_add_hit %
86       | <(eq_identifier_eq … Heq) in Hocc; //
87       ]
88     | >lookup_def_add_hit >IH1 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
89     ]
90    |*: #Hneq #Hocc
91     cut (occurs_exactly_once … lbl prefix)
92     [1,3: >occurs_exactly_once_Some_eq in Hocc; >eq_identifier_sym >Hneq // ]
93     #Hocc' lapply (IH2 lbl ?) try assumption
94     [ <inefficient_address_of_word_labels_Some_miss //
95       >lookup_def_add_miss // % @neq_identifier_neq @Hneq
96     | >lookup_def_add_miss /2/
97     ]
98   ]
99 ]
100| @pair_elim * #labels #costs #ppc #EQ destruct normalize nodelta % try %
101  #l #abs cases (abs)
102| cases (foldl_strong ? (λ_.Σx.?) ???) * * #labels #costs #ppc normalize nodelta *
103  #_ #H @H
104]
105qed.
106
107(* The function that creates the label-to-address map *)
108definition create_label_cost_map: ∀program:list labelled_instruction.
109  label_map × (BitVectorTrie costlabel 16) ≝
110    λprogram.
111      pi1 … (create_label_cost_map0 program).
112
113theorem create_label_cost_map_ok:
114 ∀instr_list.
115   let labels ≝ \fst (create_label_cost_map instr_list) in
116    ((∀id. occurs_exactly_once ??  id instr_list →
117     (bitvector_of_nat ? (lookup_def ?? labels id 0) = inefficient_address_of_word_labels_code_mem instr_list id))
118    ∧
119     (∀id. occurs_exactly_once ?? id instr_list → lookup_def ?? labels id 0 < |instr_list|)).
120 #p change with (pi1 … (create_label_cost_map0 ?)) in match (create_label_cost_map ?);
121 @pi2
122qed.
123
124definition address_of_word_labels :
125 list labelled_instruction → Identifier → Word
126
127  λcode_mem : list labelled_instruction.
128  λid: Identifier.
129   let labels ≝ \fst (create_label_cost_map code_mem) in
130    bitvector_of_nat 16 (lookup_def ASMTag ℕ labels id O).
131
132lemma address_of_word_labels_None: ∀i,id,instr_list.
133 occurs_exactly_once ?? id (instr_list@[〈None …,i〉]) →
134  address_of_word_labels instr_list id =
135  address_of_word_labels (instr_list@[〈None …,i〉]) id.
136 #i #id #instr_list #H
137 whd in match address_of_word_labels; normalize nodelta
138 lapply (create_label_cost_map_ok (instr_list@[〈None …,i〉])) * #K' #_
139 lapply (create_label_cost_map_ok instr_list) * #K #_
140 >K' // >K // <inefficient_address_of_word_labels_None //
141qed.
142
143lemma address_of_word_labels_Some_miss: ∀i,id,id',instr_list.
144 eq_identifier ? id' id = false →
145  occurs_exactly_once ?? id (instr_list@[〈Some ? id',i〉]) →
146   address_of_word_labels instr_list id =
147   address_of_word_labels (instr_list@[〈Some … id',i〉]) id.
148 #i #id #id' #instr_list #H1 #H2
149 whd in match address_of_word_labels; normalize nodelta
150 lapply (create_label_cost_map_ok (instr_list@[〈Some … id',i〉])) * #K' #_
151 lapply (create_label_cost_map_ok instr_list) * #K #_
152 >K' // >K
153 [2: lapply (occurs_exactly_once_Some ?????? H2) >H1 #H @H ]
154 @inefficient_address_of_word_labels_Some_miss //
155qed.
156
157lemma address_of_word_labels_Some_hit: ∀i,id,instr_list.
158  occurs_exactly_once ?? id (instr_list@[〈Some ? id,i〉]) →
159   address_of_word_labels (instr_list@[〈Some … id,i〉]) id
160   = bitvector_of_nat … (|instr_list|).
161 #i #id #instr_list #H
162 whd in match address_of_word_labels; normalize nodelta
163 lapply (create_label_cost_map_ok (instr_list@[〈Some … id,i〉])) * #K #_
164 >K // @inefficient_address_of_word_labels_Some_hit //
165qed.
166
167(***** Object-code *******)
168
169definition bitvector_max_nat ≝
170  λlength: nat.
171    2^length.
172
173definition code_memory_size ≝ bitvector_max_nat 16.
174
175lemma Prod_inv_rect_Type0:
176 ∀A,B. ∀P: A × B → Type[0].∀ab.
177  (∀a,b. ab = 〈a,b〉 → P 〈a,b〉) → P ab.
178 #A #B #P * /2/
179qed.
180
181notation > "hvbox('let' 〈ident x,ident y〉 {ident H} ≝ t 'in' s)"
182 with precedence 10
183for @{ Prod_inv_rect_Type0 ??? $t (λ${ident x}.λ${ident y}.λ${ident H}.$s) }.
184
185notation < "hvbox('let' 〈ident x,ident y〉 {ident H} ≝ t 'in' s)"
186 with precedence 10
187for @{ Prod_inv_rect_Type0 $z $w $r $t (λ${ident x}:$X.λ${ident y}:$Y.λ${ident H}:$h.$s) }.
188
189lemma breakup_pair' : ∀A,B,C:Type[0].∀x. ∀R:C → Prop. ∀P:∀a:A.∀b:B. x=〈a,b〉 → C.
190  R (P (\fst x) (\snd x) ?) → R (let 〈a,b〉 {H} ≝ x in P a b H).
191[2: // ]
192#A #B #C *; normalize /2/
193qed.
194
195(* timings taken from SIEMENS *)
196
197definition fetch0: ∀code_memory: BitVectorTrie Byte 16.
198    ∀program_counter: Word. Byte → instruction × Word × nat ≝
199  λpmem.
200  λpc.
201  λv.
202   let 〈b,v〉 ≝ head … v in if b then
203    let 〈b,v〉 ≝ head … v in if b then
204     let 〈b,v〉 ≝ head … v in if b then
205      let 〈b,v〉 ≝ head … v in if b then
206       let 〈b,v〉 ≝ head … v in if b then
207        〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,ACC_A〉)))))), pc〉, 1〉
208       else
209        let 〈b,v〉≝  head … v in if b then
210         let 〈b,v〉≝  head … v in if b then
211          〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),ACC_A〉)))))), pc〉, 1〉
212         else
213          let 〈b,v〉≝  head … v in if b then
214           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉))))), pc〉, 1〉
215          else
216           〈〈RealInstruction (CPL … ACC_A), pc〉, 1〉
217        else
218         let 〈b,v〉≝  head … v in if b then
219          〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT (from_singl … v),ACC_A〉)), pc〉, 2〉
220         else
221          let 〈b,v〉≝  head … v in if b then
222           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
223          else
224           〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT_DPTR,ACC_A〉)), pc〉, 2〉
225      else
226       let 〈b,v〉≝  head … v in if b then
227        〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,REGISTER v〉)))))), pc〉, 1〉
228       else
229        let 〈b,v〉≝  head … v in if b then
230         let 〈b,v〉≝  head … v in if b then
231          〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)))))), pc〉, 1〉
232         else
233          let 〈b,v〉≝  head … v in if b then
234           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉)))))), pc〉, 1〉
235          else
236           〈〈RealInstruction (CLR … ACC_A), pc〉, 1〉
237        else
238         let 〈b,v〉≝  head … v in if b then
239          〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT (from_singl … v)〉)), pc〉, 2〉
240         else
241          let 〈b,v〉≝  head … v in if b then
242           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
243          else
244           〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT_DPTR〉)), pc〉, 2〉
245     else
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 (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉
249       else
250        let 〈b,v〉≝  head … v in if b then
251         let 〈b,v〉≝  head … v in if b then
252          〈〈RealInstruction (XCHD … ACC_A (INDIRECT (from_singl … v))), 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 (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉
256          else
257           〈〈RealInstruction (DA … ACC_A), 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           〈〈RealInstruction (SETB … CARRY), pc〉, 1〉
262          else
263           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SETB … (BIT_ADDR b1)), pc〉, 1〉
264         else
265          let 〈b,v〉≝  head … v in if b then
266           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
267          else
268           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (POP … (DIRECT b1)), pc〉, 2〉
269      else
270       let 〈b,v〉≝  head … v in if b then
271        〈〈RealInstruction (XCH … 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 (XCH … 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 (XCH … ACC_A (DIRECT b1)), pc〉, 1〉
279          else
280           〈〈RealInstruction (SWAP … ACC_A), pc〉, 1〉
281        else
282         let 〈b,v〉≝  head … v in if b then
283          let 〈b,v〉≝  head … v in if b then
284           〈〈RealInstruction (CLR … CARRY), pc〉, 1〉
285          else
286           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (CLR … (BIT_ADDR b1)), 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 (([[true;true;false]]) @@ b1)), pc〉, 2〉
290          else
291           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (PUSH … (DIRECT 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       let 〈b,v〉≝  head … v in if b then
296        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〉
297       else
298        let 〈b,v〉≝  head … v in if b then
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 (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉
301         else
302          let 〈b,v〉≝  head … v in if b then
303           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〉
304          else
305           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〉
306        else
307         let 〈b,v〉≝  head … v in if b then
308          let 〈b,v〉≝  head … v in if b then
309           〈〈RealInstruction (CPL … CARRY), pc〉, 1〉
310          else
311           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (CPL … (BIT_ADDR b1)), pc〉, 1〉
312         else
313          let 〈b,v〉≝  head … v in if b then
314           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
315          else
316           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
317      else
318       let 〈b,v〉≝  head … v in if b then
319        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉)))))), pc〉, 2〉
320       else
321        let 〈b,v〉≝  head … v in if b then
322         let 〈b,v〉≝  head … v in if b then
323          let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉)))))), pc〉, 2〉
324         else
325          〈〈RealInstruction (MUL … ACC_A ACC_B), pc〉, 4〉
326        else
327         let 〈b,v〉≝  head … v in if b then
328          let 〈b,v〉≝  head … v in if b then
329           〈〈RealInstruction (INC … DPTR), pc〉, 2〉
330          else
331           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉))), 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 (([[true;false;true]]) @@ b1)), pc〉, 2〉
335          else
336           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,N_BIT_ADDR 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 (SUBB … 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 (SUBB … 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 (SUBB … ACC_A (DIRECT b1)), pc〉, 1〉
348          else
349           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SUBB … 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           〈〈MOVC … ACC_A (ACC_DPTR), pc〉, 2〉
354          else
355           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inr … 〈BIT_ADDR b1,CARRY〉)), pc〉, 2〉
356         else
357          let 〈b,v〉≝  head … v in if b then
358           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
359          else
360           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〉
361      else
362       let 〈b,v〉≝  head … v in if b then
363        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉))))), pc〉, 2〉
364       else
365        let 〈b,v〉≝  head … v in if b then
366         let 〈b,v〉≝  head … v in if b then
367          let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉))))), pc〉, 2〉
368         else
369          let 〈b,v〉≝  head … v in if b then
370           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〉
371          else
372           〈〈RealInstruction (DIV … ACC_A ACC_B), pc〉, 4〉
373        else
374         let 〈b,v〉≝  head … v in if b then
375          let 〈b,v〉≝  head … v in if b then
376           〈〈MOVC … ACC_A (ACC_PC), pc〉, 2〉
377          else
378           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
379         else
380          let 〈b,v〉≝  head … v in if b then
381           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
382          else
383           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈SJMP … (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       let 〈b,v〉≝  head … v in if b then
389        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,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          let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉)))))), pc〉, 1〉
394         else
395          let 〈b,v〉≝  head … v in if b then
396           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〉
397          else
398           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉
399        else
400         let 〈b,v〉≝  head … v in if b then
401          let 〈b,v〉≝  head … v in if b then
402           〈〈JMP … INDIRECT_DPTR, pc〉, 2〉
403          else
404           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
405         else
406          let 〈b,v〉≝  head … v in if b then
407           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
408          else
409           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JNZ … (RELATIVE b1)), pc〉, 2〉
410      else
411       let 〈b,v〉≝  head … v in if b then
412        〈〈RealInstruction (XRL … (inl … 〈ACC_A,REGISTER v〉)), 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 (XRL … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, 1〉
417         else
418          let 〈b,v〉≝  head … v in if b then
419           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉
420          else
421           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉
422        else
423         let 〈b,v〉≝  head … v in if b then
424          let 〈b,v〉≝  head … v in if b then
425           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〉
426          else
427           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉
428         else
429          let 〈b,v〉≝  head … v in if b then
430           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
431          else
432           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JZ … (RELATIVE b1)), pc〉, 2〉
433     else
434      let 〈b,v〉≝  head … v in if b then
435       let 〈b,v〉≝  head … v in if b then
436        〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,REGISTER v〉))), 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 (ANL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))), pc〉, 1〉
441         else
442          let 〈b,v〉≝  head … v in if b then
443           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
444          else
445           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
446        else
447         let 〈b,v〉≝  head … v in if b then
448          let 〈b,v〉≝  head … v in if b then
449           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〉
450          else
451           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
452         else
453          let 〈b,v〉≝  head … v in if b then
454           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
455          else
456           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JNC … (RELATIVE b1)), pc〉, 2〉
457      else
458       let 〈b,v〉≝  head … v in if b then
459        〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,REGISTER v〉))), 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 (ORL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))), pc〉, 1〉
464         else
465          let 〈b,v〉≝  head … v in if b then
466           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
467          else
468           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
469        else
470         let 〈b,v〉≝  head … v in if b then
471          let 〈b,v〉≝  head … v in if b then
472           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〉
473          else
474           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
475         else
476          let 〈b,v〉≝  head … v in if b then
477           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
478          else
479           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JC … (RELATIVE b1)), pc〉, 2〉
480    else
481     let 〈b,v〉≝  head … v in if b then
482      let 〈b,v〉≝  head … v in if b then
483       let 〈b,v〉≝  head … v in if b then
484        〈〈RealInstruction (ADDC … ACC_A (REGISTER v)), pc〉, 1〉
485       else
486        let 〈b,v〉≝  head … v in if b then
487         let 〈b,v〉≝  head … v in if b then
488          〈〈RealInstruction (ADDC … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
489         else
490          let 〈b,v〉≝  head … v in if b then
491           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DIRECT b1)), pc〉, 1〉
492          else
493           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DATA b1)), pc〉, 1〉
494        else
495         let 〈b,v〉≝  head … v in if b then
496          let 〈b,v〉≝  head … v in if b then
497           〈〈RealInstruction (RLC … ACC_A), pc〉, 1〉
498          else
499           〈〈RealInstruction (RETI …), pc〉, 2〉
500         else
501          let 〈b,v〉≝  head … v in if b then
502           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
503          else
504           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〉
505      else
506       let 〈b,v〉≝  head … v in if b then
507        〈〈RealInstruction (ADD … ACC_A (REGISTER v)), pc〉, 1〉
508       else
509        let 〈b,v〉≝  head … v in if b then
510         let 〈b,v〉≝  head … v in if b then
511          〈〈RealInstruction (ADD … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
512         else
513          let 〈b,v〉≝  head … v in if b then
514           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DIRECT b1)), pc〉, 1〉
515          else
516           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DATA b1)), pc〉, 1〉
517        else
518         let 〈b,v〉≝  head … v in if b then
519          let 〈b,v〉≝  head … v in if b then
520           〈〈RealInstruction (RL … ACC_A), pc〉, 1〉
521          else
522           〈〈RealInstruction (RET …), pc〉, 2〉
523         else
524          let 〈b,v〉≝  head … v in if b then
525           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
526          else
527           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〉
528     else
529      let 〈b,v〉≝  head … v in if b then
530       let 〈b,v〉≝  head … v in if b then
531        〈〈RealInstruction (DEC … (REGISTER v)), pc〉, 1〉
532       else
533        let 〈b,v〉≝  head … v in if b then
534         let 〈b,v〉≝  head … v in if b then
535          〈〈RealInstruction (DEC … (INDIRECT (from_singl … v))), pc〉, 1〉
536         else
537          let 〈b,v〉≝  head … v in if b then
538           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (DEC … (DIRECT b1)), pc〉, 1〉
539          else
540           〈〈RealInstruction (DEC … ACC_A), pc〉, 1〉
541        else
542         let 〈b,v〉≝  head … v in if b then
543          let 〈b,v〉≝  head … v in if b then
544           〈〈RealInstruction (RRC … ACC_A), pc〉, 1〉
545          else
546           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉
547         else
548          let 〈b,v〉≝  head … v in if b then
549           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
550          else
551           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〉
552      else
553       let 〈b,v〉≝  head … v in if b then
554        〈〈RealInstruction (INC … (REGISTER v)), pc〉, 1〉
555       else
556        let 〈b,v〉≝  head … v in if b then
557         let 〈b,v〉≝  head … v in if b then
558          〈〈RealInstruction (INC … (INDIRECT (from_singl … v))), pc〉, 1〉
559         else
560          let 〈b,v〉≝  head … v in if b then
561           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (INC … (DIRECT b1)), pc〉, 1〉
562          else
563           〈〈RealInstruction (INC … ACC_A), pc〉, 1〉
564        else
565         let 〈b,v〉≝  head … v in if b then
566          let 〈b,v〉≝  head … v in if b then
567           〈〈RealInstruction (RR … ACC_A), pc〉, 1〉
568          else
569           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉
570         else
571          let 〈b,v〉≝  head … v in if b then
572           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
573          else
574           〈〈RealInstruction (NOP …), pc〉, 1〉.
575  %
576qed.
577
578definition fetch: ∀code_memory: BitVectorTrie Byte 16.
579    ∀program_counter: Word. instruction × Word × nat ≝
580  λpmem: BitVectorTrie Byte 16.
581  λpc: Word.
582  let 〈word, byte〉 ≝ next pmem pc in
583    fetch0 pmem word byte.
Note: See TracBrowser for help on using the repository browser.