9069ba7638
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems> |
||
|---|---|---|
| .. | ||
| AARCH64 | ||
| ARM | ||
| ARM_HYP | ||
| RISCV64 | ||
| X64 | ||
| testfiles | ||
| AsmSemanticsRespects.thy | ||
| CommonOps.thy | ||
| CommonOpsLemmas.thy | ||
| ExtraSpecs.thy | ||
| FieldAccessors.thy | ||
| GhostAssertions.thy | ||
| GlobalsSwap.thy | ||
| GraphLang.thy | ||
| GraphLangLemmas.thy | ||
| GraphProof.thy | ||
| GraphRefine.thy | ||
| Makefile | ||
| ProveGraphRefine.thy | ||
| README.md | ||
| ROOT | ||
| SimplExport.thy | ||
| TailrecPre.thy | ||
README.md
Assembly Refinement Toolchain
This toolchain is used to validate the translation of C programs into compiled binaries. The semantics of the compiled binaries and the initial C programs are compared via the external SydTV tool. These tools are used to convert the Isabelle C semantics of a program into an exported SydTV-GL representation, to verify that the exported program is a refinement of the starting semantics, and to replay SydTV proofs in Isabelle/HOL.
These theories are generic. They are specialised to the case of seL4 in the proof directory.
An overview of the full proof is given with the SydTV tool. It is also described in the PLDI '13 paper.
Important Theories
The GraphLang theory introduces an Isabelle/HOL
representation of SydTV-GL programs, and a parser for them.
The SimplExport theory contains apparatus for exporting
the C semantics of a program (created by the C parser and
expressed in the Simpl language) into a textual SydTV-GL
representation.
The ProveGraphRefine theory introduces proof
automation for proving the correctness of the export process of
SimplExport.
The GraphProof theory introduces proof rules needed to
replay external SydTV refinement proofs within Isabelle/HOL. This is a work in
progress.