Changeset 957 for src/ASM/CPP2011

Timestamp:

Jun 15, 2011, 1:30:54 PM (9 years ago)

Author:

sacerdot

Message:

...

File:

• src/ASM/CPP2011/cpp-2011.tex (modified) (2 diffs)

src/ASM/CPP2011/cpp-2011.tex

@@ -4 +4 @@
 \usepackage[english]{babel}
 \usepackage[colorlinks]{hyperref}
+\usepackage[utf8x]{inputenc}
+\usepackage{listings}
+
+\newlength{\mylength}
+\newenvironment{frametxt}%
+        {\setlength{\fboxsep}{5pt}
+                \setlength{\mylength}{\linewidth}%
+                \addtolength{\mylength}{-2\fboxsep}%
+                \addtolength{\mylength}{-2\fboxrule}%
+                \Sbox
+                \minipage{\mylength}%
+                        \setlength{\abovedisplayskip}{0pt}%
+                        \setlength{\belowdisplayskip}{0pt}%
+                }%
+                {\endminipage\endSbox
+                        \[\fbox{\TheSbox}\]}
+
+%\lstdefinelanguage{matita-ocaml}
+%  {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try,on,to},
+%   morekeywords={[2]whd,normalize,elim,cases,destruct},
+%   morekeywords={[3]type,of,val,assert,let,function},
+%   mathescape=true,
+%  }
+%\lstset{language=matita-ocaml,basicstyle=\footnotesize\tt,columns=flexible,breaklines=false,
+%        keywordstyle=\bfseries, %\color{red}\bfseries,
+%        keywordstyle=[2]\bfseries, %\color{blue},
+%        keywordstyle=[3]\bfseries, %\color{blue}\bfseries,
+%%        commentstyle=\color{green},
+%%        stringstyle=\color{blue},
+%        showspaces=false,showstringspaces=false}
+%\DeclareUnicodeCharacter{8797}{:=}
+%\DeclareUnicodeCharacter{8797}{:=}
+%\DeclareUnicodeCharacter{10746}{++}
+%\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
+%\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}
+
+%\lstset{
+%  extendedchars=false,
+%  inputencoding=utf8x,
+%  tabsize=1
+%}
+
+\renewcommand{\verb}{\lstinline}
+\def\lstlanguagefiles{lst-grafite.tex}
+\lstset{language=Grafite}
 
 \title{On the correctness of an assembler for the Intel MCS-51 microprocessor}
@@ -164 +209 @@
   \end{itemize}
 
