1<!--
2     Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3
4     SPDX-License-Identifier: CC-BY-SA-4.0
5-->
6
7Assembly Refinement Toolchain
8=============================
9
10This toolchain is used to validate the translation of C programs into compiled
11binaries. The semantics of the compiled binaries and the initial C programs are
12compared via the external [SydTV tool](
13https://github.com/seL4proj/graph-refine). These tools are used to convert the
14Isabelle C semantics of a program into an exported SydTV-GL representation,
15to verify that the exported program is a refinement of the starting semantics,
16and to replay SydTV proofs in Isabelle/HOL.
17
18These theories are generic. They are specialised to the case of seL4 in the
19[proof directory](../../proof/asmrefine).
20
21An overview of the full proof is given with the [SydTV tool](
22https://github.com/seL4proj/graph-refine). It is also described in the
23PLDI '13 [paper][1].
24
25  [1]: https://ts.data61.csiro.au/publications/nictaabstracts/Sewell_MK_13.abstract.pml "Translation Validation for a Verified OS Kernel"
26
27Important Theories
28------------------
29
30The [`GraphLang`](GraphLang.thy) theory introduces an Isabelle/HOL
31representation of SydTV-GL programs, and a parser for them.
32
33The [`SimplExport`](SimplExport.thy) theory contains apparatus for exporting
34the C semantics of a program (created by the [C parser](../c-parser) and
35expressed in the [Simpl](../c-parser/Simpl) language) into a textual SydTV-GL
36representation.
37
38The [`ProveGraphRefine`](ProveGraphRefine.thy) theory introduces proof
39automation for proving the correctness of the export process of
40[`SimplExport`](SimplExport.thy).
41
42The [`GraphProof`](GraphProof.thy) theory introduces proof rules needed to
43replay external SydTV refinement proofs within Isabelle/HOL. This is a work in
44progress.
45