source: Deliverables/D1.2/Presentations/WP4-dominic.tex @ 1821

Last change on this file since 1821 was 1821, checked in by mulligan, 8 years ago

discussed merges into o'caml compiler. talk complete subject to changes mandated by claudio after checking

File size: 21.8 KB
Line 
1\documentclass[serif]{beamer}
2
3\usepackage[english]{babel}
4\usepackage{listings}
5\usepackage{microtype}
6
7\author{Dominic Mulligan}
8\title{CerCo Work Package 4}
9\date{CerCo project review meeting\\March 2012}
10
11\lstdefinelanguage{matita-ocaml}
12  {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try},
13   morekeywords={[2]whd,normalize,elim,cases,destruct},
14   morekeywords={[3]type,of},
15   mathescape=true,
16  }
17
18\lstset{language=matita-ocaml,basicstyle=\scriptsize\tt,columns=flexible,breaklines=false,
19        keywordstyle=\color{red}\bfseries,
20        keywordstyle=[2]\color{blue},
21        keywordstyle=[3]\color{blue}\bfseries,
22        commentstyle=\color{green},
23        stringstyle=\color{blue},
24        showspaces=false,showstringspaces=false}
25
26\begin{document}
27
28\begin{frame}
29\maketitle
30\end{frame}
31
32\begin{frame}
33\frametitle{Summary I}
34Relevant tasks: T4.2 and T4.3 (from the CerCo Contract):
35\begin{quotation}
36\textbf{Task 4.2}
37Functional encoding in the Calculus of Inductive Construction (indicative effort: UNIBO: 8; UDP: 2; UEDIN: 0)
38\end{quotation}
39
40\begin{quotation}
41\textbf{Task 4.3}
42Formal semantics of intermediate languages (indicative effort: UNIBO: 4; UDP: 0; UEDIN: 0)
43\end{quotation}
44\end{frame}
45
46\begin{frame}
47\frametitle{Summary II}
48Task 4.2 in detail (from the CerCo Contract):
49\begin{quotation}
50\textbf{CIC encoding: Back-end}:
51Functional Specification in the internal language of the Proof Assistant (the Calculus of Inductive Construction) of the back end of the compiler.
52This unit is meant to be composable with the front-end of deliverable D3.2, to obtain a full working compiler for Milestone M2.
53A first validation of the design principles and implementation choices for the Untrusted Cost-annotating OCaml Compiler D2.2 is achieved and reported in the deliverable, possibly triggering updates of the Untrusted Cost-annotating OCaml Compiler sources.
54\end{quotation}
55\end{frame}
56
57\begin{frame}
58\frametitle{Summary III}
59Task 4.3 in detail (from the CerCo contract):
60\begin{quotation}
61\textbf{Executable Formal Semantics of back-end intermediate languages}:
62This prototype is the formal counterpart of deliverable D2.1 for the back end side of the compiler and validates it.
63\end{quotation}
64\end{frame}
65
66\begin{frame}
67\frametitle{Backend intermediate languages I}
68\begin{itemize}
69\item
70O'Caml prototype has five backend intermediate languages: RTLabs, RTL, ERTL, LTL, LIN
71\item
72RTLabs is the `frontier' between backend and frontend, last abstract language
73\item
74RTLabs, RTL, ERTL and LTL are graph based languages: functions represented as graphs of statements, with entry and exit points
75\item
76LIN is a linearised form of LTL, and is the exit point of the compiler's backend
77\end{itemize}
78\end{frame}
79
80\begin{frame}
81\frametitle{Backend intermediate languages II}
82\begin{small}
83\begin{tabbing}
84\quad \=\,\quad \= \\
85\textsf{RTLabs}\\
86\> $\downarrow$ \> copy propagation (an endo-transformation, yet to be ported) \\
87\> $\downarrow$ \> instruction selection\\
88\> $\downarrow$ \> change of memory models in compiler\\
89\textsf{RTL}\\
90\> $\downarrow$ \> constant propagation (an endo-transformation, yet to be ported) \\
91\> $\downarrow$ \> calling convention made explicit \\
92\> $\downarrow$ \> layout of activation records \\
93\textsf{ERTL}\\
94\> $\downarrow$ \> register allocation and spilling\\
95\> $\downarrow$ \> dead code elimination\\
96\textsf{LTL}\\
97\> $\downarrow$ \> function linearisation\\
98\> $\downarrow$ \> branch compression (an endo-transformation) \\
99\textsf{LIN}\\
100\> $\downarrow$ \> relabeling\\
101\end{tabbing}
102\end{small}
103\end{frame}
104
105\begin{frame}
106\frametitle{\texttt{Joint}: a new approach I}
107\begin{itemize}
108\item
109Looking at O'Caml code, languages after RTLabs are similar
110\item
111Similar instructions, similar semantics, and so on
112\item
113Differences are slight
114\item
115Pseudoregisters used instead of hardware registers
116\item
117A few new unique instructions for each language
118\item
119In semantics: some notion of `successor' of an instruction, etc.
120\end{itemize}
121\end{frame}
122
123\begin{frame}
124\frametitle{\texttt{Joint}: a new approach II}
125\begin{itemize}
126\item
127Idea: all of these languages are just instances of a single language
128\item
129This language \texttt{Joint} is parameterised by a type of registers to be used in instructions, and so forth
130\item
131Each language after RTLabs is now just defined as the \texttt{Joint} language instantiated with some concrete types
132\item
133Similarly for semantics: common definitions that take e.g. type representing program counters as parameters
134\end{itemize}
135\end{frame}
136
137\begin{frame}[fragile]
138\frametitle{\texttt{Joint}: a new approach III}
139\texttt{Joint} instructions allow us to embed language-specific instructions:
140\begin{lstlisting}
141inductive joint_instruction (p: params__) (globals: list ident): Type[0] :=
142 | COMMENT: String $\rightarrow$ joint_instruction p globals
143 | COST_LABEL: costlabel $\rightarrow$ joint_instruction p globals
144 ...
145 | COND: acc_a_reg p $\rightarrow$ label $\rightarrow$ joint_instruction p globals
146 | extension: extend_statements p $\rightarrow$ joint_instruction p globals.
147\end{lstlisting}
148
149\begin{lstlisting}
150inductive ertl_statement_extension: Type[0] :=
151 | ertl_st_ext_new_frame: ertl_statement_extension
152 | ertl_st_ext_del_frame: ertl_statement_extension
153 | ertl_st_ext_frame_size: register $\rightarrow$ ertl_statement_extension.
154\end{lstlisting}
155\end{frame}
156
157\begin{frame}[fragile]
158\frametitle{\texttt{Joint}: a new approach IV}
159For example, the definition of the \texttt{ERTL} language is now:
160\begin{lstlisting}
161inductive move_registers: Type[0] :=
162 | pseudo: register $\rightarrow$ move_registers
163 | hardware: Register $\rightarrow$ move_registers.
164
165definition ertl_params__: params__ :=
166 mk_params__ register register register register
167  (move_registers $\times$ move_registers)
168   register nat unit ertl_statement_extension.
169definition ertl_params_: params_ :=
170 graph_params_ ertl_params__.
171definition ertl_params0: params0 :=
172 mk_params0 ertl_params__ (list register) nat.
173definition ertl_params1: params1 :=
174 rtl_ertl_params1 ertl_params0.
175definition ertl_params: $\forall$globals. params globals ≝
176 rtl_ertl_params ertl_params0.
177\end{lstlisting}
178\end{frame}
179
180\begin{frame}
181\frametitle{\texttt{Joint}: advantages}
182\begin{itemize}
183\item
184Why use \texttt{Joint}, as opposed to defining all languages individually?
185\item
186Reduces repeated code (fewer bugs, or places to change)
187\item
188Unify some proofs, making correctness proof easier
189\item
190Easier to add new intermediate languages as needed
191\item
192Easier to see relationship between consecutive languages at a glance
193\end{itemize}
194\end{frame}
195
196\begin{frame}[fragile]
197\frametitle{Instruction embedding in \texttt{Joint}}
198\begin{lstlisting}
199inductive joint_instruction (p:params__) (globals: list ident): Type[0] :=
200 ...
201 | POP: acc_a_reg p $\rightarrow$ joint_instruction p globals
202 | PUSH: acc_a_reg p $\rightarrow$ joint_instruction p globals
203 ...
204\end{lstlisting}
205\begin{itemize}
206\item
207RTLabs (not a \texttt{Joint} language) to RTL is where instruction selection takes place
208\item
209Instructions from the MCS-51 instruction set embedded in \texttt{Joint} syntax
210\end{itemize}
211\end{frame}
212
213\begin{frame}
214\frametitle{Semantics of \texttt{Joint} I}
215\begin{itemize}
216\item
217As mentioned, use of \texttt{Joint} also unifies semantics of these languages
218\item
219We use several sets of records, which represent the state that a program is in
220\item
221These records are parametric in representations for e.g. frames
222\end{itemize}
223\end{frame}
224
225\begin{frame}[fragile]
226\frametitle{Semantics of \texttt{Joint} II}
227\begin{lstlisting}
228record more_sem_params (p:params_): Type[1] :=
229{
230  framesT: Type[0];
231  empty_framesT: framesT;
232  regsT: Type[0];
233  ...
234  acca_store_: acc_a_reg p → beval → regsT → res regsT;
235  acca_retrieve_: regsT → acc_a_reg p → res beval;
236  ...
237  pair_reg_move_: regsT → pair_reg p → res regsT
238 }.
239\end{lstlisting}
240\end{frame}
241
242\begin{frame}[fragile]
243\frametitle{Semantics of \texttt{Joint} III}
244Generic functions:
245\begin{lstlisting}
246definition set_carry: $\forall$p. beval $\rightarrow$ state p $\rightarrow$ state p :=
247 $\lambda$p, carry, st.
248  mk_state $\ldots$ (st_frms $\ldots$ st) (pc $\ldots$ st)
249   (sp $\ldots$ st) (isp $\ldots$ st) carry (regs $\ldots$ st) (m $\ldots$ st).
250\end{lstlisting}
251\begin{lstlisting}
252definition goto: $\forall$globals. $\forall$p:sem_params1 globals. genv globals p $\rightarrow$
253  label $\rightarrow$ state p $\rightarrow$ res (state p) :=
254 $\lambda$globals, p, ge, l, st.
255  do oldpc $\leftarrow$ pointer_of_address (pc $\ldots$ st) ;
256  do newpc $\leftarrow$ address_of_label $\ldots$ ge oldpc l ;
257  OK $\ldots$ (set_pc $\ldots$ newpc st).
258\end{lstlisting}
259\end{frame}
260
261\begin{frame}[fragile]
262\frametitle{Semantics of \texttt{Joint} IV}
263Individual semantics obtained by instantiating records to concrete types (ERTL here):
264\begin{lstlisting}
265definition ertl_more_sem_params: more_sem_params ertl_params_ :=
266 mk_more_sem_params ertl_params_
267  (list (register_env beval)) [] ((register_env beval) $\times$ hw_register_env)
268   ($\lambda$sp. $\langle$empty_map $\ldots$,init_hw_register_env sp$\rangle$) 0 it
269   ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store
270    ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
271     ($\lambda$locals,dest_src.
272       do v $\leftarrow$
273        match \snd dest_src with
274        [ pseudo reg $\Rightarrow$ ps_reg_retrieve locals reg
275        | hardware reg $\Rightarrow$ hw_reg_retrieve locals reg
276        ];
277       match \fst dest_src with
278       [ pseudo reg $\Rightarrow$ ps_reg_store reg v locals
279       | hardware reg $\Rightarrow$ hw_reg_store reg v locals
280       ]).
281\end{lstlisting}
282\end{frame}
283
284\begin{frame}[fragile]
285\frametitle{Semantics of \texttt{Joint} V}
286For languages with `extensions', we provide a semantics:
287\begin{lstlisting}
288definition ertl_exec_extended:
289 $\forall$globals. genv globals (ertl_params globals) $\rightarrow$
290  ertl_statement_extension $\rightarrow$ label $\rightarrow$ state ertl_sem_params $\rightarrow$
291   IO io_out io_in (trace $\times$ (state ertl_sem_params)) :=
292 $\lambda$globals, ge, stm, l, st.
293  match stm with
294   [ ertl_st_ext_new_frame $\Rightarrow$
295      ! v $\leftarrow$ framesize globals $\ldots$ ge st;
296      let sp := get_hwsp st in
297      ! newsp $\leftarrow$ addr_sub sp v;
298      let st := set_hwsp newsp st in
299      ! st $\leftarrow$ next $\ldots$ (ertl_sem_params1 globals) l st ;
300        ret ? $\langle$E0, st$\rangle$
301   | ...
302   ].
303\end{lstlisting}
304\end{frame}
305
306\begin{frame}
307\frametitle{\texttt{Joint} summary}
308\begin{itemize}
309\item
310Using \texttt{Joint} we get a modular semantics
311\item
312`Common' semantics are shared amongst all languages
313\item
314Specific languages are responsible for providing the semantics of the extensions that they provide
315\item
316Show differences (and similarities) between languages clearly
317\item
318Reduces proofs
319\item
320Easy to add new languages
321\end{itemize}
322\end{frame}
323
324\begin{frame}
325\frametitle{A new intermediate language}
326\begin{itemize}
327\item
328Matita backend includes a new intermediate language: RTLntc
329\item
330Sits between RTL and ERTL
331\item
332RTLntc is the RTL language where all tailcalls have been eliminated
333\item
334This language is `implicit' in the O'Caml compiler
335\item
336There, the RTL to ERTL transformation eliminates tailcalls as part of translation
337\item
338But including an extra, explicit intermediate language is `almost free' using the \texttt{Joint} language approach
339\end{itemize}
340\end{frame}
341
342\begin{frame}
343\frametitle{The LTL to LIN transform I}
344\begin{itemize}
345\item
346The order of transformations in O'Caml prototype is fixed
347\item
348Linearisation takes place at a fixed place, in the translation between LTL and LIN
349\item
350The Matita compiler is different: linearisation is a generic process
351\item
352Any graph-based language can now be linearised
353\end{itemize}
354\end{frame}
355
356\begin{frame}
357\frametitle{The LTL to LIN transform II}
358\begin{itemize}
359\item
360The CompCert backend linearises much sooner than CerCo's
361\item
362We can now experiment with linearising much earlier
363\item
364Many transformations and optimisations can work fine on a linearised form
365\end{itemize}
366\end{frame}
367
368\begin{frame}
369\frametitle{`Free time'}
370\begin{itemize}
371\item
372We had six months of `free time', time not allotted in the Contract to working on any explicit deliverable
373\item
374We invested this time working on:
375\begin{itemize}
376\item
377The proof of correctness for the assembler
378\item
379A notion of `structured traces', used throughout the compiler formalisation, as a means of eventually proving that the compiler correctly preserves costs
380\item
381Structured traces were defined in collaboration with the team at UEDIN
382\end{itemize}
383\item
384I now explain in more detail how this time was used
385\end{itemize}
386\end{frame}
387
388\begin{frame}
389\frametitle{Assembler}
390\begin{itemize}
391\item
392After LIN, compiler spits out assembly language for MCS-51
393\item
394Assembler has pseudoinstructions similar to many commercial assembly languages
395\item
396For instance, instead of computed jumps (e.g. \texttt{SJMP} to a specific address), compiler can simply spit out a generic jump instruction to a label
397\item
398Simplifies the compiler, at the expense of introducing more proof obligations
399\end{itemize}
400\end{frame}
401
402\begin{frame}
403\frametitle{A problem: jump expansion}
404\begin{itemize}
405\item
406`Jump expansion' is our name for the following (standard) problem
407\item
408Given a pseudojump to a label $l$, how best can this be expanded into an assembly instruction \texttt{SJMP}, \texttt{AJMP} or \texttt{LJMP} to a concrete address?
409\item
410Problem also applies to conditional jumps
411\item
412Problem especially relevant for MCS-51 as it has a small code memory, therefore aggressive expansion of jumps into smallest possible concrete jump instruction needed
413\item
414But a known hard problem (NP-complete depending on architecture), and easy to imagine knotty configurations where size of jumps are interdependent
415\end{itemize}
416\end{frame}
417
418\begin{frame}
419\frametitle{Jump expansion I}
420\begin{itemize}
421\item
422We employed the following tactic: split the decision over how any particular pseudoinstruction is expanded from pseudoinstruction expansion
423\item
424Call the decision maker a `policy'
425\item
426We started the proof of correctness for the assembler based on the premise that a correct policy exists
427\item
428Further, we know that the assembler only fails to assemble a program if a good policy does not exist (a side-effect of using dependent types)
429\item
430A bad policy is a function that expands a given pseudojump into a concrete jump instruction that is `too small' for the distance to be jumped
431\end{itemize}
432\end{frame}
433
434\begin{frame}
435\frametitle{Jump expansion II}
436\begin{itemize}
437\item
438Boender at UNIBO has been working on a verified implementation of a good jump expansion policy for the MCS-51
439\item
440The strategy initially translates all pseudojumps as \texttt{SJMP} and then increases their size if necessary
441\item
442Termination of the procedure is proved, as well as a safety property, stating that jumps are not expanded into jumps that are too long
443\item
444Optimality is not proved
445\item
446Boender's work is the first formal treatment of the `jump expansion problem'
447\end{itemize}
448\end{frame}
449
450\begin{frame}
451\frametitle{Assembler correctness proof}
452\begin{itemize}
453\item
454Assuming the existence of a good jump expansion property, we completed about 50\% of the correctness proof for the assembler
455\item
456Boender's work constitutes a large missing piece (modulo a few missing lemmas), but holes still remain in the main proof
457\item
458We abandoned this work to start on other tasks
459\item
460However, we intend to return to the proof, and publishing an account of the work (possibly) as a journal paper
461\end{itemize}
462\end{frame}
463
464\begin{frame}
465\frametitle{Structured traces I}
466\begin{itemize}
467\item
468We introduced a notion of `structured traces'
469\item
470These are intended to statically capture the execution trace of a program
471\item
472Come in two variants: inductive and coinductive
473\item
474Inductive is meant to capture program execution traces that eventually halt
475\item
476Coinductive is meant to capture program execution traces that diverge
477\end{itemize}
478\end{frame}
479
480\begin{frame}
481\frametitle{Structured traces II}
482\begin{itemize}
483\item
484Here, I focus on the inductive variety
485\item
486Used the most (for now) in the backend
487\item
488In particular, used in the proof that static and dynamic cost computations coincide
489\item
490This will be explained later
491\end{itemize}
492\end{frame}
493
494\begin{frame}
495\frametitle{Structured traces III}
496\begin{itemize}
497\item
498Central insight is that program execution is always in the body of some function (from \texttt{main} onwards)
499\item
500A well formed program must have labels appearing at certain spots
501\item
502Similarly, the final instruction executed when executing a function must be a \texttt{RET} instruction
503\item
504These invariants, and others, are crystalised in the specific syntactic form of a structured trace
505\item
506Some examples...
507\end{itemize}
508\end{frame}
509
510\begin{frame}[fragile]
511\frametitle{Structured trace examples I}
512Traces end with a return being executed, or not:
513\begin{lstlisting}
514inductive trace_ends_with_ret: Type[0] :=
515 | ends_with_ret: trace_ends_with_ret
516 | doesnt_end_with_ret: trace_ends_with_ret.
517\end{lstlisting}
518A trace starting with a label and ending with a return:
519\begin{lstlisting}
520inductive trace_label_return (S: abstract_status): S $\rightarrow$ S $\rightarrow$ Type[0] :=
521 | tlr_base:
522  $\forall$status_before: S.
523  $\forall$status_after: S.
524   trace_label_label S ends_with_ret status_before status_after $\rightarrow$
525    trace_label_return S status_before status_after
526  ...
527\end{lstlisting}
528\end{frame}
529
530\begin{frame}[fragile]
531\frametitle{Structured trace examples II}
532A trace starting and ending with a cost label:
533\begin{lstlisting}
534...
535with trace_label_label: trace_ends_with_ret $\rightarrow$ S $\rightarrow$ S $\rightarrow$ Type[0] :=
536 | tll_base:
537  $\forall$ends_flag: trace_ends_with_ret.
538  $\forall$start_status: S.
539  $\forall$end_status: S.
540   trace_any_label S ends_flag start_status end_status $\rightarrow$
541   as_costed S start_status $\rightarrow$
542    trace_label_label S ends_flag start_status end_status
543...
544\end{lstlisting}
545\end{frame}
546
547\begin{frame}[fragile]
548\frametitle{Structured trace examples III}
549A call followed by a label on return:
550\begin{lstlisting}
551...
552with trace_any_label: trace_ends_with_ret $\rightarrow$ S $\rightarrow$ S $\rightarrow$ Type[0] :=
553...
554 | tal_base_call:
555  $\forall$status_pre_fun_call: S.   
556  $\forall$status_start_fun_call: S.
557  $\forall$status_final: S.
558   as_execute S status_pre_fun_call status_start_fun_call $\rightarrow$
559   $\forall$H:as_classifier S status_pre_fun_call cl_call.
560    as_after_return S (mk_Sig ?? status_pre_fun_call H) status_final $\rightarrow$
561    trace_label_return S status_start_fun_call status_final $\rightarrow$
562    as_costed S status_final $\rightarrow$
563     trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final
564...
565\end{lstlisting}
566\end{frame}
567
568\begin{frame}[fragile]
569\frametitle{Structured trace examples IV}
570A call followed by a non-empty trace:
571\begin{lstlisting}
572...
573| tal_step_call:
574 $\forall$end_flag: trace_ends_with_ret.
575 $\forall$status_pre_fun_call: S.
576 $\forall$status_start_fun_call: S.
577 $\forall$status_after_fun_call: S.
578 $\forall$status_final: S.
579  as_execute S status_pre_fun_call status_start_fun_call $\rightarrow$
580  $\forall$H:as_classifier S status_pre_fun_call cl_call.
581   as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call $\rightarrow$
582   trace_label_return S status_start_fun_call status_after_fun_call $\rightarrow$
583   ¬ as_costed S status_after_fun_call $\rightarrow$
584   trace_any_label S end_flag status_after_fun_call status_final $\rightarrow$
585    trace_any_label S end_flag status_pre_fun_call status_final
586...
587\end{lstlisting}
588\end{frame}
589
590\begin{frame}
591\frametitle{Static and dynamic costs I}
592\begin{itemize}
593\item
594Given a structured trace, we can compute its associated cost
595\item
596This is the \emph{static} cost of a program execution
597\item
598Similarly, given a program counter and a code memory (corresponding to the trace), we can compute a \emph{dynamic cost} of a simple block
599\item
600Do this by repeatedly fetching, obtaining the next instruction, and a new program counter
601\item
602This requires some predicates defining what a `good program' and what a `good program counter' are
603\end{itemize}
604\end{frame}
605
606\begin{frame}
607\frametitle{Static and dynamic costs II}
608\begin{itemize}
609\item
610We aim to prove that the dynamic and static cost calculations coincide
611\item
612This would imply that the static cost computation is correct
613\item
614This proof is surprisingly tricky to complete (about 3 man months of work so far)
615\item
616Is now about 75\% complete
617\end{itemize}
618\end{frame}
619
620\begin{frame}
621\frametitle{Changes ported to O'Caml prototype}
622\begin{itemize}
623\item
624Bug fixes spotted in the formalisation so far have been merged back into the O'Caml compiler
625\item
626Larger changes like the \texttt{Joint} machinery have so far not
627\item
628It is unclear whether they will be
629\item
630Just a generalization of what is already there
631\item
632Supposed to make formalization easier
633\end{itemize}
634\end{frame}
635
636\begin{frame}
637\frametitle{Improvements in Matita}
638\begin{itemize}
639\item
640Part of the motivation for using Matita was for CerCo to act a `stress test'
641\item
642The proofs talked about in this talk have done this
643\item
644Many improvements to Matita have been made since the last project meeting
645\item
646These include major speed-ups of e.g. printing large goals, bug fixes, the porting of CerCo code to standard library, and more options for passing to tactics
647\end{itemize}
648\end{frame}
649
650\begin{frame}
651\frametitle{Summary}
652We have:
653\begin{itemize}
654\item
655Translated the O'Caml prototype's backend intermediate languages into Matita
656\item
657Implemented the translations between languages, and given the intermediate languages a semantics
658\item
659Refactored many of the backend intermediate languages into a common, parametric `joint' language, that is later specialised
660\item
661Spotted opportunities for commuting backend translation passes
662\item
663Used six months of `free time' to define structured traces and start the proof of correctness for the assembler
664\end{itemize}
665\end{frame}
666
667\end{document}
Note: See TracBrowser for help on using the repository browser.