This report is one part of a series of documents describing the fully
verified specification, construction and implementation of a
ComLisp{compiler. ComLisp is a subset of ANSICommonLisp. Programs are
systems of first order mutually recursive function and procedure
definitions on dynamic Lisp data. ComLisp is both compiler source and
implementation language. The work is part of the DFG research project
Verifix on Correct Compilers. The major goal in Verifix is to develop
methods for correct realistic compiler construction for practically
relevant source languages and concrete target machines, and to
completely verify them down to their binary machine code
implementations.

This document describes the complete compiler construction in high
level implementation language ComLisp for a four-phase compilation
transforming ComLisp{programs to binary machine code executables on
transputer T400 processors. The compilation is modularized to four
steps using three intermediate languages, a stack language, a C-like
abstract machine oriented language, and an assembly
language. Compiling specifications between each pair of source and
target languages are given as inductively defined relations. In this
report we describe, how these specifications are refined to a system of
first order mutually recursive ComLisp-functions, i.e. to a compiler
program in high level implementation language ComLisp.

The correctly constructed ComLisp{compiler program, proved to be
compliant to the compiling specification, may be used in order to
bootstrap itself as a binary transputer{machine code executable. The
bootstrapping process, however, initially depends on an unverified
execution basis for ComLisp. Without further investigation it does not
guarantee full correctness. We depend on unverified tool support if we
use a CommonLisp system in order to execute this
compiler. Mathematical a-posteriori control (double checking) of the
bootstrapping result will close this gap for the fully verified initial
ComLisp{compiler executable. However, the compiling specification and
its correctness proof with respect to source and target language
semantics (compiling verification) as well as the documentation of the
a-posteriori double checking of the bootstrapping result are not given
here, although the essential parts of the compiling specification are
repeated in this document.