Secure diffuse computing: class #5

Structural induction, see Wikipedia.

## Lemma 1.1

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

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

then for all stacks s:

(2)\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:

(3)\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:

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

Hypothesis 4:

(5)\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…)

page revision: 3, last edited: 18 Nov 2009 13:01