Changeset 866


Ignore:
Timestamp:
May 31, 2011, 3:03:28 PM (8 years ago)
Author:
sacerdot
Message:

Significant improvement in the proof.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r865 r866  
    214214qed.
    215215
     216(*
    216217lemma subvector_hd_tl:
    217218  ∀A: Type[0].
     
    225226axiom eq_a_reflexive:
    226227  ∀a. eq_a a a = true.
    227  
    228 (*
     228
    229229let rec list_addressing_mode_tags_elim
    230230  (n: nat) (l: Vector addressing_mode_tag (S n)) on l: (l → bool) → bool ≝
     
    320320       ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (\snd instr_list).
    321321       
    322 definition tech_pc_sigma0: pseudo_assembly_program → option nat
     322definition tech_pc_sigma0: pseudo_assembly_program → option (nat × (BitVectorTrie Word 16))
    323323 λinstr_list.
    324324  match sigma0 instr_list with
     
    326326   | Some result ⇒
    327327      let 〈ppc,pc_sigma_map〉 ≝ result in
    328       let 〈pc, sigma_map〉 ≝ pc_sigma_map in
    329        Some … pc ].
     328       Some … pc_sigma_map ].
    330329
    331330definition sigma_safe: pseudo_assembly_program → option (Word → Word) ≝       
     
    412411qed.
    413412
     413axiom 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
     419axiom 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
    414425definition build_maps' ≝
    415426  λpseudo_program.
     
    421432      let pre' ≝ 〈preamble,pre〉 in
    422433      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 ∧
    425435       ∀id. occurs_exactly_once id pre →
    426436        lookup ?? id labels (zero …) = sigma pre' (address_of_word_labels_code_mem pre id))
     
    438448         ]
    439449       in
    440          match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
     450         match construct_costs 〈preamble,instr_list〉 program_counter (λx. zero ?) (λx. zero ?) costs i' with
    441451         [ None ⇒
    442452            let dummy ≝ 〈labels,pc_costs〉 in
     
    449459   let 〈pc, costs〉 ≝ pc_costs in
    450460    〈labels, costs〉.
    451  [ whd cases construct in p3 #PC #CODE #JMEQ whd %
    452     [
    453     | #id #Hid
    454       generalize in match (sig2 … t) whd in ⊢ (% → ?)
    455       >p whd in ⊢ (% → ?) >p1 whd in ⊢ (% → ?) * #IH0 #IH1
    456       whd in ⊢ (??(????%?)?) -labels1;
    457       cases label in Hid
    458        [ #Hid whd in ⊢ (??(????%?)?) >IH1 -IH1
    459           [ >(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  ]
    467477qed.
    468478
Note: See TracChangeset for help on using the changeset viewer.