Index: /Papers/itp2013/ccexec.tex
===================================================================
 /Papers/itp2013/ccexec.tex (revision 3305)
+++ /Papers/itp2013/ccexec.tex (revision 3306)
@@ 89,4 +89,8 @@
every node/.style={draw, is other}},
small vgap/.style={row sep={7mm,between origins}},
+ % for article, maybe temporary
+ is jump/.style=is other,
+ is call/.style=is other,
+ is ret/.style=is other,
}
@@ 106,4 +110,5 @@
\newcommand{\append}{\mathbin{@}}
+\newcommand{\iffdef}{\mathrel{:\Leftrightarrow}}
\begin{document}
@@ 392,5 +397,5 @@
The program semantics adopted in the traditional labelling approach is based
on labelled deductive systems. Given a set of observables $\mathcal{O}$ and
a set of states $\mathcal{S}$, the semantics of one deterministic execution
+a set of states $\S$, the semantics of one deterministic execution
step is
defined as a function $S \to S \times O^*$ where $O^*$ is a (finite) stream of
@@ 727,9 +732,11 @@
kind  are defined by structural recursion on the first trace and pattern
matching over the second. Here we turn
the definition into inference rules for the sake of readability. We also
omit from trace constructors all arguments, but those that are traces or that
+the definition into the inference rules shown in \autoref{fig:txx_rel}
+for the sake of readability. We also omit from trace constructors all arguments,
+but those that are traces or that
are used in the premises of the rules. By abuse of notation we denote all three
relations by infixing $\approx$

+relations by infixing $\approx$.
+
+\begin{figure}
\begin{multicols}{2}
\infrule
@@ 744,5 +751,6 @@
{\texttt{tlr\_step}~tll_1~tlr_1 \approx \texttt{tlr\_step}~tll_2~tlr_2}
\end{multicols}

+\vspace{3ex}
+\begin{multicols}{2}
\infrule
{\ell~s_1 = \ell~s_2 \andalso
@@ 752,11 +760,17 @@
\infrule
+ {tal_1\approx tal_2
+ }
+ {\texttt{tal\_step\_default}~tal_1 \approx tal_2}
+\end{multicols}
+\vspace{3ex}
+\infrule
{}
{\texttt{tal\_base\_not\_return}\approx taa \append \texttt{tal\_base\_not\_return}}

+\vspace{1ex}
\infrule
{}
{\texttt{tal\_base\_return}\approx taa \append \texttt{tal\_base\_return}}

+\vspace{1ex}
\infrule
{tlr_1\approx tlr_2 \andalso
@@ 764,5 +778,5 @@
}
{\texttt{tal\_base\_call}~s_1~tlr_1\approx taa \append \texttt{tal\_base\_call}~s_2~tlr_2}

+\vspace{1ex}
\infrule
{tlr_1\approx tlr_2 \andalso
@@ 771,5 +785,5 @@
}
{\texttt{tal\_base\_call}~s_1~tlr_1 \approx taa \append \texttt{tal\_step\_call}~s_2~tlr_2~tal_2)}

+\vspace{1ex}
\infrule
{tlr_1\approx tlr_2 \andalso
@@ 778,16 +792,15 @@
}
{\texttt{tal\_step\_call}~s_1~tlr_1~tal_1 \approx taa \append \texttt{tal\_base\_call}~s_2~tlr_2)}

+\vspace{1ex}
\infrule
{tlr_1 \approx tlr_2 \andalso
 s_1 \uparrow f \andalso s_2\uparrow f
+ s_1 \uparrow f \andalso s_2\uparrow f\andalso
tal_1 \approx tal_2 \andalso
}
{\texttt{tal\_step\_call}~s_1~tlr_1~tal_1 \approx taa \append \texttt{tal\_step\_call}~s_2~tlr_2~tal_2}

\infrule
 {tal_1\approx tal_2
 }
 {\texttt{tal\_step\_default}~tal_1 \approx tal_2}
+\caption{The inference rule for the relation $\approx$.}
+\label{fig:txx_rel}
+\end{figure}
+%
\begin{comment}
\begin{verbatim}
@@ 863,5 +876,5 @@
\end{verbatim}
\end{comment}

