(** We introduce a data-structure extending the RTL CFG into a control-flow graph over "traces" (in the sense of "trace-scheduling")
    Here, we use the word "path" instead of "trace" because "trace" has already a meaning in CompCert: 
      a "path" is simply a list of successive nodes in the CFG (modulo some additional wellformness conditions).

    Actually, we extend syntactically the notion of RTL programs with a structure of "path_map": 
    this gives an alternative view of the CFG -- where "nodes" are paths instead of simple instructions.
    Our wellformness condition on paths express that:
      - the CFG on paths is wellformed: any successor of a given path points to another path (possibly the same).
      - execution of a paths only emit single events.

    We represent each path only by a natural: the number of nodes in the path. These nodes are recovered from a static notion of "default successor".
    This notion of path is thus incomplete. For example, if a path contains a whole loop (and for example, unrools it several times), 
    then this loop must be a suffix of the path.

    However: it is sufficient in order to represent superblocks (each superblock being represented as a path).
    A superblock decomposition of the CFG exactly corresponds to the case where each node is in at most one path.

    Our goal is to provide two bisimulable semantics:
      - one is simply the RTL semantics
      - the other is based on a notion of "path-step": each path is executed in a single step.

    Remark that all analyses on RTL programs should thus be appliable for "free" also for RTLpath programs !
*)

Require Import Coqlib Maps.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import Op Registers.
Require Import RTL Linking.
Require Import Lia.

Notation "'SOME' X <- A 'IN' B" := (match A with Some X => B | None => None end)
         (at level 200, X ident, A at level 100, B at level 200)
         : option_monad_scope.

Notation "'ASSERT' A 'IN' B" := (if A then B else None)
         (at level 200, A at level 100, B at level 200)
         : option_monad_scope.

Local Open Scope option_monad_scope.

(** * Syntax of RTLpath programs *)

(** Internal instruction = instruction with a default successor in a path. *)

Definition default_succ (i: instruction): option node :=
  match i with
  | Inop s => Some s
  | Iop op args res s => Some s
  | Iload _ chunk addr args dst s => Some s
  | Istore chunk addr args src s => Some s
  | Icond cond args ifso ifnot _ => Some ifnot
  | _ => None (* TODO: we could choose a successor for jumptable ? *)
  end.

Definition early_exit (i: instruction): option node := (* FIXME: for jumptable, replace [node] by [list node] *)
  match i with
  | Icond cond args ifso ifnot _ => Some ifso
  | _ => None
  end.

(** Our notion of path. 

    We do not formally require that the set of path is a partition of the CFG.
    path may have intersections !

    Moreover, we do not formally require that path have a single entry-point (a superblock structure) 

    But, in practice, these properties are probably necessary in order to ensure the success of dynamic verification of scheduling.

    Here: we only require that each exit-point of a path is the entry-point of a path
     (and that internal node of a path are internal instructions)
*)


(* By convention, we say that node [n] is the entry-point of a path if it is a key of the path_map.

   Such a path of entry [n] is defined from a natural [path] representing the [path] default-successors of [n].

   Remark: a path can loop several times in the CFG.

*)

Record path_info := { 
    psize: nat; (* number minus 1 of instructions in the path *)
    input_regs: Regset.t;
    (** Registers that are used (as input_regs) by the "fallthrough successors" of the path *)
    pre_output_regs: Regset.t;
    (** This field is not used by the verificator, but is helpful for the superblock scheduler *)
    output_regs: Regset.t 
}.

Definition path_map: Type := PTree.t path_info.

Definition path_entry (pm: path_map) (n: node): Prop := pm!n <> None.

Inductive wellformed_path (c:code) (pm: path_map): nat -> node -> Prop :=
  | wf_last_node i pc:
      c!pc = Some i ->
      (forall n, List.In n (successors_instr i) -> path_entry (*c*) pm n) ->
      wellformed_path c pm 0 pc
  | wf_internal_node path i pc pc':
      c!pc = Some i ->
      default_succ i = Some pc' ->
      (forall n, early_exit i = Some n -> path_entry (*c*) pm n) ->
      wellformed_path c pm path pc' ->
      wellformed_path c pm (S path) pc.

(* all paths defined from the path_map are wellformed *)
Definition wellformed_path_map (c:code) (pm: path_map): Prop :=
  forall n path, pm!n = Some path -> wellformed_path c pm path.(psize) n.

(** We "extend" the notion of RTL program with the additional structure for path.

    There is thus a trivial "forgetful functor" from RTLpath programs to RTL ones.
*)

Record function : Type := 
 { fn_RTL:> RTL.function;
   fn_path: path_map;
   (* condition 1 below: the entry-point of the code is an entry-point of a path *) 
   fn_entry_point_wf: path_entry fn_path fn_RTL.(fn_entrypoint); 
   (* condition 2 below: the path_map is well-formed *) 
   fn_path_wf: wellformed_path_map fn_RTL.(fn_code) fn_path
 }.

Definition fundef := AST.fundef function.
Definition program := AST.program fundef unit.
Definition genv := Genv.t fundef unit.

