Changeset 971 for src

Timestamp:

Jun 16, 2011, 12:07:20 AM (10 years ago)

Author:

sacerdot

Message:

...

File:

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

src/ASM/AssemblyProof.ma

@@ -924 +924 @@
    program counters. It is at the heart of the proof. *)
 (*CSC: code taken from build_maps *)
-definition sigma0: pseudo_assembly_program → option (nat × (nat × (BitVectorTrie Word 16))) ≝
- λinstr_list.
+definition sigma00: pseudo_assembly_program → list ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
+ λinstr_list.λl:list labelled_instruction.
   foldl ??
-    (λt. λi.
+   (λt,i.
        match t with
        [ None ⇒ None ?
@@ -939 +939 @@
               let 〈pc,ignore〉 ≝ pc_ignore in
               Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ]
-       ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (\snd instr_list).
-       
-definition tech_pc_sigma0: pseudo_assembly_program → option (nat × (BitVectorTrie Word 16)) ≝
- λinstr_list.
-  match sigma0 instr_list with
+       ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) l.
+
+definition sigma0: pseudo_assembly_program → option (nat × (nat × (BitVectorTrie Word 16)))
+ ≝ λprog.sigma00 prog (\snd prog).
+
+definition tech_pc_sigma00: pseudo_assembly_program → list labelled_instruction → option (nat × nat) ≝
+ λprogram,instr_list.
+  match sigma00 program instr_list with
    [ None ⇒ None …
    | Some result ⇒
       let 〈ppc,pc_sigma_map〉 ≝ result in
-       Some … pc_sigma_map ].
+      let 〈pc,map〉 ≝ pc_sigma_map in
+       Some … 〈ppc,pc〉 ].
 
 definition sigma_safe: pseudo_assembly_program → option (Word → Word) ≝       
@@ -992 +996 @@
 qed.
 
+lemma does_not_occur_Some:
+ ∀id,id',i,list_instr.
+  eq_bv ? id' id = false →
+   does_not_occur id (list_instr@[〈Some ? id',i〉]) =
+    does_not_occur id list_instr.
+ #id #id' #i #list_instr elim list_instr
+  [ #H normalize in H ⊢ %; >H %
+  | * #x #i' #tl #IH #H whd in ⊢ (??%%) >(IH H) %]
+qed.
+
 let rec occurs_exactly_once (id:Identifier) (l:list labelled_instruction) on l : bool ≝
  match l with
@@ -1030 +1044 @@
 qed.
 
-axiom tech_pc_sigma0_append:
- ∀preamble,instr_list,prefix,label,i,pc',code,ppc,pc,costs,costs'.
-  Some … 〈pc,costs〉 = tech_pc_sigma0 〈preamble,prefix〉 →
-   construct_costs 〈preamble,instr_list〉 … ppc 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,ppc,pc,costs.
-  Some … 〈pc,costs〉 = tech_pc_sigma0 〈preamble,prefix〉 →
-   construct_costs 〈preamble,instr_list〉 … ppc pc (λx.zero 16) (λx. zero 16) costs i = None …
+lemma occurs_exactly_once_Some:
+ ∀id,id',i,prefix.
+  occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → eq_bv ? id' id ∨ occurs_exactly_once id prefix.
+ #id #id' #i #prefix elim prefix
+  [ whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
+    change with (? → eq_v ?? eq_b id' id ∨ ?) cases (eq_v ?????) normalize nodelta; /2/
+  | *; #he #i' #tl #IH whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
+    cases he; normalize nodelta
+     [ #H @ (IH H)
+     | #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??)
+       change in match (eq_v ???x id) with (eq_bv ? x id) cases (eq_bv 16 x id) normalize nodelta;
+       [ #H  | #H @IH @H]
+qed.
+
+axiom tech_pc_sigma00_append_Some:
+ ∀program,prefix,costs,label,i,pc',code,ppc,pc.
+  tech_pc_sigma00 program prefix = Some … 〈ppc,pc〉 →
+   construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →
+    tech_pc_sigma00 program (prefix@[〈label,i〉]) = Some … 〈S ppc,pc'〉.
+
+axiom tech_pc_sigma00_append_None:
+ ∀program,prefix,i,ppc,pc,costs.
+  tech_pc_sigma00 program prefix = Some … 〈ppc,pc〉 →
+   construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = None …
     → False.
 
-(*
 definition build_maps' ≝
   λpseudo_program.
-  let 〈preamble,instr_list〉 ≝ pseudo_program in
   let result ≝
    foldl_strong
     (option Identifier × pseudo_instruction)
-    (λpre. Σres:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
-      let pre' ≝ 〈preamble,pre〉 in
-      let 〈labels,pc_costs〉 ≝ res in
-       tech_pc_sigma0 pre' = Some … pc_costs ∧
+    (λpre. Σres:((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie Word 16)))).
+      let 〈labels,ppc_pc_costs〉 ≝ res in
+      let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
+      let 〈pc',costs〉 ≝ pc_costs in
+       tech_pc_sigma00 pseudo_program pre = Some ? 〈ppc',pc'〉 ∧
        ∀id. occurs_exactly_once id pre →
-        lookup ?? id labels (zero …) = sigma pre' (address_of_word_labels_code_mem pre id))
-    instr_list
+        lookup ?? id labels (zero …) = sigma pseudo_program (address_of_word_labels_code_mem pre id))
+    (\snd pseudo_program)
     (λprefix,i,tl,prf,t.
-      let 〈labels, pc_costs〉 ≝ t in
-      let 〈program_counter, costs〉 ≝ pc_costs in
+      let 〈labels, ppc_pc_costs〉 ≝ t in
+      let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in
+      let 〈pc,costs〉 ≝ pc_costs in
        let 〈label, i'〉 ≝ i in
        let labels ≝
@@ -1064 +1092 @@
          [ None ⇒ labels
          | Some label ⇒
-           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
+           let program_counter_bv ≝ bitvector_of_nat ? pc in
              insert ? ? label program_counter_bv labels
          ]
        in
-         match construct_costs 〈preamble,instr_list〉 program_counter (λx. zero ?) (λx. zero ?) costs i' with
+         match construct_costs pseudo_program ppc pc (λx. zero ?) (λx. zero ?) costs i' with
          [ None ⇒
-            let dummy ≝ 〈labels,pc_costs〉 in
+            let dummy ≝ 〈labels,ppc_pc_costs〉 in
              dummy
-         | Some construct ⇒ 〈labels, construct〉
+         | Some construct ⇒ 〈labels, 〈S ppc,construct〉〉
          ]
-    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉
+    ) 〈(Stub ? ?), 〈0, 〈0, Stub ? ?〉〉〉
   in
-   let 〈labels, pc_costs〉 ≝ result in
+   let 〈labels, ppc_pc_costs〉 ≝ result in
+   let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in
    let 〈pc, costs〉 ≝ pc_costs in
     〈labels, costs〉.
  [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 ⊢ (??(????%?)?)
-   
-  ]
+ | whd generalize in match (sig2 … t) >p >p1 >p2 >p3 *; #IH1 #IH2
+   cases construct in p4 #PC #CODE #JMEQ %
+   [ @(tech_pc_sigma00_append_Some … IH1 (jmeq_to_eq … JMEQ))
+   | #id normalize nodelta; -labels1; cases label; normalize nodelta
+     [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 //
+     | #l
+     ]]
+ | (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 *; #IH1 #IH2 
+   @(tech_pc_sigma00_append_None … IH1 (jmeq_to_eq ??? p4)) ]
 qed.