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 CSSA.
Require Import SSA.
Require Import SSAutils.
Require Import CSSAgen.
Require Import Kildall.
Require Import Conventions.
Require Import Utils.
Require Import NArith.
Require Import Events.
Require Import Permutation.
Require Import KildallComp.
Require Import DLib.
Require Import CSSAgenspec.
Require Import CSSAutils.
Unset Allow StrictProp.

Ltac sz := unfold Plt, Ple in * ; (zify; lia).

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 Plt_neq :
  forall (r1 r2 : reg),
  Plt r1 r2 ->
  r1 <> r2.

Global Hint Resolve Plt_neq: core.

Lemma nth_error_nil_notSome_node :
  forall k,
  nth_error (nil:list node) k = None.

Lemma nth_error_nil_notSome_reg :
  forall k,
  nth_error (nil:list reg) k = None.

Global Hint Resolve nth_error_nil_notSome_node
  nth_error_nil_notSome_reg: core.

Lemma notIn_notnth:
  forall k (nodes: list node) pc,
  ~ In pc nodes ->
  nth_error nodes k <> Some pc.

Lemma nth_In_reg:
  forall k (regs: list reg) r,
  nth_error regs k = Some r ->
  In r regs.

Global Hint Resolve nth_In_reg: core.

Lemma nth_In_node:
  forall k (nodes: list node) pc,
  nth_error nodes k = Some pc ->
  In pc nodes.

Global Hint Resolve nth_In_node: core.


Lemma add_successors_other :
  forall l pred from pc,
  ~ In pc l ->
  pred !!! pc = (add_successors pred from l) !!! pc.

Lemma add_successors_notfrom :
  forall l pred from pc pc',
  ~ In pc' (pred !!! pc) ->
  pc' <> from ->
  ~ In pc' ((add_successors pred from l) !!! pc).

Lemma not_in_foldelems :
  forall pc pc' elems predinit,
  ~ In pc' (map fst elems) ->
  ~ In pc' (predinit !!! pc) ->
  ~ In pc' (fold_right
      (fun pcins pred =>
        add_successors pred (fst pcins)
          (successors_instr (snd pcins)))
      predinit elems) !!! pc.

Lemma nodups_in_preds_aux :
  forall pc elems predinit,
  (forall pcins,
    In pcins elems ->
    In pc (successors_instr (snd pcins)) ->
    (successors_instr (snd pcins)) = pc :: nil) ->
  (forall elt, In elt elems ->
    ~ In (fst elt) (predinit !!! pc)) ->
  NoDup (map fst elems) ->
  NoDup (predinit !!! pc) ->
  NoDup
    (List.fold_right
      (fun pcins pred =>
        add_successors pred (fst pcins)
          (successors_instr (snd pcins)))
      predinit elems) !!! pc.

Lemma nodups_in_preds :
  forall l f preds pc,
  wf_ssa_function f ->
  preds = make_predecessors (fn_code f) successors_instr ->
  (fn_phicode f) ! pc <> None ->
  preds ! pc = Some (l : list node) ->
  ~ In pc l ->
  NoDup (pc :: l).

Lemma in_successors_if_succofpred :
  forall f pc l k n i,
  (fn_code f) ! n = Some i ->
  (make_predecessors (fn_code f) successors_instr)
    ! pc = Some l ->
  nth_error l k = Some n ->
  In pc ((successors f) !!! n).

Lemma inop_is_not_in_two_preds :
  forall f l pred pc pc',
  (make_predecessors (fn_code f) successors_instr)
    ! pc' = Some l ->
  pc <> pc' ->
  (fn_code f) ! pred = Some (Inop pc) ->
  ~ In pred l.


Lemma ple_foldmaxreg_init :
  forall l m n,
  Ple m n ->
  Ple
    m
    (List.fold_left (fun m r' => Pos.max m (r' : reg))
      l n).

Lemma max_reg_in_list_correct_aux :
  forall l (r : reg) m,
  In r l ->
  Ple r
    (List.fold_left (fun m r' => Pos.max m r') l m).

Lemma max_reg_in_list_correct :
  forall l r,
  In r l ->
  Ple r (max_reg_in_list l).

Lemma max_reg_in_Icall_inl :
  forall r args res x y,
  Ple r
    (get_max_reg_in_ins (Icall x (inl r) args res y)).

Lemma max_reg_in_Itailcall_inl :
  forall r args sig,
  Ple r
    (get_max_reg_in_ins (Itailcall sig (inl r) args)).

Lemma max_reg_in_Icall_args :
  forall ros args arg res sig y,
  In arg args ->
  Ple arg
    (get_max_reg_in_ins (Icall sig ros args res y)).

Lemma max_reg_in_Itailcall_args :
  forall ros args arg sig,
  In arg args ->
  Ple arg
    (get_max_reg_in_ins (Itailcall sig ros args)).

Lemma max_reg_in_Iop_args :
  forall op args arg res pc,
  In arg args ->
  Ple arg
    (get_max_reg_in_ins (Iop op args res pc)).

Lemma max_reg_in_Iload_args :
  forall chunk addr args arg dst pc,
  In arg args ->
  Ple arg
    (get_max_reg_in_ins (Iload chunk addr args dst pc)).

Lemma max_reg_in_Istore_args :
  forall chunk addr args arg src pc,
  In arg args ->
  Ple arg
    (get_max_reg_in_ins (Istore chunk addr args src pc)).

Lemma max_reg_in_Istore_src :
  forall chunk addr args src pc,
  Ple src
    (get_max_reg_in_ins (Istore chunk addr args src pc)).

Lemma max_reg_in_Ibuiltin_args :
  forall ef args arg res pc,
  In arg (params_of_builtin_args args) ->
  Ple arg
    (get_max_reg_in_ins (Ibuiltin ef args res pc)).

Lemma max_reg_in_Icond_args :
  forall cond args arg ifso ifnot,
  In arg args ->
  Ple arg
    (get_max_reg_in_ins (Icond cond args ifso ifnot)).

Lemma max_reg_in_Ijumptable_arg :
  forall arg tbl,
  Ple arg
    (get_max_reg_in_ins (Ijumptable arg tbl)).

Lemma max_reg_in_Ireturn_r :
  forall r,
  Ple r
    (get_max_reg_in_ins (Ireturn (Some r))).

Lemma max_reg_in_phi_dst :
  forall dst args,
  Ple dst (get_max_reg_in_phiins (Iphi args dst)).

Lemma max_reg_in_phi_arg :
  forall dst args arg,
  In arg args ->
  Ple arg (get_max_reg_in_phiins (Iphi args dst)).

