 Timestamp:
 Jun 7, 2013, 5:13:45 PM (6 years ago)
 Location:
 src/ASM/CPP2012policy
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2012policy/main.tex
r3304 r3338 3 3 \usepackage{alltt} 4 4 \usepackage{amsfonts} 5 \usepackage{amsmath} 5 6 \usepackage[british]{babel} 6 7 \usepackage{hyperref} 
src/ASM/CPP2012policy/proof.tex
r2099 r3338 4 4 detail. The main correctness statement is as follows (slightly simplified, here): 5 5 6 \begin{lstlisting} 7 definition sigma_policy_specification := 8 $\lambda$program: pseudo_assembly_program. 9 $\lambda$sigma: Word $\rightarrow$ Word. 10 $\lambda$policy: Word $\rightarrow$ bool. 11 sigma (zero $\ldots$) = zero $\ldots$ $\wedge$ 12 $\forall$ppc: Word.$\forall$ppc_ok. 13 let $\langle$preamble, instr_list$\rangle$ := program in 14 let pc := sigma ppc in 15 let instruction := 16 \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) in 17 let next_pc := \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in 18 (nat_of_bitvector $\ldots$ ppc $\leq$ instr_list $\rightarrow$ 19 next_pc = add ? pc (bitvector_of_nat $\ldots$ 20 (instruction_size $\ldots$ sigma policy ppc instruction))) 21 $\wedge$ 22 ((nat_of_bitvector $\ldots$ ppc < instr_list $\rightarrow$ 23 nat_of_bitvector $\ldots$ pc < nat_of_bitvector $\ldots$ next_pc) 24 $\vee$ (nat_of_bitvector $\ldots$ ppc = instr_list $\rightarrow$ next_pc = (zero $\ldots$))). 25 \end{lstlisting} 6 7 \begin{align*} 8 \mathrm{sigma\_policy\_specification} \equiv 9 \lambda program.\lambda sigma.\lambda policy. \notag\\ 10 sigma\ 0 = 0\ \wedge \notag\\ 11 \mathbf{let}\ instr\_list \equiv code\ program\ \mathbf{in} \notag\\ 12 \forall ppc.ppc < instr\_list \rightarrow \notag\\ 13 \mathbf{let}\ pc \equiv sigma\ ppc\ \mathbf{in} \notag\\ 14 \mathbf{let}\ instruction \equiv \mathrm{fetch\_pseudo\_instruction}\ instr\_list\ ppc\ \mathbf{in} \notag\\ 15 \mathbf{let}\ next\_pc \equiv sigma\ (ppc+1)\ \mathbf{in}\notag\\ 16 next\_pc = pc + \mathrm{instruction\_size}\ sigma\ policy\ ppc\ instruction\ \wedge\notag\\ 17 (pc + \mathrm{instruction\_size}\ sigma\ policy\ ppc\ instruction < 2^{16}\ \vee\notag\\ 18 (\forall ppc'.ppc' < instr\_list \rightarrow ppc < ppc' \rightarrow \notag\\ 19 \mathbf{let}\ instruction' \equiv \mathrm{fetch\_pseudo\_instruction}\ instr\_list\ ppc'\ ppc\_ok'\ \mathbf{in} \notag\\ 20 \mathrm{instruction\_size}\ sigma\ policy\ ppc'\ instruction' = 0)\ \wedge \notag\\ 21 pc + \mathrm{instruction\_size}\ sigma\ policy\ ppc\ instruction = 2^{16}) 22 \end{align*} 26 23 27 24 Informally, this means that when fetching a pseudoinstruction at $ppc$, the … … 68 65 implemented as a trie for ease of access; computing $\sigma(x)$ is achieved by looking 69 66 up the value of $x$ in the trie. Actually, during the fold, the value we 70 pass along is a pair $\mathbb{N} \times \mathtt{ppc _pc_map}$. The first component67 pass along is a pair $\mathbb{N} \times \mathtt{ppc\_pc\_map}$. The first component 71 68 is the number of bytes added to the program so far with respect to 72 69 the previous iteration, and the second component, {\tt ppc\_pc\_map}, is a pair
Note: See TracChangeset
for help on using the changeset viewer.