Changeset 957 for src/ASM/CPP2011/cpp2011.tex
 Timestamp:
 Jun 15, 2011, 1:30:54 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2011/cpp2011.tex
r956 r957 4 4 \usepackage[english]{babel} 5 5 \usepackage[colorlinks]{hyperref} 6 \usepackage[utf8x]{inputenc} 7 \usepackage{listings} 8 9 \newlength{\mylength} 10 \newenvironment{frametxt}% 11 {\setlength{\fboxsep}{5pt} 12 \setlength{\mylength}{\linewidth}% 13 \addtolength{\mylength}{2\fboxsep}% 14 \addtolength{\mylength}{2\fboxrule}% 15 \Sbox 16 \minipage{\mylength}% 17 \setlength{\abovedisplayskip}{0pt}% 18 \setlength{\belowdisplayskip}{0pt}% 19 }% 20 {\endminipage\endSbox 21 \[\fbox{\TheSbox}\]} 22 23 %\lstdefinelanguage{matitaocaml} 24 % {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try,on,to}, 25 % morekeywords={[2]whd,normalize,elim,cases,destruct}, 26 % morekeywords={[3]type,of,val,assert,let,function}, 27 % mathescape=true, 28 % } 29 %\lstset{language=matitaocaml,basicstyle=\footnotesize\tt,columns=flexible,breaklines=false, 30 % keywordstyle=\bfseries, %\color{red}\bfseries, 31 % keywordstyle=[2]\bfseries, %\color{blue}, 32 % keywordstyle=[3]\bfseries, %\color{blue}\bfseries, 33 %% commentstyle=\color{green}, 34 %% stringstyle=\color{blue}, 35 % showspaces=false,showstringspaces=false} 36 %\DeclareUnicodeCharacter{8797}{:=} 37 %\DeclareUnicodeCharacter{8797}{:=} 38 %\DeclareUnicodeCharacter{10746}{++} 39 %\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}} 40 %\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}} 41 42 %\lstset{ 43 % extendedchars=false, 44 % inputencoding=utf8x, 45 % tabsize=1 46 %} 47 48 \renewcommand{\verb}{\lstinline} 49 \def\lstlanguagefiles{lstgrafite.tex} 50 \lstset{language=Grafite} 6 51 7 52 \title{On the correctness of an assembler for the Intel MCS51 microprocessor} … … 164 209 \end{itemize} 165 210 211 \begin{lstlisting} 212 definition execute_1_pseudo_instruction: PseudoStatus → PseudoStatus 213 \end{lstlisting} 214 215 \begin{lstlisting} 216 definition execute: nat → Status → Status 217 \end{lstlisting} 218 219 \begin{lstlisting} 220 inductive jump_length: Type[0] ≝ 221  short_jump: jump_length 222  medium_jump: jump_length 223  long_jump: jump_length. 224 225 definition jump_expansion_policy ≝ BitVectorTrie jump_length 16. 226 \end{lstlisting} 227 228 \begin{lstlisting} 229 definition policy_ok := λpolicy.λp. sigma_safe policy p <> None .... 230 \end{lstlisting} 231 232 \begin{lstlisting} 233 definition sigma: 234 ∀p:pseudo_assembly_program. 235 ∀policy. policy_ok policy p. Word → Word 236 \end{lstlisting} 237 238 \begin{lstlisting} 239 axiom low_internal_ram_of_pseudo_low_internal_ram: 240 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7. 241 \end{lstlisting} 242 243 CSC: no option using policy 244 \begin{lstlisting} 245 definition status_of_pseudo_status: 246 internal_pseudo_address_map → PseudoStatus → option Status 247 \end{lstlisting} 248 249 \begin{lstlisting} 250 definition next_internal_pseudo_address_map0: 251 internal_pseudo_address_map → PseudoStatus → option internal_pseudo_address_map 252 \end{lstlisting} 253 254 CSC: no 2nd, 3rd options using policy 255 \begin{lstlisting} 256 ∀M,M',ps,s,s''. 257 next_internal_pseudo_address_map M ps = Some ... M' → 258 status_of_pseudo_status M ps = Some ... s → 259 status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory ... ps)) ps) = Some ... s'' → 260 ∃n. execute n s = s''. 261 \end{lstlisting} 262 263 CSC: no options using policy 264 \begin{lstlisting} 265 lemma fetch_assembly_pseudo2: 266 ∀program,assembled,costs,labels. 267 Some ... LANGLElabels,costsRANGLE = build_maps program → 268 Some ... LANGLEassembled,costsRANGLE = assembly program → 269 ∀ppc. 270 let code_memory ≝ load_code_memory assembled in 271 let preamble ≝ \fst program in 272 let data_labels ≝ construct_datalabels preamble in 273 let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in 274 let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in 275 let expansion ≝ jump_expansion ppc program in 276 let LANGLEpi,newppcRANGLE ≝ fetch_pseudo_instruction (\snd program) ppc in 277 ∃instructions. 278 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi ∧ 279 fetch_many code_memory (sigma program newppc) (sigma program ppc) instructions. 280 \end{lstlisting} 281 282 \begin{lstlisting} 283 definition expand_pseudo_instruction: 284 ∀lookup_labels.∀lookup_datalabels.∀pc.∀policy_decision. (sigma program ppc) expansion. pseudo_instruciton > list instruction. 285 \end{lstlisting} 286 287 \begin{lstlisting} 288 axiom assembly_ok_to_expand_pseudo_instruction_ok: 289 ∀program,assembled,costs. 290 Some ... LANGLEassembled,costsRANGLE = assembly program → 291 ∀ppc. 292 let code_memory ≝ load_code_memory assembled in 293 let preamble ≝ \fst program in 294 let data_labels ≝ construct_datalabels preamble in 295 let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in 296 let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in 297 let expansion ≝ jump_expansion ppc program in 298 let LANGLEpi,newppcRANGLE ≝ fetch_pseudo_instruction (\snd program) ppc in 299 ∃instructions. 300 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi. 301 \end{lstlisting} 302 303 \begin{lstlisting} 304 axiom assembly_ok: 305 ∀program,assembled,costs,labels. 306 Some ... LANGLElabels,costsRANGLE = build_maps program → 307 Some ... LANGLEassembled,costsRANGLE = assembly program → 308 let code_memory ≝ load_code_memory assembled in 309 let preamble ≝ \fst program in 310 let datalabels ≝ construct_datalabels preamble in 311 let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in 312 let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in 313 ∀ppc,len,assembledi. 314 let LANGLEpi,newppcRANGLE ≝ fetch_pseudo_instruction (\snd program) ppc in 315 Some ... LANGLElen,assemblediRANGLE = assembly_1_pseudoinstruction program ppc (sigma program ppc) lookup_labels lookup_datalabels pi → 316 encoding_check code_memory (sigma program ppc) (bitvector_of_nat ... (nat_of_bitvector ... (sigma program ppc) + len)) assembledi ∧ 317 sigma program newppc = bitvector_of_nat ... (nat_of_bitvector ... (sigma program ppc) + len). 318 \end{lstlisting} 319 320 \begin{lstlisting} 321 lemma fetch_assembly_pseudo: 322 ∀program,ppc,lookup_labels,lookup_datalabels. 323 ∀pi,code_memory,len,assembled,instructions,pc. 324 let expansion ≝ jump_expansion ppc program in 325 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (bitvector_of_nat ? pc) expansion pi → 326 Some ... LANGLElen,assembledRANGLE = assembly_1_pseudoinstruction program ppc (bitvector_of_nat ? pc) lookup_labels lookup_datalabels pi → 327 encoding_check code_memory (bitvector_of_nat ... pc) (bitvector_of_nat ... (pc + len)) assembled → 328 fetch_many code_memory (bitvector_of_nat ... (pc + len)) (bitvector_of_nat ... pc) instructions. 329 \end{lstlisting} 330 331 \begin{lstlisting} 332 theorem fetch_assembly: 333 ∀pc,i,code_memory,assembled. 334 assembled = assembly1 i → 335 let len ≝ length ... assembled in 336 encoding_check code_memory (bitvector_of_nat ... pc) (bitvector_of_nat ... (pc + len)) assembled → 337 let fetched ≝ fetch code_memory (bitvector_of_nat ... pc) in 338 let LANGLEinstr_pc, ticksRANGLE ≝ fetched in 339 let LANGLEinstr,pc'RANGLE ≝ instr_pc in 340 (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv ... pc' (bitvector_of_nat ... (pc + len))) = true. 341 \end{lstlisting} 342 166 343 %  % 167 344 % SECTION %
Note: See TracChangeset
for help on using the changeset viewer.