| ISA-comp.lisp | Proof of invariant conditions defining the correct state of programmer visible components. |
| ISA-def.lisp | The definition of our machine at the instruction-set architecture level. |
| MA2-def.lisp | The definition of our machine at the micro-architectural level. |
| MA2-lemmas.lisp | Proof of a small number of lemmas about the micro-architecture. |
| MAETT-def.lisp | The definition of Micro-Architectural Execution Trace Table. |
| MAETT-lemmas.lisp | Wrapping up two ACL2 books containing shared lemmas, MAETT-lemmas1.lisp and MAETT-lemmas2.lisp. |
| MAETT-lemmas1.lisp | Contains shared lemmas. |
| MAETT-lemmas2.lisp | Contains shared lemmas. |
| MI-inv.lisp | Proof of the invariant condition MT-inst-invariants, which defines the valid intermediate values in the pipeline. |
| TAGS | Emacs tag file. |
| absolute-path.lisp | Defining the path to the public libraries. |
| b-ops-aux-def.lisp | Supplementary definition of basic bit vector operations, in addition to those defined in the IHS library. |
| b-ops-aux.lisp | Supplementary lemmas about basic bit vector operations, in addition to those proven in the IHS library. |
| basic-def.acl2 | Compile directive. |
| basic-def.lisp | Basic definitions of architectural components used in ISA-def.lisp and MA2-def.lisp., including the memory and the register file. |
| define-u-package.lisp | Defining package U. |
| digest.lisp.txt | A digest version of the proof script. |
| exintr.lisp | Proof of the final correctness criterion. |
| ihs.lisp | IHS library loader. This turns on and off the right IHS rules for the verification work. |
| in-order.lisp | Proof of invariant conditions about execution order and program order of instructions. |
| invariant-proof.lisp | Wrapping up all the invariant proofs. |
| invariants-def.lisp | Definition of invariant conditions using our MAETT. |
| makefile | Makefile. |
| memory-inv.lisp | Proof of basic lemmas about the memory. |
| misc-inv.lisp | Proof of miscellaneous invariant conditions. |
| modifier.lisp | Definition and proof of properties about instructions that modify the register file and the memory. |
| reg-ref.lisp | Proof of invariants about register reference tables and the reservation stations. |
| trivia.lisp | Miscellaneous trivial lemmas. |
| uniq-inv.lisp | Proof of an invariant conditions that check the non-existence of the structural hazard on pipeline latches and the re-order buffer. |
| utils.acl2 | Compile directive. |
| utils.lisp | ACL2 utility functions. |
| wk-inv.lisp | Proof of weak invariant conditions. |