Changeset 3464

Timestamp:

Feb 21, 2014, 8:34:32 PM (6 years ago)

Author:

piccolo

Message:

static_dinamic in place

File:

• LTS/Vm.ma (modified) (10 diffs)

LTS/Vm.ma

@@ -32 +32 @@
 { instructions : list (AssemblerInstr p)
 ; endmain : ℕ
-; endmain_ok : endmain ≤ |instructions|
+; endmain_ok : endmain < |instructions|
 }.
 
@@ -510 +510 @@
 qed.
 
+(*
+lemma labels_pc_bounded : ∀p.∀prog : AssemblerProgram p.∀lbl,pc.∀m.
+mem ? 〈lbl,pc〉 (labels_pc p (instructions … prog) m) → 
+(m + pc) < (|(instructions … prog)|).
+#p * #instr #endmain #_  #H1 #H2 elim instr
+[ #H3 @⊥ /2/ ] #x #xs #IH #_ #lbl #pc #m whd in match (labels_pc ???); 
+#H cases(mem_append ???? H) -H
+[ whd in match labels_pc_of_instr; normalize nodelta
+  cases x normalize nodelta
+  [ #seq * [|#lab]
+  | #newpc
+  | #cond #newpc #ltrue #lfalse
+  | #lin #io #lout
+  | #f
+  |
+  ]
+  normalize [1,3,6,7: *] * [2,4,6: * [2,4:*] ]
+  #EQ destruct
+*)  
+
 unification hint  0 ≔ ; 
     X ≟ DEQInitCostLabel
@@ -592 +612 @@
 static_analisys p abs_t instr_m mT prog = return map → 
 mem … 〈lbl,pc〉 (labels_pc … (instructions … prog) O) → 
-get_map … map lbl = block_cost … prog abs_t instr_m pc (S (|(instructions … prog)|)).
+get_map … map lbl = 
+block_cost … prog abs_t instr_m pc (S (|(instructions … prog)|)) ∧
+block_cost … prog abs_t instr_m pc (S (|(instructions … prog)|)) ≠ None ?.
 #p #abs_t #instr_m #mT * #prog whd in match static_analisys; normalize nodelta
 whd in match asm_no_duplicates; normalize nodelta lapply (labels_pc ???)
@@ -600 +622 @@
 cases(bind_inversion ????? H) -H #elem * #EQelem whd in ⊢ (??%% → ?); #EQ
 destruct *
-[ #EQ destruct >get_set_hit >EQelem %
-| #H >get_set_miss [ @IH //] inversion (? == ?) [2: #_ %]
-  #ABS cases H1 -H1 #H1 @⊥ @H1 >(\P ABS) >mem_to_memb //
-  cases(map_mem … \fst … H) #z1 * #Hz1 #EQ destruct @Hz1
+[ #EQ destruct % [ >get_set_hit >EQelem % | >EQelem % whd in ⊢ (??%% → ?); #EQ destruct] 
+| #H % 
+  [ >get_set_miss [ @(proj1 … (IH …)) //] inversion (? == ?) [2: #_ %]
+    #ABS cases H1 -H1 #H1 @⊥ @H1 >(\P ABS) >mem_to_memb //
+    cases(map_mem … \fst … H) #z1 * #Hz1 #EQ destruct @Hz1
+  | @(proj2 … (IH …)) //
+  ]
 ]
 qed.
@@ -741 +766 @@
 qed.
 
-
-lemma static_dynamic : ∀p,p',prog.asm_no_duplicates p prog →
+lemma labels_of_trace_are_in_code :
+∀p,p',prog.∀st1,st2 :  vm_state p p'.∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2.
+∀lbl.
+mem … lbl (get_costlabels_of_trace … t) → 
+mem … (costlab lbl) (map ?? \fst … (labels_pc … (instructions p prog) O)).
+#p #p' #prog #st1 #st2 #t elim t
+[ #st #lbl *
+| #st1 #st2 #st3 #l * #H1 #H2 #tl #IH #lbl whd in match (get_costlabels_of_trace ????);
+  #H cases(mem_append ???? H) -H [2: #H @IH //] 
+  lapply(vm_step_to_eval … H2) whd in match eval_vmstate;
+  normalize nodelta #H cases(bind_inversion ????? H) -H #i * #EQi #_
+  inversion(emits_labels … i)
+  [ #EQemit cases(step_emit … (vm_step_to_eval … H2)) // #x * #EQ1 #EQ2 >EQ1 *
+    [2: *] #EQ destruct cases(map_mem … \fst … EQ2) #y * #H3 #EQ destruct //
+  | #f #EQemit >(proj1 … (step_non_emit … EQi (vm_step_to_eval … H2) … EQemit))
+    *
+  ]
+]  
+qed.
+
+let rec dependent_map (A,B : Type[0]) (l : list A) (f : ∀a : A.mem … a l → B) on l : list B ≝ 
+(match l return λx.l=x → ? with
+[ nil ⇒ λ_.nil ?
+| cons x xs ⇒ λprf.(f x ?) :: dependent_map A B xs (λx,prf1.f x ?)
+])(refl …).
+[ >prf %% | >prf %2 assumption]
+qed.
+
+lemma dependent_map_append : ∀A,B,l1,l2,f.
+dependent_map A B (l1 @ l2) (λa,prf.f a prf) = 
+(dependent_map A B l1 (λa,prf.f a ?)) @ (dependent_map A B l2 (λa,prf.f a ?)).
+[2: @hide_prf /2/ | 3: @hide_prf /2/]
+#A #B #l1 elim l1 normalize /2/
+qed.
+
+lemma rewrite_in_dependent_map : ∀A,B,l1,l2,f.
+        ∀EQ:l1 = l2.
+         dependent_map A B l1 (λa,prf.f a prf) =
+         dependent_map A B l2 (λa,prf.f a ?).
+[2: >EQ // | #A #B #l1 #l2 #f #EQ >EQ in f; #f % ]
+qed.
+
+
+lemma static_dynamic : ∀p,p',prog.∀no_dup : asm_no_duplicates p prog.
 ∀abs_t : abstract_transition_sys (m … p').∀instr_m.
 ∀good : static_galois … (asm_static_analisys_data p p' prog abs_t instr_m).∀mT,map1.
-static_analisys p ? instr_m mT prog = return map1 →
+∀EQmap : static_analisys p ? instr_m mT prog = return map1.
 ∀st1,st2 : vm_state p p'.
 ∀ter : terminated_trace (asm_operational_semantics p p' prog) st2.
@@ -755 +822 @@
 let stop_state ≝ match R_post_step … ter with [None ⇒ st2 | Some x ⇒ \snd x ] in
 ∀costs.
-costs = map … (λlbl.(opt_safe … (get_map … map1 lbl) ?)) (get_costlabels_of_trace …  t) →
+costs = dependent_map CostLabel ? (get_costlabels_of_trace …  t) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) →
 rel_galois … good stop_state (act_abs … abs_t (big_op … costs) (act_abs … abs_t k a1)).
-[2: @hide_prf cases daemon]
+[2: @hide_prf 
+    cases(mem_map ????? (labels_of_trace_are_in_code … prf)) *
+    #lbl' #pc * #Hmem #EQ destruct    
+    >(proj1 … (static_analisys_ok … no_dup … EQmap … Hmem))
+    @(proj2 … (static_analisys_ok … no_dup … EQmap … Hmem))
+]
 #p #p' #prog #no_dup #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #ter #t
 lapply ter -ter elim t
@@ -786 +858 @@
     [4,8: cases H1 [1,3: * |*: * #y #EQ destruct]]
     >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct
-    #a1 #good_st_a1 whd in match (map ????); #costs #EQ >EQ >neutral_r
+    #a1 #good_st_a1 whd in match (dependent_map ????); #costs #EQ >EQ >neutral_r
     >act_neutral
     @(instr_map_ok … good … EQfetch … good_st_a1) /2/
@@ -792 +864 @@
 | -st1 -st2 #st1 #st2 #st3 #l * #H3 #H4 #tl #IH #ter #k #H
   #H2 #a1 #good_a1 whd in match (get_costlabels_of_trace ????);
-  whd #costs whd in match list_cost_to_list_initcost; normalize nodelta 
-  <map_append <map_append 
-  change with (list_cost_to_list_initcost ?) in match (list_cost_to_list_initcost ?);  
-  #EQ destruct whd in H2 : (??%?); >H3 in H2; normalize nodelta #H
-  cases(bind_inversion ????? H) -H #i * #EQi
+  whd #costs >dependent_map_append
+  (*change with (list_cost_to_list_initcost ?) in match (list_cost_to_list_initcost ?);*)  
+  #EQ destruct whd in H2 : (??%?); lapply H2 >H3 in ⊢ (% → ?); -H2 
+  normalize nodelta #H cases(bind_inversion ????? H) -H #i * #EQi
   inversion(emits_labels ??)
   [ #EQemits whd in ⊢ (??%% → ?); #EQ destruct  >big_op_associative >act_op @IH
@@ -813 +884 @@
     |5,10: #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H *
     ] //
-  | cases(step_emit … EQi (vm_step_to_eval … H4) … EQemits) #x * #EQx #Hx >EQx
-    whd in match (map ????); whd in match (map ????); whd in match (big_op ??);
-    >neutral_l @opt_safe_elim #elem #EQget <(static_analisys_ok  … x … (pc … st2) … EQmap)
-    assumption
+  | cases(step_emit … EQi (vm_step_to_eval … H4) … EQemits) #x * #EQx #Hx
+    >(rewrite_in_dependent_map … EQx)
+  
+    whd in match (dependent_map ????); whd in match (dependent_map ????); whd in match (big_op ??);
+    >neutral_l @opt_safe_elim #elem #EQget
+    cases (static_analisys_ok  … x … (pc … st2) … no_dup … EQmap) //
+    #EQ #_ <EQ assumption
   | >neutral_r  @(instr_map_ok … good … EQi … good_a1) /2/
   | %
@@ -822 +896 @@
     >(monotonicity_of_block_cost … EQk') //
   | @(instr_map_ok … good … EQi … good_a1) /2/
-  | >(proj1 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits)) %
-  ]
-]
-qed.
-
-
-
-
+  | lapply (proj1 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits))
+    #EQ >(rewrite_in_dependent_map … EQ) %
+  ]
+]
+qed.
+
+
+
+