From 2e39ecb491bbd001ecdfba73115bc76e3f53f517 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 29 Jul 2020 09:17:26 +0200 Subject: Improving the coqdoc --- kvx/Asmgenproof.v | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'kvx/Asmgenproof.v') 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. -- cgit