[698] | 1 | include "ASM/BitVectorTrie.ma". |
---|
| 2 | include "ASM/Arithmetic.ma". |
---|
| 3 | include "ASM/ASM.ma". |
---|
[1600] | 4 | include "basics/russell.ma". |
---|
[475] | 5 | |
---|
[2264] | 6 | (***** Pseudo-code ******) |
---|
| 7 | |
---|
| 8 | definition 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 | |
---|
| 13 | lemma 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) % |
---|
| 19 | qed. |
---|
| 20 | |
---|
| 21 | lemma 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 | // ] |
---|
| 28 | qed. |
---|
| 29 | |
---|
| 30 | lemma 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 |
---|
| 36 | qed. |
---|
| 37 | |
---|
| 38 | (* label_map: identifier ↦ pseudo program counter *) |
---|
| 39 | definition label_map ≝ identifier_map ASMTag ℕ. |
---|
| 40 | |
---|
| 41 | (* The function that creates the label-to-address map *) |
---|
| 42 | definition 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 | ] |
---|
| 105 | qed. |
---|
| 106 | |
---|
| 107 | (* The function that creates the label-to-address map *) |
---|
| 108 | definition create_label_cost_map: ∀program:list labelled_instruction. |
---|
| 109 | label_map × (BitVectorTrie costlabel 16) ≝ |
---|
| 110 | λprogram. |
---|
| 111 | pi1 … (create_label_cost_map0 program). |
---|
| 112 | |
---|
| 113 | theorem 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 |
---|
| 122 | qed. |
---|
| 123 | |
---|
| 124 | definition 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 | |
---|
| 132 | lemma 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 // |
---|
| 141 | qed. |
---|
| 142 | |
---|
| 143 | lemma 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 // |
---|
| 155 | qed. |
---|
| 156 | |
---|
| 157 | lemma 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 // |
---|
| 165 | qed. |
---|
| 166 | |
---|
| 167 | (***** Object-code *******) |
---|
| 168 | |
---|
[1591] | 169 | definition bitvector_max_nat ≝ |
---|
| 170 | λlength: nat. |
---|
| 171 | 2^length. |
---|
[475] | 172 | |
---|
[1591] | 173 | definition code_memory_size ≝ bitvector_max_nat 16. |
---|
| 174 | |
---|
[1941] | 175 | include alias "ASM/BitVectorTrie.ma". |
---|
[1961] | 176 | include alias "ASM/Arithmetic.ma". |
---|
[1941] | 177 | |
---|
[1604] | 178 | definition next: BitVectorTrie Byte 16 → ∀program_counter: Word. Word × Byte ≝ |
---|
[1591] | 179 | λpmem: BitVectorTrie Byte 16. |
---|
| 180 | λpc: Word. |
---|
[1941] | 181 | 〈add … pc (bitvector_of_nat 16 1), lookup … pc pmem (zero …)〉. |
---|
[1591] | 182 | |
---|
[2119] | 183 | definition 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 //]] |
---|
| 220 | qed. |
---|
| 221 | |
---|
| 222 | definition load_code_memory: list Byte → BitVectorTrie Byte 16 ≝ |
---|
| 223 | λprogram.load_code_memory0 program. |
---|
| 224 | |
---|
| 225 | lemma 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)). |
---|
| 231 | whd in match load_code_memory; normalize nodelta #program @pi2 |
---|
| 232 | qed. |
---|
| 233 | |
---|
[1598] | 234 | lemma 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/ |
---|
| 238 | qed. |
---|
| 239 | |
---|
| 240 | notation > "hvbox('let' 〈ident x,ident y〉 {ident H} ≝ t 'in' s)" |
---|
| 241 | with precedence 10 |
---|
| 242 | for @{ Prod_inv_rect_Type0 ??? $t (λ${ident x}.λ${ident y}.λ${ident H}.$s) }. |
---|
| 243 | |
---|
| 244 | notation < "hvbox('let' 〈ident x,ident y〉 {ident H} ≝ t 'in' s)" |
---|
| 245 | with precedence 10 |
---|
| 246 | for @{ Prod_inv_rect_Type0 $z $w $r $t (λ${ident x}:$X.λ${ident y}:$Y.λ${ident H}:$h.$s) }. |
---|
| 247 | |
---|
| 248 | lemma 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/ |
---|
| 252 | qed. |
---|
| 253 | |
---|
[475] | 254 | (* timings taken from SIEMENS *) |
---|
| 255 | |
---|
[1604] | 256 | definition fetch0: ∀code_memory: BitVectorTrie Byte 16. |
---|
| 257 | ∀program_counter: Word. Byte → instruction × Word × nat ≝ |
---|
[1591] | 258 | λpmem. |
---|
| 259 | λpc. |
---|
| 260 | λv. |
---|
[475] | 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 |
---|
[820] | 266 | 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,ACC_A〉)))))), pc〉, 1〉 |
---|
[475] | 267 | else |
---|
| 268 | let 〈b,v〉≝ head … v in if b then |
---|
| 269 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 270 | 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),ACC_A〉)))))), pc〉, 1〉 |
---|
[475] | 271 | else |
---|
| 272 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 273 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉))))), pc〉, 1〉 |
---|
[475] | 274 | else |
---|
[856] | 275 | 〈〈RealInstruction (CPL … ACC_A), pc〉, 1〉 |
---|
[475] | 276 | else |
---|
| 277 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 278 | 〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT (from_singl … v),ACC_A〉)), pc〉, 2〉 |
---|
[475] | 279 | else |
---|
| 280 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 281 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉 |
---|
[475] | 282 | else |
---|
[820] | 283 | 〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT_DPTR,ACC_A〉)), pc〉, 2〉 |
---|
[475] | 284 | else |
---|
| 285 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 286 | 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,REGISTER v〉)))))), pc〉, 1〉 |
---|
[475] | 287 | else |
---|
| 288 | let 〈b,v〉≝ head … v in if b then |
---|
| 289 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 290 | 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)))))), pc〉, 1〉 |
---|
[475] | 291 | else |
---|
| 292 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 293 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉)))))), pc〉, 1〉 |
---|
[475] | 294 | else |
---|
[820] | 295 | 〈〈RealInstruction (CLR … ACC_A), pc〉, 1〉 |
---|
[475] | 296 | else |
---|
| 297 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 298 | 〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT (from_singl … v)〉)), pc〉, 2〉 |
---|
[475] | 299 | else |
---|
| 300 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 301 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉 |
---|
[475] | 302 | else |
---|
[820] | 303 | 〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT_DPTR〉)), pc〉, 2〉 |
---|
[475] | 304 | else |
---|
| 305 | let 〈b,v〉≝ head … v in if b then |
---|
| 306 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 307 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉 |
---|
[475] | 308 | else |
---|
| 309 | let 〈b,v〉≝ head … v in if b then |
---|
| 310 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 311 | 〈〈RealInstruction (XCHD … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉 |
---|
[475] | 312 | else |
---|
| 313 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 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〉 |
---|
[475] | 315 | else |
---|
[820] | 316 | 〈〈RealInstruction (DA … ACC_A), pc〉, 1〉 |
---|
[475] | 317 | else |
---|
| 318 | let 〈b,v〉≝ head … v in if b then |
---|
| 319 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 320 | 〈〈RealInstruction (SETB … CARRY), pc〉, 1〉 |
---|
[475] | 321 | else |
---|
[1604] | 322 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SETB … (BIT_ADDR b1)), pc〉, 1〉 |
---|
[475] | 323 | else |
---|
| 324 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 325 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉 |
---|
[475] | 326 | else |
---|
[1604] | 327 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (POP … (DIRECT b1)), pc〉, 2〉 |
---|
[475] | 328 | else |
---|
| 329 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 330 | 〈〈RealInstruction (XCH … ACC_A (REGISTER v)), pc〉, 1〉 |
---|
[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 (XCH … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉 |
---|
[475] | 335 | else |
---|
| 336 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 337 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XCH … ACC_A (DIRECT b1)), pc〉, 1〉 |
---|
[475] | 338 | else |
---|
[820] | 339 | 〈〈RealInstruction (SWAP … ACC_A), pc〉, 1〉 |
---|
[475] | 340 | else |
---|
| 341 | let 〈b,v〉≝ head … v in if b then |
---|
| 342 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 343 | 〈〈RealInstruction (CLR … CARRY), pc〉, 1〉 |
---|
[475] | 344 | else |
---|
[1604] | 345 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (CLR … (BIT_ADDR b1)), pc〉, 1〉 |
---|
[475] | 346 | else |
---|
| 347 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 348 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉 |
---|
[475] | 349 | else |
---|
[1604] | 350 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (PUSH … (DIRECT b1)), pc〉, 2〉 |
---|
[475] | 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 |
---|
[1604] | 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〉 |
---|
[475] | 356 | else |
---|
| 357 | let 〈b,v〉≝ head … v in if b then |
---|
| 358 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 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〉 |
---|
[475] | 360 | else |
---|
| 361 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 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〉 |
---|
[475] | 363 | else |
---|
[1604] | 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〉 |
---|
[475] | 365 | else |
---|
| 366 | let 〈b,v〉≝ head … v in if b then |
---|
| 367 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 368 | 〈〈RealInstruction (CPL … CARRY), pc〉, 1〉 |
---|
[475] | 369 | else |
---|
[1604] | 370 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (CPL … (BIT_ADDR b1)), pc〉, 1〉 |
---|
[475] | 371 | else |
---|
| 372 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 373 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉 |
---|
[475] | 374 | else |
---|
[1604] | 375 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉 |
---|
[475] | 376 | else |
---|
| 377 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 378 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉)))))), pc〉, 2〉 |
---|
[475] | 379 | else |
---|
| 380 | let 〈b,v〉≝ head … v in if b then |
---|
| 381 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 382 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉)))))), pc〉, 2〉 |
---|
[475] | 383 | else |
---|
[820] | 384 | 〈〈RealInstruction (MUL … ACC_A ACC_B), pc〉, 4〉 |
---|
[475] | 385 | else |
---|
| 386 | let 〈b,v〉≝ head … v in if b then |
---|
| 387 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 388 | 〈〈RealInstruction (INC … DPTR), pc〉, 2〉 |
---|
[475] | 389 | else |
---|
[1604] | 390 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉))), pc〉, 1〉 |
---|
[475] | 391 | else |
---|
| 392 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 393 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉 |
---|
[475] | 394 | else |
---|
[1604] | 395 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉 |
---|
[475] | 396 | else |
---|
| 397 | let 〈b,v〉≝ head … v in if b then |
---|
| 398 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 399 | 〈〈RealInstruction (SUBB … ACC_A (REGISTER v)), pc〉, 1〉 |
---|
[475] | 400 | else |
---|
| 401 | let 〈b,v〉≝ head … v in if b then |
---|
| 402 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 403 | 〈〈RealInstruction (SUBB … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉 |
---|
[475] | 404 | else |
---|
| 405 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 406 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DIRECT b1)), pc〉, 1〉 |
---|
[475] | 407 | else |
---|
[1604] | 408 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DATA b1)), pc〉, 1〉 |
---|
[475] | 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 |
---|
[1604] | 414 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inr … 〈BIT_ADDR b1,CARRY〉)), pc〉, 2〉 |
---|
[475] | 415 | else |
---|
| 416 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 417 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉 |
---|
[475] | 418 | else |
---|
[1604] | 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〉 |
---|
[475] | 420 | else |
---|
| 421 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 422 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉))))), pc〉, 2〉 |
---|
[475] | 423 | else |
---|
| 424 | let 〈b,v〉≝ head … v in if b then |
---|
| 425 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 426 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉))))), pc〉, 2〉 |
---|
[475] | 427 | else |
---|
| 428 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 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〉 |
---|
[475] | 430 | else |
---|
[820] | 431 | 〈〈RealInstruction (DIV … ACC_A ACC_B), pc〉, 4〉 |
---|
[475] | 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 |
---|
[1604] | 437 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉 |
---|
[475] | 438 | else |
---|
| 439 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 440 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉 |
---|
[475] | 441 | else |
---|
[1604] | 442 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈SJMP … (RELATIVE b1), pc〉, 2〉 |
---|
[475] | 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 |
---|
[1604] | 448 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉)))))), pc〉, 1〉 |
---|
[475] | 449 | else |
---|
| 450 | let 〈b,v〉≝ head … v in if b then |
---|
| 451 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 452 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉)))))), pc〉, 1〉 |
---|
[475] | 453 | else |
---|
| 454 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 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〉 |
---|
[475] | 456 | else |
---|
[1604] | 457 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉 |
---|
[475] | 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 |
---|
[1604] | 463 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉 |
---|
[475] | 464 | else |
---|
| 465 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 466 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉 |
---|
[475] | 467 | else |
---|
[1604] | 468 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JNZ … (RELATIVE b1)), pc〉, 2〉 |
---|
[475] | 469 | else |
---|
| 470 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 471 | 〈〈RealInstruction (XRL … (inl … 〈ACC_A,REGISTER v〉)), pc〉, 1〉 |
---|
[475] | 472 | else |
---|
| 473 | let 〈b,v〉≝ head … v in if b then |
---|
| 474 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 475 | 〈〈RealInstruction (XRL … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, 1〉 |
---|
[475] | 476 | else |
---|
| 477 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 478 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉 |
---|
[475] | 479 | else |
---|
[1604] | 480 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉 |
---|
[475] | 481 | else |
---|
| 482 | let 〈b,v〉≝ head … v in if b then |
---|
| 483 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 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〉 |
---|
[475] | 485 | else |
---|
[1604] | 486 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉 |
---|
[475] | 487 | else |
---|
| 488 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 489 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉 |
---|
[475] | 490 | else |
---|
[1604] | 491 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JZ … (RELATIVE b1)), pc〉, 2〉 |
---|
[475] | 492 | else |
---|
| 493 | let 〈b,v〉≝ head … v in if b then |
---|
| 494 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 495 | 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,REGISTER v〉))), pc〉, 1〉 |
---|
[475] | 496 | else |
---|
| 497 | let 〈b,v〉≝ head … v in if b then |
---|
| 498 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 499 | 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))), pc〉, 1〉 |
---|
[475] | 500 | else |
---|
| 501 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 502 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉 |
---|
[475] | 503 | else |
---|
[1604] | 504 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉 |
---|
[475] | 505 | else |
---|
| 506 | let 〈b,v〉≝ head … v in if b then |
---|
| 507 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 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〉 |
---|
[475] | 509 | else |
---|
[1604] | 510 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉 |
---|
[475] | 511 | else |
---|
| 512 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 513 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉 |
---|
[475] | 514 | else |
---|
[1604] | 515 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JNC … (RELATIVE b1)), pc〉, 2〉 |
---|
[475] | 516 | else |
---|
| 517 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 518 | 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,REGISTER v〉))), pc〉, 1〉 |
---|
[475] | 519 | else |
---|
| 520 | let 〈b,v〉≝ head … v in if b then |
---|
| 521 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 522 | 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))), pc〉, 1〉 |
---|
[475] | 523 | else |
---|
| 524 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 525 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉 |
---|
[475] | 526 | else |
---|
[1604] | 527 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉 |
---|
[475] | 528 | else |
---|
| 529 | let 〈b,v〉≝ head … v in if b then |
---|
| 530 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 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〉 |
---|
[475] | 532 | else |
---|
[1604] | 533 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉 |
---|
[475] | 534 | else |
---|
| 535 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 536 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉 |
---|
[475] | 537 | else |
---|
[1604] | 538 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JC … (RELATIVE b1)), pc〉, 2〉 |
---|
[475] | 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 |
---|
[820] | 543 | 〈〈RealInstruction (ADDC … ACC_A (REGISTER v)), pc〉, 1〉 |
---|
[475] | 544 | else |
---|
| 545 | let 〈b,v〉≝ head … v in if b then |
---|
| 546 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 547 | 〈〈RealInstruction (ADDC … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉 |
---|
[475] | 548 | else |
---|
| 549 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 550 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DIRECT b1)), pc〉, 1〉 |
---|
[475] | 551 | else |
---|
[1604] | 552 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DATA b1)), pc〉, 1〉 |
---|
[475] | 553 | else |
---|
| 554 | let 〈b,v〉≝ head … v in if b then |
---|
| 555 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 556 | 〈〈RealInstruction (RLC … ACC_A), pc〉, 1〉 |
---|
[475] | 557 | else |
---|
[820] | 558 | 〈〈RealInstruction (RETI …), pc〉, 2〉 |
---|
[475] | 559 | else |
---|
| 560 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 561 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉 |
---|
[475] | 562 | else |
---|
[1604] | 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〉 |
---|
[475] | 564 | else |
---|
| 565 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 566 | 〈〈RealInstruction (ADD … ACC_A (REGISTER v)), pc〉, 1〉 |
---|
[475] | 567 | else |
---|
| 568 | let 〈b,v〉≝ head … v in if b then |
---|
| 569 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 570 | 〈〈RealInstruction (ADD … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉 |
---|
[475] | 571 | else |
---|
| 572 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 573 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DIRECT b1)), pc〉, 1〉 |
---|
[475] | 574 | else |
---|
[1604] | 575 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DATA b1)), pc〉, 1〉 |
---|
[475] | 576 | else |
---|
| 577 | let 〈b,v〉≝ head … v in if b then |
---|
| 578 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 579 | 〈〈RealInstruction (RL … ACC_A), pc〉, 1〉 |
---|
[475] | 580 | else |
---|
[820] | 581 | 〈〈RealInstruction (RET …), pc〉, 2〉 |
---|
[475] | 582 | else |
---|
| 583 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 584 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉 |
---|
[475] | 585 | else |
---|
[1604] | 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〉 |
---|
[475] | 587 | else |
---|
| 588 | let 〈b,v〉≝ head … v in if b then |
---|
| 589 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 590 | 〈〈RealInstruction (DEC … (REGISTER v)), pc〉, 1〉 |
---|
[475] | 591 | else |
---|
| 592 | let 〈b,v〉≝ head … v in if b then |
---|
| 593 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 594 | 〈〈RealInstruction (DEC … (INDIRECT (from_singl … v))), pc〉, 1〉 |
---|
[475] | 595 | else |
---|
| 596 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 597 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (DEC … (DIRECT b1)), pc〉, 1〉 |
---|
[475] | 598 | else |
---|
[820] | 599 | 〈〈RealInstruction (DEC … ACC_A), pc〉, 1〉 |
---|
[475] | 600 | else |
---|
| 601 | let 〈b,v〉≝ head … v in if b then |
---|
| 602 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 603 | 〈〈RealInstruction (RRC … ACC_A), pc〉, 1〉 |
---|
[475] | 604 | else |
---|
[1604] | 605 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉 |
---|
[475] | 606 | else |
---|
| 607 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 608 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉 |
---|
[475] | 609 | else |
---|
[1604] | 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〉 |
---|
[475] | 611 | else |
---|
| 612 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 613 | 〈〈RealInstruction (INC … (REGISTER v)), pc〉, 1〉 |
---|
[475] | 614 | else |
---|
| 615 | let 〈b,v〉≝ head … v in if b then |
---|
| 616 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 617 | 〈〈RealInstruction (INC … (INDIRECT (from_singl … v))), pc〉, 1〉 |
---|
[475] | 618 | else |
---|
| 619 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 620 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (INC … (DIRECT b1)), pc〉, 1〉 |
---|
[475] | 621 | else |
---|
[820] | 622 | 〈〈RealInstruction (INC … ACC_A), pc〉, 1〉 |
---|
[475] | 623 | else |
---|
| 624 | let 〈b,v〉≝ head … v in if b then |
---|
| 625 | let 〈b,v〉≝ head … v in if b then |
---|
[820] | 626 | 〈〈RealInstruction (RR … ACC_A), pc〉, 1〉 |
---|
[475] | 627 | else |
---|
[1604] | 628 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉 |
---|
[475] | 629 | else |
---|
| 630 | let 〈b,v〉≝ head … v in if b then |
---|
[1604] | 631 | let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉 |
---|
[475] | 632 | else |
---|
[820] | 633 | 〈〈RealInstruction (NOP …), pc〉, 1〉. |
---|
[1604] | 634 | % |
---|
[475] | 635 | qed. |
---|
[876] | 636 | |
---|
[1604] | 637 | definition fetch: ∀code_memory: BitVectorTrie Byte 16. |
---|
| 638 | ∀program_counter: Word. instruction × Word × nat ≝ |
---|
[1591] | 639 | λpmem: BitVectorTrie Byte 16. |
---|
| 640 | λpc: Word. |
---|
[1604] | 641 | let 〈word, byte〉 ≝ next pmem pc in |
---|
[1946] | 642 | fetch0 pmem word byte. |
---|