Changeset 3352

Timestamp:

Jun 14, 2013, 1:13:57 PM (6 years ago)

Author:

boender

Message:

• nicified formulas

File:

• src/ASM/CPP2012-policy/proof.tex (modified) (7 diffs)

src/ASM/CPP2012-policy/proof.tex

@@ -4 +4 @@
 detail.  The main correctness statement is as follows (slightly simplified, here):
 
-
-\begin{align*}
-& \mathtt{sigma\_policy\_specification} \equiv
-\lambda program.\lambda sigma.\lambda policy. \notag\\
-  & sigma\ 0 = 0\ \wedge \notag\\
-        & \mathbf{let} \ instr\_list \equiv code\ program\ \mathbf{in} \notag\\
-        & \forall ppc.ppc < |instr\_list| \rightarrow \notag\\
-        & \mathbf{let}\ pc \equiv sigma\ ppc\ \mathbf{in} \notag\\
-        & \mathbf{let}\ instruction \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc\ \mathbf{in} \notag\\
-        & \mathbf{let}\ next\_pc \equiv sigma\ (ppc+1)\ \mathbf{in}\notag\\
-        &       next\_pc = pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction\ \wedge\notag\\
-  & (pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction < 2^{16}\ \vee\notag\\
-  &     (\forall ppc'.ppc' < |instr\_list| \rightarrow ppc < ppc' \rightarrow \notag\\
-        & \mathbf{let}\ instruction' \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc'\ ppc\_ok'\ \mathbf{in} \notag\\
-        &\ mathtt{instruction\_size}\ sigma\ policy\ ppc'\ instruction' = 0)\ \wedge \notag\\
-        & pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction = 2^{16})
-\end{align*}
+\begin{alignat*}{6}
+\mathtt{sigma}&\omit\rlap{$\mathtt{\_policy\_specification} \equiv
+\lambda program.\lambda sigma.\lambda policy.$} \notag\\
+  & \omit\rlap{$sigma\ 0 = 0\ \wedge$} \notag\\
+        & \mathbf{let}\ & & \omit\rlap{$instr\_list \equiv code\ program\ \mathbf{in}$} \notag\\
+        &&& \omit\rlap{$\forall ppc.ppc < |instr\_list| \rightarrow$} \notag\\
+        &&& \mathbf{let}\ && pc \equiv sigma\ ppc\ \mathbf{in} \notag\\
+        &&& \mathbf{let}\ && instruction \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc\ \mathbf{in} \notag\\
+        &&& \mathbf{let}\ && next\_pc \equiv sigma\ (ppc+1)\ \mathbf{in}\notag\\
+        &&&&& next\_pc = pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction\ \wedge\notag\\
+  &&&&& (pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction < 2^{16}\ \vee\notag\\
+  &&&&& (\forall ppc'.ppc' < |instr\_list| \rightarrow ppc < ppc' \rightarrow \notag\\
+        &&&&& \mathbf{let}\ instruction' \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc'\ ppc\_ok'\ \mathbf{in} \notag\\
+        &&&&&\ \mathtt{instruction\_size}\ sigma\ policy\ ppc'\ instruction' = 0)\ \wedge \notag\\
+        &&&&& pc + (\mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction = 2^{16}))
+\end{alignat*}
 
 Informally, this means that when fetching a pseudo-instruction at $ppc$, the
@@ -70 +69 @@
 acual $\sigma$ trie.
 
-\begin{align*}
-& \mathtt{out\_of\_program\_none} \equiv \lambda prefix.\lambda sigma. \notag\\
+\begin{alignat*}{2}
+\mathtt{out} & \mathtt{\_of\_program\_none} \equiv \lambda prefix.\lambda sigma. \notag\\
 & \forall i.i < 2^{16} \rightarrow (i > |prefix| \leftrightarrow
  \mathtt{lookup\_opt}\ i\ (\mathtt{snd}\ sigma) = \mathtt{None})
