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