\documentclass[12pt,a4paper]{article}

\usepackage[cm]{fullpage}
\usepackage{amsthm}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{xspace}
\usepackage[english]{babel}
\usepackage{fancyhdr}
\usepackage{titling}
\renewcommand{\thesection}{Exercise \projnumber.\arabic{section}:}

\newcommand{\groupnumber}{5}
\newcommand{\name}{Tobias Eidelpes}
\newcommand{\matriculation}{01527193}

\newcommand\fstar{F$^\star$\xspace}
\newcommand{\projnumber}{2}
\newcommand{\Title}{\fstar}
\setlength{\headheight}{15.2pt}
\setlength{\headsep}{20pt}
\setlength{\textheight}{680pt}
\pagestyle{fancy}
\fancyhf{}
\fancyhead[L]{Formal Methods for Security and Privacy \projnumber\ - \fstar}
\fancyhead[C]{}
\fancyhead[R]{Group \groupnumber}
\renewcommand{\headrulewidth}{0.4pt}
\fancyfoot[C]{\thepage}


\begin{document}
\thispagestyle{empty}
\noindent\framebox[\linewidth]{%
 \begin{minipage}{\linewidth}%
 \hspace*{5pt} \textbf{Formal Methods for Security and Privacy (SS2021)} \hfill Prof.~Matteo Maffei \hspace*{5pt}\\

 \begin{center}
  {\bf\Large Project \projnumber~-- \Title}
 \end{center}

 \vspace*{5pt}\hspace*{5pt} \hfill TU Wien \hspace*{5pt}
\end{minipage}%
}
\vspace{0.5cm}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\section*{Group \groupnumber}
Our group consists of the following members:
\begin{center}
\textbf{\name}

\matriculation
\end{center}

\section{Small-step semantics}

\textit{Notes on semantics. Not mandatory.}

\section{Termination}

\paragraph{Explanation of the used measure}

The measure consists of a list of size three. The entries are:

\begin{enumerate}
    \item The amount of gas in the execution state.
    \item The size of the call stack.
    \item If the call stack is constructed with \texttt{Exec}, the third element
        is the natural number 1 and if the call stack is constructed with
        \texttt{Ter}, the third element is the natural number 0.
\end{enumerate}

For the amount of gas, there are three different possibilities:

\begin{enumerate}
    \item The call stack is a plain call stack.
    \item If the call stack is in a halting state, gas specifies the amount of
        remaining gas.
    \item If there is an exception state, the amount of gas is set to 0.
\end{enumerate}

Additionally, there are three match clauses in the \texttt{step} function. The
first case matches a termination state with an empty call stack. If the state
before that was an exception, the first elements are equal but the size of the
call stack before the application of the \texttt{step} function was greater.
This means that the measure decreases. If there was no exception but of type
\texttt{Exec} with a positive amount of gas, the measure also decreases.

In the second match clause, a termination state with a non-empty call stack is
handled. The amount of gas decreases if there is a termination state of
\texttt{ExcState}, because it is set to 0. If the termination state is
\texttt{HaltState}, the amount of gas also decreases.

The third match clause handles execution of a plain call stack. If a
\texttt{HaltState} is reached, the amount of gas reduces by 1. Again, if there
occurs an exception, looking at the third element of the list gives a value
change from 1 to 0.

\section{Final states}

\paragraph{Paper proofs}

To prove \texttt{nsteps\_stop}, induction over the amount of executed steps $n$
is used. The base case starts with $n = 0$. This case is trivial since
\texttt{nsteps 0 te cs == cs}. The induction hypothesis is \texttt{nsteps (n-1)
te cs == cs} and it is assumed that $n > 0$. The induction then goes as follows:
\begin{verbatim}
nsteps n te cs = nsteps (n-1) te (step_simp te cs)
               = nsteps (n-1) te cs
               = cs
\end{verbatim}
It is allowed to reduce \texttt{step\_simp te cs} to \texttt{cs}, because
\texttt{cs} is already final.

