Changeset 957


Ignore:
Timestamp:
Jun 15, 2011, 1:30:54 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2011/cpp-2011.tex

    r956 r957  
    44\usepackage[english]{babel}
    55\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{matita-ocaml}
     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=matita-ocaml,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{lst-grafite.tex}
     50\lstset{language=Grafite}
    651
    752\title{On the correctness of an assembler for the Intel MCS-51 microprocessor}
     
    164209  \end{itemize}
    165210
     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}
     220inductive jump_length: Type[0] ≝
     221  | short_jump: jump_length
     222  | medium_jump: jump_length
     223  | long_jump: jump_length.
     224
     225definition jump_expansion_policy ≝ BitVectorTrie jump_length 16.
     226\end{lstlisting}
     227
     228\begin{lstlisting}
     229definition policy_ok := λpolicy.λp. sigma_safe policy p <> None ....
     230\end{lstlisting}
     231
     232\begin{lstlisting}
     233definition sigma:
     234 ∀p:pseudo_assembly_program.
     235  ∀policy. policy_ok policy p. Word → Word
     236\end{lstlisting}
     237
     238\begin{lstlisting}
     239axiom 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
     243CSC: no option using policy
     244\begin{lstlisting}
     245definition status_of_pseudo_status:
     246 internal_pseudo_address_map → PseudoStatus → option Status
     247\end{lstlisting}
     248
     249\begin{lstlisting}
     250definition next_internal_pseudo_address_map0:
     251 internal_pseudo_address_map → PseudoStatus → option internal_pseudo_address_map
     252\end{lstlisting}
     253
     254CSC: 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
     263CSC: no options using policy
     264\begin{lstlisting}
     265lemma 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}
     288axiom 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}
     304axiom 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}
     321lemma 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}
     332theorem 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
    166343% ---------------------------------------------------------------------------- %
    167344% SECTION                                                                      %
Note: See TracChangeset for help on using the changeset viewer.