source: src/ASM/Fetch.ma @ 2498

Last change on this file since 2498 was 2498, checked in by mckinna, 7 years ago

Refactor:
Typedefs object_code and costlabel_map lifted out from ASMCostsSplit.ma
Dependencies simplified.

File size: 32.5 KB
Line 
1include "ASM/BitVectorTrie.ma".
2include "ASM/Arithmetic.ma".
3include "ASM/ASM.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
41definition costlabel_map ≝ BitVectorTrie costlabel 16. 
42
43(* The function that creates the label-to-address map *)
44definition create_label_cost_map0: ∀program:list labelled_instruction.
45  (Σlabels_costs:label_map × costlabel_map. (* Both on ppcs *)
46    let labels ≝ \fst labels_costs in
47    (∀l.occurs_exactly_once ?? l program →
48      bitvector_of_nat ? (lookup_def ?? labels l 0) =
49       inefficient_address_of_word_labels_code_mem program l) ∧
50    (∀l.occurs_exactly_once ?? l program →lookup_def ?? labels l 0 < |program|)
51  ) ≝
52  λprogram.
53  \fst (pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)
54  (λprefix.Σlabels_costs_ppc:label_map × costlabel_map × ℕ.
55    let 〈labels,costs,ppc〉 ≝ labels_costs_ppc in
56    ppc = |prefix| ∧
57    ((∀l.occurs_exactly_once ?? l prefix →
58      bitvector_of_nat ? (lookup_def ?? labels l 0) =
59       inefficient_address_of_word_labels_code_mem prefix l) ∧
60    (∀l.occurs_exactly_once ?? l prefix → lookup_def ?? labels l 0 < |program|)))
61  program
62  (λprefix.λx.λtl.λprf.λlabels_costs_ppc.
63   let 〈labels,costs,ppc〉 ≝ pi1 ?? labels_costs_ppc in
64   let 〈label,instr〉 ≝ x in
65   let labels ≝
66     match label with
67     [ None   ⇒ labels
68     | Some l ⇒ add … labels l ppc
69     ] in
70   let costs ≝
71     match instr with
72     [ Cost cost ⇒ insert … (bitvector_of_nat ? ppc) cost costs
73     | _ ⇒ costs ] in
74      〈labels,costs,S ppc〉
75   ) 〈(empty_map …),(Stub ??),0〉)).
76[ normalize nodelta lapply (pi2 … labels_costs_ppc) >p >p1 normalize nodelta *
77  #IH1 * #IH2 #IH3 -labels_costs_ppc % [>IH1 >length_append <plus_n_Sm <plus_n_O %]
78 inversion label [#EQ | #l #EQ]
79 [ % #lbl
80   [ #Hocc <inefficient_address_of_word_labels_None [2: @Hocc] normalize nodelta
81     >occurs_exactly_once_None in Hocc; @IH2
82   | #Hocc normalize nodelta >occurs_exactly_once_None in Hocc; @IH3 ]
83 | %
84   #lbl normalize nodelta inversion (eq_identifier ? lbl l)
85    [1,3: #Heq #Hocc >(eq_identifier_eq … Heq)
86     [ >inefficient_address_of_word_labels_Some_hit
87       [ >IH1 >lookup_def_add_hit %
88       | <(eq_identifier_eq … Heq) in Hocc; //
89       ]
90     | >lookup_def_add_hit >IH1 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
91     ]
92    |*: #Hneq #Hocc
93     cut (occurs_exactly_once … lbl prefix)
94     [1,3: >occurs_exactly_once_Some_eq in Hocc; >eq_identifier_sym >Hneq // ]
95     #Hocc' lapply (IH2 lbl ?) try assumption
96     [ <inefficient_address_of_word_labels_Some_miss //
97       >lookup_def_add_miss // % @neq_identifier_neq @Hneq
98     | >lookup_def_add_miss /2/
99     ]
100   ]
101 ]
102| @pair_elim * #labels #costs #ppc #EQ destruct normalize nodelta % try %
103  #l #abs cases (abs)
104| cases (foldl_strong ? (λ_.Σx.?) ???) * * #labels #costs #ppc normalize nodelta *
105  #_ #H @H
106]
107qed.
108
109(* The function that creates the label-to-address map *)
110definition create_label_cost_map: ∀program:list labelled_instruction.
111  label_map × costlabel_map ≝
112    λprogram.
113      pi1 … (create_label_cost_map0 program).
114
115theorem create_label_cost_map_ok:
116 ∀instr_list.
117   let labels ≝ \fst (create_label_cost_map instr_list) in
118    ((∀id. occurs_exactly_once ??  id instr_list →
119     (bitvector_of_nat ? (lookup_def ?? labels id 0) = inefficient_address_of_word_labels_code_mem instr_list id))
120    ∧
121     (∀id. occurs_exactly_once ?? id instr_list → lookup_def ?? labels id 0 < |instr_list|)).
122 #p change with (pi1 … (create_label_cost_map0 ?)) in match (create_label_cost_map ?);
123 @pi2
124qed.
125
126definition address_of_word_labels :
127 list labelled_instruction → Identifier → Word
128
129  λcode_mem : list labelled_instruction.
130  λid: Identifier.
131   let labels ≝ \fst (create_label_cost_map code_mem) in
132    bitvector_of_nat 16 (lookup_def ASMTag ℕ labels id O).
133
134lemma address_of_word_labels_None: ∀i,id,instr_list.
135 occurs_exactly_once ?? id (instr_list@[〈None …,i〉]) →
136  address_of_word_labels instr_list id =
137  address_of_word_labels (instr_list@[〈None …,i〉]) id.
138 #i #id #instr_list #H
139 whd in match address_of_word_labels; normalize nodelta
140 lapply (create_label_cost_map_ok (instr_list@[〈None …,i〉])) * #K' #_
141 lapply (create_label_cost_map_ok instr_list) * #K #_
142 >K' // >K // <inefficient_address_of_word_labels_None //
143qed.
144
145lemma address_of_word_labels_Some_miss: ∀i,id,id',instr_list.
146 eq_identifier ? id' id = false →
147  occurs_exactly_once ?? id (instr_list@[〈Some ? id',i〉]) →
148   address_of_word_labels instr_list id =
149   address_of_word_labels (instr_list@[〈Some … id',i〉]) id.
150 #i #id #id' #instr_list #H1 #H2
151 whd in match address_of_word_labels; normalize nodelta
152 lapply (create_label_cost_map_ok (instr_list@[〈Some … id',i〉])) * #K' #_
153 lapply (create_label_cost_map_ok instr_list) * #K #_
154 >K' // >K
155 [2: lapply (occurs_exactly_once_Some ?????? H2) >H1 #H @H ]
156 @inefficient_address_of_word_labels_Some_miss //
157qed.
158
159lemma address_of_word_labels_Some_hit: ∀i,id,instr_list.
160  occurs_exactly_once ?? id (instr_list@[〈Some ? id,i〉]) →
161   address_of_word_labels (instr_list@[〈Some … id,i〉]) id
162   = bitvector_of_nat … (|instr_list|).
163 #i #id #instr_list #H
164 whd in match address_of_word_labels; normalize nodelta
165 lapply (create_label_cost_map_ok (instr_list@[〈Some … id,i〉])) * #K #_
166 >K // @inefficient_address_of_word_labels_Some_hit //
167qed.
168
169(***** Object-code *******)
170
171definition object_code ≝ list Byte.
172
173definition bitvector_max_nat ≝
174  λlength: nat.
175    2^length.
176
177definition code_memory_size ≝ bitvector_max_nat 16.
178
179include alias "ASM/BitVectorTrie.ma".
180include alias "ASM/Arithmetic.ma".
181
182definition next: BitVectorTrie Byte 16 → ∀program_counter: Word. Word × Byte ≝
183  λpmem: BitVectorTrie Byte 16.
184  λpc: Word.
185    〈add … pc (bitvector_of_nat 16 1), lookup … pc pmem (zero …)〉.
186
187definition load_code_memory0:
188 ∀program: object_code. Σres: BitVectorTrie Byte 16.
189  let program_size ≝ |program| in
190   program_size ≤ 2^16 →
191    ∀pc. ∀pc_ok: pc < program_size.
192     nth_safe ? pc program pc_ok = \snd (next res (bitvector_of_nat … pc))
193
194 λprogram. \snd
195  (foldl_strong ?
196   (λprefix.
197     Σres: nat × (BitVectorTrie Byte 16).
198      let 〈i,mem〉 ≝ res in
199      i = |prefix| ∧
200      (i ≤ 2^16 →
201        ∀pc. ∀pc_ok: pc < |prefix|.
202         nth_safe ? pc prefix pc_ok = \snd (next mem (bitvector_of_nat … pc))))
203   program
204   (λprefix,v,tl,prf,i_mem.
205     let 〈i,mem〉 ≝ i_mem in
206      〈S i,insert … (bitvector_of_nat … i) v mem〉)
207  〈0,Stub Byte 16〉).
208[3: cases (foldl_strong ? (λprefix.Σres.?) ???) * #i #mem * #H1 >H1 #H2 @H2
209| % // #_ #pc #abs @⊥ @(absurd … abs (not_le_Sn_O …))
210| cases i_mem in p; * #i' #mem' #H #EQ destruct(EQ) cases H -H #H1 #H2 %
211  [ >length_append >H1 normalize //
212  | #LE #pc #pc_ok
213    cases (le_to_or_lt_eq … pc_ok)
214    [2: #EQ_Spc >(?: pc = |prefix| + 0) in pc_ok;
215      [2: >length_append in EQ_Spc; normalize #EQ @injective_S >EQ //]
216      #pc_ok <nth_safe_prepend [2: //] whd in ⊢ (??%?);
217      <H1 <plus_n_O whd in ⊢ (???%); //
218    | >length_append <plus_n_Sm <plus_n_O #LT <shift_nth_prefix [2: /2/]
219      >H2 [2: @(transitive_le … LE) //]
220      cut (pc ≠ i) [ >H1 @lt_to_not_eq @lt_S_S_to_lt //] #NEQ
221      whd in ⊢ (??%%); @sym_eq @lookup_insert_miss >eq_bv_false %
222      #EQ @(absurd ?? NEQ) @(eq_bitvector_of_nat_to_eq … EQ) try assumption
223      @(transitive_lt … LE) >H1 @lt_S_S_to_lt //]]
224qed.
225
226definition load_code_memory: object_code → BitVectorTrie Byte 16 ≝
227 λprogram.load_code_memory0 program.
228
229lemma load_code_memory_ok:
230 ∀program: object_code.
231  let program_size ≝ |program| in
232   program_size ≤ 2^16 →
233    ∀pc. ∀pc_ok: pc < program_size.
234     nth_safe ? pc program pc_ok = \snd (next (load_code_memory program) (bitvector_of_nat … pc)).
235whd in match load_code_memory; normalize nodelta #program @pi2
236qed.
237
238lemma Prod_inv_rect_Type0:
239 ∀A,B. ∀P: A × B → Type[0].∀ab.
240  (∀a,b. ab = 〈a,b〉 → P 〈a,b〉) → P ab.
241 #A #B #P * /2/
242qed.
243
244notation > "hvbox('let' 〈ident x,ident y〉 {ident H} ≝ t 'in' s)"
245 with precedence 10
246for @{ Prod_inv_rect_Type0 ??? $t (λ${ident x}.λ${ident y}.λ${ident H}.$s) }.
247
248notation < "hvbox('let' 〈ident x,ident y〉 {ident H} ≝ t 'in' s)"
249 with precedence 10
250for @{ Prod_inv_rect_Type0 $z $w $r $t (λ${ident x}:$X.λ${ident y}:$Y.λ${ident H}:$h.$s) }.
251
252lemma breakup_pair' : ∀A,B,C:Type[0].∀x. ∀R:C → Prop. ∀P:∀a:A.∀b:B. x=〈a,b〉 → C.
253  R (P (\fst x) (\snd x) ?) → R (let 〈a,b〉 {H} ≝ x in P a b H).
254[2: // ]
255#A #B #C *; normalize /2/
256qed.
257
258(* timings taken from SIEMENS *)
259
260definition fetch0: ∀code_memory: BitVectorTrie Byte 16.
261    ∀program_counter: Word. Byte → instruction × Word × nat ≝
262  λpmem.
263  λpc.
264  λv.
265   let 〈b,v〉 ≝ head … v in if b then
266    let 〈b,v〉 ≝ head … v in if b then
267     let 〈b,v〉 ≝ head … v in if b then
268      let 〈b,v〉 ≝ head … v in if b then
269       let 〈b,v〉 ≝ head … v in if b then
270        〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,ACC_A〉)))))), pc〉, 1〉
271       else
272        let 〈b,v〉≝  head … v in if b then
273         let 〈b,v〉≝  head … v in if b then
274          〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),ACC_A〉)))))), pc〉, 1〉
275         else
276          let 〈b,v〉≝  head … v in if b then
277           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉))))), pc〉, 1〉
278          else
279           〈〈RealInstruction (CPL … ACC_A), pc〉, 1〉
280        else
281         let 〈b,v〉≝  head … v in if b then
282          〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT (from_singl … v),ACC_A〉)), pc〉, 2〉
283         else
284          let 〈b,v〉≝  head … v in if b then
285           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
286          else
287           〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT_DPTR,ACC_A〉)), pc〉, 2〉
288      else
289       let 〈b,v〉≝  head … v in if b then
290        〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,REGISTER v〉)))))), pc〉, 1〉
291       else
292        let 〈b,v〉≝  head … v in if b then
293         let 〈b,v〉≝  head … v in if b then
294          〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)))))), pc〉, 1〉
295         else
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 … (inl … 〈ACC_A,DIRECT b1〉)))))), pc〉, 1〉
298          else
299           〈〈RealInstruction (CLR … ACC_A), pc〉, 1〉
300        else
301         let 〈b,v〉≝  head … v in if b then
302          〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT (from_singl … v)〉)), pc〉, 2〉
303         else
304          let 〈b,v〉≝  head … v in if b then
305           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
306          else
307           〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT_DPTR〉)), pc〉, 2〉
308     else
309      let 〈b,v〉≝  head … v in if b then
310       let 〈b,v〉≝  head … v in if b then
311        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉
312       else
313        let 〈b,v〉≝  head … v in if b then
314         let 〈b,v〉≝  head … v in if b then
315          〈〈RealInstruction (XCHD … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
316         else
317          let 〈b,v〉≝  head … v in if b then
318           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉
319          else
320           〈〈RealInstruction (DA … ACC_A), pc〉, 1〉
321        else
322         let 〈b,v〉≝  head … v in if b then
323          let 〈b,v〉≝  head … v in if b then
324           〈〈RealInstruction (SETB … CARRY), pc〉, 1〉
325          else
326           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SETB … (BIT_ADDR b1)), pc〉, 1〉
327         else
328          let 〈b,v〉≝  head … v in if b then
329           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
330          else
331           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (POP … (DIRECT b1)), pc〉, 2〉
332      else
333       let 〈b,v〉≝  head … v in if b then
334        〈〈RealInstruction (XCH … ACC_A (REGISTER v)), pc〉, 1〉
335       else
336        let 〈b,v〉≝  head … v in if b then
337         let 〈b,v〉≝  head … v in if b then
338          〈〈RealInstruction (XCH … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
339         else
340          let 〈b,v〉≝  head … v in if b then
341           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XCH … ACC_A (DIRECT b1)), pc〉, 1〉
342          else
343           〈〈RealInstruction (SWAP … ACC_A), pc〉, 1〉
344        else
345         let 〈b,v〉≝  head … v in if b then
346          let 〈b,v〉≝  head … v in if b then
347           〈〈RealInstruction (CLR … CARRY), pc〉, 1〉
348          else
349           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (CLR … (BIT_ADDR b1)), pc〉, 1〉
350         else
351          let 〈b,v〉≝  head … v in if b then
352           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
353          else
354           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (PUSH … (DIRECT b1)), pc〉, 2〉
355    else
356     let 〈b,v〉≝  head … v in if b then
357      let 〈b,v〉≝  head … v in if b then
358       let 〈b,v〉≝  head … v in if b then
359        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〉
360       else
361        let 〈b,v〉≝  head … v in if b then
362         let 〈b,v〉≝  head … v in if b then
363          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〉
364         else
365          let 〈b,v〉≝  head … v in if b then
366           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〉
367          else
368           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〉
369        else
370         let 〈b,v〉≝  head … v in if b then
371          let 〈b,v〉≝  head … v in if b then
372           〈〈RealInstruction (CPL … CARRY), pc〉, 1〉
373          else
374           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (CPL … (BIT_ADDR b1)), pc〉, 1〉
375         else
376          let 〈b,v〉≝  head … v in if b then
377           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
378          else
379           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
380      else
381       let 〈b,v〉≝  head … v in if b then
382        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉)))))), pc〉, 2〉
383       else
384        let 〈b,v〉≝  head … v in if b then
385         let 〈b,v〉≝  head … v in if b then
386          let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉)))))), pc〉, 2〉
387         else
388          〈〈RealInstruction (MUL … ACC_A ACC_B), pc〉, 4〉
389        else
390         let 〈b,v〉≝  head … v in if b then
391          let 〈b,v〉≝  head … v in if b then
392           〈〈RealInstruction (INC … DPTR), pc〉, 2〉
393          else
394           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉))), pc〉, 1〉
395         else
396          let 〈b,v〉≝  head … v in if b then
397           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
398          else
399           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
400     else
401      let 〈b,v〉≝  head … v in if b then
402       let 〈b,v〉≝  head … v in if b then
403        〈〈RealInstruction (SUBB … 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 (SUBB … 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 (SUBB … ACC_A (DIRECT b1)), pc〉, 1〉
411          else
412           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SUBB … 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           〈〈MOVC … ACC_A (ACC_DPTR), pc〉, 2〉
417          else
418           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inr … 〈BIT_ADDR b1,CARRY〉)), pc〉, 2〉
419         else
420          let 〈b,v〉≝  head … v in if b then
421           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
422          else
423           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〉
424      else
425       let 〈b,v〉≝  head … v in if b then
426        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉))))), pc〉, 2〉
427       else
428        let 〈b,v〉≝  head … v in if b then
429         let 〈b,v〉≝  head … v in if b then
430          let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉))))), pc〉, 2〉
431         else
432          let 〈b,v〉≝  head … v in if b then
433           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〉
434          else
435           〈〈RealInstruction (DIV … ACC_A ACC_B), pc〉, 4〉
436        else
437         let 〈b,v〉≝  head … v in if b then
438          let 〈b,v〉≝  head … v in if b then
439           〈〈MOVC … ACC_A (ACC_PC), pc〉, 2〉
440          else
441           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
442         else
443          let 〈b,v〉≝  head … v in if b then
444           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
445          else
446           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈SJMP … (RELATIVE b1), pc〉, 2〉
447   else
448    let 〈b,v〉≝  head … v in if b then
449     let 〈b,v〉≝  head … v in if b then
450      let 〈b,v〉≝  head … v in if b then
451       let 〈b,v〉≝  head … v in if b then
452        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉)))))), pc〉, 1〉
453       else
454        let 〈b,v〉≝  head … v in if b then
455         let 〈b,v〉≝  head … v in if b then
456          let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉)))))), pc〉, 1〉
457         else
458          let 〈b,v〉≝  head … v in if b then
459           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〉
460          else
461           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉
462        else
463         let 〈b,v〉≝  head … v in if b then
464          let 〈b,v〉≝  head … v in if b then
465           〈〈JMP … INDIRECT_DPTR, pc〉, 2〉
466          else
467           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
468         else
469          let 〈b,v〉≝  head … v in if b then
470           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
471          else
472           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JNZ … (RELATIVE b1)), pc〉, 2〉
473      else
474       let 〈b,v〉≝  head … v in if b then
475        〈〈RealInstruction (XRL … (inl … 〈ACC_A,REGISTER v〉)), pc〉, 1〉
476       else
477        let 〈b,v〉≝  head … v in if b then
478         let 〈b,v〉≝  head … v in if b then
479          〈〈RealInstruction (XRL … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, 1〉
480         else
481          let 〈b,v〉≝  head … v in if b then
482           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉
483          else
484           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DATA b1〉)), 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           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〉
489          else
490           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉
491         else
492          let 〈b,v〉≝  head … v in if b then
493           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
494          else
495           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JZ … (RELATIVE b1)), pc〉, 2〉
496     else
497      let 〈b,v〉≝  head … v in if b then
498       let 〈b,v〉≝  head … v in if b then
499        〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,REGISTER v〉))), pc〉, 1〉
500       else
501        let 〈b,v〉≝  head … v in if b then
502         let 〈b,v〉≝  head … v in if b then
503          〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))), pc〉, 1〉
504         else
505          let 〈b,v〉≝  head … v in if b then
506           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
507          else
508           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
509        else
510         let 〈b,v〉≝  head … v in if b then
511          let 〈b,v〉≝  head … v in if b then
512           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〉
513          else
514           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
515         else
516          let 〈b,v〉≝  head … v in if b then
517           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
518          else
519           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JNC … (RELATIVE b1)), pc〉, 2〉
520      else
521       let 〈b,v〉≝  head … v in if b then
522        〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,REGISTER v〉))), pc〉, 1〉
523       else
524        let 〈b,v〉≝  head … v in if b then
525         let 〈b,v〉≝  head … v in if b then
526          〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))), pc〉, 1〉
527         else
528          let 〈b,v〉≝  head … v in if b then
529           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
530          else
531           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DATA b1〉))), 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           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〉
536          else
537           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
538         else
539          let 〈b,v〉≝  head … v in if b then
540           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
541          else
542           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JC … (RELATIVE b1)), pc〉, 2〉
543    else
544     let 〈b,v〉≝  head … v in if b then
545      let 〈b,v〉≝  head … v in if b then
546       let 〈b,v〉≝  head … v in if b then
547        〈〈RealInstruction (ADDC … ACC_A (REGISTER v)), pc〉, 1〉
548       else
549        let 〈b,v〉≝  head … v in if b then
550         let 〈b,v〉≝  head … v in if b then
551          〈〈RealInstruction (ADDC … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
552         else
553          let 〈b,v〉≝  head … v in if b then
554           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DIRECT b1)), pc〉, 1〉
555          else
556           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DATA b1)), pc〉, 1〉
557        else
558         let 〈b,v〉≝  head … v in if b then
559          let 〈b,v〉≝  head … v in if b then
560           〈〈RealInstruction (RLC … ACC_A), pc〉, 1〉
561          else
562           〈〈RealInstruction (RETI …), pc〉, 2〉
563         else
564          let 〈b,v〉≝  head … v in if b then
565           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
566          else
567           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〉
568      else
569       let 〈b,v〉≝  head … v in if b then
570        〈〈RealInstruction (ADD … ACC_A (REGISTER v)), pc〉, 1〉
571       else
572        let 〈b,v〉≝  head … v in if b then
573         let 〈b,v〉≝  head … v in if b then
574          〈〈RealInstruction (ADD … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
575         else
576          let 〈b,v〉≝  head … v in if b then
577           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DIRECT b1)), pc〉, 1〉
578          else
579           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DATA b1)), pc〉, 1〉
580        else
581         let 〈b,v〉≝  head … v in if b then
582          let 〈b,v〉≝  head … v in if b then
583           〈〈RealInstruction (RL … ACC_A), pc〉, 1〉
584          else
585           〈〈RealInstruction (RET …), pc〉, 2〉
586         else
587          let 〈b,v〉≝  head … v in if b then
588           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
589          else
590           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〉
591     else
592      let 〈b,v〉≝  head … v in if b then
593       let 〈b,v〉≝  head … v in if b then
594        〈〈RealInstruction (DEC … (REGISTER v)), pc〉, 1〉
595       else
596        let 〈b,v〉≝  head … v in if b then
597         let 〈b,v〉≝  head … v in if b then
598          〈〈RealInstruction (DEC … (INDIRECT (from_singl … v))), pc〉, 1〉
599         else
600          let 〈b,v〉≝  head … v in if b then
601           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (DEC … (DIRECT b1)), pc〉, 1〉
602          else
603           〈〈RealInstruction (DEC … ACC_A), pc〉, 1〉
604        else
605         let 〈b,v〉≝  head … v in if b then
606          let 〈b,v〉≝  head … v in if b then
607           〈〈RealInstruction (RRC … ACC_A), pc〉, 1〉
608          else
609           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉
610         else
611          let 〈b,v〉≝  head … v in if b then
612           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
613          else
614           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〉
615      else
616       let 〈b,v〉≝  head … v in if b then
617        〈〈RealInstruction (INC … (REGISTER v)), pc〉, 1〉
618       else
619        let 〈b,v〉≝  head … v in if b then
620         let 〈b,v〉≝  head … v in if b then
621          〈〈RealInstruction (INC … (INDIRECT (from_singl … v))), pc〉, 1〉
622         else
623          let 〈b,v〉≝  head … v in if b then
624           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (INC … (DIRECT b1)), pc〉, 1〉
625          else
626           〈〈RealInstruction (INC … ACC_A), pc〉, 1〉
627        else
628         let 〈b,v〉≝  head … v in if b then
629          let 〈b,v〉≝  head … v in if b then
630           〈〈RealInstruction (RR … ACC_A), pc〉, 1〉
631          else
632           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉
633         else
634          let 〈b,v〉≝  head … v in if b then
635           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
636          else
637           〈〈RealInstruction (NOP …), pc〉, 1〉.
638  %
639qed.
640
641definition fetch: ∀code_memory: BitVectorTrie Byte 16.
642    ∀program_counter: Word. instruction × Word × nat ≝
643  λpmem: BitVectorTrie Byte 16.
644  λpc: Word.
645  let 〈word, byte〉 ≝ next pmem pc in
646    fetch0 pmem word byte.
Note: See TracBrowser for help on using the repository browser.