Lemma ple_foldmaxphi_init :
  forall l m n,
  Ple m n ->
  Ple
    m
    (List.fold_left (fun m phi => Pos.max m
      (get_max_reg_in_phiins phi))
      l n).

Lemma max_reg_in_phib_dst_aux :
  forall phib dst args init,
  In (Iphi args dst) phib ->
  Ple (get_max_reg_in_phiins (Iphi args dst))
    (List.fold_left (fun m phiins => Pos.max m
      (get_max_reg_in_phiins phiins))
      phib init).

Lemma max_reg_in_phib_dst :
  forall phib dst args,
  In (Iphi args dst) phib ->
  Ple (get_max_reg_in_phiins (Iphi args dst))
    (get_max_reg_in_phib phib).

Lemma ple_foldmaxphib_init :
  forall l m n,
  Ple m n ->
  Ple
    m
    (List.fold_left
      (fun m (pphib : positive * phiblock) => Pos.max m
        (get_max_reg_in_phib (snd pphib)))
      l n).

Lemma ple_foldmaxins_init :
  forall l m n,
  Ple m n ->
  Ple
    m
    (List.fold_left
      (fun m (pcins : positive * instruction) => Pos.max m
        (get_max_reg_in_ins (snd pcins)))
      l n).

Lemma max_reg_in_phicode_aux :
  forall elems init pphib (pc:positive) phib,
  In pphib elems ->
  pphib = (pc, phib) ->
  Ple (get_max_reg_in_phib phib)
    (fold_left
      (fun m p =>
        Pos.max m (get_max_reg_in_phib (snd p)))
    elems init).

Lemma max_reg_in_code_aux :
  forall elems pcins (pc:positive) ins init,
  In pcins elems ->
  pcins = (pc, ins) ->
  Ple (get_max_reg_in_ins ins)
    (fold_left
        (fun m p => Pos.max m (get_max_reg_in_ins (snd p)))
      elems init).

Lemma max_reg_in_phicode :
  forall phicode pc phib,
  phicode ! pc = Some phib ->
  Ple (get_max_reg_in_phib phib)
    (get_max_reg_in_phicode phicode).

Lemma max_reg_in_code :
  forall code pc ins,
  code ! pc = Some ins ->
  Ple (get_max_reg_in_ins ins)
    (get_max_reg_in_code code).

Lemma max_reg_correct_phicode :
  forall f,
  Ple (get_max_reg_in_phicode (fn_phicode f))
    (get_maxreg f).

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


