Merge branch 'BTL_fsem' into BTL

5 files changed, 840 insertions, 284 deletions

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index caa48920..2be4fcac 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -17,6 +17,9 @@
 Require Import Coqlib Maps.
 Require Import AST Integers Values Events Memory Globalenvs Smallstep.
 Require Import RTL Op Registers OptionMonad.
+Require Import Lia.
+
+Import ListNotations.
 
 (** * Abstract syntax *)
 
@@ -91,7 +94,7 @@ Coercion BF: final >-> Funclass.
 
 Record iblock_info := { 
   entry: iblock;
-  input_regs: Regset.t; (* extra liveness information ignored by BTL semantics *)
+  input_regs: Regset.t (* extra liveness information for BTL functional semantics *)
   binfo: block_info (* Ghost field used in oracles *)
 }.
 
@@ -168,8 +171,26 @@ Record outcome := out {
    _fin: option final 
 }.
 
+(* follows RTL semantics to set the result of builtin *)
+Definition reg_builtin_res (res: builtin_res reg): option reg :=
+  match res with
+  | BR r => Some r
+  | _ => None
+  end.
+
 Section RELSEM.
 
+(** [step] (and in particular [final_step]) is parametrized by function [tr_exit] to transfer registers on each iblock exit.
+
+    In particular, [tr_exit f lpc or rs] computes from [rs] the [rs'] on which the execution from iblock [pc] in [lpc] in [f] may start.
+
+    Here, [or] is an optional register that will be assigned after exiting the iblock, but before entering in [pc]: e.g. the register set by a function call
+    before entering in return address.
+
+*)
+
+Variable tr_exit: function -> list exit -> option reg -> regset -> regset.
+
 Variable ge: genv.
 
 Definition find_function (ros: reg + ident) (rs: regset) : option fundef :=
@@ -280,10 +301,12 @@ Proof.
     destruct o; try_simplify_someHyps; subst; eauto.
 Qed.
 
+Local Open Scope list_scope.
+
 Inductive final_step stack f sp rs m: final -> trace -> state -> Prop :=
   | exec_Bgoto pc:
       final_step stack f sp rs m (Bgoto pc) E0
-                 (State stack f sp pc rs m)
+                 (State stack f sp pc (tr_exit f [pc] None rs) m)
   | exec_Breturn or stk m':
       sp = (Vptr stk Ptrofs.zero) ->
       Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
@@ -293,7 +316,7 @@ Inductive final_step stack f sp rs m: final -> trace -> state -> Prop :=
       find_function ros rs = Some fd ->
       funsig fd = sig ->
       final_step stack f sp rs m (Bcall sig ros args res pc')
-        E0 (Callstate (Stackframe res f sp pc' rs :: stack) fd rs##args m)
+        E0 (Callstate (Stackframe res f sp pc' (tr_exit f [pc'] (Some res) rs) :: stack) fd rs##args m)
   | exec_Btailcall sig ros args stk m' fd:
       find_function ros rs = Some fd ->
       funsig fd = sig ->
@@ -305,12 +328,12 @@ Inductive final_step stack f sp rs m: final -> trace -> state -> Prop :=
       eval_builtin_args ge (fun r => rs#r) sp m args vargs ->
       external_call ef ge vargs m t vres m' ->
       final_step stack f sp rs m (Bbuiltin ef args res pc')
-         t (State stack f sp pc' (regmap_setres res vres rs) m')
+         t (State stack f sp pc' (regmap_setres res vres (tr_exit f [pc'] (reg_builtin_res res) rs)) m')
   | exec_Bjumptable arg tbl n pc':
       rs#arg = Vint n ->
       list_nth_z tbl (Int.unsigned n) = Some pc' ->
       final_step stack f sp rs m (Bjumptable arg tbl)
-        E0 (State stack f sp pc' rs m)
+        E0 (State stack f sp pc' (tr_exit f tbl None rs) m)
 .
 
 (** big-step execution of one iblock *)
@@ -367,11 +390,463 @@ Inductive final_state: state -> int -> Prop :=
   | final_state_intro: forall r m,
       final_state (Returnstate nil (Vint r) m) r.
 
-(** The small-step semantics for a program. *)
+(** The "raw" CFG small-step semantics for a BTL program (e.g. close to RTL semantics) *)
+
+(* tid = transfer_identity *)
+Definition tid (_:function) (_:list exit) (_: option reg) (rs:regset) := rs.
+
+Definition cfgsem (p: program) :=
+  Semantics (step tid) (initial_state p) final_state (Genv.globalenv p).
+
+(** The full "functional" small-step semantics for a BTL program.
+    at each exit, we only transfer register in "input_regs" (i.e. "alive" registers).
+*)
+Definition transfer_regs (inputs: list reg) (rs: regset): regset :=
+  init_regs (rs##inputs) inputs.
+
+Lemma transfer_regs_inputs inputs rs r:
+  List.In r inputs -> (transfer_regs inputs rs)#r = rs#r.
+Proof.
+  unfold transfer_regs; induction inputs; simpl; intuition subst.
+  - rewrite Regmap.gss; auto.
+  - destruct (Pos.eq_dec a r).
+    + subst; rewrite Regmap.gss; auto.
+    + rewrite Regmap.gso; auto.
+Qed.
+
+Lemma transfer_regs_dead inputs rs r:
+  ~List.In r inputs -> (transfer_regs inputs rs)#r = Vundef.
+Proof.
+  unfold transfer_regs; induction inputs; simpl; intuition subst.
+  - rewrite Regmap.gi; auto.
+  - rewrite Regmap.gso; auto.
+Qed.
+
+Fixpoint union_inputs (f:function) (tbl: list exit): Regset.t :=
+  match tbl with
+  | nil => Regset.empty
+  | pc::l => let rs:= union_inputs f l in
+             match f.(fn_code)!pc with
+             | None => rs
+             | Some ib => Regset.union rs ib.(input_regs)
+             end
+  end.
+
+(* TODO: lemma not yet used
+
+Lemma union_inputs_In f tbl r:
+  Regset.In r (union_inputs f tbl) -> (exists pc, List.In pc tbl /\ exists ib, f.(fn_code)!pc = Some ib /\ Regset.In r ib.(input_regs)).
+Proof.
+  induction tbl as [|pc l]; simpl; intros.
+  - exploit Regset.empty_1; eauto. intuition.
+  - destruct ((fn_code f) ! pc) eqn:ATpc.
+    + exploit Regset.union_1; eauto.
+      destruct 1 as [X1|X1].
+      * destruct IHl as (pc' & H1 & H2); eauto.
+      * eexists; intuition eauto.
+    + destruct IHl as (pc' & H1 & H2); eauto.
+Qed.
+
+Lemma union_inputs_notIn f tbl r: 
+   (forall pc ib, List.In pc tbl -> f.(fn_code)!pc = Some ib -> ~Regset.In r ib.(input_regs))
+    -> ~Regset.In r (union_inputs f tbl).
+Proof.
+  induction tbl as [|pc l]; simpl; intuition eauto.
+  - exploit Regset.empty_1; eauto.
+  - destruct ((fn_code f) ! pc) eqn:ATpc; intuition eauto.
+    exploit Regset.union_1; intuition eauto.
+Qed.
+*)
+
+(* This function computes the union of the inputs associated to the exits
+                   minus the optional register in [or] (typically the result of a call or a builtin).
+   i.e. similar to [pre_output_regs] in RTLpath.
+*)
+Definition pre_inputs (f:function) (tbl: list exit) (or: option reg): Regset.t :=
+ let rs := union_inputs f tbl in
+ match or with 
+ | Some r => Regset.remove r rs
+ | None => rs
+ end
+ .
+
+(* TODO: lemma pre_inputs_In + pre_inputs_notIn ? *)
+
+Definition tr_inputs (f:function) (tbl: list exit) (or:option reg): regset -> regset 
+  := transfer_regs (Regset.elements (pre_inputs f tbl or)).
+
+
+(* TODO: move this elsewhere *)
+Lemma SetoidList_InA_eq_equiv A (l: list A): forall x,
+  SetoidList.InA (fun x y => x = y) x l <-> List.In x l.
+Proof.
+  intros x; split.
+  - induction 1; simpl; eauto.
+  - induction l; simpl; intuition.
+Qed.
+
+Lemma tr_pre_inputs f tbl or rs r:
+  Regset.In r (pre_inputs f tbl or) -> (tr_inputs f tbl or rs)#r = rs#r.
+Proof.
+  intros; eapply transfer_regs_inputs.
+  rewrite <- SetoidList_InA_eq_equiv.
+  eapply Regset.elements_1; eauto.
+Qed.
+
+Lemma tr_inputs_dead f tbl or rs r:
+  ~(Regset.In r (pre_inputs f tbl or)) -> (tr_inputs f tbl or rs)#r = Vundef.
+Proof.
+  intros X; eapply transfer_regs_dead; intuition eauto.
+  eapply X. eapply Regset.elements_2. 
+  rewrite -> SetoidList_InA_eq_equiv; eauto.
+Qed.
+
+Local Hint Resolve tr_pre_inputs Regset.mem_2 Regset.mem_1: core.
+
+Lemma tr_inputs_get f tbl or rs r:
+  (tr_inputs f tbl or rs)#r = if Regset.mem r (pre_inputs f tbl or) then rs#r else Vundef.
+Proof.
+  autodestruct; eauto.
+  intros; apply tr_inputs_dead; eauto.
+  intro X; exploit Regset.mem_1; eauto.
+  congruence.
+Qed.
+
+(* TODO: not yet used
+Lemma tr_inputs_ext f tbl or rs1 rs2:
+  (forall r, Regset.In r (pre_inputs f tbl or) -> rs1#r = rs2#r) ->
+  (forall r, (tr_inputs f tbl or rs1)#r = (tr_inputs f tbl or rs2)#r).
+Proof.
+  intros EQ r. rewrite !tr_inputs_get.
+  autodestruct; auto.
+Qed.
+*)
+
+Definition fsem (p: program) :=
+  Semantics (step tr_inputs) (initial_state p) final_state (Genv.globalenv p).
+
+Local Open Scope list_scope.
+
+Definition poly_tr {A} (tr: function -> list exit -> option reg -> A) f (i: final): A := 
+  match i with
+  | Bgoto pc => tr f [pc] None
+  | Bcall _ _ _ res pc => tr f [pc] (Some res)
+  | Btailcall _ _ args => tr f [] None
+  | Bbuiltin _ _ res pc => tr f [pc] (reg_builtin_res res)
+  | Breturn _ => tr f [] None
+  | Bjumptable _ tbl => tr f tbl None
+  end.
+
+Definition tr_regs: function -> final -> regset -> regset :=
+  poly_tr tr_inputs.
+
+(* TODO: NOT USEFUL ?
+Definition liveout: function -> final -> Regset.t :=
+  poly_tr pre_inputs.
+
+Lemma tr_regs_liveout_equiv f fi : tr_regs f fi = transfer_regs (Regset.elements (liveout f fi)).
+Proof.
+  destruct fi; simpl; auto.
+Qed.
+
+Local Hint Resolve tr_inputs_get: core.
+
+Lemma tr_regs_get f fi rs r: (tr_regs f fi rs)#r = if Regset.mem r (liveout f fi) then rs#r else Vundef.
+Proof.
+   Local Opaque pre_inputs.
+   destruct fi; simpl; auto.
+Qed.
+*)
+
+(* * Comparing BTL semantics modulo extensionality of [regset].
+
+NB: This is at least used in BTL_SEtheory (and probably in the future BTL_SchedulerProof).
+
+*)
+Inductive equiv_stackframe: stackframe -> stackframe -> Prop :=
+  | equiv_stackframe_intro res f sp pc (rs1 rs2: regset)
+      (EQUIV: forall r, rs1#r = rs2#r)
+      :equiv_stackframe (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2)
+  .
+
+Inductive equiv_state: state -> state -> Prop :=
+  | State_equiv stk1 stk2 f sp pc rs1 m rs2
+      (STACKS: list_forall2 equiv_stackframe stk1 stk2)
+      (EQUIV: forall r, rs1#r = rs2#r)
+      :equiv_state (State stk1 f sp pc rs1 m) (State stk2 f sp pc rs2 m)
+  | Call_equiv stk1 stk2 f args m
+      (STACKS: list_forall2 equiv_stackframe stk1 stk2)
+      :equiv_state (Callstate stk1 f args m) (Callstate stk2 f args m)
+  | Return_equiv stk1 stk2 v m
+      (STACKS: list_forall2 equiv_stackframe stk1 stk2)
+      :equiv_state (Returnstate stk1 v m) (Returnstate stk2 v m)
+  .
+Local Hint Constructors equiv_stackframe equiv_state: core.
+
+Lemma equiv_stackframe_refl stf: equiv_stackframe stf stf.
+Proof.
+  destruct stf; eauto.
+Qed.
+
+Lemma equiv_stack_refl stk: list_forall2 equiv_stackframe stk stk.
+Proof.
+  Local Hint Resolve equiv_stackframe_refl: core.
+  induction stk; simpl; constructor; auto.
+Qed.
+Local Hint Resolve equiv_stack_refl: core.
+
+Lemma equiv_state_refl s: equiv_state s s.
+Proof.
+  induction s; simpl; constructor; auto.
+Qed.
+
+Lemma equiv_stackframe_trans stf1 stf2 stf3:
+  equiv_stackframe stf1 stf2 -> equiv_stackframe stf2 stf3 -> equiv_stackframe stf1 stf3.
+Proof.
+  destruct 1; intros EQ; inv EQ; try econstructor; eauto.
+  intros; eapply eq_trans; eauto.
+Qed.
+Local Hint Resolve equiv_stackframe_trans: core.
+
+Lemma equiv_stack_trans stk1 stk2:
+  list_forall2 equiv_stackframe stk1 stk2 -> 
+  forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> 
+  list_forall2 equiv_stackframe stk1 stk3.
+Proof.
+  induction 1; intros stk3 EQ; inv EQ; econstructor; eauto.
+Qed.
+
+Lemma equiv_state_trans s1 s2 s3: equiv_state s1 s2 -> equiv_state s2 s3 -> equiv_state s1 s3.
+Proof.
+  Local Hint Resolve equiv_stack_trans: core.
+  destruct 1; intros EQ; inv EQ; econstructor; eauto.
+  intros; eapply eq_trans; eauto.
+Qed.
+
+Lemma regmap_setres_eq (rs rs': regset) res vres:
+  (forall r, rs # r = rs' # r) ->
+  forall r, (regmap_setres res vres rs) # r = (regmap_setres res vres rs') # r.
+Proof.
+  intros RSEQ r. destruct res; simpl; try congruence.
+  destruct (peq x r).
+  - subst. repeat (rewrite Regmap.gss). reflexivity.
+  - repeat (rewrite Regmap.gso); auto.
+Qed.
+
+(* * Simulation of BTL fsem by BTL cfgsem: a lock-step less-def simulation.
+
+We start by extending the previous [equiv_*] stuff for [Val.lessdef]: we need to also compare memories 
+for Mem.extends, because Vundef values are propagated in memory through stores, allocation, etc.
+
+*)
+
+Inductive lessdef_stackframe: stackframe -> stackframe -> Prop :=
+  | lessdef_stackframe_intro res f sp pc rs1 rs2
+      (REGS: forall r, Val.lessdef rs1#r rs2#r)
+      :lessdef_stackframe (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2)
+  .
+
+Inductive lessdef_state: state -> state -> Prop :=
+  | State_lessdef stk1 stk2 f sp pc rs1 m1 rs2 m2
+      (STACKS: list_forall2 lessdef_stackframe stk1 stk2)
+      (REGS: forall r, Val.lessdef rs1#r rs2#r)
+      (MEMS: Mem.extends m1 m2)
+      :lessdef_state (State stk1 f sp pc rs1 m1) (State stk2 f sp pc rs2 m2)
+  | Call_lessdef stk1 stk2 f args1 args2 m1 m2
+      (STACKS: list_forall2 lessdef_stackframe stk1 stk2)
+      (ARGS: Val.lessdef_list args1 args2)
+      (MEMS: Mem.extends m1 m2)
+      :lessdef_state (Callstate stk1 f args1 m1) (Callstate stk2 f args2 m2)
+  | Return_lessdef stk1 stk2 v1 v2 m1 m2
+      (STACKS: list_forall2 lessdef_stackframe stk1 stk2)
+      (REGS: Val.lessdef v1 v2)
+      (MEMS: Mem.extends m1 m2)
+      :lessdef_state (Returnstate stk1 v1 m1) (Returnstate stk2 v2 m2)
+  .
+Local Hint Constructors lessdef_stackframe lessdef_state: core.
+
+Lemma lessdef_stackframe_refl stf: lessdef_stackframe stf stf.
+Proof.
+  destruct stf; eauto.
+Qed.
+
+Local Hint Resolve lessdef_stackframe_refl: core.
+Lemma lessdef_stack_refl stk: list_forall2 lessdef_stackframe stk stk.
+Proof.
+  induction stk; simpl; constructor; auto.
+Qed.
+
+Local Hint Resolve lessdef_stack_refl: core.
+
+Lemma lessdef_list_refl args: Val.lessdef_list args args.
+Proof.
+  induction args; simpl; auto.
+Qed.
+
+Local Hint Resolve lessdef_list_refl Mem.extends_refl: core.
+
+Lemma lessdef_state_refl s: lessdef_state s s.
+Proof.
+  induction s; simpl; constructor; auto.
+Qed.
 
-Definition semantics (p: program) :=
-  Semantics step (initial_state p) final_state (Genv.globalenv p).
+Local Hint Resolve Val.lessdef_trans: core.
+Lemma lessdef_stackframe_trans stf1 stf2 stf3:
+  lessdef_stackframe stf1 stf2 -> lessdef_stackframe stf2 stf3 -> lessdef_stackframe stf1 stf3.
+Proof.
+  destruct 1. intros LD; inv LD; try econstructor; eauto.
+Qed.
+
+Local Hint Resolve lessdef_stackframe_trans: core.
+Lemma lessdef_stack_trans stk1 stk2:
+  list_forall2 lessdef_stackframe stk1 stk2 -> 
+  forall stk3, list_forall2 lessdef_stackframe stk2 stk3 -> 
+  list_forall2 lessdef_stackframe stk1 stk3.
+Proof.
+  induction 1; intros stk3 LD; inv LD; econstructor; eauto.
+Qed.
+
+Local Hint Resolve lessdef_stack_trans Mem.extends_extends_compose Val.lessdef_list_trans: core.
+Lemma lessdef_state_trans s1 s2 s3: lessdef_state s1 s2 -> lessdef_state s2 s3 -> lessdef_state s1 s3.
+Proof.
+  destruct 1; intros LD; inv LD; econstructor; eauto.
+Qed.
+
+Lemma init_regs_lessdef_preserv args1 args2
+  (ARGS : Val.lessdef_list args1 args2)
+  : forall rl r, Val.lessdef (init_regs args1 rl)#r (init_regs args2 rl)#r.
+Proof.
+  induction ARGS; simpl; auto.
+  intros rl r1; destruct rl; simpl in *; auto.
+  eapply set_reg_lessdef; eauto.
+  intros r2; eauto.
+Qed.
+Local Hint Resolve init_regs_lessdef_preserv: core.
+
+Lemma tr_inputs_lessdef f rs1 rs2 tbl or r
+  (REGS: forall r, Val.lessdef rs1#r rs2#r)
+  :Val.lessdef (tr_inputs f tbl or rs1)#r (tid f tbl or rs2)#r.
+Proof.
+  unfold tid; rewrite tr_inputs_get.
+  autodestruct.
+Qed.
+Local Hint Resolve tr_inputs_lessdef: core.
 
+Lemma find_function_lessdef ge ros rs1 rs2 fd
+  (FIND: find_function ge ros rs1 = Some fd)
+  (REGS: forall r, Val.lessdef rs1#r rs2#r)
+  : find_function ge ros rs2 = Some fd.
+Proof.
+  destruct ros; simpl in *; auto.
+  exploit Genv.find_funct_inv; eauto.
+  intros (b & EQ).
+  destruct (REGS r); try congruence.
+Qed.
+Local Hint Resolve find_function_lessdef regs_lessdef_regs: core.
+
+
+Lemma fsem2cfgsem_ibistep_simu ge sp rs1 m1 ib rs1' m1' of
+  (ISTEP: iblock_istep ge sp rs1 m1 ib rs1' m1' of)
+  rs2 m2
+  (REGS: forall r, Val.lessdef rs1#r rs2#r)
+  (MEMS: Mem.extends m1 m2)
+  : exists rs2' m2', iblock_istep_run ge sp ib rs2 m2 = Some (out rs2' m2' of) 
+     /\ (forall r, Val.lessdef rs1'#r rs2'#r)
+     /\ (Mem.extends m1' m2').
+Proof.
+  induction ISTEP; simpl; try_simplify_someHyps.
+Admitted.
+
+Local Hint Constructors final_step list_forall2: core.
+Local Hint Unfold regs_lessdef: core.
+
+Lemma fsem2cfgsem_finalstep_simu ge stk1 f sp rs1 m1 fin t s1 stk2 rs2 m2
+  (FSTEP: final_step tr_inputs ge stk1 f sp rs1 m1 fin t s1)
+  (STACKS: list_forall2 lessdef_stackframe stk1 stk2)
+  (REGS: forall r, Val.lessdef rs1#r rs2#r)
+  (MEMS: Mem.extends m1 m2)
+  : exists s2, final_step tid ge stk2 f sp rs2 m2 fin t s2
+               /\ lessdef_state s1 s2.
+Proof.
+  destruct FSTEP; try (eexists; split; simpl; econstructor; eauto; fail).
+  - (* return *)
+    exploit Mem.free_parallel_extends; eauto.
+    intros (m2' & FREE & MEMS2).
+    eexists; split; simpl; econstructor; eauto.
+    destruct or; simpl; auto.
+  - (* tailcall *)
+    exploit Mem.free_parallel_extends; eauto.
+    intros (m2' & FREE & MEMS2).
+    eexists; split; simpl; econstructor; eauto.
+  - (* builtin *)
+    exploit (eval_builtin_args_lessdef (ge:=ge) (e1:=(fun r => rs1 # r)) (fun r => rs2 # r)); eauto.
+    intros (vl2' & BARGS & VARGS).
+    exploit external_call_mem_extends; eauto.
+    intros (vres' & m2' & CALL2 & REGS2 & MEMS2 & UNCHANGED).
+    eexists; split; simpl; econstructor; eauto.
+    intros; apply set_res_lessdef; eauto.
+  - (* jumptable *)
+    eexists; split; simpl; econstructor; eauto.
+    destruct (REGS arg); try congruence.
+Qed.
+
+Lemma fsem2cfgsem_ibstep_simu ge stk1 stk2 f sp rs1 m1 ib t s1 rs2 m2
+  (STEP: iblock_step tr_inputs ge stk1 f sp rs1 m1 ib t s1)
+  (STACKS : list_forall2 lessdef_stackframe stk1 stk2)
+  (REGS: forall r, Val.lessdef rs1#r rs2#r)
+  (MEMS : Mem.extends m1 m2)
+  : exists s2, iblock_step tid ge stk2 f sp rs2 m2 ib t s2
+               /\ lessdef_state s1 s2.
+Proof.
+  destruct STEP as (rs1' & m1' & fin & ISTEP & FSTEP).
+  exploit fsem2cfgsem_ibistep_simu; eauto.
+  intros (rs2' & m2' & ISTEP2 & REGS2 & MEMS2).
+  rewrite <- iblock_istep_run_equiv in ISTEP2. clear ISTEP REGS MEMS.
+  exploit fsem2cfgsem_finalstep_simu; eauto.
+  intros (s2 & FSTEP2 & LESSDEF). clear FSTEP.
+  unfold iblock_step; eexists; split; eauto.
+Qed.
+
+Local Hint Constructors step: core.
+
+Lemma fsem2cfgsem_step_simu ge s1 t s1' s2
+ (STEP: step tr_inputs ge s1 t s1')
+ (REGS: lessdef_state s1 s2)
+ :exists s2' : state,
+   step tid ge s2 t s2' /\
+   lessdef_state s1' s2'.
+Proof.
+  destruct STEP; inv REGS.
+  - (* iblock *)
+    intros; exploit fsem2cfgsem_ibstep_simu; eauto. clear STEP.
+    intros (s2 & STEP2 & REGS2).
+    eexists; split; eauto.
+  - (* internal call *)
+    exploit (Mem.alloc_extends m m2 0 (fn_stacksize f) stk m' 0 (fn_stacksize f)); eauto.
+    1-2: lia.
+    intros (m2' & ALLOC2 & MEMS2). clear ALLOC MEMS.
+    eexists; split; econstructor; eauto.
+  - (* external call *)
+    exploit external_call_mem_extends; eauto.
+    intros (vres' & m2' & CALL2 & REGS2 & MEMS2 & UNCHANGED). clear EXTCALL MEMS.
+    eexists; split; econstructor; eauto.
+  - (* return *)
+    inversion STACKS as [|d1 d2 d3 d4 STF2 STK2]. subst.
+    inv STF2.
+    eexists; split; econstructor; eauto.
+    intros; eapply set_reg_lessdef; eauto.
+Qed.
+
+Theorem fsem2cfgsem prog:
+  forward_simulation (fsem prog) (cfgsem prog).
+Proof.
+  eapply forward_simulation_step with lessdef_state; simpl; auto.
+  - destruct 1; intros; eexists; intuition eauto. econstructor; eauto.
+  - intros s1 s2 r REGS FINAL; destruct FINAL.
+     inv REGS; inv STACKS; inv REGS0.
+     econstructor; eauto.
+  - intros; eapply fsem2cfgsem_step_simu; eauto.
+Qed.
 
 (** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *)
 
diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index cd69cd37..cea69f55 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -1,7 +1,12 @@
-(* A theory of symbolic execution on BTL
+(** A theory of symbolic simulation (i.e. simulation of symbolic executions) on BTL blocks.
 
 NB: an efficient implementation with hash-consing will be defined in another file (some day)
 
+The main theorem of this file is [symbolic_simu_correct] stating
+that the abstract definition of symbolic simulation of two BTL blocks
+implies the simulation for BTL.fsem block-steps.
+
+
 *)
 
 Require Import Coqlib Maps Floats.
@@ -9,10 +14,6 @@ Require Import AST Integers Values Events Memory Globalenvs Smallstep.
 Require Import Op Registers.
 Require Import RTL BTL OptionMonad.
 
-(* TODO remove this, when copy-paste of RTLpathSE_theory is clearly over... *)
-Ltac inversion_SOME := fail.  (* deprecated tactic of OptionMonad: use autodestruct instead *)
-Ltac inversion_ASSERT := fail. (* deprecated tactic of OptionMonad: use autodestruct instead *)
-
 Record iblock_exec_context := Bctx {
   cge: BTL.genv;
   cstk: list stackframe;
@@ -26,6 +27,7 @@ Record iblock_exec_context := Bctx {
 
 (* symbolic value *)
 Inductive sval :=
+  | Sundef
   | Sinput (r: reg)
   | Sop (op:operation) (lsv: list_sval)  (sm: smem)
   | Sload (sm: smem) (trap: trapping_mode) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) 
@@ -51,6 +53,7 @@ Local Open Scope option_monad_scope.
 
 Fixpoint eval_sval ctx (sv: sval): option val :=
   match sv with
+  | Sundef => Some Vundef
   | Sinput r => Some ((crs0 ctx)#r)
   | Sop op l sm =>
      SOME args <- eval_list_sval ctx l IN
@@ -109,7 +112,7 @@ Definition seval_condition ctx (cond: condition) (lsv: list_sval) (sm: smem) : o
 
 
 (** * Auxiliary definitions on Builtins *)
-(* TODO: clean this. Some (cge ctx)neric stuffs could be put in [AST.v] *)
+(* TODO: clean this. Some generic stuffs could be put in [AST.v] *)
 
 Section SEVAL_BUILTIN_ARG. (* adapted from Events.v *)
 
@@ -166,7 +169,7 @@ Qed.
 
 End SEVAL_BUILTIN_ARG.
 
-(* NB: (cge ctx)neric function that could be put into [AST] file *)
+(* NB: generic function that could be put into [AST] file *)
 Fixpoint builtin_arg_map {A B} (f: A -> B) (arg: builtin_arg A) : builtin_arg B :=
   match arg with
   | BA x => BA (f x)
@@ -381,7 +384,6 @@ Qed.
 Inductive sfval :=
   | Sgoto (pc: exit)
   | Scall (sig:signature) (svos: sval + ident) (lsv:list_sval) (res:reg) (pc:exit)
-    (* NB: [res] the return register is hard-wired ! Is it restrictive ? *)
   | Stailcall: signature -> sval + ident -> list_sval -> sfval
   | Sbuiltin (ef:external_function) (sargs: list (builtin_arg sval)) (res: builtin_res reg) (pc:exit)
   | Sjumptable (sv: sval) (tbl: list exit)
@@ -395,21 +397,24 @@ Definition sfind_function ctx (svos : sval + ident): option fundef :=
   end
 .
 
+Import ListNotations.
+Local Open Scope list_scope.
+
 Inductive sem_sfval ctx: sfval -> regset -> mem -> trace -> state -> Prop :=
   | exec_Sgoto pc rs m:
-      sem_sfval ctx (Sgoto pc) rs m E0 (State (cstk ctx) (cf ctx) (csp ctx) pc rs m)
+      sem_sfval ctx (Sgoto pc) rs m E0 (State (cstk ctx) (cf ctx) (csp ctx) pc (tr_inputs ctx.(cf) [pc] None rs) m)
   | exec_Sreturn stk osv rs m m' v:
       (csp ctx) = (Vptr stk Ptrofs.zero) ->
       Mem.free m stk 0 (cf ctx).(fn_stacksize) = Some m' ->
       match osv with Some sv => eval_sval ctx sv | None => Some Vundef end = Some v ->
-      sem_sfval ctx (Sreturn osv) rs m 
+      sem_sfval ctx (Sreturn osv) rs m
          E0 (Returnstate (cstk ctx) v m')
   | exec_Scall rs m sig svos lsv args res pc fd:
       sfind_function ctx svos = Some fd ->
       funsig fd = sig ->
       eval_list_sval ctx lsv = Some args ->
       sem_sfval ctx (Scall sig svos lsv res pc) rs m
-        E0 (Callstate (Stackframe res (cf ctx) (csp ctx) pc rs :: (cstk ctx)) fd args m)
+        E0 (Callstate (Stackframe res (cf ctx) (csp ctx) pc (tr_inputs ctx.(cf) [pc] (Some res) rs)::cstk ctx) fd args m)
   | exec_Stailcall stk rs m sig svos args fd m' lsv:
       sfind_function ctx svos = Some fd ->
       funsig fd = sig ->
@@ -422,136 +427,23 @@ Inductive sem_sfval ctx: sfval -> regset -> mem -> trace -> state -> Prop :=
       seval_builtin_args ctx m sargs vargs ->
       external_call ef (cge ctx) vargs m t vres m' ->
       sem_sfval ctx (Sbuiltin ef sargs res pc) rs m
-        t (State (cstk ctx) (cf ctx) (csp ctx) pc (regmap_setres res vres rs) m')
+        t (State (cstk ctx) (cf ctx) (csp ctx) pc (regmap_setres res vres (tr_inputs (cf ctx) [pc] (reg_builtin_res res) rs)) m')
   | exec_Sjumptable sv tbl pc' n rs m:
       eval_sval ctx sv = Some (Vint n) ->
       list_nth_z tbl (Int.unsigned n) = Some pc' ->
       sem_sfval ctx (Sjumptable sv tbl) rs m
-        E0 (State (cstk ctx) (cf ctx) (csp ctx) pc' rs m)
+        E0 (State (cstk ctx) (cf ctx) (csp ctx) pc' (tr_inputs ctx.(cf) tbl None rs) m)
 .
 
-(** * Preservation properties *)
-
-Section SymbValPreserved.
-
-Variable ge ge': BTL.genv.
-
-Hypothesis symbols_preserved_BTL: forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s.
-
-Hypothesis senv_preserved_BTL: Senv.equiv ge ge'.
-
-Lemma senv_find_symbol_preserved id:
-  Senv.find_symbol ge id = Senv.find_symbol ge' id.
-Proof.
-  destruct senv_preserved_BTL as (A & B & C). congruence.
-Qed.
-
-Lemma senv_symbol_address_preserved id ofs:
-  Senv.symbol_address ge id ofs = Senv.symbol_address ge' id ofs.
-Proof.
-  unfold Senv.symbol_address. rewrite senv_find_symbol_preserved.
-  reflexivity.
-Qed.
-
-Variable stk stk': list stackframe.
-Variable f f': function.
-Variable sp: val.
-Variable rs0: regset.
-Variable m0: mem.
-
-Lemma eval_sval_preserved sv:
-  eval_sval (Bctx ge stk f sp rs0 m0) sv = eval_sval (Bctx ge' stk' f' sp rs0 m0) sv.
-Proof.
-  induction sv using sval_mut with (P0 := fun lsv => eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv)
-                                   (P1 := fun sm => eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm); simpl; auto.
-  + rewrite IHsv; clear IHsv. destruct (eval_list_sval _ _); auto.
-    rewrite IHsv0; clear IHsv0. destruct (eval_smem _ _); auto.
-    erewrite eval_operation_preserved; eauto.
-  + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto.
-    erewrite <- eval_addressing_preserved; eauto.
-    destruct (eval_addressing _ sp _ _); auto.
-    rewrite IHsv; auto.
-  + rewrite IHsv; clear IHsv. destruct (eval_sval _ _); auto.
-    rewrite IHsv0; auto.
-  + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto.
-    erewrite <- eval_addressing_preserved; eauto.
-    destruct (eval_addressing _ sp _ _); auto.
-    rewrite IHsv; clear IHsv. destruct (eval_smem _ _); auto.
-    rewrite IHsv1; auto.
-Qed.
-
-Lemma seval_builtin_arg_preserved m: forall bs varg,
-  seval_builtin_arg (Bctx ge stk f sp rs0 m0) m bs varg ->
-  seval_builtin_arg (Bctx ge' stk' f' sp rs0 m0) m bs varg.
-Proof.
-  induction 1; simpl.
-  all: try (constructor; auto).
-  - rewrite <- eval_sval_preserved. assumption.
-  - rewrite <- senv_symbol_address_preserved. assumption.
-  - rewrite senv_symbol_address_preserved. eapply seval_BA_addrglobal.
-Qed.
-
-Lemma seval_builtin_args_preserved m lbs vargs:
-  seval_builtin_args (Bctx ge stk f sp rs0 m0) m lbs vargs ->
-  seval_builtin_args (Bctx ge' stk' f' sp rs0 m0) m lbs vargs.
-Proof.
-  induction 1; constructor; eauto.
-  eapply seval_builtin_arg_preserved; auto.
-Qed.
-
-Lemma list_sval_eval_preserved lsv: 
-  eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv.
-Proof.
-  induction lsv; simpl; auto.
-  rewrite eval_sval_preserved. destruct (eval_sval _ _); auto.
-  rewrite IHlsv; auto.
-Qed.
-
-Lemma smem_eval_preserved sm: 
-  eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm.
-Proof.
-  induction sm; simpl; auto.
-  rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto.
-  erewrite <- eval_addressing_preserved; eauto.
-  destruct (eval_addressing _ sp _ _); auto.
-  rewrite IHsm; clear IHsm. destruct (eval_smem _ _); auto.
-  rewrite eval_sval_preserved; auto.
-Qed.
-
-Lemma seval_condition_preserved cond lsv sm:
-  seval_condition (Bctx ge stk f sp rs0 m0) cond lsv sm = seval_condition (Bctx ge' stk' f' sp rs0 m0) cond lsv sm.
-Proof.
-  unfold seval_condition.
-  rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto.
-  rewrite smem_eval_preserved; auto.
-Qed.
-
-End SymbValPreserved.
-
-
 (* Syntax and Semantics of symbolic internal states *)
 (* [si_pre] is a precondition on initial context *)
 Record sistate := { si_pre: iblock_exec_context -> Prop; si_sreg: reg -> sval; si_smem: smem }.
 
 (* Predicate on which (rs, m) is a possible final state after evaluating [st] on ((crs0 ctx), (cm0 ctx)) *)
-Definition sem_sistate ctx (st: sistate) (rs: regset) (m: mem): Prop :=
-  st.(si_pre) ctx
-  /\ eval_smem ctx st.(si_smem) = Some m
-  /\ forall (r:reg), eval_sval ctx (st.(si_sreg) r) = Some (rs#r).
-
-(* Remark that we need to reason modulo "extensionality" wrt Regmap.get about regsets.
-   And, nothing in their representation as (val * PTree.t val) enforces that
-     (forall r, rs1#r = rs2#r) -> rs1 = rs2
-*)
-Lemma sem_sistate_determ ctx st rs1 m1 rs2 m2:
-  sem_sistate ctx st rs1 m1 ->
-  sem_sistate ctx st rs2 m2 ->
-  (forall r, rs1#r = rs2#r) /\ m1 = m2.
-Proof.
-  intros (_&MEM1&REG1) (_&MEM2&REG2).
-  intuition try congruence.
-  generalize (REG1 r); rewrite REG2; congruence.
-Qed.
+Definition sem_sistate ctx (sis: sistate) (rs: regset) (m: mem): Prop :=
+  sis.(si_pre) ctx
+  /\ eval_smem ctx sis.(si_smem) = Some m
+  /\ forall (r:reg), eval_sval ctx (sis.(si_sreg) r) = Some (rs#r).
 
 (** * Symbolic execution of final step *)
 Definition sexec_final_sfv (i: final) (sis: sistate): sfval := 
@@ -580,10 +472,10 @@ Local Hint Constructors sem_sfval: core.
 
 Lemma sexec_final_svf_correct ctx i sis t rs m s:
   sem_sistate ctx sis rs m ->
-  final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s -> 
+  final_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s -> 
   sem_sfval ctx (sexec_final_sfv i sis) rs m t s.
 Proof.
-  intros (PRE&MEM&REG). 
+  intros (PRE&MEM&REG).
   destruct 1; subst; try_simplify_someHyps; simpl; intros; try autodestruct; eauto.
   + (* Bcall *) intros; eapply exec_Scall; auto.
     - destruct ros; simpl in * |- *; auto.
@@ -604,7 +496,7 @@ Local Hint Resolve seval_builtin_args_exact: core.
 Lemma sexec_final_svf_exact ctx i sis t rs m s:
   sem_sistate ctx sis rs m ->
   sem_sfval ctx (sexec_final_sfv i sis) rs m t s
-  -> final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s.
+  -> final_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s.
 Proof.
   intros (PRE&MEM&REG).
   destruct i; simpl; intros LAST; inv LAST; eauto.
@@ -626,7 +518,6 @@ Proof.
     congruence.
 Qed.
 
-
 (** * symbolic execution of basic instructions *)
 
 Definition sis_init : sistate := {| si_pre:= fun _ => True; si_sreg:= fun r => Sinput r; si_smem:= Sinit |}.
@@ -735,6 +626,76 @@ Proof.
   erewrite MEM; auto.
 Qed.
 
+(** * Compute sistate associated to final values *)
+Fixpoint transfer_sreg (inputs: list reg) (sreg: reg -> sval): reg -> sval :=
+  match inputs with
+  | nil => fun r => Sundef 
+  | r1::l => fun r => if Pos.eq_dec r r1 then sreg r1 else transfer_sreg l sreg r
+  end.
+
+Definition str_inputs (f:function) (tbl: list exit) (or:option reg) := transfer_sreg (Regset.elements (pre_inputs f tbl or)).
+
+Lemma str_inputs_correct ctx sis rs tbl or r:
+  (forall r : reg, eval_sval ctx (si_sreg sis r) = Some rs # r) ->
+  eval_sval ctx (str_inputs (cf ctx) tbl or (si_sreg sis) r) = Some (tr_inputs (cf ctx) tbl or rs) # r.
+Proof.
+  intros H.
+  unfold str_inputs, tr_inputs, transfer_regs.
+  induction (Regset.elements _) as [|x l]; simpl.
+  + rewrite Regmap.gi; auto.
+  + autodestruct; intros; subst.
+    * rewrite Regmap.gss; auto.
+    * rewrite Regmap.gso; eauto.
+Qed.
+
+Local Hint Resolve str_inputs_correct: core.
+
+Definition tr_sis f (fi: final) (sis: sistate) :=
+  {| si_pre := fun ctx => (sis.(si_pre) ctx /\ forall r, eval_sval ctx (sis.(si_sreg) r) <> None);
+     si_sreg := poly_tr str_inputs f fi sis.(si_sreg); 
+     si_smem := sis.(si_smem) |}.
+
+Definition sreg_eval ctx (sis: sistate) (r: reg): option val :=
+  eval_sval ctx (sis.(si_sreg) r).
+
+Lemma tr_sis_regs_correct_aux ctx fin sis rs m:
+  sem_sistate ctx sis rs m ->
+  (forall r, sreg_eval ctx (tr_sis (cf ctx) fin sis) r = Some (tr_regs (cf ctx) fin rs) # r).
+Proof.
+  Local Opaque str_inputs.
+  unfold sreg_eval; simpl. destruct 1 as (_ & _ & REG).
+  destruct fin; simpl; eauto.
+Qed.
+
+Lemma tr_sis_regs_correct ctx fin sis rs m:
+  sem_sistate ctx sis rs m ->
+  sem_sistate ctx (tr_sis (cf ctx) fin sis) (tr_regs (cf ctx) fin rs) m.
+Proof.
+  intros H.
+  generalize (tr_sis_regs_correct_aux _ fin _ _ _ H).
+  destruct H as (PRE & MEM & REG).
+  econstructor; simpl; intuition eauto || congruence.
+Qed.
+
+Definition poly_str {A} (tr: function -> list exit -> option reg -> A) f (svf: sfval): A := 
+  match svf with
+  | Sgoto pc => tr f [pc] None
+  | Scall _ _ _ res pc => tr f [pc] (Some res)
+  | Stailcall _ _ args => tr f [] None
+  | Sbuiltin _ _ res pc => tr f [pc] (reg_builtin_res res)
+  | Sreturn _ => tr f [] None
+  | Sjumptable _ tbl => tr f tbl None
+  end.
+
+Definition str_regs: function -> sfval -> regset -> regset :=
+  poly_str tr_inputs.
+
+Lemma str_tr_regs_equiv f fin sis:
+  str_regs f (sexec_final_sfv fin sis) = tr_regs f fin.
+Proof.
+  destruct fin; simpl; auto.
+Qed.
+
 (** * symbolic execution of blocks *)
 
 (* symbolic state *)
@@ -746,8 +707,8 @@ Inductive sstate :=
 
 (* transition (t,s) produced by a sstate in initial context ctx *)
 Inductive sem_sstate ctx t s: sstate -> Prop :=
-  | sem_Sfinal sis sfv rs m
-     (SIS: sem_sistate ctx sis rs m)
+  | sem_Sfinal sis sfv rs m 
+     (SIS: sem_sistate ctx sis (str_regs (cf ctx) sfv rs) m)
      (SFV: sem_sfval ctx sfv rs m t s)
      : sem_sstate ctx t s (Sfinal sis sfv)
   | sem_Scond b cond args sm ifso ifnot
@@ -768,9 +729,9 @@ pour représenter l'ensemble des chemins.
 
 *)
 
-Fixpoint sexec_rec ib sis (k: sistate -> sstate): sstate := 
+Fixpoint sexec_rec f ib sis (k: sistate -> sstate): sstate := 
   match ib with
-  | BF fin _ => Sfinal sis (sexec_final_sfv fin sis)
+  | BF fin => Sfinal (tr_sis f fin sis) (sexec_final_sfv fin sis)
   (* basic instructions *)
   | Bnop _ => k sis
   | Bop op args res _ => k (sexec_op op args res sis)
@@ -779,19 +740,19 @@ Fixpoint sexec_rec ib sis (k: sistate -> sstate): sstate :=
   | Bstore chunk addr args src _ => k (sexec_store chunk addr args src sis)
  (* composed instructions *)
   | Bseq ib1 ib2 =>
-      sexec_rec ib1 sis (fun sis2 => sexec_rec ib2 sis2 k) 
+      sexec_rec f ib1 sis (fun sis2 => sexec_rec f ib2 sis2 k) 
   | Bcond cond args ifso ifnot _ =>
       let args := list_sval_inj (List.map sis.(si_sreg) args) in
-      let ifso := sexec_rec ifso sis k in
-      let ifnot := sexec_rec ifnot sis k in
+      let ifso := sexec_rec f ifso sis k in
+      let ifnot := sexec_rec f ifnot sis k in
       Scond cond args sis.(si_smem) ifso ifnot
   end
   .
 
-Definition sexec ib := sexec_rec ib sis_init (fun _ => Sabort).
+Definition sexec f ib := sexec_rec f ib sis_init (fun _ => Sabort).
 
 Local Hint Constructors sem_sstate: core.
-Local Hint Resolve sexec_op_correct sexec_final_svf_correct 
+Local Hint Resolve sexec_op_correct sexec_final_svf_correct tr_sis_regs_correct_aux tr_sis_regs_correct
                    sexec_load_TRAP_correct sexec_store_correct sis_init_correct: core.
 
 Lemma sexec_rec_correct ctx t s ib rs m rs1 m1 ofin
@@ -799,131 +760,72 @@ Lemma sexec_rec_correct ctx t s ib rs m rs1 m1 ofin
   (SIS: sem_sistate ctx sis rs m)
   (CONT: match ofin with
          | None => forall sis', sem_sistate ctx sis' rs1 m1 -> sem_sstate ctx t s (k sis')
-         | Some fin => final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs1 m1 fin t s
+         | Some fin => final_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs1 m1 fin t s
          end),
-  sem_sstate ctx t s (sexec_rec ib sis k).
+  sem_sstate ctx t s (sexec_rec (cf ctx) ib sis k).
 Proof.
   induction ISTEP; simpl; try autodestruct; eauto.
+  (* final value *)
+  intros; econstructor; eauto.
+  rewrite str_tr_regs_equiv; eauto.
   (* condition *)
   all: intros;
     eapply sem_Scond; eauto; [
       erewrite seval_condition_eq; eauto |
-      replace (if b then sexec_rec ifso sis k else sexec_rec ifnot sis k) with (sexec_rec (if b then ifso else ifnot) sis k); 
+      replace (if b then sexec_rec (cf ctx) ifso sis k else sexec_rec (cf ctx) ifnot sis k) with (sexec_rec (cf ctx) (if b then ifso else ifnot) sis k); 
       try autodestruct; eauto ].
 Qed.
 
+
 (* NB: each concrete execution can be executed on the symbolic state (produced from [sexec]) 
   (sexec is a correct over-approximation)
 *)
 Theorem sexec_correct ctx ib t s: 
-  iblock_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s ->
-  sem_sstate ctx t s (sexec ib).
+  iblock_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s ->
+  sem_sstate ctx t s (sexec (cf ctx) ib).
 Proof.
   destruct 1 as (rs' & m' & fin & ISTEP & FSTEP).
   eapply sexec_rec_correct; simpl; eauto.
 Qed.
 
-
-(* TODO: déplacer les trucs sur equiv_stackframe -> regmap_setres_eq dans BTL! *)
-Inductive equiv_stackframe: stackframe -> stackframe -> Prop :=
-  | equiv_stackframe_intro res f sp pc rs1 rs2
-      (EQUIV: forall r : positive, rs1 !! r = rs2 !! r):
-      equiv_stackframe (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2)
-  .
-
-Inductive equiv_state: state -> state -> Prop :=
-  | State_equiv stack f sp pc rs1 m rs2
-     (EQUIV: forall r, rs1#r = rs2#r): 
-     equiv_state (State stack f sp pc rs1 m) (State stack f sp pc rs2 m)
-  | Call_equiv stk stk' f args m
-      (STACKS: list_forall2 equiv_stackframe stk stk'):
-      equiv_state (Callstate stk f args m) (Callstate stk' f args m)
-  | Return_equiv stk stk' v m
-      (STACKS: list_forall2 equiv_stackframe stk stk'):
-      equiv_state (Returnstate stk v m) (Returnstate stk' v m)
-  .
-
-Local Hint Constructors equiv_stackframe equiv_state: core.
-
-Lemma equiv_stackframe_refl stf: equiv_stackframe stf stf.
-Proof.
-  destruct stf; eauto.
-Qed.
-
-Lemma equiv_stack_refl stk: list_forall2 equiv_stackframe stk stk.
-Proof.
-  Local Hint Resolve equiv_stackframe_refl: core.
-  induction stk; simpl; constructor; auto.
-Qed.
-
-Lemma equiv_state_refl s: equiv_state s s.
-Proof.
-  Local Hint Resolve equiv_stack_refl: core.
-  induction s; simpl; constructor; auto.
-Qed.
-
-Lemma equiv_stackframe_trans stf1 stf2 stf3:
-  equiv_stackframe stf1 stf2 -> equiv_stackframe stf2 stf3 -> equiv_stackframe stf1 stf3.
-Proof.
-  destruct 1; intros EQ; inv EQ; try econstructor; eauto.
-  intros; eapply eq_trans; eauto.
-Qed.
-
-Lemma equiv_stack_trans stk1 stk2:
-  list_forall2 equiv_stackframe stk1 stk2 -> 
-  forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> 
-  list_forall2 equiv_stackframe stk1 stk3.
-Proof.
-  Local Hint Resolve equiv_stackframe_trans: core.
-  induction 1; intros stk3 EQ; inv EQ; econstructor; eauto.
-Qed.
-
-Lemma equiv_state_trans s1 s2 s3: equiv_state s1 s2 -> equiv_state s2 s3 -> equiv_state s1 s3.
+(* Remark that we want to reason modulo "extensionality" wrt Regmap.get about regsets.
+   And, nothing in their representation as (val * PTree.t val) enforces that
+     (forall r, rs1#r = rs2#r) -> rs1 = rs2
+*)
+Lemma sem_sistate_tr_sis_determ ctx sis rs1 m1 fi rs2 m2:
+  sem_sistate ctx sis rs1 m1 ->
+  sem_sistate ctx (tr_sis (cf ctx) fi sis) rs2 m2 ->
+     (forall r, rs2#r = (tr_regs (cf ctx) fi rs1)#r) 
+  /\ m1 = m2.
 Proof.
-  Local Hint Resolve equiv_stack_trans: core.
-  destruct 1; intros EQ; inv EQ; econstructor; eauto.
-  intros; eapply eq_trans; eauto.
+  intros H1 H2.
+  lapply (tr_sis_regs_correct_aux ctx fi sis rs1 m1); eauto.
+  unfold sreg_eval; intros X.
+  destruct H1 as (_&MEM1&REG1).
+  destruct H2 as (_&MEM2&REG2); simpl in *.
+  intuition try congruence.
+  cut (Some rs2 # r = Some (tr_regs (cf ctx) fi rs1)#r).
+  { congruence. }
+  rewrite <- REG2, X. auto.
 Qed.
 
-Lemma regmap_setres_eq (rs rs': regset) res vres:
-  (forall r, rs # r = rs' # r) ->
-  forall r, (regmap_setres res vres rs) # r = (regmap_setres res vres rs') # r.
-Proof.
-  intros RSEQ r. destruct res; simpl; try congruence.
-  destruct (peq x r).
-  - subst. repeat (rewrite Regmap.gss). reflexivity.
-  - repeat (rewrite Regmap.gso); auto.
-Qed.
+Local Hint Constructors equiv_stackframe list_forall2: core.
+Local Hint Resolve regmap_setres_eq equiv_stack_refl equiv_stack_refl: core.
 
 Lemma sem_sfval_equiv rs1 rs2 ctx sfv m t s:
   sem_sfval ctx sfv rs1 m t s ->
-  (forall r, rs1#r = rs2#r) -> 
-  exists s', equiv_state s s' /\  sem_sfval ctx sfv rs2 m t s'.
-Proof. 
-  Local Hint Resolve equiv_stack_refl equiv_state_refl regmap_setres_eq: core.
-  Local Hint Constructors sem_sfval: core.
-  destruct 1; eexists; split; econstructor; eauto.
-  econstructor; eauto.
+  (forall r, (str_regs (cf ctx) sfv rs1)#r = (str_regs (cf ctx) sfv rs2)#r) ->
+  exists s', sem_sfval ctx sfv rs2 m t s' /\ equiv_state s s'.
+Proof.
+  unfold str_regs.
+  destruct 1; simpl in *; intros; subst; eexists; split; econstructor; eauto; try congruence.
 Qed.
 
-Local Hint Resolve sexec_final_svf_exact: core.
-
 Definition abort_sistate ctx (sis: sistate): Prop :=
   ~(sis.(si_pre) ctx)
   \/ eval_smem ctx sis.(si_smem) = None
   \/ exists (r: reg), eval_sval ctx (sis.(si_sreg) r) = None.
 
-Lemma sem_sistate_exclude_abort ctx sis rs m:
-  sem_sistate ctx sis rs m ->
-  abort_sistate ctx sis ->
-  False.
-Proof.
-  intros SIS ABORT. inv SIS. destruct H0 as (H0 & H0').
-  inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; congruence.
-Qed.
-
-Local Hint Resolve sem_sistate_exclude_abort: core.
-
 Lemma set_sreg_preserves_abort ctx sv dst sis:
   abort_sistate ctx sis ->
   abort_sistate ctx (set_sreg dst sv sis).
@@ -963,11 +865,20 @@ Proof.
   intros; eapply set_smem_preserves_abort; eauto.
 Qed.
 
+Lemma sem_sistate_tr_sis_exclude_abort ctx sis fi rs m:
+  sem_sistate ctx (tr_sis (cf ctx) fi sis) rs m ->
+  abort_sistate ctx sis ->
+  False.
+Proof.
+  intros ((PRE1 & PRE2) & MEM & REG); simpl in *.
+  intros [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; try congruence.
+Qed.
+
 Local Hint Resolve sexec_op_preserves_abort sexec_load_preserves_abort
-  sexec_store_preserves_abort: core.
+  sexec_store_preserves_abort sem_sistate_tr_sis_exclude_abort: core.
 
 Lemma sexec_exclude_abort ctx ib t s1: forall sis k
-  (SEXEC: sem_sstate ctx t s1 (sexec_rec ib sis k))
+  (SEXEC: sem_sstate ctx t s1 (sexec_rec (cf ctx) ib sis k))
   (CONT: forall sis', sem_sstate ctx t s1 (k sis') -> (abort_sistate ctx sis') -> False)
   (ABORT: abort_sistate ctx sis),
   False.
@@ -1039,17 +950,17 @@ Proof.
   intros; rewrite REG; autodestruct; try_simplify_someHyps.
 Qed.
 
-Local Hint Resolve sexec_op_abort sexec_load_TRAP_abort sexec_store_abort: core.
+Local Hint Resolve sexec_op_abort sexec_load_TRAP_abort sexec_store_abort sexec_final_svf_exact: core.
 
 Lemma sexec_rec_exact ctx ib t s1: forall sis k
-  (SEXEC: sem_sstate ctx t s1 (sexec_rec ib sis k))
+  (SEXEC: sem_sstate ctx t s1 (sexec_rec (cf ctx) ib sis k))
   rs m
   (SIS: sem_sistate ctx sis rs m)
   (CONT: forall sis', sem_sstate ctx t s1 (k sis') -> (abort_sistate ctx sis') -> False)
   ,
      match iblock_istep_run (cge ctx) (csp ctx) ib rs m with
      | Some (out rs' m' (Some fin)) =>
-        exists s2, final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs' m' fin t s2 /\ equiv_state s1 s2
+        exists s2, final_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs' m' fin t s2 /\ equiv_state s1 s2
      | Some (out rs' m' None) => exists sis', (sem_sstate ctx t s1 (k sis')) /\ (sem_sistate ctx sis' rs' m')
      | None => False
      end.
@@ -1057,11 +968,11 @@ Proof.
   induction ib; simpl; intros; eauto.
   - (* final *)
     inv SEXEC.
-    exploit (sem_sistate_determ ctx sis rs m rs0 m0); eauto.
+    exploit (sem_sistate_tr_sis_determ ctx sis rs m fi); eauto.
     intros (REG&MEM); subst.
     exploit (sem_sfval_equiv rs0 rs); eauto.
-    intros (s2 & EQUIV & SFV').
-    eexists; split; eauto.
+    * intros; rewrite REG, str_tr_regs_equiv; auto.
+    * intros (s2 & EQUIV & SFV'); eauto.
   - (* Bop *) autodestruct; eauto.
   - destruct trap; [| inv SEXEC ].
     repeat autodestruct; eauto.
@@ -1094,8 +1005,8 @@ Qed.
   (sexec is exact).
 *)
 Theorem sexec_exact ctx ib t s1: 
-  sem_sstate ctx t s1 (sexec ib) ->
-  exists s2, iblock_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s2
+  sem_sstate ctx t s1 (sexec (cf ctx) ib) ->
+  exists s2, iblock_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s2
              /\ equiv_state s1 s2.
 Proof.
   intros; exploit sexec_rec_exact; eauto.
@@ -1109,3 +1020,141 @@ Proof.
     inversion SEXEC.
 Qed.
 
+(** * High-Level specification of the symbolic simulation test as predicate [symbolic_simu] *)
+
+Record simu_proof_context := Sctx {
+   sge1: BTL.genv;
+   sge2: BTL.genv;
+   sge_match: forall s, Genv.find_symbol sge1 s = Genv.find_symbol sge2 s;
+   sstk1: list BTL.stackframe;
+   sstk2: list BTL.stackframe;
+   sstk_equiv: list_forall2 equiv_stackframe sstk1 sstk2;
+   sf1: BTL.function;
+   sf2: BTL.function;
+   ssp: val;
+   srs0: regset; 
+   sm0: mem
+}.
+
+Definition bctx1 (ctx: simu_proof_context):= Bctx ctx.(sge1) ctx.(sstk1) ctx.(sf1) ctx.(ssp) ctx.(srs0) ctx.(sm0).
+Definition bctx2 (ctx: simu_proof_context):= Bctx ctx.(sge2) ctx.(sstk2) ctx.(sf2) ctx.(ssp) ctx.(srs0) ctx.(sm0).
+
+Definition sstate_simu (ctx: simu_proof_context) (st1 st2: sstate) :=
+  forall t s1, sem_sstate (bctx1 ctx) t s1 st1 ->
+  exists s2, sem_sstate (bctx2 ctx) t s2 st2 /\ equiv_state s1 s2.
+
+Definition symbolic_simu ctx ib1 ib2: Prop := sstate_simu ctx (sexec (sf1 ctx) ib1) (sexec (sf2 ctx) ib2).
+
+Theorem symbolic_simu_correct ctx ib1 ib2:
+  symbolic_simu ctx ib1 ib2 ->
+  forall t s1, iblock_step tr_inputs (sge1 ctx) (sstk1 ctx) (sf1 ctx) (ssp ctx) (srs0 ctx) (sm0 ctx) ib1 t s1 ->
+  exists s2, iblock_step tr_inputs (sge2 ctx) (sstk2 ctx) (sf2 ctx) (ssp ctx) (srs0 ctx) (sm0 ctx) ib2 t s2 /\ equiv_state s1 s2.
+Proof.
+  unfold symbolic_simu, sstate_simu.
+  intros SIMU t s1 STEP1.
+  exploit (sexec_correct (bctx1 ctx)); simpl; eauto.
+  intros; exploit SIMU; eauto.
+  intros (s2 & SEM1 & EQ1).
+  exploit (sexec_exact (bctx2 ctx)); simpl; eauto.
+  intros (s3 & STEP2 & EQ2).
+  clear STEP1; eexists; split; eauto.
+  eapply equiv_state_trans; eauto.
+Qed.
+
+(** * Preservation properties *)
+
+Section SymbValPreserved.
+
+Variable ge ge': BTL.genv.
+
+Hypothesis symbols_preserved_BTL: forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s.
+
+Hypothesis senv_preserved_BTL: Senv.equiv ge ge'.
+
+Lemma senv_find_symbol_preserved id:
+  Senv.find_symbol ge id = Senv.find_symbol ge' id.
+Proof.
+  destruct senv_preserved_BTL as (A & B & C). congruence.
+Qed.
+
+Lemma senv_symbol_address_preserved id ofs:
+  Senv.symbol_address ge id ofs = Senv.symbol_address ge' id ofs.
+Proof.
+  unfold Senv.symbol_address. rewrite senv_find_symbol_preserved.
+  reflexivity.
+Qed.
+
+Variable stk stk': list stackframe.
+Variable f f': function.
+Variable sp: val.
+Variable rs0: regset.
+Variable m0: mem.
+
+Lemma eval_sval_preserved sv:
+  eval_sval (Bctx ge stk f sp rs0 m0) sv = eval_sval (Bctx ge' stk' f' sp rs0 m0) sv.
+Proof.
+  induction sv using sval_mut with (P0 := fun lsv => eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv)
+                                   (P1 := fun sm => eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm); simpl; auto.
+  + rewrite IHsv; clear IHsv. destruct (eval_list_sval _ _); auto.
+    rewrite IHsv0; clear IHsv0. destruct (eval_smem _ _); auto.
+    erewrite eval_operation_preserved; eauto.
+  + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto.
+    erewrite <- eval_addressing_preserved; eauto.
+    destruct (eval_addressing _ sp _ _); auto.
+    rewrite IHsv; auto.
+  + rewrite IHsv; clear IHsv. destruct (eval_sval _ _); auto.
+    rewrite IHsv0; auto.
+  + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto.
+    erewrite <- eval_addressing_preserved; eauto.
+    destruct (eval_addressing _ sp _ _); auto.
+    rewrite IHsv; clear IHsv. destruct (eval_smem _ _); auto.
+    rewrite IHsv1; auto.
+Qed.
+
+Lemma seval_builtin_arg_preserved m: forall bs varg,
+  seval_builtin_arg (Bctx ge stk f sp rs0 m0) m bs varg ->
+  seval_builtin_arg (Bctx ge' stk' f' sp rs0 m0) m bs varg.
+Proof.
+  induction 1; simpl.
+  all: try (constructor; auto).
+  - rewrite <- eval_sval_preserved. assumption.
+  - rewrite <- senv_symbol_address_preserved. assumption.
+  - rewrite senv_symbol_address_preserved. eapply seval_BA_addrglobal.
+Qed.
+
+Lemma seval_builtin_args_preserved m lbs vargs:
+  seval_builtin_args (Bctx ge stk f sp rs0 m0) m lbs vargs ->
+  seval_builtin_args (Bctx ge' stk' f' sp rs0 m0) m lbs vargs.
+Proof.
+  induction 1; constructor; eauto.
+  eapply seval_builtin_arg_preserved; auto.
+Qed.
+
+Lemma list_sval_eval_preserved lsv: 
+  eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv.
+Proof.
+  induction lsv; simpl; auto.
+  rewrite eval_sval_preserved. destruct (eval_sval _ _); auto.
+  rewrite IHlsv; auto.
+Qed.
+
+Lemma smem_eval_preserved sm: 
+  eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm.
+Proof.
+  induction sm; simpl; auto.
+  rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto.
+  erewrite <- eval_addressing_preserved; eauto.
+  destruct (eval_addressing _ sp _ _); auto.
+  rewrite IHsm; clear IHsm. destruct (eval_smem _ _); auto.
+  rewrite eval_sval_preserved; auto.
+Qed.
+
+Lemma seval_condition_preserved cond lsv sm:
+  seval_condition (Bctx ge stk f sp rs0 m0) cond lsv sm = seval_condition (Bctx ge' stk' f' sp rs0 m0) cond lsv sm.
+Proof.
+  unfold seval_condition.
+  rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto.
+  rewrite smem_eval_preserved; auto.
+Qed.
+
+End SymbValPreserved.
diff --git a/scheduling/BTLroadmap.md b/scheduling/BTLroadmap.md
index 39ea12d0..0cbcd7d6 100644
--- a/scheduling/BTLroadmap.md
+++ b/scheduling/BTLroadmap.md
@@ -3,8 +3,8 @@
 BTL aims to be an IR dedicated to defensive certification of middle-end optimizations (before register allocation).
 It provides a CFG of "loop-free" blocks, where each block is run in one step emitting at most a single observational event.
 The "local" optimizations (i.e. preserving "locally" the semantics of such blocks) would be checked by symbolic execution with rewriting rules.
-The only info required from oracles: a "dupmap" mapping block entries.
-In contrast, the "global" optimizations would require some invariants annotations at block entry (provided by oracles).
+The main info required from oracles: a "dupmap" mapping block entries (and maybe strategies for controlling path explosion during symbolic execution -- see below).
+Moreover, the "global" optimizations would require some invariants annotations at block entry (provided by oracles).
 
 Examples of optimizations that we aim to support:
 
@@ -16,6 +16,9 @@ Examples of optimizations that we aim to support:
 
 We sketch below the various kinds of supported optimizations in development order...
 
+Remark that we may port most of the current optimizations from RTL to BTL (even maybe, register allocation).
+However, RTL will probably remain useful for "fine-tuned" duplication that crosses block boundaries (e.g. Duplicate module).
+
 ## Introduction
 
 En gros la syntaxe d'un bloc BTL est définie par:
@@ -83,7 +86,7 @@ coder la "simulation modulo liveness" dans une "simulation
 less_undef".  Ça peut rendre le cadre du test de simulation plus
 simple et plus général.
 
-**Idée** à côté de la sémantique "à la RTL" pour BTL, on pourrait
+**Idée_Informelle** à côté de la sémantique "à la RTL" pour BTL, on pourrait
 définir une nouvelle sémantique (basée sur la même sémantique à grand
 pas dans les blocs), où c'est juste "l'entrée dans un bloc" qui change
 de sémantique. Intuitivement, cette nouvelle sémantique considèrerait
@@ -102,30 +105,49 @@ totales) dans BTL.  Pour l'encodage de SSA, il suffira d'étendre le
 mécanisme d'initialisation du "rs0" d'un bloc avec un passage de
 paramètres.
 
-En fait, pour le test d'exécution symbolique, il semble plus simple de mettre les Vundef à la fin de la transition...
+**REM** pour le test d'exécution symbolique, il semble plus adapté de
+mettre les Vundef juste à la fin de la transition (précédente) plutôt
+qu'au début (de la suivante).  On pourrait aussi faire les deux (dans le détail, ça ne ferait pas exactement deux fois la même chose: 
+par exemple, quand on sort sur un call ou un builtin, le résultat du call/builtin n'est jamais dans le liveout puisqu'il va être écrasé de toute façon pendant la transition, 
+mais il peut être -- ou pas -- dans le livein de la transition suivante dans ce même bloc).
+
+Avoir une initialisation à Vundef en début de bloc permettrait de
+faire une analyse des expressions mal initialisées - par exemple à
+partir du bloc d'entrée de la fonction. Ça semble complémentaire de
+l'analyse de "liveout". Mais utilisable uniquement dans le cadre d'une
+combinaison "exécution symbolique"+"value analysis" (donc pas tout de suite).
+
+Donc, dans un premier temps, la "functional semantics" encode/abstrait la notion de "liveout" pour le test d'exécution symbolique. 
+Les définitions des deux sémantiques (symbolique et "functional") se font donc en simultanée.
 
-**IMPLEM PLAN**
+**STATUS**
+
+1. See [BTL.fsem]  (Pour l'instant CFGSemantics => BTL.semantics et FunctionalSemantics => BTL.fsem)
+
+**TODO**
 
-1. définir the "functional semantics" of BTL.
-2. prouver la simulation BTL.FunctionalSemantics -> BTL.CFGSemantics (facile normalement: c'est du "less_undef lockstep").
-3. implémenter une passe BTL.CFGSemantics -> BTL.FunctionalSemantics.
+1. prouver la simulation BTL.FunctionalSemantics -> BTL.CFGSemantics (facile normalement: c'est du "less_undef lockstep").
+2. implémenter une passe BTL.CFGSemantics -> BTL.FunctionalSemantics.
    en gros: on implémente un vérificateur des infos de liveness.
    c'est la correction du "input_regs" qui garantit que la simulation est correct.
    La preuve devrait normalement être très similaire à RTLpathLivegenproof. 
 
-
 ## "Basic" symbolic execution / symbolic simulation
 
-We will implement a "basic" (e.g without rewriting rules) "less_undef" simulation test for BTL.FunctionalSemantics.
+We will implement a "basic" (e.g without rewriting rules) simulation test for BTL.FunctionalSemantics. 
+Dans un premier temps: pas besoin de "less_undef lockstep", on peut se contenter de tester l'égalité des registres de chaque côté: les registres hors liveout seront égaux à Vundef de chaque côté.
 
-**IMPLEM NOTE**
+**STATUS**
 
-- use Continuation Passing Style for an easy recursive generation of "all execution paths".
+- BTL_SEtheory: DONE
+ - model of symbolic execution in Continuation-Passing Style for BTL with "correctness" and "completness" thms wrt BTL.fsem
+ - high-level specification [sstate_simu] of "symbolic simulation" over iblocks (wrt BTL.fsem).
 
-**CURRENT STATUS**
+**TODO**
 
-- model of symbolic execution in Continuation-Passing Style for BTL with "correctness" and "completness" thms.
-- next step: high-level specification of "symbolic simulation" + preservation proof w.r.t  BTL.FunctionalSemantics.
+1. Verif du "scheduling" (aka analogue de RTLpathScheduler & RTLSchedulerproof).
+2. raffinement intermediaire avant le hash-consing ? ça permettrait de décomposer encore davantage la preuve ?
+Y a-t-il un moyen simple de faire le tests d'inclusion des fails potentiels à coût linéaire plutôt que quadratique (contrairement à RTLpath) ?
 
 ## Port of RTLpath optimizations to BTL
 
@@ -327,9 +349,13 @@ Au final, on obtient deux BDD identiques sur cet exemple (sans explosion combina
 
 ## Invariants at block entry
 
-Extends the symbolic simulation test to support invariants at block entry, including global renaming of registers.
+Extends the symbolic simulation test to support invariants at block entry, including global renaming of registers. Case-study: support of strength-reduction.
+
+**IDEAS**
 
-Case-study: support of strength-reduction.
+- En pratique, il faudra peut-être affiner la sémantique symbolique des "jumptable" pour que ça marche bien: avec un "état symbolique interne" par sortie (au lieu d'un état symbolique interne global dans la sémantique actuelle). Ça semble nécessaire pour gérer les invariants de renommage par exemple: en effet, il y a potentiellement un renommage différent pour chaque sortie.
+
+- Est-ce qu'il ne faut pas envisager une combinaison "execution symbolique + value analysis" ? La value analysis pourrait se faire directement sur la sémantique symbolique (donc en sortie de l'exécution symbolique), avec un mécanisme de mémoïsation (pour éviter les calculs redondants dus à la duplication de termes dans l'état symbolique). Intérêts: la value analysis ne se ferait que sur les registres live. Elle serait aussi plus sans doute un peu simple (par exemple inutile d'avoir un "join": on peut se contenter d'un test d'inclusion sur chacun des chemins).
 
 ## Support of SSA-optimizations
 
@@ -339,6 +365,4 @@ This should enable to represent SSA-forms in BTL IR, more or less like in MLIR.
 
 ## Alias analysis in the symbolic simulation
 
-A REGARDER [papier pointé par Justus](https://vbpf.github.io/assets/prevail-paper.pdf)
-
-
+A REGARDER [papier pointé par Justus](https://vbpf.github.io/assets/prevail-paper.pdf) 
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v
index 7b62a844..46f360c5 100644
--- a/scheduling/BTLtoRTLproof.v
+++ b/scheduling/BTLtoRTLproof.v
@@ -303,7 +303,7 @@ Qed.
 Lemma final_simu_except_goto sp dupmap stack stack' f f' rs1 m1 pc1 fin t s
   (STACKS : list_forall2 match_stackframes stack stack')
   (TRANSF : match_function dupmap f f')
-  (FS : final_step ge stack f sp rs1 m1 fin t s)
+  (FS : final_step tid ge stack f sp rs1 m1 fin t s)
   (i : instruction)
   (ATpc1 : (RTL.fn_code f') ! pc1 = Some i)
   (MF : match_final_inst dupmap fin i)
@@ -349,7 +349,7 @@ Lemma iblock_step_simulation sp dupmap stack stack' f f' ib rs0 m0 rs1 m1 pc0 fi
   (TRANSF: match_function dupmap f f')
   (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 (Some fin))
   (MIB : match_iblock dupmap (RTL.fn_code f') true pc0 ib None)
-  (FS : final_step ge stack f sp rs1 m1 fin t s)
+  (FS : final_step tid ge stack f sp rs1 m1 fin t s)
   : exists s', plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) t s' /\ match_states s s'.
 Proof.
   intros; exploit iblock_istep_simulation; eauto.
@@ -370,7 +370,7 @@ Proof.
 Qed.
 
 Theorem plus_simulation s1 t s1':
-  step ge s1 t s1' ->
+  step tid ge s1 t s1' ->
   forall s2 (MS: match_states s1 s2),
   exists s2',
      plus RTL.step tge s2 t s2'
@@ -401,8 +401,8 @@ Proof.
     + inv H1. econstructor; eauto.
 Qed.
 
-Theorem transf_program_correct:
-  forward_simulation (semantics prog) (RTL.semantics tprog).
+Theorem transf_program_correct_cfg:
+  forward_simulation (BTL.cfgsem prog) (RTL.semantics tprog).
 Proof.
   eapply forward_simulation_plus with match_states.
   - eapply senv_preserved.
@@ -411,4 +411,12 @@ Proof.
   - eapply plus_simulation.
 Qed.
 
+Theorem transf_program_correct:
+  forward_simulation (BTL.fsem prog) (RTL.semantics tprog).
+Proof.
+  eapply compose_forward_simulations.
+  - eapply fsem2cfgsem.
+  - eapply transf_program_correct_cfg.
+Qed.
+
 End RTL_SIMULATES_BTL.
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index f561ee7a..7d83931b 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -538,7 +538,7 @@ Lemma match_strong_state_simu
   (MSS2 : match_strong_state dupmap st st' f f' sp rs2 m2 rs0 m0 pcB0 pcR0 pcR2 ib2 ib0 false)
   (MES  : measure ib2 < n)
   : exists (oib' : option iblock),
-      (exists s2', step tge (State st' f' sp pcB0 rs0 m0) t s2'
+      (exists s2', step tid tge (State st' f' sp pcB0 rs0 m0) E0 s2'
           /\ match_states oib' s1' s2')
           \/ (omeasure oib' < n /\ t=E0
           /\ match_states oib' s1' (State st' f' sp pcB0 rs0 m0)).
@@ -566,7 +566,7 @@ Lemma opt_simu_intro
   (MSTRONG : match_strong_state dupmap st st' f f' sp rs m rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst)
   (NGOTO : is_goto ib = false)
   : exists (oib' : option iblock),
-     (exists s2', step tge (State st' f' sp pcB0 rs0 m0) t s2' /\ match_states oib' s1' s2')
+     (exists s2', step tid tge (State st' f' sp pcB0 rs0 m0) t s2' /\ match_states oib' s1' s2')
   \/ (omeasure oib' < omeasure (Some ib) /\ t=E0 /\ match_states oib' s1' (State st' f' sp pcB0 rs0 m0)).
 Proof.
   inv MSTRONG; subst. inv MIB.
@@ -699,7 +699,7 @@ Theorem opt_simu s1 t s1' oib s2:
  RTL.step ge s1 t s1' ->
  match_states oib s1 s2 ->
  exists (oib' : option iblock),
-     (exists s2', step tge s2 t s2' /\ match_states oib' s1' s2')
+     (exists s2', step tid tge s2 t s2' /\ match_states oib' s1' s2')
   \/ (omeasure oib' < omeasure oib /\ t=E0 /\ match_states oib' s1' s2) 
  .
 Proof.
@@ -738,9 +738,9 @@ Qed.
 Local Hint Resolve plus_one star_refl: core.
 
 Theorem transf_program_correct:
-  forward_simulation (RTL.semantics prog) (BTL.semantics tprog).
+  forward_simulation (RTL.semantics prog) (BTL.cfgsem tprog).
 Proof.
-  eapply (Forward_simulation (L1:=RTL.semantics prog) (L2:=semantics tprog) (ltof _ omeasure) match_states).
+  eapply (Forward_simulation (L1:=RTL.semantics prog) (L2:=cfgsem tprog) (ltof _ omeasure) match_states).
   constructor 1; simpl.
   - apply well_founded_ltof.
   - eapply transf_initial_states.