diff options
Diffstat (limited to 'kvx/Asmgenproof.v')
-rw-r--r-- | kvx/Asmgenproof.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/kvx/Asmgenproof.v b/kvx/Asmgenproof.v index f43acd37..9e35e268 100644 --- a/kvx/Asmgenproof.v +++ b/kvx/Asmgenproof.v @@ -13,7 +13,7 @@ (* *) (* *************************************************************) -(** Correctness proof for Asmgen *) +(** Composing all passes from Mach to KVX Asm *) Require Import Coqlib Errors. Require Import Integers Floats AST Linking. @@ -46,7 +46,7 @@ Proof. exists tp; split. apply Asm.transf_program_match; auto. auto. Qed. -(** Return Address Offset *) +(** Return Address Offset for Mach *) Definition return_address_offset: Mach.function -> Mach.code -> ptrofs -> Prop := Mach_return_address_offset Asmblockgenproof.return_address_offset. @@ -59,6 +59,7 @@ Proof. intros; eapply Asmblockgenproof.return_address_exists; eauto. Qed. +(** Main preservation theorem: from Mach to KVX Asm *) Section PRESERVATION. @@ -86,7 +87,7 @@ End PRESERVATION. Instance TransfAsm: TransfLink match_prog := pass_match_link (compose_passes block_passes). (*******************************************) -(* Stub actually needed by driver/Compiler *) +(** Stub actually needed by driver/Compiler *) Module Asmgenproof0. |