Changeset 3478 for LTS

Timestamp:

Sep 22, 2014, 4:50:21 PM (6 years ago)

Author:

piccolo

Message:

fixed costlabels

Location:

LTS

Files:

• DICE2014/slides.tex (modified) (8 diffs)
• Language.ma (modified) (2 diffs)
• Simulation.ma (modified) (14 diffs)
• Traces.ma (modified) (5 diffs)
• Vm.ma (modified) (11 diffs)

LTS/DICE2014/slides.tex

@@ -21 +21 @@
 ]{powerdot}
 %\documentclass[mode=handout,nopagebreaks,paper=a4paper]{powerdot}
-
+\usepackage{multirow}
 %\usepackage[latin1]{inputenc}
 \usepackage{pstricks,pst-node,pst-text,pst-tree}
@@ -217 +217 @@
 $\;$\\[-9mm]
 \begin{center}
-\includegraphics[width=7cm]{cerco.eps}
+\includegraphics[width=6cm]{cerco.eps}
 \end{center}
 This talk:
@@ -223 +223 @@
 \begin{minipage}{12cm}
 \begin{itemize}
-\item There are some hidden assumption and limitations of labelling approach: {\red instructions with multiple predecessors} and {\red function calls}.
-\item We present a {\red revisitation of labelling approach} able to cope the above mentioned limitations.
-\item All the presented results have been formalized in the {\red Matita proof assistant}.
+\item We revise the labelling approach to lift some restriction: {\red instructions having only one predecessor} and {\red absence of function calls}.
+\item We replace simple status independent costs with arbitrary semantics domains used in {\red abstract interpretation} to analyze caches, pipelines,$\ldots$.
+\item All the presented results are formalized in the {\red Matita proof assistant}.
 \end{itemize}
 \end{minipage}
@@ -279 +279 @@
 \item No more label emission statements.
 \end{itemize}
-\begin{lstlisting}[language=Grafite]
-record abstract_status : Type[2] ≝ 
- { as_status :> Type[0]
- ; as_execute : ActionLabel → relation as_status
- ; as_syntactical_succ : relation as_status
- ; as_classify : as_status → status_class
- ; as_initial : as_status → bool
- ; as_final : as_status → bool
- ; jump_emits : ∀s1,s2,l.as_classify ... s1 = cl_jump → 
-      as_execute l s1 s2 → is_non_silent_cost_act l
- }.
-\end{lstlisting}
+\begin{center}
+\begin{tabular}{ll l}
+\begin{lstlisting}
+swith(E){
+  case e1 :
+  Emit L1;
+  I1;
+  case e2 :
+  Emit L2;
+  I2;
+}
+\end{lstlisting} &$\qquad$&
+\begin{lstlisting}
+swith(E){
+  case e1,L1 :
+
+  I1;
+  case L3,e2,L2 : //L3 emitted coming 
+                  // from case e1
+  I2;
+}
+\end{lstlisting}
+\end{tabular}
+\end{center}
+% \begin{lstlisting}[language=Grafite]
+% record abstract_status : Type[2] ≝ 
+%  { as_status :> Type[0]
+%  ; as_execute : ActionLabel → relation as_status
+%  ; as_syntactical_succ : relation as_status
+%  ; as_classify : as_status → status_class
+%  ; as_initial : as_status → bool
+%  ; as_final : as_status → bool
+%  ; jump_emits : ∀s1,s2,l.as_classify ... s1 = cl_jump → 
+%       as_execute l s1 s2 → is_non_silent_cost_act l
+%  }.
+% \end{lstlisting}
 \end{wideslide}
 
@@ -338 +362 @@
 \end{minipage}
 }\\[3mm]
