Changeset 1666 for src/ASM/Interpret.ma
 Timestamp:
 Jan 28, 2012, 1:42:15 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Interpret.ma
r1606 r1666 1 include "ASM/Status .ma".1 include "ASM/StatusProofs.ma". 2 2 include "ASM/Fetch.ma". 3 3 … … 119 119 include alias "ASM/BitVectorTrie.ma". 120 120 121 122 lemma set_flags_ignores_clock:123 ∀M,s,f1,f2,f3. clock M s = clock … (set_flags … s f1 f2 f3).124 //125 qed.126 127 lemma set_program_counter_ignores_clock:128 ∀M: Type[0].129 ∀s: PreStatus M.130 ∀pc: Word.131 clock M (set_program_counter … s pc) = clock … s.132 #M #s #pc %133 qed.134 135 lemma set_low_internal_ram_ignores_clock:136 ∀M: Type[0].137 ∀s: PreStatus M.138 ∀ram: BitVectorTrie Byte 7.139 clock … (set_low_internal_ram … s ram) = clock … s.140 #M #s #ram %141 qed.142 143 lemma set_high_internal_ram_ignores_clock:144 ∀m: Type[0].145 ∀s: PreStatus m.146 ∀ram: BitVectorTrie Byte 7.147 clock … (set_high_internal_ram … s ram) = clock … s.148 #m #s #ram %149 qed.150 151 lemma set_8051_sfr_ignores_clock:152 ∀M: Type[0].153 ∀s: PreStatus M.154 ∀sfr: SFR8051.155 ∀v: Byte.156 clock … (set_8051_sfr ? s sfr v) = clock … s.157 #M #s #sfr #v %158 qed.159 160 lemma write_at_stack_pointer_ignores_clock:161 ∀m: Type[0].162 ∀s: PreStatus m.163 ∀v: Byte.164 clock … (write_at_stack_pointer m s v) = clock … s.165 #m #s #v166 whd in match write_at_stack_pointer; normalize nodelta167 cases(split … 4 4 ?) #nu #nl normalize nodelta168 cases(get_index_v … 4 nu 0 ?) normalize nodelta169 [ >set_low_internal_ram_ignores_clock  >set_high_internal_ram_ignores_clock ] %170 qed.171 172 lemma clock_set_clock:173 ∀M: Type[0].174 ∀s: PreStatus M.175 ∀v.176 clock … (set_clock … s v) = v.177 #M #s #v %178 qed.179 180 121 definition execute_1_preinstruction': 181 122 ∀ticks: nat × nat. 182 ∀a, m: Type[0]. (a → PreStatusm → Word) → preinstruction a →183 ∀s: PreStatus m .184 Σs': PreStatus m .185 Or (clock … s' = \fst ticks + clock … s) (clock …s' = \snd ticks + clock … s) ≝123 ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → preinstruction a → 124 ∀s: PreStatus m cm. 125 Σs': PreStatus m cm. 126 Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) ≝ 186 127 λticks: nat × nat. 187 λa, m: Type[0]. 188 λaddr_of: a → PreStatus m → Word.128 λa, m: Type[0]. λcm. 129 λaddr_of: a → PreStatus m cm → Word. 189 130 λinstr: preinstruction a. 190 λs: PreStatus m .191 let add_ticks1 ≝ λs: PreStatus m . set_clock … s (\fst ticks + clock …s) in192 let add_ticks2 ≝ λs: PreStatus m . set_clock … s (\snd ticks + clock …s) in193 match instr return λx. Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock …s) with131 λs: PreStatus m cm. 132 let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in 133 let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in 134 match instr in preinstruction return λx. Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock ?? s) (clock ?? s' = \snd ticks + clock ?? s) with 194 135 [ ADD addr1 addr2 ⇒ 195 136 let s ≝ add_ticks1 s in 196 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ?s false addr1)197 (get_arg_8 ?s false addr2) false in137 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1) 138 (get_arg_8 … s false addr2) false in 198 139 let cy_flag ≝ get_index' ? O ? flags in 199 140 let ac_flag ≝ get_index' ? 1 ? flags in 200 141 let ov_flag ≝ get_index' ? 2 ? flags in 201 let s ≝ set_arg_8 ?s ACC_A result in202 set_flags ?s cy_flag (Some Bit ac_flag) ov_flag142 let s ≝ set_arg_8 … s ACC_A result in 143 set_flags … s cy_flag (Some Bit ac_flag) ov_flag 203 144  ADDC addr1 addr2 ⇒ 204 145 let s ≝ add_ticks1 s in 205 let old_cy_flag ≝ get_cy_flag ? s in206 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ?s false addr1)207 (get_arg_8 ?s false addr2) old_cy_flag in146 let old_cy_flag ≝ get_cy_flag ?? s in 147 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1) 148 (get_arg_8 … s false addr2) old_cy_flag in 208 149 let cy_flag ≝ get_index' ? O ? flags in 209 150 let ac_flag ≝ get_index' ? 1 ? flags in 210 151 let ov_flag ≝ get_index' ? 2 ? flags in 211 let s ≝ set_arg_8 ?s ACC_A result in212 set_flags ?s cy_flag (Some Bit ac_flag) ov_flag152 let s ≝ set_arg_8 … s ACC_A result in 153 set_flags … s cy_flag (Some Bit ac_flag) ov_flag 213 154  SUBB addr1 addr2 ⇒ 214 155 let s ≝ add_ticks1 s in 215 let old_cy_flag ≝ get_cy_flag ? s in216 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ?s false addr1)217 (get_arg_8 ?s false addr2) old_cy_flag in156 let old_cy_flag ≝ get_cy_flag ?? s in 157 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1) 158 (get_arg_8 … s false addr2) old_cy_flag in 218 159 let cy_flag ≝ get_index' ? O ? flags in 219 160 let ac_flag ≝ get_index' ? 1 ? flags in 220 161 let ov_flag ≝ get_index' ? 2 ? flags in 221 let s ≝ set_arg_8 ?s ACC_A result in222 set_flags ?s cy_flag (Some Bit ac_flag) ov_flag162 let s ≝ set_arg_8 … s ACC_A result in 163 set_flags … s cy_flag (Some Bit ac_flag) ov_flag 223 164  ANL addr ⇒ 224 165 let s ≝ add_ticks1 s in … … 228 169 [ inl l' ⇒ 229 170 let 〈addr1, addr2〉 ≝ l' in 230 let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ?s true addr2) in231 set_arg_8 ?s addr1 and_val171 let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 172 set_arg_8 … s addr1 and_val 232 173  inr r ⇒ 233 174 let 〈addr1, addr2〉 ≝ r in 234 let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ?s true addr2) in235 set_arg_8 ?s addr1 and_val175 let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 176 set_arg_8 … s addr1 and_val 236 177 ] 237 178  inr r ⇒ 238 179 let 〈addr1, addr2〉 ≝ r in 239 let and_val ≝ andb (get_cy_flag ? s) (get_arg_1 ?s addr2 true) in240 set_flags ? s and_val (None ?) (get_ov_flag? s)180 let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in 181 set_flags … s and_val (None ?) (get_ov_flag ?? s) 241 182 ] 242 183  ORL addr ⇒ … … 247 188 [ inl l' ⇒ 248 189 let 〈addr1, addr2〉 ≝ l' in 249 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ?s true addr2) in250 set_arg_8 ?s addr1 or_val190 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 191 set_arg_8 … s addr1 or_val 251 192  inr r ⇒ 252 193 let 〈addr1, addr2〉 ≝ r in 253 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ?s true addr2) in254 set_arg_8 ?s addr1 or_val194 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 195 set_arg_8 … s addr1 or_val 255 196 ] 256 197  inr r ⇒ 257 198 let 〈addr1, addr2〉 ≝ r in 258 let or_val ≝ (get_cy_flag ? s) ∨ (get_arg_1 ?s addr2 true) in259 set_flags ? s or_val (None ?) (get_ov_flag ?s)199 let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in 200 set_flags … s or_val (None ?) (get_ov_flag … s) 260 201 ] 261 202  XRL addr ⇒ … … 264 205 [ inl l' ⇒ 265 206 let 〈addr1, addr2〉 ≝ l' in 266 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ?s true addr2) in267 set_arg_8 ?s addr1 xor_val207 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 208 set_arg_8 … s addr1 xor_val 268 209  inr r ⇒ 269 210 let 〈addr1, addr2〉 ≝ r in 270 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ?s true addr2) in271 set_arg_8 ?s addr1 xor_val211 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 212 set_arg_8 … s addr1 xor_val 272 213 ] 273 214  INC addr ⇒ 274 match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → Σs': PreStatus m . Or (clock … s' = \fst ticks + clock … s) (clock …s' = \snd ticks + clock … s) with215 match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) with 275 216 [ ACC_A ⇒ λacc_a: True. 276 217 let s' ≝ add_ticks1 s in 277 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ?s' true ACC_A) (bitvector_of_nat 8 1) in278 set_arg_8 ?s' ACC_A result218 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in 219 set_arg_8 … s' ACC_A result 279 220  REGISTER r ⇒ λregister: True. 280 221 let s' ≝ add_ticks1 s in 281 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ?s' true (REGISTER r)) (bitvector_of_nat 8 1) in282 set_arg_8 ?s' (REGISTER r) result222 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in 223 set_arg_8 … s' (REGISTER r) result 283 224  DIRECT d ⇒ λdirect: True. 284 225 let s' ≝ add_ticks1 s in 285 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ?s' true (DIRECT d)) (bitvector_of_nat 8 1) in286 set_arg_8 ?s' (DIRECT d) result226 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in 227 set_arg_8 … s' (DIRECT d) result 287 228  INDIRECT i ⇒ λindirect: True. 288 229 let s' ≝ add_ticks1 s in 289 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ?s' true (INDIRECT i)) (bitvector_of_nat 8 1) in290 set_arg_8 ?s' (INDIRECT i) result230 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in 231 set_arg_8 … s' (INDIRECT i) result 291 232  DPTR ⇒ λdptr: True. 292 233 let s' ≝ add_ticks1 s in 293 let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr ?s' SFR_DPL) (bitvector_of_nat 8 1) in294 let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr ?s' SFR_DPH) (zero 8) carry in295 let s ≝ set_8051_sfr ?s' SFR_DPL bl in296 set_8051_sfr ?s' SFR_DPH bu234 let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in 235 let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in 236 let s ≝ set_8051_sfr … s' SFR_DPL bl in 237 set_8051_sfr … s' SFR_DPH bu 297 238  _ ⇒ λother: False. ⊥ 298 239 ] (subaddressing_modein … addr) … … 302 243  DEC addr ⇒ 303 244 let s ≝ add_ticks1 s in 304 let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 ?s true addr) (bitvector_of_nat 8 1) false in305 set_arg_8 ?s addr result245 let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in 246 set_arg_8 … s addr result 306 247  MUL addr1 addr2 ⇒ 307 248 let s ≝ add_ticks1 s in 308 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ?s SFR_ACC_A) in309 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ?s SFR_ACC_B) in249 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in 250 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in 310 251 let product ≝ acc_a_nat * acc_b_nat in 311 252 let ov_flag ≝ product ≥ 256 in 312 253 let low ≝ bitvector_of_nat 8 (product mod 256) in 313 254 let high ≝ bitvector_of_nat 8 (product ÷ 256) in 314 let s ≝ set_8051_sfr ?s SFR_ACC_A low in315 set_8051_sfr ?s SFR_ACC_B high255 let s ≝ set_8051_sfr … s SFR_ACC_A low in 256 set_8051_sfr … s SFR_ACC_B high 316 257  DIV addr1 addr2 ⇒ 317 258 let s ≝ add_ticks1 s in 318 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ?s SFR_ACC_A) in319 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ?s SFR_ACC_B) in259 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in 260 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in 320 261 match acc_b_nat with 321 [ O ⇒ set_flags ?s false (None Bit) true262 [ O ⇒ set_flags … s false (None Bit) true 322 263  S o ⇒ 323 264 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in 324 265 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in 325 let s ≝ set_8051_sfr ?s SFR_ACC_A q in326 let s ≝ set_8051_sfr ?s SFR_ACC_B r in327 set_flags ?s false (None Bit) false266 let s ≝ set_8051_sfr … s SFR_ACC_A q in 267 let s ≝ set_8051_sfr … s SFR_ACC_B r in 268 set_flags … s false (None Bit) false 328 269 ] 329 270  DA addr ⇒ 330 271 let s ≝ add_ticks1 s in 331 let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr ?s SFR_ACC_A) in332 if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag ?s) then333 let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr ?s SFR_ACC_A) (bitvector_of_nat 8 6) false in272 let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr … s SFR_ACC_A) in 273 if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then 274 let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in 334 275 let cy_flag ≝ get_index' ? O ? flags in 335 276 let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in … … 337 278 let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in 338 279 let new_acc ≝ nu @@ acc_nl' in 339 let s ≝ set_8051_sfr ?s SFR_ACC_A new_acc in340 set_flags ? s cy_flag (Some ? (get_ac_flag ? s)) (get_ov_flag ?s)280 let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in 281 set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s) 341 282 else 342 283 s … … 344 285 s 345 286  CLR addr ⇒ 346 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m . Or (clock … s' = \fst ticks + clock … s) (clock …s' = \snd ticks + clock … s) with287 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) with 347 288 [ ACC_A ⇒ λacc_a: True. 348 289 let s ≝ add_ticks1 s in 349 set_arg_8 ?s ACC_A (zero 8)290 set_arg_8 … s ACC_A (zero 8) 350 291  CARRY ⇒ λcarry: True. 351 292 let s ≝ add_ticks1 s in 352 set_arg_1 ?s CARRY false293 set_arg_1 … s CARRY false 353 294  BIT_ADDR b ⇒ λbit_addr: True. 354 295 let s ≝ add_ticks1 s in 355 set_arg_1 ?s (BIT_ADDR b) false296 set_arg_1 … s (BIT_ADDR b) false 356 297  _ ⇒ λother: False. ⊥ 357 298 ] (subaddressing_modein … addr) 358 299  CPL addr ⇒ 359 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m . Or (clock … s' = \fst ticks + clock … s) (clock …s' = \snd ticks + clock … s) with300 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) with 360 301 [ ACC_A ⇒ λacc_a: True. 361 302 let s ≝ add_ticks1 s in 362 let old_acc ≝ get_8051_sfr ?s SFR_ACC_A in303 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 363 304 let new_acc ≝ negation_bv ? old_acc in 364 set_8051_sfr ?s SFR_ACC_A new_acc305 set_8051_sfr … s SFR_ACC_A new_acc 365 306  CARRY ⇒ λcarry: True. 366 307 let s ≝ add_ticks1 s in 367 let old_cy_flag ≝ get_arg_1 ?s CARRY true in308 let old_cy_flag ≝ get_arg_1 … s CARRY true in 368 309 let new_cy_flag ≝ ¬old_cy_flag in 369 set_arg_1 ?s CARRY new_cy_flag310 set_arg_1 … s CARRY new_cy_flag 370 311  BIT_ADDR b ⇒ λbit_addr: True. 371 312 let s ≝ add_ticks1 s in 372 let old_bit ≝ get_arg_1 ?s (BIT_ADDR b) true in313 let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in 373 314 let new_bit ≝ ¬old_bit in 374 set_arg_1 ?s (BIT_ADDR b) new_bit315 set_arg_1 … s (BIT_ADDR b) new_bit 375 316  _ ⇒ λother: False. ? 376 317 ] (subaddressing_modein … addr) 377 318  SETB b ⇒ 378 319 let s ≝ add_ticks1 s in 379 set_arg_1 ?s b false320 set_arg_1 … s b false 380 321  RL _ ⇒ (* DPM: always ACC_A *) 381 322 let s ≝ add_ticks1 s in 382 let old_acc ≝ get_8051_sfr ?s SFR_ACC_A in323 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 383 324 let new_acc ≝ rotate_left … 1 old_acc in 384 set_8051_sfr ?s SFR_ACC_A new_acc325 set_8051_sfr … s SFR_ACC_A new_acc 385 326  RR _ ⇒ (* DPM: always ACC_A *) 386 327 let s ≝ add_ticks1 s in 387 let old_acc ≝ get_8051_sfr ?s SFR_ACC_A in328 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 388 329 let new_acc ≝ rotate_right … 1 old_acc in 389 set_8051_sfr ?s SFR_ACC_A new_acc330 set_8051_sfr … s SFR_ACC_A new_acc 390 331  RLC _ ⇒ (* DPM: always ACC_A *) 391 332 let s ≝ add_ticks1 s in 392 let old_cy_flag ≝ get_cy_flag ? s in393 let old_acc ≝ get_8051_sfr ?s SFR_ACC_A in333 let old_cy_flag ≝ get_cy_flag ?? s in 334 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 394 335 let new_cy_flag ≝ get_index' ? O ? old_acc in 395 336 let new_acc ≝ shift_left … 1 old_acc old_cy_flag in 396 let s ≝ set_arg_1 ?s CARRY new_cy_flag in397 set_8051_sfr ?s SFR_ACC_A new_acc337 let s ≝ set_arg_1 … s CARRY new_cy_flag in 338 set_8051_sfr … s SFR_ACC_A new_acc 398 339  RRC _ ⇒ (* DPM: always ACC_A *) 399 340 let s ≝ add_ticks1 s in 400 let old_cy_flag ≝ get_cy_flag ? s in401 let old_acc ≝ get_8051_sfr ?s SFR_ACC_A in341 let old_cy_flag ≝ get_cy_flag ?? s in 342 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 402 343 let new_cy_flag ≝ get_index' ? 7 ? old_acc in 403 344 let new_acc ≝ shift_right … 1 old_acc old_cy_flag in 404 let s ≝ set_arg_1 ?s CARRY new_cy_flag in405 set_8051_sfr ?s SFR_ACC_A new_acc345 let s ≝ set_arg_1 … s CARRY new_cy_flag in 346 set_8051_sfr … s SFR_ACC_A new_acc 406 347  SWAP _ ⇒ (* DPM: always ACC_A *) 407 348 let s ≝ add_ticks1 s in 408 let old_acc ≝ get_8051_sfr ?s SFR_ACC_A in349 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 409 350 let 〈nu,nl〉 ≝ split ? 4 4 old_acc in 410 351 let new_acc ≝ nl @@ nu in 411 set_8051_sfr ?s SFR_ACC_A new_acc352 set_8051_sfr … s SFR_ACC_A new_acc 412 353  PUSH addr ⇒ 413 match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m . Or (clock … s' = \fst ticks + clock … s) (clock …s' = \snd ticks + clock … s) with354 match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) with 414 355 [ DIRECT d ⇒ λdirect: True. 415 356 let s ≝ add_ticks1 s in 416 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ?s SFR_SP) (bitvector_of_nat 8 1) in417 let s ≝ set_8051_sfr ?s SFR_SP new_sp in418 write_at_stack_pointer ?s d357 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 358 let s ≝ set_8051_sfr … s SFR_SP new_sp in 359 write_at_stack_pointer … s d 419 360  _ ⇒ λother: False. ⊥ 420 361 ] (subaddressing_modein … addr) 421 362  POP addr ⇒ 422 363 let s ≝ add_ticks1 s in 423 let contents ≝ read_at_stack_pointer ? s in424 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ?s SFR_SP) (bitvector_of_nat 8 1) false in425 let s ≝ set_8051_sfr ?s SFR_SP new_sp in426 set_arg_8 ?s addr contents364 let contents ≝ read_at_stack_pointer ?? s in 365 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 366 let s ≝ set_8051_sfr … s SFR_SP new_sp in 367 set_arg_8 … s addr contents 427 368  XCH addr1 addr2 ⇒ 428 369 let s ≝ add_ticks1 s in 429 let old_addr ≝ get_arg_8 ?s false addr2 in430 let old_acc ≝ get_8051_sfr ?s SFR_ACC_A in431 let s ≝ set_8051_sfr ?s SFR_ACC_A old_addr in432 set_arg_8 ?s addr2 old_acc370 let old_addr ≝ get_arg_8 … s false addr2 in 371 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 372 let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in 373 set_arg_8 … s addr2 old_acc 433 374  XCHD addr1 addr2 ⇒ 434 375 let s ≝ add_ticks1 s in 435 let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr ?s SFR_ACC_A) in436 let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 ?s false addr2) in376 let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr … s SFR_ACC_A) in 377 let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 … s false addr2) in 437 378 let new_acc ≝ acc_nu @@ arg_nl in 438 379 let new_arg ≝ arg_nu @@ acc_nl in 439 let s ≝ set_8051_sfr ?s SFR_ACC_A new_acc in440 set_arg_8 ?s addr2 new_arg380 let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in 381 set_arg_8 … s addr2 new_arg 441 382  RET ⇒ 442 383 let s ≝ add_ticks1 s in 443 let high_bits ≝ read_at_stack_pointer ? s in444 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ?s SFR_SP) (bitvector_of_nat 8 1) false in445 let s ≝ set_8051_sfr ?s SFR_SP new_sp in446 let low_bits ≝ read_at_stack_pointer ? s in447 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ?s SFR_SP) (bitvector_of_nat 8 1) false in448 let s ≝ set_8051_sfr ?s SFR_SP new_sp in384 let high_bits ≝ read_at_stack_pointer ?? s in 385 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 386 let s ≝ set_8051_sfr … s SFR_SP new_sp in 387 let low_bits ≝ read_at_stack_pointer ?? s in 388 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 389 let s ≝ set_8051_sfr … s SFR_SP new_sp in 449 390 let new_pc ≝ high_bits @@ low_bits in 450 set_program_counter ?s new_pc391 set_program_counter … s new_pc 451 392  RETI ⇒ 452 393 let s ≝ add_ticks1 s in 453 let high_bits ≝ read_at_stack_pointer ? s in454 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ?s SFR_SP) (bitvector_of_nat 8 1) false in455 let s ≝ set_8051_sfr ?s SFR_SP new_sp in456 let low_bits ≝ read_at_stack_pointer ? s in457 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ?s SFR_SP) (bitvector_of_nat 8 1) false in458 let s ≝ set_8051_sfr ?s SFR_SP new_sp in394 let high_bits ≝ read_at_stack_pointer ?? s in 395 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 396 let s ≝ set_8051_sfr … s SFR_SP new_sp in 397 let low_bits ≝ read_at_stack_pointer ?? s in 398 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 399 let s ≝ set_8051_sfr … s SFR_SP new_sp in 459 400 let new_pc ≝ high_bits @@ low_bits in 460 set_program_counter ?s new_pc401 set_program_counter … s new_pc 461 402  MOVX addr ⇒ 462 403 let s ≝ add_ticks1 s in … … 465 406 [ inl l ⇒ 466 407 let 〈addr1, addr2〉 ≝ l in 467 set_arg_8 ? s addr1 (get_arg_8 ?s false addr2)408 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 468 409  inr r ⇒ 469 410 let 〈addr1, addr2〉 ≝ r in 470 set_arg_8 ? s addr1 (get_arg_8 ?s false addr2)411 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 471 412 ] 472 413  MOV addr ⇒ … … 483 424 [ inl l'''' ⇒ 484 425 let 〈addr1, addr2〉 ≝ l'''' in 485 set_arg_8 ? s addr1 (get_arg_8 ?s false addr2)426 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 486 427  inr r'''' ⇒ 487 428 let 〈addr1, addr2〉 ≝ r'''' in 488 set_arg_8 ? s addr1 (get_arg_8 ?s false addr2)429 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 489 430 ] 490 431  inr r''' ⇒ 491 432 let 〈addr1, addr2〉 ≝ r''' in 492 set_arg_8 ? s addr1 (get_arg_8 ?s false addr2)433 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 493 434 ] 494 435  inr r'' ⇒ 495 436 let 〈addr1, addr2〉 ≝ r'' in 496 set_arg_16 ? s (get_arg_16 ?s addr2) addr1437 set_arg_16 … s (get_arg_16 … s addr2) addr1 497 438 ] 498 439  inr r ⇒ 499 440 let 〈addr1, addr2〉 ≝ r in 500 set_arg_1 ? s addr1 (get_arg_1 ?s addr2 false)441 set_arg_1 … s addr1 (get_arg_1 … s addr2 false) 501 442 ] 502 443  inr r ⇒ 503 444 let 〈addr1, addr2〉 ≝ r in 504 set_arg_1 ? s addr1 (get_arg_1 ?s addr2 false)445 set_arg_1 … s addr1 (get_arg_1 … s addr2 false) 505 446 ] 506 447  JC addr ⇒ 507 if get_cy_flag ? s then448 if get_cy_flag ?? s then 508 449 let s ≝ add_ticks1 s in 509 set_program_counter ?s (addr_of addr s)450 set_program_counter … s (addr_of addr s) 510 451 else 511 452 let s ≝ add_ticks2 s in 512 453 s 513 454  JNC addr ⇒ 514 if ¬(get_cy_flag ? s) then455 if ¬(get_cy_flag ?? s) then 515 456 let s ≝ add_ticks1 s in 516 set_program_counter ?s (addr_of addr s)457 set_program_counter … s (addr_of addr s) 517 458 else 518 459 let s ≝ add_ticks2 s in 519 460 s 520 461  JB addr1 addr2 ⇒ 521 if get_arg_1 ?s addr1 false then462 if get_arg_1 … s addr1 false then 522 463 let s ≝ add_ticks1 s in 523 set_program_counter ?s (addr_of addr2 s)464 set_program_counter … s (addr_of addr2 s) 524 465 else 525 466 let s ≝ add_ticks2 s in 526 467 s 527 468  JNB addr1 addr2 ⇒ 528 if ¬(get_arg_1 ?s addr1 false) then469 if ¬(get_arg_1 … s addr1 false) then 529 470 let s ≝ add_ticks1 s in 530 set_program_counter ?s (addr_of addr2 s)471 set_program_counter … s (addr_of addr2 s) 531 472 else 532 473 let s ≝ add_ticks2 s in 533 474 s 534 475  JBC addr1 addr2 ⇒ 535 let s ≝ set_arg_1 ?s addr1 false in536 if get_arg_1 ?s addr1 false then476 let s ≝ set_arg_1 … s addr1 false in 477 if get_arg_1 … s addr1 false then 537 478 let s ≝ add_ticks1 s in 538 set_program_counter ?s (addr_of addr2 s)479 set_program_counter … s (addr_of addr2 s) 539 480 else 540 481 let s ≝ add_ticks2 s in 541 482 s 542 483  JZ addr ⇒ 543 if eq_bv ? (get_8051_sfr ?s SFR_ACC_A) (zero 8) then484 if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then 544 485 let s ≝ add_ticks1 s in 545 set_program_counter ?s (addr_of addr s)486 set_program_counter … s (addr_of addr s) 546 487 else 547 488 let s ≝ add_ticks2 s in 548 489 s 549 490  JNZ addr ⇒ 550 if ¬(eq_bv ? (get_8051_sfr ?s SFR_ACC_A) (zero 8)) then491 if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then 551 492 let s ≝ add_ticks1 s in 552 set_program_counter ?s (addr_of addr s)493 set_program_counter … s (addr_of addr s) 553 494 else 554 495 let s ≝ add_ticks2 s in … … 558 499 [ inl l ⇒ 559 500 let 〈addr1, addr2'〉 ≝ l in 560 let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ?s false addr1))561 (nat_of_bitvector ? (get_arg_8 ?s false addr2')) in562 if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ?s false addr2')) then501 let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1)) 502 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in 503 if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then 563 504 let s ≝ add_ticks1 s in 564 let s ≝ set_program_counter ?s (addr_of addr2 s) in565 set_flags ? s new_cy (None ?) (get_ov_flag? s)505 let s ≝ set_program_counter … s (addr_of addr2 s) in 506 set_flags … s new_cy (None ?) (get_ov_flag ?? s) 566 507 else 567 508 let s ≝ add_ticks2 s in 568 set_flags ? s new_cy (None ?) (get_ov_flag? s)509 set_flags … s new_cy (None ?) (get_ov_flag ?? s) 569 510  inr r' ⇒ 570 511 let 〈addr1, addr2'〉 ≝ r' in 571 let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ?s false addr1))572 (nat_of_bitvector ? (get_arg_8 ?s false addr2')) in573 if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ?s false addr2')) then512 let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1)) 513 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in 514 if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then 574 515 let s ≝ add_ticks1 s in 575 let s ≝ set_program_counter ?s (addr_of addr2 s) in576 set_flags ? s new_cy (None ?) (get_ov_flag? s)516 let s ≝ set_program_counter … s (addr_of addr2 s) in 517 set_flags … s new_cy (None ?) (get_ov_flag ?? s) 577 518 else 578 519 let s ≝ add_ticks2 s in 579 set_flags ? s new_cy (None ?) (get_ov_flag? s)520 set_flags … s new_cy (None ?) (get_ov_flag ?? s) 580 521 ] 581 522  DJNZ addr1 addr2 ⇒ 582 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ?s true addr1) (bitvector_of_nat 8 1) false in583 let s ≝ set_arg_8 ?s addr1 result in523 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in 524 let s ≝ set_arg_8 … s addr1 result in 584 525 if ¬(eq_bv ? result (zero 8)) then 585 526 let s ≝ add_ticks1 s in 586 set_program_counter ?s (addr_of addr2 s)527 set_program_counter … s (addr_of addr2 s) 587 528 else 588 529 let s ≝ add_ticks2 s in 589 530 s 590 ]. (*15s*)531 _ ⇒ ? ]. (*15s*) 591 532 try (cases(other)) 592 533 try assumption (*20s*) … … 597 538 ) (*66s*) 598 539 normalize nodelta /2 by or_introl, or_intror/ (*35s*) 540 (*CSC: the times are now much longer. I suspect because the inclusion of 541 all StatusProofs makes the search space larger :( *) 599 542 qed. 600 543 601 544 definition execute_1_preinstruction: 602 545 ∀ticks: nat × nat. 603 ∀a, m: Type[0]. (a → PreStatusm → Word) → preinstruction a →604 PreStatus m → PreStatusm ≝ execute_1_preinstruction'.546 ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → preinstruction a → 547 PreStatus m cm → PreStatus m cm ≝ execute_1_preinstruction'. 605 548 606 549 lemma execute_1_preinstruction_ok: 607 ∀ticks,a,m, f,i,s.608 clock ? (execute_1_preinstruction ticks am f i s) = \fst ticks + clock … s ∨609 clock ? (execute_1_preinstruction ticks am f i s) = \snd ticks + clock … s.610 #ticks #a #m # f #i #s whd in match execute_1_preinstruction; normalize nodelta @pi2550 ∀ticks,a,m,cm,f,i,s. 551 clock ?? (execute_1_preinstruction ticks a m cm f i s) = \fst ticks + clock … s ∨ 552 clock ?? (execute_1_preinstruction ticks a m cm f i s) = \snd ticks + clock … s. 553 #ticks #a #m #cm #f #i #s whd in match execute_1_preinstruction; normalize nodelta @pi2 611 554 qed. 612 555 613 definition execute_1_0: ∀ s: Status. ∀current:instruction × Word × nat.614 Σs': Status . clock …s' = \snd current + clock … s ≝615 λ s0,instr_pc_ticks.556 definition execute_1_0: ∀cm. ∀s: Status cm. ∀current:instruction × Word × nat. 557 Σs': Status cm. clock ?? s' = \snd current + clock … s ≝ 558 λcm,s0,instr_pc_ticks. 616 559 let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in 617 560 let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in 618 let s ≝ set_program_counter ?s0 pc in619 match instr return λ_.Status with620 [ RealInstruction instr ⇒ execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] ?561 let s ≝ set_program_counter … s0 pc in 562 match instr return λ_.Status cm with 563 [ RealInstruction instr ⇒ execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] … 621 564 (λx. λs. 622 565 match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with 623 [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ?s) (sign_extension r))566 [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter … s) (sign_extension r)) 624 567  _ ⇒ λabsd. ⊥ 625 568 ] (subaddressing_modein … x)) instr s 626 569  MOVC addr1 addr2 ⇒ 627 let s ≝ set_clock ? s (ticks + clock ?s) in628 match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs': Status . clock …s' = ticks + clock … s0 with570 let s ≝ set_clock … s (ticks + clock … s) in 571 match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with 629 572 [ ACC_DPTR ⇒ λacc_dptr: True. 630 let big_acc ≝ (zero 8) @@ (get_8051_sfr ?s SFR_ACC_A) in631 let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ?s SFR_DPL) in573 let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in 574 let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in 632 575 let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in 633 let result ≝ lookup ? ? new_addr (code_memory ? s)(zero ?) in634 set_8051_sfr ?s SFR_ACC_A result576 let result ≝ lookup ? ? new_addr cm (zero ?) in 577 set_8051_sfr … s SFR_ACC_A result 635 578  ACC_PC ⇒ λacc_pc: True. 636 let big_acc ≝ (zero 8) @@ (get_8051_sfr ?s SFR_ACC_A) in637 let 〈carry, inc_pc〉 ≝ half_add ? (program_counter ? s) (bitvector_of_nat 16 1) in579 let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in 580 let 〈carry, inc_pc〉 ≝ half_add ? (program_counter ?? s) (bitvector_of_nat 16 1) in 638 581 (* DPM: Under specified: does the carry from PC incrementation affect the *) 639 582 (* addition of the PC with the DPTR? At the moment, no. *) 640 let s ≝ set_program_counter ?s inc_pc in583 let s ≝ set_program_counter … s inc_pc in 641 584 let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in 642 let result ≝ lookup ? ? new_addr (code_memory ? s)(zero ?) in643 set_8051_sfr ?s SFR_ACC_A result585 let result ≝ lookup ? ? new_addr cm (zero ?) in 586 set_8051_sfr … s SFR_ACC_A result 644 587  _ ⇒ λother: False. ⊥ 645 588 ] (subaddressing_modein … addr2) 646 589  JMP _ ⇒ (* DPM: always indirect_dptr *) 647 let s ≝ set_clock ? s (ticks + clock ?s) in648 let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ?s SFR_DPL) in649 let big_acc ≝ (zero 8) @@ (get_8051_sfr ?s SFR_ACC_A) in590 let s ≝ set_clock … s (ticks + clock … s) in 591 let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in 592 let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in 650 593 let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in 651 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ?s) jmp_addr in652 set_program_counter ?s new_pc594 let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) jmp_addr in 595 set_program_counter … s new_pc 653 596  LJMP addr ⇒ 654 let s ≝ set_clock ? s (ticks + clock ?s) in655 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status . clock …s' = ticks + clock … s0 with597 let s ≝ set_clock … s (ticks + clock … s) in 598 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with 656 599 [ ADDR16 a ⇒ λaddr16: True. 657 set_program_counter ?s a600 set_program_counter … s a 658 601  _ ⇒ λother: False. ⊥ 659 602 ] (subaddressing_modein … addr) 660 603  SJMP addr ⇒ 661 let s ≝ set_clock ? s (ticks + clock ?s) in662 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs': Status . clock …s' = ticks + clock … s0 with604 let s ≝ set_clock … s (ticks + clock … s) in 605 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with 663 606 [ RELATIVE r ⇒ λrelative: True. 664 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ?s) (sign_extension r) in665 set_program_counter ?s new_pc607 let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) (sign_extension r) in 608 set_program_counter … s new_pc 666 609  _ ⇒ λother: False. ⊥ 667 610 ] (subaddressing_modein … addr) 668 611  AJMP addr ⇒ 669 let s ≝ set_clock ? s (ticks + clock ?s) in670 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status . clock …s' = ticks + clock … s0 with612 let s ≝ set_clock … s (ticks + clock … s) in 613 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with 671 614 [ ADDR11 a ⇒ λaddr11: True. 672 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ?s) in615 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in 673 616 let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in 674 617 let bit ≝ get_index' ? O ? nl in 675 618 let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in 676 619 let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in 677 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ?s) new_addr in678 set_program_counter ?s new_pc620 let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) new_addr in 621 set_program_counter … s new_pc 679 622  _ ⇒ λother: False. ⊥ 680 623 ] (subaddressing_modein … addr) 681 624  ACALL addr ⇒ 682 let s ≝ set_clock ? s (ticks + clock ?s) in683 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status . clock …s' = ticks + clock … s0 with625 let s ≝ set_clock … s (ticks + clock … s) in 626 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with 684 627 [ ADDR11 a ⇒ λaddr11: True. 685 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ?s SFR_SP) (bitvector_of_nat 8 1) in686 let s ≝ set_8051_sfr ?s SFR_SP new_sp in687 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ?s) in688 let s ≝ write_at_stack_pointer ?s pc_bl in689 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ?s SFR_SP) (bitvector_of_nat 8 1) in690 let s ≝ set_8051_sfr ?s SFR_SP new_sp in691 let s ≝ write_at_stack_pointer ?s pc_bu in628 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 629 let s ≝ set_8051_sfr … s SFR_SP new_sp in 630 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in 631 let s ≝ write_at_stack_pointer … s pc_bl in 632 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 633 let s ≝ set_8051_sfr … s SFR_SP new_sp in 634 let s ≝ write_at_stack_pointer … s pc_bu in 692 635 let 〈thr, eig〉 ≝ split ? 3 8 a in 693 636 let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in 694 637 let new_addr ≝ (fiv @@ thr) @@ pc_bl in 695 set_program_counter ?s new_addr638 set_program_counter … s new_addr 696 639  _ ⇒ λother: False. ⊥ 697 640 ] (subaddressing_modein … addr) 698 641  LCALL addr ⇒ 699 let s ≝ set_clock ? s (ticks + clock ?s) in700 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status . clock …s' = ticks + clock … s0 with642 let s ≝ set_clock … s (ticks + clock … s) in 643 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with 701 644 [ ADDR16 a ⇒ λaddr16: True. 702 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ?s SFR_SP) (bitvector_of_nat 8 1) in703 let s ≝ set_8051_sfr ?s SFR_SP new_sp in704 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ?s) in705 let s ≝ write_at_stack_pointer ?s pc_bl in706 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ?s SFR_SP) (bitvector_of_nat 8 1) in707 let s ≝ set_8051_sfr ?s SFR_SP new_sp in708 let s ≝ write_at_stack_pointer ?s pc_bu in709 set_program_counter ?s a645 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 646 let s ≝ set_8051_sfr … s SFR_SP new_sp in 647 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in 648 let s ≝ write_at_stack_pointer … s pc_bl in 649 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 650 let s ≝ set_8051_sfr … s SFR_SP new_sp in 651 let s ≝ write_at_stack_pointer … s pc_bu in 652 set_program_counter … s a 710 653  _ ⇒ λother: False. ⊥ 711 654 ] (subaddressing_modein … addr) 712 ]. (*10s*)655 ]. (*10s*) 713 656 [*:try assumption] 714 657 [1,2,3,4,5,7: @pi2 (*35s*) 715 8: lapply (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] ?658 8: lapply (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] … 716 659 (λx. λs. 717 660 match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with 718 [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ?s) (sign_extension r))661 [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter … s) (sign_extension r)) 719 662  _ ⇒ λabsd. ⊥ 720 663 ] (subaddressing_modein … x)) instr1 s1) try @absd * #H @H 721 664 *: normalize nodelta try // (*17s*) 722 > set_program_counter_ignores_clock// (* Andrea:??*) ]665 >clock_set_program_counter // (* Andrea:??*) ] 723 666 qed. 724 667 725 668 definition current_instruction_cost ≝ 726 λ s: Status.727 \snd (fetch (code_memory … s)(program_counter … s)).728 729 definition execute_1': ∀ s:Status.730 Σs':Status . clock … s' = current_instruction_costs + clock … s ≝731 λ s: Status.732 let instr_pc_ticks ≝ fetch (code_memory ? s) (program_counter ?s) in733 execute_1_0 s instr_pc_ticks.734 735 definition execute_1: Status → Status≝ execute_1'.736 737 lemma execute_1_ok: ∀ s. clock … (execute_1 s) = current_instruction_costs + clock … s.738 # s whd in match execute_1; normalize nodelta @pi2669 λcm.λs: Status cm. 670 \snd (fetch cm (program_counter … s)). 671 672 definition execute_1': ∀cm.∀s:Status cm. 673 Σs':Status cm. clock ?? s' = current_instruction_cost cm s + clock … s ≝ 674 λcm. λs: Status cm. 675 let instr_pc_ticks ≝ fetch cm (program_counter … s) in 676 execute_1_0 cm s instr_pc_ticks. 677 678 definition execute_1: ∀cm. Status cm → Status cm ≝ execute_1'. 679 680 lemma execute_1_ok: ∀cm.∀s. clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s. 681 #cm #s whd in match execute_1; normalize nodelta @pi2 739 682 qed. (*x Andrea: indexing takes ages here *) 740 683 741 definition execute_1_pseudo_instruction0: (nat × nat) → PseudoStatus → ? → ? → PseudoStatus≝742 λticks, s,instr,pc.743 let s ≝ set_program_counter ? s pc in684 definition execute_1_pseudo_instruction0: (nat × nat) → ∀cm. PseudoStatus cm → ? → ? → PseudoStatus cm ≝ 685 λticks,cm,s,instr,pc. 686 let s ≝ set_program_counter ?? s pc in 744 687 let s ≝ 745 688 match instr with 746 [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels y x) instr s 747  Comment cmt ⇒ 748 let s ≝ set_clock ? s (\fst ticks + clock ? s) in 749 s 689 [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels cm x) instr s 690  Comment cmt ⇒ set_clock … s (\fst ticks + clock … s) 750 691  Cost cst ⇒ s 751 692  Jmp jmp ⇒ 752 let s ≝ set_clock ? s (\fst ticks + clock ?s) in753 set_program_counter ? s (address_of_word_labels sjmp)693 let s ≝ set_clock … s (\fst ticks + clock … s) in 694 set_program_counter … s (address_of_word_labels cm jmp) 754 695  Call call ⇒ 755 let s ≝ set_clock ? s (\fst ticks + clock ?s) in756 let a ≝ address_of_word_labels scall in757 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ?s SFR_SP) (bitvector_of_nat 8 1) in758 let s ≝ set_8051_sfr ?s SFR_SP new_sp in759 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ?s) in760 let s ≝ write_at_stack_pointer ?s pc_bl in761 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ?s SFR_SP) (bitvector_of_nat 8 1) in762 let s ≝ set_8051_sfr ?s SFR_SP new_sp in763 let s ≝ write_at_stack_pointer ?s pc_bu in764 set_program_counter ?s a696 let s ≝ set_clock ?? s (\fst ticks + clock … s) in 697 let a ≝ address_of_word_labels cm call in 698 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 699 let s ≝ set_8051_sfr … s SFR_SP new_sp in 700 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in 701 let s ≝ write_at_stack_pointer … s pc_bl in 702 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 703 let s ≝ set_8051_sfr … s SFR_SP new_sp in 704 let s ≝ write_at_stack_pointer … s pc_bu in 705 set_program_counter … s a 765 706  Mov dptr ident ⇒ 766 let s ≝ set_clock ? s (\fst ticks + clock ?s) in767 let the_preamble ≝ \fst (code_memory ? s)in707 let s ≝ set_clock ?? s (\fst ticks + clock … s) in 708 let the_preamble ≝ \fst cm in 768 709 let data_labels ≝ construct_datalabels the_preamble in 769 set_arg_16 ? s (get_arg_16 ?s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr710 set_arg_16 … s (get_arg_16 … s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr 770 711 ] 771 712 in … … 775 716 qed. 776 717 777 definition execute_1_pseudo_instruction: (Word → nat × nat) → PseudoStatus → PseudoStatus≝778 λticks_of, s.779 let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ?s) in780 let ticks ≝ ticks_of (program_counter ?s) in781 execute_1_pseudo_instruction0 ticks s instr pc.782 783 let rec execute (n: nat) ( s: Status) on n: Status≝718 definition execute_1_pseudo_instruction: (Word → nat × nat) → ∀cm. PseudoStatus cm → PseudoStatus cm ≝ 719 λticks_of,cm,s. 720 let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd cm) (program_counter … s) in 721 let ticks ≝ ticks_of (program_counter … s) in 722 execute_1_pseudo_instruction0 ticks cm s instr pc. 723 724 let rec execute (n: nat) (cm:?) (s: Status cm) on n: Status cm ≝ 784 725 match n with 785 726 [ O ⇒ s 786  S o ⇒ execute o (execute_1s)727  S o ⇒ execute o … (execute_1 … s) 787 728 ]. 788 729 789 let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) ( s: PseudoStatus) on n: PseudoStatus≝730 let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (cm:?) (s: PseudoStatus cm) on n: PseudoStatus cm ≝ 790 731 match n with 791 732 [ O ⇒ s 792  S o ⇒ execute_pseudo_instruction o ticks_of (execute_1_pseudo_instruction ticks_ofs)733  S o ⇒ execute_pseudo_instruction o ticks_of … (execute_1_pseudo_instruction ticks_of … s) 793 734 ].
Note: See TracChangeset
for help on using the changeset viewer.