+\begin{lstlisting}
+ definition execute_1_pseudo_instruction: PseudoStatus → PseudoStatus
+\end{lstlisting}
+
+\begin{lstlisting}
+ definition execute: nat → Status → Status
+\end{lstlisting}
+
+\begin{lstlisting}
+inductive jump_length: Type[0] ≝
+  | short_jump: jump_length
+  | medium_jump: jump_length
+  | long_jump: jump_length.
+
+definition jump_expansion_policy ≝ BitVectorTrie jump_length 16.
+\end{lstlisting}
+
+\begin{lstlisting}
+definition policy_ok := λpolicy.λp. sigma_safe policy p <> None ....
+\end{lstlisting}
+
+\begin{lstlisting}
+definition sigma:
+ ∀p:pseudo_assembly_program.
+  ∀policy. policy_ok policy p. Word → Word
+\end{lstlisting}
+
+\begin{lstlisting}
+axiom low_internal_ram_of_pseudo_low_internal_ram:
+ ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
+\end{lstlisting}
+
+CSC: no option using policy 
+\begin{lstlisting}
+definition status_of_pseudo_status:
+ internal_pseudo_address_map → PseudoStatus → option Status
+\end{lstlisting}
+
+\begin{lstlisting}
+definition next_internal_pseudo_address_map0:
+ internal_pseudo_address_map → PseudoStatus → option internal_pseudo_address_map
+\end{lstlisting}
+
+CSC: no 2nd, 3rd options using policy 
+\begin{lstlisting}
+ ∀M,M',ps,s,s''.
+  next_internal_pseudo_address_map M ps = Some ... M' →
+  status_of_pseudo_status M ps = Some ... s →
+  status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory ... ps)) ps) = Some ... s'' →
+   ∃n. execute n s = s''.
+\end{lstlisting}
+
+CSC: no options using policy 
+\begin{lstlisting}
+lemma fetch_assembly_pseudo2:
+ ∀program,assembled,costs,labels.
+  Some ... LANGLElabels,costsRANGLE = build_maps program →
+  Some ... LANGLEassembled,costsRANGLE = assembly program →
+   ∀ppc.
+    let code_memory ≝ load_code_memory assembled in
+    let preamble ≝ \fst program in
+    let data_labels ≝ construct_datalabels preamble in
+    let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
+    let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
+    let expansion ≝ jump_expansion ppc program in
+    let LANGLEpi,newppcRANGLE ≝ fetch_pseudo_instruction (\snd program) ppc in
+     ∃instructions.
+      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi ∧
+       fetch_many code_memory (sigma program newppc) (sigma program ppc) instructions.
+\end{lstlisting}
+
+\begin{lstlisting}
+ definition expand_pseudo_instruction:
+  ∀lookup_labels.∀lookup_datalabels.∀pc.∀policy_decision. (sigma program ppc) expansion. pseudo_instruciton -> list instruction.
+\end{lstlisting}
+
+\begin{lstlisting}
+axiom assembly_ok_to_expand_pseudo_instruction_ok:
+ ∀program,assembled,costs.
+  Some ... LANGLEassembled,costsRANGLE = assembly program →
+   ∀ppc.
+    let code_memory ≝ load_code_memory assembled in
+    let preamble ≝ \fst program in   
+    let data_labels ≝ construct_datalabels preamble in
+    let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
+    let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
+    let expansion ≝ jump_expansion ppc program in
+    let LANGLEpi,newppcRANGLE ≝ fetch_pseudo_instruction (\snd program) ppc in
+     ∃instructions.
+      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi.
+\end{lstlisting}
+
+\begin{lstlisting}
+axiom assembly_ok:
+ ∀program,assembled,costs,labels.
+  Some ... LANGLElabels,costsRANGLE = build_maps program →
+  Some ... LANGLEassembled,costsRANGLE = assembly program →
+  let code_memory ≝ load_code_memory assembled in
+  let preamble ≝ \fst program in
+  let datalabels ≝ construct_datalabels preamble in
+  let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
+  let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in
+   ∀ppc,len,assembledi.
+    let LANGLEpi,newppcRANGLE ≝ fetch_pseudo_instruction (\snd program) ppc in
+     Some ... LANGLElen,assemblediRANGLE = assembly_1_pseudoinstruction program ppc (sigma program ppc) lookup_labels lookup_datalabels pi →
+      encoding_check code_memory (sigma program ppc) (bitvector_of_nat ... (nat_of_bitvector ... (sigma program ppc) + len)) assembledi ∧
+       sigma program newppc = bitvector_of_nat ... (nat_of_bitvector ... (sigma program ppc) + len).
+\end{lstlisting}
+
+\begin{lstlisting}
+lemma fetch_assembly_pseudo:
+ ∀program,ppc,lookup_labels,lookup_datalabels.
+  ∀pi,code_memory,len,assembled,instructions,pc.
+   let expansion ≝ jump_expansion ppc program in
+   Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (bitvector_of_nat ? pc) expansion pi →
+    Some ... LANGLElen,assembledRANGLE = assembly_1_pseudoinstruction program ppc (bitvector_of_nat ? pc) lookup_labels lookup_datalabels pi →
+     encoding_check code_memory (bitvector_of_nat ... pc) (bitvector_of_nat ... (pc + len)) assembled →
+      fetch_many code_memory (bitvector_of_nat ... (pc + len)) (bitvector_of_nat ... pc) instructions.
+\end{lstlisting}
+
+\begin{lstlisting}
+theorem fetch_assembly:
+  ∀pc,i,code_memory,assembled.
+    assembled = assembly1 i →
+      let len ≝ length ... assembled in
+      encoding_check code_memory (bitvector_of_nat ... pc) (bitvector_of_nat ... (pc + len)) assembled →
+      let fetched ≝ fetch code_memory (bitvector_of_nat ... pc) in
+      let LANGLEinstr_pc, ticksRANGLE ≝ fetched in
+      let LANGLEinstr,pc'RANGLE ≝ instr_pc in
+       (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv ... pc' (bitvector_of_nat ... (pc + len))) = true.
+\end{lstlisting}
+
 % ---------------------------------------------------------------------------- %
 % SECTION                                                                      %