Changeset 3463 for LTS

Timestamp:

Feb 21, 2014, 6:15:38 PM (7 years ago)

Author:

piccolo

Message:

 

File:

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

LTS/Vm.ma

@@ -29 +29 @@
 | Iret: AssemblerInstr p.
 
-definition AssemblerProgram ≝λp.list (AssemblerInstr p) × ℕ.
+record AssemblerProgram (p : assembler_params) : Type[0] ≝ 
+{ instructions : list (AssemblerInstr p)
+; endmain : ℕ
+; endmain_ok : endmain ≤ |instructions|
+}.
 
 definition fetch: ∀p.AssemblerProgram p → ℕ → option (AssemblerInstr p) ≝
- λp,l,n. nth_opt ? n (\fst l).
+ λp,l,n. nth_opt ? n (instructions … l).
 
 definition stackT: Type[0] ≝ list (nat).
@@ -43 +47 @@
 ; eval_asm_io : io_instr p → asm_store_type → option asm_store_type
 ; cost_of_io : io_instr p → asm_store_type → m
-; cost_of : AssemblerInstr p → m
+; cost_of : AssemblerInstr p → asm_store_type →  m
 }.
 
@@ -73 +77 @@
            asm_is_io … st1 = asm_is_io … st2 → 
            S (pc … st1) = pc … st2 → 
