Changeset 3535

Timestamp:

Mar 16, 2015, 4:30:28 PM (5 years ago)

Author:

piccolo

Message:

final statement of cerco with the first pass integrated in place

Location:

LTS

Files:

• Final.ma (modified) (3 diffs)
• Lang_meas.ma (added)
• Language.ma (modified) (18 diffs)
• Traces.ma (modified) (3 diffs)
• Vm.ma (modified) (9 diffs)
• costs.ma (modified) (1 diff)

LTS/Final.ma

@@ -14 +14 @@
 
 include "Simulation.ma".
-include "Vm.ma".   
+include "Vm.ma". 
+include "Lang_meas.ma". 
 
 theorem cerco:
@@ -76 +77 @@
 #S1 #p #p' #prog letin S2 ≝ (asm_operational_semantics ???) #rel #sim_conds
 #R #mT #map #EQmap #si #s1 #s2 #sn #t #Hmeas #si' #Hclass #Rsisi'
-cases (simulates_measurable … sim_conds … Hmeas … Hclass Rsisi')
+cases (simulates_measurable S1 S2 rel sim_conds … Hmeas … Rsisi') 
+[2: #H cases Hclass >H #ABS cases(ABS (refl …)) ]
 #sn' * #t' ** #Rsnsn' #EQcostlabs * #s1' * #s2' #Hmeas'
 %{sn'} %{t'} %{Rsnsn'} %{EQcostlabs} %{s1'} %{s2'} %{Hmeas'} #acts #EQacts
@@ -83 +85 @@
 qed.  
 
+lemma is_permutation_mem : ∀A :DeqSet.
+∀l1,l2 : list A.∀x : A.mem … x l1 →
+is_permutation A l1 l2 → mem … x l2.
+cases daemon
+qed.
+
+definition is_abelian ≝ λM : monoid.
+∀x,y : M.op … M x y = op … M y x.
+
+lemma action_on_permutation : ∀M : abstract_transition_sys.is_abelian (abs_instr M) → 
+∀l1,l2 : list (abs_instr M).∀a.is_permutation … l1 l2 → 
+(〚l1〛 a) = (〚l2〛 a).
+cases daemon
+qed.
+
+lemma is_permutation_dependent_map : ∀A,B : DeqSet.∀l1,l2 : list A.
+∀f : (∀a : A.mem … a l1 → B).∀g : (∀a : A.mem … a l2 → B).
+∀perm : is_permutation A l1 l2.
+(∀a : A.
+ ∀prf : mem … a l1.f a prf = g a ?) → 
+is_permutation B (dependent_map … l1 f) (dependent_map … l2 g).
+[2: @(is_permutation_mem … perm) //]
+cases daemon
+qed.
+
+theorem final_cerco : 
+(* for all programs in the imperative language (possibly with call non post labelled) *)
+∀p,p',prog.
+no_duplicates_labels … prog → 
+
+(* let t_prog be the same program in which all calls are post-labelled *)
+let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
+
+(* Let S1 be the operational semantics of the source code  *)
+let S1 ≝ operational_semantics p p' prog in 
+
+(* Let S2 be the operational semantics of the soource code with call post labelled  *)
+let S2 ≝ operational_semantics p p' t_prog in
+
+(* for all assmbler programs *)
+∀p_asm,p_asm',prog_asm.
+(* Let S3 be the operational semantics of the compiled code  *)
+let S3 ≝ asm_operational_semantics p_asm p_asm' prog_asm in
+
+(* If the simulation conditions between the source with call post-labelled and compiled
+    code holds (i.e. if the compiler is correct after the first pass) *)
+∀rel: relations S2 S3. simulation_conditions … rel →
+
+(* let REL be semantical relation between the states of the source program and
+   the states of compiled code *)
+let REL ≝ λsi : S1.λsi' : S3.∃si'' : S2.∃abs_top,abs_tail.state_rel … m keep abs_top abs_tail si si'' ∧
+Srel … rel si'' si' in
+
+ (* Given an abstract interpretation framework for the compiled code *)
+∀R: asm_abstract_interpretation p_asm p_asm' prog_asm.
+
+(* If the abstract instructions monoid is abelian *)
+is_abelian (abs_instr … (aabs_d … (asm_galois_conn … R))) →  
+ 
+ (* If the static analysis does not fail *)
+∀mT,map1. ∀EQmap : static_analisys … (instr_map … R) mT prog_asm = return map1.
+
+ (* For every source trace whose measurable fragment starts in s1 and ends in s2 or,
+   equivalently, whose state after the initial labelled transition is s1 
+   and whose state after the final labelled transition is s2  *)
+ ∀si,s1,s2,sn. ∀t: raw_trace S1 … si sn.
+ measurable … s1 s2 … t →
+
+ (* For each target non I/O state si' in relation with the source state si *)
+ ∀si': S3. as_classify … si' ≠ cl_io → REL si si' →
+
+ (* There exists a corresponding target trace starting from si' *)
+ ∃sn'. ∃t': raw_trace … si' sn'.
+  REL sn sn' ∧ 
+  
+   (* Let labels be the costlabels observed in the trace of the source with all call post-labelled 
+     (last one excluded), that can be computed from the costlabels observed in the trace of
+     the source language *)
+ let labels ≝ map_labels_on_trace … m … (chop … (get_costlabels_of_trace …  t)) in
+  
+  (*The labels emitted by the trace of the source with all call post-labelled 
+    is a permutation of the labels emitted by the target trace (excluded the last one) *)
+  ∃perm:is_permutation … labels (chop … (get_costlabels_of_trace … t')).
+ 
+ (* that has a measurable fragment starting in s1' and ending in s2' *)
+ ∃s1',s2'. measurable … s1' s2' … t' ∧
+
+(* Let abs_actions be the list of statically computed abstract actions
+   associated to each label in labels. *)
+ ∀abs_actions.
+  abs_actions =
+   dependent_map … labels (λlbl,prf.(opt_safe … (get_map … map1 lbl) …)) →
+
+ (* Given an abstract state in relation with the first state of the measurable
+    fragment *)
+ ∀a1.R s1' a1 →
+
+ (* The final state of the measurable fragment is in relation with the one
+   obtained by applying every semantics in abs_trace. *)
+ R s2' (〚abs_actions〛 a1).
+[2: @hide_prf normalize nodelta in prf; change with labels in prf : (???%);
+    lapply(is_permutation_mem … prf … perm) -prf #prf
+    cases(mem_map ????? (labels_of_trace_are_in_code … (chop_mem … prf))) *
+    #lbl' #pc * #Hmem #EQ destruct
+    >(proj1 … (static_analisys_ok … EQmap … Hmem))
+    @(proj2 … (static_analisys_ok … EQmap … Hmem))
+]
+#p #p' #prog #no_dup @pair_elim * #t_prog #m #keep #EQt_prog normalize nodelta
+#p_asm #p_asm' #prog_asm #rel #sim_cond #R #abelian #mT #map #EQmap #si #s1 #s2 #sn
+#t #meas_t #si' #Hclass * #si'' * #abs_top * #abs_tail * #Rsi_si'' #Rsi_si'
+lapply(correctness_theorem … p' prog no_dup) >EQt_prog normalize nodelta
+#H cases(H … meas_t … Rsi_si'') -H #abs_top' * #abs_tail' * #sn'' * #t'' ** #Rsn_sn''
+#Hperm * #s1'' * #s2'' #meas_t''
+cases(cerco … sim_cond … EQmap … meas_t'' … Rsi_si') //
+#sn' * #t' * #Rsn_sn' * #EQcost * #s1' * #s2' * #meas_t' normalize nodelta #Hcerco
+%{sn'} %{t'} %
+[ %{sn''} %{abs_top'} %{abs_tail'} /2 by conj/ ] %
+ [ @(is_permutation_transitive … Hperm) >EQcost // ]
+ %{s1'} %{s2'} %{meas_t'} #abs_actions #EQactions #a1 #Rs1_a1
+ >(action_on_permutation … abelian)
+ [@Hcerco [% | assumption]
+ | >EQactions -EQactions @is_permutation_dependent_map //
+ |
+ ]
+qed.
+
 (* TODO:
-1. Monoide di costo: eliminare.
-2. Discorso I/O, fallimento della block-cost, ipotesi di premisurabilita'
-   sull'assembler
+1. Spostare chop e eliminare suffix.
+2. La block cost non fallisce in caso di I/O.
 3. Integrare la prima passata di Language nel risultato finale
 5. Cambi al control flow: Paolo's trick (label = coppia label-pezzo di stato)

LTS/Language.ma

@@ -1959 +1959 @@
           ] |1,4:]
     %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
-    ]
-  |*: cases daemon
-  ] cases daemon
-qed.
-
-(*
   |
    #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12
@@ -2012 +2006 @@
         >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta
         >EQi'' normalize nodelta % // % // % // % [2: assumption ] % // % // 
-    ] #abs_top1 * #s2' * #t' **** #Hst3_s2' #EQcost #EQlen
-      #stack_safety #pre_t' %{abs_top1}
+    ] #abs_top1 * #s2' * #t' ***** #Hst3_s2' #EQcost #EQlen
+      #stack_safety #pre_t' #Hsil %{abs_top1}
     %{s2'} %{(t_ind … t')}
     [ @hide_prf @(cond_true … EQcode_s1') //
     |
-    ]
+    ] % [ 
     % [ % 
     [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'} 
@@ -2030 +2024 @@
     ]]
     %2 // [2: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
+    ]
+    #h inversion h in ⊢ ?; 
+    [#H1 #H2 #H3 #H4 #H5 #H6 destruct 
+    | #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 destruct
+    ]
   | #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12
     #EQ1 #EQ2 destruct(EQ1 EQ2) #EQio_st11 #EQio_st12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t
@@ -2075 +2074 @@
         >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta
         >EQi'' normalize nodelta % // % // % // % [2: assumption ] % // % // 
-    ] #abs_top1 * #s2' * #t' **** #Hst3_s2' #EQcost #EQlen #stack_safety
-    #pre_t' 
+    ] #abs_top1 * #s2' * #t' ***** #Hst3_s2' #EQcost #EQlen #stack_safety
+    #pre_t' #Hsil
     %{abs_top1} %{s2'} %{(t_ind … t')}
     [ @hide_prf @(cond_false … EQcode_s1') //
     |
-    ]
+    ] % [
     % [ % 
     [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'} 
@@ -2092 +2091 @@
       %{tl1} % // whd in EQk1 : (??%%); destruct //
     ] ]
-    %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
+    %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct ]
+    #h inversion h in ⊢ ?;
+    [ #H21 #H22 #H23 #H24 #H25 #H26 destruct
+    | #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 destruct
+    ]
  | #cond #ltrue #i_true #lfalse #i_false #store #EQcode_st11 #EQev_loop #EQcont_st12 #EQ1 #EQ2 destruct
    #EQio_11 #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass11 #_ #Hpre #IH #s1' #abs_top #abs_tail
@@ -2140 +2143 @@
        % //
    ]
-   #abs_cont1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
-   #pre_t' %{abs_cont1} %{s2'} %{(t_ind … t')}
-   [ @hide_prf @(loop_true … EQcode_s1') // |]
+   #abs_cont1 * #s2' * #t' ***** #Hst3_s2' #EQcosts #EQlen #stack_safety
+   #pre_t' #Hsil %{abs_cont1} %{s2'} %{(t_ind … t')}
+   [ @hide_prf @(loop_true … EQcode_s1') // |] % [
    % [ %
    [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'}
@@ -2154 +2157 @@
       %{tl1} % // whd in EQk1 : (??%%); destruct //
    ] ]
-   %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
+   %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct ]
+   #h inversion h in ⊢ ?;
+   [ #H41 #H42 #H43 #H44 #H45 #H46 destruct
+   | #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 destruct
+   ]
  | #cond #ltrue #i_true #lfalse #i_false #mem #EQcode_st11 #EQev_loop #EQcont_st12 #EQ1 #EQstore11 destruct
    #EQio_11 #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass11 #_ #Hpre #IH #s1' #abs_top #abs_tail
@@ -2200 +2207 @@
         % // % // % // % [2: %] //
    ]
-   #abs_cont1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety 
-   #pre_t' %{abs_cont1} %{s2'} %{(t_ind … t')}
-   [ @hide_prf @(loop_false … EQcode_s1') // |]
+   #abs_cont1 * #s2' * #t' ***** #Hst3_s2' #EQcosts #EQlen #stack_safety 
+   #pre_t' #Hsil %{abs_cont1} %{s2'} %{(t_ind … t')}
+   [ @hide_prf @(loop_false … EQcode_s1') // |] % [
    % [ %
    [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'}
@@ -2211 +2218 @@
      cases(stack_safety … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % //
    ]]
-   %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
+   %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct]
+   #h inversion h in ⊢ ?;
+   [ #H61 #H62 #H63 #H64 #H65 #H66 destruct
+   | #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 destruct
+   ]
  | #lin #io #lout #i #mem #EQcode_st11 #EQev_io #EQcost_st12 #EQcont_st12
    #EQ destruct #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass_11 #_ #Hpre
@@ -2257 +2268 @@
        [2: >EQcost_st12 % ] % [ % // % //] >(\P EQget_lout1) %
    ]
-   #abs_cont1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety 
-   #pre_t' %{abs_cont1} %{s2'} %{(t_ind … t')}
-   [ @hide_prf @(io_in … EQcode_s1') // |]
+   #abs_cont1 * #s2' * #t' ***** #Hst3_s2' #EQcosts #EQlen #stack_safety 
+   #pre_t' #Hsil %{abs_cont1} %{s2'} %{(t_ind … t')}
+   [ @hide_prf @(io_in … EQcode_s1') // |] % [
    % [ % 
    [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'}
@@ -2271 +2282 @@
       %{tl1} % // whd in EQk1 : (??%%); destruct //
    ]]
-   %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
+   %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct ]
+   #h inversion h in ⊢ ?;
+   [ #H81 #H82 #H83 #H84 #H85 #H86 destruct
+   | #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 #H99 destruct
+   ]
   | #f #act_p #r_lb #cd #mem #env_it #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10
     #EQ11 #EQ12 destruct #tl #_ * #x #EQ destruct(EQ)
@@ -2341 +2356 @@
    #r_t' #EQcode_s1' 
   whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) 
-  #EQstore11 #EQio_11 #EQ destruct
+  #EQstore11 #EQio_111 #EQ destruct
   cases(IH … (mk_state ? i cont_s1'' (store … st12) (io_info … st12)) abs_tail_cont gen_labs) 
   [2: whd >EQcheck normalize nodelta % // % // % // % // @EQi' ] 
-  #abs_top1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
-  #pre_t' %{abs_top1} %{s2'} %{(t_ind … t')}
+  #abs_top1 * #s2' * #t' ***** #Hst3_s2' #EQcosts #EQlen #stack_safety
+  #pre_t' #Hsil %{abs_top1} %{s2'} %{(t_ind … t')}
   [ @hide_prf @(ret_instr … EQcode_s1' … EQcont_s1') //
-  | ]
+  | ] % [
   % [ %
   [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'} 
@@ -2360 +2375 @@
     % [ >EQk1 % | whd in ⊢ (??%%); @eq_f // ]
   ]]
-  %3 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
+  %3 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct ]
+  #h inversion h in ⊢ ?; 
+  [ #H101 #H102 #H103 #H104 #H105 #H106 destruct
+  | #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 destruct
+  ]
 | #st1 #st2 #st3 #lab #H inversion H in ⊢ ?; #st11 #st12
   [1,2,3,4,5,6,7,9:
@@ -2437 +2456 @@
             ]
           ]
-          #abs_top''' * #st3' * #t' **** #Hst3st3' #EQcosts #EQlen #stack_safety 
-          #pre_t' %{abs_top'''}
+          #abs_top''' * #st3' * #t' ***** #Hst3st3' #EQcosts #EQlen #stack_safety 
+          #pre_t' #Hsil %{abs_top'''}
           %{st3'} %{(t_ind … (call_act f (f_lab … env_it')) …  t')}
-          [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ] 
+          [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ] % [ 
           % [ %
           [ % [2: whd in ⊢ (??%%); >EQlen %]
@@ -2455 +2474 @@
           ]]
           %4 // [2,4: % [2: % // |]] normalize >EQcode_st1' normalize nodelta % #EQ destruct
+          ]
+          #h inversion h in ⊢ ?;
+          [ #H121 #H122 #H123 #H124 #H125 #H126 destruct 
+          | #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 #H138 #H139 destruct
+          ]
         | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
         ]
@@ -2556 +2580 @@
           ]
      ]
-     #abs_top''' * #st41' * #t1' **** #Hst41st41' #EQcosts #EQlen #stack_safety1
-     #pre_t1'
+     #abs_top''' * #st41' * #t1' ***** #Hst41st41' #EQcosts #EQlen #stack_safety1
+     #pre_t1' #Hsil1
      whd in Hst41st41'; inversion(check_continuations …) in Hst41st41'; [ #_ * ]
      ** #H2 #abs_top_cont' #abs_tail_cont' >EQcont41 in ⊢ (% → ?); 
@@ -2620 +2644 @@
              abs_tail_cont abs_top'''')
      [2: whd >EQ_contst42 normalize nodelta % // % // % // % // @EQi' ]
-     #abs_top_1 * #st5' * #t2' **** #Hst5_st5' #EQcosts' 
-     #EQlen'  #stack_safety2 #pre_t2' %{abs_top_1} %{st5'} %{(t_ind … (t1' @ (t_ind … t2')))}
+     #abs_top_1 * #st5' * #t2' ***** #Hst5_st5' #EQcosts' 
+     #EQlen'  #stack_safety2 #pre_t2' #Hsil2 %{abs_top_1} %{st5'} %{(t_ind … (t1' @ (t_ind … t2')))}
      [3: @hide_prf @(call …  EQcode_st1' …  EQenv_it') //
      |1: @hide_prf @(ret_instr … EQcode_st41' … EQcont_st41') //
      |2,4: skip
-     ] 
+     ] % [
      % [ % 
      [ % [2: whd in ⊢ (??%%); @eq_f >len_append >len_append @eq_f2 //
@@ -2653 +2677 @@
        ]
      ]
-]
-qed.
-
-*)
+  ] #h inversion h in ⊢ ?;
+  [ #H141 #H142 #H143 #H144 #H145 #H146 destruct
+  |#H148 #H149 #H150 #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 destruct
+  ]
+]  
+qed.
+
 
 lemma silent_in_silent : ∀p,p',prog.

LTS/Traces.ma

@@ -274 +274 @@
 λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1.
 
-let rec get_costlabels_of_trace (S : abstract_status) (st1 : S) (st2 : S)
-(t : raw_trace S st1 st2) on t : list CostLabel ≝ 
-match t with
-[ t_base st ⇒ [ ]
-| t_ind st1' st2' st3' l prf t' ⇒ 
-    let tl ≝ get_costlabels_of_trace … t' in
-    match l with
+definition actionlabel_to_costlabel ≝ 
+λl : ActionLabel.match l with
     [ call_act f c ⇒ [ c ]
     | ret_act x ⇒ match x with 
@@ -290 +285 @@
                   | None ⇒ [] 
                   ]
-   ] @ tl
+   ].
+
+let rec get_costlabels_of_trace (S : abstract_status) (st1 : S) (st2 : S)
+(t : raw_trace S st1 st2) on t : list CostLabel ≝ 
+match t with
+[ t_base st ⇒ [ ]
+| t_ind st1' st2' st3' l prf t' ⇒ 
+    let tl ≝ get_costlabels_of_trace … t' in
+    actionlabel_to_costlabel l  @ tl
 ].
 
@@ -636 +639 @@
 
 definition measurable :
- ∀S: abstract_status. ∀si,s1,s3,sn : S. raw_trace … si sn → Prop ≝
+ ∀S: abstract_status. ∀si,s1,s3,sn : S. raw_trace … si sn →  Prop ≝
 λS,si,s1,s3,sn,t.
  ∃s0,s2:S. ∃ti0 : raw_trace … si s0.∃t12 : raw_trace … s1 s2.∃t3n : raw_trace … s3 sn.

LTS/Vm.ma

@@ -685 +685 @@
 definition terminated_trace : ∀S : abstract_status.∀s1,s3 : S.raw_trace … s1 s3 → Prop ≝ 
 λS,s1,s3,t.∃s2: S.∃t1 : raw_trace … s1 s2.∃ l,prf.t = t1 @ (t_ind ? s2 s3 s3 l prf … (t_base … s3))
-∧ is_costlabelled_act l. 
+∧ is_costlabelled_act l ∧ pre_measurable_trace … t1. 
 
 definition big_op: ∀M: monoid. list M → M ≝
@@ -821 +821 @@
       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 *
+      [ #EQemit cases(step_emit … (vm_step_to_eval … H2)) // #x * #EQ1 #EQ2 whd in match actionlabel_to_costlabel;
+        normalize nodelta >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))
+      | #f #EQemit whd in match actionlabel_to_costlabel; normalize nodelta 
+        >(proj1 … (step_non_emit … EQi (vm_step_to_eval … H2) … EQemit))
         *
       ]
@@ -882 +884 @@
 qed.
 
+(*
 definition actionlabel_to_costlabel : ActionLabel → list CostLabel ≝
 λa.match a with
@@ -888 +891 @@
 | cost_act opt_l ⇒ match opt_l with [None ⇒ [ ] | Some l ⇒ [a_non_functional_label l]]
 ].
+*)
 
 lemma get_cost_label_of_trace_tind : ∀S : abstract_status.
@@ -922 +926 @@
 (* For every pre_measurable, terminated trace *)
 ∀st1,st2. ∀t: raw_trace (asm_operational_semantics … prog) … st1 st2.
- terminated_trace … t → pre_measurable_trace … t → 
+ terminated_trace … t →
 
 (* Let labels be the costlabels observed in the trace (last one excluded) *)
@@ -951 +955 @@
 ]
 #p #p' #prog #R #mT #map1 #EQmap #st1 #st2 #t * #st3 * #t1 *
-#l1 * #prf1 * #EQ destruct #Hlabelled
+#l1 * #prf1 ** #EQ destruct #Hlabelled
 >(rewrite_in_dependent_map ??? (get_costlabels_of_trace … t1))
 [2: >get_cost_label_append  >get_cost_label_of_trace_tind >append_nil cases(actionlabel_ok … Hlabelled)
@@ -1200 +1204 @@
 ]
 #p #p' #prog #R #mT #map1 #EQmap #si #s1 #s2 #sn #t #measurable
-cases measurable #premeas * #s0 * #s3 * #ti0 * #t12 * #t3n *  #l1 * #l2 * #prf1 * #prf2 
-***** #EQ destruct #Hl1 #Hl2 #_ #silent_ti0 #silent_t3n #acts cases(actionlabel_ok … Hl1)
+cases measurable #s0 * #s3 * #ti0 * #t13 * #t2n* #l1 * #l2 * #prf1 * #prf2
+******* #pre_t13 #EQ destruct #Hl1 #Hl2 #Hcall_l2 #sil_ti0 #sil_t2n #Hcall_l1
+#acts cases(actionlabel_ok … Hl1)
 #c1 #EQc1 >rewrite_in_dependent_map
-[2: >get_cost_label_append in ⊢ (??%?); >(get_cost_label_silent_is_empty … silent_ti0) in ⊢ (??%?);
+[2: >get_cost_label_append in ⊢ (??%?); >(get_cost_label_silent_is_empty … sil_ti0) in ⊢ (??%?);
      >get_cost_label_of_trace_tind in ⊢ (??%?); >get_cost_label_append in ⊢ (??%?);
       >get_cost_label_of_trace_tind in ⊢ (??%?);
-     >(get_cost_label_silent_is_empty … silent_t3n) in ⊢ (??%?);
+     >(get_cost_label_silent_is_empty … sil_t2n) in ⊢ (??%?);
      >append_nil in ⊢ (??%?); >EQc1 in ⊢ (??%?); whd in ⊢ (??(??%)?);
      whd in ⊢ (??(??(???%))?); >chop_cons in ⊢ (??%?); 
@@ -1215 +1220 @@
  >(big_op_associative ? [?]) #a1 >act_op #HR
 letin actsl ≝ (dependent_map ????);
-@(static_dynamic_inv … EQmap … (t12 @ t_ind … prf2 (t_base …)) … actsl … HR)
-  [ /6 width=6 by conj, ex_intro/
-  | lapply(sub_trace_premeasurable_l2 … premeas) 
+@(static_dynamic_inv … EQmap … (t13 @ (t_ind … prf2 (t_base …))) … HR)
+  [ /7 width=6 by conj, ex_intro/
+  (*| lapply(sub_trace_premeasurable_l2 … pre_t13) 
     change with ((t_base ? s1) @ t12) in match t12 in ⊢ (% → ?);
     change with ((t_ind ???????)@(t_ind ???????)) in ⊢ (????% → ?);
@@ -1224 +1229 @@
     change with ((t_base ??)@?) in ⊢ (????(??????(???????%)) → ?);
     change with ((t_ind ???????)@?) in ⊢ (????(??????%) → ?);
-    <append_associative #H @(sub_trace_premeasurable_l1 … H) 
-  | cases s1 in prf1 t12; [3: #st1] cases s0 [3,6,9: #st0] *
+    <append_associative #H @(sub_trace_premeasurable_l1 … H) *)
+  | cases s1 in prf1 t13; [3: #st1] cases s0 [3,6,9: #st0] *
     [2: #H #EQ lapply(refl ? (FINAL p p')) generalize in match (FINAL p p') in ⊢ (??%? → %);
         #st' #EQst' #tr lapply prf2 lapply EQst' -EQst' cases tr

LTS/costs.ma

@@ -16 +16 @@
 
 record monoid: Type[1] ≝
- { carrier :> Type[0]
+ { carrier :> DeqSet
  ; op: carrier → carrier → carrier
  ; e: carrier