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/Asmblockdeps.v | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) (limited to 'kvx/Asmblockdeps.v') diff --git a/kvx/Asmblockdeps.v b/kvx/Asmblockdeps.v index 1881e7e9..3d981100 100644 --- a/kvx/Asmblockdeps.v +++ b/kvx/Asmblockdeps.v @@ -12,12 +12,14 @@ (* *) (* *************************************************************) -(** * Translation from Asmblock to AbstractBB +(** * Translation from [Asmvliw] to [AbstractBB] *) - We define a specific instance of AbstractBB, named L, translate bblocks from Asmblock into this instance - AbstractBB will then define two semantics for L : a sequential, and a semantic one - We prove a bisimulation between the parallel semantics of L and AsmVLIW - From this, we also deduce a bisimulation between the sequential semantics of L and Asmblock *) +(** We define a specific instance [L] of [AbstractBB] and translate [bblocks] from [Asmvliw] into [L]. + [AbstractBB] will then define two semantics for [L]: a sequential and a parallel one. + We prove a bisimulation between the parallel semantics of [L] and [AsmVLIW]. + We also prove a bisimulation between the sequential semantics of [L] and [Asmblock]. + Then, the checkers on [Asmblock] and [Asmvliw] are deduced from those of [L]. + *) Require Import AST. Require Import Asmblock. @@ -40,7 +42,7 @@ Require Import Lia. Open Scope impure. -(** Definition of L *) +(** Definition of [L] *) Module P<: ImpParam. Module R := Pos. @@ -660,7 +662,7 @@ Module IST := ImpSimu L ImpPosDict. Import L. Import P. -(** Compilation from Asmblock to L *) +(** Compilation from [Asmvliw] to [L] *) Local Open Scope positive_scope. @@ -748,6 +750,8 @@ Definition inv_ppos (p: R.t) : option preg := Notation "a @ b" := (Econs a b) (at level 102, right associativity). +(** Translations of instructions *) + Definition trans_control (ctl: control) : inst := match ctl with | Pret => [(#PC, PReg(#RA))] @@ -859,6 +863,8 @@ Proof. intros. destruct bb as [hdr bdy ex COR]; unfold no_header; simpl. unfold trans_block. simpl. reflexivity. Qed. +(** Lemmas on the translation *) + Definition state := L.mem. Definition exec := L.run. @@ -1800,6 +1806,7 @@ Definition bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock) : ?? bool := Local Hint Resolve IST.bblock_simu_test_correct bblock_simu_reduce IST.verb_bblock_simu_test_correct: wlp. +(** Main simulation (Impure) theorem *) Theorem bblock_simu_test_correct verb p1 p2 : WHEN bblock_simu_test verb p1 p2 ~> b THEN b=true -> forall ge fn, Asmblockprops.bblock_simu ge fn p1 p2. Proof. @@ -1807,7 +1814,7 @@ Proof. Qed. Hint Resolve bblock_simu_test_correct: wlp. -(* Coerce bblock_simu_test into a pure function (this is a little unsafe like all oracles in CompCert). *) +(** ** Coerce bblock_simu_test into a pure function (this is a little unsafe like all oracles in CompCert). *) Import UnsafeImpure. -- cgit