+%
In the preceding rules, a $taa$ is an inhabitant of the
$\texttt{trace\_any\_any}~s_1~s_2$ (shorthand $\texttt{TAA}~s_1~s_2$),
@@ 873,5 +886,4 @@
left of a \texttt{TAL}. A \texttt{TAA} captures
a sequence of silent moves.

The \texttt{tal\_collapsable} unary predicate over \texttt{TAL}'s
holds when the argument does not contain any function call and it ends
@@ 879,4 +891,6 @@
can still perform a sequence of silent actions while remaining similar.
+As should be expected, even though the rules are asymmetric $\approx$ is in fact
+an equivalence relation.
\section{Forward simulation}
\label{simulation}
@@ 894,8 +908,8 @@
simulation we are interested in (preservation of observables), we are
forced to prove a stronger notion of forward simulation that introduces
an explicit relation between states. The classical notion of a 1to0ormany
forward simulation is the existence of a relation $R$ over states such that
if $s_1 R s_2$ and $s_1 \to^1 s_1'$ then there exists an $s_2'$ such that
$s_2 \to^* s_2'$ and $s_1' R s_2'$. In our context, we need to replace the
+an explicit relation between states. The classical notion of a 1tomany
+forward simulation is the existence of a relation $\S$ over states such that
+if $s_1 \S s_2$ and $s_1 \to^1 s_1'$ then there exists an $s_2'$ such that
+$s_2 \to^* s_2'$ and $s_1' \S s_2'$. In our context, we need to replace the
one and multi step transition relations $\to^n$ with the existence of
a structured trace between the two states, and we need to add the request that
@@ 903,6 +917,6 @@
something like:\\
for all $s_1,s_2,s_1'$ such that there is a $\tau_1$ from
$s_1$ to $s_1'$ and $s_1 R s_2$ there exists an $s_2'$ such that
$s_1' R s_2'$ and a $\tau_2$ from $s_2$ to $s_2'$ such that
+$s_1$ to $s_1'$ and $s_1 \S s_2$ there exists an $s_2'$ such that
+$s_1' \S s_2'$ and a $\tau_2$ from $s_2$ to $s_2'$ such that
$\tau_1$ is similar to $\tau_2$. We call this particular form of forward
simulation \emph{trace reconstruction}.
@@ 937,14 +951,14 @@
Therefore we now introduce an abstract notion of relation set between abstract
statuses and an abstract notion of 1to0ormany forward simulation conditions.
+statuses and an abstract notion of 1tomany forward simulation conditions.
These two definitions enjoy the following remarkable properties:
\begin{enumerate}
\item they are generic enough to accommodate all passes of the CerCo compiler
 \item the conjunction of the 1to0ormany forward simulation conditions are
 just slightly stricter than the statement of a 1to0ormany forward
+ \item the conjunction of the 1tomany forward simulation conditions are
+ just slightly stricter than the statement of a 1tomany forward
simulation in the classical case. In particular, they only require
the construction of very simple forms of structured traces made of
silent states only.
 \item they allow to prove our main result of the paper: the 1to0ormany
+ \item they allow to prove our main result of the paper: the 1tomany
forward simulation conditions are sufficient to prove the trace
reconstruction theorem
@@ 960,5 +974,5 @@
that the cost model can be computed on the object code and lifted to the
source code to reason on nonfunctional properties, assuming that
the 1to0ormany forward simulation conditions are fulfilled for every
+the 1tomany forward simulation conditions are fulfilled for every
compiler pass.
@@ 970,62 +984,64 @@
by every pass. The remaining two are derived relations.
The $\mathcal{S}$ relation between states is the classical relation used
+The $\S$ relation between states is the classical relation used
in forward simulation proofs. It correlates the data of the status
(e.g. registers, memory, etc.).
The $\mathcal{C}$ relation correlates call states. It allows to track the
+The $\C$ relation correlates call states. It allows to track the
position in the target code of every call in the source code.
The $\mathcal{L}$ relation simply says that the two states are both label
emitting states that emit the same label. It allows to track the position in
+The $\L$ relation simply says that the two states are both label
+emitting states that emit the same label, \emph{i.e.}\ $s_1\L s_2\iffdef \ell~s_1=\ell~s_2$.
+It allows to track the position in
the target code of every cost emitting statement in the source code.
Finally the $\mathcal{R}$ relation is the more complex one. Two states
$s_1$ and $s_2$ are $\mathcal{R}$ correlated if every time $s_1$ is the
successors of a call state that is $\mathcal{C}$related to a call state
$s_2'$ in the target code, then $s_2$ is the successor of $s_2'$.
+Finally the $\R$ relation is the more complex one. Two states
+$s_1$ and $s_2$ are $\R$ correlated if every time $s_1$ is the
+successors of a call state that is $\C$related to a call state
+$s_2'$ in the target code, then $s_2$ is the successor of $s_2'$. Formally:
+$$s_1\R s_2 \iffdef \forall s_1',s_2'.s_1'\C s_2' \to s_1'\ar s_1 \to s_2' \ar s_2.$$
We will require all pairs of states that follow a related call to be
$\mathcal{R}$related. This is the fundamental requirement to grant
that the target trace is well structured, i.e. that function calls are well
nested and always return where they are supposed to.

