1 files changed, 11 insertions, 10 deletions
diff --git a/kvx/abstractbb/SeqSimuTheory.v b/kvx/abstractbb/SeqSimuTheory.v
index 61f8f2ec..a957c50a 100644
--- a/kvx/abstractbb/SeqSimuTheory.v
+++ b/kvx/abstractbb/SeqSimuTheory.v
@@ -55,13 +55,14 @@ with list_term_eval ge (l: list_term) (m: mem) {struct l}: option (list value) :
     end
   end.
 
-(* the symbolic memory:
-  - pre: pre-condition expressing that the computation has not yet abort on a None.
-  - post: the post-condition for each pseudo-register 
-*)
-Record smem:= {pre: genv -> mem -> Prop; post:> R.t -> term}.
-
-(** initial symbolic memory *)
+(** The (abstract) symbolic memory state *)
+Record smem :=
+{
+   pre: genv -> mem -> Prop; (**r pre-condition expressing that the computation has not yet abort on a None. *)
+   post:> R.t -> term (**r the output term computed on each pseudo-register *)
+}.
+
+(** Initial symbolic memory state *)
 Definition smem_empty := {| pre:=fun _ _ => True; post:=(fun x => Input x) |}.
 
 Fixpoint exp_term (e: exp) (d old: smem) : term :=
@@ -78,11 +79,12 @@ with list_exp_term (le: list_exp) (d old: smem) : list_term :=
   end.
 
 
-(** assignment of the symbolic memory *)
+(** assignment of the symbolic memory state *)
 Definition smem_set (d:smem) x (t:term) := 
   {| pre:=(fun ge m => (term_eval ge (d x) m) <> None /\ (d.(pre) ge m));
      post:=fun y => if R.eq_dec x y then t else d y |}.
 
+(** Simulation theory: the theorem [bblock_smem_simu] ensures that the simulation between two abstract basic blocks is implied by the simulation between their symbolic execution. *)
 Section SIMU_THEORY.
 
 Variable ge: genv.
@@ -375,8 +377,7 @@ Qed.
 
 End SIMU_THEORY.
 
-(** REMARKS: more abstract formulation of the proof... 
-    but relying on functional_extensionality.
+(** REMARK: this theorem reformulates the lemma above in a more abstract way (but relies on functional_extensionality axiom).
 *)
 Definition smem_correct ge (d: smem) (m: mem) (om: option mem): Prop:=
    forall m', om=Some m' <-> (d.(pre) ge m /\ forall x, term_eval ge (d x) m = Some (m' x)).