Changeset 3352

Ignore:
Timestamp:
Jun 14, 2013, 1:13:57 PM (6 years ago)
Message:
• nicified formulas
File:
1 edited

Legend:

Unmodified
 r3342 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 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 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 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\\ 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 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 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*}