Started general renaming for clearer and more understandable code

3 files changed, 243 insertions, 250 deletions

diff --git a/mppa_k1c/lib/RTLpath.v b/mppa_k1c/lib/RTLpath.v
index 35f6e715..7134de10 100644
--- a/mppa_k1c/lib/RTLpath.v
+++ b/mppa_k1c/lib/RTLpath.v
@@ -141,36 +141,36 @@ Coercion program_RTL: program >-> RTL.program.
 
 (* Semantics of internal instructions (mimicking RTL semantics) *)
 
-Record istate := ist { continue: bool; the_pc: node; the_rs: regset; the_mem: mem }.
+Record istate := mk_istate { icontinue: bool; ipc: node; irs: regset; imem: mem }.
 
 (* FIXME - prediction *)
 (* Internal step through the path *)
 Definition istep (ge: RTL.genv) (i: instruction) (sp: val) (rs: regset) (m: mem): option istate :=
   match i with
-  | Inop pc' => Some (ist true pc' rs m)
+  | Inop pc' => Some (mk_istate true pc' rs m)
   | Iop op args res pc' =>
       SOME v <- eval_operation ge sp op rs##args m IN
-      Some (ist true pc' (rs#res <- v) m)
+      Some (mk_istate true pc' (rs#res <- v) m)
   | Iload TRAP chunk addr args dst pc' =>
       SOME a <- eval_addressing ge sp addr rs##args IN
       SOME v <- Mem.loadv chunk m a IN
-      Some (ist true pc' (rs#dst <- v) m)
+      Some (mk_istate true pc' (rs#dst <- v) m)
   | Iload NOTRAP chunk addr args dst pc' =>
-      let default_state := ist true pc' rs#dst <- (default_notrap_load_value chunk) m in
+      let default_state := mk_istate true pc' rs#dst <- (default_notrap_load_value chunk) m in
       match (eval_addressing ge sp addr rs##args) with
       | None => Some default_state
       | Some a => match (Mem.loadv chunk m a) with
           | None => Some default_state
-          | Some v => Some (ist true pc' (rs#dst <- v) m)
+          | Some v => Some (mk_istate true pc' (rs#dst <- v) m)
           end
       end
   | Istore chunk addr args src pc' =>
       SOME a <- eval_addressing ge sp addr rs##args IN
       SOME m' <- Mem.storev chunk m a rs#src IN
-      Some (ist true pc' rs m')
+      Some (mk_istate true pc' rs m')
   | Icond cond args ifso ifnot _ =>
       SOME b <- eval_condition cond rs##args m IN
-      Some (ist (negb b) (if b then ifso else ifnot) rs m)
+      Some (mk_istate (negb b) (if b then ifso else ifnot) rs m)
   | _ => None (* TODO jumptable ? *)
   end.
 
@@ -179,12 +179,12 @@ Definition istep (ge: RTL.genv) (i: instruction) (sp: val) (rs: regset) (m: mem)
 (* Executes until a state [st] is reached where st.(continue) is false *)
 Fixpoint isteps ge (path:nat) (f: function) sp rs m pc: option istate :=
   match path with
-  | O => Some (ist true pc rs m)
+  | O => Some (mk_istate true pc rs m)
   | S p =>
     SOME i <- (fn_code f)!pc IN
     SOME st <- istep ge i sp rs m IN
-    if st.(continue) then
-      isteps ge p f sp st.(the_rs) st.(the_mem) st.(the_pc)
+    if (icontinue st) then
+      isteps ge p f sp (irs st) (imem st) (ipc st)
     else
       Some st
   end.
@@ -252,7 +252,7 @@ Inductive path_last_step ge pge stack (f: function): val -> node -> regset -> me
      (fn_code f)!pc = Some i ->
      istep ge i sp rs m = Some st ->
      path_last_step ge pge stack f sp pc rs m
-                    E0 (State stack f sp st.(the_pc) st.(the_rs) st.(the_mem))
+                    E0 (State stack f sp (ipc st) (irs st) (imem st))
   | exec_Icall sp pc rs m sig ros args res pc' fd:
       (fn_code f)!pc = Some(Icall sig ros args res pc') ->
       find_function pge ros rs = Some fd ->
@@ -288,12 +288,12 @@ Inductive path_last_step ge pge stack (f: function): val -> node -> regset -> me
 Inductive path_step ge pge (path:nat) stack f sp rs m pc: trace -> state -> Prop :=
   | exec_early_exit st:
      isteps ge path f sp rs m pc = Some st ->
-     st.(continue) = false ->
-     path_step ge pge path stack f sp rs m pc E0 (State stack f sp st.(the_pc) st.(the_rs) st.(the_mem))
+     (icontinue st) = false ->
+     path_step ge pge path stack f sp rs m pc E0 (State stack f sp (ipc st) (irs st) (imem st))
   | exec_normal_exit st t s:
      isteps ge path f sp rs m pc = Some st ->
-     st.(continue) = true ->
-     path_last_step ge pge stack f sp st.(the_pc) st.(the_rs) st.(the_mem) t s ->
+     (icontinue st) = true ->
+     path_last_step ge pge stack f sp (ipc st) (irs st) (imem st) t s ->
      path_step ge pge path stack f sp rs m pc t s.
 
 (* Either internal path execution, or the usual exec_function / exec_return borrowed from RTL *)
@@ -396,7 +396,7 @@ Local Hint Resolve RTL.exec_Inop RTL.exec_Iop RTL.exec_Iload RTL.exec_Istore RTL
 Lemma istep_correct ge i stack (f:function) sp rs m st :
   istep ge i sp rs m = Some st ->
   forall pc, (fn_code f)!pc = Some i ->
-  RTL.step ge (State stack f sp pc rs m) E0 (State stack f sp st.(the_pc) st.(the_rs) st.(the_mem)).
+  RTL.step ge (State stack f sp pc rs m) E0 (State stack f sp st.(ipc) st.(irs) st.(imem)).
 Proof.
   destruct i; simpl; try congruence; simplify_SOME x.
   1-3: explore_destruct; simplify_SOME x.
@@ -407,12 +407,12 @@ Local Hint Resolve star_refl: core.
 (* isteps reflects a star relation on RTL.step *)
 Lemma isteps_correct ge path stack f sp: forall rs m pc st,
   isteps ge path f sp rs m pc = Some st ->
-  star RTL.step ge (State stack f sp pc rs m) E0 (State stack f sp st.(the_pc) st.(the_rs) st.(the_mem)).
+  star RTL.step ge (State stack f sp pc rs m) E0 (State stack f sp st.(ipc) st.(irs) st.(imem)).
 Proof.
   induction path; simpl; try_simplify_someHyps.
   inversion_SOME i; intros Hi.
   inversion_SOME st0; intros Hst0.
-  destruct (continue st0) eqn:cont.
+  destruct (icontinue st0) eqn:cont.
   + intros; eapply star_step.
     - eapply istep_correct; eauto.
     - simpl; eauto.
@@ -425,13 +425,13 @@ Qed.
 
 Lemma isteps_correct_early_exit ge path stack f sp: forall rs m pc st,
   isteps ge path f sp rs m pc = Some st ->
-  st.(continue) = false ->
-  plus RTL.step ge (State stack f sp pc rs m) E0 (State stack f sp st.(the_pc) st.(the_rs) st.(the_mem)).
+  st.(icontinue) = false ->
+  plus RTL.step ge (State stack f sp pc rs m) E0 (State stack f sp st.(ipc) st.(irs) st.(imem)).
 Proof.
   destruct path; simpl; try_simplify_someHyps; try congruence.
   inversion_SOME i; intros Hi.
   inversion_SOME st0; intros Hst0.
-  destruct (continue st0) eqn:cont.
+  destruct (icontinue st0) eqn:cont.
   + intros; eapply plus_left.
     - eapply istep_correct; eauto.
     - eapply isteps_correct; eauto.
@@ -609,7 +609,7 @@ Local Opaque path_entry.
 
 Lemma istep_successors ge i sp rs m st:
   istep ge i sp rs m = Some st -> 
-  In (the_pc st) (successors_instr i).
+  In (ipc st) (successors_instr i).
 Proof.
   destruct i; simpl; try congruence; simplify_SOME x.
   all: explore_destruct; simplify_SOME x.
@@ -617,23 +617,23 @@ Qed.
 
 Lemma istep_normal_exit ge i sp rs m st:
   istep ge i sp rs m = Some st ->
-  st.(continue) = true ->
-  default_succ i = Some st.(the_pc).
+  st.(icontinue) = true ->
+  default_succ i = Some st.(ipc).
 Proof.
   destruct i; simpl; try congruence; simplify_SOME x.
   all: explore_destruct; simplify_SOME x.
 Qed.
 
 Lemma isteps_normal_exit ge path f sp: forall rs m pc st,
-  st.(continue) = true ->
+  st.(icontinue) = true ->
   isteps ge path f sp rs m pc = Some st ->
-  nth_default_succ (fn_code f) path pc = Some st.(the_pc).
+  nth_default_succ (fn_code f) path pc = Some st.(ipc).
 Proof.
   induction path; simpl. { try_simplify_someHyps. }
   intros rs m pc st CONT; try_simplify_someHyps.
   inversion_SOME i; intros Hi.
   inversion_SOME st0; intros Hst0.
-  destruct (continue st0) eqn:X; try congruence.
+  destruct (icontinue st0) eqn:X; try congruence.
   try_simplify_someHyps.
   intros; erewrite istep_normal_exit; eauto.
 Qed.
@@ -644,9 +644,9 @@ Qed.
 *)
 Lemma isteps_step_right ge path f sp: forall rs m pc st i,
   isteps ge path f sp rs m pc = Some st ->
-  st.(continue) = true ->
-  (fn_code f)!(st.(the_pc)) = Some i ->
-  istep ge i sp st.(the_rs) st.(the_mem) = isteps ge (S path) f sp rs m pc.
+  st.(icontinue) = true ->
+  (fn_code f)!(st.(ipc)) = Some i ->
+  istep ge i sp st.(irs) st.(imem) = isteps ge (S path) f sp rs m pc.
 Proof.
   induction path.
   + simpl; intros; try_simplify_someHyps. simplify_SOME st.
@@ -654,25 +654,25 @@ Proof.
   + intros rs m pc st i H.
     simpl in H.
     generalize H; clear H; simplify_SOME xx.
-    destruct (continue xx0) eqn: CONTxx0.
+    destruct (icontinue xx0) eqn: CONTxx0.
     * intros; erewrite IHpath; eauto.
     * intros; congruence.
 Qed.
 
 Lemma isteps_inversion_early ge path f sp: forall rs m pc st,
   isteps ge path f sp rs m pc = Some st ->
-  (continue st)=false ->
+  (icontinue st)=false ->
   exists st0 i path0,
     (path > path0)%nat /\
     isteps ge path0 f sp rs m pc = Some st0 /\ 
-    st0.(continue) = true /\ 
-    (fn_code f)!(st0.(the_pc)) = Some i /\
-    istep ge i sp st0.(the_rs) st0.(the_mem) = Some st.
+    st0.(icontinue) = true /\ 
+    (fn_code f)!(st0.(ipc)) = Some i /\
+    istep ge i sp st0.(irs) st0.(imem) = Some st.
 Proof.
   induction path as [|path]; simpl.
   - intros; try_simplify_someHyps; try congruence.
   - intros rs m pc st; inversion_SOME i; inversion_SOME st0.
-    destruct (continue st0) eqn: CONT.
+    destruct (icontinue st0) eqn: CONT.
     + intros STEP PC STEPS CONT0. exploit IHpath; eauto.
       clear STEPS.
       intros (st1 & i0 & path0 & BOUND & STEP1 & CONT1 & X1 & X2); auto.
@@ -687,7 +687,7 @@ Qed.
 Lemma isteps_resize ge path0 path1 f sp rs m pc st: 
  (path0 <= path1)%nat ->
   isteps ge path0 f sp rs m pc = Some st ->
-  (continue st)=false ->
+  (icontinue st)=false ->
   isteps ge path1 f sp rs m pc = Some st.
 Proof.
   induction 1 as [|path1]; simpl; auto.
@@ -696,7 +696,7 @@ Proof.
   induction path1 as [|path]; simpl; auto.
   - intros; try_simplify_someHyps; try congruence.
   - intros rs m pc st; inversion_SOME i; inversion_SOME st0; intros; try_simplify_someHyps.
-    destruct (continue st0) eqn: CONT0; eauto.
+    destruct (icontinue st0) eqn: CONT0; eauto.
 Qed.
 
 (* FIXME - add prediction *)
@@ -707,8 +707,8 @@ Inductive is_early_exit pc: instruction -> Prop :=
 
 Lemma istep_early_exit ge i sp rs m st :
   istep ge i sp rs m = Some st -> 
-  st.(continue) = false -> 
-  st.(the_rs) = rs /\ st.(the_mem) = m /\ is_early_exit st.(the_pc) i.
+  st.(icontinue) = false -> 
+  st.(irs) = rs /\ st.(imem) = m /\ is_early_exit st.(ipc) i.
 Proof.
   Local Hint Resolve Icond_early_exit: core.
   destruct i; simpl; try congruence; simplify_SOME b; simpl; try congruence.
@@ -782,7 +782,7 @@ Inductive match_inst_states_goal (idx: nat) (s1:RTL.state): state -> Prop :=
     (fn_path f)!pc = Some path ->
     (idx <= path.(psize))%nat ->
       isteps ge (path.(psize)-idx) f sp rs m pc = Some s2 ->
-      s1 = State stack f sp s2.(the_pc) s2.(the_rs) s2.(the_mem) ->
+      s1 = State stack f sp s2.(ipc) s2.(irs) s2.(imem) ->
       match_inst_states_goal idx s1 (State stack f sp pc rs m).
 
 Definition match_inst_states (idx: nat) (s1:RTL.state) (s2:state): Prop :=
@@ -797,7 +797,7 @@ Lemma istep_complete t i stack f sp rs m pc s':
   RTL.step ge (State stack f sp pc rs m) t s' ->
   (fn_code f)!pc = Some i -> 
   default_succ i <> None -> 
-  t = E0 /\ exists st, istep ge i sp rs m = Some st /\ s'=(State stack f sp st.(the_pc) st.(the_rs) st.(the_mem)).
+  t = E0 /\ exists st, istep ge i sp rs m = Some st /\ s'=(State stack f sp st.(ipc) st.(irs) st.(imem)).
 Proof.
   intros H X; inversion H; simpl; subst; try rewrite X in * |-; clear X; simplify_someHyps; try congruence;
   (split; auto); simplify_someHyps; eexists; split; simplify_someHyps; eauto.
@@ -808,8 +808,8 @@ Lemma stuttering path idx stack f sp rs m pc st t s1':
    isteps ge (path.(psize)-(S idx)) f sp rs m pc = Some st ->
    (fn_path f)!pc = Some path ->
    (S idx <= path.(psize))%nat ->
-   st.(continue) = true ->
-   RTL.step ge (State stack f sp st.(the_pc) st.(the_rs) st.(the_mem)) t s1' ->
+   st.(icontinue) = true ->
+   RTL.step ge (State stack f sp st.(ipc) st.(irs) st.(imem)) t s1' ->
    t = E0 /\ match_inst_states idx s1' (State stack f sp pc rs m).
 Proof.
   intros PSTEP PATH BOUND CONT RSTEP; exploit (internal_node_path (path.(psize)-(S idx))); omega || eauto.
@@ -827,11 +827,11 @@ Qed.
 Lemma normal_exit path stack f sp rs m pc st t s1':
    isteps ge path.(psize) f sp rs m pc = Some st ->
    (fn_path f)!pc = Some path ->
-   st.(continue) = true ->
-   RTL.step ge (State stack f sp st.(the_pc) st.(the_rs) st.(the_mem)) t s1' ->
+   st.(icontinue) = true ->
+   RTL.step ge (State stack f sp st.(ipc) st.(irs) st.(imem)) t s1' ->
    wf_stackframe stack ->
    exists s2', 
-      (path_last_step ge pge stack f sp st.(the_pc) st.(the_rs) st.(the_mem)) t s2' 
+      (path_last_step ge pge stack f sp st.(ipc) st.(irs) st.(imem)) t s2' 
        /\ (exists idx', match_states idx' s1' s2').
 Proof.
   Local Hint Resolve istep_successors list_nth_z_in: core. (* Hint for path_entry proofs *)
@@ -846,7 +846,7 @@ Proof.
     exploit (exec_istate ge pge); eauto.
     eexists; intuition eauto.
     unfold match_states, match_inst_states; simpl.
-    destruct (initialize_path (*fn_code f*) (fn_path f) (the_pc st0)) as (path0 & Hpath0); eauto.
+    destruct (initialize_path (*fn_code f*) (fn_path f) (ipc st0)) as (path0 & Hpath0); eauto.
     exists (path0.(psize)); intuition eauto.
     econstructor; eauto.
     * enough (path0.(psize)-path0.(psize)=0)%nat as ->; simpl; eauto || omega.
@@ -893,19 +893,19 @@ Lemma path_step_complete stack f sp rs m pc t s1' idx path st:
   isteps ge (path.(psize)-idx) f sp rs m pc = Some st ->
   (fn_path f)!pc = Some path ->
   (idx <= path.(psize))%nat ->
-  RTL.step ge (State stack f sp st.(the_pc) st.(the_rs) st.(the_mem)) t s1' ->
+  RTL.step ge (State stack f sp st.(ipc) st.(irs) st.(imem)) t s1' ->
   wf_stackframe stack ->
   exists idx' s2', 
       (path_step ge pge path.(psize) stack f sp rs m pc t s2' 
        \/  (t = E0 /\ s2'=(State stack f sp pc rs m) /\ (idx' < idx)%nat)
-       \/ (exists path', path_step ge pge path.(psize) stack f sp rs m pc E0 (State stack f sp st.(the_pc) st.(the_rs) st.(the_mem))
-                         /\ (fn_path f)!(the_pc st) = Some path' /\ path'.(psize) = O
-                         /\ path_step ge pge path'.(psize) stack f sp st.(the_rs) st.(the_mem) st.(the_pc) t s2')
+       \/ (exists path', path_step ge pge path.(psize) stack f sp rs m pc E0 (State stack f sp st.(ipc) st.(irs) st.(imem))
+                         /\ (fn_path f)!(ipc st) = Some path' /\ path'.(psize) = O
+                         /\ path_step ge pge path'.(psize) stack f sp st.(irs) st.(imem) st.(ipc) t s2')
        )
       /\ match_states idx' s1' s2'.
 Proof.
   Local Hint Resolve exec_early_exit exec_normal_exit: core.
-  intros PSTEP PATH BOUND RSTEP WF; destruct (st.(continue)) eqn: CONT.
+  intros PSTEP PATH BOUND RSTEP WF; destruct (st.(icontinue)) eqn: CONT.
   destruct idx as [ | idx].
   + (* path_step on normal_exit *)
      assert (path.(psize)-0=path.(psize))%nat as HH by omega. rewrite HH in PSTEP. clear HH.
@@ -920,7 +920,7 @@ Proof.
     exploit (isteps_resize ge (path.(psize) - idx)%nat path.(psize)); eauto; try omega.
     clear PSTEP; intros PSTEP.
     (* TODO for clarification: move the assert below into a separate lemma *)
-    assert (HPATH0: exists path0, (fn_path f)!(the_pc st) = Some path0).
+    assert (HPATH0: exists path0, (fn_path f)!(ipc st) = Some path0).
     { clear RSTEP.
       exploit isteps_inversion_early; eauto.
       intros (st0 & i & path0 & BOUND0 & PSTEP0 & CONT0 & PC0 & STEP0).
@@ -948,7 +948,7 @@ Proof.
       - simpl; eauto.
       - simpl; eauto.
     * (* single step case *)
-      exploit (stuttering path1 ps stack f sp (the_rs st) (the_mem st) (the_pc st)); simpl; auto.
+      exploit (stuttering path1 ps stack f sp (irs st) (imem st) (ipc st)); simpl; auto.
       - { rewrite Hpath1size; enough (S ps-S ps=0)%nat as ->; try omega.  simpl; eauto. }
       - omega.
       - simpl; eauto.
diff --git a/mppa_k1c/lib/RTLpathLiveproofs.v b/mppa_k1c/lib/RTLpathLiveproofs.v
index a807279b..8e2c22cd 100644
--- a/mppa_k1c/lib/RTLpathLiveproofs.v
+++ b/mppa_k1c/lib/RTLpathLiveproofs.v
@@ -98,10 +98,10 @@ Proof.
 Qed.
 
 Record eqlive_istate alive (st1 st2: istate): Prop :=
-   { eqlive_continue: continue st1 = continue st2;
-     eqlive_the_pc: the_pc st1 = the_pc st2;
-     eqlive_the_rs: eqlive_reg alive (the_rs st1) (the_rs st2);
-     eqlive_the_mem: (the_mem st1) = (the_mem st2) }.
+   { eqlive_continue: icontinue st1 = icontinue st2;
+     eqlive_ipc: ipc st1 = ipc st2;
+     eqlive_irs: eqlive_reg alive (irs st1) (irs st2);
+     eqlive_imem: (imem st1) = (imem st2) }.
 
 Lemma iinst_checker_eqlive ge sp pm alive i res rs1 rs2 m st1: 
   eqlive_reg (ext alive) rs1 rs2 -> 
@@ -174,8 +174,8 @@ Qed.
 Lemma iinst_checker_istep_continue ge sp pm alive i res rs m st: 
   iinst_checker pm alive i = Some res ->
   istep ge i sp rs m = Some st ->
-  continue st = true ->
-  (snd res)=(the_pc st).
+  icontinue st = true ->
+  (snd res)=(ipc st).
 Proof.
   intros; exploit iinst_checker_default_succ; eauto.
   erewrite istep_normal_exit; eauto.
@@ -199,8 +199,8 @@ Lemma iinst_checker_eqlive_stopped ge sp pm alive i res rs1 rs2 m st1:
   eqlive_reg (ext alive) rs1 rs2 -> 
   istep ge i sp rs1 m = Some st1 ->
   iinst_checker pm alive i = Some res -> 
-  continue st1 = false ->
-  exists path st2, pm!(the_pc st1) = Some path /\ istep ge i sp rs2 m = Some st2 /\ eqlive_istate (ext path.(input_regs)) st1 st2.
+  icontinue st1 = false ->
+  exists path st2, pm!(ipc st1) = Some path /\ istep ge i sp rs2 m = Some st2 /\ eqlive_istate (ext path.(input_regs)) st1 st2.
 Proof.
   intros EQLIVE.
   set (tmp := istep ge i sp rs2).
@@ -220,7 +220,7 @@ Lemma ipath_checker_eqlive_normal ge ps (f:function) sp pm: forall alive pc res
   eqlive_reg (ext alive) rs1 rs2 ->
   ipath_checker ps f pm alive pc = Some res ->
   isteps ge ps f sp rs1 m pc = Some st1 ->
-  continue st1 = true ->
+  icontinue st1 = true ->
   exists st2, isteps ge ps f sp rs2 m pc = Some st2 /\ eqlive_istate (ext (fst res)) st1 st2.
 Proof.
   induction ps as [|ps]; simpl; try_simplify_someHyps.
@@ -233,7 +233,7 @@ Proof.
     destruct 1 as (st2 & ISTEP & [CONT PC RS MEM]).
     try_simplify_someHyps.
     rewrite <- CONT, <- MEM, <- PC.
-    destruct (continue st0) eqn:CONT'.
+    destruct (icontinue st0) eqn:CONT'.
     * intros; exploit iinst_checker_istep_continue; eauto.
       rewrite <- PC; intros X; rewrite X in * |-. eauto.
     * try_simplify_someHyps.
@@ -243,14 +243,14 @@ Qed.
 Lemma ipath_checker_isteps_continue ge ps (f:function) sp pm: forall alive pc res rs m st, 
   ipath_checker ps f pm alive pc = Some res ->
   isteps ge ps f sp rs m pc = Some st ->
-  continue st = true ->
-  (snd res)=(the_pc st).
+  icontinue st = true ->
+  (snd res)=(ipc st).
 Proof.
   induction ps as [|ps]; simpl; try_simplify_someHyps.
   inversion_SOME i; try_simplify_someHyps.
   inversion_SOME res0.
   inversion_SOME st0.
-  destruct (continue st0) eqn:CONT'.
+  destruct (icontinue st0) eqn:CONT'.
   - intros; exploit iinst_checker_istep_continue; eauto.
     intros EQ; rewrite EQ in * |-; clear EQ; eauto.
   - try_simplify_someHyps; congruence.
@@ -260,15 +260,15 @@ Lemma ipath_checker_eqlive_stopped ge ps (f:function) sp pm: forall alive pc res
   eqlive_reg (ext alive) rs1 rs2 -> 
   ipath_checker ps f pm alive pc = Some res -> 
   isteps ge ps f sp rs1 m pc = Some st1 -> 
-  continue st1 = false ->
-  exists path st2, pm!(the_pc st1) = Some path /\ isteps ge ps f sp rs2 m pc = Some st2 /\ eqlive_istate (ext path.(input_regs)) st1 st2.
+  icontinue st1 = false ->
+  exists path st2, pm!(ipc st1) = Some path /\ isteps ge ps f sp rs2 m pc = Some st2 /\ eqlive_istate (ext path.(input_regs)) st1 st2.
 Proof.
   induction ps as [|ps]; simpl; try_simplify_someHyps; try congruence.
   inversion_SOME i; try_simplify_someHyps.
   inversion_SOME res0.
   inversion_SOME st0.
   intros.
-  destruct (continue st0) eqn:CONT'; try_simplify_someHyps; intros.
+  destruct (icontinue st0) eqn:CONT'; try_simplify_someHyps; intros.
   * intros; exploit iinst_checker_eqlive; eauto.
     destruct 1 as (st2 & ISTEP & [CONT PC RS MEM]).
     exploit iinst_checker_istep_continue; eauto.
@@ -452,7 +452,7 @@ Proof.
     intros PC ISTEP. erewrite inst_checker_from_iinst_checker; eauto.
     inversion_SOME res.
     intros.
-    destruct (continue st1) eqn: CONT.
+    destruct (icontinue st1) eqn: CONT.
     - (* CONT => true *)
       exploit iinst_checker_eqlive; eauto.
       destruct 1 as (st2 & ISTEP2 & [CONT' PC2 RS MEM]).
diff --git a/mppa_k1c/lib/RTLpathSE_theory.v b/mppa_k1c/lib/RTLpathSE_theory.v
index 1caea687..9c0c0c0a 100644
--- a/mppa_k1c/lib/RTLpathSE_theory.v
+++ b/mppa_k1c/lib/RTLpathSE_theory.v
@@ -47,103 +47,104 @@ Fixpoint list_sval_inj (l: list sval): list_sval :=
 Local Open Scope option_monad_scope.
 
 (* FIXME - add non trapping load eval *)
-Fixpoint sval_eval (ge: RTL.genv) (sp:val) (sv: sval) (rs0: regset) (m0: mem): option val :=
+Fixpoint seval_sval (ge: RTL.genv) (sp:val) (sv: sval) (rs0: regset) (m0: mem): option val :=
   match sv with
   | Sinput r => Some (rs0#r)
   | Sop op l sm =>
-     SOME args <- list_sval_eval ge sp l rs0 m0 IN
-     SOME m <- smem_eval ge sp sm rs0 m0 IN
+     SOME args <- seval_list_sval ge sp l rs0 m0 IN
+     SOME m <- seval_smem ge sp sm rs0 m0 IN
      eval_operation ge sp op args m
   | Sload sm chunk addr lsv =>
-     SOME args <- list_sval_eval ge sp lsv rs0 m0 IN
+     SOME args <- seval_list_sval ge sp lsv rs0 m0 IN
      SOME a <- eval_addressing ge sp addr args IN
-     SOME m <- smem_eval ge sp sm rs0 m0 IN
+     SOME m <- seval_smem ge sp sm rs0 m0 IN
      Mem.loadv chunk m a 
   end
-with list_sval_eval (ge: RTL.genv) (sp:val) (lsv: list_sval) (rs0: regset) (m0: mem): option (list val) :=
+with seval_list_sval (ge: RTL.genv) (sp:val) (lsv: list_sval) (rs0: regset) (m0: mem): option (list val) :=
   match lsv with
   | Snil => Some nil
   | Scons sv lsv' => 
-    SOME v <- sval_eval ge sp sv rs0 m0 IN
-    SOME lv <- list_sval_eval ge sp lsv' rs0 m0 IN
+    SOME v <- seval_sval ge sp sv rs0 m0 IN
+    SOME lv <- seval_list_sval ge sp lsv' rs0 m0 IN
     Some (v::lv)
   end
-with smem_eval (ge: RTL.genv) (sp:val) (sm: smem) (rs0: regset) (m0: mem): option mem :=
+with seval_smem (ge: RTL.genv) (sp:val) (sm: smem) (rs0: regset) (m0: mem): option mem :=
   match sm with
   | Sinit => Some m0
   | Sstore sm chunk addr lsv srce =>
-     SOME args <- list_sval_eval ge sp lsv rs0 m0 IN
+     SOME args <- seval_list_sval ge sp lsv rs0 m0 IN
      SOME a <- eval_addressing ge sp addr args IN
-     SOME m <- smem_eval ge sp sm rs0 m0 IN
-     SOME sv <- sval_eval ge sp srce rs0 m0 IN
+     SOME m <- seval_smem ge sp sm rs0 m0 IN
+     SOME sv <- seval_sval ge sp srce rs0 m0 IN
      Mem.storev chunk m a sv
   end.
 
 (* Syntax and Semantics of local symbolic internal states *)
-Record local_istate := { pre: RTL.genv -> val -> regset -> mem -> Prop; the_sreg: reg -> sval; the_smem: smem }.
+(* [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 sem_local_istate (ge: RTL.genv) (sp:val) (st: local_istate) (rs0: regset) (m0: mem) (rs: regset) (m: mem): Prop :=
-  st.(pre) ge sp rs0 m0
-  /\ smem_eval ge sp st.(the_smem) rs0 m0 = Some m
-  /\ forall (r:reg), sval_eval ge sp (st.(the_sreg) r) rs0 m0 = Some (rs#r).
+Definition smatch_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).
 
-Definition has_aborted_on_basic (ge: RTL.genv) (sp:val) (st: local_istate) (rs0: regset) (m0: mem): Prop :=
-  ~(st.(pre) ge sp rs0 m0)
-  \/ smem_eval ge sp st.(the_smem) rs0 m0 = None
-  \/ exists (r: reg), sval_eval ge sp (st.(the_sreg) r) rs0 m0 = None.
+Definition sabort_local (ge: RTL.genv) (sp:val) (st: sistate_local) (rs0: regset) (m0: mem): Prop :=
+  ~(st.(si_pre) ge sp rs0 m0)
+  \/ seval_smem ge sp st.(si_smem) rs0 m0 = None
+  \/ exists (r: reg), seval_sval ge sp (st.(si_sreg) r) rs0 m0 = None.
 
 (* Syntax and semantics of symbolic exit states *)
-Record exit_istate := { the_cond: condition; cond_args: list_sval; exit_ist: local_istate; cond_ifso: node }.
+Record sistate_exit := { si_cond: condition; si_scondargs: list_sval; si_elocal: sistate_local; si_ifso: node }.
 
 Definition seval_condition ge sp (cond: condition) (lsv: list_sval) (sm: smem) rs0 m0 : option bool :=
-  SOME args <- list_sval_eval ge sp lsv rs0 m0 IN
-  SOME m <- smem_eval ge sp sm rs0 m0 IN
+  SOME args <- seval_list_sval ge sp lsv rs0 m0 IN
+  SOME m <- seval_smem ge sp sm rs0 m0 IN
   eval_condition cond args m.
 
-Definition has_not_yet_exit ge sp (lx: list exit_istate) rs0 m0: Prop :=
+Definition all_fallthrough ge sp (lx: list sistate_exit) rs0 m0: Prop :=
   forall ext, List.In ext lx ->
-  seval_condition ge sp ext.(the_cond) ext.(cond_args) ext.(exit_ist).(the_smem) rs0 m0 = Some false.
+  seval_condition ge sp ext.(si_cond) ext.(si_scondargs) ext.(si_elocal).(si_smem) rs0 m0 = Some false.
 
 
-Definition has_aborted_on_test ge sp (lx: list exit_istate) rs0 m0: Prop :=
+Definition sabort_exits ge sp (lx: list sistate_exit) rs0 m0: Prop :=
   exists ext,  List.In ext lx
-    /\ seval_condition ge sp ext.(the_cond) ext.(cond_args) ext.(exit_ist).(the_smem) rs0 m0 = None.
+    /\ seval_condition ge sp ext.(si_cond) ext.(si_scondargs) ext.(si_elocal).(si_smem) rs0 m0 = None.
 
 
-Inductive sem_early_exit (ge: RTL.genv) (sp:val) (lx:list exit_istate) (rs0: regset) (m0: mem) rs m pc: Prop :=
-  SEE_intro ext lx':
+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':
     is_tail (ext::lx') lx ->
-    has_not_yet_exit ge sp lx' rs0 m0 ->
-    seval_condition ge sp ext.(the_cond) ext.(cond_args) ext.(exit_ist).(the_smem) rs0 m0 = Some true ->
-    sem_local_istate ge sp ext.(exit_ist) rs0 m0 rs m ->
-    ext.(cond_ifso) = pc ->
-    sem_early_exit ge sp lx rs0 m0 rs m pc.
+    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 ->
+    ext.(si_ifso) = pc ->
+    smatch_exits ge sp lx rs0 m0 rs m pc.
 
 
 (** * Syntax and Semantics of symbolic internal state *)
-Record s_istate := { the_pc: node; exits: list exit_istate; curr: local_istate }. 
+Record sistate := { si_pc: node; si_exits: list sistate_exit; si_local: sistate_local }. 
 
-Definition sem_istate (ge: RTL.genv) (sp:val) (st: s_istate) (rs0: regset) (m0: mem) (is: istate): Prop :=
-  if (is.(continue)) 
+Definition smatch (ge: RTL.genv) (sp:val) (st: sistate) (rs0: regset) (m0: mem) (is: istate): Prop :=
+  if (is.(icontinue)) 
   then 
-    sem_local_istate ge sp st.(curr) rs0 m0 is.(the_rs) is.(the_mem) 
-    /\ st.(the_pc) = is.(RTLpath.the_pc)
-    /\ has_not_yet_exit ge sp st.(exits) rs0 m0
-  else sem_early_exit ge sp st.(exits) rs0 m0 is.(the_rs) is.(the_mem) is.(RTLpath.the_pc).
+    smatch_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).
 
-Definition has_aborted (ge: RTL.genv) (sp:val) (st: s_istate) (rs0: regset) (m0: mem): Prop :=
-    has_aborted_on_basic ge sp st.(curr) rs0 m0
- \/ has_aborted_on_test ge sp st.(exits) rs0 m0.
+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 sem_option_istate ge sp (st: s_istate) rs0 m0 (ois: option istate): Prop :=
+Definition smatch_opt ge sp (st: sistate) rs0 m0 (ois: option istate): Prop :=
   match ois with
-  | Some is => sem_istate ge sp st rs0 m0 is
-  | None => has_aborted ge sp st rs0 m0
+  | Some is => smatch ge sp st rs0 m0 is
+  | None => sabort ge sp st rs0 m0
   end.
 
-Definition sem_option2_istate ge sp (ost: option s_istate) rs0 m0 (ois: option istate) : Prop :=
+Definition smatch_opt2 ge sp (ost: option sistate) rs0 m0 (ois: option istate) : Prop :=
   match ost with
-  | Some st => sem_option_istate ge sp st rs0 m0 ois
+  | Some st => smatch_opt ge sp st rs0 m0 ois
   | None => ois=None
   end.
 
@@ -154,10 +155,10 @@ Definition sem_option2_istate ge sp (ost: option s_istate) rs0 m0 (ois: option i
  *)
 
 Definition istate_eq ist1 ist2 :=
-  ist1.(continue) = ist2.(continue) /\
-  ist1.(RTLpath.the_pc) = ist2.(RTLpath.the_pc) /\
-  (forall r, (ist1.(the_rs)#r) = ist2.(the_rs)#r) /\ 
-  ist1.(the_mem) = ist2.(the_mem).
+  ist1.(icontinue) = ist2.(icontinue) /\
+  ist1.(ipc) = ist2.(ipc) /\
+  (forall r, (ist1.(irs)#r) = ist2.(irs)#r) /\ 
+  ist1.(imem) = ist2.(imem).
 
 (* TODO: is it useful 
 Lemma has_not_yet_exit_cons_split ge sp ext lx rs0 m0:
@@ -168,48 +169,48 @@ Proof.
 Qed.
 *)
 
-Lemma exclude_early_NYE ge sp st rs0 m0 rs m pc:
-  sem_early_exit ge sp (exits st) rs0 m0 rs m pc ->
-  has_not_yet_exit ge sp (exits st) rs0 m0 ->
+Lemma all_fallthrough_noexit ge sp st rs0 m0 rs m pc:
+  smatch_exits ge sp (si_exits st) rs0 m0 rs m pc ->
+  all_fallthrough ge sp (si_exits st) rs0 m0 ->
   False.
 Proof.
   Local Hint Resolve is_tail_in: core.
   destruct 1 as [ext lx' lc NYE' EVAL SEM PC]. subst.
-  unfold has_not_yet_exit; intros NYE; rewrite NYE in EVAL; eauto.
+  unfold all_fallthrough; intros NYE; rewrite NYE in EVAL; eauto.
   try congruence.
 Qed.
 
-Lemma sem_istate_exclude_incompatible_continue ge sp st rs m is1 is2:
-  is1.(continue) = true ->
-  is2.(continue) = false ->
-  sem_istate ge sp st rs m is1 ->
-  sem_istate ge sp st rs m is2 ->
+Lemma smatch_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 ->
   False.
 Proof.
-  Local Hint Resolve exclude_early_NYE: core.
-  unfold sem_istate.
+  Local Hint Resolve all_fallthrough_noexit: core.
+  unfold smatch.
   intros CONT1 CONT2.
   rewrite CONT1, CONT2; simpl.
   intuition eauto.
 Qed.
 
-Lemma sem_istate_determ_continue ge sp st rs m is1 is2:
-   sem_istate ge sp st rs m is1 ->
-   sem_istate ge sp st rs m is2 ->
-   is1.(continue) = is2.(continue).
+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 ->
+   is1.(icontinue) = is2.(icontinue).
 Proof.
-   Local Hint Resolve sem_istate_exclude_incompatible_continue: core.
-   destruct (Bool.bool_dec is1.(continue) is2.(continue)) as [|H]; auto.
+   Local Hint Resolve smatch_exclude_incompatible_continue: core.
+   destruct (Bool.bool_dec is1.(icontinue) is2.(icontinue)) as [|H]; auto.
    intros H1 H2. assert (absurd: False); intuition.
-   destruct (continue is1) eqn: His1, (continue is2) eqn: His2; eauto.
+   destruct (icontinue is1) eqn: His1, (icontinue is2) eqn: His2; eauto.
 Qed.
 
-Lemma sem_local_istate_determ ge sp st rs0 m0 rs1 m1 rs2 m2:
-  sem_local_istate ge sp st rs0 m0 rs1 m1 -> 
-  sem_local_istate ge sp st rs0 m0 rs2 m2 ->
+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 ->
   (forall r, rs1#r = rs2#r) /\ m1 = m2.
 Proof.
-  unfold sem_local_istate. intuition try congruence.
+  unfold smatch_local. intuition try congruence.
   generalize (H5 r); rewrite H4; congruence.
 Qed.
 
@@ -226,23 +227,23 @@ Lemma exit_cond_determ ge sp rs0 m0 l1 l2:
   is_tail l1 l2 -> forall ext1 lx1 ext2 lx2, 
   l1=(ext1 :: lx1) -> 
   l2=(ext2 :: lx2) ->
-  has_not_yet_exit ge sp lx1 rs0 m0 ->
-  seval_condition ge sp (the_cond ext1) (cond_args ext1) (the_smem (exit_ist ext1)) rs0 m0 = Some true ->
-  has_not_yet_exit ge sp lx2 rs0 m0 ->
+  all_fallthrough ge sp lx1 rs0 m0 ->
+  seval_condition ge sp (si_cond ext1) (si_scondargs ext1) (si_smem (si_elocal ext1)) rs0 m0 = Some true ->
+  all_fallthrough ge sp lx2 rs0 m0 ->
   ext1=ext2.
 Proof.
   destruct 1 as [l1|i l1 l3 T1]; intros ext1 lx1 ext2 lx2 EQ1 EQ2; subst; 
   inversion EQ2; subst; auto.
   intros D1 EVAL NYE.
   Local Hint Resolve is_tail_in: core.
-  unfold has_not_yet_exit in NYE.
+  unfold all_fallthrough in NYE.
   rewrite NYE in EVAL; eauto.
   try congruence.
 Qed.
 
-Lemma sem_early_exit_determ ge sp lx rs0 m0 rs1 m1 pc1 rs2 m2 pc2 :
-  sem_early_exit ge sp lx rs0 m0 rs1 m1 pc1 ->  
-  sem_early_exit ge sp lx rs0 m0 rs2 m2 pc2 ->
+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 ->
   pc1 = pc2 /\ (forall r, rs1#r = rs2#r) /\ m1 = m2.
 Proof.
   Local Hint Resolve exit_cond_determ eq_sym: core.
@@ -250,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 (sem_local_istate_determ ge sp (exit_ist ext2) rs0 m0 rs1 m1 rs2 m2); auto.
+  - subst. destruct (smatch_local_determ ge sp (si_elocal ext2) rs0 m0 rs1 m1 rs2 m2); auto.
 Qed.
 
-Lemma sem_istate_determ ge sp st rs m is1 is2:
-  sem_istate ge sp st rs m is1 ->
-  sem_istate ge sp st rs m is2 ->
+Lemma smatch_determ ge sp st rs m is1 is2:
+  smatch ge sp st rs m is1 ->
+  smatch ge sp st rs m is2 ->
   istate_eq is1 is2.
 Proof.
   unfold istate_eq.
   intros SEM1 SEM2. 
-  exploit (sem_istate_determ_continue ge sp st rs m is1 is2); eauto.
-  intros CONTEQ. unfold sem_istate in * |-. rewrite CONTEQ in * |- *.
-  destruct (continue is2).
-  - destruct (sem_local_istate_determ ge sp (curr st) rs m (the_rs is1) (the_mem is1) (the_rs is2) (the_mem is2)); 
+  exploit (smatch_determ_continue ge sp st rs m is1 is2); eauto.
+  intros CONTEQ. unfold smatch 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)); 
     intuition (try congruence).
-  - destruct (sem_early_exit_determ ge sp (exits st) rs m (the_rs is1) (the_mem is1) (RTLpath.the_pc is1) (the_rs is2) (the_mem is2) (RTLpath.the_pc is2));
+  - destruct (smatch_exits_determ ge sp (si_exits st) rs m (irs is1) (imem is1) (ipc is1) (irs is2) (imem is2) (ipc is2));
     intuition.
 Qed.
 
-Lemma sem_istate_exclude_abort_basic_continue ge sp st rs m is:
-  continue is = true ->
-  has_aborted_on_basic ge sp (curr st) rs m ->
-  sem_istate ge sp st rs m is -> False.
+Lemma smatch_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.
 Proof.
-  intros CONT ABORT SEM. unfold sem_istate in SEM. rewrite CONT in SEM.
+  intros CONT ABORT SEM. unfold smatch 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.
@@ -282,10 +283,10 @@ Proof.
   - inv ABORT3. rewrite SEML3 in H. discriminate.
 Qed.
 
-Lemma sem_istate_exclude_abort_basic_nocontinue ge sp st rs0 m0 is:
-  continue is = false ->
-  has_aborted_on_basic ge sp (curr st) rs0 m0 ->
-  sem_istate ge sp st rs0 m0 is -> False.
+Lemma smatch_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.
 Proof.
 (*   intros CONT ABORT SEM. unfold sem_istate in SEM. rewrite CONT in SEM.
   destruct st as [pc exits iis]. simpl in *.
@@ -298,99 +299,91 @@ Proof.
 Admitted.
 
 
-Lemma sem_istate_exclude_abort_basic ge sp st rs m is:
-  has_aborted_on_basic ge sp (curr st) rs m ->
-  sem_istate ge sp st rs m is -> False.
+Lemma smatch_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.
 Proof.
-  intros. destruct (continue is) eqn:CONT.
-  - eapply sem_istate_exclude_abort_basic_continue; eauto.
-  - eapply sem_istate_exclude_abort_basic_nocontinue; eauto.
+  intros. destruct (icontinue is) eqn:CONT.
+  - eapply smatch_exclude_sabort_local_continue; eauto.
+  - eapply smatch_exclude_sabort_local_nocontinue; eauto.
 Qed.
 
-Lemma sem_istate_exclude_abort_test ge sp st rs m is:
-  has_aborted_on_test ge sp (exits st) rs m ->
-  sem_istate ge sp st rs m is -> False.
+Lemma smatch_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.
 Proof.
 Admitted.
 
- Lemma sem_istate_exclude_abort ge sp st rs m is: 
-   has_aborted ge sp st rs m ->
-   sem_istate ge sp st rs m is -> False.
- Proof.
+Lemma smatch_exclude_sabort ge sp st rs m is:
+  sabort ge sp st rs m ->
+  smatch ge sp st rs m is -> False.
+Proof.
   intros ABORT SEM.
   inv ABORT.
-  - eapply sem_istate_exclude_abort_basic; eauto.
-  - eapply sem_istate_exclude_abort_test; eauto.
+  - eapply smatch_exclude_sabort_local; eauto.
+  - eapply smatch_exclude_sabort_exits; eauto.
 Qed.
 
-
-(* 
-    intros [[AB|[AB|AB]]|AB];
-    ( unfold sem_istate, sem_local_istate; destruct (continue is) eqn: CONT;
-       [ intros (PRE & REG & MEM) | intros [ext lx' TAIL NYE COND (PRE&REG&MEM) PC] ]; intuition try congruence).
-    (* TODO: découper cette grosse preuve à faire en lemmes *)
- Admitted.
- *)
-
-
-Definition istate_eq_option ist1 oist :=
+Definition istate_eq_opt ist1 oist :=
   exists ist2, oist = Some ist2 /\ istate_eq ist1 ist2.
 
-Lemma sem_option_istate_determ ge sp st rs m ois is:
-  sem_option_istate ge sp st rs m ois ->
-  sem_istate ge sp st rs m is -> 
-  istate_eq_option is ois.
+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 ->
+  istate_eq_opt is ois.
 Proof.
   destruct ois as [is1|]; simpl; eauto.
-  - intros; eexists; intuition; eapply sem_istate_determ; eauto.
-  - intros; exploit sem_istate_exclude_abort; eauto. destruct 1.
+  - intros; eexists; intuition; eapply smatch_determ; eauto.
+  - intros; exploit smatch_exclude_sabort; eauto. destruct 1.
 Qed.
 
 (** * Symbolic execution of one internal step *)
 
-Definition sreg_set (st:local_istate) (r:reg) (sv:sval) :=
-  {| pre:=(fun ge sp rs m => sval_eval ge sp (st.(the_sreg) r) rs m <> None /\ (st.(pre) ge sp rs m));
-     the_sreg:=fun y => if Pos.eq_dec r y then sv else st.(the_sreg) y;
-     the_smem:= st.(the_smem)|}.
+Definition slocal_set_sreg (st:sistate_local) (r:reg) (sv:sval) :=
+  {| si_pre:=(fun ge sp rs m => seval_sval ge sp (st.(si_sreg) r) rs m <> None /\ (st.(si_pre) ge sp rs m));
+     si_sreg:=fun y => if Pos.eq_dec r y then sv else st.(si_sreg) y;
+     si_smem:= st.(si_smem)|}.
 
-Definition smem_set (st:local_istate) (sm:smem) :=
-  {| pre:=(fun ge sp rs m => smem_eval ge sp st.(the_smem) rs m <> None /\ (st.(pre) ge sp rs m));
-     the_sreg:= st.(the_sreg);
-     the_smem:= sm |}.
+Definition slocal_set_smem (st:sistate_local) (sm:smem) :=
+  {| si_pre:=(fun ge sp rs m => seval_smem ge sp st.(si_smem) rs m <> None /\ (st.(si_pre) ge sp rs m));
+     si_sreg:= st.(si_sreg);
+     si_smem:= sm |}.
 
-Definition sist (st: s_istate) (pc: node) (nxt: local_istate): option s_istate :=
-   Some {| the_pc := pc; exits := st.(exits); curr:= nxt |}.
+Definition sist_set_local (st: sistate) (pc: node) (nxt: sistate_local): option sistate :=
+   Some {| si_pc := pc; si_exits := st.(si_exits); si_local:= nxt |}.
 
 (* FIXME - add notrap *)
-Definition symb_istep (i: instruction) (st: s_istate): option s_istate := 
+Definition symb_istep (i: instruction) (st: sistate): option sistate := 
   match i with
   | Inop pc' => 
-      sist st pc' st.(curr)
+      sist_set_local st pc' st.(si_local)
   | Iop op args dst pc' =>
-      let prev := st.(curr) in
-      let vargs := list_sval_inj (List.map prev.(the_sreg) args) in
-      let next := sreg_set prev dst (Sop op vargs prev.(the_smem)) in
-      sist st pc' next
+      let prev := st.(si_local) in
+      let vargs := list_sval_inj (List.map prev.(si_sreg) args) in
+      let next := slocal_set_sreg prev dst (Sop op vargs prev.(si_smem)) in
+      sist_set_local st pc' next
   | Iload _ chunk addr args dst pc' =>
-      let prev := st.(curr) in
-      let vargs := list_sval_inj (List.map prev.(the_sreg) args) in
-      let next := sreg_set prev dst (Sload prev.(the_smem) chunk addr vargs) in
-      sist st pc' next
+      let prev := st.(si_local) in
+      let vargs := list_sval_inj (List.map prev.(si_sreg) args) in
+      let next := slocal_set_sreg prev dst (Sload prev.(si_smem) chunk addr vargs) in
+      sist_set_local st pc' next
   | Istore chunk addr args src pc' =>
-      let prev := st.(curr) in
-      let vargs := list_sval_inj (List.map prev.(the_sreg) args) in
-      let next := smem_set prev (Sstore prev.(the_smem) chunk addr vargs (prev.(the_sreg) src)) in
-      sist st pc' next
+      let prev := st.(si_local) in
+      let vargs := list_sval_inj (List.map prev.(si_sreg) args) in
+      let next := slocal_set_smem prev (Sstore prev.(si_smem) chunk addr vargs (prev.(si_sreg) src)) in
+      sist_set_local st pc' next
    | Icond cond args ifso ifnot _ =>
-      let prev := st.(curr) in
-      let vargs := list_sval_inj (List.map prev.(the_sreg) args) in
-      let ex := {| the_cond:=cond; cond_args:=vargs; exit_ist := prev; cond_ifso := ifso |} in
-      Some {| the_pc := ifnot; exits := ex::st.(exits); curr := prev |}
+      let prev := st.(si_local) in
+      let vargs := list_sval_inj (List.map prev.(si_sreg) args) in
+      let ex := {| si_cond:=cond; si_scondargs:=vargs; si_elocal := prev; si_ifso := ifso |} in
+      Some {| si_pc := ifnot; si_exits := ex::st.(si_exits); si_local := prev |}
   | _ => 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, sval_eval ge sp (sreg r) rs0 m0 = Some (rs # r)) ->
+   (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).
 Proof.
   intros H; induction l as [|r l]; simpl; auto.
@@ -553,7 +546,7 @@ Fixpoint symb_isteps (path:nat) (f: function) (st: s_istate): option s_istate :=
   end.
 
 Lemma symb_isteps_correct_false ge sp path f rs0 m0 st' is: 
-  is.(continue)=false -> 
+  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.
@@ -599,7 +592,7 @@ Proof.
 Qed.
 
 Lemma symb_isteps_correct_true ge sp path (f:function) rs0 m0: forall st is,
-  is.(continue)=true -> 
+  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
@@ -619,7 +612,7 @@ Proof.
     exploit symb_istep_correct; eauto. 
     inversion_SOME st1; intros Hst1; erewrite Hst1; simpl.
     - inversion_SOME is1; intros His1;rewrite His1; simpl. 
-      * destruct (continue is1) eqn:CONT1.
+      * destruct (icontinue is1) eqn:CONT1.
         (* continue is0 = true *)
         intros; eapply IHpath; eauto.
         destruct i; simpl in * |- *; unfold sist in * |- *; try_simplify_someHyps.
@@ -677,7 +670,7 @@ Inductive sfval :=
 
 Definition s_find_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 <- sval_eval ge sp sv rs0 m0 IN Genv.find_funct pge v
+  | inl sv => SOME v <- seval 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.
 
@@ -714,7 +707,7 @@ 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 => sval_eval ge sp sv rs0 m0 | None => Some Vundef end = Some v ->
+      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 
          E0 (Returnstate stack v m')
 .
@@ -723,11 +716,11 @@ Record s_state := { internal:> s_istate; 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:
-     is.(continue) = false ->
+     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:
-     is.(continue) = true -> 
+     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 
@@ -871,7 +864,7 @@ Proof.
        exploit symb_istep_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.(continue)) eqn: CONT.
+       intro SEM; destruct (ist.(icontinue)) eqn: CONT.
        { (* continue ist = true *)
          eapply sem_normal; simpl; eauto.
          unfold sem_istate in SEM.
@@ -1026,8 +1019,8 @@ Variable ge ge': RTL.genv.
 
 Hypothesis symbols_preserved_RTL: forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s.
 
-Lemma sval_eval_preserved sp sv rs0 m0: 
-  sval_eval ge sp sv rs0 m0 = sval_eval ge' sp sv rs0 m0.
+Lemma seval_preserved sp sv rs0 m0:
+  seval ge sp sv rs0 m0 = seval 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)
@@ -1039,7 +1032,7 @@ Proof.
     erewrite <- eval_addressing_preserved; eauto.
     destruct (eval_addressing _ sp _ _); auto.
     rewrite IHsv; auto.
-  + rewrite IHsv; clear IHsv. destruct (sval_eval _ _ _ _); auto.
+  + rewrite IHsv; clear IHsv. destruct (seval _ _ _ _); auto.
     rewrite IHsv0; auto.
   + rewrite IHsv0; clear IHsv0. destruct (list_sval_eval _ _ _ _); auto.
     erewrite <- eval_addressing_preserved; eauto.
@@ -1052,7 +1045,7 @@ 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.
 Proof.
   induction lsv; simpl; auto.
-  rewrite sval_eval_preserved. destruct (sval_eval _ _ _ _); auto.
+  rewrite seval_preserved. destruct (seval _ _ _ _); auto.
   rewrite IHlsv; auto.
 Qed.
 
@@ -1064,7 +1057,7 @@ Proof.
   erewrite <- eval_addressing_preserved; eauto.
   destruct (eval_addressing _ sp _ _); auto.
   rewrite IHsm; clear IHsm. destruct (smem_eval _ _ _ _); auto.
-  rewrite sval_eval_preserved; auto.
+  rewrite seval_preserved; auto.
 Qed.
 
 Lemma seval_condition_preserved sp cond lsv sm rs0 m0:
@@ -1080,12 +1073,12 @@ End SymbValPreserved.
 Require Import RTLpathLivegen RTLpathLiveproofs.
 
 Definition istate_simulive alive (srce: PTree.t node) (is1 is2: istate): Prop :=
-     is1.(continue) = is2.(continue)
+     is1.(icontinue) = is2.(icontinue)
      /\ eqlive_reg alive is1.(the_rs) is2.(the_rs)
      /\ is1.(the_mem) = is2.(the_mem).
 
 Definition istate_simu f (srce: PTree.t node) is1 is2: Prop :=
-  if is1.(continue) then
+  if is1.(icontinue) then
      (* TODO: il faudra raffiner le (fun _ => True) si on veut autoriser l'oracle à
         ajouter du "code mort" sur des registres non utilisés (loop invariant code motion à la David)
         Typiquement, pour connaître la frame des registres vivants, il faudra faire une propagation en arrière