\begin{alltt}
record status_rel (S1,S2 : abstract_status) : Type[1] := \{
 \(\mathcal{S}\): S1 \(\to\) S2 \(\to\) Prop;
 \(\mathcal{C}\): (\(\Sigma\)s.as_classifier S1 s cl_call) \(\to\)
 (\(\Sigma\)s.as_classifier S2 s cl_call) \(\to\) Prop \}.

definition \(\mathcal{L}\) S1 S2 st1 st2 := as_label S1 st1 = as_label S2 st2.

definition \(\mathcal{R}\) S1 S2 (R: status_rel S1 S2) s1_ret s2_ret ≝
 \(\forall\)s1_pre,s2_pre.
 as_after_return s1_pre s1_ret \(\to\) s1_pre \(\mathcal{R}\) s2_pre \(\to\)
 as_after_return s2_pre s2_ret.
\end{alltt}
+$\R$related. This is the fundamental requirement granting
+that the target trace is well structured, \emph{i.e.}\ that calls are well
+nested and returning where they are supposed to.
+
+% \begin{alltt}
+% record status_rel (S1,S2 : abstract_status) : Type[1] := \{
+% \(\S\): S1 \(\to\) S2 \(\to\) Prop;
+% \(\C\): (\(\Sigma\)s.as_classifier S1 s cl_call) \(\to\)
+% (\(\Sigma\)s.as_classifier S2 s cl_call) \(\to\) Prop \}.
+%
+% definition \(\L\) S1 S2 st1 st2 := as_label S1 st1 = as_label S2 st2.
+%
+% definition \(\R\) S1 S2 (R: status_rel S1 S2) s1_ret s2_ret ≝
+% \(\forall\)s1_pre,s2_pre.
+% as_after_return s1_pre s1_ret \(\to\) s1_pre \(\R\) s2_pre \(\to\)
+% as_after_return s2_pre s2_ret.
+% \end{alltt}
\begin{figure}
\centering
\begin{tabular}{@{}c@{}c@{}}
\begin{subfigure}{.475\linewidth}
\centering
\begin{tikzpicture}[every join/.style={ar}, join all, thick,
 every label/.style=overlay, node distance=10mm]
 \matrix [diag] (m) {%
 \node (s1) [is jump] {}; & \node [fill=white] (t1) {};\\
 \node (s2) {}; & \node (t2) {}; \\
 };
 \node [above=0 of t1, overlay] {$\alpha$};
 {[stealth]
 \draw (s1)  (t1);
 \draw [new] (s2)  node [above] {$*$} (t2);
 }
 \draw (s1) to node [rel] {$\S$} (s2);
 \draw [new] (t1) to node [rel] {$\S,\L$} (t2);