Definition fundef_RTL (fu: fundef) : RTL.fundef := 
  match fu with
  | Internal f => Internal f.(fn_RTL)
  | External ef => External ef
  end.
Coercion fundef_RTL: fundef >-> RTL.fundef.

Definition transf_program (p: program) : RTL.program := transform_program fundef_RTL p.
Coercion transf_program: program >-> RTL.program.

(** * Path-step semantics of RTLpath programs *)

(* Semantics of internal instructions (mimicking RTL semantics) *)

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 (mk_istate true pc' rs m)
  | Iop op args res pc' =>
      SOME v <- eval_operation ge sp op rs##args m IN
      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 (mk_istate true pc' (rs#dst <- v) m)
  | Iload NOTRAP chunk addr args dst pc' =>
      let default_state := mk_istate true pc' rs#dst <- Vundef 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 (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 (mk_istate true pc' rs m')
  | Icond cond args ifso ifnot _ =>
      SOME b <- eval_condition cond rs##args m IN
      Some (mk_istate (negb b) (if b then ifso else ifnot) rs m)
  | _ => None (* TODO jumptable ? *)
  end.

(** Execution of a path in a single step *)

(* 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 (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 (icontinue st) then
      isteps ge p f sp (irs st) (imem st) (ipc st)
    else
      Some st
  end.

Definition find_function (pge: genv) (ros: reg + ident) (rs: regset) : option fundef :=
  match ros with
  | inl r => Genv.find_funct pge rs#r
  | inr symb =>
      match Genv.find_symbol pge symb with
      | None => None
      | Some b => Genv.find_funct_ptr pge b
      end
  end.

Inductive stackframe : Type :=
  | Stackframe
             (res: reg)            (**r where to store the result *)
             (f: function)         (**r calling function *)
             (sp: val)             (**r stack pointer in calling function *)
             (pc: node)            (**r program point in calling function *)
             (rs: regset)          (**r register state in calling function *)
  .

Definition stf_RTL (st: stackframe): RTL.stackframe :=
  match st with
  | Stackframe res f sp pc rs => RTL.Stackframe res f sp pc rs
  end.

Fixpoint stack_RTL (stack: list stackframe): list RTL.stackframe :=
  match stack with
  | nil => nil
  | cons stf stack' => cons (stf_RTL stf) (stack_RTL stack')
  end.

Inductive state : Type :=
  | State
             (stack: list stackframe) (**r call stack *)
             (f: function)            (**r current function *)
             (sp: val)                (**r stack pointer *)
             (pc: node)               (**r current program point in [c] *)
             (rs: regset)             (**r register state *)
             (m: mem)                 (**r memory state *)
  | Callstate
             (stack: list stackframe) (**r call stack *)
             (f: fundef)              (**r function to call *)
             (args: list val)         (**r arguments to the call *)
             (m: mem)                 (**r memory state *)
  | Returnstate
             (stack: list stackframe) (**r call stack *)
             (v: val)                 (**r return value for the call *)
             (m: mem)                 (**r memory state *)
  .

Definition state_RTL (s: state): RTL.state :=
  match s with
  | State stack f sp pc rs m => RTL.State (stack_RTL stack) f sp pc rs m
  | Callstate stack f args m => RTL.Callstate (stack_RTL stack) f args m
  | Returnstate stack v m => RTL.Returnstate (stack_RTL stack) v m
  end.
Coercion state_RTL: state >-> RTL.state.

(* Used to execute the last instruction of a path (isteps is only in charge of executing the instructions before the last) *)
Inductive path_last_step ge pge stack (f: function): val -> node -> regset -> mem -> trace -> state -> Prop :=
  | exec_istate i sp pc rs m st:
     (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 (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 ->
      funsig fd = sig ->
      path_last_step ge pge stack f sp pc rs m
        E0 (Callstate (Stackframe res f sp pc' rs :: stack) fd rs##args m)
  | exec_Itailcall stk pc rs m sig ros args fd m':
      (fn_code f)!pc = Some(Itailcall sig ros args) ->
      find_function pge ros rs = Some fd ->
      funsig fd = sig ->
      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
      path_last_step ge pge stack f (Vptr stk Ptrofs.zero) pc rs m
        E0 (Callstate stack fd rs##args m')
  | exec_Ibuiltin sp pc rs m ef args res pc' vargs t vres m':
      (fn_code f)!pc = Some(Ibuiltin ef args res pc') ->
      eval_builtin_args ge (fun r => rs#r) sp m args vargs ->
      external_call ef ge vargs m t vres m' ->
      path_last_step ge pge stack f sp pc rs m
         t (State stack f sp pc' (regmap_setres res vres rs) m')
  | exec_Ijumptable sp pc rs m arg tbl n pc': (* TODO remove jumptable from here ? *)
      (fn_code f)!pc = Some(Ijumptable arg tbl) ->
      rs#arg = Vint n ->
      list_nth_z tbl (Int.unsigned n) = Some pc' ->
      path_last_step ge pge stack f sp pc rs m
        E0 (State stack f sp pc' rs m)
  | exec_Ireturn stk pc rs m or m':
      (fn_code f)!pc = Some(Ireturn or) ->
      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
      path_last_step ge pge stack f (Vptr stk Ptrofs.zero) pc rs m
        E0 (Returnstate stack (regmap_optget or Vundef rs) m').

(* Executes an entire path *)
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 ->
     (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 ->
     (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 *)
Inductive step ge pge: state -> trace -> state -> Prop :=
  | exec_path path stack f sp rs m pc t s: 
      (fn_path f)!pc = Some path ->
      path_step ge pge path.(psize) stack f sp rs m pc t s ->
      step ge pge (State stack f sp pc rs m) t s
  | exec_function_internal s f args m m' stk:
      Mem.alloc m 0 (fn_RTL f).(fn_stacksize) = (m', stk) ->
      step ge pge (Callstate s (Internal f) args m)
        E0 (State s
                  f
                  (Vptr stk Ptrofs.zero)
                  f.(fn_entrypoint)
                  (init_regs args f.(fn_params))
                  m')
  | exec_function_external s ef args res t m m':
      external_call ef ge args m t res m' ->
      step ge pge (Callstate s (External ef) args m) 
            t (Returnstate s res m')
  | exec_return res f sp pc rs s vres m:
      step ge pge (Returnstate (Stackframe res f sp pc rs :: s) vres m)
        E0 (State s f sp pc (rs#res <- vres) m).

Inductive initial_state (p:program) : state -> Prop :=
    initial_state_intro  (b : block) (f : fundef) (m0 : mem):
                          Genv.init_mem p = Some m0 ->
                          Genv.find_symbol (Genv.globalenv p) (prog_main p) = Some b ->
                          Genv.find_funct_ptr (Genv.globalenv p) b = Some f ->
                          funsig f = signature_main -> initial_state p (Callstate nil f nil m0).

Definition final_state (st: state) (i:int): Prop 
 := RTL.final_state st i.

Definition semantics (p: program) :=
  Semantics (step (Genv.globalenv (transf_program p))) (initial_state p) final_state (Genv.globalenv p).

(** * Proving the bisimulation between (semantics p) and (RTL.semantics p). *)

(** ** Preliminaries: simple tactics for option-monad *)

Lemma destruct_SOME A B (P: option B -> Prop) (e: option A) (f: A -> option B):
  (forall x, e = Some x -> P (f x)) -> (e = None -> P None) -> (P (SOME x <- e IN f x)).
Proof.
  intros; destruct e; simpl; auto.
Qed.

Lemma destruct_ASSERT B (P: option B -> Prop) (e: bool) (x: option B):
  (e = true -> P x) -> (e = false -> P None) -> (P (ASSERT e IN x)).
Proof.
  intros; destruct e; simpl; auto.
Qed.

Ltac inversion_SOME x :=
  try (eapply destruct_SOME; [ let x := fresh x in intro x | simpl; try congruence ]).

Ltac inversion_ASSERT :=
  try (eapply destruct_ASSERT; [ idtac | simpl; try congruence ]).

Ltac simplify_someHyp :=
  match goal with
  | H: None = Some _ |- _  => inversion H; clear H; subst
  | H: Some _ = None |- _  => inversion H; clear H; subst
  | H: ?t = ?t |- _ => clear H
  | H: Some _ = Some _ |- _  => inversion H; clear H; subst
  | H: Some _ <> None |- _ => clear H
  | H: None <> Some _ |- _ => clear H
  | H: _ = Some _ |- _ => (try rewrite !H in * |- *); generalize H; clear H
  | H: _ = None |- _ => (try rewrite !H in * |- *); generalize H; clear H
  end.

Ltac explore_destruct :=
  repeat (match goal with
  | [H: ?expr = ?val |- context[match ?expr with | _ => _ end]] => rewrite H
  | [H: match ?var with | _ => _ end |- _] => destruct var
  | [ |- context[match ?m with | _ => _ end] ] => destruct m
  | _ => discriminate
  end).

Ltac simplify_someHyps := 
  repeat (simplify_someHyp; simpl in * |- *).

Ltac try_simplify_someHyps := 
  try (intros; simplify_someHyps; eauto).

(* TODO: try to improve this tactic with a better control over names and inversion *)
Ltac simplify_SOME x :=
  (repeat inversion_SOME x); try_simplify_someHyps.

(** ** The easy way: Forward simulation of RTLpath by RTL 

This way can be viewed as a correctness property: all transitions in RTLpath are valid RTL transitions !

*)

Local Hint Resolve RTL.exec_Inop RTL.exec_Iop RTL.exec_Iload RTL.exec_Istore RTL.exec_Icond RTL.exec_Iload_notrap1 RTL.exec_Iload_notrap2: core.

(* istep reflects RTL.step *)
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.(ipc) st.(irs) st.(imem)).
Proof.
  destruct i; simpl; try congruence; simplify_SOME x.
  1-3: explore_destruct; simplify_SOME x.
Qed.

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.(ipc) st.(irs) st.(imem)).
Proof.
  induction path; simpl; try_simplify_someHyps.
  inversion_SOME i; intros Hi.
  inversion_SOME st0; intros Hst0.
  destruct (icontinue st0) eqn:cont.
  + intros; eapply star_step.
    - eapply istep_correct; eauto.
    - simpl; eauto.
    - auto.
  + intros; simplify_someHyp; eapply star_step.
    - eapply istep_correct; eauto.
    - simpl; eauto.
    - auto.
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.(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 (icontinue st0) eqn:cont.
  + intros; eapply plus_left.
    - eapply istep_correct; eauto.
    - eapply isteps_correct; eauto.
    - auto.
  + intros X; inversion X; subst.
    eapply plus_one.
    eapply istep_correct; eauto.
Qed.

Local Hint Resolve list_forall2_nil match_globdef_fun linkorder_refl match_globvar_intro: core.

Section CORRECTNESS.

Variable p: program.

Lemma match_prog_RTL: match_program (fun _ f tf => tf = fundef_RTL f) eq p (transf_program p).
Proof.
  eapply match_transform_program; eauto.
Qed.

Let pge := Genv.globalenv p.
Let ge := Genv.globalenv (transf_program p).

Lemma senv_preserved: Senv.equiv pge ge.
Proof (Genv.senv_match match_prog_RTL).

Lemma symbols_preserved s: Genv.find_symbol ge s = Genv.find_symbol pge s.
Proof (Genv.find_symbol_match match_prog_RTL s).

Lemma find_function_RTL_match ros rs fd:
  find_function pge ros rs = Some fd -> RTL.find_function ge ros rs = Some (fundef_RTL fd).
Proof.
  destruct ros; simpl.
  + intro; exploit (Genv.find_funct_match match_prog_RTL); eauto.
    intros (cuint & tf & H1 & H2 & H3); subst; auto.
  + rewrite symbols_preserved.
    destruct (Genv.find_symbol pge i); simpl; try congruence.
    intro; exploit (Genv.find_funct_ptr_match match_prog_RTL); eauto. 
    intros (cuint & tf & H1 & H2 & H3); subst; auto.
Qed.

Local Hint Resolve istep_correct RTL.exec_Ibuiltin RTL.exec_Ijumptable RTL.exec_Ireturn RTL.exec_Icall RTL.exec_Itailcall find_function_RTL_match: core.

Lemma path_last_step_correct stack f sp pc rs m t s:
  path_last_step ge pge stack f sp pc rs m t s ->
  RTL.step ge (State stack f sp pc rs m) t s.
Proof.
  destruct 1; try (eapply istep_correct); simpl; eauto.
Qed.

Lemma path_step_correct path stack f sp pc rs m t s:
  path_step ge pge path stack f sp rs m pc t s ->
  plus RTL.step ge (State stack f sp pc rs m) t s.
Proof.
  destruct 1.
  + eapply isteps_correct_early_exit; eauto.
  + eapply plus_right.
    eapply isteps_correct; eauto.
    eapply path_last_step_correct; eauto.
    auto.
Qed.

Local Hint Resolve plus_one RTL.exec_function_internal RTL.exec_function_external RTL.exec_return: core.

Lemma step_correct s t s': step ge pge s t s' -> plus RTL.step ge s t s'.
Proof.
  destruct 1; try (eapply path_step_correct); simpl; eauto.
Qed.

Theorem RTLpath_correct: forward_simulation (semantics p) (RTL.semantics p).
Proof.
  eapply forward_simulation_plus with (match_states := fun s1 s2 => s2 = state_RTL s1); simpl; auto.
  - apply senv_preserved.
  - destruct 1; intros; eexists; intuition eauto. econstructor; eauto.
    + apply (Genv.init_mem_match match_prog_RTL); auto.
    + rewrite (Genv.find_symbol_match match_prog_RTL).
      rewrite (match_program_main match_prog_RTL); eauto.
    + exploit (Genv.find_funct_ptr_match match_prog_RTL); eauto.
      intros (cunit & tf0 & XX); intuition subst; eauto.
  - unfold final_state; intros; subst; eauto.
  - intros; subst. eexists; intuition.
    eapply step_correct; eauto.
Qed.

End CORRECTNESS.

Lemma program_equals {A B: Type} : forall (p1 p2: AST.program A B),
  prog_defs p1 = prog_defs p2 ->
  prog_public p1 = prog_public p2 ->
  prog_main p1 = prog_main p2 ->
  p1 = p2.
Proof.
  intros. destruct p1. destruct p2. simpl in *. subst. auto.
Qed.

Lemma cons_extract {A: Type} : forall (l: list A) a b, a = b -> a::l = b::l.
Proof.
  intros. congruence.
Qed.

(* Definition transf_program : RTLpath.program -> RTL.program := transform_program fundef_RTL.

Lemma transf_program_proj: forall p, transf_program (transf_program p) = p.
Proof.
  intros p. destruct p as [defs pub main]. unfold program_proj. simpl.
  apply program_equals; simpl; auto.
  induction defs.
  - simpl; auto.
  - simpl. rewrite IHdefs. 
    destruct a as [id gd]; simpl.
    destruct gd as [f|v]; simpl; auto.
    rewrite transf_fundef_proj. auto.
Qed. *)


(** The hard way: Forward simulation of RTL by RTLpath 

This way can be viewed as a completeness property: all transitions in RTL can be represented as RTLpath transitions !

*)

(* This lemma is probably needed to compose a pass from RTL -> RTLpath with other passes.*)
Lemma match_RTL_prog {LA: Linker fundef} {LV: Linker unit} p: match_program (fun _ f tf => f = fundef_RTL tf) eq (transf_program p) p.
Proof. 
  unfold match_program, match_program_gen; intuition.
  unfold transf_program at 2; simpl.
  generalize (prog_defs p).
  induction l as [|a l]; simpl; eauto.
  destruct a; simpl.
  intros; eapply list_forall2_cons; eauto.
  unfold match_ident_globdef; simpl; intuition; destruct g as [f|v]; simpl; eauto.
  eapply match_globdef_var. destruct v; eauto.
Qed.

(* Theory of wellformed paths *)

Fixpoint nth_default_succ (c: code) (path:nat) (pc: node): option node :=
  match path with
  | O => Some pc
  | S path' => 
     SOME i <- c!pc IN
     SOME pc' <- default_succ i IN
     nth_default_succ c path' pc' 
  end.

Lemma wellformed_suffix_path c pm path path':
   (path' <= path)%nat -> 
  forall pc, wellformed_path c pm path pc -> 
   exists pc', nth_default_succ c (path-path') pc = Some pc' /\ wellformed_path c pm path' pc'.
Proof.
  induction 1 as [|m].
  + intros. enough (path'-path'=0)%nat as ->; [simpl;eauto|lia].
  + intros pc WF; enough (S m-path'=S (m-path'))%nat as ->; [simpl;eauto|lia].
    inversion WF; subst; clear WF; intros; simplify_someHyps.
    intros; simplify_someHyps; eauto.
Qed.

Definition nth_default_succ_inst (c: code) (path:nat) pc: option instruction :=
   SOME pc <- nth_default_succ c path pc IN
   c!pc.

Lemma final_node_path f path pc:
   (fn_path f)!pc = Some path -> 
   exists i, nth_default_succ_inst (fn_code f) path.(psize) pc = Some i 
             /\ (forall n, List.In n (successors_instr i) -> path_entry (*fn_code f*) (fn_path f) n).
Proof.
  intros; exploit fn_path_wf; eauto.
  intro WF.
  set (ps:=path.(psize)).
  exploit (wellformed_suffix_path (fn_code f) (fn_path f) ps O); lia || eauto.
  destruct 1 as (pc' & NTH_SUCC & WF'); auto.
  assert (ps - 0 = ps)%nat as HH by lia. rewrite HH in NTH_SUCC. clear HH.
  unfold nth_default_succ_inst.
  inversion WF'; clear WF'; subst. simplify_someHyps; eauto.
Qed.

Lemma internal_node_path path f path0 pc:
   (fn_path f)!pc = (Some path0) -> 
   (path < path0.(psize))%nat ->
   exists i pc',
      nth_default_succ_inst (fn_code f) path pc = Some i /\
      default_succ i = Some pc' /\
      (forall n, early_exit i = Some n -> path_entry (*fn_code f*) (fn_path f) n).
Proof.
  intros; exploit fn_path_wf; eauto.
  set (ps:=path0.(psize)).
  intro WF; exploit (wellformed_suffix_path (fn_code f) (fn_path f) ps (ps-path)); eauto. { lia. }
  destruct 1 as (pc' & NTH_SUCC & WF').
  assert (ps - (ps - path) = path)%nat as HH by lia. rewrite HH in NTH_SUCC. clear HH.
  unfold nth_default_succ_inst. 
  inversion WF'; clear WF'; subst. { lia. }
  simplify_someHyps; eauto.
Qed.

Lemma initialize_path (*c*) pm n: path_entry (*c*) pm n -> exists path, pm!n = Some path.
Proof.
  unfold path_entry; destruct pm!n; eauto. intuition congruence.
Qed.
Local Hint Resolve fn_entry_point_wf: core.
Local Opaque path_entry.

Lemma istep_successors ge i sp rs m st:
  istep ge i sp rs m = Some st -> 
  In (ipc st) (successors_instr i).
Proof.
  destruct i; simpl; try congruence; simplify_SOME x.
  all: explore_destruct; simplify_SOME x.
Qed.

Lemma istep_normal_exit ge i sp rs m st:
  istep ge i sp rs m = Some st ->
  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.(icontinue) = true ->
  isteps ge path f sp rs m pc = Some st ->
  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 (icontinue st0) eqn:X; try congruence.
  try_simplify_someHyps.
  intros; erewrite istep_normal_exit; eauto.
Qed.


(* TODO: the three following lemmas could maybe simplified by introducing an auxiliary
    left-recursive definition equivalent to isteps ?
*)
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.(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.
    destruct st as [b]; destruct b; simpl; auto.
  + intros rs m pc st i H.
    simpl in H.
    generalize H; clear H; simplify_SOME xx.
    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 ->
  (icontinue st)=false ->
  exists st0 i path0,
    (path > path0)%nat /\
    isteps ge path0 f sp rs m pc = Some st0 /\ 
    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 (icontinue st0) eqn: CONT.
    + intros STEP PC STEPS CONT0. exploit IHpath; eauto.
      clear STEPS.
      intros (st1 & i0 & path0 & BOUND & STEP1 & CONT1 & X1 & X2); auto.
      exists st1. exists i0. exists (S path0). intuition.
      simpl; try_simplify_someHyps. 
      rewrite CONT. auto.
    + intros; try_simplify_someHyps; try congruence.
      eexists. exists i. exists O; simpl. intuition eauto.
      lia.
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 ->
  (icontinue st)=false ->
  isteps ge path1 f sp rs m pc = Some st.
Proof.
  induction 1 as [|path1]; simpl; auto.
  intros PSTEP CONT. exploit IHle; auto. clear PSTEP IHle H path0.
  generalize rs m pc st CONT; clear rs m pc st CONT. 
  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 (icontinue st0) eqn: CONT0; eauto.
Qed.

(* FIXME - add prediction *)
Inductive is_early_exit pc: instruction -> Prop :=
  | Icond_early_exit cond args ifnot predict:
     is_early_exit pc (Icond cond args pc ifnot predict)
 . (* TODO add jumptable here ? *)

Lemma istep_early_exit ge i sp rs m st :
  istep ge i sp rs m = Some st -> 
  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.
  all: explore_destruct; simplify_SOME b; try discriminate.
Qed.

Section COMPLETENESS.

Variable p: program.

Let pge := Genv.globalenv p.
Let ge := Genv.globalenv (transf_program p).

Lemma find_funct_ptr_RTL_preserv b f:
   Genv.find_funct_ptr ge b = Some f -> (exists f0, Genv.find_funct_ptr pge b = Some f0 /\ f = f0).
Proof.
  intros; exploit (Genv.find_funct_ptr_match (match_RTL_prog p)); eauto.
  destruct 1 as (cunit & tf & X & Y & Z); subst.
  eauto.
Qed.

Lemma find_RTL_function_match ros rs fd:
  RTL.find_function ge ros rs = Some fd -> exists fd', fd = fundef_RTL fd' /\ find_function pge ros rs = Some fd'.
Proof.
  destruct ros; simpl.
  + intro; exploit (Genv.find_funct_match (match_RTL_prog p)); eauto.
    intros (cuint & tf & H1 & H2 & H3); subst; eauto.
  + rewrite (symbols_preserved p); unfold pge.
    destruct (Genv.find_symbol (Genv.globalenv p) i); simpl; try congruence.
    intro; exploit find_funct_ptr_RTL_preserv; eauto.
    intros (tf & H1 & H2); subst; eauto.
Qed.


(** *** Definition of well-formed stacks and of match_states *)
Definition wf_stf (st: stackframe): Prop :=
  match st with
  | Stackframe res f sp pc rs => path_entry (*f.(fn_code)*) f.(fn_path) pc
  end.

Definition wf_stackframe (stack: list stackframe): Prop :=
  forall st, List.In st stack -> wf_stf st.

Lemma wf_stackframe_nil: wf_stackframe nil.
Proof.
  unfold wf_stackframe; simpl. tauto.
Qed.
Local Hint Resolve wf_stackframe_nil: core.

Lemma wf_stackframe_cons st stack:
  wf_stackframe (st::stack) <-> (wf_stf st) /\ wf_stackframe stack.
Proof.
  unfold wf_stackframe; simpl; intuition (subst; auto).
Qed.

Definition stack_of (s: state):  list stackframe :=
  match s with
  | State stack f sp pc rs m => stack
  | Callstate stack f args m => stack
  | Returnstate stack v m => stack
  end.

Definition is_inst (s: RTL.state): bool :=
  match s with
  | RTL.State stack f sp pc rs m => true
  | _ => false
  end.

Inductive match_inst_states_goal (idx: nat) (s1:RTL.state): state -> Prop :=
  | State_match path stack f sp pc rs m s2:
    (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.(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 :=
  if is_inst s1 then match_inst_states_goal idx s1 s2 else s1 = state_RTL s2.

Definition match_states (idx: nat) (s1:RTL.state) (s2:state): Prop :=
    match_inst_states idx s1 s2
 /\ wf_stackframe (stack_of s2).

(** *** Auxiliary lemmas of completeness *)
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.(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.
  all: explore_destruct; simplify_SOME a.
Qed.

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.(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))); lia || eauto.
  intros (i & pc' & Hi & Hpc & DUM).
  unfold nth_default_succ_inst in Hi.
  erewrite isteps_normal_exit in Hi; eauto.
  exploit istep_complete; congruence || eauto.
  intros (SILENT & st0 & STEP0 & EQ).
  intuition; subst; unfold match_inst_states; simpl.
  intros; refine (State_match _ _ path stack f sp pc rs m _ PATH _ _ _); simpl; lia || eauto.
  set (ps:=path.(psize)). enough (ps - idx = S (ps - (S idx)))%nat as ->; try lia.
  erewrite <- isteps_step_right; eauto.
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.(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.(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 *)
  intros PSTEP PATH CONT RSTEP WF; exploit (final_node_path f path); eauto.
  intros (i & Hi & SUCCS).
  unfold nth_default_succ_inst in Hi.
  erewrite isteps_normal_exit in Hi; eauto.
  destruct (default_succ i) eqn:Hn0.
  + (* exec_istate *)
    exploit istep_complete; congruence || eauto.
    intros (SILENT & st0 & STEP0 & EQ); subst.
    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) (ipc st0)) as (path0 & Hpath0); eauto.
    exists (path0.(psize)); intuition eauto.
    econstructor; eauto.
    * enough (path0.(psize)-path0.(psize)=0)%nat as ->; simpl; eauto || lia.
    * simpl; eauto.
  + generalize Hi; inversion RSTEP; clear RSTEP; subst; (repeat (simplify_someHyp; simpl in * |- * )); try congruence; eauto.
    - (* Icall *)
      intros; exploit find_RTL_function_match; eauto.
      intros (fd' & MATCHfd & Hfd'); subst.
      exploit (exec_Icall ge pge); eauto.
      eexists; intuition eauto.
      eexists O; unfold match_states, match_inst_states; simpl; intuition eauto.
      rewrite wf_stackframe_cons; intuition simpl; eauto.
    - (* Itailcall *)
      intros; exploit find_RTL_function_match; eauto.
      intros (fd' & MATCHfd & Hfd'); subst.
      exploit (exec_Itailcall ge pge); eauto.
      eexists; intuition eauto.
      eexists O; unfold match_states, match_inst_states; simpl; intuition eauto.
    - (* Ibuiltin *)
      intros; exploit exec_Ibuiltin; eauto.
      eexists; intuition eauto.
      unfold match_states, match_inst_states; simpl.
      destruct (initialize_path (*fn_code f*) (fn_path f) pc') as (path0 & Hpath0); eauto.
      exists path0.(psize); intuition eauto.
      econstructor; eauto.
      * enough (path0.(psize)-path0.(psize)=0)%nat as ->; simpl; eauto || lia.
      * simpl; eauto.
   - (* Ijumptable *)
      intros; exploit exec_Ijumptable; eauto.
      eexists; intuition eauto.
      unfold match_states, match_inst_states; simpl.
      destruct (initialize_path (*fn_code f*) (fn_path f) pc') as (path0 & Hpath0); eauto.
      exists path0.(psize); intuition eauto.
      econstructor; eauto.
      * enough (path0.(psize)-path0.(psize)=0)%nat as ->; simpl; eauto || lia.
      * simpl; eauto.
  - (* Ireturn *)
      intros; exploit exec_Ireturn; eauto.
      eexists; intuition eauto.
      eexists O; unfold match_states, match_inst_states; simpl; intuition eauto.
Qed.

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.(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.(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.(icontinue)) eqn: CONT.
  destruct idx as [ | idx].
  + (* path_step on normal_exit *)
     assert (path.(psize)-0=path.(psize))%nat as HH by lia. rewrite HH in PSTEP. clear HH.
     exploit normal_exit; eauto.
     intros (s2' & LSTEP & (idx' & MATCH)).
     exists idx'; exists s2'; intuition eauto.
  + (* stuttering step *)
    exploit stuttering; eauto.
    unfold match_states; exists idx; exists (State stack f sp pc rs m); 
    intuition.
  + (* one or two path_step on early_exit *)
    exploit (isteps_resize ge (path.(psize) - idx)%nat path.(psize)); eauto; try lia.
    clear PSTEP; intros PSTEP.
    (* TODO for clarification: move the assert below into a separate lemma *)
    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).
      exploit istep_early_exit; eauto.
      intros (X1 & X2 & EARLY_EXIT).
      destruct st as [cont pc0 rs0 m0]; simpl in * |- *; intuition subst.
      exploit (internal_node_path path0); lia || eauto.
      intros (i' & pc' & Hi' & Hpc' & ENTRY).
      unfold nth_default_succ_inst in Hi'.
      erewrite isteps_normal_exit in Hi'; eauto.
      clear pc' Hpc' STEP0 PSTEP0 BOUND0; try_simplify_someHyps; intros.
      destruct EARLY_EXIT as [cond args ifnot]; simpl in ENTRY;
      destruct (initialize_path (*fn_code f*) (fn_path f) pc0); eauto.
    }
    destruct HPATH0 as (path1  & Hpath1).
    destruct (path1.(psize)) as [|ps] eqn:Hpath1size.
    * (* two step case *)
      exploit (normal_exit path1); try rewrite Hpath1size; simpl; eauto.
      simpl; intros (s2' & LSTEP & (idx' & MATCH)).
      exists idx'. exists s2'. constructor; auto.
      right. right. eexists; intuition eauto.
      (* now, prove the last step *)
      rewrite Hpath1size; exploit exec_normal_exit. 4:{ eauto. } 
      - simpl; eauto.
      - simpl; eauto.
      - simpl; eauto.
    * (* single step case *)
      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 lia.  simpl; eauto. }
      - lia.
      - simpl; eauto.
      - simpl; eauto.
      - intuition subst.
        repeat eexists; intuition eauto.
Qed.

Lemma step_noninst_complete s1 t s1' s2:
  is_inst s1 = false ->
  s1 = state_RTL s2 ->
  RTL.step ge s1 t s1' ->
  wf_stackframe (stack_of s2) ->
  exists s2', step ge pge s2 t s2' /\ exists idx, match_states idx s1' s2'.
Proof.
  intros H0 H1 H2 WFSTACK; destruct s2; subst; simpl in * |- *; try congruence;
  inversion H2; clear H2; subst; try_simplify_someHyps; try congruence.
  + (* exec_function_internal *)
    destruct f; simpl in H3; inversion H3; subst; clear H3.
    eexists; constructor 1.
    * eapply exec_function_internal; eauto.
    * unfold match_states, match_inst_states; simpl.
      destruct (initialize_path (*fn_code f*) (fn_path f) (fn_entrypoint (fn_RTL f))) as (path & Hpath); eauto.
      exists path.(psize). constructor; auto.
      econstructor; eauto.
      - set (ps:=path.(psize)). enough (ps-ps=O)%nat as ->; simpl; eauto.
        lia.
      - simpl; auto.
  + (* exec_function_external *)
    destruct f; simpl in H3 |-; inversion H3; subst; clear H3.
    eexists; constructor 1.
    * apply exec_function_external; eauto.
    * unfold match_states, match_inst_states; simpl. exists O; auto.
  + (* exec_return *)
    destruct stack eqn: Hstack; simpl in H1; inversion H1; clear H1; subst.
    destruct s0 eqn: Hs0; simpl in H0; inversion H0; clear H0; subst.
    eexists; constructor 1.
    * apply exec_return.
    * unfold match_states, match_inst_states; simpl.
      rewrite wf_stackframe_cons in WFSTACK.
      destruct WFSTACK as (H0 & H1); simpl in H0.
      destruct (initialize_path (*fn_code f0*) (fn_path f0) pc0) as (path & Hpath); eauto.
      exists path.(psize). constructor; auto.
      econstructor; eauto.
      - set (ps:=path.(psize)). enough (ps-ps=O)%nat as ->; simpl; eauto.
        lia.
      - simpl; auto.
Qed.

(** *** The main completeness lemma and the simulation theorem...*)
Lemma step_complete s1 t s1' idx s2:
 match_states idx s1 s2 ->
 RTL.step ge s1 t s1' ->
 exists idx' s2', (plus (step ge) pge s2 t s2' \/ (t = E0 /\ s2=s2' /\ (idx' < idx)%nat)) /\ match_states idx' s1' s2'.
Proof.
  Local Hint Resolve plus_one plus_two exec_path: core.
  unfold match_states at 1, match_inst_states. intros (IS_INST & WFSTACK). destruct (is_inst s1) eqn: His1.
  - clear His1; destruct IS_INST as [path stack f sp pc rs m s2 X X0 X1 X2]; auto; subst; simpl in * |- *. 
    intros STEP; exploit path_step_complete; eauto.
    intros (idx' & s2' & H0 & H1).
    eexists; eexists; eauto.
    destruct H0 as [H0|[H0|(path'&H0)]]; intuition subst; eauto.
  - intros; exploit step_noninst_complete; eauto.
    intros (s2' & STEP & (idx0 & MATCH)).
    exists idx0; exists s2'; intuition auto.
Qed.

Theorem RTLpath_complete: forward_simulation (RTL.semantics p) (semantics p).
Proof.
  eapply (Forward_simulation (L1:=RTL.semantics p) (L2:=semantics p) lt match_states).
  constructor 1; simpl.
  - apply lt_wf.
  - unfold match_states, match_inst_states. destruct 1; simpl; exists O.
    destruct (find_funct_ptr_RTL_preserv b f) as (f0 & X1 & X2); subst; eauto.
    exists (Callstate nil f0 nil m0). simpl; split; try econstructor; eauto.
    + apply (Genv.init_mem_match (match_RTL_prog p)); auto.
    + rewrite (Genv.find_symbol_match (match_RTL_prog p)).
      rewrite (match_program_main (match_RTL_prog p)); eauto.
  - unfold final_state, match_states, match_inst_states. intros i s1 s2 r (H0 & H1) H2; destruct H2.
    destruct s2; simpl in * |- *; inversion H0; subst.
    constructor.
  - Local Hint Resolve star_refl: core.
    intros; exploit step_complete; eauto.
    destruct 1 as (idx' & s2' & X).
    exists idx'. exists s2'. intuition (subst; eauto). 
  - intros id; destruct (senv_preserved p); simpl in * |-. intuition.
Qed.

End COMPLETENESS.