Finished renaming

2 files changed, 339 insertions, 337 deletions

diff --git a/mppa_k1c/lib/RTLpathSE_theory.v b/mppa_k1c/lib/RTLpathSE_theory.v
index 9c0c0c0a..e38e66dd 100644
--- a/mppa_k1c/lib/RTLpathSE_theory.v
+++ b/mppa_k1c/lib/RTLpathSE_theory.v
@@ -83,7 +83,7 @@ with seval_smem (ge: RTL.genv) (sp:val) (sm: smem) (rs0: regset) (m0: mem): opti
 (* [si_pre] is a precondition on initial ge, sp, rs0, m0 *)
 Record sistate_local := { si_pre: RTL.genv -> val -> regset -> mem -> Prop; si_sreg: reg -> sval; si_smem: smem }.
 
-Definition smatch_local (ge: RTL.genv) (sp:val) (st: sistate_local) (rs0: regset) (m0: mem) (rs: regset) (m: mem): Prop :=
+Definition simatch_local (ge: RTL.genv) (sp:val) (st: sistate_local) (rs0: regset) (m0: mem) (rs: regset) (m: mem): Prop :=
   st.(si_pre) ge sp rs0 m0
   /\ seval_smem ge sp st.(si_smem) rs0 m0 = Some m
   /\ forall (r:reg), seval_sval ge sp (st.(si_sreg) r) rs0 m0 = Some (rs#r).
@@ -111,46 +111,46 @@ Definition sabort_exits ge sp (lx: list sistate_exit) rs0 m0: Prop :=
     /\ seval_condition ge sp ext.(si_cond) ext.(si_scondargs) ext.(si_elocal).(si_smem) rs0 m0 = None.
 
 
-Inductive smatch_exits (ge: RTL.genv) (sp:val) (lx:list sistate_exit) (rs0: regset) (m0: mem) rs m pc: Prop :=
-  smatch_exits_intro ext lx':
+Inductive simatch_exits (ge: RTL.genv) (sp:val) (lx:list sistate_exit) (rs0: regset) (m0: mem) rs m pc: Prop :=
+  simatch_exits_intro ext lx':
     is_tail (ext::lx') lx ->
     all_fallthrough ge sp lx' rs0 m0 ->
     seval_condition ge sp ext.(si_cond) ext.(si_scondargs) ext.(si_elocal).(si_smem) rs0 m0 = Some true ->
-    smatch_local ge sp ext.(si_elocal) rs0 m0 rs m ->
+    simatch_local ge sp ext.(si_elocal) rs0 m0 rs m ->
     ext.(si_ifso) = pc ->
-    smatch_exits ge sp lx rs0 m0 rs m pc.
+    simatch_exits ge sp lx rs0 m0 rs m pc.
 
 
 (** * Syntax and Semantics of symbolic internal state *)
 Record sistate := { si_pc: node; si_exits: list sistate_exit; si_local: sistate_local }. 
 
-Definition smatch (ge: RTL.genv) (sp:val) (st: sistate) (rs0: regset) (m0: mem) (is: istate): Prop :=
+Definition simatch (ge: RTL.genv) (sp:val) (st: sistate) (rs0: regset) (m0: mem) (is: istate): Prop :=
   if (is.(icontinue)) 
   then 
-    smatch_local ge sp st.(si_local) rs0 m0 is.(irs) is.(imem) 
+    simatch_local ge sp st.(si_local) rs0 m0 is.(irs) is.(imem)
     /\ st.(si_pc) = is.(ipc)
     /\ all_fallthrough ge sp st.(si_exits) rs0 m0
-  else smatch_exits ge sp st.(si_exits) rs0 m0 is.(irs) is.(imem) is.(ipc).
+  else simatch_exits ge sp st.(si_exits) rs0 m0 is.(irs) is.(imem) is.(ipc).
 
 Definition sabort (ge: RTL.genv) (sp:val) (st: sistate) (rs0: regset) (m0: mem): Prop :=
     sabort_local ge sp st.(si_local) rs0 m0
  \/ sabort_exits ge sp st.(si_exits) rs0 m0.
 
-Definition smatch_opt ge sp (st: sistate) rs0 m0 (ois: option istate): Prop :=
+Definition simatch_opt ge sp (st: sistate) rs0 m0 (ois: option istate): Prop :=
   match ois with
-  | Some is => smatch ge sp st rs0 m0 is
+  | Some is => simatch ge sp st rs0 m0 is
   | None => sabort ge sp st rs0 m0
   end.
 
-Definition smatch_opt2 ge sp (ost: option sistate) rs0 m0 (ois: option istate) : Prop :=
+Definition simatch_opt2 ge sp (ost: option sistate) rs0 m0 (ois: option istate) : Prop :=
   match ost with
-  | Some st => smatch_opt ge sp st rs0 m0 ois
+  | Some st => simatch_opt ge sp st rs0 m0 ois
   | None => ois=None
   end.
 
 (** * An internal state represents a parallel program !
 
-     We prove below that the semantics [sem_option_istate] is deterministic.
+     We prove below that the semantics [simatch_opt] is deterministic.
 
  *)
 
@@ -162,15 +162,15 @@ Definition istate_eq ist1 ist2 :=
 
 (* TODO: is it useful 
 Lemma has_not_yet_exit_cons_split ge sp ext lx rs0 m0:
-   has_not_yet_exit ge sp (ext::lx) rs0 m0 <-> 
-    (seval_condition ge sp ext.(the_cond) ext.(cond_args) ext.(exit_ist).(the_smem) rs0 m0 = Some false /\ has_not_yet_exit ge sp lx rs0 m0).
+   all_fallthrough ge sp (ext::lx) rs0 m0 <->
+    (seval_condition ge sp ext.(the_cond) ext.(cond_args) ext.(exit_ist).(si_smem) rs0 m0 = Some false /\ all_fallthrough ge sp lx rs0 m0).
 Proof.
-  unfold has_not_yet_exit; simpl; intuition (subst; auto).
+  unfold all_fallthrough; simpl; intuition (subst; auto).
 Qed.
 *)
 
 Lemma all_fallthrough_noexit ge sp st rs0 m0 rs m pc:
-  smatch_exits ge sp (si_exits st) rs0 m0 rs m pc ->
+  simatch_exits ge sp (si_exits st) rs0 m0 rs m pc ->
   all_fallthrough ge sp (si_exits st) rs0 m0 ->
   False.
 Proof.
@@ -180,37 +180,37 @@ Proof.
   try congruence.
 Qed.
 
-Lemma smatch_exclude_incompatible_continue ge sp st rs m is1 is2:
+Lemma simatch_exclude_incompatible_continue ge sp st rs m is1 is2:
   is1.(icontinue) = true ->
   is2.(icontinue) = false ->
-  smatch ge sp st rs m is1 ->
-  smatch ge sp st rs m is2 ->
+  simatch ge sp st rs m is1 ->
+  simatch ge sp st rs m is2 ->
   False.
 Proof.
   Local Hint Resolve all_fallthrough_noexit: core.
-  unfold smatch.
+  unfold simatch.
   intros CONT1 CONT2.
   rewrite CONT1, CONT2; simpl.
   intuition eauto.
 Qed.
 
-Lemma smatch_determ_continue ge sp st rs m is1 is2:
-   smatch ge sp st rs m is1 ->
-   smatch ge sp st rs m is2 ->
+Lemma simatch_determ_continue ge sp st rs m is1 is2:
+   simatch ge sp st rs m is1 ->
+   simatch ge sp st rs m is2 ->
    is1.(icontinue) = is2.(icontinue).
 Proof.
-   Local Hint Resolve smatch_exclude_incompatible_continue: core.
+   Local Hint Resolve simatch_exclude_incompatible_continue: core.
    destruct (Bool.bool_dec is1.(icontinue) is2.(icontinue)) as [|H]; auto.
    intros H1 H2. assert (absurd: False); intuition.
    destruct (icontinue is1) eqn: His1, (icontinue is2) eqn: His2; eauto.
 Qed.
 
-Lemma smatch_local_determ ge sp st rs0 m0 rs1 m1 rs2 m2:
-  smatch_local ge sp st rs0 m0 rs1 m1 ->
-  smatch_local ge sp st rs0 m0 rs2 m2 ->
+Lemma simatch_local_determ ge sp st rs0 m0 rs1 m1 rs2 m2:
+  simatch_local ge sp st rs0 m0 rs1 m1 ->
+  simatch_local ge sp st rs0 m0 rs2 m2 ->
   (forall r, rs1#r = rs2#r) /\ m1 = m2.
 Proof.
-  unfold smatch_local. intuition try congruence.
+  unfold simatch_local. intuition try congruence.
   generalize (H5 r); rewrite H4; congruence.
 Qed.
 
@@ -241,9 +241,9 @@ Proof.
   try congruence.
 Qed.
 
-Lemma smatch_exits_determ ge sp lx rs0 m0 rs1 m1 pc1 rs2 m2 pc2 :
-  smatch_exits ge sp lx rs0 m0 rs1 m1 pc1 ->
-  smatch_exits ge sp lx rs0 m0 rs2 m2 pc2 ->
+Lemma simatch_exits_determ ge sp lx rs0 m0 rs1 m1 pc1 rs2 m2 pc2 :
+  simatch_exits ge sp lx rs0 m0 rs1 m1 pc1 ->
+  simatch_exits ge sp lx rs0 m0 rs2 m2 pc2 ->
   pc1 = pc2 /\ (forall r, rs1#r = rs2#r) /\ m1 = m2.
 Proof.
   Local Hint Resolve exit_cond_determ eq_sym: core.
@@ -251,31 +251,31 @@ Proof.
   destruct 1 as [ext2 lx2 TAIL2 NYE2 EVAL2 SEM2 PC2]; subst.
   assert (X:ext1=ext2).
   - destruct (is_tail_bounded_total (ext1 :: lx1) (ext2::lx2) lx) as [TAIL|TAIL]; eauto.
-  - subst. destruct (smatch_local_determ ge sp (si_elocal ext2) rs0 m0 rs1 m1 rs2 m2); auto.
+  - subst. destruct (simatch_local_determ ge sp (si_elocal ext2) rs0 m0 rs1 m1 rs2 m2); auto.
 Qed.
 
-Lemma smatch_determ ge sp st rs m is1 is2:
-  smatch ge sp st rs m is1 ->
-  smatch ge sp st rs m is2 ->
+Lemma simatch_determ ge sp st rs m is1 is2:
+  simatch ge sp st rs m is1 ->
+  simatch ge sp st rs m is2 ->
   istate_eq is1 is2.
 Proof.
   unfold istate_eq.
   intros SEM1 SEM2. 
-  exploit (smatch_determ_continue ge sp st rs m is1 is2); eauto.
-  intros CONTEQ. unfold smatch in * |-. rewrite CONTEQ in * |- *.
+  exploit (simatch_determ_continue ge sp st rs m is1 is2); eauto.
+  intros CONTEQ. unfold simatch in * |-. rewrite CONTEQ in * |- *.
   destruct (icontinue is2).
-  - destruct (smatch_local_determ ge sp (si_local st) rs m (irs is1) (imem is1) (irs is2) (imem is2)); 
+  - destruct (simatch_local_determ ge sp (si_local st) rs m (irs is1) (imem is1) (irs is2) (imem is2)); 
     intuition (try congruence).
-  - destruct (smatch_exits_determ ge sp (si_exits st) rs m (irs is1) (imem is1) (ipc is1) (irs is2) (imem is2) (ipc is2));
+  - destruct (simatch_exits_determ ge sp (si_exits st) rs m (irs is1) (imem is1) (ipc is1) (irs is2) (imem is2) (ipc is2));
     intuition.
 Qed.
 
-Lemma smatch_exclude_sabort_local_continue ge sp st rs m is:
+Lemma simatch_exclude_sabort_local_continue ge sp st rs m is:
   icontinue is = true ->
   sabort_local ge sp (si_local st) rs m ->
-  smatch ge sp st rs m is -> False.
+  simatch ge sp st rs m is -> False.
 Proof.
-  intros CONT ABORT SEM. unfold smatch in SEM. rewrite CONT in SEM.
+  intros CONT ABORT SEM. unfold simatch in SEM. rewrite CONT in SEM.
   destruct SEM as (SEML & _ & _). inversion SEML as (SEML1 & SEML2 & SEML3); clear SEML.
   inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; clear ABORT.
   - contradiction.
@@ -283,13 +283,13 @@ Proof.
   - inv ABORT3. rewrite SEML3 in H. discriminate.
 Qed.
 
-Lemma smatch_exclude_sabort_local_nocontinue ge sp st rs0 m0 is:
+Lemma simatch_exclude_sabort_local_nocontinue ge sp st rs0 m0 is:
   icontinue is = false ->
   sabort_local ge sp (si_local st) rs0 m0 ->
-  smatch ge sp st rs0 m0 is -> False.
+  simatch ge sp st rs0 m0 is -> False.
 Proof.
-(*   intros CONT ABORT SEM. unfold sem_istate in SEM. rewrite CONT in SEM.
-  destruct st as [pc exits iis]. simpl in *.
+(*   intros CONT ABORT SEM. unfold simatch in SEM. rewrite CONT in SEM.
+  destruct st as [pc si_exits iis]. simpl in *.
   destruct is as [cont pc' rs' m']. simpl in *.
   inv SEM. inversion H2 as (SEML1 & SEML2 & SEML3); clear H2.
   inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; clear ABORT.
@@ -299,42 +299,42 @@ Proof.
 Admitted.
 
 
-Lemma smatch_exclude_sabort_local ge sp st rs m is:
+Lemma simatch_exclude_sabort_local ge sp st rs m is:
   sabort_local ge sp (si_local st) rs m ->
-  smatch ge sp st rs m is -> False.
+  simatch ge sp st rs m is -> False.
 Proof.
   intros. destruct (icontinue is) eqn:CONT.
-  - eapply smatch_exclude_sabort_local_continue; eauto.
-  - eapply smatch_exclude_sabort_local_nocontinue; eauto.
+  - eapply simatch_exclude_sabort_local_continue; eauto.
+  - eapply simatch_exclude_sabort_local_nocontinue; eauto.
 Qed.
 
-Lemma smatch_exclude_sabort_exits ge sp st rs m is:
+Lemma simatch_exclude_sabort_exits ge sp st rs m is:
   sabort_exits ge sp (si_exits st) rs m ->
-  smatch ge sp st rs m is -> False.
+  simatch ge sp st rs m is -> False.
 Proof.
 Admitted.
 
-Lemma smatch_exclude_sabort ge sp st rs m is:
+Lemma simatch_exclude_sabort ge sp st rs m is:
   sabort ge sp st rs m ->
-  smatch ge sp st rs m is -> False.
+  simatch ge sp st rs m is -> False.
 Proof.
   intros ABORT SEM.
   inv ABORT.
-  - eapply smatch_exclude_sabort_local; eauto.
-  - eapply smatch_exclude_sabort_exits; eauto.
+  - eapply simatch_exclude_sabort_local; eauto.
+  - eapply simatch_exclude_sabort_exits; eauto.
 Qed.
 
 Definition istate_eq_opt ist1 oist :=
   exists ist2, oist = Some ist2 /\ istate_eq ist1 ist2.
 
-Lemma smatch_opt_determ ge sp st rs m ois is:
-  smatch_opt ge sp st rs m ois ->
-  smatch ge sp st rs m is ->
+Lemma simatch_opt_determ ge sp st rs m ois is:
+  simatch_opt ge sp st rs m ois ->
+  simatch ge sp st rs m is ->
   istate_eq_opt is ois.
 Proof.
   destruct ois as [is1|]; simpl; eauto.
-  - intros; eexists; intuition; eapply smatch_determ; eauto.
-  - intros; exploit smatch_exclude_sabort; eauto. destruct 1.
+  - intros; eexists; intuition; eapply simatch_determ; eauto.
+  - intros; exploit simatch_exclude_sabort; eauto. destruct 1.
 Qed.
 
 (** * Symbolic execution of one internal step *)
@@ -353,7 +353,7 @@ Definition sist_set_local (st: sistate) (pc: node) (nxt: sistate_local): option
    Some {| si_pc := pc; si_exits := st.(si_exits); si_local:= nxt |}.
 
 (* FIXME - add notrap *)
-Definition symb_istep (i: instruction) (st: sistate): option sistate := 
+Definition sistep (i: instruction) (st: sistate): option sistate :=
   match i with
   | Inop pc' => 
       sist_set_local st pc' st.(si_local)
@@ -380,11 +380,10 @@ Definition symb_istep (i: instruction) (st: sistate): option sistate :=
   | _ => None (* TODO jumptable ? *)
   end.
 
-(* TODO TODO - continue renaming *)
 
-Lemma list_sval_eval_inj ge sp l rs0 m0 (sreg: reg -> sval) rs: 
-   (forall r : reg, seval ge sp (sreg r) rs0 m0 = Some (rs # r)) ->
-   list_sval_eval ge sp (list_sval_inj (map sreg l)) rs0 m0 = Some (rs ## l).
+Lemma seval_list_sval_inj ge sp l rs0 m0 (sreg: reg -> sval) rs: 
+   (forall r : reg, seval_sval ge sp (sreg r) rs0 m0 = Some (rs # r)) ->
+   seval_list_sval ge sp (list_sval_inj (map sreg l)) rs0 m0 = Some (rs ## l).
 Proof.
   intros H; induction l as [|r l]; simpl; auto.
   inversion_SOME v.
@@ -393,242 +392,242 @@ Proof.
   try_simplify_someHyps.
 Qed.
 
-Lemma symb_istep_preserv_early_exits i ge sp st rs0 m0 rs m pc st':
-  sem_early_exit ge sp st.(exits) rs0 m0 rs m pc ->
-  symb_istep i st = Some st' ->
-  sem_early_exit ge sp st'.(exits) rs0 m0 rs m pc.
+Lemma sistep_preserves_simatch_exits i ge sp st rs0 m0 rs m pc st':
+  simatch_exits ge sp st.(si_exits) rs0 m0 rs m pc ->
+  sistep i st = Some st' ->
+  simatch_exits ge sp st'.(si_exits) rs0 m0 rs m pc.
 Proof.
   intros H.
-  destruct i; simpl; unfold sist, sem_istate, sem_local_istate; simpl; try_simplify_someHyps.
+  destruct i; simpl; unfold sist_set_local, simatch, simatch_local; simpl; try_simplify_someHyps.
   destruct H as [ext lx TAIL NYE COND INV PC].
   econstructor; try (eapply is_tail_cons; eapply TAIL); eauto.
 Qed.
 
-Lemma sreg_set_preserv_has_aborted ge sp st rs0 m0 r sv:
-  has_aborted_on_basic ge sp st rs0 m0 ->
-  has_aborted_on_basic ge sp (sreg_set st r sv) rs0 m0.
+Lemma slocal_set_sreg_preserves_sabort_local ge sp st rs0 m0 r sv:
+  sabort_local ge sp st rs0 m0 ->
+  sabort_local ge sp (slocal_set_sreg st r sv) rs0 m0.
 Proof.
-  unfold has_aborted_on_basic. simpl; intuition.
+  unfold sabort_local. simpl; intuition.
   destruct H as [r1 H]. destruct (Pos.eq_dec r r1) as [TEST|TEST] eqn: HTEST.
   - subst; rewrite H; intuition.
   - right. right. exists r1. rewrite HTEST. auto.
 Qed.
 
-Lemma smem_set_preserv_has_aborted ge sp st rs0 m0 m:
-  has_aborted_on_basic ge sp st rs0 m0 ->
-  has_aborted_on_basic ge sp (smem_set st m) rs0 m0.
+Lemma slocal_set_smem_preserves_sabort_local ge sp st rs0 m0 m:
+  sabort_local ge sp st rs0 m0 ->
+  sabort_local ge sp (slocal_set_smem st m) rs0 m0.
 Proof.
-  unfold has_aborted_on_basic. simpl; intuition.
+  unfold sabort_local. simpl; intuition.
 Qed.
 
-Lemma symb_istep_preserv_has_aborted i ge sp rs0 m0 st st': 
-  symb_istep i st = Some st' ->
-  has_aborted ge sp st rs0 m0 -> has_aborted ge sp st' rs0 m0.
+Lemma sistep_preserves_sabort i ge sp rs0 m0 st st':
+  sistep i st = Some st' ->
+  sabort ge sp st rs0 m0 -> sabort ge sp st' rs0 m0.
 Proof.
-  Local Hint Resolve sreg_set_preserv_has_aborted smem_set_preserv_has_aborted: core.
-  unfold has_aborted.
-  destruct i; simpl; unfold sist, sem_istate, sem_local_istate; simpl; try_simplify_someHyps; intuition eauto.
+  Local Hint Resolve slocal_set_sreg_preserves_sabort_local slocal_set_smem_preserves_sabort_local: core.
+  unfold sabort.
+  destruct i; simpl; unfold sist_set_local, simatch, simatch_local; simpl; try_simplify_someHyps; intuition eauto.
   (* COND *)
-  right. unfold has_aborted_on_test in * |- *.
+  right. unfold sabort_exits in * |- *.
   destruct H as (ext & H1 & H2).
   simpl; exists ext; intuition.
 Qed.
 
-Lemma symb_istep_WF i st:
-  symb_istep i st = None -> default_succ i = None.
+Lemma sistep_WF i st:
+  sistep i st = None -> default_succ i = None.
 Proof.
-  destruct i; simpl; unfold sist; simpl; congruence.
+  destruct i; simpl; unfold sist_set_local; simpl; congruence.
 Qed.
 
-Lemma symb_istep_default_succ i st st':
-  symb_istep i st = Some st' -> default_succ i = Some (st'.(the_pc)).
+Lemma sistep_default_succ i st st':
+  sistep i st = Some st' -> default_succ i = Some (st'.(si_pc)).
 Proof.
-  destruct i; simpl; unfold sist; simpl; try congruence;
+  destruct i; simpl; unfold sist_set_local; simpl; try congruence;
   intro H; inversion_clear H; simpl; auto.
 Qed.
 
-Lemma symb_istep_correct ge sp i st rs0 m0 rs m:
-  sem_local_istate ge sp st.(curr) rs0 m0 rs m ->
-  has_not_yet_exit ge sp st.(exits) rs0 m0 ->
-  sem_option2_istate ge sp (symb_istep i st) rs0 m0 (istep ge i sp rs m).
+Lemma sistep_correct ge sp i st rs0 m0 rs m:
+  simatch_local ge sp st.(si_local) rs0 m0 rs m ->
+  all_fallthrough ge sp st.(si_exits) rs0 m0 ->
+  simatch_opt2 ge sp (sistep i st) rs0 m0 (istep ge i sp rs m).
 Proof.
   intros (PRE & MEM & REG) NYE.
   destruct i; simpl; auto.
   + (* Nop *)
-    unfold sem_istate, sem_local_istate; simpl; try_simplify_someHyps.
+    unfold simatch, simatch_local; simpl; try_simplify_someHyps.
   + (* Op *)
     inversion_SOME v; intros OP; simpl.
-    - unfold sem_istate, sem_local_istate; simpl; intuition.
+    - unfold simatch, simatch_local; simpl; intuition.
       * exploit REG. try_simplify_someHyps.
       * destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto].
         subst; rewrite Regmap.gss; simpl; auto.
-        erewrite list_sval_eval_inj; simpl; auto.
+        erewrite seval_list_sval_inj; simpl; auto.
         try_simplify_someHyps.
-    - unfold has_aborted, has_aborted_on_basic; simpl. 
+    - unfold sabort, sabort_local; simpl.
       left. right. right.
       exists r. destruct (Pos.eq_dec r r); try congruence.
-      simpl. erewrite list_sval_eval_inj; simpl; auto.
+      simpl. erewrite seval_list_sval_inj; simpl; auto.
       try_simplify_someHyps.
   + (* LOAD *) admit. (* FIXME *)
 (*     inversion_SOME a0; intros ADD.
     { inversion_SOME v; intros LOAD; simpl.
-      - explore_destruct; unfold sem_istate, sem_local_istate; simpl; intuition.
+      - explore_destruct; unfold simatch, simatch_local; simpl; intuition.
         * exploit REG. try_simplify_someHyps.
         * destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto].
           subst; rewrite Regmap.gss; simpl.
-          erewrite list_sval_eval_inj; simpl; auto.
+          erewrite seval_list_sval_inj; simpl; auto.
           try_simplify_someHyps.
-      - unfold has_aborted, has_aborted_on_basic; simpl.
+      - unfold sabort, sabort_local; simpl.
         left. right. right.
         exists r. destruct (Pos.eq_dec r r); try congruence.
-        simpl. erewrite list_sval_eval_inj; simpl; auto.
+        simpl. erewrite seval_list_sval_inj; simpl; auto.
         try_simplify_someHyps. }
-    { unfold has_aborted, has_aborted_on_basic; simpl. 
+    { unfold sabort, sabort_local; simpl.
       left. right. right.
       exists r. destruct (Pos.eq_dec r r); try congruence.
-      simpl. erewrite list_sval_eval_inj; simpl; auto.
+      simpl. erewrite seval_list_sval_inj; simpl; auto.
       rewrite ADD; simpl; auto. } *)
    + (* STORE *)
     inversion_SOME a0; intros ADD.
     { inversion_SOME m'; intros STORE; simpl.
-      - unfold sem_istate, sem_local_istate; simpl; intuition.
+      - unfold simatch, simatch_local; simpl; intuition.
         * congruence.
-        * erewrite list_sval_eval_inj; simpl; auto.
+        * erewrite seval_list_sval_inj; simpl; auto.
           erewrite REG.
           try_simplify_someHyps.
-      - unfold has_aborted, has_aborted_on_basic; simpl.
+      - unfold sabort, sabort_local; simpl.
         left. right. left.
-        erewrite list_sval_eval_inj; simpl; auto.
+        erewrite seval_list_sval_inj; simpl; auto.
         erewrite REG.
         try_simplify_someHyps. }
-    { unfold has_aborted, has_aborted_on_basic; simpl.
+    { unfold sabort, sabort_local; simpl.
       left. right. left.
-      erewrite list_sval_eval_inj; simpl; auto.
+      erewrite seval_list_sval_inj; simpl; auto.
       erewrite ADD; simpl; auto. }
    + (* COND *)
     Local Hint Resolve is_tail_refl: core.
-    Local Hint Unfold sem_local_istate: core.
+    Local Hint Unfold simatch_local: core.
     inversion_SOME b; intros COND.
-    { destruct b; simpl; unfold sem_istate, sem_local_istate; simpl.
+    { destruct b; simpl; unfold simatch, simatch_local; simpl.
       - intros; econstructor; eauto; simpl.
         unfold seval_condition.
-        erewrite list_sval_eval_inj; simpl; auto.
+        erewrite seval_list_sval_inj; simpl; auto.
         try_simplify_someHyps.
-      - intuition. unfold has_not_yet_exit in * |- *. simpl.
+      - intuition. unfold all_fallthrough in * |- *. simpl.
         intuition. subst. simpl.
         unfold seval_condition.
-        erewrite list_sval_eval_inj; simpl; auto.
+        erewrite seval_list_sval_inj; simpl; auto.
         try_simplify_someHyps. }
-    { unfold has_aborted, has_aborted_on_test; simpl.
+    { unfold sabort, sabort_exits; simpl.
       right. eexists; intuition eauto. simpl.
         unfold seval_condition.
-        erewrite list_sval_eval_inj; simpl; auto.
+        erewrite seval_list_sval_inj; simpl; auto.
         try_simplify_someHyps. }
 Admitted.
 
-Lemma symb_istep_correct_None ge sp i st rs0 m0 rs m:
-  sem_local_istate ge sp (st.(curr)) rs0 m0 rs m ->
-  symb_istep i st = None -> 
+Lemma sistep_correct_None ge sp i st rs0 m0 rs m:
+  simatch_local ge sp (st.(si_local)) rs0 m0 rs m ->
+  sistep i st = None ->
   istep ge i sp rs m = None.
 Proof.
   intros (PRE & MEM & REG).
-  destruct i; simpl; unfold sist, sem_istate, sem_local_istate; simpl; try_simplify_someHyps.
+  destruct i; simpl; unfold sist_set_local, simatch, simatch_local; simpl; try_simplify_someHyps.
 Qed.
 
 (** * Symbolic execution of the internal steps of a path *)
-Fixpoint symb_isteps (path:nat) (f: function) (st: s_istate): option s_istate :=
+Fixpoint sisteps (path:nat) (f: function) (st: sistate): option sistate :=
   match path with
   | O => Some st
   | S p =>
-    SOME i <- (fn_code f)!(st.(the_pc)) IN
-    SOME st1 <- symb_istep i st IN
-    symb_isteps p f st1
+    SOME i <- (fn_code f)!(st.(si_pc)) IN
+    SOME st1 <- sistep i st IN
+    sisteps p f st1
   end.
 
-Lemma symb_isteps_correct_false ge sp path f rs0 m0 st' is: 
+Lemma sisteps_correct_false ge sp path f rs0 m0 st' is:
   is.(icontinue)=false ->
-  forall st, sem_istate ge sp st rs0 m0 is -> 
-  symb_isteps path f st = Some st' ->
-  sem_istate ge sp st' rs0 m0 is.
+  forall st, simatch ge sp st rs0 m0 is ->
+  sisteps path f st = Some st' ->
+  simatch ge sp st' rs0 m0 is.
 Proof.
-  Local Hint Resolve symb_istep_preserv_early_exits: core.
-  intros CONT; unfold sem_istate; rewrite CONT.
+  Local Hint Resolve sistep_preserves_simatch_exits: core.
+  intros CONT; unfold simatch; rewrite CONT.
   induction path; simpl.
-  + unfold sist; try_simplify_someHyps.
+  + unfold sist_set_local; try_simplify_someHyps.
   + intros st; inversion_SOME i.
     inversion_SOME st1; eauto.
 Qed.
 
-Lemma symb_isteps_preserv_has_aborted ge sp path f rs0 m0 st': forall st, 
-  symb_isteps path f st = Some st' ->
-  has_aborted ge sp st rs0 m0 -> has_aborted ge sp st' rs0 m0.
+Lemma sisteps_preserves_sabort ge sp path f rs0 m0 st': forall st,
+  sisteps path f st = Some st' ->
+  sabort ge sp st rs0 m0 -> sabort ge sp st' rs0 m0.
 Proof.
-  Local Hint Resolve symb_istep_preserv_has_aborted: core.
+  Local Hint Resolve sistep_preserves_sabort: core.
   induction path; simpl.
-  + unfold sist; try_simplify_someHyps.
+  + unfold sist_set_local; try_simplify_someHyps.
   + intros st; inversion_SOME i.
     inversion_SOME st1; eauto.
 Qed.
 
-Lemma symb_isteps_WF path f: forall st,
-  symb_isteps path f st = None -> nth_default_succ (fn_code f) path st.(the_pc) = None.
+Lemma sisteps_WF path f: forall st,
+  sisteps path f st = None -> nth_default_succ (fn_code f) path st.(si_pc) = None.
 Proof.
   induction path; simpl.
-  + unfold sist. intuition congruence.
-  + intros st; destruct ((fn_code f) ! (the_pc st)); simpl; try tauto.
-    destruct (symb_istep i st) as [st1|] eqn: Hst1; simpl.
-    - intros; erewrite symb_istep_default_succ; eauto.
-    - intros; erewrite symb_istep_WF; eauto.
+  + unfold sist_set_local. intuition congruence.
+  + intros st; destruct ((fn_code f) ! (si_pc st)); simpl; try tauto.
+    destruct (sistep i st) as [st1|] eqn: Hst1; simpl.
+    - intros; erewrite sistep_default_succ; eauto.
+    - intros; erewrite sistep_WF; eauto.
 Qed.
 
-Lemma symb_isteps_default_succ path f st': forall st,
-  symb_isteps path f st = Some st' -> nth_default_succ (fn_code f) path st.(the_pc) = Some st'.(the_pc).
+Lemma sisteps_default_succ path f st': forall st,
+  sisteps path f st = Some st' -> nth_default_succ (fn_code f) path st.(si_pc) = Some st'.(si_pc).
 Proof.
   induction path; simpl.
-  + unfold sist. intros st H. inversion_clear H; simpl; try congruence.
-  + intros st; destruct ((fn_code f) ! (the_pc st)); simpl; try congruence.
-    destruct (symb_istep i st) as [st1|] eqn: Hst1; simpl; try congruence.
-    intros; erewrite symb_istep_default_succ; eauto.
+  + unfold sist_set_local. intros st H. inversion_clear H; simpl; try congruence.
+  + intros st; destruct ((fn_code f) ! (si_pc st)); simpl; try congruence.
+    destruct (sistep i st) as [st1|] eqn: Hst1; simpl; try congruence.
+    intros; erewrite sistep_default_succ; eauto.
 Qed.
 
-Lemma symb_isteps_correct_true ge sp path (f:function) rs0 m0: forall st is,
+Lemma sisteps_correct_true ge sp path (f:function) rs0 m0: forall st is,
   is.(icontinue)=true ->
-  sem_istate ge sp st rs0 m0 is -> 
-  nth_default_succ (fn_code f) path st.(the_pc) <> None ->
-  sem_option2_istate ge sp (symb_isteps path f st) rs0 m0
-                         (isteps ge path f sp is.(the_rs) is.(the_mem) is.(RTLpath.the_pc))
+  simatch ge sp st rs0 m0 is ->
+  nth_default_succ (fn_code f) path st.(si_pc) <> None ->
+  simatch_opt2 ge sp (sisteps path f st) rs0 m0
+                         (isteps ge path f sp is.(irs) is.(imem) is.(ipc))
   .
 Proof.
-  Local Hint Resolve symb_isteps_correct_false symb_isteps_preserv_has_aborted symb_isteps_WF: core.
+  Local Hint Resolve sisteps_correct_false sisteps_preserves_sabort sisteps_WF: core.
   induction path; simpl.
   + intros st is CONT INV WF;
-    unfold sem_istate, sist in * |- *;
+    unfold simatch, sist_set_local in * |- *;
     try_simplify_someHyps. simpl.
     destruct is; simpl in * |- *; subst; intuition auto.
-  + intros st is CONT; unfold sem_istate at 1; rewrite CONT.
+  + intros st is CONT; unfold simatch at 1; rewrite CONT.
     intros (LOCAL & PC & NYE) WF.
     rewrite <- PC.
     inversion_SOME i; intro Hi; rewrite Hi in WF |- *; simpl; auto.
-    exploit symb_istep_correct; eauto. 
+    exploit sistep_correct; eauto.
     inversion_SOME st1; intros Hst1; erewrite Hst1; simpl.
     - inversion_SOME is1; intros His1;rewrite His1; simpl. 
       * destruct (icontinue is1) eqn:CONT1.
-        (* continue is0 = true *)
+        (* icontinue is0 = true *)
         intros; eapply IHpath; eauto.
-        destruct i; simpl in * |- *; unfold sist in * |- *; try_simplify_someHyps.
-        (* continue is0 = false -> EARLY EXIT *)
-        destruct (symb_isteps path f st1) as [st2|] eqn: Hst2; simpl; eauto.
-        destruct WF. erewrite symb_istep_default_succ; eauto.
+        destruct i; simpl in * |- *; unfold sist_set_local in * |- *; try_simplify_someHyps.
+        (* icontinue is0 = false -> EARLY EXIT *)
+        destruct (sisteps path f st1) as [st2|] eqn: Hst2; simpl; eauto.
+        destruct WF. erewrite sistep_default_succ; eauto.
         (* try_simplify_someHyps; eauto. *)
-      * destruct (symb_isteps path f st1) as [st2|] eqn: Hst2; simpl; eauto.
+      * destruct (sisteps path f st1) as [st2|] eqn: Hst2; simpl; eauto.
     - intros His1;rewrite His1; simpl; auto.
 Qed.
 
 (** REM: in the following two unused lemmas *)
 
-Lemma symb_isteps_right_assoc_decompose f path: forall st st',
-  symb_isteps (S path) f st = Some st' ->
-  exists st0, symb_isteps path f st = Some st0 /\ symb_isteps 1%nat f st0 = Some st'.
+Lemma sisteps_right_assoc_decompose f path: forall st st',
+  sisteps (S path) f st = Some st' ->
+  exists st0, sisteps path f st = Some st0 /\ sisteps 1%nat f st0 = Some st'.
 Proof.
   induction path; simpl; eauto.
   intros st st'.
@@ -637,10 +636,10 @@ Proof.
   try_simplify_someHyps; eauto.
 Qed.
 
-Lemma symb_isteps_right_assoc_compose f path: forall st st0 st',
-  symb_isteps path f st = Some st0 ->
-  symb_isteps 1%nat f st0 = Some st' ->
-  symb_isteps (S path) f st = Some st'.
+Lemma sisteps_right_assoc_compose f path: forall st st0 st',
+  sisteps path f st = Some st0 ->
+  sisteps 1%nat f st0 = Some st' ->
+  sisteps (S path) f st = Some st'.
 Proof.
   induction path.
   + intros st st0 st' H. simpl in H.
@@ -668,20 +667,20 @@ Inductive sfval :=
   | Sreturn: option sval -> sfval
 .
 
-Definition s_find_function (pge: RTLpath.genv) (ge: RTL.genv) (sp: val) (svos : sval + ident) (rs0: regset) (m0: mem): option fundef :=
+Definition sfind_function (pge: RTLpath.genv) (ge: RTL.genv) (sp: val) (svos : sval + ident) (rs0: regset) (m0: mem): option fundef :=
   match svos with
-  | inl sv => SOME v <- seval ge sp sv rs0 m0 IN Genv.find_funct pge v
+  | inl sv => SOME v <- seval_sval ge sp sv rs0 m0 IN Genv.find_funct pge v
   | inr symb => SOME b <- Genv.find_symbol pge symb IN Genv.find_funct_ptr pge b
   end.
 
-Inductive sfval_sem (pge: RTLpath.genv) (ge: RTL.genv) (sp:val) (st: s_istate) stack (f: function) (rs0: regset) (m0: mem): sfval -> regset -> mem -> trace -> state -> Prop :=
+Inductive sfmatch (pge: RTLpath.genv) (ge: RTL.genv) (sp:val) (st: sistate) stack (f: function) (rs0: regset) (m0: mem): sfval -> regset -> mem -> trace -> state -> Prop :=
   | exec_Snone rs m:
-      sfval_sem pge ge sp st stack f rs0 m0 Snone rs m E0 (State stack f sp st.(the_pc) rs m)
+      sfmatch pge ge sp st stack f rs0 m0 Snone rs m E0 (State stack f sp st.(si_pc) rs m)
   | exec_Scall rs m sig svos lsv args res pc fd:
-      s_find_function pge ge sp svos rs0 m0 = Some fd ->
+      sfind_function pge ge sp svos rs0 m0 = Some fd ->
       funsig fd = sig ->
-      list_sval_eval ge sp lsv rs0 m0 = Some args ->
-      sfval_sem pge ge sp st stack f rs0 m0 (Scall sig svos lsv res pc) rs m
+      seval_list_sval ge sp lsv rs0 m0 = Some args ->
+      sfmatch pge ge sp st stack f rs0 m0 (Scall sig svos lsv res pc) rs m
         E0 (Callstate (Stackframe res f sp pc rs :: stack) fd args m)
 (* TODO:
   | exec_Itailcall stk pc rs m sig ros args fd m':
@@ -707,52 +706,52 @@ Inductive sfval_sem (pge: RTLpath.genv) (ge: RTL.genv) (sp:val) (st: s_istate) s
   | exec_Sreturn stk osv rs m m' v:
       sp = (Vptr stk Ptrofs.zero) ->
       Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-      match osv with Some sv => seval ge sp sv rs0 m0 | None => Some Vundef end = Some v ->
-      sfval_sem pge ge sp st stack f rs0 m0 (Sreturn osv) rs m 
+      match osv with Some sv => seval_sval ge sp sv rs0 m0 | None => Some Vundef end = Some v ->
+      sfmatch pge ge sp st stack f rs0 m0 (Sreturn osv) rs m
          E0 (Returnstate stack v m')
 .
 
-Record s_state := { internal:> s_istate; final: sfval }.
+Record sstate := { internal:> sistate; final: sfval }.
 
-Inductive sem_state pge (ge: RTL.genv) (sp:val) (st: s_state) stack f (rs0: regset) (m0: mem): trace -> state -> Prop :=
-  | sem_early is:
+Inductive smatch pge (ge: RTL.genv) (sp:val) (st: sstate) stack f (rs0: regset) (m0: mem): trace -> state -> Prop :=
+  | smatch_early is:
      is.(icontinue) = false ->
-     sem_istate ge sp st rs0 m0 is -> 
-     sem_state pge ge sp st stack f rs0 m0 E0 (State stack f sp is.(RTLpath.the_pc) is.(the_rs) is.(the_mem))
-  | sem_normal is t s:
+     simatch ge sp st rs0 m0 is ->
+     smatch pge ge sp st stack f rs0 m0 E0 (State stack f sp is.(ipc) is.(irs) is.(imem))
+  | smatch_normal is t s:
      is.(icontinue) = true ->
-     sem_istate ge sp st rs0 m0 is ->  
-     sfval_sem pge ge sp st stack f rs0 m0 st.(final) is.(the_rs) is.(the_mem) t s ->
-     sem_state pge ge sp st stack f rs0 m0 t s 
+     simatch ge sp st rs0 m0 is ->
+     sfmatch pge ge sp st stack f rs0 m0 st.(final) is.(irs) is.(imem) t s ->
+     smatch pge ge sp st stack f rs0 m0 t s
   .
 
 (** * Symbolic execution of final step *)
-Definition symb_fstep (i: instruction) (prev: local_istate): sfval := 
+Definition sfstep (i: instruction) (prev: sistate_local): sfval :=
   match i with
   | Icall sig ros args res pc => 
-    let svos := sum_left_map prev.(the_sreg) ros in
-    let sargs := list_sval_inj (List.map prev.(the_sreg) args) in
+    let svos := sum_left_map prev.(si_sreg) ros in
+    let sargs := list_sval_inj (List.map prev.(si_sreg) args) in
     Scall sig svos sargs res pc
   | Ireturn or => 
-    let sor := SOME r <- or IN Some (prev.(the_sreg) r) in
+    let sor := SOME r <- or IN Some (prev.(si_sreg) r) in
     Sreturn sor
   | _ => Snone
   end.
 
-Lemma symb_fstep_correct pge ge sp i (f:function) pc st stack rs0 m0 t rs m s:
+Lemma sfstep_correct pge ge sp i (f:function) pc st stack rs0 m0 t rs m s:
   (fn_code f) ! pc = Some i ->
-  pc = st.(the_pc) ->
-  sem_local_istate ge sp (curr st) rs0 m0 rs m ->
+  pc = st.(si_pc) ->
+  simatch_local ge sp (si_local st) rs0 m0 rs m ->
   path_last_step ge pge stack f sp pc rs m t s ->
-  symb_istep i st = None -> 
-  sfval_sem pge ge sp st stack f rs0 m0 (symb_fstep i (curr st)) rs m t s.
+  sistep i st = None ->
+  sfmatch pge ge sp st stack f rs0 m0 (sfstep i (si_local st)) rs m t s.
 Proof.
   intros PC1 PC2 (PRE&MEM&REG) LAST Hi. destruct LAST; subst; try_simplify_someHyps; simpl.
-  + (* Snone *) destruct i; simpl in Hi |- *; unfold sist in Hi; try congruence.
+  + (* Snone *) destruct i; simpl in Hi |- *; unfold sist_set_local in Hi; try congruence.
   + (* Icall *) intros; eapply exec_Scall; auto.
     - destruct ros; simpl in * |- *; auto.
       rewrite REG; auto.
-    - erewrite list_sval_eval_inj; simpl; auto.
+    - erewrite seval_list_sval_inj; simpl; auto.
   + (* Itaillcall *) admit.
   + (* Ibuiltin *) admit.
   + (* Ijumptable *) admit.
@@ -760,19 +759,19 @@ Proof.
     destruct or; simpl; auto.
 Admitted.
 
-Lemma symb_fstep_complete i (f:function) pc st ge pge sp stack rs0 m0 t rs m s:
+Lemma sfstep_complete i (f:function) pc st ge pge sp stack rs0 m0 t rs m s:
   (fn_code f) ! pc = Some i ->
-  pc = st.(the_pc) ->
-  sem_local_istate ge sp (curr st) rs0 m0 rs m ->
-  sfval_sem pge ge sp st stack f rs0 m0 (symb_fstep i (curr st)) rs m t s ->
-  symb_istep i st = None -> 
+  pc = st.(si_pc) ->
+  simatch_local ge sp (si_local st) rs0 m0 rs m ->
+  sfmatch pge ge sp st stack f rs0 m0 (sfstep i (si_local st)) rs m t s ->
+  sistep i st = None -> 
   path_last_step ge pge stack f sp pc rs m t s.
 Proof.
   intros PC1 PC2 (PRE&MEM&REG) LAST Hi. 
   destruct i as [ | | | |(*Icall*)sig ros args res pc'| | | | |(*Ireturn*)or]; 
-  subst; try_simplify_someHyps; try (unfold sist in Hi; try congruence); inversion LAST; subst; clear LAST; simpl in * |- *.
+  subst; try_simplify_someHyps; try (unfold sist_set_local in Hi; try congruence); inversion LAST; subst; clear LAST; simpl in * |- *.
   + (* Icall *)
-    erewrite list_sval_eval_inj in * |- ; simpl; try_simplify_someHyps; auto.
+    erewrite seval_list_sval_inj in * |- ; simpl; try_simplify_someHyps; auto.
     intros; eapply exec_Icall; eauto.
     destruct ros; simpl in * |- *; auto.
     rewrite REG in * |- ; auto.
@@ -788,22 +787,22 @@ Admitted.
 
 (** * Main function of the symbolic execution *)
 
-Definition init_local_istate := {| pre:= fun _ _ _ _ => True; the_sreg:= fun r => Sinput r; the_smem:= Sinit |}.
+Definition init_sistate_local := {| si_pre:= fun _ _ _ _ => True; si_sreg:= fun r => Sinput r; si_smem:= Sinit |}.
 
-Definition init_istate pc := {| the_pc:= pc; exits:=nil; curr:= init_local_istate |}.
+Definition init_sistate pc := {| si_pc:= pc; si_exits:=nil; si_local:= init_sistate_local |}.
 
-Lemma init_sem_istate ge sp pc rs m: sem_istate ge sp (init_istate pc) rs m (ist true pc rs m).
+Lemma init_simatch ge sp pc rs m: simatch ge sp (init_sistate pc) rs m (mk_istate true pc rs m).
 Proof.
-  unfold sem_istate, sem_local_istate, has_not_yet_exit; simpl. intuition.
+  unfold simatch, simatch_local, all_fallthrough; simpl. intuition.
 Qed.
 
-Definition symb_step (f: function) (pc:node): option s_state :=
+Definition sstep (f: function) (pc:node): option sstate :=
   SOME path <- (fn_path f)!pc IN
-  SOME st <- symb_isteps path.(psize) f (init_istate pc) IN
-  SOME i <- (fn_code f)!(st.(the_pc)) IN
-  Some (match symb_istep i st with
+  SOME st <- sisteps path.(psize) f (init_sistate pc) IN
+  SOME i <- (fn_code f)!(st.(si_pc)) IN
+  Some (match sistep i st with
        | Some st' => {| internal := st'; final := Snone |}
-       | None => {| internal := st; final := symb_fstep i st.(curr) |}
+       | None => {| internal := st; final := sfstep i st.(si_local) |}
        end).
 
 Lemma final_node_path_simpl f path pc:
@@ -816,67 +815,70 @@ Qed.
 
 Lemma symb_path_last_step i st st' ge pge stack (f:function) sp pc rs m t s: 
   (fn_code f) ! pc = Some i ->
-  pc = st.(the_pc) ->
-  symb_istep i st = Some st' ->
+  pc = st.(si_pc) ->
+  sistep i st = Some st' ->
   path_last_step ge pge stack f sp pc rs m t s ->
-  exists ist, istep ge i sp rs m = Some ist /\ t = E0 /\ s = (State stack f sp ist.(RTLpath.the_pc) ist.(RTLpath.the_rs) ist.(the_mem)).
+  exists mk_istate,
+     istep ge i sp rs m = Some mk_istate
+  /\ t = E0
+  /\ s = (State stack f sp mk_istate.(ipc) mk_istate.(RTLpath.irs) mk_istate.(imem)).
 Proof.
   intros PC1 PC2 Hst' LAST; destruct LAST; subst; try_simplify_someHyps; simpl.
 Qed.
 
-(* NB: each concrete execution can be executed on the symbolic state (produced from [symb_step]) 
-(symb_step is a correct over-approximation)
+(* NB: each concrete execution can be executed on the symbolic state (produced from [sstep]) 
+(sstep is a correct over-approximation)
 *)
-Theorem symb_step_correct f pc pge ge sp path stack rs m t s: 
+Theorem sstep_correct f pc pge ge sp path stack rs m t s:
   (fn_path f)!pc = Some path ->
   path_step ge pge path.(psize) stack f sp rs m pc t s ->
-  exists st, symb_step f pc = Some st /\ sem_state pge ge sp st stack f rs m t s.
+  exists st, sstep f pc = Some st /\ smatch pge ge sp st stack f rs m t s.
 Proof.
-   Local Hint Resolve init_sem_istate symb_istep_preserv_early_exits: core.
-   intros PATH STEP; unfold symb_step; rewrite PATH; simpl.
+   Local Hint Resolve init_simatch sistep_preserves_simatch_exits: core.
+   intros PATH STEP; unfold sstep; rewrite PATH; simpl.
    lapply (final_node_path_simpl f path pc); eauto. intro WF.
-   exploit (symb_isteps_correct_true ge sp path.(psize) f rs m (init_istate pc) (ist true pc rs m)); simpl; eauto.
+   exploit (sisteps_correct_true ge sp path.(psize) f rs m (init_sistate pc) (mk_istate true pc rs m)); simpl; eauto.
    { intros ABS. apply WF; unfold nth_default_succ_inst. rewrite ABS; auto. }
    (destruct (nth_default_succ_inst (fn_code f) path.(psize) pc) as [i|] eqn: Hi; [clear WF|congruence]).
    destruct STEP as [sti STEPS CONT|sti t s STEPS CONT LAST];
    (* intro Hst *)
-   (rewrite STEPS; unfold sem_option2_istate; destruct (symb_isteps _ _ _) as [st|] eqn: Hst; try congruence);
+   (rewrite STEPS; unfold simatch_opt2; destruct (sisteps _ _ _) as [st|] eqn: Hst; try congruence);
    (* intro SEM *)
-   (simpl; unfold sem_istate; simpl; rewrite CONT; intro SEM);
+   (simpl; unfold simatch; simpl; rewrite CONT; intro SEM);
    (* intro Hi' *)
-   ( assert (Hi': (fn_code f) ! (the_pc st) = Some i); 
+   ( assert (Hi': (fn_code f) ! (si_pc st) = Some i);
      [ unfold nth_default_succ_inst in Hi; 
-       exploit symb_isteps_default_succ; eauto; simpl;
+       exploit sisteps_default_succ; eauto; simpl;
        intros DEF; rewrite DEF in Hi; auto 
        | clear Hi; rewrite Hi' ]);
    (* eexists *)
    (eexists; constructor; eauto).
    - (* early *)
-     eapply sem_early; eauto.
-     unfold sem_istate; simpl; rewrite CONT.
-     destruct (symb_istep i st) as [st'|] eqn: Hst'; simpl; eauto.
+     eapply smatch_early; eauto.
+     unfold simatch; simpl; rewrite CONT.
+     destruct (sistep i st) as [st'|] eqn: Hst'; simpl; eauto.
    - destruct SEM as (SEM & PC & HNYE).
-     destruct (symb_istep i st) as [st'|] eqn: Hst'; simpl.
+     destruct (sistep i st) as [st'|] eqn: Hst'; simpl.
      + (* normal on Snone *)
        rewrite <- PC in LAST.
        exploit symb_path_last_step; eauto; simpl.
-       intros (ist & ISTEP & Ht & Hs); subst.
-       exploit symb_istep_correct; eauto. simpl.
+       intros (mk_istate & ISTEP & Ht & Hs); subst.
+       exploit sistep_correct; eauto. simpl.
        erewrite Hst', ISTEP; simpl.
        clear LAST CONT STEPS PC SEM HNYE Hst Hi' Hst' ISTEP st sti i.
-       intro SEM; destruct (ist.(icontinue)) eqn: CONT.
-       { (* continue ist = true *)
-         eapply sem_normal; simpl; eauto.
-         unfold sem_istate in SEM.
+       intro SEM; destruct (mk_istate.(icontinue)) eqn: CONT.
+       { (* icontinue mk_istate = true *)
+         eapply smatch_normal; simpl; eauto.
+         unfold simatch in SEM.
          rewrite CONT in SEM.
          destruct SEM as (SEM & PC & HNYE).
          rewrite <- PC.
          eapply exec_Snone. }
-       { eapply sem_early; eauto. }
+       { eapply smatch_early; eauto. }
      + (* normal non-Snone instruction *) 
-       eapply sem_normal; eauto.
-       * unfold sem_istate; simpl; rewrite CONT; intuition.
-       * simpl. eapply symb_fstep_correct; eauto.
+       eapply smatch_normal; eauto.
+       * unfold simatch; simpl; rewrite CONT; intuition.
+       * simpl. eapply sfstep_correct; eauto.
          rewrite PC; auto.
 Qed.
 
@@ -939,10 +941,10 @@ Proof.
 Qed.
 *)
 
-Lemma sfval_sem_equiv pge ge sp (f:function) st sv stack rs0 m0 t rs1 rs2 m s:
-  sfval_sem pge ge sp st stack f rs0 m0 sv rs1 m t s ->
+Lemma sfmatch_equiv pge ge sp (f:function) st sv stack rs0 m0 t rs1 rs2 m s:
+  sfmatch pge ge sp st stack f rs0 m0 sv rs1 m t s ->
   (forall r, rs1#r = rs2#r) -> 
-  exists s', equiv_state s s' /\ sfval_sem pge ge sp st stack f rs0 m0 sv rs2 m t s'.
+  exists s', equiv_state s s' /\ sfmatch pge ge sp st stack f rs0 m0 sv rs2 m t s'.
 Proof. 
   Local Hint Resolve equiv_stack_refl: core.
   destruct 1.
@@ -958,57 +960,57 @@ Proof.
     + eapply exec_Sreturn; eauto.
 Qed.
 
-(* NB: each execution of a symbolic state (produced from [symb_step]) represents a concrete execution
-  (symb_step is exact).
+(* NB: each execution of a symbolic state (produced from [sstep]) represents a concrete execution
+  (sstep is exact).
 *)
-Theorem symb_step_exact f pc pge ge sp path stack st rs m t s1: 
+Theorem sstep_exact f pc pge ge sp path stack st rs m t s1:
   (fn_path f)!pc = Some path ->
-  symb_step f pc = Some st -> 
-  sem_state pge ge sp st stack f rs m t s1 ->
+  sstep f pc = Some st ->
+  smatch pge ge sp st stack f rs m t s1 ->
   exists s2, path_step ge pge path.(psize) stack f sp rs m pc t s2 /\ 
              equiv_state s1 s2.
 Proof.
-  Local Hint Resolve init_sem_istate: core.
-  unfold symb_step; intros PATH SSTEP SEM; rewrite PATH in SSTEP.
+  Local Hint Resolve init_simatch: core.
+  unfold sstep; intros PATH SSTEP SEM; rewrite PATH in SSTEP.
   lapply (final_node_path_simpl f path pc); eauto. intro WF.
-  exploit (symb_isteps_correct_true ge sp path.(psize) f rs m (init_istate pc) (ist true pc rs m)); simpl; eauto.
+  exploit (sisteps_correct_true ge sp path.(psize) f rs m (init_sistate pc) (mk_istate true pc rs m)); simpl; eauto.
   { intros ABS. apply WF; unfold nth_default_succ_inst. rewrite ABS; auto. }
   (destruct (nth_default_succ_inst (fn_code f) path.(psize) pc) as [i|] eqn: Hi; [clear WF|congruence]).
   unfold nth_default_succ_inst in Hi.
-  destruct (symb_isteps path.(psize) f (init_istate pc)) as [st0|] eqn: Hst0; simpl.
+  destruct (sisteps path.(psize) f (init_sistate pc)) as [st0|] eqn: Hst0; simpl.
   2:{ (* absurd case *)
-      exploit symb_isteps_WF; eauto.
+      exploit sisteps_WF; eauto.
       simpl; intros NDS; rewrite NDS in Hi; congruence. }
-  exploit symb_isteps_default_succ; eauto; simpl.
+  exploit sisteps_default_succ; eauto; simpl.
   intros NDS; rewrite NDS in Hi.
   rewrite Hi in SSTEP.
   intros ISTEPS. try_simplify_someHyps.
-  destruct (symb_istep i st0) as [st'|] eqn: Hst'; simpl.
+  destruct (sistep i st0) as [st'|] eqn: Hst'; simpl.
   + (* normal exit on Snone instruction *)
     admit.
   + destruct SEM as [is CONT SEM|is t s CONT SEM1 SEM2]; simpl in * |- *.
     - (* early exit *)
       intros.
-      exploit sem_option_istate_determ; eauto.
+      exploit simatch_opt_determ; eauto.
       destruct 1 as (st & Hst & EQ1 & EQ2 & EQ3 & EQ4).
       eexists. econstructor 1.
       * eapply exec_early_exit; eauto.
       * rewrite EQ2, EQ4; eapply State_equiv. auto.
     - (* normal exit non-Snone instruction *)
       intros.
-      exploit sem_option_istate_determ; eauto.
+      exploit simatch_opt_determ; eauto.
       destruct 1 as (st & Hst & EQ1 & EQ2 & EQ3 & EQ4).
-      unfold sem_istate in SEM1.
+      unfold simatch in SEM1.
       rewrite CONT in SEM1. destruct SEM1 as (SEM1 & PC0 & NYE0).
-      exploit sfval_sem_equiv; eauto.
+      exploit sfmatch_equiv; eauto.
       clear SEM2; destruct 1 as (s' & Ms' & SEM2).
       rewrite ! EQ4 in * |-; clear EQ4.
       rewrite ! EQ2 in * |-; clear EQ2.
       exists s'; intuition.
       eapply exec_normal_exit; eauto.
-      eapply symb_fstep_complete; eauto.
+      eapply sfstep_complete; eauto.
       * congruence.
-      * unfold sem_local_istate in * |- *. intuition try congruence.
+      * unfold simatch_local in * |- *. intuition try congruence.
 Admitted.
 
 (** * Simulation of RTLpath code w.r.t symbolic execution *)
@@ -1020,43 +1022,43 @@ Variable ge ge': RTL.genv.
 Hypothesis symbols_preserved_RTL: forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s.
 
 Lemma seval_preserved sp sv rs0 m0:
-  seval ge sp sv rs0 m0 = seval ge' sp sv rs0 m0.
+  seval_sval ge sp sv rs0 m0 = seval_sval ge' sp sv rs0 m0.
 Proof.
   Local Hint Resolve symbols_preserved_RTL: core.
-  induction sv using sval_mut with (P0 := fun lsv => list_sval_eval ge sp lsv rs0 m0 = list_sval_eval ge' sp lsv rs0 m0)
-                                   (P1 := fun sm => smem_eval ge sp sm rs0 m0 = smem_eval ge' sp sm rs0 m0); simpl; auto.
-  + rewrite IHsv; clear IHsv. destruct (list_sval_eval _ _ _ _); auto.
-    rewrite IHsv0; clear IHsv0. destruct (smem_eval _ _ _ _); auto.
+  induction sv using sval_mut with (P0 := fun lsv => seval_list_sval ge sp lsv rs0 m0 = seval_list_sval ge' sp lsv rs0 m0)
+                                   (P1 := fun sm => seval_smem ge sp sm rs0 m0 = seval_smem ge' sp sm rs0 m0); simpl; auto.
+  + rewrite IHsv; clear IHsv. destruct (seval_list_sval _ _ _ _); auto.
+    rewrite IHsv0; clear IHsv0. destruct (seval_smem _ _ _ _); auto.
     erewrite eval_operation_preserved; eauto.
-  + rewrite IHsv0; clear IHsv0. destruct (list_sval_eval _ _ _ _); auto.
+  + rewrite IHsv0; clear IHsv0. destruct (seval_list_sval _ _ _ _); auto.
     erewrite <- eval_addressing_preserved; eauto.
     destruct (eval_addressing _ sp _ _); auto.
     rewrite IHsv; auto.
-  + rewrite IHsv; clear IHsv. destruct (seval _ _ _ _); auto.
+  + rewrite IHsv; clear IHsv. destruct (seval_sval _ _ _ _); auto.
     rewrite IHsv0; auto.
-  + rewrite IHsv0; clear IHsv0. destruct (list_sval_eval _ _ _ _); auto.
+  + rewrite IHsv0; clear IHsv0. destruct (seval_list_sval _ _ _ _); auto.
     erewrite <- eval_addressing_preserved; eauto.
     destruct (eval_addressing _ sp _ _); auto.
-    rewrite IHsv; clear IHsv. destruct (smem_eval _ _ _ _); auto.
+    rewrite IHsv; clear IHsv. destruct (seval_smem _ _ _ _); auto.
     rewrite IHsv1; auto.
 Qed.
 
 Lemma list_sval_eval_preserved sp lsv rs0 m0: 
-  list_sval_eval ge sp lsv rs0 m0 = list_sval_eval ge' sp lsv rs0 m0.
+  seval_list_sval ge sp lsv rs0 m0 = seval_list_sval ge' sp lsv rs0 m0.
 Proof.
   induction lsv; simpl; auto.
-  rewrite seval_preserved. destruct (seval _ _ _ _); auto.
+  rewrite seval_preserved. destruct (seval_sval _ _ _ _); auto.
   rewrite IHlsv; auto.
 Qed.
 
 Lemma smem_eval_preserved sp sm rs0 m0: 
-  smem_eval ge sp sm rs0 m0 = smem_eval ge' sp sm rs0 m0.
+  seval_smem ge sp sm rs0 m0 = seval_smem ge' sp sm rs0 m0.
 Proof.
   induction sm; simpl; auto.
-  rewrite list_sval_eval_preserved. destruct (list_sval_eval _ _ _ _); auto.
+  rewrite list_sval_eval_preserved. destruct (seval_list_sval _ _ _ _); auto.
   erewrite <- eval_addressing_preserved; eauto.
   destruct (eval_addressing _ sp _ _); auto.
-  rewrite IHsm; clear IHsm. destruct (smem_eval _ _ _ _); auto.
+  rewrite IHsm; clear IHsm. destruct (seval_smem _ _ _ _); auto.
   rewrite seval_preserved; auto.
 Qed.
 
@@ -1064,7 +1066,7 @@ Lemma seval_condition_preserved sp cond lsv sm rs0 m0:
  seval_condition ge sp cond lsv sm rs0 m0 = seval_condition ge' sp cond lsv sm rs0 m0.
 Proof.
   unfold seval_condition.
-  rewrite list_sval_eval_preserved. destruct (list_sval_eval _ _ _ _); auto.
+  rewrite list_sval_eval_preserved. destruct (seval_list_sval _ _ _ _); auto.
   rewrite smem_eval_preserved; auto.
 Qed.
 
@@ -1074,8 +1076,8 @@ Require Import RTLpathLivegen RTLpathLiveproofs.
 
 Definition istate_simulive alive (srce: PTree.t node) (is1 is2: istate): Prop :=
      is1.(icontinue) = is2.(icontinue)
-     /\ eqlive_reg alive is1.(the_rs) is2.(the_rs)
-     /\ is1.(the_mem) = is2.(the_mem).
+     /\ eqlive_reg alive is1.(irs) is2.(irs)
+     /\ is1.(imem) = is2.(imem).
 
 Definition istate_simu f (srce: PTree.t node) is1 is2: Prop :=
   if is1.(icontinue) then
@@ -1085,17 +1087,17 @@ Definition istate_simu f (srce: PTree.t node) is1 is2: Prop :=
         sur la dernière instruction du superblock. *)
      istate_simulive (fun _ => True) srce is1 is2
   else
-     exists path, f.(fn_path)!(is1.(RTLpath.the_pc)) = Some path 
+     exists path, f.(fn_path)!(is1.(ipc)) = Some path
      /\ istate_simulive (fun r => Regset.In r path.(input_regs)) srce is1 is2
-     /\ srce!(is2.(RTLpath.the_pc)) = Some is1.(RTLpath.the_pc).
+     /\ srce!(is2.(ipc)) = Some is1.(ipc).
 
-(* NOTE: a pure semantic definition on [s_istate], for a total freedom in refinements *)
-Definition s_istate_simu (f: RTLpath.function) (srce: PTree.t node) (st1 st2: s_istate): Prop :=
+(* NOTE: a pure semantic definition on [sistate], for a total freedom in refinements *)
+Definition sistate_simu (f: RTLpath.function) (srce: PTree.t node) (st1 st2: sistate): Prop :=
   forall sp ge1 ge2, 
   (forall s, Genv.find_symbol ge2 s = Genv.find_symbol ge1 s) ->
   liveness_ok_function f ->
-  forall rs m is1, sem_istate ge1 sp st1 rs m is1 -> 
-     exists is2, sem_istate ge2 sp st2 rs m is2 /\ istate_simu f srce is1 is2.
+  forall rs m is1, simatch ge1 sp st1 rs m is1 ->
+     exists is2, simatch ge2 sp st2 rs m is2 /\ istate_simu f srce is1 is2.
 
 (* NOTE: a syntactic definition on [sfval] in order to abstract the [match_states] *)
 Inductive sfval_simu (f: RTLpath.function) (srce: PTree.t node) (opc1 opc2: node): sfval -> sfval -> Prop :=
@@ -1108,14 +1110,14 @@ Inductive sfval_simu (f: RTLpath.function) (srce: PTree.t node) (opc1 opc2: node
   | Sreturn_simu os:
      sfval_simu f srce opc1 opc2 (Sreturn os) (Sreturn os).
 
-Definition s_state_simu f srce (s1 s2: s_state): Prop :=
-       s_istate_simu f srce s1.(internal) s2.(internal)
-    /\ sfval_simu f srce s1.(the_pc) s2.(the_pc) s1.(final) s2.(final).
+Definition sstate_simu f srce (s1 s2: sstate): Prop :=
+       sistate_simu f srce s1.(internal) s2.(internal)
+    /\ sfval_simu f srce s1.(si_pc) s2.(si_pc) s1.(final) s2.(final).
 
-Definition symb_step_simu srce (f1 f2: RTLpath.function) pc1 pc2: Prop :=
-    forall st1, symb_step f1 pc1 = Some st1 -> 
-    exists st2, symb_step f2 pc2 = Some st2 /\ s_state_simu f1 srce st1 st2.
+Definition sstep_simu srce (f1 f2: RTLpath.function) pc1 pc2: Prop :=
+    forall st1, sstep f1 pc1 = Some st1 ->
+    exists st2, sstep f2 pc2 = Some st2 /\ sstate_simu f1 srce st1 st2.
 
-(* IDEA: we will provide an efficient test for checking "symb_step_simu" property, by hash-consing.
-   See usage of [symb_step_simu] in [RTLpathScheduler].
-*)
\ No newline at end of file
+(* IDEA: we will provide an efficient test for checking "sstep_simu" property, by hash-consing.
+   See usage of [sstep_simu] in [RTLpathScheduler].
+*)
diff --git a/mppa_k1c/lib/RTLpathScheduler.v b/mppa_k1c/lib/RTLpathScheduler.v
index fb2be412..4478ee72 100644
--- a/mppa_k1c/lib/RTLpathScheduler.v
+++ b/mppa_k1c/lib/RTLpathScheduler.v
@@ -33,7 +33,7 @@ Record match_function (dupmap: PTree.t node) (f1 f2: RTLpath.function): Prop :=
   preserv_entrypoint: dupmap!(f2.(fn_entrypoint)) = Some f1.(fn_entrypoint);
   dupmap_path_entry1: forall pc1 pc2, dupmap!pc2 = Some pc1 -> path_entry (fn_path f1) pc1;
   dupmap_path_entry2: forall pc1 pc2, dupmap!pc2 = Some pc1 -> path_entry (fn_path f2) pc2;
-  dupmap_correct: forall pc1 pc2, dupmap!pc2 = Some pc1 -> symb_step_simu dupmap f1 f2 pc1 pc2
+  dupmap_correct: forall pc1 pc2, dupmap!pc2 = Some pc1 -> sstep_simu dupmap f1 f2 pc1 pc2
 }.
 
 (* TODO: remove these two stub parameters *)
@@ -110,13 +110,13 @@ Lemma match_stack_equiv stk1 stk2:
   forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> 
   list_forall2 match_stackframes stk1 stk3.
 Proof.
-  Local Hint Resolve match_stackframes_equiv.
+  Local Hint Resolve match_stackframes_equiv: core.
   induction 1; intros stk3 EQ; inv EQ; econstructor; eauto.
 Qed.
 
 Lemma match_states_equiv s1 s2 s3: match_states s1 s2 -> equiv_state s2 s3 -> match_states s1 s3.
 Proof.
-  Local Hint Resolve match_stack_equiv.
+  Local Hint Resolve match_stack_equiv: core.
   destruct 1; intros EQ; inv EQ; econstructor; eauto.
   intros; eapply eqlive_reg_triv_trans; eauto.
 Qed.
@@ -139,7 +139,7 @@ Qed.
 
 Lemma eqlive_match_states s1 s2 s3: eqlive_states s1 s2 -> match_states s2 s3 -> match_states s1 s3.
 Proof.
-  Local Hint Resolve eqlive_match_stack.
+  Local Hint Resolve eqlive_match_stack: core.
   destruct 1; intros MS; inv MS; try_simplify_someHyps; econstructor; eauto.
   eapply eqlive_reg_trans; eauto.
 Qed.
@@ -293,15 +293,15 @@ Proof.
 Qed.
 
 Lemma s_find_function_preserved sp svos rs0 m0 fd:
-  s_find_function pge ge sp svos rs0 m0 = Some fd ->
-  exists fd', s_find_function tpge tge sp svos rs0 m0 = Some fd' 
+  sfind_function pge ge sp svos rs0 m0 = Some fd ->
+  exists fd', sfind_function tpge tge sp svos rs0 m0 = Some fd'
               /\ transf_fundef fd = OK fd'
               /\ liveness_ok_fundef fd.
 Proof.
-  Local Hint Resolve symbols_preserved_RTL.
-  unfold s_find_function. destruct svos; simpl.
-  + rewrite (sval_eval_preserved ge tge); auto.
-    destruct (sval_eval _ _ _ _); try congruence.
+  Local Hint Resolve symbols_preserved_RTL: core.
+  unfold sfind_function. destruct svos; simpl.
+  + rewrite (seval_preserved ge tge); auto.
+    destruct (seval_sval _ _ _ _); try congruence.
     intros; exploit functions_preserved; eauto.
     intros (fd' & cunit & X). eexists. intuition eauto.
     eapply find_funct_liveness_ok; eauto.
@@ -310,27 +310,27 @@ Proof.
     intros (fd' & X). eexists. intuition eauto.
 Qed.
 
-Lemma sem_istate_simu f dupmap sp st st' rs m is:
-  sem_istate ge sp st rs m is ->
+Lemma sistate_simu f dupmap sp st st' rs m is:
+  simatch ge sp st rs m is ->
   liveness_ok_function f ->
-  s_istate_simu f dupmap st st' ->
+  sistate_simu f dupmap st st' ->
   exists is',
-    sem_istate tge sp st' rs m is' /\ istate_simu f dupmap is is'.
+    simatch tge sp st' rs m is' /\ istate_simu f dupmap is is'.
 Proof.
   intros SEM LIVE X; eapply X; eauto.
 Qed.
 
 
-Lemma sem_sfval_simu dupmap f f' stk stk' sp st st' rs0 m0 sv sv' rs m t s:
+Lemma sfmatch_simu dupmap f f' stk stk' sp st st' rs0 m0 sv sv' rs m t s:
   match_function dupmap f f' ->
   liveness_ok_function f ->
   list_forall2 match_stackframes stk stk' ->
   (* s_istate_simu f dupmap st st' -> *)
-  sfval_simu f dupmap st.(the_pc) st'.(the_pc) sv sv' ->
-  sfval_sem pge ge sp st stk f rs0 m0 sv rs m t s ->
-  exists s', sfval_sem tpge tge sp st' stk' f' rs0 m0 sv' rs m t s' /\ match_states s s'.
+  sfval_simu f dupmap st.(si_pc) st'.(si_pc) sv sv' ->
+  sfmatch pge ge sp st stk f rs0 m0 sv rs m t s ->
+  exists s', sfmatch tpge tge sp st' stk' f' rs0 m0 sv' rs m t s' /\ match_states s s'.
 Proof.
-  Local Hint Resolve transf_fundef_correct.
+  Local Hint Resolve transf_fundef_correct: core.
   intros FUN LIVE STK (* SIS *) SFV. destruct SFV; intros SEM; inv SEM; simpl.
   - (* Snone *)
     exploit initialize_path. { eapply dupmap_path_entry1; eauto. }
@@ -350,38 +350,38 @@ Proof.
     eexists; split; econstructor; eauto.
     + erewrite <- preserv_fnstacksize; eauto.
     + destruct os; auto.
-      erewrite <- sval_eval_preserved; eauto.
+      erewrite <- seval_preserved; eauto.
 Qed.
 
 (* The main theorem on simulation of symbolic states ! *)
-Theorem sem_symb_state_simu dupmap f f' stk stk' sp st st' rs m t s:
+Theorem smatch_sstate_simu dupmap f f' stk stk' sp st st' rs m t s:
   match_function dupmap f f' ->
   liveness_ok_function f ->
   list_forall2 match_stackframes stk stk' ->
-  sem_state pge ge sp st stk f rs m t s ->
-  s_state_simu f dupmap st st' ->
-  exists s', sem_state tpge tge sp st' stk' f' rs m t s' /\ match_states s s'.
+  smatch pge ge sp st stk f rs m t s ->
+  sstate_simu f dupmap st st' ->
+  exists s', smatch tpge tge sp st' stk' f' rs m t s' /\ match_states s s'.
 Proof.
   intros MFUNC LIVE STACKS SEM (SIMU1 & SIMU2). destruct SEM as [is CONT SEM|is t s' CONT SEM1 SEM2]; simpl.
   - (* sem_early *)
-    exploit sem_istate_simu; eauto.
+    exploit sistate_simu; eauto.
     unfold istate_simu; rewrite CONT.
     intros (is' & SEM' & (path & PATH & (CONT' & RS' & M') & PC')).
-    exists (State stk' f' sp (RTLpath.the_pc is') (the_rs is') (the_mem is')).
+    exists (State stk' f' sp (ipc is') (irs is') (imem is')).
     split.
-    + eapply sem_early; auto. congruence.
+    + eapply smatch_early; auto. congruence.
     + rewrite M'. econstructor; eauto.
   - (* sem_normal *)
-    exploit sem_istate_simu; eauto.
+    exploit sistate_simu; eauto.
     unfold istate_simu; rewrite CONT.
     intros (is' & SEM' & (CONT' & RS' & M')).
     rewrite <- eqlive_reg_triv in RS'.
-    exploit sem_sfval_simu; eauto.
+    exploit sfmatch_simu; eauto.
     clear SEM2; intros (s0 & SEM2 & MATCH0).
-    exploit sfval_sem_equiv; eauto.
+    exploit sfmatch_equiv; eauto.
     clear SEM2; rewrite M'; rewrite CONT' in CONT; intros (s1 & EQ & SEM2).
     exists s1; split.
-    + eapply sem_normal; eauto.
+    + eapply smatch_normal; eauto.
     + eapply match_states_equiv; eauto.
 Qed.
 
@@ -398,13 +398,13 @@ Proof.
   exploit initialize_path. { eapply dupmap_path_entry2; eauto. }
   intros (path' & PATH').
   exists path'.
-  exploit (symb_step_correct f pc pge ge sp path stk rs m t s); eauto.
+  exploit (sstep_correct f pc pge ge sp path stk rs m t s); eauto.
   intros (st & SYMB & SEM); clear STEP.
   exploit dupmap_correct; eauto.
   clear SYMB; intros (st' & SYMB & SIMU).
-  exploit sem_symb_state_simu; eauto.
+  exploit smatch_sstate_simu; eauto.
   intros (s0 & SEM0 & MATCH). 
-  exploit symb_step_exact; eauto.
+  exploit sstep_exact; eauto.
   intros (s' & STEP' & EQ).
   exists s'; intuition.
   eapply match_states_equiv; eauto.
@@ -417,7 +417,7 @@ Lemma step_simulation s1 t s1' s2:
      step tge tpge s2 t s2'
   /\ match_states s1' s2'.
 Proof.
-  Local Hint Resolve eqlive_stacks_refl transf_fundef_correct.
+  Local Hint Resolve eqlive_stacks_refl transf_fundef_correct: core.
   destruct 1 as [path stack f sp rs m pc t s PATH STEP | | | ]; intros MS; inv MS.
 (* exec_path *)
   - try_simplify_someHyps. intros.