Changeset 1971 for src/ASM/AssemblyProofSplit.ma
 Timestamp:
 May 20, 2012, 10:34:31 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplit.ma
r1969 r1971 88 88 #P #A #a #abs destruct 89 89 qed. 90 91 (* 92 lemma pi1_let_commute: 93 ∀A,B,C,P. ∀c:A × B. ∀t: Σc:C.P c. 94 pi1 … (let 〈x1,y1〉 ≝ c in t) = (let 〈x1,y1〉 ≝ c in pi1 … t). 95 #A #B #C #P * #a #b * // 96 qed. 97 98 lemma pi1_let_as_commute: 99 ∀A,B,C,P. ∀c:A × B. ∀t: Σc:C.P c. 100 pi1 … (let 〈x1,y1〉 as H ≝ c in t) = 101 (let 〈x1,y1〉 as H ≝ c in pi1 … t). 102 #A #B #C #P * #a #b * // 103 qed. 104 *) 105 106 lemma tech_pi1_let_as_commute: 107 ∀A,B,C,P. ∀f. ∀c,c':A × B. 108 ∀t: ∀a,b. 〈a,b〉=c → Σc:C.P c. 109 ∀t': ∀a,b. 〈a,b〉=c' → Σc:C.P c. 110 c=c' → (∀x,y,H,H'.t x y H = f (pi1 … (t' x y H'))) → 111 pi1 … (let 〈x1,y1〉 as H ≝ c in t x1 y1 H) = 112 f (pi1 … (let 〈x1,y1〉 as H ≝ c' in t' x1 y1 H)). 113 #A #B #C #P #f * #a #b * #a' #b' #t #t' #EQ1 destruct normalize /2/ 114 qed. 115 116 include alias "arithmetics/nat.ma". 117 include alias "basics/logic.ma". 118 include alias "ASM/BitVectorTrie.ma". 119 120 lemma pair_replace: 121 ∀A,B,T:Type[0].∀P:T → Prop. ∀t. ∀a,b.∀c,c': A × B. c=c' → c ≃ 〈a,b〉 → 122 P (t a b) → P (let 〈a',b'〉 ≝ c' in t a' b'). 123 #A #B #T #P #t #a #b * #x #y * #x' #y' #H1 #H2 destruct // 124 qed. 125 126 lemma main_lemma_preinstruction: 127 ∀M,M': internal_pseudo_address_map. 128 ∀preamble : preamble. ∀instr_list : list labelled_instruction. 129 ∀cm: pseudo_assembly_program. 130 ∀EQcm: cm = 〈preamble,instr_list〉. 131 ∀sigma : Word→Word. ∀policy : Word→bool. 132 ∀sigma_policy_witness : sigma_policy_specification cm sigma policy. 133 ∀ps : PseudoStatus cm. 134 ∀ppc : Word. 135 ∀EQppc : ppc=program_counter pseudo_assembly_program cm ps. 136 ∀labels : label_map. 137 ∀costs : BitVectorTrie costlabel 16. 138 ∀create_label_cost_refl : create_label_cost_map instr_list=〈labels,costs〉. 139 ∀assembled : list Byte. 140 ∀costs' : BitVectorTrie costlabel 16. 141 ∀assembly_refl : assembly 〈preamble,instr_list〉 sigma policy=〈assembled,costs'〉. 142 ∀EQassembled : assembled=\fst (assembly cm sigma policy). 143 ∀newppc : Word. 144 ∀lookup_labels : Identifier→Word. 145 ∀EQlookup_labels : lookup_labels = (λx:Identifier.sigma (address_of_word_labels_code_mem instr_list x)). 146 ∀lookup_datalabels : identifier ASMTag→Word. 147 ∀ EQlookup_datalabels : lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)). 148 ∀EQnewppc : newppc=add 16 ppc (bitvector_of_nat 16 1). 149 ∀instr: preinstruction Identifier. 150 ∀ticks. 151 ∀EQticks: ticks = ticks_of0 〈preamble,instr_list〉 sigma policy ppc (Instruction instr). 152 ∀addr_of. 153 ∀EQaddr_of: addr_of = (λx:Identifier 154 .λy:PreStatus pseudo_assembly_program cm 155 .address_of_word_labels cm x). 156 ∀s. 157 ∀EQs: s = (set_program_counter pseudo_assembly_program cm ps 158 (add 16 ppc (bitvector_of_nat 16 1))). 159 ∀P. 160 ∀EQP: 161 P = (λs. ∃n:ℕ 162 .execute n 163 (code_memory_of_pseudo_assembly_program cm sigma 164 policy) 165 (status_of_pseudo_status M cm ps sigma policy) 166 =status_of_pseudo_status M' cm s sigma policy). 167 sigma (add 16 ppc (bitvector_of_nat 16 1)) 168 =add 16 (sigma ppc) 169 (bitvector_of_nat 16 170 (\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc 171 lookup_datalabels (Instruction instr)))) 172 →next_internal_pseudo_address_map0 pseudo_assembly_program (Instruction instr) 173 M cm ps 174 =Some internal_pseudo_address_map M' 175 →fetch_many (load_code_memory assembled) 176 (sigma (add 16 ppc (bitvector_of_nat 16 1))) (sigma ppc) 177 (expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels 178 (Instruction instr)) 179 →P (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm 180 addr_of instr s). 181 #M #M' #preamble #instr_list #cm #EQcm #sigma #policy #sigma_policy_witness #ps #ppc #EQppc #labels 182 #costs #create_label_cost_refl #assembled #costs' #assembly_refl #EQassembled #newppc 183 #lookup_labels #EQlookup_labels #lookup_datalabels #EQlookup_datalabels #EQnewppc #instr 184 #ticks #EQticks #addr_of #EQaddr_of #s #EQs #P #EQP 185 #sigma_increment_commutation #maps_assm #fetch_many_assm 186 letin a ≝ Identifier letin m ≝ pseudo_assembly_program 187 cut (Σxxx:PseudoStatus cm. P (execute_1_preinstruction ticks a m cm addr_of instr s)) 188 [2: * // ] 189 @( 190 let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in 191 let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in 192 match instr in preinstruction return λx. x = instr → Σs'.? with 193 [ ADD addr1 addr2 ⇒ λinstr_refl. 194 let s ≝ add_ticks1 s in 195 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1) 196 (get_arg_8 … s false addr2) false in 197 let cy_flag ≝ get_index' ? O ? flags in 198 let ac_flag ≝ get_index' ? 1 ? flags in 199 let ov_flag ≝ get_index' ? 2 ? flags in 200 let s ≝ set_arg_8 … s ACC_A result in 201 set_flags … s cy_flag (Some Bit ac_flag) ov_flag 202  ADDC addr1 addr2 ⇒ λinstr_refl. 203 let s ≝ add_ticks1 s in 204 let old_cy_flag ≝ get_cy_flag ?? s in 205 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1) 206 (get_arg_8 … s false addr2) old_cy_flag in 207 let cy_flag ≝ get_index' ? O ? flags in 208 let ac_flag ≝ get_index' ? 1 ? flags in 209 let ov_flag ≝ get_index' ? 2 ? flags in 210 let s ≝ set_arg_8 … s ACC_A result in 211 set_flags … s cy_flag (Some Bit ac_flag) ov_flag 212  SUBB addr1 addr2 ⇒ λinstr_refl. 213 let s ≝ add_ticks1 s in 214 let old_cy_flag ≝ get_cy_flag ?? s in 215 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1) 216 (get_arg_8 … s false addr2) old_cy_flag in 217 let cy_flag ≝ get_index' ? O ? flags in 218 let ac_flag ≝ get_index' ? 1 ? flags in 219 let ov_flag ≝ get_index' ? 2 ? flags in 220 let s ≝ set_arg_8 … s ACC_A result in 221 set_flags … s cy_flag (Some Bit ac_flag) ov_flag 222  ANL addr ⇒ λinstr_refl. 223 let s ≝ add_ticks1 s in 224 match addr with 225 [ inl l ⇒ 226 match l with 227 [ inl l' ⇒ 228 let 〈addr1, addr2〉 ≝ l' in 229 let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 230 set_arg_8 … s addr1 and_val 231  inr r ⇒ 232 let 〈addr1, addr2〉 ≝ r in 233 let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 234 set_arg_8 … s addr1 and_val 235 ] 236  inr r ⇒ 237 let 〈addr1, addr2〉 ≝ r in 238 let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in 239 set_flags … s and_val (None ?) (get_ov_flag ?? s) 240 ] 241  ORL addr ⇒ λinstr_refl. 242 let s ≝ add_ticks1 s in 243 match addr with 244 [ inl l ⇒ 245 match l with 246 [ inl l' ⇒ 247 let 〈addr1, addr2〉 ≝ l' in 248 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 249 set_arg_8 … s addr1 or_val 250  inr r ⇒ 251 let 〈addr1, addr2〉 ≝ r in 252 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 253 set_arg_8 … s addr1 or_val 254 ] 255  inr r ⇒ 256 let 〈addr1, addr2〉 ≝ r in 257 let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in 258 set_flags … s or_val (None ?) (get_ov_flag … s) 259 ] 260  XRL addr ⇒ λinstr_refl. 261 let s ≝ add_ticks1 s in 262 match addr with 263 [ inl l' ⇒ 264 let 〈addr1, addr2〉 ≝ l' in 265 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 266 set_arg_8 … s addr1 xor_val 267  inr r ⇒ 268 let 〈addr1, addr2〉 ≝ r in 269 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 270 set_arg_8 … s addr1 xor_val 271 ] 272  INC addr ⇒ λinstr_refl. 273 match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → Σs': PreStatus m cm. ? with 274 [ ACC_A ⇒ λacc_a: True. 275 let s' ≝ add_ticks1 s in 276 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in 277 set_arg_8 … s' ACC_A result 278  REGISTER r ⇒ λregister: True. 279 let s' ≝ add_ticks1 s in 280 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in 281 set_arg_8 … s' (REGISTER r) result 282  DIRECT d ⇒ λdirect: True. 283 let s' ≝ add_ticks1 s in 284 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in 285 set_arg_8 … s' (DIRECT d) result 286  INDIRECT i ⇒ λindirect: True. 287 let s' ≝ add_ticks1 s in 288 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in 289 set_arg_8 … s' (INDIRECT i) result 290  DPTR ⇒ λdptr: True. 291 let s' ≝ add_ticks1 s in 292 let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in 293 let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in 294 let s ≝ set_8051_sfr … s' SFR_DPL bl in 295 set_8051_sfr … s' SFR_DPH bu 296  _ ⇒ λother: False. ⊥ 297 ] (subaddressing_modein … addr) 298  NOP ⇒ λinstr_refl. 299 let s ≝ add_ticks2 s in 300 s 301  DEC addr ⇒ λinstr_refl. 302 let s ≝ add_ticks1 s in 303 let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in 304 set_arg_8 … s addr result 305  MUL addr1 addr2 ⇒ λinstr_refl. 306 let s ≝ add_ticks1 s in 307 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in 308 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in 309 let product ≝ acc_a_nat * acc_b_nat in 310 let ov_flag ≝ product ≥ 256 in 311 let low ≝ bitvector_of_nat 8 (product mod 256) in 312 let high ≝ bitvector_of_nat 8 (product ÷ 256) in 313 let s ≝ set_8051_sfr … s SFR_ACC_A low in 314 set_8051_sfr … s SFR_ACC_B high 315  DIV addr1 addr2 ⇒ λinstr_refl. 316 let s ≝ add_ticks1 s in 317 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in 318 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in 319 match acc_b_nat with 320 [ O ⇒ set_flags … s false (None Bit) true 321  S o ⇒ 322 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in 323 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in 324 let s ≝ set_8051_sfr … s SFR_ACC_A q in 325 let s ≝ set_8051_sfr … s SFR_ACC_B r in 326 set_flags … s false (None Bit) false 327 ] 328  DA addr ⇒ λinstr_refl. 329 let s ≝ add_ticks1 s in 330 let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr … s SFR_ACC_A) in 331 if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then 332 let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in 333 let cy_flag ≝ get_index' ? O ? flags in 334 let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in 335 if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then 336 let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in 337 let new_acc ≝ nu @@ acc_nl' in 338 let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in 339 set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s) 340 else 341 s 342 else 343 s 344  CLR addr ⇒ λinstr_refl. 345 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. ? with 346 [ ACC_A ⇒ λacc_a: True. 347 let s ≝ add_ticks1 s in 348 set_arg_8 … s ACC_A (zero 8) 349  CARRY ⇒ λcarry: True. 350 let s ≝ add_ticks1 s in 351 set_arg_1 … s CARRY false 352  BIT_ADDR b ⇒ λbit_addr: True. 353 let s ≝ add_ticks1 s in 354 set_arg_1 … s (BIT_ADDR b) false 355  _ ⇒ λother: False. ⊥ 356 ] (subaddressing_modein … addr) 357  CPL addr ⇒ λinstr_refl. 358 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. ? with 359 [ ACC_A ⇒ λacc_a: True. 360 let s ≝ add_ticks1 s in 361 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 362 let new_acc ≝ negation_bv ? old_acc in 363 set_8051_sfr … s SFR_ACC_A new_acc 364  CARRY ⇒ λcarry: True. 365 let s ≝ add_ticks1 s in 366 let old_cy_flag ≝ get_arg_1 … s CARRY true in 367 let new_cy_flag ≝ ¬old_cy_flag in 368 set_arg_1 … s CARRY new_cy_flag 369  BIT_ADDR b ⇒ λbit_addr: True. 370 let s ≝ add_ticks1 s in 371 let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in 372 let new_bit ≝ ¬old_bit in 373 set_arg_1 … s (BIT_ADDR b) new_bit 374  _ ⇒ λother: False. ? 375 ] (subaddressing_modein … addr) 376  SETB b ⇒ λinstr_refl. 377 let s ≝ add_ticks1 s in 378 set_arg_1 … s b false 379  RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *) 380 let s ≝ add_ticks1 s in 381 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 382 let new_acc ≝ rotate_left … 1 old_acc in 383 set_8051_sfr … s SFR_ACC_A new_acc 384  RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *) 385 let s ≝ add_ticks1 s in 386 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 387 let new_acc ≝ rotate_right … 1 old_acc in 388 set_8051_sfr … s SFR_ACC_A new_acc 389  RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *) 390 let s ≝ add_ticks1 s in 391 let old_cy_flag ≝ get_cy_flag ?? s in 392 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 393 let new_cy_flag ≝ get_index' ? O ? old_acc in 394 let new_acc ≝ shift_left … 1 old_acc old_cy_flag in 395 let s ≝ set_arg_1 … s CARRY new_cy_flag in 396 set_8051_sfr … s SFR_ACC_A new_acc 397  RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *) 398 let s ≝ add_ticks1 s in 399 let old_cy_flag ≝ get_cy_flag ?? s in 400 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 401 let new_cy_flag ≝ get_index' ? 7 ? old_acc in 402 let new_acc ≝ shift_right … 1 old_acc old_cy_flag in 403 let s ≝ set_arg_1 … s CARRY new_cy_flag in 404 set_8051_sfr … s SFR_ACC_A new_acc 405  SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *) 406 let s ≝ add_ticks1 s in 407 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 408 let 〈nu,nl〉 ≝ split ? 4 4 old_acc in 409 let new_acc ≝ nl @@ nu in 410 set_8051_sfr … s SFR_ACC_A new_acc 411  PUSH addr ⇒ λinstr_refl. 412 match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m cm. ? with 413 [ DIRECT d ⇒ λdirect: True. 414 let s ≝ add_ticks1 s in 415 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 416 let s ≝ set_8051_sfr … s SFR_SP new_sp in 417 write_at_stack_pointer … s d 418  _ ⇒ λother: False. ⊥ 419 ] (subaddressing_modein … addr) 420  POP addr ⇒ λinstr_refl. 421 let s ≝ add_ticks1 s in 422 let contents ≝ read_at_stack_pointer ?? s in 423 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 424 let s ≝ set_8051_sfr … s SFR_SP new_sp in 425 set_arg_8 … s addr contents 426  XCH addr1 addr2 ⇒ λinstr_refl. 427 let s ≝ add_ticks1 s in 428 let old_addr ≝ get_arg_8 … s false addr2 in 429 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 430 let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in 431 set_arg_8 … s addr2 old_acc 432  XCHD addr1 addr2 ⇒ λinstr_refl. 433 let s ≝ add_ticks1 s in 434 let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr … s SFR_ACC_A) in 435 let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 … s false addr2) in 436 let new_acc ≝ acc_nu @@ arg_nl in 437 let new_arg ≝ arg_nu @@ acc_nl in 438 let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in 439 set_arg_8 … s addr2 new_arg 440  RET ⇒ λinstr_refl. 441 let s ≝ add_ticks1 s in 442 let high_bits ≝ read_at_stack_pointer ?? s in 443 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 444 let s ≝ set_8051_sfr … s SFR_SP new_sp in 445 let low_bits ≝ read_at_stack_pointer ?? s in 446 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 447 let s ≝ set_8051_sfr … s SFR_SP new_sp in 448 let new_pc ≝ high_bits @@ low_bits in 449 set_program_counter … s new_pc 450  RETI ⇒ λinstr_refl. 451 let s ≝ add_ticks1 s in 452 let high_bits ≝ read_at_stack_pointer ?? s in 453 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 454 let s ≝ set_8051_sfr … s SFR_SP new_sp in 455 let low_bits ≝ read_at_stack_pointer ?? s in 456 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 457 let s ≝ set_8051_sfr … s SFR_SP new_sp in 458 let new_pc ≝ high_bits @@ low_bits in 459 set_program_counter … s new_pc 460  MOVX addr ⇒ λinstr_refl. 461 let s ≝ add_ticks1 s in 462 (* DPM: only copies  doesn't affect I/O *) 463 match addr with 464 [ inl l ⇒ 465 let 〈addr1, addr2〉 ≝ l in 466 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 467  inr r ⇒ 468 let 〈addr1, addr2〉 ≝ r in 469 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 470 ] 471  MOV addr ⇒ λinstr_refl. 472 let s ≝ add_ticks1 s in 473 match addr with 474 [ inl l ⇒ 475 match l with 476 [ inl l' ⇒ 477 match l' with 478 [ inl l'' ⇒ 479 match l'' with 480 [ inl l''' ⇒ 481 match l''' with 482 [ inl l'''' ⇒ 483 let 〈addr1, addr2〉 ≝ l'''' in 484 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 485  inr r'''' ⇒ 486 let 〈addr1, addr2〉 ≝ r'''' in 487 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 488 ] 489  inr r''' ⇒ 490 let 〈addr1, addr2〉 ≝ r''' in 491 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 492 ] 493  inr r'' ⇒ 494 let 〈addr1, addr2〉 ≝ r'' in 495 set_arg_16 … s (get_arg_16 … s addr2) addr1 496 ] 497  inr r ⇒ 498 let 〈addr1, addr2〉 ≝ r in 499 set_arg_1 … s addr1 (get_arg_1 … s addr2 false) 500 ] 501  inr r ⇒ 502 let 〈addr1, addr2〉 ≝ r in 503 set_arg_1 … s addr1 (get_arg_1 … s addr2 false) 504 ] 505  JC addr ⇒ λinstr_refl. 506 if get_cy_flag ?? s then 507 let s ≝ add_ticks1 s in 508 set_program_counter … s (addr_of addr s) 509 else 510 let s ≝ add_ticks2 s in 511 s 512  JNC addr ⇒ λinstr_refl. 513 if ¬(get_cy_flag ?? s) then 514 let s ≝ add_ticks1 s in 515 set_program_counter … s (addr_of addr s) 516 else 517 let s ≝ add_ticks2 s in 518 s 519  JB addr1 addr2 ⇒ λinstr_refl. 520 if get_arg_1 … s addr1 false then 521 let s ≝ add_ticks1 s in 522 set_program_counter … s (addr_of addr2 s) 523 else 524 let s ≝ add_ticks2 s in 525 s 526  JNB addr1 addr2 ⇒ λinstr_refl. 527 if ¬(get_arg_1 … s addr1 false) then 528 let s ≝ add_ticks1 s in 529 set_program_counter … s (addr_of addr2 s) 530 else 531 let s ≝ add_ticks2 s in 532 s 533  JBC addr1 addr2 ⇒ λinstr_refl. 534 let s ≝ set_arg_1 … s addr1 false in 535 if get_arg_1 … s addr1 false then 536 let s ≝ add_ticks1 s in 537 set_program_counter … s (addr_of addr2 s) 538 else 539 let s ≝ add_ticks2 s in 540 s 541  JZ addr ⇒ λinstr_refl. 542 if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then 543 let s ≝ add_ticks1 s in 544 set_program_counter … s (addr_of addr s) 545 else 546 let s ≝ add_ticks2 s in 547 s 548  JNZ addr ⇒ λinstr_refl. 549 if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then 550 let s ≝ add_ticks1 s in 551 set_program_counter … s (addr_of addr s) 552 else 553 let s ≝ add_ticks2 s in 554 s 555  CJNE addr1 addr2 ⇒ λinstr_refl. 556 match addr1 with 557 [ inl l ⇒ 558 let 〈addr1, addr2'〉 ≝ l in 559 let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1)) 560 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in 561 if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then 562 let s ≝ add_ticks1 s in 563 let s ≝ set_program_counter … s (addr_of addr2 s) in 564 set_flags … s new_cy (None ?) (get_ov_flag ?? s) 565 else 566 let s ≝ add_ticks2 s in 567 set_flags … s new_cy (None ?) (get_ov_flag ?? s) 568  inr r' ⇒ 569 let 〈addr1, addr2'〉 ≝ r' in 570 let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1)) 571 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in 572 if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then 573 let s ≝ add_ticks1 s in 574 let s ≝ set_program_counter … s (addr_of addr2 s) in 575 set_flags … s new_cy (None ?) (get_ov_flag ?? s) 576 else 577 let s ≝ add_ticks2 s in 578 set_flags … s new_cy (None ?) (get_ov_flag ?? s) 579 ] 580  DJNZ addr1 addr2 ⇒ λinstr_refl. 581 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in 582 let s ≝ set_arg_8 … s addr1 result in 583 if ¬(eq_bv ? result (zero 8)) then 584 let s ≝ add_ticks1 s in 585 set_program_counter … s (addr_of addr2 s) 586 else 587 let s ≝ add_ticks2 s in 588 s 589 ] (refl … instr)) 590 try (cases(other)) 591 try assumption (*20s*) 592 try (% @False) (*6s*) (* Bug exploited here to implement solve :*) 593 try ( 594 @(execute_1_technical … (subaddressing_modein …)) 595 @I 596 ) (*66s*) 597 whd in match execute_1_preinstruction; normalize nodelta 598 [1: (* ADD *) 599 >p normalize nodelta 600 >EQP %{1} 601 whd in ⊢ (??%?); 602 (* work on fetch_many *) 603 <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled 604 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 605 whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy)); 606 <EQppc 607 cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * * 608 #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm; 609 lapply (eq_bv_eq … fetch_many_assm) fetch_many_assm #EQnewpc 610 >(eq_instruction_to_eq … eq_instr) instr' whd in ⊢ (??%?); 611 @(pair_replace ?????????? p) 612 [2: normalize nodelta >EQs s >EQticks' ticks' 613 <instr_refl in EQticks; #EQticks >EQticks ticks 614 <instr_refl in sigma_increment_commutation; #sigma_increment_commutation 615 whd in ⊢ (??%%); 616 @split_eq_status 617 try % 618 [3: whd in ⊢ (??%%); >EQnewpc >sigma_increment_commutation % 619 2: whd in ⊢ (??%%); >set_clock_mk_Status_commutation 620 whd in match (set_flags ??????); 621 (* CSC: TO BE COMPLETED *) 622 ] 623  (*>get_arg_8_ok_set_clock*) (*CSC: to be done *) 624 ] 625 626 ] cases daemon 627 qed. 628 (* 629 630 631 @list_addressing_mode_tags_elim_prop try % whd 632 @list_addressing_mode_tags_elim_prop try % whd #arg 633 (* XXX: we first work on sigma_increment_commutation *) 634 #sigma_increment_commutation 635 normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation; 636 (* XXX: we work on the maps *) 637 whd in ⊢ (??%? → ?); 638 try (change with (if ? then ? else ? = ? → ?) 639 cases (addressing_mode_ok ????? ∧ addressing_mode_ok ?????) normalize nodelta) 640 #H try @(None_Some_elim ??? H) @(Some_Some_elim ????? H) #map_refl_assm <map_refl_assm 641 (* XXX: we assume the fetch_many hypothesis *) 642 #fetch_many_assm 643 (* XXX: we give the existential *) 644 %{1} 645 whd in match (execute_1_pseudo_instruction0 ?????); 646 (* XXX: work on the left hand side of the equality *) 647 whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc 648 (* XXX: execute fetches some more *) 649 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 650 whd in fetch_many_assm; 651 >EQassembled in fetch_many_assm; 652 cases (fetch ??) * #instr #newpc #ticks normalize nodelta * * 653 #eq_instr #EQticks whd in EQticks:(???%); >EQticks 654 #fetch_many_assm whd in fetch_many_assm; 655 lapply (eq_bv_eq … fetch_many_assm) fetch_many_assm #EQnewpc 656 >(eq_instruction_to_eq … eq_instr) instr 657 [ @(pose … (pi1 … (execute_1_preinstruction' …))) #lhs #EQlhs 658 @(pose … 659 (λlhs. status_of_pseudo_status M 〈preamble,instr_list〉 lhs sigma policy)) 660 #Pl #EQPl 661 cut (∀A,B:Type[0].∀f,f':A → B.∀x. f=f' → f x = f' x) [2: #eq_f_g_to_eq 662 lapply (λy.eq_f_g_to_eq ???? y EQPl) #XX <(XX lhs) XX >EQlhs lhs 663 whd in ⊢ (??%?); whd in ⊢ (??(???%)(?(???%))); 664 @pair_elim 665 >tech_pi1_let_as_commute 666 667 *) 668 90 669 91 670 theorem main_thm: … … 180 759 ] 181 760 ] 182 1: (* Instruction *) pi; * 761 1: (* Instruction *) pi; #instr 762 @(main_lemma_preinstruction M M' preamble instr_list … (refl …) … sigma_policy_witness 763 … EQppc … create_label_cost_refl … assembly_refl EQassembled … EQlookup_labels … 764 EQlookup_datalabels EQnewppc instr … (refl …) … (refl …) … (refl …) … (refl …)) 765 4,5: cases daemon 766 ] 767 qed. 768 (* 769 * 183 770 [1,2,3: (* ADD, ADDC, SUBB *) 184 771 @list_addressing_mode_tags_elim_prop try % whd … … 207 794 #fetch_many_assm whd in fetch_many_assm; 208 795 lapply (eq_bv_eq … fetch_many_assm) fetch_many_assm #EQnewpc 209 >(eq_instruction_to_eq … eq_instr) instr whd in ⊢ (??%?); 796 >(eq_instruction_to_eq … eq_instr) instr 797 [ @(pose … (pi1 … (execute_1_preinstruction' …))) #lhs #EQlhs 798 @(pose … 799 (λlhs. status_of_pseudo_status M 〈preamble,instr_list〉 lhs sigma policy)) 800 #Pl #EQPl 801 cut (∀A,B:Type[0].∀f,f':A → B.∀x. f=f' → f x = f' x) [2: #eq_f_g_to_eq 802 lapply (λy.eq_f_g_to_eq ???? y EQPl) #XX <(XX lhs) XX >EQlhs lhs 803 whd in ⊢ (??%?); whd in ⊢ (??(???%)(?(???%))); 804 @pair_elim 805 >tech_pi1_let_as_commute 806 807 808 whd in ⊢ (??%?); 210 809 [ @(pose … (execute_1_preinstruction' ???????)) 211 810 #lhs whd in ⊢ (???% → ?); #EQlhs 212 811 @(pose … (execute_1_preinstruction' ???????)) 213 812 #rhs whd in ⊢ (???% → ?); #EQrhs 214 813 814 215 815 CSC: delirium 216 816 … … 573 1173 cases daemon (* EASY CASES TO BE COMPLETED *) 574 1174 qed. 1175 *)
Note: See TracChangeset
for help on using the changeset viewer.