1 files changed, 56 insertions, 38 deletions

diff --git a/kvx/abstractbb/AbstractBasicBlocksDef.v b/kvx/abstractbb/AbstractBasicBlocksDef.v
index 0b1c502d..6960f363 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 :=
@@ -168,7 +170,7 @@ Lemma exp_equiv e old1 old2:
    (exp_eval e m1 old1) = (exp_eval e m2 old2).
 Proof.
   intros H1.
-  induction e using exp_mut with (P0:=fun l =>  forall m1 m2, (forall x, m1 x = m2 x) -> list_exp_eval l m1 old1 = list_exp_eval l m2 old2); simpl; try congruence; auto.
+  induction e using exp_mut with (P0:=fun l =>  forall m1 m2, (forall x, m1 x = m2 x) -> list_exp_eval l m1 old1 = list_exp_eval l m2 old2); cbn; try congruence; auto.
   - intros; erewrite IHe; eauto.
   - intros; erewrite IHe, IHe0; auto.
 Qed.
@@ -181,38 +183,38 @@ Lemma inst_equiv_refl i old1 old2:
   forall m1 m2, (forall x, m1 x = m2 x) -> 
   res_eq (inst_run i m1 old1) (inst_run i m2 old2).
 Proof.
-  intro H; induction i as [ | [x e]]; simpl; eauto.
+  intro H; induction i as [ | [x e]]; cbn; eauto.
   intros m1 m2 H1. erewrite exp_equiv; eauto.
-  destruct (exp_eval e m2 old2); simpl; auto.
+  destruct (exp_eval e m2 old2); cbn; auto.
   apply IHi.
   unfold assign; intro y. destruct (R.eq_dec x y); auto. 
 Qed.
 
 Lemma bblock_equiv_refl p: forall m1 m2, (forall x, m1 x = m2 x) -> res_eq (run p m1) (run p m2).
 Proof.
-  induction p as [ | i p']; simpl; eauto.
+  induction p as [ | i p']; cbn; eauto.
   intros m1 m2 H; lapply (inst_equiv_refl i m1 m2); auto.
   intros X; lapply (X m1 m2); auto; clear X.
-  destruct (inst_run i m1 m1); simpl.
-  - intros [m3 [H1 H2]]; rewrite H1; simpl; auto.
-  - intros H1; rewrite H1; simpl; auto.
+  destruct (inst_run i m1 m1); cbn.
+  - intros [m3 [H1 H2]]; rewrite H1; cbn; auto.
+  - intros H1; rewrite H1; cbn; auto.
 Qed.
 
 Lemma res_eq_sym om1 om2: res_eq om1 om2 -> res_eq om2 om1.
 Proof.
-  destruct om1; simpl.
-  - intros [m2 [H1 H2]]; subst; simpl. eauto.
-  - intros; subst; simpl; eauto.
+  destruct om1; cbn.
+  - intros [m2 [H1 H2]]; subst; cbn. eauto.
+  - intros; subst; cbn; eauto.
 Qed.
 
 Lemma res_eq_trans (om1 om2 om3: option mem): 
   (res_eq om1 om2) -> (res_eq om2 om3) -> (res_eq om1 om3).
 Proof.
-  destruct om1; simpl.
-  - intros [m2 [H1 H2]]; subst; simpl.
-    intros [m3 [H3 H4]]; subst; simpl.
+  destruct om1; cbn.
+  - intros [m2 [H1 H2]]; subst; cbn.
+    intros [m3 [H3 H4]]; subst; cbn.
     eapply ex_intro; intuition eauto. rewrite H2; auto.
-  - intro; subst; simpl; auto.
+  - intro; subst; cbn; auto.
 Qed.
 
 Lemma bblock_simu_alt p1 p2: bblock_simu p1 p2 <-> (forall m1 m2,  (forall x, m1 x = m2 x) -> (run p1 m1)<>None -> res_eq (run p1 m1) (run p2 m2)).
@@ -230,8 +232,8 @@ Lemma run_app p1: forall m1 p2,
      | None => None
      end.
 Proof.
-   induction p1; simpl; try congruence.
-   intros; destruct (inst_run _ _ _); simpl; auto.
+   induction p1; cbn; try congruence.
+   intros; destruct (inst_run _ _ _); cbn; auto.
 Qed.
 
 Lemma run_app_None p1 m1 p2:
@@ -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)
@@ -328,17 +334,27 @@ Fixpoint allvalid ge (l: list term) m : Prop :=
 Lemma allvalid_extensionality ge (l: list term) m:
   allvalid ge l m <-> (forall t, List.In t l -> term_eval ge t m <> None).
 Proof.
-  induction l as [|t l]; simpl; try (tauto).
+  induction l as [|t l]; cbn; try (tauto).
   destruct l.
   - intuition (congruence || eauto).
   - 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,26 +362,24 @@ 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.
-  unfold match_pt; simpl; intros; intuition congruence.
+  unfold match_pt; cbn; intros; intuition congruence.
 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).
 Proof.
-  eapply intro_fail_correct; simpl; tauto.
+  eapply intro_fail_correct; cbn; tauto.
 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
@@ -376,15 +390,16 @@ Definition nofail (is_constant: op -> bool) (t: term):=
 Lemma nofail_correct (is_constant: op -> bool) t:
  (forall ge o, is_constant o = true -> op_eval ge o nil <> None) -> match_pt t (nofail is_constant t).
 Proof.
-  destruct t; simpl.
-  + intros; eapply intro_fail_correct; simpl; intuition congruence.
-  + intros; destruct l; simpl; auto with wlp.
-    destruct (is_constant o) eqn:Heqo; simpl; intuition eauto with wlp.
-     eapply intro_fail_correct; simpl; intuition eauto with wlp.
+  destruct t; cbn.
+  + intros; eapply intro_fail_correct; cbn; intuition congruence.
+  + intros; destruct l; cbn; auto with wlp.
+    destruct (is_constant o) eqn:Heqo; cbn; intuition eauto with wlp.
+     eapply intro_fail_correct; cbn; intuition eauto with wlp.
 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) |}.
 
@@ -409,7 +425,7 @@ Lemma app_fail_allvalid_correct l pt t1 t2: forall
   (V2: forall (ge : genv) (m : mem), term_eval ge t2 m <> None <-> allvalid ge (mayfail {| mayfail := t1 :: l; effect := t1 |}) m)
   (ge : genv) (m : mem), term_eval ge t2 m <> None <-> allvalid ge (mayfail (app_fail l pt)) m.
 Proof.
-  intros; generalize (V1 ge m) (V2 ge m); rewrite !allvalid_extensionality; simpl. clear V1 V2.
+  intros; generalize (V1 ge m) (V2 ge m); rewrite !allvalid_extensionality; cbn. clear V1 V2.
   intuition subst.
   + rewrite rev_append_rev, in_app_iff, <- in_rev in H3. destruct H3; eauto.
   + eapply H3; eauto.
@@ -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;