-\end{align*}
+\end{alignat*}
 
 This invariant states that any pseudo-address not yet examined is not
 present in the lookup trie.
 
-\begin{align*}
-& \mathtt{not\_jump\_default} \equiv \lambda prefix.\lambda sigma.\notag\\
+\begin{alignat*}{2}
+\mathtt{not} & \mathtt{\_jump\_default} \equiv \lambda prefix.\lambda sigma.\notag\\
 & \forall i.i < |prefix| \rightarrow\notag\\
 & \neg\mathtt{is\_jump}\ (\mathtt{nth}\ i\ prefix) \rightarrow\notag\\
 & \mathtt{lookup}\ i\ (\mathtt{snd}\ sigma) = \mathtt{short\_jump}
-\end{align*}
+\end{alignat*}
 
 This invariant states that when we try to look up the jump length of a
@@ -90 +89 @@
 value, a short jump.
 
-\begin{align*}
-& \mathtt{jump\_increase} \equiv \lambda pc.\lambda op.\lambda p.
-        \forall i.i < |prefix| \rightarrow\notag\\      
-&       \mathbf{let}\ oj \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ op)\ \mathbf{in} \notag\\
-&       \mathbf{let}\ j \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ p)\ \mathbf{in} \notag\\
-&       \mathtt{jmpleq}\ oj\ j
-\end{align*}
+\begin{alignat*}{4}
+\mathtt{jump} & \omit\rlap{$\mathtt{\_increase} \equiv \lambda pc.\lambda op.\lambda p.$} \notag\\
+        & \omit\rlap{$\forall i.i < |prefix| \rightarrow$} \notag\\     
+&       \mathbf{let}\  && oj \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ op)\ \mathbf{in} \notag\\
+&       \mathbf{let}\ && j \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ p)\ \mathbf{in} \notag\\
+&&&     \mathtt{jmpleq}\ oj\ j
+\end{alignat*}
 
 This invariant states that between iterations (with $op$ being the previous
@@ -102 +101 @@
 increase. It is needed for proving termination.
 
-\begin{align*}
-& \mathtt{sigma\_compact\_unsafe} \equiv \lambda prefix.\lambda sigma.\notag\\
-& \forall n.n < |prefix| \rightarrow\notag\\
-& \mathbf{match}\ \mathtt{lookup\_opt}\ n\ (\mathtt{snd}\ sigma)\ \mathbf{with}\notag\\
-& \mathtt{None} \Rightarrow \mathrm{False} \notag\\
-& \mathtt{Some}\ \langle pc, j \rangle \Rightarrow
-        \mathbf{match}\ \mathtt{lookup\_opt}\ (n+1)\ (\mathtt{snd}\ sigma)\ \mathbf{with}\notag\\
-& \mathtt{None} \Rightarrow \mathrm{False} \notag\\
-& \mathtt{Some}\ \langle pc_1, j_1 \rangle \Rightarrow
-                pc_1 = pc + \mathtt{instruction\_size\_jmplen}\ j\ (\mathtt{nth}\ n\ prefix)
-\end{align*}
+\begin{alignat*}{6}
+\mathtt{sigma} & \omit\rlap{$\mathtt{\_compact\_unsafe} \equiv \lambda prefix.\lambda sigma.$}\notag\\
+& \omit\rlap{$\forall n.n < |prefix| \rightarrow$}\notag\\
+& \mathbf{match}\ && \omit\rlap{$\mathtt{lookup\_opt}\ n\ (\mathtt{snd}\ sigma)\ \mathbf{with}$}\notag\\
+&&& \omit\rlap{$\mathtt{None} \Rightarrow \mathrm{False}$} \notag\\
+&&& \omit\rlap{$\mathtt{Some}\ \langle pc, j \rangle \Rightarrow$} \notag\\
+&&& \mathbf{match}\ && \mathtt{lookup\_opt}\ (n+1)\ (\mathtt{snd}\ sigma)\ \mathbf{with}\notag\\
+&&&&& \mathtt{None} \Rightarrow \mathrm{False} \notag\\
+&&&&& \mathtt{Some}\ \langle pc_1, j_1 \rangle \Rightarrow
+                pc_1 = pc + \notag\\
+&&&&& \ \ \mathtt{instruction\_size\_jmplen}\ j\ (\mathtt{nth}\ n\ prefix)
+\end{alignat*}
 
 This is a temporary formulation of the main property\\
@@ -124 +124 @@
 property.
 
-\begin{align*}
-& \mathtt{sigma\_safe} \equiv \lambda prefix.\lambda labels.\lambda old\_sigma.\lambda sigma\notag\\
-& \forall i.i < |prefix| \rightarrow \notag\\
-& \mathbf{let}\ instr \equiv \mathtt{nth}\ i\ prefix\ \mathbf{in}\notag\\
-& \forall dest\_label.\mathtt{is\_jump\_to\_instr}\ dest\_label \rightarrow\notag\\
-& \mathbf{let}\ paddr \equiv \mathtt{lookup}\ labels\ dest\_label\ \mathbf{in} \notag\\
-& \mathbf{let}\ \langle j, src, dest \rangle \equiv\notag\\
-& \mathbf{if}\ paddr\ \leq\ i\ \mathbf{then}\notag\\
-& \mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ sigma)\ \mathbf{in} \notag\\
-& \mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ (\mathtt{snd}\ sigma)\ \mathbf{in}\notag\\
-& \mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ (\mathtt{snd}\ sigma)\ \mathbf{in}\notag\\
-&       \langle j, pc\_plus\_jl, addr \rangle\notag\\
-&\mathbf{else} \notag\\
-&\mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ sigma)\ \mathbf{in} \notag\\
-&\mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ (\mathtt{snd}\ old\_sigma)\ \mathbf{in}\notag\\
-&\mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ (\mathtt{snd}\ old\_sigma)\ \mathbf{in}\notag\\
-&\langle j, pc\_plus\_jl, addr \rangle\ \mathbf{in}\notag\\
-&\mathbf{match}\ j\ \mathbf{with} \notag\\
-&\mathrm{short\_jump} \Rightarrow \mathtt{short\_jump\_valid}\ src\ dest\notag\\
-&\mathrm{absolute\_jump} \Rightarrow \mathtt{absolute\_jump\_valid}\ src\ dest\notag\\
-&\mathrm{long\_jump} \Rightarrow \mathrm{True}
-\end{align*}
+\begin{alignat*}{6}
+\mathtt{sigma} & \omit\rlap{$\mathtt{\_safe} \equiv \lambda prefix.\lambda labels.\lambda old\_sigma.\lambda sigma$}\notag\\
+& \omit\rlap{$\forall i.i < |prefix| \rightarrow$} \notag\\
+& \omit\rlap{$\forall dest\_label.\mathtt{is\_jump\_to\ (\mathtt{nth}\ i\ prefix})\ dest\_label \rightarrow$} \notag\\
+& \mathbf{let} && \omit\rlap{$\ paddr \equiv \mathtt{lookup}\ labels\ dest\_label\ \mathbf{in}$} \notag\\
+& \mathbf{let} && \omit\rlap{$\ \langle j, src, dest \rangle \equiv$}\notag\\
+&&& \omit\rlap{$\mathbf{if} \ paddr\ \leq\ i\ \mathbf{then}$}\notag\\
+&&&&& \mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ sigma)\ \mathbf{in} \notag\\
+&&&&& \mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ (\mathtt{snd}\ sigma)\ \mathbf{in}\notag\\
+&&&&& \mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ (\mathtt{snd}\ sigma)\ \mathbf{in}\notag\\
+&&&&&   \langle j, pc\_plus\_jl, addr \rangle\notag\\
+&&&\mathbf{else} \notag\\
+&&&&&\mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ sigma)\ \mathbf{in} \notag\\
+&&&&&\mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ (\mathtt{snd}\ old\_sigma)\ \mathbf{in}\notag\\
+&&&&&\mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ (\mathtt{snd}\ old\_sigma)\ \mathbf{in}\notag\\
+&&&&&\langle j, pc\_plus\_jl, addr \rangle\notag\\
+&&&\omit\rlap{$\mathbf{in}$}\notag\\
+&&&\mathbf{match} && \ j\ \mathbf{with} \notag\\
+&&&&&\mathrm{short\_jump} \Rightarrow \mathtt{short\_jump\_valid}\ src\ dest\notag\\
+&&&&&\mathrm{absolute\_jump} \Rightarrow \mathtt{absolute\_jump\_valid}\ src\ dest\notag\\
+&&&&&\mathrm{long\_jump} \Rightarrow \mathrm{True}
+\end{alignat*}
 
 This is a more direct safety property: it states that branch instructions are