-           op … (cost … st1) (cost_of p p' (Seq p i l)) = cost … st2 → 
+           op … (cost … st1) (cost_of p p' (Seq p i l) (asm_store … st1)) = cost … st2 → 
            vmstep … (cost_act l) st1 st2
 | vm_ijump : ∀st1,st2 : vm_state p p'.∀new_pc : ℕ. 
@@ -82 +86 @@
            asm_is_io … st1 = asm_is_io … st2 → 
            new_pc = pc … st2 → 
-           op … (cost … st1) (cost_of p p' (Ijmp … new_pc)) = cost … st2 → 
+           op … (cost … st1) (cost_of p p' (Ijmp … new_pc) (asm_store … st1)) = cost … st2 → 
            vmstep … (cost_act (None ?)) st1 st2
 | vm_cjump_true : 
@@ -93 +97 @@
            asm_is_io … st1 = asm_is_io … st2 → 
            pc … st2 = new_pc → 
-           op … (cost … st1) (cost_of p p' (CJump p cond new_pc ltrue lfalse)) = cost … st2 → 
+           op … (cost … st1) (cost_of p p' (CJump p cond new_pc ltrue lfalse) (asm_store … st1)) = cost … st2 → 
            vmstep … (cost_act (Some ? ltrue)) st1 st2
 | vm_cjump_false : 
@@ -104 +108 @@
            asm_is_io … st1 = asm_is_io … st2 → 
            S (pc … st1) = pc … st2 → 
-           op … (cost … st1) (cost_of p p' (CJump … cond new_pc ltrue lfalse)) = cost … st2 → 
+           op … (cost … st1) (cost_of p p' (CJump … cond new_pc ltrue lfalse) (asm_store … st1)) = cost … st2 → 
            vmstep … (cost_act (Some ? lfalse)) st1 st2
 | vm_io_in :  
@@ -134 +138 @@
            asm_is_io … st1 = asm_is_io … st2 → 
            entry_of_function p  f = pc … st2 → 
-           op … (cost … st1) (cost_of p p' (Icall p f)) = cost … st2 → 
+           op … (cost … st1) (cost_of p p' (Icall p f) (asm_store … st1)) = cost … st2 → 
            label_of_pc ? (call_label_fun p) (entry_of_function p f) = return lbl → 
            vmstep … (call_act f lbl) st1 st2
@@ -146 +150 @@
            newpc = pc … st2 → 
            label_of_pc ? (return_label_fun p) newpc = return lbl → 
-           op … (cost … st1) (cost_of p p' (Iret p)) = cost … st2 → 
+           op … (cost … st1) (cost_of p p' (Iret p) (asm_store … st1)) = cost … st2 → 
            vmstep … (ret_act (Some ? lbl)) st1 st2.
 
@@ -161 +165 @@
      return 〈cost_act opt_l,
              mk_vm_state ?? (S (pc … st)) (asm_stack … st) new_store false
-                (op … (cost … st) (cost_of p p' (Seq p x opt_l)))〉
+                (op … (cost … st) (cost_of p p' (Seq p x opt_l) (asm_store … st)))〉
 | Ijmp newpc ⇒ 
    if asm_is_io … st then
@@ -168 +172 @@
      return 〈cost_act (None ?),
              mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false
-                (op … (cost … st) (cost_of p p' (Ijmp … newpc)))〉
+                (op … (cost … st) (cost_of p p' (Ijmp … newpc) (asm_store … st)))〉
 | CJump cond newpc ltrue lfalse ⇒ 
    if asm_is_io … st then
@@ -177 +181 @@
        return 〈cost_act (Some ? ltrue),
                mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false
-                (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse)))〉
+                (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse) (asm_store … st)))〉
      else
        return 〈cost_act (Some ? lfalse),
                mk_vm_state ?? (S (pc … st)) (asm_stack … st) (asm_store … st) false
-                (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse)))〉
+                (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse) (asm_store … st)))〉
 | Iio lin io lout ⇒ 
               if asm_is_io … st then 
@@ -203 +207 @@
                              ((S (pc … st)) :: (asm_stack … st))
                              (asm_store … st) false
-                             (op … (cost … st) (cost_of p p' (Icall p f)))〉
+                             (op … (cost … st) (cost_of p p' (Icall p f) (asm_store … st)))〉
 | Iret ⇒ if asm_is_io … st then
             None ?
@@ -211 +215 @@
             return 〈ret_act (Some ? lbl),
                     mk_vm_state ?? newpc tl (asm_store … st) false   
-                     (op … (cost … st) (cost_of p p' (Iret p)))〉
+                     (op … (cost … st) (cost_of p p' (Iret p) (asm_store … st)))〉
 ].
 
@@ -245 +249 @@
 qed.
 
+ 
+lemma vm_step_to_eval : ∀p,p',prog,st1,st2,l.vmstep … prog l st1 st2 → 
+eval_vmstate p p' prog st1 = return 〈l,st2〉.
+#p #p' #prog * #pc1 #stack1 #store1 #io1 #cost1
+* #pc2 #stack2 #store2 #io2 #cost2 #l #H inversion H
+[ #s1 #s2 #i #opt_l #EQfetch #EQio #EQstore #EQstack #EQio1 #EQpc #EQcost
+  #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; normalize nodelta   
+  >EQfetch >m_return_bind normalize nodelta >EQio normalize nodelta >EQstore
+  >m_return_bind <EQio1 >EQio <EQpc >EQstack >EQcost %
+| #s1 #s2 #newpc #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQnewpc #EQcost
+  #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; normalize nodelta
+  >EQfetch >m_return_bind normalize nodelta >EQio1 normalize nodelta <EQio2 >EQio1
+  >EQstore >EQstack <EQcost >EQstore %
+|3,4: #s1 #s2 #cond #newoc #ltrue #lfalse #EQev_cond #EQfetch #EQio1 #EQstore
+  #EQstack #EQio2 #EQnewoc #EQcost #EQ1 #EQ2 #EQ3 #EQ4 destruct
+  whd in match eval_vmstate; normalize nodelta >EQfetch >m_return_bind 
+  normalize nodelta >EQio1 normalize nodelta >EQev_cond >m_return_bind
+  normalize nodelta <EQio1 >EQio2 >EQstore >EQstack <EQcost >EQstore [%] >EQnewoc %
+|5,6: #s1 #s2 #lin #io #lout #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQpc
+   #EQcost #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate;
+   normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1
+   normalize nodelta >EQstack <EQpc >EQcost [ >EQstore <EQio2 %]
+   >EQstore >m_return_bind <EQpc <EQio2 %
+| #s1 #s2 #f #lbl #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQentry
+  #EQcost #EQlab_pc #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate;
+  normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1
+  normalize nodelta >EQlab_pc >m_return_bind >EQentry >EQcost <EQio2 >EQio1
+  <EQstack >EQstore %
+| #s1 #s2 #newpc #lbl #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQnewpc
+  #EQlab_pc #EQcosts #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate;
+  normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1 normalize nodelta
+  >EQstack whd in match option_pop; normalize nodelta >m_return_bind
+  >EQlab_pc >m_return_bind >EQcosts >EQstore  <EQio2 >EQio1 %
+]
+qed.
+
+coercion vm_step_to_eval.
+
 include "../src/utilities/hide.ma".
 
@@ -252 +294 @@
 λp,p',prog.mk_abstract_status 
                 (vm_state p p') 
-                (λl.λst1,st2 : vm_state p p'.(eqb (pc ?? st1) (\snd prog)) = false ∧ 
+                (λl.λst1,st2 : vm_state p p'.(eqb (pc ?? st1) (endmain … prog)) = false ∧ 
                                vmstep p p' prog l st1 st2) 
                 (λ_.λ_.True)
@@ -269 +311 @@
                 (λ_.true) 
                 (λs.eqb (pc ?? s) O)
-                (λs.eqb (pc … s) (\snd prog))
+                (λs.eqb (pc … s) (endmain … prog))
                 ???.
-@hide_prf cases daemon (*
+@hide_prf
 [ #s1 #s2 #l inversion(fetch ???) normalize nodelta
   [ #_ #EQ destruct] * normalize nodelta
@@ -281 +323 @@
   | #_
   ]
-  #EQ destruct * #_ #H inversion H in ⊢ ?;
-  [ #st1 #st2 #i #lbl #EQ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 
-  | #st1 #st2 #new_pc #EQ #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23
-  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35
-  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47
-  | #st1 #st2 #lin #io #lout #EQ #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59
-  | #st1 #st2 #lin #io #lout #EQ #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71
-  | #st1 #st2 #f #EQ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83
-  | #st1 #st2 #new_pc #EQ #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95
-  ]   
-  destruct >EQfetch in EQ; whd in ⊢ (??%% → ?); #EQ 
-  lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct % //
+  #EQ destruct * #_ #H lapply(vm_step_to_eval … H) whd in match eval_vmstate;
+  normalize nodelta >EQfetch >m_return_bind normalize nodelta cases(asm_is_io ??)
+  normalize nodelta [ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(bind_inversion ????? H) -H
+  * * #_ normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct % //
 | #s1 #s2 #l inversion(fetch ???) normalize nodelta
   [ #_ #EQ destruct] * normalize nodelta
@@ -302 +336 @@
   | #_
   ]
-  #EQ destruct * #_ #H inversion H in ⊢ ?;
-  [ #st1 #st2 #i #lbl #EQf #EQio1 #H2 #H3 #H4 #EQio2 #H6 #H7 #H8 #H9 #H10 #H11 
-  | #st1 #st2 #new_pc #EQf #EQio1 #H13 #H14 #H15 #EQio2 #H17 #H18 #H19 #H20 #H21 #H22
-  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQf #EQio1 #H26 #H27 #H28 #EQio2 #H30 #H31 #H32 #H33 #H34 #H35
-  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQf #EQio1 #H38 #H39 #H40 #EQio2 #H42 #H43 #H44 #H45 #H46 #H47
-  | #st1 #st2 #lin #io #lout #EQf #EQio1 #H50 #H51 #H52 #EQio2 #H54 #H55 #H56 #H57 #H58 #H59
-  | #st1 #st2 #lin #io #lout #EQf #EQio1 #H61 #H62 #H63 #EQio2 #H65 #H66 #H67 #H68 #H69 #H70
-  | #st1 #st2 #f #EQf #EQio1 #H74 #H75 #H76 #EQio2 #H78 #H79 #H80 #H81 #H82 #H83
-  | #st1 #st2 #new_pc #EQf #EQio1 #H86 #H87 #H88 #EQio2 #H90 #H91 #H92 #H93 #H94 #H95
-  ]   
-  destruct >EQio in EQio2; >EQio1 #EQ destruct %{lin} //
+  #EQ destruct * #_ #H lapply(vm_step_to_eval … H) whd in match eval_vmstate;
+  normalize nodelta #H cases(bind_inversion ????? H) -H *
+  [ #seq1 #lbl1 
+  | #n1
+  | #cond1 #newpc1 #ltrue1 #lfalse1
+  | #lin1 #io1 #lout1
+  | #f 
+  |
+  ]
+  normalize nodelta * #_ cases(asm_is_io ??) normalize nodelta
+  [1,3,5,9,11: whd in ⊢ (??%% → ?); #EQ destruct
+  |2,6,7,10,12: #H cases(bind_inversion ????? H) -H #x * #_ 
+    [2: cases x normalize nodelta
+    |5: #H cases(bind_inversion ????? H) -H #y * #_ 
+    ]
+  ] 
+  whd in ⊢ (??%% → ?); #EQ destruct destruct % //
 |  #s1 #s2 #l inversion(fetch ???) normalize nodelta
   [ #_ #EQ destruct] * normalize nodelta
   [ #seq #lbl #_
   | #n #_
-  | #cond #newpc #ltrue #lfalse #EQfetch
-  | #lin #io #lout #EQfetch cases (asm_is_io ??) normalize nodelta
+  | #cond #newpc #ltrue #lfalse #_
+  | #lin #io #lout #EQfetch inversion(asm_is_io ??) normalize nodelta #EQio
   | #f #_
   | #_
   ]
-  #EQ destruct * #_ #H inversion H in ⊢ ?;
-  [ #st1 #st2 #i #lbl #EQ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 
-  | #st1 #st2 #new_pc #EQ #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23
-  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35
-  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47
-  | #st1 #st2 #lin1 #io1 #lout1 #EQ #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59
-  | #st1 #st2 #lin1 #io1 #lout1 #EQ #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71
-  | #st1 #st2 #f #EQ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83
-  | #st1 #st2 #new_pc #EQ #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95
-  ]   
-  destruct >EQfetch in EQ; whd in ⊢ (??%% → ?); #EQ 
-  lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct % //
-]*)
+  #EQ destruct * #_ #H lapply(vm_step_to_eval … H) whd in match eval_vmstate;
+  normalize nodelta  >EQfetch >m_return_bind normalize nodelta >EQio
+  normalize nodelta #H cases(bind_inversion ????? H) -H #x * #_ 
+  whd in ⊢ (??%% → ?); #EQ destruct % //
 qed.
 
@@ -358 +389 @@
  … (fetch_state p p' prog) instr_m.
 
+definition non_empty_list : ∀A.list A → bool ≝ 
+λA,l.match l with [ nil ⇒ false | _ ⇒  true ].
 
 let rec block_cost (p : assembler_params) 
@@ -368 +401 @@
   [ O ⇒ None ?
   | S program_size' ⇒ 
-    if eqb program_counter (\snd prog) then
+    if eqb program_counter (endmain … prog) then
        return e … abs_t
     else
@@ -379 +412 @@
   ].
  
-axiom initial_act : CostLabel.
+inductive InitCostLabel : Type[0] ≝ 
+  costlab : CostLabel → InitCostLabel
+| initial_act : InitCostLabel.
+
+definition eq_init_costlabel ≝ (λi1,i2.match i1 with
+ [ initial_act ⇒ match i2 with [initial_act ⇒ true | _ ⇒ false ]
+ | costlab c ⇒ match i2 with [costlab c1 ⇒ c == c1 | _ ⇒ false ]
+ ]).
+
+definition DEQInitCostLabel ≝ mk_DeqSet InitCostLabel eq_init_costlabel ?.
+* [#c] * [1,3: #c1] whd in match eq_init_costlabel; normalize nodelta 
+[4: /2/ | 2,3: % #EQ destruct] % [ #H >(\P H) % | #EQ destruct >(\b (refl …)) %]
+qed.
+
+coercion costlab.
+
+definition list_cost_to_list_initcost : list CostLabel → list InitCostLabel ≝ 
+map … costlab.
+
+coercion list_cost_to_list_initcost.
   
 record cost_map_T (dom : DeqSet) (codom : Type[0]) : Type[1] ≝ 
@@ -390 +442 @@
 }.
 
-let rec labels_pc (p : assembler_params)
-(prog : list (AssemblerInstr p)) (program_counter : ℕ) on prog : list (CostLabel × ℕ) ≝ 
-match prog with
-[ nil ⇒ [〈initial_act,O〉] @ 
-        map … (λx.let〈y,z〉 ≝ x in 〈a_call z,y〉) (call_label_fun … p) @
-        map … (λx.let〈y,z〉 ≝ x in 〈a_return_post z,y〉) (return_label_fun … p)
-| cons i is ⇒ 
-  match i with
+definition labels_pc_of_instr : ∀p.AssemblerInstr p → ℕ → list (InitCostLabel × ℕ) ≝ 
+λp,i,program_counter.
+match i with
   [ Seq _ opt_l ⇒ match opt_l with 
-                  [ Some lbl ⇒ [〈a_non_functional_label lbl,S program_counter〉]
+                  [ Some lbl ⇒ [〈costlab (a_non_functional_label lbl),S program_counter〉]
                   | None ⇒ [ ]
                   ]
   | Ijmp _ ⇒ [ ]
-  | CJump _ newpc ltrue lfalse ⇒ [〈a_non_functional_label ltrue,newpc〉;〈a_non_functional_label lfalse,S program_counter〉]
-  | Iio lin _ lout ⇒ [〈a_non_functional_label lout,S program_counter〉]
+  | CJump _ newpc ltrue lfalse ⇒ [〈costlab (a_non_functional_label ltrue),newpc〉;
+                                  〈costlab (a_non_functional_label lfalse),S program_counter〉]
+  | Iio lin _ lout ⇒ [〈costlab (a_non_functional_label lin),program_counter〉;
+                      〈costlab (a_non_functional_label lout),S program_counter〉]
   | Icall f ⇒ [ ]
   | Iret ⇒ [ ]
-  ] @ labels_pc p is (S program_counter)              
+  ].
+
+let rec labels_pc (p : assembler_params)
+(prog : list (AssemblerInstr p)) (program_counter : ℕ) on prog : list (InitCostLabel × ℕ) ≝ 
+match prog with
+[ nil ⇒ [〈initial_act,O〉] @ 
+        map … (λx.let〈y,z〉 ≝ x in 〈costlab (a_call z),y〉) (call_label_fun … p) @
+        map … (λx.let〈y,z〉 ≝ x in 〈costlab (a_return_post z),y〉) (return_label_fun … p)
+| cons i is ⇒ (labels_pc_of_instr … i program_counter)@labels_pc p is (S program_counter)
 ].
 
+lemma labels_pc_ok : ∀p,prog,i,lbl,pc,m.
+fetch p prog pc = return i →
+mem ? lbl (labels_pc_of_instr … i (m+pc)) → 
+mem ? lbl (labels_pc p (instructions … prog) m).
+#p * #instrs #end_main #Hend_main #i #lbl #pc 
+whd in match fetch; normalize nodelta lapply pc -pc
+-end_main elim instrs
+[ #pc #m whd in ⊢ (??%% → ?); #EQ destruct]
+#x #xs #IH * [|#pc'] #m whd in ⊢ (??%% → ?);
+[ #EQ destruct #lbl_addr whd in match (labels_pc ???);
+  /2 by mem_append_l1/
+| #EQ #H2 whd in match (labels_pc ???); @mem_append_l2 @(IH … EQ) //
+]
+qed.
+
+lemma labels_pc_return: ∀p,prog,x1,x2.
+ label_of_pc ReturnPostCostLabel (return_label_fun p) x1=return x2 →
+ ∀m.
+   mem … 〈costlab (a_return_post x2),x1〉 (labels_pc p (instructions p prog) m).
+ #p * #l #endmain #_ whd in match (labels_pc ???); #x1 #x2 #H elim l
+[ #m @mem_append_l2 @mem_append_l2 whd in H:(??%?);
+  elim (return_label_fun ?) in H; [ whd in ⊢ (??%% → ?); #EQ destruct]
+  * #x #y #tl #IH whd in ⊢ (??%? → %); normalize nodelta @eqb_elim
+  normalize nodelta
+  [ #EQ whd in ⊢ (??%% → ?); #EQ2 destruct /2/
+  | #NEQ #H2 %2 @IH // ] 
+| #hd #tl #IH #m @mem_append_l2 @IH ]
+qed.
+
+lemma labels_pc_call: ∀p,prog,x1,x2.
+ label_of_pc CallCostLabel (call_label_fun p) x1=return x2 →
+ ∀m.
+   mem … 〈costlab (a_call x2),x1〉 (labels_pc p (instructions p prog) m).
+ #p * #l #endmain #_ whd in match (labels_pc ???); #x1 #x2 #H elim l
+[ #m @mem_append_l2 @mem_append_l1 whd in H:(??%?);
+  elim (call_label_fun ?) in H; [ whd in ⊢ (??%% → ?); #EQ destruct]
+  * #x #y #tl #IH whd in ⊢ (??%? → %); normalize nodelta @eqb_elim
+  normalize nodelta
+  [ #EQ whd in ⊢ (??%% → ?); #EQ2 destruct /2/
+  | #NEQ #H2 %2 @IH // ] 
+| #hd #tl #IH #m @mem_append_l2 @IH ]
+qed.
+
+unification hint  0 ≔ ; 
+    X ≟ DEQInitCostLabel
+(* ---------------------------------------- *) ⊢ 
+    InitCostLabel ≡ carr X.
+
+
+unification hint  0 ≔ p1,p2; 
+    X ≟ DEQInitCostLabel
+(* ---------------------------------------- *) ⊢ 
+    eq_init_costlabel p1 p2 ≡ eqb X p1 p2.
+    
+
+let rec m_foldr (M : Monad) (X,Y : Type[0]) (f : X→Y→M Y) (l : list X) (y : Y) on l : M Y ≝ 
+match l with
+[ nil ⇒ return y
+| cons x xs ⇒ ! z ← m_foldr M X Y f xs y; f x z
+].
+
 definition static_analisys : ∀p : assembler_params.∀abs_t : monoid.(AssemblerInstr p → abs_t) → 
-∀mT : cost_map_T DEQCostLabel abs_t.AssemblerProgram p → option mT ≝
+∀mT : cost_map_T DEQInitCostLabel abs_t.AssemblerProgram p → option mT ≝
 λp,abs_t,instr_m,mT,prog.
-let 〈instrs,final〉 ≝ prog in
-let prog_size ≝ S (|instrs|) in
-m_fold Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost p prog abs_t instr_m w prog_size;  
-                               return set_map … m z k) (labels_pc … instrs O) 
-      (empty_map ?? mT). 
+let prog_size ≝ S (|instructions … prog|) in
+m_foldr Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost p prog abs_t instr_m w prog_size;  
+                               return set_map … m z k) (labels_pc … (instructions … prog) O) 
+      (empty_map ?? mT).
+      
+
+include "basics/lists/listb.ma".
+
+(*doppione da mettere a posto*)
+let rec no_duplicates (A : DeqSet) (l : list A) on l : Prop ≝ 
+match l with
+[ nil ⇒ True 
+| cons x xs ⇒ ¬ (bool_to_Prop (x ∈ xs)) ∧ no_duplicates … xs
+].
+
+definition asm_no_duplicates ≝ 
+λp,prog.no_duplicates … (map ?? \fst … (labels_pc … (instructions p prog) O)).
 
 (*falso: necessita di no_duplicates*)
-axiom static_analisys_ok : ∀p,abs_t,instr_m,mT,prog,lbl,pc,map.
+
+definition eq_deq_prod : ∀D1,D2 : DeqSet.D1 × D2 → D1 × D2 → bool ≝ 
+λD1,D2,x,y.\fst x == \fst y ∧ \snd x == \snd y.
+
+definition DeqProd ≝ λD1 : DeqSet.λD2 : DeqSet.
+mk_DeqSet (D1 × D2) (eq_deq_prod D1 D2) ?.
+@hide_prf
+* #x1 #x2 * #y1 #y2 whd in match eq_deq_prod; normalize nodelta
+% [2: #EQ destruct @andb_Prop >(\b (refl …)) %]
+inversion (? ==?) #EQ1 whd in match (andb ??); #EQ2 destruct
+>(\P EQ1) >(\P EQ2) %
+qed.
+(*
+unification hint  0 ≔ D1,D2 ; 
+    X ≟ DeqProd D1 D2
+(* ---------------------------------------- *) ⊢ 
+    D1 × D2 ≡ carr X.
+
+
+unification hint  0 ≔ D1,D2,p1,p2; 
+    X ≟ DeqProd D1 D2
+(* ---------------------------------------- *) ⊢ 
+    eq_deq_prod D1 D2 p1 p2 ≡ eqb X p1 p2.
+    
+definition deq_prod_to_prod : ∀D1,D2 : DeqSet.DeqProd D1 D2 → D1 × D2 ≝ 
+λD1,D2,x.x.
+
+coercion deq_prod_to_prod.
+*)
+
+lemma map_mem : ∀A,B,f,l,a.mem A a l → ∃b : B.mem B b (map A B f l) 
+∧ b = f a.
+#A #B #f #l elim l [ #a *] #x #xs #IH #a *
+[ #EQ destruct %{(f x)} % // % // | #H cases(IH … H)
+  #b * #H1 #EQ destruct %{(f a)} % // %2 //
+]
+qed.
+
+lemma static_analisys_ok : ∀p,abs_t,instr_m,mT,prog,lbl,pc,map.
+asm_no_duplicates p prog → 
 static_analisys p abs_t instr_m mT prog = return map → 
-mem … 〈lbl,pc〉 (labels_pc … (\fst prog) O) → 
-get_map … map lbl = block_cost … prog abs_t instr_m pc (S (|(\fst prog)|)).  
+mem … 〈lbl,pc〉 (labels_pc … (instructions … prog) O) → 
+get_map … map lbl = block_cost … prog abs_t instr_m pc (S (|(instructions … prog)|)).
+#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 ???)
+#l #endmain #Hendmain elim l [ #x #y #z #w #h * ]
+* #hd1 #hd2 #tl #IH #lbl #pc #map * #H1 #H2 #H 
+cases(bind_inversion ????? H) -H #map1 * #EQmap1 normalize nodelta #H 
+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
+]
+qed.
 
 include "Simulation.ma".
@@ -437 +619 @@
                ]
  }.
- 
-axiom vm_step_to_eval : ∀p,p',prog,st1,st2,l.vmstep … prog l st1 st2 → 
-eval_vmstate p p' prog st1 = return 〈l,st2〉.
-
-coercion vm_step_to_eval.
 
 definition big_op: ∀M: monoid. list M → M ≝
@@ -472 +649 @@
 qed.
 
-lemma static_dynamic : ∀p,p',prog.
+lemma monotonicity_of_block_cost : ∀p,prog,abs_t,instr_m,pc,size,k.
+block_cost p prog abs_t instr_m pc size = return k → 
+∀size'.size ≤ size' → 
+block_cost p prog abs_t instr_m pc size' = return k.
+#p #prog #abs_t #instr_m #pc #size lapply pc elim size
+[ #pc #k whd in ⊢ (??%% → ?); #EQ destruct]
+#n #IH #pc #k whd in ⊢ (??%% → ?); @eqb_elim
+[ #EQ destruct normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct
+  #size' * [2: #m #_] whd in ⊢ (??%%); @eqb_elim try( #_ %) * #H @⊥ @H %
+| #Hpc normalize nodelta #H cases(bind_inversion ????? H) -H #i
+  * #EQi #H cases(bind_inversion ????? H) -H #elem * #EQelem whd in ⊢ (??%% → ?);
+  #EQ destruct #size' *
+  [ whd in ⊢ (??%?); @eqb_elim
+    [ #EQ @⊥ @(absurd ?? Hpc) assumption ]
+    #_ normalize nodelta >EQi >m_return_bind >EQelem %
+  | #m #Hm whd in ⊢ (??%?); @eqb_elim
+    [ #EQ @⊥ @(absurd ?? Hpc) assumption ]
+    #_ normalize nodelta >EQi >m_return_bind
+    cases (emits_labels ??) in EQelem; normalize nodelta
+    [ whd in ⊢ (??%%→ ??%%); #EQ destruct %]
+    #f #EQelem >(IH … EQelem) [2: /2/ ] %
+  ]
+]
+qed.
+
+lemma step_emit : ∀p,p',prog,st1,st2,l,i.
+fetch p prog (pc … st1) = return i →
+eval_vmstate p p' … prog st1 = return 〈l,st2〉 →  
+emits_labels … i = None ? → ∃x.
+match l in ActionLabel return λ_:ActionLabel.(list CostLabel) with 
+[call_act f c ⇒ [a_call c]
+|ret_act x ⇒ 
+   match x with [None⇒[]|Some c⇒[a_return_post c]]
+|cost_act x ⇒
+   match x with [None⇒[]|Some c⇒[a_non_functional_label c]]
+|init_act⇒[ ]
+] = [x] ∧ 
+ (mem … 〈costlab x,pc … st2〉 (labels_pc p (instructions … prog) O)).
+#p #p' #prog #st1 #st2 #l #i #EQi whd in match eval_vmstate; normalize nodelta
+>EQi >m_return_bind normalize nodelta cases i in EQi; -i normalize nodelta
+[ #seq * [|#lab]
+| #newpc
+| #cond #newpc #ltrue #lfalse
+| #lin #io #lout
+| #f
+|
+]
+#EQi cases(asm_is_io ???) normalize nodelta
+[1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct
+|2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x1 * #EQx1
+  [3: cases x1 in EQx1; -x1 #EQx1 normalize nodelta
+  |6: #H cases(bind_inversion ????? H) -H #x2 * #EQx2
+  ]
+]
+whd in ⊢ (??%% → ?); #EQ destruct whd in match emits_labels;
+normalize nodelta #EQ destruct % [2,4,6,8,10,12,14: % try % |*:]
+[1,2,4,5,7: @(labels_pc_ok … EQi) normalize /3 by or_introl,or_intror/ ]
+/2 by labels_pc_return, labels_pc_call/
+qed.
+
+lemma step_non_emit : ∀p,p',prog,st1,st2,l,i,f.
+fetch p prog (pc … st1) = return i →
+eval_vmstate p p' … prog st1 = return 〈l,st2〉 →  
+emits_labels … i = Some ? f → 
+match l in ActionLabel return λ_:ActionLabel.(list CostLabel) with 
+[call_act f c ⇒ [a_call c]
+|ret_act x ⇒ 
+   match x with [None⇒[]|Some c⇒[a_return_post c]]
+|cost_act x ⇒
+   match x with [None⇒[]|Some c⇒[a_non_functional_label c]]
+|init_act⇒[ ]
+] = [ ] ∧ pc … st2 = f (pc … st1).
+#p #p' #prog #st1 #st2 #l #i #f #EQi whd in match eval_vmstate; normalize nodelta
+>EQi >m_return_bind normalize nodelta cases i in EQi; -i normalize nodelta
+[ #seq * [|#lab]
+| #newpc
+| #cond #newpc #ltrue #lfalse
+| #lin #io #lout
+| #f
+|
+]
+#EQi cases(asm_is_io ???) normalize nodelta
+[1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct
+|2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x1 * #EQx1
+  [3: cases x1 in EQx1; -x1 #EQx1 normalize nodelta
+  |6: #H cases(bind_inversion ????? H) -H #x2 * #EQx2
+  ]
+]
+whd in ⊢ (??%% → ?); #EQ destruct whd in match emits_labels;
+normalize nodelta #EQ destruct /2 by refl, conj/
+qed.
+
+
+lemma static_dynamic : ∀p,p',prog.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.
@@ -481 +751 @@
 ∀k.
 pre_measurable_trace … t → 
-block_cost p prog … instr_m (pc … st1) (S (|(\fst prog)|)) = return k → 
+block_cost p prog … instr_m (pc … st1) (S (|(instructions … prog)|)) = return k → 
 ∀a1.rel_galois … good st1 a1 → 
 let stop_state ≝ match R_post_step … ter with [None ⇒ st2 | Some x ⇒ \snd x ] in
@@ -488 +758 @@
 rel_galois … good stop_state (act_abs … abs_t (big_op … costs) (act_abs … abs_t k a1)).
 [2: @hide_prf cases daemon]
-#p #p' #prog #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #ter #t
+#p #p' #prog #no_dup #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #ter #t
 lapply ter -ter elim t
 [ #st #ter inversion(R_post_step … ter) normalize nodelta [| * #lbl #st3 ] 
@@ -522 +792 @@
 | -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 <map_append #EQ destruct >big_op_associative >act_op @IH
-  [    
-  inversion H in ⊢ ?; 
-  [ #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct
-  | #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #opt_l #EQ destruct #pre_tl1 #_
-    #EQ1 #EQ2 #EQ3 #EQ4 destruct
-  | #s1 #s2 #s3 #lbl #s1_noio #exe #tl1 * #lbl1 #EQ destruct #pre_tl1 #_
-    #EQ1 #EQ2 #EQ3 #EQ4 destruct
-  | #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #f * #lbl1 #EQ destruct
-    * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
-  | #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H *
-  ] //
-  | whd in H2 : (??%?); >H3 in H2; normalize nodelta #H
-    cases(bind_inversion ????? H) #i * #EQi whd in match (emits_labels ??);
-  
-  inversion l [#fn #lbl | * [|#lbl] | * [|#lbl] ] #EQlbl normalize nodelta
-  inversion (R_post_step ???) [|2,4,6,8,10,12,14,16: * #post_lbl #post_state]
-  #EQR_post_step normalize nodelta lapply (IH ter) -IH
-  >EQR_post_step normalize nodelta #IH
-  whd in match (foldl ?????);
-  [ >act_op @IH
-  try (> act_op)
-
-
-
-
-
-
-  whd in ⊢ (??%% → ?); [ >H1 in ⊢ (% → ?); | >H1 in ⊢ (% → ?); | >H1 in ⊢ (% → ?);]
-  normalize nodelta lapply(vm_step_to_eval … H2) whd in match eval_vmstate;
-  normalize nodelta #H cases(bind_inversion ????? H) -H * normalize nodelta
-  [1,7,13: #seq * [2,4,6: #lbl1]
-  |2,8,14: #newpc
-  |3,9,15: #cond #newpc #ltrue #lfalse
-  |4,10,16: #lin #io #lout
-  |5,11,17: #f
-  |*:
-  ] * normalize nodelta #EQfetch 
-  [13,14,15: whd in s1_noio : (?(??%?)); >EQfetch in s1_noio; 
-    normalize nodelta cases(asm_is_io ???) normalize nodelta
-    [1,3,5: * #H @⊥ @H % ] #_
-  |*: cases(asm_is_io ???) normalize nodelta
-     [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35:
-        whd in ⊢ (??%% → ?); #EQ destruct]
-  [13    
-    
-     #i * #EQi #H cases(bind_inversion ????? H) -H #el
-    inversion H4
-    [ #s1 #s2 #i1 * [| #lbl] #EQfetch #no_io #EQstore #EQstack #EQio #EQpc
-      #EQcost #EQ1 #EQ2 #EQ3 #EQ4 destruct >EQi in EQfetch; whd in ⊢ (??%% → ?);
-      #EQ destruct whd in match emits_labels; normalize nodelta
-      [ cases H1 whd in ⊢ (% → ?); [ * |  #EQ destruct]]
-      * whd in ⊢ (??%% → ?); #EQ destruct >neutral whd in ⊢ (??%% → ?);
-      #EQ destruct whd in match (foldr ?????);
-
-
-
-
+  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
+  inversion(emits_labels ??)
+  [ #EQemits whd in ⊢ (??%% → ?); #EQ destruct  >big_op_associative >act_op @IH
+  | #f #EQemits normalize nodelta #H
+    cases(bind_inversion ????? H) -H #k' * #EQk' whd in ⊢ (??%% → ?);
+    #EQ destruct(EQ) >act_op whd in match (append ???); @IH
+  ]
+  [1,5: inversion H in ⊢ ?; 
+    [1,6: #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct
+    |2,7: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #opt_l #EQ destruct #pre_tl1 #_
+      #EQ1 #EQ2 #EQ3 #EQ4 destruct
+    |3,8: #s1 #s2 #s3 #lbl #s1_noio #exe #tl1 * #lbl1 #EQ destruct #pre_tl1 #_
+      #EQ1 #EQ2 #EQ3 #EQ4 destruct
+    |4,9: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #f * #lbl1 #EQ destruct
+      * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
+    |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
+  | >neutral_r  @(instr_map_ok … good … EQi … good_a1) /2/
+  | %
+  | >(proj2 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits))
+    >(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.
+
+
+
+