\end{tikzpicture}
\caption{The \texttt{cl\_jump} case.}
\label{subfig:cl_jump}
\end{subfigure}
&
\begin{subfigure}{.475\linewidth}
+\begin{tabular}{@{}c@{}c@{}c@{}}
+% \begin{subfigure}{.475\linewidth}
+% \centering
+% \begin{tikzpicture}[every join/.style={ar}, join all, thick,
+% every label/.style=overlay, node distance=10mm]
+% \matrix [diag] (m) {%
+% \node (s1) [is jump] {}; & \node [fill=white] (t1) {};\\
+% \node (s2) {}; & \node (t2) {}; \\
+% };
+% \node [above=0 of t1, overlay] {$\alpha$};
+% {[stealth]
+% \draw (s1)  (t1);
+% \draw [new] (s2)  node [above] {$*$} (t2);
+% }
+% \draw (s1) to node [rel] {$\S$} (s2);
+% \draw [new] (t1) to node [rel] {$\S,\L$} (t2);
+% \end{tikzpicture}
+% \caption{The \texttt{cl\_jump} case.}
+% \label{subfig:cl_jump}
+% \end{subfigure}
+% &
+\begin{subfigure}{.25\linewidth}
\centering
\begin{tikzpicture}[every join/.style={ar}, join all, thick,
@@ 1042,9 +1058,9 @@
\draw [new] (t1) to node [rel] {$\S,\L$} (t2);
\end{tikzpicture}
\caption{The \texttt{cl\_oher} case.}
\label{subfig:cl_other}
+\caption{The \texttt{cl\_oher} and \texttt{cl\_jump} cases.}
+\label{subfig:cl_other_jump}
\end{subfigure}
\\
\begin{subfigure}{.475\linewidth}
+&
+\begin{subfigure}{.375\linewidth}
\centering
\begin{tikzpicture}[every join/.style={ar}, join all, thick,
@@ 1071,5 +1087,5 @@
\end{subfigure}
&
\begin{subfigure}{.475\linewidth}
+\begin{subfigure}{.375\linewidth}
\centering
\begin{tikzpicture}[every join/.style={ar}, join all, thick,
@@ 1095,5 +1111,5 @@
\end{subfigure}
\end{tabular}
\caption{The hypotheses for the preservation of structured traces, simplified.
+\caption{Mnemonic diagrams depicting the hypotheses for the preservation of structured traces.
Dashed lines
and arrows indicates how the diagrams must be closed when solid relations
@@ 1102,5 +1118,5 @@
\end{figure}
\paragraph{1to0ormany forward simulation conditions.}
+\paragraph{1tomany forward simulation conditions.}
\begin{condition}[Cases \texttt{cl\_other} and \texttt{cl\_jump}]
For all $s_1,s_1',s_2$ such that $s_1 \S s_1'$, and
@@ 1112,5 +1128,6 @@
\end{condition}
In the above condition, a $\texttt{trace\_any\_any\_free}~s_1~s_2$ (which from now on
+In the above condition depicted in \autoref{subfig:cl_other_jump},
+a $\texttt{trace\_any\_any\_free}~s_1~s_2$ (which from now on
will be shorthanded as \verb+TAAF+) is an
inductive type of structured traces that do not contain function calls or
@@ 1130,14 +1147,14 @@
$\verb+TAAF+~s_b~s_2'$ such that:
$s_a\class\texttt{cl\_call}$, the \texttt{as\_call\_ident}'s of
the two call states are the same, $s_1 \mathcal{C} s_a$,
+the two call states are the same, $s_1 \C s_a$,
$s_a\exec s_b$, $s_1' \L s_b$ and
$s_1' \S s_2'$.
\end{condition}
The condition says that, to simulate a function call, we can perform a
+The condition, depicted in \autoref{subfig:cl_call} says that, to simulate a function call, we can perform a
sequence of silent actions before and after the function call itself.
The old and new call states must be $\mathcal{C}$related, the old and new
states at the beginning of the function execution must be $\mathcal{L}$related
and, finally, the two initial and final states must be $\mathcal{S}$related
+The old and new call states must be $\C$related, the old and new
+states at the beginning of the function execution must be $\L$related
+and, finally, the two initial and final states must be $\S$related
as usual.
@@ 1147,5 +1164,5 @@
$\verb+TAA+~s_2~s_a$, a
$\verb+TAAF+~s_b~s_2'$ called $taaf$ such that:
$s_a$ is classified as a \texttt{cl\_return},
+$s_a\class\texttt{cl\_return}$,
$s_a\exec s_b$,
$s_1' \R s_b$ and
@@ 1155,8 +1172,9 @@
Similarly to the call condition, to simulate a return we can perform a
sequence of silent actions before and after the return statement itself.
The old and the new statements after the return must be $\mathcal{R}$related,
+sequence of silent actions before and after the return statement itself,
+as depicted in \autoref{subfig:cl_return}.
+The old and the new statements after the return must be $\R$related,
to grant that they returned to corresponding calls.
The two initial and final states must be $\mathcal{S}$related
+The two initial and final states must be $\S$related
as usual and, moreover, they must exhibit the same labels. Finally, when
the suffix is non empty we must take care of not inserting a new
@@ 1247,8 +1265,8 @@
\end{comment}
\paragraph{Main result: the 1to0ormany forward simulation conditions
+\paragraph{Main result: the 1tomany forward simulation conditions
are sufficient to trace reconstruction}
Let us assume that a relation set is given such that the 1to0ormany
+Let us assume that a relation set is given such that the 1tomany
forward simulation conditions are satisfied. Under this assumption we
can prove the following three trace reconstruction theorems by mutual
@@ 1283,57 +1301,59 @@
precomputed preamble, even if this is likely to be the case in concrete
implementations. The preamble in input is necessary for compositionality, e.g.
because the 1to0ormany forward simulation conditions allow in the
+because the 1tomany forward simulation conditions allow in the
case of function calls to execute a preamble of silent instructions just after
the function call.
\begin{theorem}[\texttt{status\_simulation\_produce\_tll}]
For every $s_1,s_1',s_{2_b},s_2$ s.t.
there is a $\texttt{TLL}~b~s_1~s_1'$ called $tll_1$ and a
$\verb+TAA+~s_{2_b}~s_2$ and $s_1 \L s_{2_b}$ and
$s_1 \S s_2$, there exists $s_{2_m},s_2'$ s.t.
\begin{itemize}
 \item if $b$ (the trace ends with a return) then there exists $s_{2_m},s_2'$
 and a trace $\texttt{TLL}~b~s_{2_b}~s_{2_m}$ called $tll_2$
 and a $\texttt{TAAF}~s_{2_m}~s_2'$ called $taa_2$ s.t.
 $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
 $s_1' \R s_{2_m}$ and
 $tll_1\approx tll_2$ and
 if $taa_2$ is non empty then $\lnot \ell~s_{2_m}$;
 \item else there exists $s_2'$ and a
 $\texttt{TLL}~b~s_{2_b}~s_2'$ called $tll_2$ such that
 $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
 $tll_1\approx tll_2$.
\end{itemize}
\end{theorem}

The statement is similar to the previous one: a source
\texttt{trace\_label\_label} and a given target preamble of silent states
in the target code induce a similar \texttt{trace\_label\_label} in the
target code, possibly followed by a sequence of silent moves that become the
preamble for the next \texttt{trace\_label\_label} translation.

\begin{theorem}[\texttt{status\_simulation\_produce\_tal}]
For every $s_1,s_1',s_2$ s.t.
there is a $\texttt{TAL}~b~s_1~s_1'$ called $tal_1$ and
$s_1 \mathcal{S} s_2$
\begin{itemize}
 \item if $b$ (the trace ends with a return) then there exists $s_{2_m},s_2'$
 and a trace $\texttt{TAL}~b~s_2~s_{2_m}$ called $tal_2$ and a
 $\texttt{TAAF}~s_{2_m}~s_2'$ called $taa_2$ s.t.
 $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
 $s_1' \R s_{2_m}$ and
 $tal_1 \approx tal_2$ and
 if $taa_2$ is non empty then $\lnot \ell~s_{2_m}$;
 \item else there exists $s_2'$ and a
 $\texttt{TAL}~b~s_2~s_2'$ called $tal_2$ such that
 either $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
 $tal_1\approx tal_2$
 or $s_1' \mathrel{{\S} \cap {\L}} s_2$ and
 $\texttt{tal\_collapsable}~tal_1$ and $\lnot \ell~s_1$.
\end{itemize}
\end{theorem}

The statement is also similar to the previous ones, but for the lack of
the target code preamble.
+Clearly similar results are also available for the other two types of structured
+traces (in fact, they are all proved simultaneously by mutual induction).
+% \begin{theorem}[\texttt{status\_simulation\_produce\_tll}]
+% For every $s_1,s_1',s_{2_b},s_2$ s.t.
+% there is a $\texttt{TLL}~b~s_1~s_1'$ called $tll_1$ and a
+% $\verb+TAA+~s_{2_b}~s_2$ and $s_1 \L s_{2_b}$ and
+% $s_1 \S s_2$, there exists $s_{2_m},s_2'$ s.t.
+% \begin{itemize}
+% \item if $b$ (the trace ends with a return) then there exists $s_{2_m},s_2'$
+% and a trace $\texttt{TLL}~b~s_{2_b}~s_{2_m}$ called $tll_2$
+% and a $\texttt{TAAF}~s_{2_m}~s_2'$ called $taa_2$ s.t.
+% $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
+% $s_1' \R s_{2_m}$ and
+% $tll_1\approx tll_2$ and
+% if $taa_2$ is non empty then $\lnot \ell~s_{2_m}$;
+% \item else there exists $s_2'$ and a
+% $\texttt{TLL}~b~s_{2_b}~s_2'$ called $tll_2$ such that
+% $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
+% $tll_1\approx tll_2$.
+% \end{itemize}
+% \end{theorem}
+%
+% The statement is similar to the previous one: a source
+% \texttt{trace\_label\_label} and a given target preamble of silent states
+% in the target code induce a similar \texttt{trace\_label\_label} in the
+% target code, possibly followed by a sequence of silent moves that become the
+% preamble for the next \texttt{trace\_label\_label} translation.
+%
+% \begin{theorem}[\texttt{status\_simulation\_produce\_tal}]
+% For every $s_1,s_1',s_2$ s.t.
+% there is a $\texttt{TAL}~b~s_1~s_1'$ called $tal_1$ and
+% $s_1 \S s_2$
+% \begin{itemize}
+% \item if $b$ (the trace ends with a return) then there exists $s_{2_m},s_2'$
+% and a trace $\texttt{TAL}~b~s_2~s_{2_m}$ called $tal_2$ and a
+% $\texttt{TAAF}~s_{2_m}~s_2'$ called $taa_2$ s.t.
+% $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
+% $s_1' \R s_{2_m}$ and
+% $tal_1 \approx tal_2$ and
+% if $taa_2$ is non empty then $\lnot \ell~s_{2_m}$;
+% \item else there exists $s_2'$ and a
+% $\texttt{TAL}~b~s_2~s_2'$ called $tal_2$ such that
+% either $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
+% $tal_1\approx tal_2$
+% or $s_1' \mathrel{{\S} \cap {\L}} s_2$ and
+% $\texttt{tal\_collapsable}~tal_1$ and $\lnot \ell~s_1$.
+% \end{itemize}
+% \end{theorem}
+%
+% The statement is also similar to the previous ones, but for the lack of
+% the target code preamble.
\begin{comment}
@@ 1341,5 +1361,5 @@
For every $s_1,s_1',s_2$ s.t.
there is a $\texttt{trace\_label\_return}~s_1~s_1'$ called $tlr_1$ and
$s_1 (\mathcal{L} \cap \mathcal{S}) s_2$
+$s_1 (\L \cap \S) s_2$
there exists $s_{2_m},s_2'$ s.t.
there is a $\texttt{trace\_label\_return}~s_2~s_{2_m}$ called $tlr_2$ and
@@ 1347,6 +1367,6 @@
s.t. if $taaf$ is non empty then $\lnot (\texttt{as\_costed}~s_{2_m})$,
and $\texttt{tlr\_rel}~tlr_1~tlr_2$
and $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and
$s_1' \mathcal{R} s_{2_m}$.
+and $s_1' (\S \cap \L) s_2'$ and
+$s_1' \R s_{2_m}$.
\end{corollary}
\end{comment}
@@ 1415,5 +1435,5 @@
simulation related to nonfunctional properties (preservation of structure)
from that related to functional properties. In particular, we reduce the
problem of preservation of structure to that of showing a 1to0ormany
+problem of preservation of structure to that of showing a 1tomany
forward simulation that only adds a few additional proof obligations to those
of a traditional, function properties only, proof.