Require Recdef.
Require Import FSets.
Require Import Coqlib.
Require Import Ordered.
Require Import Errors.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Globalenvs.
Require Import Op.
Require Import Registers.
Require Import Smallstep.
Require Import RTL.
Require Import SSA.
Require Import SSAutils.
Require Import CSSA.
Require Import RTLdparspec.
Require Import Kildall.
Require Import Conventions.
Require Import Utils.
Require Import NArith.
Require Import Events.
Require Import Permutation.
Require Import DLib.
Require Import CSSAproof.
Require Import RTLpar.
Require Import RTLdpar.

Lemma max_reg_correct_code: forall f,
    Ple (CSSAgen.get_max_reg_in_code (RTLpar.fn_code f))
        (get_maxreg f).

Notation no_fresh := (fun f => Parmov.is_not_temp reg (fun _ : reg => (fresh_init f))).

Lemma get_maxreg_is_not_temp_code :
  forall f pc,
    match (fn_code f) ! pc with
      | None => True
      | Some ins =>
          match ins with
            | SSA.Inop s => True
            | SSA.Iop op args dst s =>
              forall r, In r (dst::args) -> no_fresh f r
            | SSA.Iload ch ad args dst s =>
              forall r, In r (dst::args) -> no_fresh f r
            | SSA.Istore ch ad args src s =>
              forall r, In r (src::args) -> no_fresh f r
            | SSA.Icall sig ros args dst s =>
              match ros with
                | inl rf => forall r, In r (rf::dst::args) -> no_fresh f r
                | inr _ => forall r, In r (dst::args) -> no_fresh f r
              end
            | SSA.Itailcall sig ros args =>
              match ros with
                | inl rf => forall r, In r (rf::args) -> no_fresh f r
                | inr _ => forall r, In r args -> no_fresh f r
              end
            | SSA.Ibuiltin ef args dst s =>
              forall r, In r ((params_of_builtin_res dst) ++ (params_of_builtin_args args)) -> no_fresh f r
            | SSA.Icond cond args ifso ifnot =>
              forall r, In r args -> no_fresh f r
            | SSA.Ijumptable arg tbl =>
              no_fresh f arg
            | SSA.Ireturn rop =>
              match rop with
                | Some r => no_fresh f r
                | _ => True
              end
          end
    end.

Lemma max_reg_correct_parccode : forall f,
  Ple (get_max_reg_in_parcode (fn_parcopycode f)) (get_maxreg f).

Lemma ple_foldmaxparcb_init :
  forall l m n,
  Ple m n ->
  Ple
    m
    (List.fold_left
      (fun m (pparcb : positive * parcopyblock) => Pos.max m
        (get_max_reg_in_parcb (snd pparcb)))
      l n).

Lemma max_reg_in_parcode_aux :
  forall elems init pparcb (pc:positive) parcb,
  In pparcb elems ->
  pparcb = (pc, parcb) ->
  Ple (get_max_reg_in_parcb parcb)
    (fold_left
      (fun m p =>
        Pos.max m (get_max_reg_in_parcb (snd p)))
    elems init).

Lemma max_reg_in_parcode :
  forall parcode pc p,
  parcode ! pc = Some p ->
  Ple (get_max_reg_in_parcb p)
    (get_max_reg_in_parcode parcode).

Lemma ple_foldmaxreg_init :
  forall l m n,
  Ple m n ->
  Ple
    m
    (List.fold_left (fun (m0 : positive) (parc : parcopy) =>
         Pos.max m0 (get_max_reg_in_parc parc))
      l n).

Lemma get_max_reg_in_parcb_correct_src_aux :
  forall l (r : reg) m d,
  In (r,d) (parcb_to_moves l) ->
  Ple r
    (List.fold_left (fun m parc => Pos.max m (get_max_reg_in_parc parc)) l m).

Lemma get_max_reg_in_parcb_dst_correct_aux :
  forall l (r : reg) m d,
  In (r,d) (parcb_to_moves l) ->
  Ple d
    (List.fold_left (fun m parc => Pos.max m (get_max_reg_in_parc parc)) l m).

Lemma get_max_reg_in_parcb_src_correct :
  forall l r d,
  In (r,d) (parcb_to_moves l) ->
  Ple r (get_max_reg_in_parcb l).

