Secure diffuse computing: class #5


Structural induction, see Wikipedia.

Lemma 1.1

Let e be a BabyImp expression and let $eT[1..j]$ be Cexpr(e). For all state σ if

\begin{align} [[e]] \sigma = v \end{align}

then for all stacks s:

\begin{align} <i, s, \sigma> \rightarrow^* <j + 1, v::s, \sigma> \end{align}

By structural induction on source expressions.

Base case: x, v

Inductive case: e op e'

Base case

Hypothesis 1: $e \equiv x$

Hypothesis 2: $[[ x ]] \sigma = \sigma(x)$

Hypothesis 3: $\xi \textrm{expr} (x) = \textrm{load} x$

By semantics of target language:

\begin{align} <i, s, \sigma> \rightarrow <i + 1, \sigma(x)::s, \sigma> \end{align}

Inductive case

Hypothesis 1: $e \equiv e_1 \textrm{op} e_2$

Inductive hypothesis: the lemma holds for $e_1$ and $e_2$.

Hypothesis 3:

\begin{align} [[e_1 \textrm{op} e_2]]\sigma = [[e_1]]\sigma \textrm{op} [[e_2]]\sigma \end{align}

Hypothesis 4:

\begin{align} ET[i..j] = E_2[i..j_{e_2}]::E_1[i_{e_i}+1..j-1]::\textrm{primop} \end{align}

(lost this part…)

Unclear, need to ask the teachers, since most is obviously derived works.