source: src/ASM/Fetch.ma @ 2672

Last change on this file since 2672 was 2516, checked in by mckinna, 8 years ago

removed typedefs; restored older versions; moved typedefs to compiler.ma
AssemblyProofSplit? *still* doesn't typecheck: disambiguation errors!
File size: 32.4 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
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
175include alias "ASM/BitVectorTrie.ma".
176include alias "ASM/Arithmetic.ma".
177
178definition next: BitVectorTrie Byte 16 → ∀program_counter: Word. Word × Byte ≝
179  λpmem: BitVectorTrie Byte 16.
180  λpc: Word.
181    〈add … pc (bitvector_of_nat 16 1), lookup … pc pmem (zero …)〉.
182
183definition load_code_memory0:
184 ∀program: list Byte. Σres: BitVectorTrie Byte 16.
185  let program_size ≝ |program| in
186   program_size ≤ 2^16 →
187    ∀pc. ∀pc_ok: pc < program_size.
188     nth_safe ? pc program pc_ok = \snd (next res (bitvector_of_nat … pc))
189≝
190 λprogram. \snd
191  (foldl_strong ?
192   (λprefix.
193     Σres: nat × (BitVectorTrie Byte 16).
194      let 〈i,mem〉 ≝ res in
195      i = |prefix| ∧
196      (i ≤ 2^16 →
197        ∀pc. ∀pc_ok: pc < |prefix|.
198         nth_safe ? pc prefix pc_ok = \snd (next mem (bitvector_of_nat … pc))))
199   program
200   (λprefix,v,tl,prf,i_mem.
201     let 〈i,mem〉 ≝ i_mem in
202      〈S i,insert … (bitvector_of_nat … i) v mem〉)
203  〈0,Stub Byte 16〉).
204[3: cases (foldl_strong ? (λprefix.Σres.?) ???) * #i #mem * #H1 >H1 #H2 @H2
205| % // #_ #pc #abs @⊥ @(absurd … abs (not_le_Sn_O …))
206| cases i_mem in p; * #i' #mem' #H #EQ destruct(EQ) cases H -H #H1 #H2 %
207  [ >length_append >H1 normalize //
208  | #LE #pc #pc_ok
209    cases (le_to_or_lt_eq … pc_ok)
210    [2: #EQ_Spc >(?: pc = |prefix| + 0) in pc_ok;
211      [2: >length_append in EQ_Spc; normalize #EQ @injective_S >EQ //]
212      #pc_ok <nth_safe_prepend [2: //] whd in ⊢ (??%?);
213      <H1 <plus_n_O whd in ⊢ (???%); //
214    | >length_append <plus_n_Sm <plus_n_O #LT <shift_nth_prefix [2: /2/]
215      >H2 [2: @(transitive_le … LE) //]
216      cut (pc ≠ i) [ >H1 @lt_to_not_eq @lt_S_S_to_lt //] #NEQ
217      whd in ⊢ (??%%); @sym_eq @lookup_insert_miss >eq_bv_false %
218      #EQ @(absurd ?? NEQ) @(eq_bitvector_of_nat_to_eq … EQ) try assumption
219      @(transitive_lt … LE) >H1 @lt_S_S_to_lt //]]
220qed.
221
222definition load_code_memory: list Byte → BitVectorTrie Byte 16 ≝
223 λprogram.load_code_memory0 program.
224
225lemma load_code_memory_ok:
226 ∀program: list Byte.
227  let program_size ≝ |program| in
228   program_size ≤ 2^16 →
229    ∀pc. ∀pc_ok: pc < program_size.
230     nth_safe ? pc program pc_ok = \snd (next (load_code_memory program) (bitvector_of_nat … pc)).
231whd in match load_code_memory; normalize nodelta #program @pi2
232qed.
233
234lemma Prod_inv_rect_Type0:
235 ∀A,B. ∀P: A × B → Type[0].∀ab.
236  (∀a,b. ab = 〈a,b〉 → P 〈a,b〉) → P ab.
237 #A #B #P * /2/
238qed.
239
240notation > "hvbox('let' 〈ident x,ident y〉 {ident H} ≝ t 'in' s)"
241 with precedence 10
242for @{ Prod_inv_rect_Type0 ??? $t (λ${ident x}.λ${ident y}.λ${ident H}.$s) }.
243
244notation < "hvbox('let' 〈ident x,ident y〉 {ident H} ≝ t 'in' s)"
245 with precedence 10
246for @{ Prod_inv_rect_Type0 $z $w $r $t (λ${ident x}:$X.λ${ident y}:$Y.λ${ident H}:$h.$s) }.
247
248lemma breakup_pair' : ∀A,B,C:Type[0].∀x. ∀R:C → Prop. ∀P:∀a:A.∀b:B. x=〈a,b〉 → C.
249  R (P (\fst x) (\snd x) ?) → R (let 〈a,b〉 {H} ≝ x in P a b H).
250[2: // ]
251#A #B #C *; normalize /2/
252qed.
253
254(* timings taken from SIEMENS *)
255
256definition fetch0: ∀code_memory: BitVectorTrie Byte 16.
257    ∀program_counter: Word. Byte → instruction × Word × nat ≝
258  λpmem.
259  λpc.
260  λv.
261   let 〈b,v〉 ≝ head … v in if b then
262    let 〈b,v〉 ≝ head … v in if b then
263     let 〈b,v〉 ≝ head … v in if b then
264      let 〈b,v〉 ≝ head … v in if b then
265       let 〈b,v〉 ≝ head … v in if b then
266        〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,ACC_A〉)))))), pc〉, 1〉
267       else
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 … 〈INDIRECT (from_singl … v),ACC_A〉)))))), pc〉, 1〉
271         else
272          let 〈b,v〉≝  head … v in if b then
273           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉))))), pc〉, 1〉
274          else
275           〈〈RealInstruction (CPL … ACC_A), pc〉, 1〉
276        else
277         let 〈b,v〉≝  head … v in if b then
278          〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT (from_singl … v),ACC_A〉)), pc〉, 2〉
279         else
280          let 〈b,v〉≝  head … v in if b then
281           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
282          else
283           〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT_DPTR,ACC_A〉)), pc〉, 2〉
284      else
285       let 〈b,v〉≝  head … v in if b then
286        〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,REGISTER v〉)))))), pc〉, 1〉
287       else
288        let 〈b,v〉≝  head … v in if b then
289         let 〈b,v〉≝  head … v in if b then
290          〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)))))), pc〉, 1〉
291         else
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 … (inl … 〈ACC_A,DIRECT b1〉)))))), pc〉, 1〉
294          else
295           〈〈RealInstruction (CLR … ACC_A), pc〉, 1〉
296        else
297         let 〈b,v〉≝  head … v in if b then
298          〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT (from_singl … v)〉)), pc〉, 2〉
299         else
300          let 〈b,v〉≝  head … v in if b then
301           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
302          else
303           〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT_DPTR〉)), pc〉, 2〉
304     else
305      let 〈b,v〉≝  head … v in if b then
306       let 〈b,v〉≝  head … v in if b then
307        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (DJNZ … (REGISTER v) (RELATIVE b1)), 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          〈〈RealInstruction (XCHD … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
312         else
313          let 〈b,v〉≝  head … v in if b then
314           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉
315          else
316           〈〈RealInstruction (DA … ACC_A), 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 (SETB … CARRY), pc〉, 1〉
321          else
322           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SETB … (BIT_ADDR b1)), pc〉, 1〉
323         else
324          let 〈b,v〉≝  head … v in if b then
325           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
326          else
327           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (POP … (DIRECT b1)), pc〉, 2〉
328      else
329       let 〈b,v〉≝  head … v in if b then
330        〈〈RealInstruction (XCH … ACC_A (REGISTER v)), pc〉, 1〉
331       else
332        let 〈b,v〉≝  head … v in if b then
333         let 〈b,v〉≝  head … v in if b then
334          〈〈RealInstruction (XCH … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
335         else
336          let 〈b,v〉≝  head … v in if b then
337           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XCH … ACC_A (DIRECT b1)), pc〉, 1〉
338          else
339           〈〈RealInstruction (SWAP … ACC_A), pc〉, 1〉
340        else
341         let 〈b,v〉≝  head … v in if b then
342          let 〈b,v〉≝  head … v in if b then
343           〈〈RealInstruction (CLR … CARRY), pc〉, 1〉
344          else
345           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (CLR … (BIT_ADDR b1)), pc〉, 1〉
346         else
347          let 〈b,v〉≝  head … v in if b then
348           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
349          else
350           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (PUSH … (DIRECT b1)), pc〉, 2〉
351    else
352     let 〈b,v〉≝  head … v in if b then
353      let 〈b,v〉≝  head … v in if b then
354       let 〈b,v〉≝  head … v in if b then
355        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〉
356       else
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 … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉
360         else
361          let 〈b,v〉≝  head … v in if b then
362           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〉
363          else
364           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〉
365        else
366         let 〈b,v〉≝  head … v in if b then
367          let 〈b,v〉≝  head … v in if b then
368           〈〈RealInstruction (CPL … CARRY), pc〉, 1〉
369          else
370           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (CPL … (BIT_ADDR b1)), pc〉, 1〉
371         else
372          let 〈b,v〉≝  head … v in if b then
373           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
374          else
375           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
376      else
377       let 〈b,v〉≝  head … v in if b then
378        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉)))))), pc〉, 2〉
379       else
380        let 〈b,v〉≝  head … v in if b then
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 … 〈INDIRECT (from_singl … v),DIRECT b1〉)))))), pc〉, 2〉
383         else
384          〈〈RealInstruction (MUL … ACC_A ACC_B), pc〉, 4〉
385        else
386         let 〈b,v〉≝  head … v in if b then
387          let 〈b,v〉≝  head … v in if b then
388           〈〈RealInstruction (INC … DPTR), pc〉, 2〉
389          else
390           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉))), pc〉, 1〉
391         else
392          let 〈b,v〉≝  head … v in if b then
393           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
394          else
395           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
396     else
397      let 〈b,v〉≝  head … v in if b then
398       let 〈b,v〉≝  head … v in if b then
399        〈〈RealInstruction (SUBB … ACC_A (REGISTER v)), pc〉, 1〉
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 (INDIRECT (from_singl … v))), pc〉, 1〉
404         else
405          let 〈b,v〉≝  head … v in if b then
406           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DIRECT b1)), pc〉, 1〉
407          else
408           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DATA b1)), pc〉, 1〉
409        else
410         let 〈b,v〉≝  head … v in if b then
411          let 〈b,v〉≝  head … v in if b then
412           〈〈MOVC … ACC_A (ACC_DPTR), pc〉, 2〉
413          else
414           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inr … 〈BIT_ADDR b1,CARRY〉)), pc〉, 2〉
415         else
416          let 〈b,v〉≝  head … v in if b then
417           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
418          else
419           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〉
420      else
421       let 〈b,v〉≝  head … v in if b then
422        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉))))), pc〉, 2〉
423       else
424        let 〈b,v〉≝  head … v in if b then
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,INDIRECT (from_singl … v)〉))))), pc〉, 2〉
427         else
428          let 〈b,v〉≝  head … v in if b then
429           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〉
430          else
431           〈〈RealInstruction (DIV … ACC_A ACC_B), pc〉, 4〉
432        else
433         let 〈b,v〉≝  head … v in if b then
434          let 〈b,v〉≝  head … v in if b then
435           〈〈MOVC … ACC_A (ACC_PC), pc〉, 2〉
436          else
437           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
438         else
439          let 〈b,v〉≝  head … v in if b then
440           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
441          else
442           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈SJMP … (RELATIVE b1), pc〉, 2〉
443   else
444    let 〈b,v〉≝  head … v in if b then
445     let 〈b,v〉≝  head … v in if b then
446      let 〈b,v〉≝  head … v in if b then
447       let 〈b,v〉≝  head … v in if b then
448        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉)))))), pc〉, 1〉
449       else
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 … 〈INDIRECT (from_singl … v),DATA b1〉)))))), pc〉, 1〉
453         else
454          let 〈b,v〉≝  head … v in if b then
455           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〉
456          else
457           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉
458        else
459         let 〈b,v〉≝  head … v in if b then
460          let 〈b,v〉≝  head … v in if b then
461           〈〈JMP … INDIRECT_DPTR, pc〉, 2〉
462          else
463           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
464         else
465          let 〈b,v〉≝  head … v in if b then
466           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
467          else
468           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JNZ … (RELATIVE b1)), pc〉, 2〉
469      else
470       let 〈b,v〉≝  head … v in if b then
471        〈〈RealInstruction (XRL … (inl … 〈ACC_A,REGISTER v〉)), pc〉, 1〉
472       else
473        let 〈b,v〉≝  head … v in if b then
474         let 〈b,v〉≝  head … v in if b then
475          〈〈RealInstruction (XRL … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, 1〉
476         else
477          let 〈b,v〉≝  head … v in if b then
478           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉
479          else
480           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉
481        else
482         let 〈b,v〉≝  head … v in if b then
483          let 〈b,v〉≝  head … v in if b then
484           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〉
485          else
486           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉
487         else
488          let 〈b,v〉≝  head … v in if b then
489           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
490          else
491           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JZ … (RELATIVE b1)), pc〉, 2〉
492     else
493      let 〈b,v〉≝  head … v in if b then
494       let 〈b,v〉≝  head … v in if b then
495        〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,REGISTER v〉))), pc〉, 1〉
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,INDIRECT (from_singl … v)〉))), pc〉, 1〉
500         else
501          let 〈b,v〉≝  head … v in if b then
502           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
503          else
504           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
505        else
506         let 〈b,v〉≝  head … v in if b then
507          let 〈b,v〉≝  head … v in if b then
508           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〉
509          else
510           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
511         else
512          let 〈b,v〉≝  head … v in if b then
513           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
514          else
515           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JNC … (RELATIVE b1)), pc〉, 2〉
516      else
517       let 〈b,v〉≝  head … v in if b then
518        〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,REGISTER v〉))), pc〉, 1〉
519       else
520        let 〈b,v〉≝  head … v in if b then
521         let 〈b,v〉≝  head … v in if b then
522          〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))), pc〉, 1〉
523         else
524          let 〈b,v〉≝  head … v in if b then
525           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
526          else
527           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
528        else
529         let 〈b,v〉≝  head … v in if b then
530          let 〈b,v〉≝  head … v in if b then
531           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〉
532          else
533           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
534         else
535          let 〈b,v〉≝  head … v in if b then
536           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
537          else
538           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JC … (RELATIVE b1)), pc〉, 2〉
539    else
540     let 〈b,v〉≝  head … v in if b then
541      let 〈b,v〉≝  head … v in if b then
542       let 〈b,v〉≝  head … v in if b then
543        〈〈RealInstruction (ADDC … ACC_A (REGISTER v)), pc〉, 1〉
544       else
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 (INDIRECT (from_singl … v))), pc〉, 1〉
548         else
549          let 〈b,v〉≝  head … v in if b then
550           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DIRECT b1)), pc〉, 1〉
551          else
552           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DATA b1)), pc〉, 1〉
553        else
554         let 〈b,v〉≝  head … v in if b then
555          let 〈b,v〉≝  head … v in if b then
556           〈〈RealInstruction (RLC … ACC_A), pc〉, 1〉
557          else
558           〈〈RealInstruction (RETI …), pc〉, 2〉
559         else
560          let 〈b,v〉≝  head … v in if b then
561           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
562          else
563           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〉
564      else
565       let 〈b,v〉≝  head … v in if b then
566        〈〈RealInstruction (ADD … ACC_A (REGISTER v)), pc〉, 1〉
567       else
568        let 〈b,v〉≝  head … v in if b then
569         let 〈b,v〉≝  head … v in if b then
570          〈〈RealInstruction (ADD … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
571         else
572          let 〈b,v〉≝  head … v in if b then
573           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DIRECT b1)), pc〉, 1〉
574          else
575           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DATA b1)), pc〉, 1〉
576        else
577         let 〈b,v〉≝  head … v in if b then
578          let 〈b,v〉≝  head … v in if b then
579           〈〈RealInstruction (RL … ACC_A), pc〉, 1〉
580          else
581           〈〈RealInstruction (RET …), pc〉, 2〉
582         else
583          let 〈b,v〉≝  head … v in if b then
584           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
585          else
586           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〉
587     else
588      let 〈b,v〉≝  head … v in if b then
589       let 〈b,v〉≝  head … v in if b then
590        〈〈RealInstruction (DEC … (REGISTER v)), pc〉, 1〉
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 … (INDIRECT (from_singl … v))), pc〉, 1〉
595         else
596          let 〈b,v〉≝  head … v in if b then
597           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (DEC … (DIRECT b1)), pc〉, 1〉
598          else
599           〈〈RealInstruction (DEC … ACC_A), pc〉, 1〉
600        else
601         let 〈b,v〉≝  head … v in if b then
602          let 〈b,v〉≝  head … v in if b then
603           〈〈RealInstruction (RRC … ACC_A), pc〉, 1〉
604          else
605           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉
606         else
607          let 〈b,v〉≝  head … v in if b then
608           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
609          else
610           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〉
611      else
612       let 〈b,v〉≝  head … v in if b then
613        〈〈RealInstruction (INC … (REGISTER v)), pc〉, 1〉
614       else
615        let 〈b,v〉≝  head … v in if b then
616         let 〈b,v〉≝  head … v in if b then
617          〈〈RealInstruction (INC … (INDIRECT (from_singl … v))), pc〉, 1〉
618         else
619          let 〈b,v〉≝  head … v in if b then
620           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (INC … (DIRECT b1)), pc〉, 1〉
621          else
622           〈〈RealInstruction (INC … ACC_A), pc〉, 1〉
623        else
624         let 〈b,v〉≝  head … v in if b then
625          let 〈b,v〉≝  head … v in if b then
626           〈〈RealInstruction (RR … ACC_A), pc〉, 1〉
627          else
628           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉
629         else
630          let 〈b,v〉≝  head … v in if b then
631           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
632          else
633           〈〈RealInstruction (NOP …), pc〉, 1〉.
634  %
635qed.
636
637definition fetch: ∀code_memory: BitVectorTrie Byte 16.
638    ∀program_counter: Word. instruction × Word × nat ≝
639  λpmem: BitVectorTrie Byte 16.
640  λpc: Word.
641  let 〈word, byte〉 ≝ next pmem pc in
642    fetch0 pmem word byte.
Note: See TracBrowser for help on using the repository browser.