source: src/ASM/Fetch.ma @ 3155

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

Simplified preliminaries:

inefficient_address_of_word_labels, and hence create_cost_label_map,

make redundant appeal to bivector_of_nat to change return type,
when only address_of_word_labels need return a Word.

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