@@ -201 +201 @@
 If an iteration returns {\tt None}, we have the following invariant:
 
-\begin{align*}
-& \mathtt{nec\_plus\_ultra} \equiv \lambda program.\lambda p. \notag\\
+\begin{alignat*}{2}
+\mathtt{nec} & \mathtt{\_plus\_ultra} \equiv \lambda program.\lambda p. \notag\\
 &\neg(\forall i.i < |program|\ \rightarrow \notag\\
 & \mathtt{is\_jump}\ (\mathtt{nth}\ i\ program)\ \rightarrow \notag\\
 & \mathtt{lookup}\ i\ (\mathtt{snd}\ p) = \mathrm{long\_jump}).
-\end{align*}
+\end{alignat*}
 
 This invariant is applied to $old\_sigma$; if our program becomes too large
@@ -221 +221 @@
 invariant:
 
-\begin{align*}
-& \mathtt{sigma\_compact} \equiv \lambda program.\lambda sigma. \notag\\
-& \forall n.n < |program|\ \rightarrow \notag\\
-& \mathbf{match}\ \mathtt{lookup\_opt}\ n\ (\mathtt{snd}\ sigma)\ \mathbf{with}\notag\\
-& \mathrm{None}\ \Rightarrow\ \mathrm{False}\notag\\
-& \mathrm{Some}\ \langle pc, j \rangle \Rightarrow\notag\\
-& \mathbf{match}\ \mathtt{lookup\_opt}\ (n+1)\ (\mathtt{snd}\ sigma)\ \mathbf{with}\notag\\
-&       \mathrm{None}\ \Rightarrow\ \mathrm{False}\notag\\
-& \mathrm{Some} \langle pc1, j1 \rangle \Rightarrow\notag\\
-& pc1 = pc + \mathtt{instruction\_size}\ n\ (\mathtt{nth}\ n\ program)
-\end{align*}
+\begin{alignat*}{6}
+\mathtt{sigma} & \omit\rlap{$\mathtt{\_compact} \equiv \lambda program.\lambda sigma.$} \notag\\
+& \omit\rlap{$\forall n.n < |program|\ \rightarrow$} \notag\\
+& \mathbf{match}\ && \omit\rlap{$\mathtt{lookup\_opt}\ n\ (\mathtt{snd}\ sigma)\ \mathbf{with}$}\notag\\
+&&& \omit\rlap{$\mathrm{None}\ \Rightarrow\ \mathrm{False}$}\notag\\
+&&& \omit\rlap{$\mathrm{Some}\ \langle pc, j \rangle \Rightarrow$}\notag\\
+&&& \mathbf{match}\ && \mathtt{lookup\_opt}\ (n+1)\ (\mathtt{snd}\ sigma)\ \mathbf{with}\notag\\
+&&&&&   \mathrm{None}\ \Rightarrow\ \mathrm{False}\notag\\
+&&&&& \mathrm{Some} \langle pc1, j1 \rangle \Rightarrow\notag\\
+&&&&& \ \ pc1 = pc + \mathtt{instruction\_size}\ n\ (\mathtt{nth}\ n\ program)
+\end{alignat*}