Lemma get_max_reg_in_parcb_dst_correct :
  forall l r d,
  In (r,d) (parcb_to_moves l) ->
  Ple d (get_max_reg_in_parcb l).

Lemma get_maxreg_is_not_temp_parcopies :
  forall f pc parcb,
    (fn_parcopycode f) ! pc = Some parcb ->
    Parmov.move_no_temp reg (fun _ => fresh_init f) (parcb_to_moves parcb).

Ltac sz := unfold Plt, Ple in * ; (zify; lia).
Ltac allinv :=
  repeat
    match goal with
      | [ H1: (st_code ?s) ! ?pc = Some _ ,
        H2: (st_code ?s) ! ?pc = Some _ |- _ ] =>
      rewrite H1 in H2; inv H2
      | [ H1: Some _ = (st_code ?s) ! ?pc ,
        H2: (st_code ?s) ! ?pc = Some _ |- _ ] =>
      rewrite H1 in H2; inv H2
      | _ => idtac
    end.

Reasoning about monadic computations

Remark bind_inversion:
  forall (A B: Type) (f: mon A) (g: A -> mon B)
         (y: B) (s1 s3: state) (i: state_incr s1 s3),
  bind f g s1 = OK y s3 i ->
  exists x, exists s2, exists i1, exists i2,
  f s1 = OK x s2 i1 /\ g x s2 = OK y s3 i2.

