Changeset 866 for src

Timestamp:

May 31, 2011, 3:03:28 PM (10 years ago)

Author:

sacerdot

Message:

Significant improvement in the proof.

File:

• src/ASM/AssemblyProof.ma (modified) (8 diffs)

src/ASM/AssemblyProof.ma

@@ -214 +214 @@
 qed.
 
+(*
 lemma subvector_hd_tl:
   ∀A: Type[0].
@@ -225 +226 @@
 axiom eq_a_reflexive:
   ∀a. eq_a a a = true.
-  
-(*
+
 let rec list_addressing_mode_tags_elim
   (n: nat) (l: Vector addressing_mode_tag (S n)) on l: (l → bool) → bool ≝
@@ -320 +320 @@
        ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (\snd instr_list).
        
-definition tech_pc_sigma0: pseudo_assembly_program → option nat ≝
+definition tech_pc_sigma0: pseudo_assembly_program → option (nat × (BitVectorTrie Word 16)) ≝
  λinstr_list.
   match sigma0 instr_list with
@@ -326 +326 @@
    | Some result ⇒
       let 〈ppc,pc_sigma_map〉 ≝ result in
-      let 〈pc, sigma_map〉 ≝ pc_sigma_map in
-       Some … pc ].
+       Some … pc_sigma_map ].
 
 definition sigma_safe: pseudo_assembly_program → option (Word → Word) ≝       
@@ -412 +411 @@
 qed.
 
+axiom tech_pc_sigma0_append:
+ ∀preamble,instr_list,prefix,label,i,pc',code,pc,costs,costs'.
+  Some … 〈pc,costs〉 = tech_pc_sigma0 〈preamble,prefix〉 →
+   construct_costs 〈preamble,instr_list〉 … pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →
+    tech_pc_sigma0 〈preamble,prefix@[〈label,i〉]〉 = Some … 〈pc',costs'〉.
+
+axiom tech_pc_sigma0_append_None:
+ ∀preamble,instr_list,prefix,i,pc,costs.
+  Some … 〈pc,costs〉 = tech_pc_sigma0 〈preamble,prefix〉 →
+   construct_costs 〈preamble,instr_list〉 … pc (λx.zero 16) (λx. zero 16) costs i = None …
+    → False.
+
 definition build_maps' ≝
   λpseudo_program.
@@ -421 +432 @@
       let pre' ≝ 〈preamble,pre〉 in
       let 〈labels,pc_costs〉 ≝ res in
-      let 〈program_counter,costs〉 ≝ pc_costs in
-       tech_pc_sigma0 pre' = Some … program_counter ∧
+       tech_pc_sigma0 pre' = Some … pc_costs ∧
        ∀id. occurs_exactly_once id pre →
         lookup ?? id labels (zero …) = sigma pre' (address_of_word_labels_code_mem pre id))
@@ -438 +448 @@
          ]
        in
-         match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
+         match construct_costs 〈preamble,instr_list〉 program_counter (λx. zero ?) (λx. zero ?) costs i' with
          [ None ⇒
             let dummy ≝ 〈labels,pc_costs〉 in
@@ -449 +459 @@
    let 〈pc, costs〉 ≝ pc_costs in
     〈labels, costs〉.
- [ whd cases construct in p3 #PC #CODE #JMEQ whd %
-    [ 
-    | #id #Hid
-      generalize in match (sig2 … t) whd in ⊢ (% → ?)
-      >p whd in ⊢ (% → ?) >p1 whd in ⊢ (% → ?) * #IH0 #IH1
-      whd in ⊢ (??(????%?)?) -labels1;
-      cases label in Hid
-       [ #Hid whd in ⊢ (??(????%?)?) >IH1 -IH1
-          [ >(address_of_word_labels_code_mem_None … Hid)
-            (* MANCA LEMMA: INDIRIZZO TROVATO NEL PROGRAMMA! *)
-          | whd in Hid >occurs_exactly_once_None in Hid // ]
-       | -label #label #Hid whd in ⊢ (??(????%?)?)
-      
-       ]]
- | (* dummy case *)
- | whd % // #pc normalize in ⊢ (% → ?) #abs @⊥ // ]
+ [3: whd % // #id normalize in ⊢ (% → ?) #abs @⊥ //
+ | whd cases construct in p3 #PC #CODE #JMEQ %
+    [ @(tech_pc_sigma0_append ??????????? (jmeq_to_eq ??? JMEQ)) | #id #Hid ]
+ | (* dummy case *) @⊥
+   @(tech_pc_sigma0_append_None ?? prefix ???? (jmeq_to_eq ??? p3)) ]
+ [*: generalize in match (sig2 … t) whd in ⊢ (% → ?)
+     >p whd in ⊢ (% → ?) >p1 * #IH0 #IH1 >IH0 // ]
+ whd in ⊢ (??(????%?)?) -labels1;
+ cases label in Hid
+  [ #Hid whd in ⊢ (??(????%?)?) >IH1 -IH1
+     [ >(address_of_word_labels_code_mem_None … Hid)
+       (* MANCA LEMMA: INDIRIZZO TROVATO NEL PROGRAMMA! *)
+     | whd in Hid >occurs_exactly_once_None in Hid // ]
+  | -label #label #Hid whd in ⊢ (??(????%?)?)
+   
+  ]
 qed.