Changeset 2058 for src

Timestamp:

Jun 13, 2012, 3:17:24 PM (9 years ago)

Author:

mulligan

Message:

First draft of changes to main sections (i.e. those describing the proof itself).

File:

• src/ASM/CPP2012-asm/cpp-2012-asm.tex (modified) (8 diffs)

src/ASM/CPP2012-asm/cpp-2012-asm.tex

@@ -206 +206 @@
 \label{subsect.the.assembler.and.semantics.of.machine.code}
 
-The formalisation in Matita of the semantics of MCS-51 machine code is described in~\cite{mulligan:executable:2011}.
-We merely describe enough here to understand the rest of the proof.
-
-The emulator centres around a \texttt{Status} record, describing the microprocessor's state.
+Our emulator centres around a \texttt{Status} record, describing the microprocessor's state.
 This record contains fields corresponding to the microprocessor's program counter, registers, and so on.
 At the machine code level, code memory is implemented as a compact trie of bytes, addressed by the program counter.
-Machine code programs are loaded into \texttt{Status} using the \texttt{load\_code\_memory} function.
+We parameterise \texttt{Status} records by this representation as a few technical tasks manipulating statuses are made simpler using this approach, as well as permitting a modicum of abstraction.
 
 We may execute a single step of a machine code program using the \texttt{execute\_1} function, which returns an updated \texttt{Status}:
 \begin{lstlisting}