+\onslide{2-}{
 {\red Assumptions:}
 \begin{itemize}
-\item All the instruction in the (static) block are reached during computation.
-\item The cost function should be commutative.
-\end{itemize}
+\item<2-> All the instruction in the (static) block are reached during computation.
+\item<2-> The cost function should be commutative.
+\end{itemize}
+}
+\onslide{3-}{
 {\red Problems:}
 \begin{itemize}
-\item It does not work with {\blue non-commutative cost functions}. Because of stateful hardware components (cache, pipelines ...) this method does not scale to {\blue modern hardware}.
-\item It does not work with {\blue compiler that do not respect the calling structure} of the source code because it is not possible to statically predict {\blue which instruction will be executed after a function return}.
-\end{itemize}
-\end{wideslide}
-
-\begin{wideslide}[method=direct]{First solution: structured traces}
+\item<3-> It does not work with {\blue non-commutative cost functions}. Because of stateful hardware components (cache, pipelines ...) this method does not scale to {\blue modern hardware}.
+\item<3-> It does not work with {\blue compiler that do not respect the calling structure} of the source code because it is not possible to statically predict {\blue which instruction will be executed after a function return}.
+\end{itemize}}
+\end{wideslide}
+
+\begin{wideslide}{First solution: structured traces}
+\onslide*{1}{
 \begin{itemize}
 \item The usual notion of {\red flat execution trace} is inadequate for a simulation argument.
@@ -356 +384 @@
 \item Traces of called function are {\red nested}, invariants on position of costlabels are {\red enforced} and steps are grouped {\red according to costlabels}.
 \end{itemize}
-\begin{center}
-\includegraphics[width=8cm]{trace.eps}
-\end{center}
-\end{wideslide}
-
-\begin{wideslide}[method=direct]{Measurable traces}
-$\;$\\[-7mm]
-\begin{lstlisting}[language=Grafite]
-inductive pre_measurable_trace (S : abstract_status) :
-∀st1,st2 : S.raw_trace ? st1 st2 → Prop ≝ 
-| pm_empty : ∀st : S. as_classify … st ≠ cl_io → pre_measurable_trace … (t_base… st)
-| pm_cons_cost_act : ∀st1,st2,st3 : S.∀l : ActionLabel.
-   ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
-   as_classify … st1 ≠ cl_io → is_cost_act l → pre_measurable_trace … tl → 
-   pre_measurable_trace … (t_ind … prf … tl)
-………  
-| pm_balanced_call : ∀st1,st2,st3,st4,st5.∀l1,l2.
-   ∀prf : as_execute S l1 st1 st2.∀t1 : raw_trace S st2 st3.
-   ∀t2 : raw_trace S st4 st5.∀prf' : as_execute S l2 st3 st4.
-   as_classify … st1 ≠ cl_io → as_classify … st3 ≠ cl_io 
-   →  is_call_act l1 → ¬ is_call_post_label … st1 → 
-   pre_measurable_trace … t1 → pre_measurable_trace … t2 → 
-   as_syntactical_succ S st1 st4 → 
-   is_unlabelled_ret_act l2 → 
-   pre_measurable_trace … (t_ind … prf … (t1 @ (t_ind … prf' … t2))).
-\end{lstlisting} 
-\end{wideslide}
-
-\begin{wideslide}[method=direct]{Simulation statement}
+}
+\onslide*{2-}{
+\begin{tabular}{l c}
+\onslide*{3,4,5}{\green}$\tt EMIT \; L_1$ &  \onslide*{2,3,4}{{\red Flat trace}} \onslide*{5}{{\red Structured trace}}\\
+\onslide*{3,4,5}{\green}$\tt I_1$ & \multirow{7}{*}{
+\onslide*{2,3,4}{
+\xymatrix{ \onslide*{3,4}{\green} \bullet \onslide*{1,2}{\ar[r]^{{\tt L_1}}} \onslide*{3,4}{\ar@[green][r]^{{\tt \green L_1}}} & \onslide*{3,4}{\green} \bullet \onslide*{1,2}{\ar[r]^{{\tt I_1}}} \onslide*{3,4}{\ar@[green][r]^{{\tt \green I_1}}} & \onslide*{3,4}{\green} \ldots \onslide*{1,2}{\ar[r]^{{\tt I_n}}} \onslide*{3,4}{\ar@[green][r]^{{\tt \green I_n}}} & \onslide*{3,4}{\green} \bullet \onslide*{1,2}{\ar[r]^{{\tt CALL}}} \onslide*{3,4}{\ar@[green][r]^{{\tt \green CALL}}} & \bullet \ar[r]^{{\tt J_1}} & \ldots \ar[r]^{{\tt RET}} & \onslide*{3,4}{\green} \bullet \onslide*{1,2}{\ar[r]^{{\tt I_{n+1}}}} \onslide*{3,4}{\ar@[green][r]^{{\tt \green I_{n+1}}}} & \onslide*{3,4}{\green} \ldots \onslide*{1,2}{\ar[r]^{{\tt I_m}}} \onslide*{3,4}{\ar@[green][r]^{{\tt \green I_m}}} & \onslide*{3,4}{\green} \bullet }
+}
+\onslide*{5}{
+\xymatrix{ & & & \bullet \ar[r]^{{\tt J_1}} & \black \ldots \ar[r] & \bullet \ar[d]^{{\tt RET}}\\
+\green \bullet \ar@[green][r]^{{\tt \green L_1}} & \green \bullet \ar@[green][r]^{{\tt \green I_1}} & \green \ldots \ar@[green][r]^{{\tt \green I_n}} & \green \bullet \ar@[green][u]^{{\tt \green CALL}}  & \triangleright & \green \bullet \ar@[green][r]^{{\tt \green I_{n+1}}} & \green \ldots \ar@[green][r]^{{\tt \green I_m}} & \green \bullet }
+}
+}\\
+\onslide*{3,4,5}{\green}$\vdots$ & \\
+\onslide*{3,4,5}{\green}$\tt I_n$ &  \\
+\onslide*{3,4,5}{\green}$\tt CALL$ & \\
+\onslide*{3,4,5}{\green}$\tt I_{n+1}$ & \\
+\onslide*{3,4,5}{\green}$\vdots$ & \\
+\onslide*{3,4,5}{\green}$\tt I_m$
+\end{tabular}
+}
+$\;$\\[3mm]
+\onslide*{4}{{\red What is the global invariant granting both that call/return are balanced and that we can statically predict the return address?}}
+
+% \onslide*{2}{
+% \xymatrix{a & b \\
+%           c & d}
+% }
+\end{wideslide}
+
+% \begin{wideslide}[method=direct]{Measurable traces}
+% $\;$\\[-7mm]
+% \begin{lstlisting}[language=Grafite]
+% inductive pre_measurable_trace (S : abstract_status) :
+% ∀st1,st2 : S.raw_trace ? st1 st2 → Prop ≝ 
+% | pm_empty : ∀st : S. as_classify … st ≠ cl_io → pre_measurable_trace … (t_base… st)
+% | pm_cons_cost_act : ∀st1,st2,st3 : S.∀l : ActionLabel.
+%    ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
+%    as_classify … st1 ≠ cl_io → is_cost_act l → pre_measurable_trace … tl → 
+%    pre_measurable_trace … (t_ind … prf … tl)
+% ………  
+% | pm_balanced_call : ∀st1,st2,st3,st4,st5.∀l1,l2.
+%    ∀prf : as_execute S l1 st1 st2.∀t1 : raw_trace S st2 st3.
+%    ∀t2 : raw_trace S st4 st5.∀prf' : as_execute S l2 st3 st4.
+%    as_classify … st1 ≠ cl_io → as_classify … st3 ≠ cl_io 
+%    →  is_call_act l1 → ¬ is_call_post_label … st1 → 
+%    pre_measurable_trace … t1 → pre_measurable_trace … t2 → 
+%    as_syntactical_succ S st1 st4 → 
+%    is_unlabelled_ret_act l2 → 
+%    pre_measurable_trace … (t_ind … prf … (t1 @ (t_ind … prf' … t2))).
+% \end{lstlisting} 
+% \end{wideslide}
+
+\begin{wideslide}[method=file]{Simulation statement}
 $\;$\\[-7mm]
 \begin{lstlisting}[language=Grafite]
@@ -392 +445 @@
 \end{lstlisting}
 \begin{itemize}
-\item Simulation conditions are local conditions for {\red sequential}, {\red conditional}, {\red call} and {\red return} steps.
-\begin{center}
+\item<2-> Simulation conditions are local conditions for {\red sequential}, {\red conditional}, {\red call} and {\red return} steps.
+\begin{center}
+\onslide*{2}{
+\xymatrix{st1 \ar[rr] \ar@{.}[d]|-{sim} & & st1' \ar@{.}[d]|-{sim} \\
+          st2 \ar[rr]^{*} & & st2'}}
+\onslide*{3-}{
 \includegraphics[width=5cm]{diag.eps}
-\end{center}
-\item The generated trace should contain {\red the same sequence of costlabels} (up to permutation) of the starting one.
+}
+\end{center}
+\item<4-> The generated trace should contain {\red the same sequence of costlabels} (up to permutation) of the starting one.
 \end{itemize}
 \end{wideslide}
@@ -409 +467 @@
 still requirred to be commutative.
 \end{itemize}
+\onslide{2-}{
 \psshadowbox{
 \begin{minipage}{12cm}
 We ask every function call to be immediately followed by a label emission statement so the scope of a label no longer extends after a function call.
 \end{minipage}
-}
+}}
 $\;$\\
+\onslide{3-}{
 {\red Drawbacks}
 \begin{itemize}
-\item A lot of labels should be injected in the code!
-\item The value of the variable $\tt cost$ at the end of a block containing function-calls is the sum of the increments that occurs after every call.
-\item A proof of termination is requirred!
-\end{itemize}
-\end{wideslide}
-
-\begin{wideslide}[method=direct]{Return post label pass}
-We define a {\blue sound and precise} translation to a program having all return instructions that are followed by a label emission.
-\begin{lstlisting}[language=Grafite]
-lemma correctness : ∀p,p',prog.no_duplicates_labels … prog → let 〈t_prog,m,keep〉 ≝ trans_prog … prog in ∀s1,s2,s1' : state p.∀abs_top,abs_tail.
-∀t : raw_trace (operational_semantics…p' prog) s1 s2.pre_measurable_trace…t → state_rel…m keep abs_top abs_tail s1 s1' → ∃abs_top',abs_tail'.∃s2'.
-∃t' : raw_trace (operational_semantics…p' t_prog) s1' s2'.
-state_rel…m keep abs_top' abs_tail' s2 s2' ∧ is_permutation …  ∧ len…t = len…t' ∧ pre_measurable_trace…t'.
-\end{lstlisting}
-\begin{itemize}
-\item {\blue Benefits}: the user can reason with smaller blocks and simpler costs and the compiler do not need to care about extra invariant.
-\item {\red Drawbacks}: This pass is not always possible in case of non commutative costs.
-\end{itemize}
-\end{wideslide}
-
-\begin{wideslide}[method=direct]{Static/dynamic correctness}
-\begin{lstlisting}[language=Grafite]
-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.∀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.
-∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2.
-∀k.pre_measurable_trace…t → 
-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
-∀costs.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)).
-\end{lstlisting}
-\end{wideslide}
+\item<3-> A lot of labels should be injected in the code!
+\item<3-> The value of the variable $\tt cost$ at the end of a block containing function-calls is the sum of the increments that occurs after every call.
+\item<3-> A proof of termination is requirred!
+\end{itemize}}
+\end{wideslide}
+
+\begin{wideslide}{Return post label pass}
+At the level of source code, we define a {\blue sound and precise} translation to a program having all return instructions that are followed by a label emission. \\[4mm]
+\begin{tabular}{l c l}
+\onslide*{1,2,3}{$\tt EMIT \; L;$}\onslide*{4}{$\tt cost += k_1 + k_2;$} & \multirow{7}{6cm}{\centering $\Rightarrow$} & \onslide*{2}{$\red \tt EMIT \; L1$}\onslide*{3-}{$\tt cost+=k_1;$} \\
+$\tt I_1;$ &                                   & \onslide{2-}{$\tt I_1;$} \\
+$\vdots$ &                                     & \onslide{2-}{$\vdots$} \\
+$\tt f();$ &                                   & \onslide{2-}{$\tt f();$} \\
+$\tt I_2;$ &                                   & \onslide*{2}{{\red $\tt EMIT \; L2;$}}\onslide*{3-}{$\tt cost+=k_2$;} \\
+$\vdots$ &                                     & \onslide{2-}{$\tt I_2;$} \\
+$\tt I_n;$ &                                   & \onslide{2-}{$\vdots$} \\ 
+           &                                   & \onslide{2-}{$\tt I_n$} 
+\end{tabular}
+\end{wideslide}
+
+
+\begin{wideslide}{Return post label pass}
+\begin{itemize}
+\item<1-> {\blue Benefits}: the user can reason with smaller blocks and simpler costs and the compiler do not need to care about extra invariant.
+\item<1-> {\red Drawbacks}: This pass is not always possible in case of non commutative costs.
+\end{itemize}
+To prove correctness it is necessary to define a state relation (being preserved during the translation) keeping track of the fresh labels created.\\[3mm]
+\onslide*{2-}{
+\begin{center}
+\psshadowbox{
+\begin{minipage}{6cm}
+{\red \centering About 3000 lines of Matita code!}
+\end{minipage}
+}
+\end{center}
+}
+\end{wideslide}
+
+\begin{wideslide}{Static analysis correctness}
+\onslide*{1}{
+\psshadowbox{
+\begin{minipage}{12cm}
+Static analysis of cost is {\red correct} when the actual cost of executing a block of instructions of the object code starting from a label (dynamic cost) is equal to the sum of the costs of each reached label of the trace computed by the static analyzer (static cost).
+\end{minipage}
+}}
+\onslide*{2-}{
+\begin{tabular}{l l}
+$\tt \onslide*{3-}{\red} EMIT \; L1$ & \multirow{7}{*}{\xymatrix{\onslide*{1,2,3}{\bullet} \onslide*{4-}{s_1} \onslide*{2-}{\ar[r]^{{\tt L_1}}} \onslide*{3-}{\ar@[red][r]^{{\tt \red L_1}}} & \onslide*{1,2,3}{\bullet} \onslide*{4-}{s_2} \onslide*{2}{\ar[r]} \onslide*{3-}{\ar@[red][r]^{{\tt \red I_1}}} & \onslide*{4-}{s_3} \onslide*{1,2,3}{\bullet} \onslide*{2}{\ar[r]} \onslide*{3-}{\ar@[red][r]^{{\tt \red I_2}}} & \onslide*{1,2,3}{\bullet} \onslide*{4-}{s_4} \onslide*{2}{\ar[r]} \onslide*{3-}{\ar@[red][r]^{{\tt \red COND}}} & \onslide*{1,2,3}{\bullet} \onslide*{4-}{s_5} \onslide*{2}{\ar[r]^{{\tt L_2}}} \onslide*{3-}{\ar@[blue][r]^{{\tt \blue L_2}}} & \onslide*{1,2,3}{\bullet} \onslide*{4-}{s_6} \onslide*{2}{\ar[r]} \onslide*{3-}{\ar@[blue][r]^{{\tt \blue I_3}}} & \onslide*{1,2,3}{\bullet} \onslide*{4-}{s_7} \onslide*{2}{\ar[r]} \onslide*{3-}{\ar@[blue][r]^{{\tt \blue I_4}}} & \onslide*{1,2,3}{\bullet} \onslide*{4-}{s_8}}}  \\ 
+$\tt \onslide*{3-}{\red} I_1$ & \\
+$\tt \onslide*{3-}{\red} I_2$ & \\
+$\tt \onslide*{3-}{\red} COND \; l1$ & \\
+$\tt \onslide*{3-}{\blue} EMIT \; L2$ & \\
+$\tt \onslide*{3-}{\blue} I_3$ & \\
+$\tt \onslide*{3-}{\blue} I_4$ & 
+\end{tabular}
+}
+$\;$\\[3mm]
+\onslide*{3}{
+$$\begin{array}{l l l}
+cost_{trace} &=& {\red k(I_1) + k(I_2) + k(COND)}+ {\blue k(I_3) + k(I_4)} \\
+       &=& {\red(k(I_1) + k(I_2) + k(COND))} + {\blue (k(I_3) + k(I_4))} \\
+       &=& {\red cost(L_1)} + {\blue cost(L_2)}
+\end{array} $$
+}
+\onslide*{4}{
+Lifting to cost dependent from the state
+\begin{itemize}
+\item The cost is a function from states to states which can be composed (the cost is incorporated in the state).
+\item To compute complexity, one is interested only on a part of the state
+\end{itemize}
+\begin{center}
+{\red Galois connection} between an abstract transition system and a concrete one.
+\end{center}
+}
+\onslide*{5}{
+Under the hypothesis that $s_1$ is in connection with the abstract state $a_1$ and $\den{-}$ is the function computing the cost of the instruction in the abstract state (i.e. an {\red action on the cost monoid}), we have
+$$
+\begin{array}{l l l}
+cost_{trace} &=& cost\_of({\blue \den{{\tt I_4}} (\den{{\tt I_3}}} ({\red \den{{\tt COND}}  (\den{{\tt I_2}} (\den{{\tt I_1}}} a_1))))) \\
+           &=& cost\_of(({\blue (\den{{\tt I_4}} \circ \den{{\tt I_3}})} \circ {\red (\den{{\tt COND}} \circ \den{{\tt I_2}} \circ \den{{\tt I_1}})}) a_1) \\
+           &=& cost\_of(({\blue cost(L_2)} \circ {\red cost(L_1)}) a_1)
+\end{array}
+$$
+}
+\end{wideslide}
+
 
 \begin{wideslide}{Conclusion}
-\begin{itemize}
-\item We present an improvement of the labelling approach for a precise resource analisys of the source code.
-\item We extend labelling approach to cope hidden assumptions on conditional instructions and function calls.
-\item We are able (almost always) to deal with non commutative costs.
-\item The usual assumption that compilation preserves the structure of basic blocks is still present.
+Improvement of the labelling approach.
+\begin{itemize}
+\item Function calls.
+\item Instructions with multiple predecessors (e.g. switch, goto $\ldots$).
+\item Costs for stateful hardware (e.g. cache, pipelines $\ldots$).
+\item From lifting of costs ($\mathbb{N}$)
+ to lifting of abstract interpretation ($\mathcal{A} \to \mathcal{A}$).
 \end{itemize}
 Future works
 \begin{itemize}
 \item Abandoning SOS semantics.
-\item We would like to extend our framework to compilation process that does not preserve basic block structure as in [Tranquilli13QPLAS].
+\item We would like to extend our framework to compilation process that does not preserve basic block structure as in [Tranquilli13].
 \end{itemize}
 \end{wideslide}

LTS/Language.ma

@@ -926 +926 @@
 lemma fresh_keep_n_ok : ∀n,m,l.
 is_fresh_for_return l n → n ≤ m → is_fresh_for_return l m.
-#n #m #l lapply n -n lapply m -m elim l // ** #x #xs #IH #n #m
+#n #m #l lapply n -n lapply m -m elim l // * 
+[1,2,3: * #x] #xs #IH #n #m
 normalize [2: * #H1] #H2 #H3 [ %] /2 by transitive_le/
 qed.
@@ -1355 +1356 @@
 lemma fresh_for_subset : ∀l1,l2,n.l1 ⊆ l2 → is_fresh_for_return … l2 n → 
 is_fresh_for_return … l1 n.
-#l1 elim l1 // ** #x #xs #IH #l2 #n * #H1 #H2 #H3 whd
+#l1 elim l1 // * [1,2,3: * #x] #xs #IH #l2 #n * #H1 #H2 #H3 whd
 try(@IH) // % [2: @IH //] elim l2 in H1 H3; normalize [*]
-** #y #ys #IH normalize 
+* [1,2,3: * #y] #ys #IH normalize 
 [2,3: * [2,4: #H3 [2: @IH //] * #H4 #H5 @IH //
 |*: #EQ destruct * //
 ]]
 *
-[ #EQ destruct ] #H3 #H4 @IH //
+[1,3: #EQ destruct ] #H3 #H4 @IH //
 qed.
 
 lemma fresh_append : ∀n,l1,l2.is_fresh_for_return l1 n → is_fresh_for_return l2 n → 
 is_fresh_for_return (l1@l2) n.
-#n #l1 lapply n -n elim l1 // ** #x #xs #IH #n #l2 [2: * #H1 ] #H2 #H3 
+#n #l1 lapply n -n elim l1 // * [1,2,3: * #x] #xs #IH #n #l2 [2: * #H1 ] #H2 #H3 
 [ % // @IH //] @IH //
 qed.

LTS/Simulation.ma

@@ -110 +110 @@
                   | None ⇒ [] 
                   ]
-    | init_act ⇒ []
-    ] @ tl
+
+   ] @ tl
 ].
 
@@ -240 +240 @@
  append … (get_costlabels_of_trace … t1) (get_costlabels_of_trace … t2).
 #S #st1 #st2 #st3 #t1 elim t1 [ #st #t2 % ] #st1' #st2' #st3' *
-[#f * #l | * [| * #l] | *  [| #l] |] #prf #tl #IH #t2 normalize try @eq_f @IH
+[#f * #l | * [| * #l] | *  [| #l] ] #prf #tl #IH #t2 normalize try @eq_f @IH
 qed.
  
@@ -402 +402 @@
 
 record measurable_trace (S : abstract_status) : Type[0] ≝
- { L_label: ActionLabel
+ { L_label: option ActionLabel
  ; R_label : option ActionLabel 
  ; L_pre_state : option S
@@ -411 +411 @@
  ; pre_meas : pre_measurable_trace … trace
  ; L_init_ok : match L_pre_state with
-               [ None ⇒ bool_to_Prop(as_initial … L_s1) ∧ L_label = init_act
-               | Some s ⇒ is_costlabelled_act L_label ∧
-                          as_execute … L_label s L_s1 
+               [ None ⇒ bool_to_Prop(as_initial … L_s1) ∧ L_label = None ?
+               | Some s ⇒ ∃l. L_label = Some ? l ∧ is_costlabelled_act l ∧
+                          as_execute … l s L_s1 
                ]
  ; R_fin_ok : match R_label with
@@ -454 +454 @@
 ∀rel : relations S.
 simulation_conditions … rel → 
-∀s1,s1': S.∀l.l ≠ init_act → l ≠ cost_act (None ?) →  as_execute S l s1 s1' → 
+∀s1,s1': S.∀l.l ≠ cost_act (None ?) →  as_execute S l s1 s1' → 
 (as_classify … s1 ≠ cl_io ∨ as_classify … s1' ≠ cl_io) →
 ∀s2.
@@ -463 +463 @@
 (is_call_act l → is_call_post_label … s1 → is_call_post_label … s2') ∧
 (as_classify … s1' ≠ cl_io → as_classify … s2'' ≠ cl_io).
-#S #rel #good #s1 #s1' #l #l_noinit #l_notau #prf #HIO #s2 #REL cases(case_cl_io … (as_classify … s1))
+#S #rel #good #s1 #s1' #l #l_notau #prf #HIO #s2 #REL cases(case_cl_io … (as_classify … s1))
 [ #EQs1_io cases(io_exiting … EQs1_io … prf) #lab #EQ destruct(EQ) 
   cases HIO [ >EQs1_io * #EQ @⊥ @EQ % ] #Hio_s1'
@@ -477 +477 @@
     %{exe} %{s2''} %{(t_base …)} % [2: >EQs1' * #H @⊥ @H % ] %
      [ /4 by or_intror, conj, nmk/] * #f * #l #EQ destruct
-  | #Hclass_s1' cases l in prf l_noinit l_notau;
-    [ #f #l #prf #_ #_ inversion(is_call_post_label … s1)
+  | #Hclass_s1' cases l in prf l_notau;
+    [ #f #l #prf #_ inversion(is_call_post_label … s1)
       [ #Hpost cases(simulate_call_pl … good … prf … REL)
         [2: >Hpost % |3,4: assumption]
@@ -492 +492 @@
      ]
    | *
-     [ #prf #_ #_ cases(simulate_ret_n … good … prf … REL) [2,3: //] #s2' * #s2''
+     [ #prf #_ cases(simulate_ret_n … good … prf … REL) [2,3: //] #s2' * #s2''
        * #s2''' * #t1 * #exe * #t3 *** #REL' #sil_t1 #sil_t3 #_ %{s2'}
        %{t1} %{(or_introl … sil_t1)} %{s2''} %{exe} %{s2'''} %{t3} % 
        [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
        % [ % // % // ] * #f * #l #EQ destruct
-     | #l #prf #_ #_ cases(simulate_ret_l … good … prf … REL) [2,3: //]
+     | #l #prf #_ cases(simulate_ret_l … good … prf … REL) [2,3: //]
        #s2' * #s2'' * #s2''' * #t1 * #exe * #t3 ** #REL' #sil_t1 #sil_t3
        %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''} %{t3} % 
@@ -503 +503 @@
        % [ % // % //] * #f * #l #EQ destruct
     ]
-  | * [ #_ #_ * #H @⊥ @H % ] #lab #prf #_ #_ 
+  | * [ #_ * #H @⊥ @H % ] #lab #prf #_ 
     cases(simulate_label … prf … REL) [2,3,4: // ] #s2' * #s2'' * #s2''' * #t1 
     * #exe * #t3 ** #REL' #sil_t1 #sil_t3 %{s2'} %{t1} %{sil_t1} %{s2''} %{exe}
@@ -509 +509 @@
     [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
     % [% // % //] * #f * #l #EQ destruct
-  | #_ * #H @⊥ @H %
   ]
   % //
@@ -549 +548 @@
 [2: #REL_pre
     cut
-     (∃pre_state: S.
+     (∃pre_state: S.∃ l.
       ∃tr_i : raw_trace S s2 pre_state. silent_trace … tr_i ∧
-      ∃middle_state: S.
-       as_execute … (L_label … t) pre_state middle_state ∧
+      ∃middle_state: S.L_label … t = Some ? l ∧
+       as_execute … l pre_state middle_state ∧
       ∃final_state: S.
       ∃tr_i2: raw_trace S middle_state final_state. silent_trace … tr_i2 ∧
        as_classify … final_state ≠ cl_io ∧
        Srel … rel (L_s1 … t) final_state)
-    [ lapply(L_init_ok … t) >EQpre normalize nodelta * #Hcost #exe   
-      cases(instr_execute_commute … good … (L_label … t) … exe … REL_pre)
-      [2,3: % #EQ >EQ in Hcost; * |4: %2 @(head_of_premeasurable_is_not_io … (pre_meas … t)) ]
+      [ lapply(L_init_ok … t) >EQpre normalize nodelta * #l ** #EQllabe #Hcost #exe   
+      cases(instr_execute_commute … good … l … exe … REL_pre)
+      [2: % #EQ >EQ in Hcost; * |3: %2 @(head_of_premeasurable_is_not_io … (pre_meas … t)) ]
       #s2' * #t1 * #sil_t1 * #s2'' * #exe * #s2''' * #t3 *** #sil_t3 #REL' #Hcall 
-      #Hclass %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''} %{t3} % // % //
+      #Hclass %{s2'} %{l} %{t1} %{sil_t1} %{s2''} % [% //] %{s2'''} %{t3} % // % //
       cases sil_t3 [/2 by pre_silent_io/ ] inversion t3
       [ #H109 #H110 #H111 #H112 #H113 destruct @Hclass @(head_of_premeasurable_is_not_io … (pre_meas … t)) ]
       #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 cases H125
       #H @⊥ @H %]
-    * #pre_state * #tr_i * #silent_i * #middle_state * #step_pre_middle
+    * #pre_state * #l' * #tr_i * #silent_i * #middle_state ** #EQl' #step_pre_middle
     * #final_state * #tr_i2 ** #silent_i2 #final_not_io #REL
 | #REL
-  cut(bool_to_Prop (as_initial S s2)∧L_label S t=init_act)
+  cut(bool_to_Prop (as_initial S s2)∧L_label S t=None ?)
       [ lapply(L_init_ok … t) >EQpre normalize nodelta * #H1 #H2 % [2: //] 
         @(initial_is_initial … good … H1) assumption ] * #initial_s2 #init_label
@@ -602 +601 @@
          * >EQpost #EQ destruct #exe
           cases(instr_execute_commute … good … final_label … exe … REL') 
-          [2,3,6,7: % #EQ destruct cases H1 [1,3,5,7: * |*: normalize #EQ destruct]
-          |4,8: %1 @tail_of_premeasurable_is_not_io // 
+          [2,5: % #EQ destruct cases H1 [1,3,5,7: * |*: normalize #EQ destruct]
+          |3,6: %1 @tail_of_premeasurable_is_not_io // 
           ]
           #s2' * #t1 * #sil_t1 * #s2'' * #exe * #s2''' * #t3 *** #sil_t3 #REL'
@@ -613 +612 @@
      normalize nodelta /5 by conj/
 |3: %{(mk_measurable_trace … (L_label … t) (R_label … t) … (Some ? pre_state) … (Some ? post_state') … (tr_i2 @ t' @ tr') …)}
-    normalize nodelta [2: % // lapply(L_init_ok … t) >EQpre normalize nodelta * // 
+    normalize nodelta [2: %{l'} % // % // lapply(L_init_ok … t) >EQpre normalize nodelta * #l'' ** >EQl'
+      #EQ destruct // 
     |3: /3 by append_silent_premeasurable, append_premeasurable_silent/
     |4: % [2: %{final_state'} /5 by ex_intro, conj/ ] % /8 by ex_intro, conj/ % [ /3 by conj/]
@@ -625 +625 @@
   normalize nodelta
   [ assumption
-  | % // lapply(L_init_ok … t) >EQpre normalize nodelta * //
+  | %{l'} % // % // lapply(L_init_ok … t) >EQpre normalize nodelta * #l'' ** >EQl' #EQ destruct //
   | /4 by append_premeasurable_silent/
   | % // % [2: %{pre_state} /3/ ] % [ /2/] >get_cost_label_append 

LTS/Traces.ma

@@ -33 +33 @@
  | a_call : CallCostLabel → CostLabel
  | a_return_post : ReturnPostCostLabel → CostLabel
- | a_non_functional_label : NonFunctionalLabel → CostLabel.
+ | a_non_functional_label : NonFunctionalLabel → CostLabel
+ | i_act : CostLabel.
 
 coercion a_call.
@@ -149 +150 @@
   | a_non_functional_label x1 ⇒ 
      λc2.match c2 with [a_non_functional_label y1 ⇒ x1 == y1 | _ ⇒ false ]
+  | i_act ⇒ λc2.match c2 with [i_act ⇒ true | _ ⇒ false ]
   ].
 
 lemma eq_costlabel_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) → 
 (c1 ≠ c2 → P false) → P (eq_costlabel c1 c2).
-#P * #c1 * #c2 #H1 #H2 whd in match (eq_costlabel ??);
+#P * [1,2,3: #c1 |] * [1,2,3,5,6,7,9,10,11,13,14,15: #c2 |*:] 
+#H1 #H2 whd in match (eq_costlabel ??);
 try (@H2 % #EQ destruct) 
 [ change with (eq_call_cost_lab ??) in ⊢ (?%); @eq_call_cost_lab_elim
@@ -162 +165 @@
 | change with (eq_nf_label ??) in ⊢ (?%); @eq_fn_label_elim
   [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ]
+| @H1 %
 ]
 qed.
@@ -187 +191 @@
  | call_act : FunctionName → CallCostLabel → ActionLabel
  | ret_act : option(ReturnPostCostLabel) → ActionLabel
- | cost_act : option NonFunctionalLabel → ActionLabel
- | init_act : ActionLabel.
+ | cost_act : option NonFunctionalLabel → ActionLabel.
  
 definition is_cost_label : ActionLabel → Prop ≝ 
@@ -263 +266 @@
                     | ret_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ]
                     | cost_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ]
-                    | init_act ⇒ False
                     ].
 (*

LTS/Vm.ma

@@ -411 +411 @@
     return (op … abs_t (instr_m … instr) n) 
   ].
- 
-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] ≝ 
 { map_type :> Type[0]
@@ -442 +422 @@
 }.
 
-definition labels_pc_of_instr : ∀p.AssemblerInstr p → ℕ → list (InitCostLabel × ℕ) ≝ 
+definition labels_pc_of_instr : ∀p.AssemblerInstr p → ℕ → list (CostLabel × ℕ) ≝ 
 λp,i,program_counter.
 match i with
   [ Seq _ opt_l ⇒ match opt_l with 
-                  [ Some lbl ⇒ [〈costlab (a_non_functional_label lbl),S program_counter〉]
+                  [ Some lbl ⇒ [〈(a_non_functional_label lbl),S program_counter〉]
                   | None ⇒ [ ]
                   ]
   | Ijmp _ ⇒ [ ]
-  | 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〉]
+  | 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 lin),program_counter〉;
+                      〈(a_non_functional_label lout),S program_counter〉]
   | Icall f ⇒ [ ]
   | Iret ⇒ [ ]
@@ -459 +439 @@
 
 let rec labels_pc (p : assembler_params)
-(prog : list (AssemblerInstr p)) (program_counter : ℕ) on prog : list (InitCostLabel × ℕ) ≝ 
+(prog : list (AssemblerInstr p)) (program_counter : ℕ) on prog : list (CostLabel × ℕ) ≝ 
 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)
+[ nil ⇒ [〈i_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 ⇒ (labels_pc_of_instr … i program_counter)@labels_pc p is (S program_counter)
 ].
@@ -485 +465 @@
  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).
+   mem … 〈(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:(??%?);
@@ -499 +479 @@
  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).
+   mem … 〈(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:(??%?);
@@ -530 +510 @@
 *)  
 
-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
@@ -549 +517 @@
 
 definition static_analisys : ∀p : assembler_params.∀abs_t : monoid.(AssemblerInstr p → abs_t) → 
-∀mT : cost_map_T DEQInitCostLabel abs_t.AssemblerProgram p → option mT ≝
+∀mT : cost_map_T DEQCostLabel abs_t.AssemblerProgram p → option mT ≝
 λp,abs_t,instr_m,mT,prog.
 let prog_size ≝ S (|instructions … prog|) in
@@ -709 +677 @@
 |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)).
+ (mem … 〈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
@@ -744 +711 @@
 |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
@@ -770 +736 @@
 ∀lbl.
 mem … lbl (get_costlabels_of_trace … t) → 
-mem … (costlab lbl) (map ?? \fst … (labels_pc … (instructions p prog) O)).
+mem … (lbl) (map ?? \fst … (labels_pc … (instructions p prog) O)).
 #p #p' #prog #st1 #st2 #t elim t
 [ #st #lbl *
@@ -902 +868 @@
 qed.
 
+definition actionlabel_to_costlabel : ActionLabel → list CostLabel ≝
+λa.match a with
+[ call_act f l ⇒ [a_call l]
+| ret_act opt_l ⇒ match opt_l with [None ⇒ [ ] | Some l ⇒ [a_return_post l]]
+| cost_act opt_l ⇒ match opt_l with [None ⇒ [ ] | Some l ⇒ [a_non_functional_label l]]
+].
+
+definition get_costlabels_of_measurable_trace : ∀S : abstract_status.measurable_trace S → list CostLabel ≝ 
+λS,t.
+ match L_label … t with
+ [ None ⇒ [i_act]
+ | Some l ⇒ actionlabel_to_costlabel l
+ ] @
+ get_costlabels_of_trace … (trace … t).
+
 (*get_costlabels_of_measurable_trace deve aggiungere la label iniziale.*)
-theorem static_dynamic : ∀p,p',prog.∀no_dup : asm_no_duplicates p prog.
+theorem static_dynamic_meas : ∀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.
 ∀EQmap : static_analisys p ? instr_m mT prog = return map1.
 ∀t : measurable_trace (asm_operational_semantics p p' prog).
-∀a1.rel_galois … good st1 (L_s1 … t) → 
+∀a1.rel_galois … good (L_s1 … t) a1 → 
 let stop_state ≝ match R_post_state … t with [None ⇒ R_s2 … t | Some x ⇒ x ] in
-∀costs.
-costs = dependent_map CostLabel ? (get_costlabels_of_measurable_trace …  t) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) →
-rel_galois … good stop_state (act_abs … abs_t (big_op … costs) a1).
-
-
-
+∀abs_trace.
+abs_trace = dependent_map CostLabel ? (get_costlabels_of_measurable_trace …  t) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) →
+rel_galois … good stop_state (act_abs … abs_t (big_op … abs_trace) a1).
+[2: @hide_prf
+    whd in match get_costlabels_of_measurable_trace in prf; normalize nodelta in prf;
+    cases(mem_append ???? prf) -prf
+    [2: #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))
+    | inversion(L_label … t) normalize nodelta [| #lbl'] #EQleft
+      [ * [2: *] #EQ destruct cases daemon (* i_act sta sempre nel codice *)
+      | (* per inversione su as_execute *) cases daemon
+      ]
+    ]
+]
+#p #p' #prog #no_dup #abs_t #instr_m #good #mT #map1 #EQmap1 #t #a1 #rel_galois #abs_trace #EQabs_trace
+xxxxxx
+lapply(static_dynamic … (trace …t) … abs_trace) try //
+
+