Changeset 866
 Timestamp:
 May 31, 2011, 3:03:28 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r865 r866 214 214 qed. 215 215 216 (* 216 217 lemma subvector_hd_tl: 217 218 ∀A: Type[0]. … … 225 226 axiom eq_a_reflexive: 226 227 ∀a. eq_a a a = true. 227 228 (* 228 229 229 let rec list_addressing_mode_tags_elim 230 230 (n: nat) (l: Vector addressing_mode_tag (S n)) on l: (l → bool) → bool ≝ … … 320 320 ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (\snd instr_list). 321 321 322 definition tech_pc_sigma0: pseudo_assembly_program → option nat≝322 definition tech_pc_sigma0: pseudo_assembly_program → option (nat × (BitVectorTrie Word 16)) ≝ 323 323 λinstr_list. 324 324 match sigma0 instr_list with … … 326 326  Some result ⇒ 327 327 let 〈ppc,pc_sigma_map〉 ≝ result in 328 let 〈pc, sigma_map〉 ≝ pc_sigma_map in 329 Some … pc ]. 328 Some … pc_sigma_map ]. 330 329 331 330 definition sigma_safe: pseudo_assembly_program → option (Word → Word) ≝ … … 412 411 qed. 413 412 413 axiom tech_pc_sigma0_append: 414 ∀preamble,instr_list,prefix,label,i,pc',code,pc,costs,costs'. 415 Some … 〈pc,costs〉 = tech_pc_sigma0 〈preamble,prefix〉 → 416 construct_costs 〈preamble,instr_list〉 … pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 → 417 tech_pc_sigma0 〈preamble,prefix@[〈label,i〉]〉 = Some … 〈pc',costs'〉. 418 419 axiom tech_pc_sigma0_append_None: 420 ∀preamble,instr_list,prefix,i,pc,costs. 421 Some … 〈pc,costs〉 = tech_pc_sigma0 〈preamble,prefix〉 → 422 construct_costs 〈preamble,instr_list〉 … pc (λx.zero 16) (λx. zero 16) costs i = None … 423 → False. 424 414 425 definition build_maps' ≝ 415 426 λpseudo_program. … … 421 432 let pre' ≝ 〈preamble,pre〉 in 422 433 let 〈labels,pc_costs〉 ≝ res in 423 let 〈program_counter,costs〉 ≝ pc_costs in 424 tech_pc_sigma0 pre' = Some … program_counter ∧ 434 tech_pc_sigma0 pre' = Some … pc_costs ∧ 425 435 ∀id. occurs_exactly_once id pre → 426 436 lookup ?? id labels (zero …) = sigma pre' (address_of_word_labels_code_mem pre id)) … … 438 448 ] 439 449 in 440 match construct_costs pseudo_programprogram_counter (λx. zero ?) (λx. zero ?) costs i' with450 match construct_costs 〈preamble,instr_list〉 program_counter (λx. zero ?) (λx. zero ?) costs i' with 441 451 [ None ⇒ 442 452 let dummy ≝ 〈labels,pc_costs〉 in … … 449 459 let 〈pc, costs〉 ≝ pc_costs in 450 460 〈labels, costs〉. 451 [ whd cases construct in p3 #PC #CODE #JMEQ whd %452 [453  #id #Hid454 generalize in match (sig2 … t) whd in ⊢ (% → ?)455 >p whd in ⊢ (% → ?) >p1 whd in ⊢ (% → ?) * #IH0 #IH1456 whd in ⊢ (??(????%?)?) labels1;457 cases label in Hid458 [ #Hid whd in ⊢ (??(????%?)?) >IH1 IH1459 [ >(address_of_word_labels_code_mem_None … Hid)460 (* MANCA LEMMA: INDIRIZZO TROVATO NEL PROGRAMMA! *)461  whd in Hid >occurs_exactly_once_None in Hid // ]462  label #label #Hid whd in ⊢ (??(????%?)?)463 464 ]]465  (* dummy case *)466  whd % // #pc normalize in ⊢ (% → ?) #abs @⊥ //]461 [3: whd % // #id normalize in ⊢ (% → ?) #abs @⊥ // 462  whd cases construct in p3 #PC #CODE #JMEQ % 463 [ @(tech_pc_sigma0_append ??????????? (jmeq_to_eq ??? JMEQ))  #id #Hid ] 464  (* dummy case *) @⊥ 465 @(tech_pc_sigma0_append_None ?? prefix ???? (jmeq_to_eq ??? p3)) ] 466 [*: generalize in match (sig2 … t) whd in ⊢ (% → ?) 467 >p whd in ⊢ (% → ?) >p1 * #IH0 #IH1 >IH0 // ] 468 whd in ⊢ (??(????%?)?) labels1; 469 cases label in Hid 470 [ #Hid whd in ⊢ (??(????%?)?) >IH1 IH1 471 [ >(address_of_word_labels_code_mem_None … Hid) 472 (* MANCA LEMMA: INDIRIZZO TROVATO NEL PROGRAMMA! *) 473  whd in Hid >occurs_exactly_once_None in Hid // ] 474  label #label #Hid whd in ⊢ (??(????%?)?) 475 476 ] 467 477 qed. 468 478
Note: See TracChangeset
for help on using the changeset viewer.