-definition execute_1: Status $\rightarrow$ Status := $\ldots$
+definition execute_1: $\forall$cm. Status cm $\rightarrow$ Status cm := $\ldots$
 \end{lstlisting}
 The function \texttt{execute} allows one to execute an arbitrary, but fixed (due to Matita's normalisation requirement) number of steps of a program.
+Execution proceeds by a case analysis on the instruction fetched from code memory using the program counter of the input \texttt{Status} record.
 
 Naturally, assembly programs have analogues.
@@ -228 +226 @@
 Our analogue of \texttt{execute\_1} is \texttt{execute\_1\_pseudo\_instruction}:
 \begin{lstlisting}
-definition execute_1_pseudo_instruction: (Word $\rightarrow$ nat $\times$ nat) $\rightarrow$
-                                         PseudoStatus $\rightarrow$ PseudoStatus := $\ldots$
+definition execute_1_pseudo_instruction:
+ (Word $\rightarrow$ nat $\times$ nat) $\rightarrow$ $\forall$cm. PseudoStatus cm $\rightarrow$ PseudoStatus cm := $\ldots$
 \end{lstlisting}
 Notice, here, that the emulation function for assembly programs takes an additional argument.
@@ -241 +239 @@
 
 The assembler, mapping programs consisting of lists of pseudoinstructions to lists of bytes, operates in a mostly straightforward manner.
-To a degree of approximation, the assembler on an assembly program, consisting of $n$ pseudoinstructions $\mathtt{P_i}$ for $1 \leq i \leq n$, works as in the following diagram (we use $-^{*}$ to denote a combined map and flatten operation):
+To a degree of approximation the assembler, on an assembly program consisting of $n$ pseudoinstructions $\mathtt{P_i}$ for $1 \leq i \leq n$, works as in the following diagram (we use $-^{*}$ to denote a combined map and flatten operation):
 \begin{displaymath}
 [\mathtt{P_1}, \ldots \mathtt{P_n}] \xrightarrow{\left(\mathtt{P_i} \xrightarrow{\mbox{\fontsize{7}{9}\selectfont$\mathtt{expand\_pseudo\_instruction}$}} \mathtt{[I^1_i, \ldots I^q_i]} \xrightarrow{\mbox{\fontsize{7}{9}\selectfont$\mathtt{~~~~~~~~assembly1^{*}~~~~~~~~}$}} \mathtt{[0110]}\right)^{*}} \mathtt{[010101]}
@@ -252 +250 @@
 % SECTION                                                                      %
 % ---------------------------------------------------------------------------- %
-\subsection{Policies}
-\label{subsect.policies}
-
-Policies exist to dictate how conditional and unconditional jumps at the assembly level should be expanded into machine code instructions.
-Using policies, we are able to completely decouple the decision over how jumps are expanded with the act of expansion, simplifying our proofs.
-As mentioned, the MCS-51 instruction set includes three different jump instructions: \texttt{SJMP}, \texttt{AJMP} and \texttt{LJMP}; call these `short', `medium' and `long' jumps, respectively:
-\begin{lstlisting}
-inductive jump_length: Type[0] :=
-  |short_jump:jump_length |medium_jump:jump_length |long_jump:jump_length.
-\end{lstlisting}
-
-A \texttt{jump\_expansion\_policy} is a map from pseudo program counters (implemented as \texttt{Word}s) to \texttt{jump\_length}s.
-Efficient implementations of policies are based on tries.
-Intuitively, a policy maps positions in a program (indexed using program counters implemented as \texttt{Word}s) to a particular variety of jump:
-\begin{lstlisting}
-definition policy_type := Word $\rightarrow$ jump_length.
-\end{lstlisting}
-
-Next, we require a series of `sigma' functions.
-These functions map assembly program counters to their machine code counterparts, establishing the correspondence between `positions' in an assembly program and `positions' in a machine code program.
-At the heart of this process is \texttt{sigma0} which traverses an assembly program building maps from pseudo program counters to program counters.
-This function fails if and only if an internal call to \texttt{assembly\_1\_pseudoinstruction\_safe} fails, which happens if a jump pseudoinstruction is expanded incorrectly:
-\begin{lstlisting}
-definition sigma0: pseudo_assembly_program $\rightarrow$ policy_type
-  $\rightarrow$ option (nat $\times$ (nat $\times$ (BitVectorTrie Word 16))) := $\ldots$
-\end{lstlisting}
-Here, the returned \texttt{BitVectorTrie} is a map between pseudo program counters and program counters, and is constructed by successively expanding pseudoinstructions and incrementing the two program counters the requisite amount to keep them in correct correspondence.
-The two natural numbers returned are the maximum values that the two program counters attained.
-
-We eventually lift this to functions from pseudo program counters to program counters, implemented as \texttt{Word}s:
-\begin{lstlisting}
-definition sigma_safe:
-  pseudo_assembly_program $\rightarrow$ policy_type $\rightarrow$ option (Word $\rightarrow$ Word) := $\ldots$
-\end{lstlisting}
-
-Now, it's possible to define what a `good policy' is for a program \texttt{p}.
-A policy \texttt{pol} is deemed good when it prevents \texttt{sigma\_safe} from failing on \texttt{p}.
-Failure is only possible when the policy dictates that short or medium jumps be expanded to jumps to locations too far away, or when the produced object code does not fit into code memory.
-A \texttt{policy} for a program \texttt{p} is a policy that is good for \texttt{p}:
-\begin{lstlisting}
-definition policy_ok := $\lambda$pol.$\lambda$p. sigma_safe p $\neq$ None $\ldots$
-definition policy :=
-  $\lambda$p. $\Sigma$jump_expansion: policy_type. policy_ok jump_expansion p
-\end{lstlisting}
-
-Finally, we obtain \texttt{sigma}, a mapping from pseudo program counters to program counters that takes in input a good policy and thus never fails.
-Note how we avoid failure here, and in most of the remaining functions, by restricting the domain using the dependent type \texttt{policy}:
-\begin{lstlisting}
-definition sigma: $\forall$p. policy p $\rightarrow$ Word $\rightarrow$ Word := $\ldots$
-\end{lstlisting}
-
-% ---------------------------------------------------------------------------- %
-% SECTION                                                                      %
-% ---------------------------------------------------------------------------- %
 \subsection{Correctness of the assembler with respect to fetching}
 \label{subsect.total.correctness.of.the.assembler}
 
+Throughout the proof of correctness for assembly we assume that policies are bifurcated into two functions: \texttt{sigma} mapping \texttt{Word} to \texttt{Word} and \texttt{policy} mapping \texttt{Word} to \texttt{bool}.
+For our purposes, \texttt{sigma} is most interesting, as it maps pseudo program counters to program counters; \texttt{policy} is merely a technical device used in jump expansion.
+
 Using our policies, we now work toward proving the total correctness of the assembler.
 By `total correctness', we mean that the assembly process never fails when provided with a good policy and that the process does not change the semantics of a certain class of well behaved assembly programs.
-Naturally, this necessitates keeping some sort of correspondence between addresses at the assembly level and addresses at the machine code level.
-For this, we use the \texttt{sigma} machinery defined at the end of Subsection~\ref{subsect.policies}.
+By `good policy' we mean that policies provided to us will keep a lockstep correspondence between addresses at the assembly level and addresses at the machine code level:
+\begin{displaymath}
+\texttt{sigma}(\texttt{ppc} + 1) = \texttt{pc} + \texttt{current\_instruction\_size}
+\end{displaymath}
+along with some other technical properties related to program counters falling within the bounds of our programs.
+We assume the correctness of the policies given to us using a function, \texttt{sigma\_policy\_specification} that we take in input, when needed.
 
 We expand pseudoinstructions using the function \texttt{expand\_pseudo\_instruction}.
-This takes an assembly program (consisting of a list of pseudoinstructions), a good policy for the program and a pointer to the pseudo code memory.
+This takes an assembly program (consisting of a list of pseudoinstructions), a policy for the program, a map detailing the physical addresses of data labels from the pseudo program's preamble, and the pseudoinstruction to be expanded.
 It returns a list of instructions, corresponding to the expanded pseudoinstruction referenced by the pointer.
-The policy is used to decide how to expand \texttt{Call}s, \texttt{Jmp}s and conditional jumps.
-The function is given a dependent type that incorporates its specification.
-Its pre- and post-conditions are omitted in the paper due to lack of space.
-We show them as an example in the next function, \texttt{build\_maps}.
+Execution proceeds by case analysis on the pseudoinstruction given as input.
+The policy, \texttt{sigma}, is used to decide how to expand \texttt{Call}s, \texttt{Jmp}s and conditional jumps.
 \begin{lstlisting}
 definition expand_pseudo_instruction:
-  $\forall$program. $\forall$pol: policy program.
-  $\forall$ppc:Word. $\ldots$ $\Sigma$res. list instruction. $\ldots$ := $\ldots$
-\end{lstlisting}
-
-The following function, \texttt{build\_maps}, is used to construct a pair of mappings from program counters to labels and cost labels, respectively.
-Cost labels are a technical device used in the CerCo prototype C compiler for proving that the compiler is cost preserving.
-For our purposes in this paper, they can be safely ignored, though the interested reader may consult~\cite{amadio:certifying:2010} for an overview.
-
-The label map, on the other hand, records the position of labels that appear in an assembly program, so that the pseudoinstruction expansion process can replace them with real memory addresses:
-\begin{lstlisting}
-definition build_maps:
- $\forall$p. $\forall$pol: policy p.
- $\Sigma$res : ((BitVectorTrie Word 16) $\times$ (BitVectorTrie Word 16)).
-   let $\langle$labels, costs$\rangle$ := res in
-     $\forall$id. occurs_exactly_once id ($\pi_2$ p) $\rightarrow$
-    let addr := address_of_word_labels_code_mem ($\pi_2$ p) id in
-      lookup $\ldots$ id labels (zero $\ldots$) = sigma pseudo_program pol addr := $\ldots$
-\end{lstlisting}
-The type of \texttt{build\_maps} owes to our use of Matita's Russell facility to provide a strong specification for the function in the type (c.f. the use of $\Sigma$-types and coercions, through which Russell is simulated in Matita).
-We express that for all labels that appear exactly once in any assembly program, the newly created map used in the implementation, and the stronger \texttt{sigma} function used in the specification, agree.
-
-Using \texttt{build\_maps}, we can express the following lemma, expressing the correctness of the assembly function:
-\begin{lstlisting}
-lemma assembly_ok: $\forall$p,pol,assembled.
-  let $\langle$labels, costs$\rangle$ := build_maps p pol in
-  $\langle$assembled,costs$\rangle$ = assembly p pol $\rightarrow$
-  let cmem := load_code_memory assembled in
-  let preamble := $\pi_1$ p in
-  let dlbls := construct_datalabels preamble in
-  let addr := address_of_word_labels_code_mem ($\pi_2$ p) in
-  let lk_lbls := λx. sigma p pol (addr x) in
-  let lk_dlbls := λx. lookup $\ldots$ x datalabels (zero ?) in
-  $\forall$ppc, pi, newppc.
-  $\forall$prf: $\langle$pi, newppc$\rangle$ = fetch_pseudo_instruction ($\pi_2$ p) ppc.
-  $\forall$len, assm.
-  let spol := sigma program pol ppc in
-  let spol_len := spol + len in
-  let echeck := encoding_check cmem spol spol_len assm in
-  let a1pi := assembly_1_pseudoinstruction in
-  $\langle$len, assm$\rangle$ = a1pi p pol ppc lk_lbls lk_dlbls pi (refl $\ldots$) (refl $\ldots$) ? $\rightarrow$
-    echeck $\wedge$ sigma p pol newppc = spol_len.
-\end{lstlisting}
-Suppose also we assemble our program \texttt{p} in accordance with a policy \texttt{pol} to obtain \texttt{assembled}.
-Here, we perform a `sanity check' to ensure that the two cost label maps generated are identical, before loading the assembled program into code memory \texttt{cmem}.
+ $\forall$lookup_labels: Identifier $\rightarrow$ Word.
+ $\forall$sigma: Word $\rightarrow$ Word.
+ $\forall$policy: Word $\rightarrow$ bool.
+  Word $\rightarrow$ (Identifier $\rightarrow$ Word) $\rightarrow$
+   pseudo_instruction $\rightarrow$ list instruction := ...
+\end{lstlisting}
+
+We can express the following lemma, expressing the correctness of the assembly function (slightly simplified):
+\begin{lstlisting}
+lemma assembly_ok:
+ $\forall$program: pseudo_assembly_program.
+ $\forall$sigma: Word $\rightarrow$ Word.
+ $\forall$policy: Word $\rightarrow$ bool.
+ $\forall$sigma_policy_witness.
+ $\forall$assembled.
+ $\forall$costs': BitVectorTrie costlabel 16.
+ let $\langle$preamble, instr_list$\rangle$ := program in
+ let $\langle$labels, costs$\rangle$ := create_label_cost_map instr_list in
+  $\langle$assembled,costs'$\rangle$ = assembly program sigma policy $\rightarrow$
+   let cmem := load_code_memory assembled in
+   $\forall$ppc.
+    let $\langle$pi, newppc$\rangle$ := fetch_pseudo_instruction instr_list ppc in     
+    let $\langle$len,assembled$\rangle$ := assembly_1_pseudoinstruction $\ldots$ ppc $\ldots$ pi in
+    let pc := sigma ppc in
+    let pc_plus_len := add $\ldots$ pc (bitvector_of_nat $\ldots$ len) in
+     encoding_check cmem pc pc_plus_len assembled $\wedge$
+      sigma newppc = add $\ldots$ pc (bitvector_of_nat $\ldots$ len).
+\end{lstlisting}
+Here, \texttt{encoding\_check} is a recursive function that checks that assembled machine code is correctly stored in code memory.
+Suppose also we assemble our program \texttt{p} in accordance with a policy \texttt{sigma} to obtain \texttt{assembled}, loading the assembled program into code memory \texttt{cmem}.
 Then, for every pseudoinstruction \texttt{pi}, pseudo program counter \texttt{ppc} and new pseudo program counter \texttt{newppc}, such that we obtain \texttt{pi} and \texttt{newppc} from fetching a pseudoinstruction at \texttt{ppc}, we check that assembling this pseudoinstruction produces the correct number of machine code instructions, and that the new pseudo program counter \texttt{ppc} has the value expected of it.
 
-Theorem \texttt{fetch\_assembly} establishes that the \texttt{fetch} and \texttt{assembly1} functions interact correctly.
+Lemma \texttt{fetch\_assembly} establishes that the \texttt{fetch} and \texttt{assembly1} functions interact correctly.
 The \texttt{fetch} function, as its name implies, fetches the instruction indexed by the program counter in the code memory, while \texttt{assembly1} maps a single instruction to its byte encoding:
 \begin{lstlisting}
-theorem fetch_assembly: $\forall$pc, i, cmem, assembled.  assembled=assembly1 i $\rightarrow$
+lemma fetch_assembly:
+ $\forall$pc: Word.
+ $\forall$i: instruction.
+ $\forall$code_memory: BitVectorTrie Byte 16.
+ $\forall$assembled: list Byte.
+  assembled = assembly1 i $\rightarrow$
   let len := length $\ldots$ assembled in
-  encoding_check cmem pc (pc + len) assembled $\rightarrow$
-    let fetched := fetch code_memory (bitvector_of_nat $\ldots$ pc) in
-    let $\langle$instr_pc, ticks$\rangle$ := fetched in
-    let $\langle$instr, pc'$\rangle$ := instr_pc in
-      (eq_instruction instr i $\wedge$ eqb ticks (ticks_of_instruction instr) $\wedge$
-       eq_bv $\ldots$ pc' (pc + len)) = true.
+  let pc_plus_len := add $\ldots$ pc (bitvector_of_nat $\ldots$ len) in
+   encoding_check code_memory pc pc_plus_len assembled $\rightarrow$
+   let $\langle$instr, pc', ticks$\rangle$ := fetch code_memory pc in
+    (eq_instruction instr i $\wedge$
+     eqb ticks (ticks_of_instruction instr) $\wedge$
+     eq_bv $\ldots$ pc' pc_plus_len) = true.
 \end{lstlisting}
 In particular, we read \texttt{fetch\_assembly} as follows.
 Given an instruction, \texttt{i}, we first assemble the instruction to obtain \texttt{assembled}, checking that the assembled instruction was stored in code memory correctly.
-Fetching from code memory, we obtain \texttt{fetched}, a tuple consisting of the instruction, new program counter, and the number of ticks this instruction will take to execute.
-Deconstructing these tuples, we finally check that the fetched instruction is the same instruction that we began with, and the number of ticks this instruction will take to execute is the same as the result returned by a lookup function, \texttt{ticks\_of\_instruction}, devoted to tracking this information.
+Fetching from code memory, we obtain a tuple consisting of the instruction, new program counter, and the number of ticks this instruction will take to execute.
+We finally check that the fetched instruction is the same instruction that we began with, and the number of ticks this instruction will take to execute is the same as the result returned by a lookup function, \texttt{ticks\_of\_instruction}, devoted to tracking this information.
 Or, in plainer words, assembling and then immediately fetching again gets you back to where you started.
 
@@ -390 +330 @@
 \begin{lstlisting}
 lemma fetch_assembly_pseudo:
- ∀program.∀pol:policy program.∀ppc.∀code_memory.
-  let pi := $\pi_1$ (fetch_pseudo_instruction ($\pi_2$ program) ppc) in
-  let instructions := expand_pseudo_instruction program pol ppc ... in
-  let $\langle$len,assembled$\rangle$ := assembly_1_pseudoinstruction program pol ppc ... in
-  encoding_check code_memory pc (pc + len) assembled →
-  fetch_many code_memory (pc + len) pc instructions.
-\end{lstlisting}
-Here, \texttt{len} is the number of machine code instructions the pseudoinstruction at hand has been expanded into, and \texttt{encoding\_check} is a recursive function that checks that assembled machine code is correctly stored in code memory.
+ $\forall$program: pseudo_assembly_program.
+ $\forall$sigma: Word $\rightarrow$ Word.
+ $\forall$policy: Word $\rightarrow$ bool.
+ $\forall$ppc.
+ $\forall$code_memory.
+ let $\langle$preamble, instr_list$\rangle$ := program in
+ let pi := $\pi_1$ (fetch_pseudo_instruction instr_list ppc) in
+ let pc := sigma ppc in
+ let instrs := expand_pseudo_instruction $\ldots$ sigma policy ppc $\ldots$ pi in
+ let $\langle$l, a$\rangle$ := assembly_1_pseudoinstruction $\ldots$ sigma policy ppc $\ldots$ pi in
+ let pc_plus_len := add $\ldots$ pc (bitvector_of_nat $\ldots$ l) in
+  encoding_check code_memory pc pc_plus_len a $\rightarrow$
+   fetch_many code_memory pc_plus_len pc instructions.
+\end{lstlisting}
+Here, \texttt{l} is the number of machine code instructions the pseudoinstruction at hand has been expanded into.
 We assemble a single pseudoinstruction with \texttt{assembly\_1\_pseudoinstruction}, which internally calls \texttt{jump\_expansion} and \texttt{expand\_pseudo\_instruction}.
 The function \texttt{fetch\_many} fetches multiple machine code instructions from code memory and performs some routine checks.
 
 Intuitively, Lemma \texttt{fetch\_assembly\_pseudo} can be read as follows.
-Suppose we expand the pseudoinstruction at \texttt{ppc} with the policy decision \texttt{pol}, obtaining the list of machine code instructions \texttt{instructions}.
-Suppose we also assemble the pseudoinstruction at \texttt{ppc} to obtain \texttt{assembled}, a list of bytes.
+Suppose we expand the pseudoinstruction at \texttt{ppc} with the policy decision \texttt{sigma}, obtaining the list of machine code instructions \texttt{instrs}.
+Suppose we also assemble the pseudoinstruction at \texttt{ppc} to obtain \texttt{a}, a list of bytes.
 Then, we check with \texttt{fetch\_many} that the number of machine instructions that were fetched matches the number of instruction that \texttt{expand\_pseudo\_instruction} expanded.
 
 The final lemma in this series is \texttt{fetch\_assembly\_pseudo2} that combines the Lemma \texttt{fetch\_assembly\_pseudo} with the correctness of the functions that load object code into the processor's memory.
+Again, we slightly simplify:
 \begin{lstlisting}
 lemma fetch_assembly_pseudo2:
- ∀program,pol,ppc.
-  let $\langle$labels,costs$\rangle$ := build_maps program pol in
-  let assembled := $\pi_1$ (assembly program pol) in
-  let code_memory := load_code_memory assembled in
-  let data_labels := construct_datalabels ($\pi_1$ program) in
-  let lookup_labels :=
-    λx. sigma $\ldots$ pol (address_of_word_labels_code_mem ($\pi_2$ program) x) in
-  let lookup_datalabels := λx. lookup ? ? x data_labels (zero ?) in
-  let $\langle$pi,newppc$\rangle$ := fetch_pseudo_instruction ($\pi_2$ program) ppc in
-  let instrs ≝ expand_pseudo_instruction program pol ppc ... in
-   fetch_many code_memory (sigma $\ldots$ pol newppc) (sigma $\ldots$ pol ppc) instrs.
-\end{lstlisting}
+ $\forall$program.
+ $\forall$sigma.
+ $\forall$policy.
+ $\forall$sigma_policy_specification_witness.
+ $\forall$ppc.
+  let $\langle$preamble, instr_list$\rangle$ := program in
+  let $\langle$labels, costs$\rangle$ := create_label_cost_map instr_list in
+  let $\langle$assembled, costs'$\rangle$ := $\pi_1$ $\ldots$ (assembly program sigma policy) in
+  let cmem := load_code_memory assembled in
+  let $\langle$pi, newppc$\rangle$ := fetch_pseudo_instruction instr_list ppc in
+  let instructions := expand_pseudo_instruction $\ldots$ sigma ppc $\ldots$ pi in
+    fetch_many cmem (sigma newppc) (sigma ppc) instructions.
+\end{lstlisting}
+
+Here we use $\pi_1 \ldots$ to eject out the existential witness from the Russell-typed function \texttt{assembly}.
 
 We read \texttt{fetch\_assembly\_pseudo2} as follows.
-Suppose we are able to successfully assemble an assembly program using \texttt{assembly} and produce a code memory, \texttt{code\_memory}.
-Then, fetching a pseudoinstruction from the pseudo code memory at address \texttt{ppc} corresponds to fetching a sequence of instructions from the real code memory at address \texttt{sigma program pol ppc}.
-The fetched sequence corresponds to the expansion, according to \texttt{pol}, of the pseudoinstruction.
+Suppose we are able to successfully assemble an assembly program using \texttt{assembly} and produce a code memory, \texttt{cmem}.
+Then, fetching a pseudoinstruction from the pseudo code memory at address \texttt{ppc} corresponds to fetching a sequence of instructions from the real code memory using $\sigma$ to expand pseudoinstructions.
+The fetched sequence corresponds to the expansion, according to \texttt{sigma}, of the pseudoinstruction.
 
 At first, the lemmas appears to immediately imply the correctness of the assembler.
@@ -437 +388 @@
 \label{subsect.total.correctness.for.well.behaved.assembly.programs}
 
-In any `reasonable' assembly language addresses in code memory are just data that can be manipulated in multiple ways by the program.
-An assembly program can forge, compare and move addresses around, shift existing addresses or apply logical and arithmetical operations to them.
-Further, every optimising assembler is allowed to modify code memory.
-Hence only the semantics of a few of the aforementioned operations are preserved by an optimising assembler/compiler.
-Moreover, this characterisation of well behaved programs is clearly undecidable.
-
-To obtain a reasonable statement of correctness for our assembler, we need to trace memory locations (and, potentially, registers) that contain memory addresses.
-This is necessary for two purposes.
-
-First we must detect (at run time) programs that manipulate addresses in well behaved ways, according to some approximation of well-behavedness.
+The traditional approach to verifying the correctness of an assembler is to treat memory addresses as opaque structures that cannot be modified.
+This prevents assembly programs from performing any `dangerous', semantics breaking manipulations of memory addresses by making these programs simply unrepresentable in the source language.
+
+Here, we take a different approach to this problem: we trace memory locations (and, potentially, registers) that contain memory addresses.
+We then prove that only those assembly programs that use addresses in `safe' ways have their semantics preserved by the assembly process.
+We believe that this approach is more flexible when compared to the traditional approach, as in principle it allows us to introduce some permitted \emph{benign} manipulations of addresses that the traditional approach, using opaque addresses, cannot handle, therefore expanding the set of input programs that can be assembled correctly.
+
+However, with this approach we must detect (at run time) programs that manipulate addresses in well behaved ways, according to some approximation of well-behavedness.
 Second, we must compute statuses that correspond to pseudo-statuses.
 The contents of the program counter must be translated, as well as the contents of all traced locations, by applying the \texttt{sigma} map.
@@ -473 +422 @@
 This never fails, providing that our policy is correct:
 \begin{lstlisting}
-definition status_of_pseudo_status: internal_pseudo_address_map $\rightarrow$
-  $\forall$ps:PseudoStatus. policy (code_memory $\ldots$ ps) $\rightarrow$ Status
+definition status_of_pseudo_status:
+ internal_pseudo_address_map $\rightarrow$ $\forall$pap. $\forall$ps: PseudoStatus pap.
+ $\forall$sigma: Word $\rightarrow$ Word. $\forall$policy: Word $\rightarrow$ bool.
+  Status (code_memory_of_pseudo_assembly_program pap sigma policy)
 \end{lstlisting}
 
@@ -482 +433 @@
 \begin{lstlisting}
 definition next_internal_pseudo_address_map: internal_pseudo_address_map
-  $\rightarrow$ PseudoStatus $\rightarrow$ option internal_pseudo_address_map
-\end{lstlisting}
+ $\rightarrow$ PseudoStatus $\rightarrow$ option internal_pseudo_address_map
+\end{lstlisting}
+Note, if we wished to allow `benign manipulations' of addresses, it would be this function that needs to be changed.
 
 The function \texttt{ticks\_of} computes how long---in clock cycles---a pseudoinstruction will take to execute when expanded in accordance with a given policy.
 The function returns a pair of natural numbers, needed for recording the execution times of each branch of a conditional jump.
 \begin{lstlisting}
-definition ticks_of:
-  $\forall$p:pseudo_assembly_program. policy p $\rightarrow$ Word $\rightarrow$ nat $\times$ nat := $\ldots$
+axiom ticks_of:
+ $\forall$p:pseudo_assembly_program. policy p $\rightarrow$ Word $\rightarrow$ nat $\times$ nat := $\ldots$
 \end{lstlisting}
 
 Finally, we are able to state and prove our main theorem.
-This relates the execution of a single assembly instruction and the execution of (possibly) many machine code instructions, as long .
-That is, the assembly process preserves the semantics of an assembly program, as it is translated into machine code, as long as we are able to track memory addresses properly:
+This relates the execution of a single assembly instruction and the execution of (possibly) many machine code instructions, as long as we are able to track memory addresses properly:
 \begin{lstlisting}
 theorem main_thm:
- ∀M,M':internal_pseudo_address_map.∀ps.∀pol: policy ps.
-  next_internal_pseudo_address_map M ps = Some $\ldots$ M' →
-   ∃n.
-      execute n (status_of_pseudo_status M ps pol)
-    = status_of_pseudo_status M'
-       (execute_1_pseudo_instruction (ticks_of (code_memory $\ldots$ ps) pol) ps)
-       [pol].
+ $\forall$M, M': internal_pseudo_address_map.
+ $\forall$program: pseudo_assembly_program.
+ let $\langle$preamble, instr_list$\rangle$ := program in
+ $\forall$is_well_labelled: is_well_labelled_p instr_list.
+ $\forall$sigma: Word $\rightarrow$ Word.
+ $\forall$policy: Word $\rightarrow$ bool.
+ $\forall$sigma_policy_specification_witness.
+ $\forall$ps: PseudoStatus program.
+ $\forall$program_counter_in_bounds.
+  next_internal_pseudo_address_map M program ps = Some $\ldots$ M' $\rightarrow$
+  $\exists$n. execute n $\ldots$ (status_of_pseudo_status M $\ldots$ ps sigma policy) =
+   status_of_pseudo_status M' $\ldots$ (execute_1_pseudo_instruction
+     (ticks_of program sigma policy) program ps) sigma policy.
 \end{lstlisting}
 The statement is standard for forward simulation, but restricted to \texttt{PseudoStatuses} \texttt{ps} whose next instruction to be executed is well-behaved with respect to the \texttt{internal\_pseudo\_address\_map} \texttt{M}.
+Further, we explicitly requires proof that our policy is correct and the pseudo program counter lies within the bounds of the program.
 Theorem \texttt{main\_thm} establishes the total correctness of the assembly process and can simply be lifted to the forward simulation of an arbitrary number of well behaved steps on the assembly program.