From fd09c489f94df50c6579973e85c205ec07d60187 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Fri, 31 Jul 2020 08:16:51 +0200
Subject: Improving Coqdoc on abstractbb

---
 kvx/abstractbb/AbstractBasicBlocksDef.v | 44 +++++++++++++++++++++++----------
 1 file changed, 31 insertions(+), 13 deletions(-)

(limited to 'kvx/abstractbb/AbstractBasicBlocksDef.v')

diff --git a/kvx/abstractbb/AbstractBasicBlocksDef.v b/kvx/abstractbb/AbstractBasicBlocksDef.v
index 0b1c502d..948ed660 100644
--- a/kvx/abstractbb/AbstractBasicBlocksDef.v
+++ b/kvx/abstractbb/AbstractBasicBlocksDef.v
@@ -45,7 +45,7 @@ End LangParam.
 
 
 
-(** * Syntax and (sequential) semantics of "basic blocks" *)
+(** * Syntax and (sequential) semantics of "abstract basic blocks" *)
 Module MkSeqLanguage(P: LangParam).
 
 Export P.
@@ -62,12 +62,12 @@ Definition assign (m: mem) (x:R.t) (v: value): mem
   := fun y => if R.eq_dec x y then v else m y.
 
 
-(** expressions *)
+(** Expressions *)
 
 Inductive exp :=
-  | PReg (x:R.t)
-  | Op (o:op) (le: list_exp)
-  | Old (e: exp)
+  | PReg (x:R.t)              (**r pseudo-register *)
+  | Op (o:op) (le: list_exp)  (**r operation *)
+  | Old (e: exp)              (**r evaluation of [e] in the initial state of the instruction (see [inst] below) *)
 with list_exp :=
   | Enil
   | Econs (e:exp) (le:list_exp)
@@ -95,7 +95,8 @@ with list_exp_eval (le: list_exp) (m old: mem): option (list value) :=
   | LOld le => list_exp_eval le old old
   end.
 
-Definition inst := list (R.t * exp). (* = a sequence of assignments *) 
+(** An instruction represents a sequence of assignments where [Old] refers to the initial state of the sequence. *) 
+Definition inst := list (R.t * exp). 
 
 Fixpoint inst_run (i: inst) (m old: mem): option mem :=
   match i with
@@ -107,6 +108,7 @@ Fixpoint inst_run (i: inst) (m old: mem): option mem :=
      end
   end.
 
+(** A basic block is a sequence of instructions. *) 
 Definition bblock := list inst.
 
 Fixpoint run (p: bblock) (m: mem): option mem :=
@@ -250,12 +252,16 @@ Qed.
 
 End SEQLANG.
 
-Module Terms.
 
-(** terms in the symbolic evaluation 
-NB: such a term represents the successive computations in one given pseudo-register
+(** * Terms in the symbolic execution *)
+
+(** Such a term represents the successive computations in one given pseudo-register. 
+The [hid] has no formal semantics: it is only used by the hash-consing oracle (itself dynamically checked to behave like an identity function).
+
 *)
 
+Module Terms.
+
 Inductive term :=
   | Input (x:R.t) (hid:hashcode)
   | App (o: op) (l: list_term) (hid:hashcode)
@@ -334,11 +340,21 @@ Proof.
   - rewrite IHl; clear IHl. intuition (congruence || eauto).
 Qed.
 
+(** * Rewriting rules in the symbolic execution *)
+
+(** The symbolic execution is parametrized by rewriting rules on pseudo-terms. *)
+
 Record pseudo_term: Type := intro_fail {
   mayfail: list term;
   effect: term
 }.
 
+(** Simulation relation between a term and a pseudo-term *)
+
+Definition match_pt (t: term) (pt: pseudo_term) :=
+      (forall ge m, term_eval ge t m <> None <-> allvalid ge pt.(mayfail) m)
+   /\ (forall ge m0 m1, term_eval ge t m0 = Some m1 -> term_eval ge pt.(effect) m0 = Some m1).
+
 Lemma inf_option_equivalence (A:Type) (o1 o2: option A):
   (o1 <> None -> o1 = o2) <-> (forall m1, o1 = Some m1 -> o2 = Some m1).
 Proof.
@@ -346,10 +362,6 @@ Proof.
   symmetry; eauto.
 Qed.
 
-Definition match_pt (t: term) (pt: pseudo_term) :=
-      (forall ge m, term_eval ge t m <> None <-> allvalid ge pt.(mayfail) m)
-   /\ (forall ge m0 m1, term_eval ge t m0 = Some m1 -> term_eval ge pt.(effect) m0 = Some m1).
-
 Lemma intro_fail_correct (l: list term) (t: term) :
    (forall ge m, term_eval ge t m <> None <-> allvalid ge l m) -> match_pt t (intro_fail l t).
 Proof.
@@ -357,6 +369,7 @@ Proof.
 Qed.
 Hint Resolve intro_fail_correct: wlp.
 
+(** The default reduction of a term to a pseudo-term *) 
 Definition identity_fail (t: term):= intro_fail [t] t.
 
 Lemma identity_fail_correct (t: term): match_pt t (identity_fail t).
@@ -366,6 +379,7 @@ Qed.
 Global Opaque identity_fail.
 Hint Resolve identity_fail_correct: wlp.
 
+(** The reduction for constant term *) 
 Definition nofail (is_constant: op -> bool) (t: term):=
     match t with
     | Input x _ => intro_fail ([])%list t
@@ -385,6 +399,7 @@ Qed.
 Global Opaque nofail.
 Hint Resolve nofail_correct: wlp.
 
+(** Term equivalence preserve the simulation by pseudo-terms *)
 Definition term_equiv t1 t2:= forall ge m, term_eval ge t1 m = term_eval ge t2 m.
 
 Global Instance term_equiv_Equivalence : Equivalence term_equiv.
@@ -401,6 +416,7 @@ Proof.
 Qed.
 Hint Resolve match_pt_term_equiv: wlp.
 
+(** Other generic reductions *)
 Definition app_fail (l: list term) (pt: pseudo_term): pseudo_term :=
   {| mayfail := List.rev_append l pt.(mayfail); effect := pt.(effect) |}.
 
@@ -431,6 +447,8 @@ Extraction Inline app_fail.
 Import ImpCore.Notations.
 Local Open Scope impure_scope.
 
+(** Specification of rewriting functions in parameter of the symbolic execution: in the impure monad, because the rewriting functions produce hash-consed terms (wrapped in pseudo-terms).
+*)
 Record reduction:= {
   result:> term -> ?? pseudo_term;
   result_correct: forall t, WHEN result t ~> pt THEN match_pt t pt;
-- 
cgit