Ltac monadInv1 H :=
  match type of H with
  | (OK _ _ _ = OK _ _ _) =>
      inversion H; clear H; try subst
  | (Error _ _ = OK _ _ _) =>
      discriminate
  | (ret _ _ = OK _ _ _) =>
      inversion H; clear H; try subst
  | (error _ _ = OK _ _ _) =>
      discriminate
  | (bind ?F ?G ?S = OK ?X ?S' ?I) =>
      let x := fresh "x" in (
      let s := fresh "s" in (
      let i1 := fresh "INCR" in (
      let i2 := fresh "INCR" in (
      let EQ1 := fresh "EQ" in (
      let EQ2 := fresh "EQ" in (
      destruct (bind_inversion _ _ F G X S S' I H) as [x [s [i1 [i2 [EQ1 EQ2]]]]];
      clear H;
      try (monadInv1 EQ2)))))))
  end.

Ltac monadInv H :=
  match type of H with
  | (ret _ _ = OK _ _ _) => monadInv1 H
  | (error _ _ = OK _ _ _) => monadInv1 H
  | (bind ?F ?G ?S = OK ?X ?S' ?I) => monadInv1 H
  | (bind2 ?F ?G ?S = OK ?X ?S' ?I) => monadInv1 H
  | (?F _ _ _ _ _ _ _ _ = OK _ _ _) =>
      ((progress simpl in H) || unfold F in H); monadInv1 H
  | (?F _ _ _ _ _ _ _ = OK _ _ _) =>
      ((progress simpl in H) || unfold F in H); monadInv1 H
  | (?F _ _ _ _ _ _ = OK _ _ _) =>
      ((progress simpl in H) || unfold F in H); monadInv1 H
  | (?F _ _ _ _ _ = OK _ _ _) =>
      ((progress simpl in H) || unfold F in H); monadInv1 H
  | (?F _ _ _ _ = OK _ _ _) =>
      ((progress simpl in H) || unfold F in H); monadInv1 H
  | (?F _ _ _ = OK _ _ _) =>
      ((progress simpl in H) || unfold F in H); monadInv1 H
  | (?F _ _ = OK _ _ _) =>
      ((progress simpl in H) || unfold F in H); try monadInv1 H
  | (?F _ = OK _ _ _) =>
      ((progress simpl in H) || unfold F in H); monadInv1 H
  end.

Lemma mfold_unit_step: forall (A: Type) (f: A -> mon unit) l u a s1 s2 INCR,
  mfold_unit f (a::l) s1 = OK u s2 INCR ->
  exists u'' , exists s'', exists INCR'', exists INCR''',
    f a s1 = OK u'' s'' INCR''
    /\ (mfold_unit f l s'' = OK u s2 INCR''').

Global Hint Resolve state_incr_refl: dessa.
Global Hint Resolve state_incr_trans : dessa.

Ltac saturateTrans :=
  match goal with
  | H1: state_incr ?x ?y, H2: state_incr ?y ?z |- _ =>
      match goal with
      | H: state_incr x z |- _ =>
         fail 1
      | _ =>
         let i := fresh "INCR" in
         (generalize (state_incr_trans x y z H1 H2); intro i;
          saturateTrans)
      end
  | _ => idtac
  end.

Ltac expl_incr pc :=
  match goal with
    | [ H : forall pc : positive,
       (st_code ?s0) ! pc = None \/ (st_code ?s0) ! pc = (st_code ?s2) ! pc |- _ ] =>
    eelim (H pc) ; eauto ; (intros ; congruence)
  end.

The implementation of DeSSA satisfies its specification

Properties of auxiliary functions

Lemma copy_ins_at:
  forall s1 s2 incr pc max i code u,
  copy_ins pc max i code s1 = OK u s2 incr ->
  (s2.(st_code)! pc = Some i
    /\ (forall pc', pc' <> pc -> s2.(st_code)!pc' = s1.(st_code)!pc')
    /\ s1.(st_code) ! pc = None).

Lemma copy_ins_at_renum:
  forall s1 s2 incr pc max i code u,
  copy_ins pc max i code s1 = OK u s2 incr ->
  (map_pc (st_renum s2)) pc = pc
  /\
  (forall pc', pc' <> pc ->
               (map_pc (st_renum s2)) pc' = (map_pc (st_renum s1)) pc').

Global Hint Resolve copy_ins_at: dessa.

Lemma reach_moves_incr : forall lnew s1 s2 succ' lastnew block ,
  reach_moves (st_code s1) succ' lastnew block lnew ->
  state_incr s1 s2 ->
  reach_moves (st_code s2) succ' lastnew block lnew.

Lemma copy_ins_next_fs : forall s1 s x pc max ins code INCR,
  copy_ins pc max ins code s1 = OK x s INCR ->
  (st_nextnode_fs s1) = (st_nextnode_fs s).

Lemma add_reach_moves : forall opc pc parcb s1 s2 incr,
  add_moves opc pc parcb s1 = OK tt s2 incr ->
  exists lnew,
    reach_moves (st_code s2) (st_nextnode_fs s1) pc parcb lnew.

Lemma add_moves_renum : forall opc pc parcb s1 s2 incr,
  add_moves opc pc parcb s1 = OK tt s2 incr ->
  (match opc with
     | Some opc => (forall pc', pc' <> opc -> (st_renum s2) ! pc' = (st_renum s1) ! pc')
                   /\ (st_code s2) ! (map_pc (st_renum s2) opc) = Some (RTL.Inop pc)
     | None => (forall pc, (st_renum s2) ! pc = (st_renum s1) ! pc)
   end).

Lemma add_moves_renum_last : forall opc parcb pc s1 s2 incr,
                               pc <> opc ->
  add_moves (Some opc) pc parcb s1 = OK tt s2 incr ->
  (parcb = nil /\ map_pc (st_renum s2) pc = (map_pc (st_renum s1) pc))
  \/ exists lnew,
        reach_moves (st_code s2) (st_nextnode_fs s1) pc parcb lnew /\
        exists rpc (lnew' : list node),
          rev lnew = rpc :: lnew' /\
          (map_pc (st_renum s2) opc) = rpc.

Ltac kick :=
  match goal with
    | [ H: (RTLpar.fn_code ?f) ! _ = Some (Itailcall _ (inl ident _) _) |- _] =>
      econstructor 8 ; eauto
    | [ H: (RTLpar.fn_code ?f) ! _ = Some (Icall _ (inl ident _) _ _ _) |- _] =>
      econstructor 6 ; eauto
    | _ =>
      (econstructor ; eauto)
  end ;
  (intros rr Hrr; try inv Hrr).

Correctness of copy_wwo_add

Lemma copy_wwo_add_dssa_spec: forall f (WF: wf_function f) fresh pc max s1 s2 incr ins,
  (fn_code f) ! pc = Some ins ->
  copy_wwo_add fresh (make_predecessors (fn_code f) SSA.successors_instr)
               (fn_code f) (fn_parcopycode f) max pc s1 = OK tt s2 incr ->
  rtldpar_spec fresh (fn_code f) (fn_parcopycode f) (st_code s2) (map_pc (st_renum s2))
               pc.

Lemma copy_ins_unch_renum : forall pc max ins code s1 s2 INCR,
   copy_ins pc max ins code s1 = OK tt s2 INCR ->
   forall pc', pc' <> pc -> (map_pc (st_renum s2)) pc' = (map_pc (st_renum s1) pc').

Lemma copy_wwo_unch_renum : forall preds code pcode fresh max s1 s2 incr pc,
  (copy_wwo_add fresh preds code pcode max) pc s1 = OK tt s2 incr ->
  forall pc', pc <> pc' -> (map_pc (st_renum s2)) pc' = (map_pc (st_renum s1) pc').

Lemma mfold_copy_wwo_unch_renum : forall preds code pcode fresh l max s1 s2 incr,
  mfold_unit (copy_wwo_add fresh preds code pcode max) l s1 = OK tt s2 incr ->
  forall pc, ~ In pc l -> (map_pc (st_renum s2)) pc = (map_pc (st_renum s1) pc).
    
Lemma mfold_dssa_spec : forall f (WF: wf_function f) fresh l max s1 s2 incr,
  mfold_unit
    (copy_wwo_add fresh
                  (make_predecessors (fn_code f) successors_instr)
                  (fn_code f) (RTLpar.fn_parcopycode f) max)
    l s1 = OK tt s2 incr ->
  (list_norepet l) ->
  forall pc ins,
    In pc l -> (fn_code f) ! pc = Some ins ->
    rtldpar_spec fresh (fn_code f) (fn_parcopycode f)
                 (st_code s2) (map_pc (st_renum s2)) pc.

Lemma NoDup_list_norepet : forall (A: Type) (l:list A), NoDup l -> list_norepet l.

Lemma list_norepet_NoDup : forall (A: Type) (l:list A), list_norepet l -> NoDup l.

Lemma get_max_fold''' : forall l maxacc lacc,
  NoDup (l++lacc) ->
  NoDup (snd (fold_left (fun (al: positive * list positive) pc => let (a,l) := al in if plt a pc then (pc,pc::l) else (a,pc::l)) l (maxacc,lacc))).

Lemma get_max_nodup : forall (A: Type) t,
  NoDup (snd (@get_max A t)).

Definition mapping (f: function) : (PTree.t node) :=
  let '(init,max,lp) := init_state f in
  let fresh := fresh_init f in
  let preds := make_predecessors (fn_code f) SSA.successors_instr in
  match mfold_unit (copy_wwo_add fresh
                                 preds (fn_code f) (fn_parcopycode f) max)
                   (sort_pp lp) init with
    | Error m => PTree.empty node
    | OK u s'' H => (st_renum s'')
  end.
  

Specification compliancy of the implementation

Lemma transl_function_spec_ok : forall f (WF: wf_function f) tf,
    transl_function f = Errors.OK tf ->
    transl_function_spec f tf (map_pc (mapping f)).

Semantic preservation

Require Import Linking.

Section PRESERVATION.

  Definition match_prog (p: RTLpar.program) (tp: RTL.program) :=
    match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp.

  Lemma transf_program_match:
    forall p tp, transl_program p = Errors.OK tp -> match_prog p tp.

  Section CORRECTNESS.

    Variable prog: RTLpar.program.
    Variable tprog: RTL.program.
    Hypothesis TRANSF_PROG: match_prog prog tprog.
    Hypothesis WF_PROG : wf_program prog.
    Hypothesis MILL_PROG : mill_program prog.

    Let ge := Genv.globalenv prog.
    Let tge := Genv.globalenv tprog.
    
    Lemma symbols_preserved:
      forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.

    Lemma functions_translated:
      forall (v: val) (f: fundef),
        Genv.find_funct ge v = Some f ->
        exists tf, Genv.find_funct tge v = Some tf
                   /\ transl_fundef f = Errors.OK tf.

    Lemma function_ptr_translated:
      forall b (f: fundef),
        Genv.find_funct_ptr ge b = Some f ->
        exists tf, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = Errors.OK tf.

    Lemma sig_fundef_translated:
      forall f tf,
        transl_fundef f = Errors.OK tf ->
        RTL.funsig tf = funsig f.

    Lemma sig_function_translated:
      forall f tf,
        transl_function f = Errors.OK tf ->
        RTL.fn_sig tf = fn_sig f.

    Lemma spec_ros_r_find_function:
      forall rs rs' f r,
        find_function ge (inl _ r) rs = Some f ->
        rs# r = rs'#r ->
        exists tf,
          RTL.find_function tge (inl _ r) rs' = Some tf
          /\ RTLdpar.transl_fundef f = Errors.OK tf.

    Lemma spec_ros_id_find_function:
      forall rs rs' f id,
        find_function ge (inr _ id) rs = Some f ->
        exists tf,
          RTL.find_function tge (inr _ id) rs' = Some tf
          /\ RTLdpar.transl_fundef f = Errors.OK tf.

    Lemma stacksize_preserved: forall f tf,
        transl_function f = Errors.OK tf ->
        fn_stacksize f = RTL.fn_stacksize tf.

    Lemma senv_preserved:
      Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge).

Create HintDb valagree.
Hint Resolve symbols_preserved : valagree.
Hint Resolve eval_addressing_preserved : valagree.
Hint Resolve eval_operation_preserved : valagree.
Hint Resolve sig_function_translated : valagree.
Hint Resolve sig_fundef_translated : valagree.
Hint Resolve senv_preserved : valagree.
Hint Resolve stacksize_preserved: valagree.


Definition parcopy_store_e (parcb: list (reg * reg) ) (rs: regset) : regset :=
  fold_left (fun rs parc =>
               match parc with
                 | (src,dst) => rs# dst <- (rs# src)
               end) parcb rs.
    
Lemma reach_moves_star : forall mvs fresh ts sp rs m tf succ lnew ,
  reach_moves (RTL.fn_code tf) fresh succ mvs lnew ->
  star RTL.step tge (RTL.State ts tf sp fresh rs m) E0
                    (RTL.State ts tf sp succ (parcopy_store_e mvs rs) m).

Lemma rev_nil_nil {A: Type} : forall (l:list A), rev l = nil -> l = nil.

Lemma reach_moves_star_last : forall mvs l fresh tf succ,
  reach_moves (RTL.fn_code tf) fresh succ mvs l ->
  forall a lnew, rev l = (a::lnew) ->
  forall ts sp rs m,
  star RTL.step tge (RTL.State ts tf sp fresh rs m) E0
                    (RTL.State ts tf sp a (parcopy_store_e mvs rs) m).

Simulation relation

Variant match_regset (f: function) : SSA.regset -> RTL.regset -> Prop :=
| mrg_intro : forall rs rs',
  (forall r,
    no_fresh f r ->
    rs# r = rs'# r) ->
    match_regset f rs rs'.

Lemma match_regset_args : forall f args rs rs' ,
  match_regset f rs rs' ->
  (forall arg, In arg args -> no_fresh f arg) ->
  rs## args = rs'## args.
Hint Resolve match_regset_args : valagree.

Inductive match_stackframes : list stackframe -> list RTL.stackframe -> Prop :=
| match_stackframes_nil: match_stackframes nil nil
| match_stackframes_cons:
  forall res f sp pc rs rs' s tf ts
    (STACK : match_stackframes s ts)
    (SPEC: transl_function f = Errors.OK tf)
    (WF: wf_function f)
    (MILL: mill_function f)
    (MREG: match_regset f rs rs'),
    match_stackframes
    ((Stackframe res f sp pc rs) :: s)
    ((RTL.Stackframe res tf sp (map_pc (mapping f) pc) rs') :: ts).
Hint Constructors match_stackframes: core.

Set Implicit Arguments.

Variant match_states: RTLpar.state -> RTL.state -> Prop :=
  | match_states_intro:
    forall s ts sp pc rs rs' m f tf
     (WF: wf_function f)
     (MILL: mill_function f)
     (SPEC: transl_function f = Errors.OK tf)
     (STACK: match_stackframes s ts)
     (MREG: match_regset f rs rs'),
      match_states (State s f sp pc rs m) (RTL.State ts tf sp ((map_pc (mapping f)) pc) rs' m)
  | match_states_call:
    forall s ts f tf args m
     (WF: wf_fundef f)
     (MILL: mill_fundef f)
     (SPEC: transl_fundef f = Errors.OK tf)
     (STACK: match_stackframes s ts),
      match_states (Callstate s f args m) (RTL.Callstate ts tf args m)
  | match_states_return:
      forall s ts v m
     (STACK: match_stackframes s ts ),
        match_states (Returnstate s v m) (RTL.Returnstate ts v m).
Hint Constructors match_states: core.

Lemma transf_initial_states:
  forall st1, initial_state prog st1 ->
    exists st2, RTL.initial_state tprog st2 /\ match_states st1 st2.

Lemma transf_final_states:
  forall st1 st2 r,
  match_states st1 st2 -> final_state st1 r -> RTL.final_state st2 r.

Ltac normalized pc :=
  match goal with
    | [NORM : forall (pc: positive) (ins: SSA.instruction), _ ->
          rtldpar_spec ?tmp ?code1 ?pcode1 ?code2 ?R pc |- _] =>
      let Hpc := fresh "Hpc" in
        let Hnorm := fresh "Hnorm" in
        assert (Hpc := NORM pc);
          exploit Hpc ; eauto ; clear Hpc ; intro Hnorm ; inv Hnorm ; allinv ; try congruence
  end;
  try invh map_pamr;
  try match goal with
        | [H: (if ?t_if then _ else _) = _ |- _ ] => destruct t_if ; try congruence ; inv H
      end.

Ltac allinv_par :=
  repeat
    match goal with
      | [H: value ?s = Some ?s' |- _ ] => inv H
      | [ H1: (RTL.fn_code ?tf) ! ?pc = Some _ ,
          H2: (RTL.fn_code ?tf) ! ?pc = Some _ |- _ ] =>
      rewrite H1 in H2; inv H2
      | [ H1: (RTLpar.fn_code ?tf) ! ?pc = Some _ ,
          H2: (RTLpar.fn_code ?tf) ! ?pc = Some _ |- _ ] =>
      rewrite H1 in H2; inv H2
      | [ H1: (RTLpar.fn_parcopycode ?tf) ! ?pc = Some _ ,
          H2: (RTLpar.fn_parcopycode ?tf) ! ?pc = Some _ |- _ ] =>
      rewrite H1 in H2; inv H2
      | _ => idtac
    end.

Lemma exec_seq_parcopy_store_e : forall p rs r,
        (Parmov.exec_seq reg peq val (rev p) (fun r => rs !! r) r =
        (parcopy_store_e (rev p) rs) # r).

Lemma exec_par_parcopy_store : forall f p rs rs' r,
                                 match_regset f rs rs' ->
  forall
    (FRESH : Parmov.move_no_temp reg (fun _ : reg => (fresh_init f))
                                      (parcb_to_moves p))
    (NOFRESH: no_fresh f r),
    (parcopy_store p rs) !! r =
    Parmov.exec_par reg peq val (parcb_to_moves p)
                    (fun r => rs' # r) r.
  
Lemma match_regset_parmoves:
  forall f rs rs' p,
  forall (FRESH : Parmov.move_no_temp reg (fun _ : reg => (fresh_init f)) (parcb_to_moves p))
         (MILL: Parmov.is_mill reg (parcb_to_moves p)),
    match_regset f rs rs' ->
    match_regset f (parcopy_store p rs)
                 (parcopy_store_e (seq_parmoves (fresh_init f) (parcb_to_moves p)) rs').
  
Lemma wf_njp_id : forall f (WF: wf_function f) tf R pc,
  (transl_function_spec f tf R) ->
  forall ins, (fn_code f) ! pc = Some ins ->
  ~ (join_point pc f) ->
  (R pc = pc).

Lemma wf_ninop_id_succ : forall f (WF: wf_function f) tf R pc,
  (transl_function_spec f tf R) ->
  forall ins, (fn_code f) ! pc = Some ins ->
  (forall s, ins <> Inop s) ->
  forall s, In s (successors_instr ins) -> (R s = s).
    

This relation is indeed a simulation

Lemma transl_step_correct:
  forall s1 t s2,
    step ge s1 t s2 ->
    forall s1' (MS: match_states s1 s1'),
      exists s2', plus RTL.step tge s1' t s2' /\ match_states s2 s2'.

Semantics preservation

Theorem transf_program_correct:
  forward_simulation (semantics prog) (RTL.semantics tprog).

  End CORRECTNESS.
  
End PRESERVATION.