Changeset 2080 for src/ASM/CPP2012policy/proof.tex
 Timestamp:
 Jun 14, 2012, 11:57:51 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2012policy/proof.tex
r2065 r2080 81 81 82 82 \begin{lstlisting} 83 definition jump_expansion': 84 $\forall$program:preamble $\times$ ($\Sigma$l:list labelled_instruction.S (l) < 2^16). 85 option ($\Sigma$sigma:Word → Word $\times$ bool. 86 $\forall$ppc: Word.$\forall$ppc_ok. 87 let pc := \fst (sigma ppc) in 88 let labels := \fst (create_label_cost_map (\snd program)) in 89 let lookup_labels := 90 $\lambda$x.bitvector_of_nat ? (lookup_def ?? labels x 0) in 91 let instruction := 92 \fst (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in 93 let next_pc := \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in 94 And (nat_of_bitvector $\ldots$ ppc $\leq$ \snd program → 95 next_pc = add ? pc (bitvector_of_nat $\ldots$ 96 (instruction_size lookup_labels ($\lambda$x.\fst (sigma x)) 97 ($\lambda$x.\snd (sigma x)) ppc instruction)) 98 ) 99 (Or (nat_of_bitvector $\ldots$ ppc < \snd program → 100 nat_of_bitvector $\ldots$ pc < nat_of_bitvector $\ldots$ next_pc) 101 (nat_of_bitvector $\ldots$ ppc = \snd program → next_pc = (zero $\ldots$)))) 83 definition sigma_policy_specification :=: 84 $\lambda$program: pseudo_assembly_program. 85 $\lambda$sigma: Word → Word. 86 $\lambda$policy: Word → bool. 87 sigma (zero $\ldots$) = zero $\ldots$ $\wedge$ 88 $\forall$ppc: Word.$\forall$ppc_ok. 89 let instr_list := \snd program in 90 let pc ≝ sigma ppc in 91 let labels := \fst (create_label_cost_map (\snd program)) in 92 let lookup_labels := 93 $\lambda$x.bitvector_of_nat ? (lookup_def ?? labels x 0) in 94 let instruction := 95 \fst (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in 96 let next_pc := \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in 97 (nat_of_bitvector $\ldots$ ppc ≤ instr_list → 98 next_pc = add 16 pc (bitvector_of_nat $\ldots$ 99 (instruction_size lookup_labels sigma policy ppc instruction))) 100 $\wedge$ 101 ((nat_of_bitvector $\ldots$ ppc < instr_list → 102 nat_of_bitvector $\ldots$ pc < nat_of_bitvector $\ldots$ next_pc) 103 $\vee$ (nat_of_bitvector $\ldots$ ppc = instr_list → next_pc = (zero $\ldots$))). 102 104 \end{lstlisting} 103 105 … … 113 115 address can be zero (this is the case where the program size is exactly equal 114 116 to the amount of memory). 117 118 And finally, we enforce that the program starts at address 0, i.e. 119 $\sigma(0) = 0$.
Note: See TracChangeset
for help on using the changeset viewer.