Lemma wf_unique_def_phib_aux :
  forall phib,
  NoDup phib ->
  (forall (r : reg) (args0 args' : list reg),
    In (Iphi args0 r) phib ->
    In (Iphi args' r) phib -> args0 = args') ->
  unique_def_phib_spec phib.

Lemma wf_unique_def_phib :
  forall phib f pc,
  SSA.wf_ssa_function f ->
  (fn_phicode f) ! pc = Some phib ->
  unique_def_phib_spec phib.

Lemma notinpredspc :
  forall f pc preds phib,
  normalized_jp f ->
  (fn_phicode f) ! pc = Some phib ->
  (make_predecessors (fn_code f) successors_instr)
    ! pc = Some preds ->
  ~ In pc preds.


Lemma initialize_phi_block_correct :
  forall x pc s s' INCR,
  initialize_phi_block pc s = OK x s' INCR ->
  (st_phicode s') ! pc = Some nil.

Lemma initialize_parcopy_block_correct :
  forall x pc s s' INCR,
  initialize_parcopy_block pc s = OK x s' INCR ->
  (st_parcopycode s') ! pc = Some nil.

Lemma initialize_parcopy_block_correct2 :
  forall pc' x pc s s' INCR,
  initialize_parcopy_block pc' s = OK x s' INCR ->
  (st_parcopycode s) ! pc = Some nil ->
  (st_parcopycode s') ! pc = Some nil.

Lemma initialize_parcopy_blocks_correct_aux :
  forall l x pc s s' INCR,
  initialize_parcopy_blocks l s = OK x s' INCR ->
  (st_parcopycode s) ! pc = Some nil ->
  (st_parcopycode s') ! pc = Some nil.

Lemma initialize_parcopy_blocks_correct :
  forall l x pc s s' INCR,
  initialize_parcopy_blocks l s = OK x s' INCR ->
  In pc l ->
  (st_parcopycode s') ! pc = Some nil.

Global Hint Resolve initialize_parcopy_blocks_correct: core.

Lemma initialize_parcopy_blocks_correct_parcother :
  forall l x pc s s' INCR,
  initialize_parcopy_blocks l s = OK x s' INCR ->
  ~ In pc l ->
  (st_parcopycode s) ! pc = (st_parcopycode s') ! pc.

Lemma initialize_parcopy_blocks_correct_other :
  forall l u s s' INCR,
  initialize_parcopy_blocks l s = OK u s' INCR ->
  st_phicode s = st_phicode s'.

Inductive gen_new_regs_spec (maxreg : positive)
    (fs_init : positive)
    : positive -> list reg -> list reg -> Prop :=
| gen_new_regs_spec_nil:
    forall (GNRSPECinitnil: Plt maxreg fs_init),
    gen_new_regs_spec maxreg fs_init fs_init
      nil nil
| gen_new_regs_spec_cons:
    forall arg args arg' args' fs_max
    (GNRSPECinit: arg' = fs_init)
    (GNRSPECold: Ple arg maxreg)
    (GNRSPECfresh: Plt maxreg arg')
    (GNRSPECrec:
      gen_new_regs_spec maxreg (Pos.succ fs_init) fs_max
        args args'),
    gen_new_regs_spec maxreg fs_init fs_max
      (arg :: args) (arg' :: args').

Lemma gen_new_regs_spec_incr :
  forall maxreg fs_init fs_max args args',
  gen_new_regs_spec maxreg fs_init fs_max
    args args' ->
  Ple fs_init fs_max.

Global Hint Resolve gen_new_regs_spec_incr: core.

Lemma gen_new_regs_spec_ple_arg_maxreg :
  forall maxreg fs_init fs_max args args',
  gen_new_regs_spec maxreg fs_init fs_max
    args args' ->
  forall k arg,
    nth_error args k = Some arg ->
  Ple arg maxreg.

Lemma gen_new_regs_spec_plt_maxreg_arg' :
  forall maxreg fs_init fs_max args args',
  gen_new_regs_spec maxreg fs_init fs_max
    args args' ->
  forall k arg',
    nth_error args' k = Some arg' ->
  Plt maxreg arg'.

Lemma gen_new_regs_spec_max_in :
  forall maxreg fs_init fs_max args args',
  gen_new_regs_spec maxreg fs_init fs_max
    args args' ->
  (forall arg', In arg' args' -> Plt arg' fs_max).

Lemma gen_new_regs_spec_min_in :
  forall maxreg fs_init fs_max args args',
  gen_new_regs_spec maxreg fs_init fs_max
    args args' ->
  (forall arg', In arg' args' -> Ple fs_init arg').

Global Hint Resolve gen_new_regs_spec_min_in: core.

Lemma gen_new_regs_spec_nthNotNonefromNotNone :
  forall maxreg fs_init fs_max args args',
  gen_new_regs_spec maxreg fs_init fs_max
    args args' ->
  forall k,
  nth_error args k <> None
  -> nth_error args' k <> None.

Global Hint Resolve gen_new_regs_spec_nthNotNonefromNotNone: core.

Lemma gen_new_regs_spec_nthNotNonetoNotNone :
  forall maxreg fs_init fs_max args args',
  gen_new_regs_spec maxreg fs_init fs_max
    args args' ->
  forall k,
  nth_error args' k <> None
  -> nth_error args k <> None.

Global Hint Resolve gen_new_regs_spec_nthNotNonetoNotNone: core.

Lemma gen_new_regs_correct :
  forall args s s' args' INCR maxreg,
  (Plt maxreg (next_fresh_reg s)) ->
  (forall arg, In arg args -> Ple arg maxreg) ->
  gen_new_regs args s = OK args' s' INCR ->
  gen_new_regs_spec maxreg (next_fresh_reg s)
    (next_fresh_reg s') args args'.

Global Hint Resolve gen_new_regs_correct: core.

Lemma gen_new_regs_correct_parcode :
  forall args s args' s' INCR,
  gen_new_regs args s = OK args' s' INCR ->
  st_parcopycode s = st_parcopycode s'.

Global Hint Resolve gen_new_regs_correct_parcode: core.

Lemma gen_new_regs_correct_phicode :
  forall args s args' s' INCR,
  gen_new_regs args s = OK args' s' INCR ->
  st_phicode s = st_phicode s'.

Global Hint Resolve gen_new_regs_correct_phicode: core.

Lemma add_parcopies_correct_fresh :
  forall parcopies copy_nodes s u s' INCR,
  add_parcopies parcopies copy_nodes s = OK u s' INCR ->
  (next_fresh_reg s) = (next_fresh_reg s').

Global Hint Resolve add_parcopies_correct_fresh: core.

Lemma add_parcopies_correct_phicode :
  forall parcopies copy_nodes s u s' INCR,
  add_parcopies parcopies copy_nodes s = OK u s' INCR ->
  st_phicode s = st_phicode s'.

Global Hint Resolve add_parcopies_correct_phicode: core.

Inductive add_parcopies_spec (pcode1 : parcopycode) :
  list parcopy -> list node
    -> parcopycode ->
  Prop :=
| add_parcopies_spec_nil:
    add_parcopies_spec pcode1 nil nil pcode1
| add_parcopies_spec_cons:
    forall pc parcb pcode2 parcopy copy_nodes
      parcopies
    (APSPECparcb: pcode2 ! pc = Some parcb)
    (APSPECnodup: ~ In pc copy_nodes)
    (APSPECrec:
      add_parcopies_spec pcode1 parcopies copy_nodes
        pcode2),
    add_parcopies_spec pcode1 (parcopy :: parcopies)
      (pc :: copy_nodes)
      (PTree.set pc (parcopy :: parcb) pcode2).

Lemma add_parcopies_spec_correct_other :
  forall pcode1 parcopies copy_nodes pcode2,
  add_parcopies_spec pcode1 parcopies copy_nodes pcode2 ->
  forall pc,
  ~ In pc copy_nodes ->
  pcode1 ! pc = pcode2 ! pc.

Global Hint Resolve add_parcopies_spec_correct_other: core.

Lemma add_parcopies_k_notSomefromNone :
  forall parcode1 parcopies copy_nodes parcode2,
  add_parcopies_spec parcode1 parcopies
    copy_nodes parcode2 ->
  forall pc,
  parcode2 ! pc <> None -> parcode1 ! pc <> None.

Lemma add_parcopies_k :
  forall pcode1 parcopies copy_nodes pcode2,
  add_parcopies_spec pcode1 parcopies copy_nodes pcode2 ->
  forall k pred parcopy parcb,
  nth_error copy_nodes k = Some pred ->
  nth_error parcopies k = Some parcopy ->
  pcode1 ! pred = Some parcb ->
  pcode2 ! pred = Some (parcopy :: parcb).

Lemma add_parcopies_pred_exist_parcb :
  forall pcode1 parcopies copy_nodes pcode2,
  add_parcopies_spec pcode1 parcopies copy_nodes pcode2 ->
  forall pred (parcb parcb0 : parcopyblock),
  In pred copy_nodes ->
  pcode1 ! pred = Some parcb0 ->
  exists parcb,
  pcode2 ! pred = Some parcb.

Lemma add_parcopies_nth_notNonetonotNone :
  forall pcode1 parcopies copy_nodes pcode2,
  add_parcopies_spec pcode1 parcopies copy_nodes pcode2 ->
  forall k,
  nth_error copy_nodes k <> None ->
  nth_error parcopies k <> None.

Global Hint Resolve add_parcopies_nth_notNonetonotNone: core.

Lemma add_parcopies_correct :
  forall copy_nodes s parcopies u s' INCR,
  NoDup copy_nodes ->
  add_parcopies parcopies copy_nodes s = OK u s' INCR ->
  add_parcopies_spec (st_parcopycode s) parcopies copy_nodes
    (st_parcopycode s').

Global Hint Resolve add_parcopies_correct: core.

Inductive build_parcopies_spec :
  list reg -> list reg -> list parcopy -> Prop :=
| build_parcopies_spec_nil:
    build_parcopies_spec nil nil nil
| build_parcopies_spec_cons:
    forall arg arg' args args' parcopies,
    build_parcopies_spec args args' parcopies ->
    build_parcopies_spec (arg :: args) (arg' :: args')
      (Iparcopy arg arg' :: parcopies).

Lemma build_parcopies_correct:
  forall args args' s parcopies s' INCR,
  build_parcopies args args' s = OK parcopies s' INCR ->
  build_parcopies_spec args args' parcopies.

Global Hint Resolve build_parcopies_correct: core.

Lemma build_parcopies_nth:
  forall args args' parcopies,
  build_parcopies_spec args args' parcopies ->
  forall k arg arg',
  nth_error args k = Some arg ->
  nth_error args' k = Some arg' ->
  nth_error parcopies k = Some (Iparcopy arg arg').

Global Hint Resolve build_parcopies_nth: core.

Lemma build_parcopies_nth_revargs:
  forall args args' parcopies,
  build_parcopies_spec args args' parcopies ->
  forall k,
  nth_error parcopies k <> None ->
  nth_error args k <> None.

Global Hint Resolve build_parcopies_nth_revargs: core.

Lemma build_parcopies_correct_phicode:
  forall args args' s parcopies s' INCR,
  build_parcopies args args' s = OK parcopies s' INCR ->
  st_phicode s = st_phicode s'.

Global Hint Resolve build_parcopies_correct_phicode: core.

Lemma build_parcopies_correct_fresh:
  forall args args' s parcopies s' INCR,
  build_parcopies args args' s = OK parcopies s' INCR ->
  (next_fresh_reg s) = (next_fresh_reg s').

Global Hint Resolve build_parcopies_correct_fresh: core.

Lemma build_parcopies_correct_parcopycode:
  forall args args' s parcopies s' INCR,
  build_parcopies args args' s = OK parcopies s' INCR ->
  st_parcopycode s = st_parcopycode s'.

Global Hint Resolve build_parcopies_correct_parcopycode: core.

Variant add_parcopy_spec (pc : node): reg -> reg -> parcopycode -> parcopycode -> Prop :=
| add_parcopy_spec_intro:
    forall dst' dst parcode parcb,
    parcode ! pc = Some parcb ->
    add_parcopy_spec pc dst' dst
      parcode (PTree.set pc
        ((Iparcopy dst' dst) :: parcb) parcode).

Lemma add_parcopy_correct:
  forall dst' dst pc s u s' INCR,
  add_parcopy (Iparcopy dst' dst) pc s = OK u s' INCR ->
  add_parcopy_spec pc dst' dst
    (st_parcopycode s) (st_parcopycode s').

Global Hint Resolve add_parcopy_correct: core.

Lemma add_parcopy_correct_phicode:
  forall dst' dst pc s u s' INCR,
  add_parcopy (Iparcopy dst' dst) pc s = OK u s' INCR ->
  st_phicode s = st_phicode s'.

Global Hint Resolve add_parcopy_correct_phicode: core.

Lemma add_parcopy_correct_fresh:
  forall dst' dst pc s u s' INCR,
  add_parcopy (Iparcopy dst' dst) pc s = OK u s' INCR ->
  (next_fresh_reg s) = (next_fresh_reg s').

Global Hint Resolve add_parcopy_correct_fresh: core.

Lemma add_new_phi_correct_fresh:
  forall dst' args' pc s u s' INCR,
  add_new_phi dst' args' pc s = OK u s' INCR ->
  (next_fresh_reg s) = (next_fresh_reg s').

Global Hint Resolve add_new_phi_correct_fresh: core.

Lemma add_new_phi_correct_parcode:
  forall dst' args' pc s u s' INCR,
  add_new_phi dst' args' pc s = OK u s' INCR ->
  st_parcopycode s = st_parcopycode s'.

Global Hint Resolve add_new_phi_correct_parcode: core.

Lemma add_new_phi_correct_phicodeNotNone:
  forall dst' args' pc s u s' INCR,
  add_new_phi dst' args' pc s = OK u s' INCR ->
  (st_phicode s) ! pc <> None.

Global Hint Resolve add_new_phi_correct_phicodeNotNone: core.

Variant add_new_phi_spec (pc : node) : reg -> list reg -> phicode -> phicode -> Prop :=
| add_new_phi_spec_intro:
    forall dst' args' phicode phib',
      phicode ! pc = Some phib' ->
      add_new_phi_spec pc dst' args'
                       phicode
                       (PTree.set pc (Iphi args' dst' :: phib') phicode).

Lemma add_new_phi_correct:
  forall dst' args' pc s u s' INCR,
  add_new_phi dst' args' pc s = OK u s' INCR ->
  add_new_phi_spec pc dst' args'
    (st_phicode s) (st_phicode s').

Global Hint Resolve add_new_phi_correct: core.

Inductive handle_phi_block_spec (maxreg: positive)
  (preds : list node) (pc : node)
  : phiblock -> positive -> positive ->
    phicode -> phicode ->
    parcopycode -> parcopycode ->
    Prop :=
| handle_phi_block_spec_nil:
    forall phicode parcode fs_init,
    handle_phi_block_spec maxreg preds pc
      nil fs_init fs_init
      phicode phicode
      parcode parcode
| handle_phi_block_spec_cons:
    forall args dst args' dst'
      block
      fs_init fs_next fs_last
      parcopies
      parcode1 parcode2 parcode3 parcode4
      phicode1 phicode2 phicode3

    (PBSPECargsfresh:
      (forall arg, In arg args -> Ple arg maxreg))
    (PBSPECdst_old: Ple dst maxreg)
    (PBSPECfs_init_fresh: Plt maxreg fs_init)

    (PBSPECnewreg: dst' = fs_init)
    (PBSPECgen_new_regs:
      gen_new_regs_spec maxreg (Pos.succ fs_init) fs_next
        args args')

    (PBSPECrec:
      handle_phi_block_spec maxreg preds pc
        block fs_next fs_last
        phicode1 phicode2 parcode1 parcode2)

    (PBSPECparcopies:
      build_parcopies_spec args args' parcopies)
    (PBSPECadd_parcopy:
      add_parcopy_spec pc dst' dst parcode2 parcode3)
    (PBSPECadd_parcopies:
      add_parcopies_spec parcode3 parcopies preds parcode4)
    (PBSPECnew_phi:
      add_new_phi_spec pc dst' args' phicode2 phicode3),

    handle_phi_block_spec maxreg preds pc
      (Iphi args dst :: block) fs_init fs_last
      phicode1 phicode3
      parcode1 parcode4.

Lemma handle_phi_block_spec_incr :
  forall maxreg preds pc block fs_init fs_last
    phicode1 phicode2 parcode1 parcode2,
  handle_phi_block_spec maxreg preds pc
    block fs_init fs_last phicode1 phicode2
      parcode1 parcode2 ->
  Ple fs_init fs_last.

Global Hint Resolve handle_phi_block_spec_incr: core.

Lemma handle_phi_block_spec_ple_init_arg :
  forall maxreg preds pc block fs_init fs_last
    phicode1 phicode2 parcode1 parcode2,
  handle_phi_block_spec maxreg preds pc
    block fs_init fs_last
    phicode1 phicode2 parcode1 parcode2 ->
  forall arg' args' dst' phib',
  phicode1 ! pc = Some nil ->
  phicode2 ! pc = Some phib' ->
  In (Iphi args' dst') phib' ->
  In arg' args' ->
  Ple fs_init arg'.

Lemma handle_phi_block_spec_ple_init_dst :
  forall maxreg preds pc block fs_init fs_last
    phicode1 phicode2 parcode1 parcode2,
  handle_phi_block_spec maxreg preds pc
    block fs_init fs_last
    phicode1 phicode2 parcode1 parcode2 ->
  forall args' dst' phib',
  phicode1 ! pc = Some nil ->
  phicode2 ! pc = Some phib' ->
  In (Iphi args' dst') phib' ->
  Ple fs_init dst'.

Ltac normalize_new_phi :=
  match goal with
  | [ H: ((PTree.set ?pc (Iphi ?args'0 ?dst'0 :: ?phib'0)
          ?phicode) ! ?pc =
          Some (Iphi ?args' ?dst' :: ?phib'))
    |- _ ] =>
      rewrite PTree.gss in H;
      assert (EQ1: args' = args'0) by congruence;
      assert (EQ2: dst' = dst'0) by congruence;
      assert (EQ3: phib' = phib'0) by congruence;
      rewrite EQ1 in *; rewrite EQ2 in *;
      rewrite EQ3 in *
  | _ => idtac
  end.

Lemma handle_phi_block_spec_plt_arg :
  forall maxreg preds pc block fs_next fs_last
    phicode1 phicode2 parcode1 parcode2,
  handle_phi_block_spec maxreg preds pc
    block fs_next fs_last
    phicode1 phicode2 parcode1 parcode2 ->
  phicode1 ! pc = Some nil ->
  forall phib' dst' args' (arg':reg)
    args'' arg'' arg' dst'',
  phicode2 ! pc = Some (Iphi args' dst' :: phib') ->
  In (Iphi args'' dst'') phib' ->
  In arg' args' ->
  In arg'' args'' ->
  Plt arg' arg''.

Lemma handle_phi_block_spec_plt_dst :
  forall maxreg preds pc block fs_next fs_last
    phicode1 phicode2 parcode1 parcode2,
  handle_phi_block_spec maxreg preds pc
    block fs_next fs_last
    phicode1 phicode2 parcode1 parcode2 ->
  phicode1 ! pc = Some nil ->
  forall phib' dst' args' (arg':reg)
    args'' dst'',
  phicode2 ! pc = Some (Iphi args' dst' :: phib') ->
  In (Iphi args'' dst'') phib' ->
  Plt dst' dst''.

Lemma handle_phi_block_spec_fresh1 :
  forall maxreg preds pc block fs_next fs_last
    phicode1 phicode2 parcode1 parcode2,
  handle_phi_block_spec maxreg preds pc
    block fs_next fs_last
    phicode1 phicode2 parcode1 parcode2 ->
  forall arg' k phib' dst' args',
  phicode1 ! pc = Some nil ->
  phicode2 ! pc = Some (Iphi args' dst' :: phib') ->
  forall (args'' : list reg) (arg'' dst'' : reg),
  In (Iphi args'' dst'') phib' ->
  nth_error args'' k = Some arg'' ->
  nth_error args' k = Some arg' ->
  arg' <> arg''.

Lemma handle_phi_block_spec_fresh2 :
  forall maxreg preds pc block fs_next fs_last
    phicode1 phicode2 parcode1 parcode2,
  handle_phi_block_spec maxreg preds pc
    block fs_next fs_last
    phicode1 phicode2 parcode1 parcode2 ->
  forall phib' dst' args',
  phicode1 ! pc = Some nil ->
  phicode2 ! pc = Some (Iphi args' dst' :: phib') ->
  forall (args'' : list reg) (arg'' dst'' : reg),
  In (Iphi args'' dst'') phib' ->
  dst' <> dst''.

Lemma handle_phi_block_spec_fresh3 :
  forall maxreg preds pc,
  NoDup (pc :: preds) ->
  forall block fs_next fs_last
    phicode1 phicode2 parcode1 parcode2,
  handle_phi_block_spec maxreg preds pc
    block fs_next fs_last
    phicode1 phicode2 parcode1 parcode2 ->
  forall arg' k phib' dst' args',
  phicode1 ! pc = Some nil ->
  phicode2 ! pc = Some (Iphi args' dst' :: phib') ->
  forall args'' dst'',
  In (Iphi args'' dst'') phib' ->
  nth_error args' k = Some arg' ->
  arg' <> dst''.

Lemma handle_phi_block_spec_exists_phib' :
  forall maxreg preds pc block fs_next fs_last
    phicode1 phicode2 parcode1 parcode2 phib,
  handle_phi_block_spec maxreg preds pc
    block fs_next fs_last
    phicode1 phicode2 parcode1 parcode2 ->
  phicode1 ! pc = Some phib ->
  exists phib',
  phicode2 ! pc = Some phib'.

Lemma handle_phi_block_spec_exists_parcb' :
  forall maxreg preds pc block fs_next fs_last
    phicode1 phicode2 parcode1 parcode2,
  NoDup (pc :: preds) ->
  handle_phi_block_spec maxreg preds pc
    block fs_next fs_last
    phicode1 phicode2 parcode1 parcode2 ->
  parcode1 ! pc = Some nil ->
  exists parcb',
  parcode2 ! pc = Some parcb'.

Lemma handle_phi_block_spec_exists_parcb :
  forall maxreg preds pc block fs_next fs_last
    phicode1 phicode2 parcode1 parcode2 pred,
  NoDup (pc :: preds) ->
  handle_phi_block_spec maxreg preds pc
    block fs_next fs_last
    phicode1 phicode2 parcode1 parcode2 ->
  In pred preds ->
  parcode1 ! pred = Some nil ->
  exists parcb,
  parcode2 ! pred = Some parcb.

Lemma handle_phi_block_spec_preserves_parcother :
  forall maxreg preds pc block fs_next fs_last
    phicode1 phicode2 parcode1 parcode2,
  handle_phi_block_spec maxreg preds pc
    block fs_next fs_last
    phicode1 phicode2 parcode1 parcode2 ->
  forall pc',
  NoDup (pc :: preds) ->
  pc' <> pc ->
  ~ In pc' preds ->
  parcode1 ! pc' = parcode2 ! pc'.

Lemma handle_phi_block_spec_preserves_phibother :
  forall maxreg preds pc block fs_next fs_last
    phicode1 phicode2 parcode1 parcode2,
  handle_phi_block_spec maxreg preds pc
    block fs_next fs_last
    phicode1 phicode2 parcode1 parcode2 ->
  forall pc',
  pc' <> pc ->
  phicode1 ! pc' = phicode2 ! pc'.

Lemma handle_phi_block_correct :
  forall maxreg preds pc,
  NoDup (pc :: preds) ->
  forall block s u s' INCR,
  (forall args dst, In (Iphi args dst) block
    -> Ple dst maxreg) ->
  (forall args dst, In (Iphi args dst) block ->
    forall arg, In arg args -> Ple arg maxreg) ->
  (Plt maxreg (next_fresh_reg s)) ->
  handle_phi_block preds block pc s = OK u s' INCR ->
  handle_phi_block_spec maxreg preds pc
    block (next_fresh_reg s) (next_fresh_reg s')
    (st_phicode s) (st_phicode s')
    (st_parcopycode s) (st_parcopycode s').

Lemma handle_phi_block_spec_equiv_phib :
  forall maxreg preds pc,
  NoDup (pc :: preds) ->
  forall phib fs_init fs_last
    phicode1 phicode2 parcode1 parcode2
    k pred,
  handle_phi_block_spec maxreg preds pc
    phib fs_init fs_last
    phicode1 phicode2
    parcode1 parcode2 ->
  forall parcb parcb' phib',
  parcode1 ! pc = Some nil ->
  phicode1 ! pc = Some nil ->
  parcode2 ! pc = Some parcb' ->
  phicode2 ! pc = Some phib' ->
  nth_error preds k = Some pred ->
  parcode1 ! pred = Some nil ->
  parcode2 ! pred = Some parcb ->
  equiv_phib_spec maxreg k phib parcb phib' parcb'.

Lemma equiv_phib_spec_plt_maxreg_phib'dst :
  forall maxreg k phib parcb phib' parcb',
  equiv_phib_spec maxreg k phib parcb phib' parcb' ->
  forall args' dst',
  In (Iphi args' dst') phib' ->
  Plt maxreg dst'.

Lemma equiv_phib_spec_plt_maxreg_phib'arg :
  forall maxreg k phib parcb phib' parcb',
  equiv_phib_spec maxreg k phib parcb phib' parcb' ->
  forall arg' args' dst',
  In (Iphi args' dst') phib' ->
  nth_error args' k = Some arg' ->
  Plt maxreg arg'.

Lemma equiv_phib_spec_parcbdst_inphib' :
  forall maxreg k phib parcb phib' parcb',
  equiv_phib_spec maxreg k phib parcb phib' parcb' ->
  forall arg arg',
  In (Iparcopy arg arg') parcb ->
  exists args' dst',
  nth_error args' k = Some arg' /\
  In (Iphi args' dst') phib'.

Lemma equiv_phib_spec_parcb'src_inphib' :
  forall maxreg k phib parcb phib' parcb',
  equiv_phib_spec maxreg k phib parcb phib' parcb' ->
  forall dst dst',
  In (Iparcopy dst' dst) parcb' ->
  exists args',
  In (Iphi args' dst') phib'.

Lemma equiv_phib_spec_parcb'dst_inphib :
  forall maxreg k phib parcb phib' parcb',
  equiv_phib_spec maxreg k phib parcb phib' parcb' ->
  forall dst dst',
  In (Iparcopy dst' dst) parcb' ->
  exists args,
  In (Iphi args dst) phib.

Lemma equiv_phib_spec_ple_phibdst_maxreg :
  forall maxreg k phib parcb phib' parcb',
  equiv_phib_spec maxreg k phib parcb phib' parcb' ->
  forall args dst,
  In (Iphi args dst) phib ->
  Ple dst maxreg.

Lemma equiv_phib_spec_correct :
  forall maxreg k phib parcb phib' parcb',
  unique_def_phib_spec phib ->
  equiv_phib_spec maxreg k phib parcb phib' parcb' ->
  equiv_phib maxreg k phib parcb phib' parcb'.


Lemma nodupnth_get_index :
  forall l pc k,
  NoDup l ->
  nth_error l k = Some pc ->
  get_index l pc = Some k.

Lemma index_pred_from_nth :
  forall l pc k pc' preds,
  NoDup (pc :: l) ->
  preds ! pc = Some l ->
  nth_error l k = Some pc' ->
  index_pred preds pc' pc = Some k.

Lemma handle_phi_block_spec_from_handle_phi_block :
  forall f pc preds s1 s s0 s2 x x0 u
    INCR INCR1 INCR2 phib,
  (make_predecessors (fn_code f) successors_instr) ! pc = Some preds ->
  wf_ssa_function f ->
  Plt (get_maxreg f) (next_fresh_reg s1) ->
  initialize_phi_block pc s1 = OK x s INCR ->
  initialize_parcopy_blocks (pc :: preds) s = OK x0 s0 INCR1 ->
  normalized_jp f ->
  (fn_phicode f) ! pc = Some phib ->
  handle_phi_block preds phib pc s0 = OK u s2 INCR2 ->
  handle_phi_block_spec (get_maxreg f) preds pc
    phib
    (next_fresh_reg s0)
    (next_fresh_reg s2)
    (st_phicode s0) (st_phicode s2)
    (st_parcopycode s0) (st_parcopycode s2).

Lemma copy_node_cssagen_spec_parcode_other :
  forall f pc s1 s2 incr pc' phib preds,
  wf_ssa_function f ->
  normalized_jp f ->
  copy_node
    (make_predecessors (fn_code f) successors_instr)
    (fn_code f) (fn_phicode f) pc s1
    = OK tt s2 incr ->
  (fn_phicode f) ! pc = Some phib ->
  (make_predecessors (fn_code f) successors_instr)
    ! pc = Some preds ->
  pc' <> pc ->
  ~ In pc' preds ->
  Plt (get_maxreg f) (next_fresh_reg s1) ->
  (st_parcopycode s1) ! pc' = (st_parcopycode s2) ! pc'.

Lemma copy_node_cssagen_spec_phicode_other :
  forall f pc s1 s2 u incr pc' phib preds,
  wf_ssa_function f ->
  normalized_jp f ->
  copy_node
    (make_predecessors (fn_code f) successors_instr)
    (fn_code f) (fn_phicode f) pc s1
    = OK u s2 incr ->
  (fn_phicode f) ! pc = Some phib ->
  (make_predecessors (fn_code f) successors_instr)
    ! pc = Some preds ->
  pc' <> pc ->
  Plt (get_maxreg f) (next_fresh_reg s1) ->
  (st_phicode s1) ! pc' = (st_phicode s2) ! pc'.

Lemma copy_node_cssagenspec_other :
  forall f s1 pc k s2 pc' incr phib,
  cssa_spec
    (get_maxreg f)
    (make_predecessors (fn_code f) successors_instr)
    (fn_code f)
    (fn_phicode f) (st_phicode s1)
    (st_parcopycode s1)
    pc k ->
  wf_ssa_function f ->
  normalized_jp f ->
  Plt (get_maxreg f) (next_fresh_reg s1) ->
  copy_node
    (make_predecessors (fn_code f) successors_instr)
    (fn_code f) (fn_phicode f) pc' s1
    = OK tt s2 incr ->
  (fn_phicode f) ! pc = Some phib ->
  pc <> pc' ->
  cssa_spec
    (get_maxreg f)
    (make_predecessors (fn_code f) successors_instr)
    (fn_code f)
    (fn_phicode f) (st_phicode s2)
    (st_parcopycode s2)
    pc k.

Lemma copy_node_cssagenspec_other_mfold :
  forall f,
  wf_ssa_function f ->
  normalized_jp f ->
  forall l s1 pc k s2 u incr,
  cssa_spec
    (get_maxreg f)
    (make_predecessors (fn_code f) successors_instr)
    (fn_code f)
    (fn_phicode f) (st_phicode s1)
    (st_parcopycode s1)
    pc k ->
  mfold_unit (copy_node
    (make_predecessors (fn_code f) successors_instr)
    (fn_code f) (fn_phicode f))
    l s1 = OK u s2 incr ->
  ~ In pc l ->
  Plt (get_maxreg f) (next_fresh_reg s1) ->
  cssa_spec
    (get_maxreg f)
    (make_predecessors (fn_code f) successors_instr)
    (fn_code f)
    (fn_phicode f) (st_phicode s2)
    (st_parcopycode s2)
    pc k.

Lemma copy_node_cssagenspec :
  forall f pc s1 s2 incr k,
    wf_ssa_function f ->
    normalized_jp f ->
    Plt (get_maxreg f) (next_fresh_reg s1) ->
    copy_node
      (make_predecessors (fn_code f) successors_instr)
      (fn_code f) (fn_phicode f) pc s1
      = OK tt s2 incr ->
    cssa_spec
      (get_maxreg f)
      (make_predecessors (fn_code f) successors_instr)
      (fn_code f)
      (fn_phicode f) (st_phicode s2)
      (st_parcopycode s2)
      pc k.

Lemma mfold_copy_node_correct :
  forall f,
  wf_ssa_function f ->
  normalized_jp f ->
  forall l pc
    u s s' incr k,
  mfold_unit (copy_node
    (make_predecessors (fn_code f) successors_instr)
    (fn_code f) (fn_phicode f))
    l s = OK u s' incr ->
  Plt (get_maxreg f) (next_fresh_reg s) ->
  NoDup l ->
  In pc l ->
  cssa_spec (get_maxreg f)
    (make_predecessors (fn_code f) successors_instr)
    (fn_code f) (fn_phicode f)
    (st_phicode s') (st_parcopycode s') pc k.

Normalisations validators proofs

Lemma inops_checker_correct :
  forall f,
  wf_ssa_function f ->
  check_jp_inops f = true ->
  inop_in_jp f.

Lemma normalisation_checker_correct_aux :
  forall f,
  check_joinpoints f = true ->
  forall pc succ,
  (fn_code f) ! pc = Some (Inop succ) ->
  (fn_phicode f) ! succ <> None ->
  (fn_phicode f) ! pc = None.

Lemma In_nth_error : forall l (pc : node),
  In pc l ->
  exists k, nth_error l k = Some pc.

Lemma normalisation_checker_correct :
  forall f,
  wf_ssa_function f ->
  check_joinpoints f = true ->
  normalized_jp f.

Proof of the transformation specification

Lemma transl_function_charact:
  forall f tf,
  wf_ssa_function f ->
  transl_function f = Errors.OK tf ->
  tr_function f tf.

Lemma transl_function_spec_ok : forall f tf,
  normalized_jp f ->
  tr_function f tf ->
  transl_function_spec f tf.

Require Import Linking.

Section PRESERVATION.

  Definition match_prog (p: SSA.program) (tp: CSSA.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: SSA.program.
    Variable tprog: CSSA.program.
    Hypothesis TRANSF_PROG: match_prog prog tprog.
    Hypothesis WF_PROG : wf_ssa_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.

    Variant match_regset (max_reg: positive) : SSA.regset -> SSA.regset -> Prop :=
    | mrg_intro : forall rs rs',
        (forall r, (Ple r max_reg) -> rs# r = rs'# r) ->
        match_regset max_reg rs rs'.

    Inductive match_stackframes :
      list stackframe -> list CSSA.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))
               (WFF: wf_ssa_function f)
               (MREG: match_regset (get_maxreg f) rs rs'),
          match_stackframes
            ((Stackframe res f sp pc rs) :: s)
            ((CSSA.Stackframe res tf sp pc rs') :: ts).

    Hint Constructors match_stackframes: core.

    Set Implicit Arguments.
    
    Variant match_states: SSA.state -> CSSA.state -> Prop :=
    | match_states_intro:
        forall s ts sp pc rs rs' m f tf
               (SPEC: transl_function f = Errors.OK tf)
               (STACK: match_stackframes s ts)
               (WFF: wf_ssa_function f)
               (MREG: match_regset (get_maxreg f) rs rs'),
          match_states (State s f sp pc rs m)
                       (CSSA.State ts tf sp pc rs' m)
    | match_states_call:
        forall s ts f tf args m
               (SPEC: transl_fundef f = Errors.OK tf)
               (STACK: match_stackframes s ts)
               (WFF: wf_ssa_fundef f),
          match_states (Callstate s f args m)
                       (CSSA.Callstate ts tf args m)
    | match_states_return:
        forall s ts v m
               (STACK: match_stackframes s ts ),
          match_states (Returnstate s v m)
                       (CSSA.Returnstate ts v m).
    Hint Constructors match_states: core.

Lemma function_ptr_translated: forall b f,
  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,
    wf_ssa_fundef f ->
    transl_fundef f = Errors.OK tf ->
    CSSA.funsig tf = SSA.funsig f.

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

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

Lemma instructions_preserved: forall f tf,
  transl_function f = Errors.OK tf ->
  CSSA.fn_code tf = fn_code f.

Lemma no_new_joinpoints: forall f tf,
  transl_function f = Errors.OK tf ->
  forall pc,
    CSSA.join_point pc tf ->
    join_point pc f.

Lemma join_points_preserved: forall f tf,
  transl_function f = Errors.OK tf ->
  forall pc,
    join_point pc f ->
    CSSA.join_point pc tf.

Lemma registers_equal: forall rs rs' args max_reg,
    (forall r, In r args -> Ple r max_reg) ->
    match_regset max_reg rs rs' ->
    rs' ## args = rs ## args.

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

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

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

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

parallel block evaluation simplification lemmas

Lemma parcopy_store_other : forall rs r parcb,
  (forall src dst, In (Iparcopy src dst) parcb -> r <> dst) ->
  rs !! r = (parcopy_store parcb rs) !! r.

Lemma copy_out_of_parcb :
  forall (rs : SSA.regset) (parcb : parcopyblock) (src dst : reg),
  (forall src' dst', In (CSSA.Iparcopy src' dst') parcb -> src <> dst') ->
  parcopy_store (CSSA.Iparcopy src dst :: parcb) rs =
    (parcopy_store parcb rs)# dst <- ((parcopy_store parcb rs) # src).

Lemma copy_out_of_phib : forall (rs : SSA.regset) (phib : phiblock)
    (src dst : reg) (args : list reg) (k : nat),
    (forall args' dst', In (Iphi args' dst') phib -> src <> dst') ->
    nth_error args k = Some src ->
    phi_store k (Iphi args dst :: phib) rs =
    (phi_store k phib rs)# dst <- ((phi_store k phib rs) # src).

equiv_phib inductive predicate consequences

Lemma equiv_phib_fresh_parcb : forall maxreg k phib parcb phib' parcb' src dst
  (EQ_PHIB: equiv_phib maxreg k phib parcb phib' parcb')
  (IN_parcb: In (Iparcopy src dst) parcb),
  Plt maxreg dst.

Lemma equiv_phib_fresh_phib'2 : forall maxreg k phib parcb phib' parcb' args dst
  (EQ_PHIB: equiv_phib maxreg k phib parcb phib' parcb')
  (IN_parcb: In (Iphi args dst) phib'),
  Plt maxreg dst.

Lemma equiv_phib_nth : forall maxreg k phib phib' parcb parcb',
  equiv_phib maxreg k phib parcb phib' parcb' ->
  forall args dst, In (Iphi args dst) phib'
    -> exists arg, nth_error args k = Some arg.

Lemma equiv_phib_parcsrc_phib'dst :
  forall maxreg k phib phib' parcb parcb',
  equiv_phib maxreg k phib parcb phib' parcb' ->
  forall src dst,
  In (Iparcopy src dst) parcb' ->
  exists args, In (Iphi args src) phib'.

Lemma equiv_phib_args_k_notnone : forall maxreg k phib parcb phib' parcb' args dst,
  equiv_phib maxreg k phib parcb phib' parcb' ->
  In (Iphi args dst) phib'
  -> nth_error args k <> None.

Lemma reg_Ple_Plt_not_eq : forall maxreg (r1 r2 : reg),
  Ple r1 maxreg ->
  Plt maxreg r2 ->
  r1 <> r2.

Hint Resolve equiv_phib_fresh_parcb equiv_phib_fresh_phib'2
  equiv_phib_nth equiv_phib_args_k_notnone
  reg_Ple_Plt_not_eq: core.

Hint Resolve parc_dst_in: core.

Definition phib_dst (phiins : phiinstruction) :=
  match phiins with
  | Iphi args dst => dst
  end.

Lemma in_phib_dst_exists_args : forall dst phib,
  In dst (map phib_dst phib) ->
  exists args, In (Iphi args dst) phib.

Lemma in_phib_dst_in : forall args dst phib,
  In (Iphi args dst) phib ->
  In dst (map phib_dst phib).

Lemma in_phib_dst_simul :
  forall rs (phib : phiblock) (r : reg) (k : nat) args arg,
  NoDup (map phib_dst phib) ->
  In (Iphi args r) phib ->
  (forall args' dst', In (Iphi args' dst') phib
    -> nth_error args' k <> None) ->
  nth_error args k = Some arg ->
  (phi_store k phib rs) !! r = rs !! arg.

Lemma in_parcb_dst_simul : forall rs (r : reg) (parcb : parcopyblock) src,
  NoDup (map parc_dst parcb) ->
  In (Iparcopy src r) parcb ->
  (parcopy_store parcb rs) !! r = rs !! src.

Lemma equiv_phib_nodups_parcb_dst :
  forall maxreg k phib parcb phib' parcb',
  equiv_phib maxreg k phib parcb phib' parcb' ->
  NoDup (map parc_dst parcb).

Hint Resolve equiv_phib_nodups_parcb_dst: core.

Lemma equiv_phib_nodups_phib'_dst : forall maxreg k phib parcb phib' parcb',
  equiv_phib maxreg k phib parcb phib' parcb' ->
  NoDup (map phib_dst phib').

Hint Resolve equiv_phib_nodups_phib'_dst: core.

Lemma equiv_phib_spec_rev: forall maxreg k phib parcb phib' parcb',
  equiv_phib maxreg k phib parcb phib' parcb' ->
  equiv_phib_spec maxreg k phib parcb phib' parcb'.

Lemma equiv_phib_nodups_parcb'_dst : forall maxreg k phib parcb phib' parcb',
  unique_def_phib_spec phib ->
  equiv_phib maxreg k phib parcb phib' parcb' ->
  NoDup (map parc_dst parcb').

Hint Resolve equiv_phib_nodups_parcb'_dst: core.

Lemma parcb_not_in : forall r parcb,
  ~ In r (map parc_dst parcb) ->
  forall src dst,
  In (Iparcopy src dst) parcb ->
  r <> dst.

Hint Resolve parcb_not_in: core.

Lemma phi_store_emulation : forall rs rs' k phib parcb phib' parcb' maxreg,
  match_regset maxreg rs rs' ->
  unique_def_phib_spec phib ->
  equiv_phib maxreg k phib parcb phib' parcb' ->
  forall r,
  Ple r maxreg ->
  (phi_store k phib rs) !! r =
  (parcopy_store parcb'
    (phi_store k phib'
      (parcopy_store parcb rs'))) !! r.

(index_preds preds pc) injectivity

Lemma get_index_acc_le_k : forall l pc acc k,
  get_index_acc l pc acc = Some k ->
  acc <= k.

Lemma index_acc_inj : forall l pc1 pc2 k p,
  get_index_acc l pc1 p = Some k ->
  get_index_acc l pc2 p = Some k ->
  pc1 = pc2.

Lemma index_preds_pc_inj : forall f pc1 pc2 succ k preds,
  preds = make_predecessors (fn_code f) successors_instr ->
  index_pred preds pc1 succ = Some k ->
  index_pred preds pc2 succ = Some k ->
  pc1 = pc2.

Lemma get_preds_some : forall preds (pc : node) lpreds,
  preds ! pc = Some lpreds ->
  preds !!! pc = lpreds.

Lemma match_regset_args : forall args maxreg rs rs',
  match_regset maxreg rs rs' ->
  (forall arg, In arg args -> Ple arg maxreg) ->
  rs' ## args = rs ## args.

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

Proving the transformation

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

Theorem transf_program_correct:
  forward_simulation (SSA.semantics prog) (CSSA.semantics tprog).

  End CORRECTNESS.
  
End PRESERVATION.