Now it is possible to prove the lemma \texttt{progress}: \texttt{cs ==
step\_simp te cs} $\rightarrow$ \texttt{isFinal cs}. Since \texttt{step\_simp}
has the same value as the \texttt{step} function, when the outcome is
\texttt{Next}, the call stack is different from \texttt{cs}. This means that the
left side of the lemma does not hold and therefore the right side does not have
to hold to satisfy the implication. If the outcome is \texttt{Stop}, \texttt{cs}
can only equal \texttt{Ter ts []} and therefore the left side is satisfied. When
the left side is satisfied, \texttt{cs} is a final state and therefore it
follows that \texttt{isFinal cs} is also true.

\paragraph{Explanation on used equalities}

The lemma uses propositional equality, because \texttt{callstack} has the
keyword \texttt{noeq}, which means that the type does not satisfy decidable
equality. The usual equality only works with types that satisfy decidable
equality and therefore propositional equality is needed.

\section{Uniqueness of call stacks}

\paragraph{Paper proofs}

Note: The previously defined measure is written as \texttt{|cs|}, where
\texttt{cs} is a call stack.

To prove \texttt{order\_decreases} it needs to be shown that from \texttt{nsteps
n te cs == cs'} and $n > 0$ follows \texttt{|cs'| << |cs|} for all
$n\in\mathbb{N}$. The proof is by induction on \texttt{n}. For \texttt{n = 1},
\texttt{nsteps 1 te cs} is equal to \texttt{step\_simp te cs}. Similarly to
Exercise 2.2 it follows that the hypothesis holds, because \texttt{cs} is not a
final state. After that, the induction step is \texttt{nsteps (n+1) te cs ==
cs'}, which can be rewritten as \texttt{nsteps n te (step\_simp te cs) == cs'}
(definition of \texttt{nsteps}). With the reasoning from the base case where
\texttt{n = 1}, it follows that \texttt{|step\_simp te cs| << |cs|}. Now there
are two cases: either the call stack \texttt{|step\_simp te cs} is final or not.
For the first case, the lemma \texttt{nsteps\_stop} can be used to derive
\texttt{step\_simp te cs == cs'} from \texttt{nsteps n te (step\_simp te cs) ==
cs'}, where \texttt{|step\_simp te cs| << |cs|} holds. For the second case, we
simply take the induction hypothesis to conclude that the induction holds.

Taking the previous proof, for \texttt{callstacks\_unique} it is evident that
\texttt{|cs'| << |cs|} holds. It follows that \texttt{cs'} $\neq$ \texttt{cs} by
proof of contradiction: Assuming that \texttt{cs' == cs} and \texttt{|cs'| <<
|cs|} is true, it would require that the top constant in both lists
\texttt{LexTop} satisfies \texttt{LexTop << LexTop}. Since this is impossible,
it contradicts the assumption and therefore it follows that \texttt{cs'} $\neq$
\texttt{cs}.

\section{Exception Propagation}

\paragraph{Paper proof}

Proof by induction:

\begin{verbatim}
length ps = 0

nsteps (2 * (length [])) te (Ter ExcState []) == (Ter ExcState [])
nsteps 0 te (Ter ExcState []) == (Ter ExcState [])
(Ter ExcState []) == (Ter ExcState [])
\end{verbatim}

\begin{verbatim}
length ps to (length ps) + 1

nsteps (2 * (length ps)) te (Ter ExcState ps) == (Ter ExcState [])
nsteps ((2 * (length ps)) - 1) te (step simp (Ter ExcState ps)) == (Ter ExcState [])
nsteps ((2 * (length ps)) - 1) te (Exec (apply returneffects ts s)::ps’) == (Ter ExcState [])
nsteps ((2 * (length ps)) - 1) te (Exec s’::ps’) == (Ter ExcState [])
nsteps ((2 * (length ps)) - 2) te (step simp (Exec s’::ps’)) == (Ter ExcState [])
nsteps ((2 * (length ps)) - 2) te (Ter (ExcState ps’)) == (Ter ExcState [])
nsteps (2 * ((length ps) - 1)) te (Ter (ExcState ps’)) == (Ter ExcState [])
nsteps (2 * (length ps’)) te (Ter (ExcState ps’)) == (Ter ExcState [])
\end{verbatim}

\end{document}