path: root/mppa_k1c/PostpassSchedulingproof.v

(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

Require Import Coqlib Errors.
Require Import Integers Floats AST Linking.
Require Import Values Memory Events Globalenvs Smallstep.
Require Import Op Locations Machblock Conventions Asmblock.
Require Import Asmblockgenproof0.
Require Import PostpassScheduling.
Require Import Asmblockgenproof.
Require Import Axioms.

Local Open Scope error_monad_scope.

Definition match_prog (p tp: Asmvliw.program) :=
  match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.

Lemma transf_program_match:
  forall p tp, transf_program p = OK tp -> match_prog p tp.
Proof.
  intros. eapply match_transform_partial_program; eauto.
Qed.

Remark builtin_body_nil:
  forall bb ef args res, exit bb = Some (PExpand (Pbuiltin ef args res)) -> body bb = nil.
Proof.
  intros. destruct bb as [hd bdy ex WF]. simpl in *.
  apply wf_bblock_refl in WF. inv WF. unfold builtin_alone in H1.
  eapply H1; eauto.
Qed.

Lemma exec_body_app:
  forall l l' ge rs m rs'' m'',
  exec_body ge (l ++ l') rs m = Next rs'' m'' ->
  exists rs' m',
       exec_body ge l rs m = Next rs' m'
    /\ exec_body ge l' rs' m' = Next rs'' m''.
Proof.
  induction l.
  - intros. simpl in H. repeat eexists. auto.
  - intros. rewrite <- app_comm_cons in H. simpl in H.
    destruct (exec_basic_instr ge a rs m) eqn:EXEBI.
    + apply IHl in H. destruct H as (rs1 & m1 & EXEB1 & EXEB2).
      repeat eexists. simpl. rewrite EXEBI. eauto. auto.
    + discriminate.
Qed.

Lemma exec_body_pc:
  forall l ge rs1 m1 rs2 m2,
  exec_body ge l rs1 m1 = Next rs2 m2 ->
  rs2 PC = rs1 PC.
Proof.
  induction l.
  - intros. inv H. auto.
  - intros until m2. intro EXEB.
    inv EXEB. destruct (exec_basic_instr _ _ _) eqn:EBI; try discriminate.
    eapply IHl in H0. rewrite H0.
    erewrite exec_basic_instr_pc; eauto.
Qed.

Lemma next_eq:
  forall (rs rs': regset) m m',
  rs = rs' -> m = m' -> Next rs m = Next rs' m'.
Proof.
  intros; apply f_equal2; auto.
Qed.

Lemma regset_double_set:
  forall r1 r2 (rs: regset) v1 v2,
  r1 <> r2 ->
  (rs # r1 <- v1 # r2 <- v2) = (rs # r2 <- v2 # r1 <- v1).
Proof.
  intros. apply functional_extensionality. intros r. destruct (preg_eq r r1).
  - subst. rewrite Pregmap.gso; auto. repeat (rewrite Pregmap.gss). auto.
  - destruct (preg_eq r r2).
    + subst. rewrite Pregmap.gss. rewrite Pregmap.gso; auto. rewrite Pregmap.gss. auto.
    + repeat (rewrite Pregmap.gso; auto).
Qed.

Lemma regset_double_set_id:
  forall r (rs: regset) v1 v2,
  (rs # r <- v1 # r <- v2) = (rs # r <- v2).
Proof.
  intros. apply functional_extensionality. intros. destruct (preg_eq r x).
  - subst r. repeat (rewrite Pregmap.gss; auto).
  - repeat (rewrite Pregmap.gso); auto.
Qed.

Lemma exec_load_offset_pc_var:
  forall t rs m rd ra ofs rs' m' v,
  exec_load_offset t rs m rd ra ofs = Next rs' m' ->
  exec_load_offset t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
Proof.
  intros. unfold exec_load_offset in *. unfold parexec_load_offset in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ofs); try discriminate.
  destruct (Mem.loadv _ _ _).
  - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
  - discriminate.
Qed.

Lemma exec_load_reg_pc_var:
  forall t rs m rd ra ro rs' m' v,
  exec_load_reg t rs m rd ra ro = Next rs' m' ->
  exec_load_reg t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'.
Proof.
  intros. unfold exec_load_reg in *. unfold parexec_load_reg in *. rewrite Pregmap.gso; try discriminate.
  destruct (Mem.loadv _ _ _).
  - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
  - discriminate.
Qed.

Lemma exec_load_regxs_pc_var:
  forall t rs m rd ra ro rs' m' v,
  exec_load_regxs t rs m rd ra ro = Next rs' m' ->
  exec_load_regxs t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'.
Proof.
  intros. unfold exec_load_regxs in *. unfold parexec_load_regxs in *. rewrite Pregmap.gso; try discriminate.
  destruct (Mem.loadv _ _ _).
  - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
  - discriminate.
Qed.

Lemma exec_load_offset_q_pc_var:
  forall rs m rd ra ofs rs' m' v,
  exec_load_q_offset rs m rd ra ofs = Next rs' m' ->
  exec_load_q_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
Proof.
  intros. unfold exec_load_q_offset in *. unfold parexec_load_q_offset in *.
  destruct (gpreg_q_expand rd) as [rd0 rd1].
  (* destruct (ireg_eq rd0 ra); try discriminate. *)
  rewrite Pregmap.gso; try discriminate.
  destruct (Mem.loadv _ _ _); try discriminate.
  inv H.
  destruct (Mem.loadv _ _ _); try discriminate.
  inv H1. f_equal.
  rewrite (regset_double_set PC rd0) by discriminate.
  rewrite (regset_double_set PC rd1) by discriminate.
  reflexivity.
Qed.

Lemma exec_load_offset_o_pc_var:
  forall rs m rd ra ofs rs' m' v,
  exec_load_o_offset rs m rd ra ofs = Next rs' m' ->
  exec_load_o_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
Proof.
  intros. unfold exec_load_o_offset in *. unfold parexec_load_o_offset in *.
  destruct (gpreg_o_expand rd) as [[[rd0 rd1] rd2] rd3].
(*
  destruct (ireg_eq rd0 ra); try discriminate.
  destruct (ireg_eq rd1 ra); try discriminate.
  destruct (ireg_eq rd2 ra); try discriminate.
*)
  rewrite Pregmap.gso; try discriminate.
  simpl in *.
  destruct (Mem.loadv _ _ _); try discriminate.
  destruct (Mem.loadv _ _ _); try discriminate.
  destruct (Mem.loadv _ _ _); try discriminate.
  destruct (Mem.loadv _ _ _); try discriminate.
  rewrite (regset_double_set PC rd0) by discriminate.
  rewrite (regset_double_set PC rd1) by discriminate.
  rewrite (regset_double_set PC rd2) by discriminate.
  rewrite (regset_double_set PC rd3) by discriminate.
  inv H.
  trivial.
Qed.

Lemma exec_store_offset_pc_var:
  forall t rs m rd ra ofs rs' m' v,
  exec_store_offset t rs m rd ra ofs = Next rs' m' ->
  exec_store_offset t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
Proof.
  intros. unfold exec_store_offset in *. unfold parexec_store_offset in *. rewrite Pregmap.gso; try discriminate.
  destruct (eval_offset ofs); try discriminate.
  destruct (Mem.storev _ _ _).
  - inv H. apply next_eq; auto.
  - discriminate.
Qed.

Lemma exec_store_q_offset_pc_var:
  forall rs m rd ra ofs rs' m' v,
  exec_store_q_offset rs m rd ra ofs = Next rs' m' ->
  exec_store_q_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
Proof.
  intros. unfold exec_store_q_offset in *. unfold parexec_store_q_offset in *. rewrite Pregmap.gso; try discriminate.
  simpl in *.
  destruct (gpreg_q_expand _) as [s0 s1].
  destruct (Mem.storev _ _ _); try discriminate.
  destruct (Mem.storev _ _ _); try discriminate.
  inv H. apply next_eq; auto.
Qed.

Lemma exec_store_o_offset_pc_var:
  forall rs m rd ra ofs rs' m' v,
  exec_store_o_offset rs m rd ra ofs = Next rs' m' ->
  exec_store_o_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
Proof.
  intros.
  unfold exec_store_o_offset in *. unfold parexec_store_o_offset in *.
  destruct (gpreg_o_expand _) as [[[s0 s1] s2] s3].
  destruct (Mem.storev _ _ _); try discriminate.
  destruct (Mem.storev _ _ _); try discriminate.
  destruct (Mem.storev _ _ _); try discriminate.
  destruct (Mem.storev _ _ _); try discriminate.
  inv H.
  trivial.
Qed.
  
Lemma exec_store_reg_pc_var:
  forall t rs m rd ra ro rs' m' v,
  exec_store_reg t rs m rd ra ro = Next rs' m' ->
  exec_store_reg t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'.
Proof.
  intros. unfold exec_store_reg in *. unfold parexec_store_reg in *. rewrite Pregmap.gso; try discriminate.
  destruct (Mem.storev _ _ _).
  - inv H. apply next_eq; auto.
  - discriminate.
Qed.

Lemma exec_store_regxs_pc_var:
  forall t rs m rd ra ro rs' m' v,
  exec_store_regxs t rs m rd ra ro = Next rs' m' ->
  exec_store_regxs t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'.
Proof.
  intros. unfold exec_store_regxs in *. unfold parexec_store_regxs in *. rewrite Pregmap.gso; try discriminate.
  destruct (Mem.storev _ _ _).
  - inv H. apply next_eq; auto.
  - discriminate.
Qed.

Lemma exec_basic_instr_pc_var:
  forall ge i rs m rs' m' v,
  exec_basic_instr ge i rs m = Next rs' m' ->
  exec_basic_instr ge i (rs # PC <- v) m = Next (rs' # PC <- v) m'.
Proof.
  intros. unfold exec_basic_instr in *. unfold bstep in *. destruct i.
  - unfold exec_arith_instr in *. destruct i; destruct i.
      all: try (exploreInst; inv H; apply next_eq; auto;
      apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate).
(* 
      (* Some cases treated seperately because exploreInst destructs too much *)
      all: try (inv H; apply next_eq; auto; apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate). *)
  - destruct i.
    + exploreInst; apply exec_load_offset_pc_var; auto.
    + exploreInst; apply exec_load_reg_pc_var; auto.
    + exploreInst; apply exec_load_regxs_pc_var; auto.
    + apply exec_load_offset_q_pc_var; auto.
    + apply exec_load_offset_o_pc_var; auto.
  - destruct i.
    + exploreInst; apply exec_store_offset_pc_var; auto.
    + exploreInst; apply exec_store_reg_pc_var; auto.
    + exploreInst; apply exec_store_regxs_pc_var; auto.
    + apply exec_store_q_offset_pc_var; auto.
    + apply exec_store_o_offset_pc_var; auto.
  - destruct (Mem.alloc _ _ _) as (m1 & stk). repeat (rewrite Pregmap.gso; try discriminate).
    destruct (Mem.storev _ _ _ _); try discriminate.
    inv H. apply next_eq; auto. apply functional_extensionality. intros.
    rewrite (regset_double_set GPR32 PC); try discriminate.
    rewrite (regset_double_set GPR12 PC); try discriminate.
    rewrite (regset_double_set FP PC); try discriminate. reflexivity.
  - repeat (rewrite Pregmap.gso; try discriminate).
    destruct (Mem.loadv _ _ _); try discriminate.
    destruct (rs GPR12); try discriminate.
    destruct (Mem.free _ _ _ _); try discriminate.
    inv H. apply next_eq; auto.
    rewrite (regset_double_set GPR32 PC).
    rewrite (regset_double_set GPR12 PC). reflexivity.
    all: discriminate.
  - destruct rs0; try discriminate. inv H. apply next_eq; auto.
    repeat (rewrite Pregmap.gso; try discriminate). apply regset_double_set; discriminate.
  - destruct rd; try discriminate. inv H. apply next_eq; auto.
    repeat (rewrite Pregmap.gso; try discriminate). apply regset_double_set; discriminate.
  - inv H. apply next_eq; auto.
Qed.

Lemma exec_body_pc_var:
  forall l ge rs m rs' m' v,
  exec_body ge l rs m = Next rs' m' ->
  exec_body ge l (rs # PC <- v) m = Next (rs' # PC <- v) m'.
Proof.
  induction l.
  - intros. simpl. simpl in H. inv H. auto.
  - intros. simpl in *.
    destruct (exec_basic_instr ge a rs m) eqn:EXEBI; try discriminate.
    erewrite exec_basic_instr_pc_var; eauto.
Qed.

Lemma pc_set_add:
  forall rs v r x y,
  0 <= x <= Ptrofs.max_unsigned ->
  0 <= y <= Ptrofs.max_unsigned ->
  rs # r <- (Val.offset_ptr v (Ptrofs.repr (x + y))) = rs # r <- (Val.offset_ptr (rs # r <- (Val.offset_ptr v (Ptrofs.repr x)) r) (Ptrofs.repr y)).
Proof.
  intros. apply functional_extensionality. intros r0. destruct (preg_eq r r0).
  - subst. repeat (rewrite Pregmap.gss); auto.
    destruct v; simpl; auto.
    rewrite Ptrofs.add_assoc.
    cutrewrite (Ptrofs.repr (x + y) = Ptrofs.add (Ptrofs.repr x) (Ptrofs.repr y)); auto.
    unfold Ptrofs.add.
    cutrewrite (x + y = Ptrofs.unsigned (Ptrofs.repr x) + Ptrofs.unsigned (Ptrofs.repr y)); auto.
    repeat (rewrite Ptrofs.unsigned_repr); auto.
  - repeat (rewrite Pregmap.gso; auto).
Qed.

Lemma concat2_straight:
  forall a b bb rs m rs'' m'' f ge,
  concat2 a b = OK bb ->
  exec_bblock ge f bb rs m = Next rs'' m'' ->
  exists rs' m',
       exec_bblock ge f a rs m = Next rs' m'
    /\ rs' PC = Val.offset_ptr (rs PC) (Ptrofs.repr (size a))
    /\ exec_bblock ge f b rs' m' = Next rs'' m''.
Proof.
  intros until ge. intros CONC2 EXEB.
  exploit concat2_zlt_size; eauto. intros (LTA & LTB).
  exploit concat2_noexit; eauto. intros EXA.
  exploit concat2_decomp; eauto. intros. inv H.
  unfold exec_bblock in EXEB. destruct (exec_body ge (body bb) rs m) eqn:EXEB'; try discriminate.
  rewrite H0 in EXEB'. apply exec_body_app in EXEB'. destruct EXEB' as (rs1 & m1 & EXEB1 & EXEB2).
  eexists; eexists. split.
    unfold exec_bblock. rewrite EXEB1. rewrite EXA. simpl. eauto.
  split.
    exploit exec_body_pc. eapply EXEB1. intros. rewrite <- H. auto.
    unfold exec_bblock. unfold nextblock, incrPC. rewrite regset_same_assign. erewrite exec_body_pc_var; eauto.
    rewrite <- H1. unfold nextblock in EXEB. rewrite regset_double_set_id.
    assert (size bb = size a + size b).
    { unfold size. rewrite H0. rewrite H1. rewrite app_length. rewrite EXA. simpl. rewrite Nat.add_0_r.
      repeat (rewrite Nat2Z.inj_add). omega. }
    clear EXA H0 H1. rewrite H in EXEB.
    assert (rs1 PC = rs0 PC). { apply exec_body_pc in EXEB2. auto. }
    rewrite H0. rewrite <- pc_set_add; auto.
    exploit size_positive. instantiate (1 := a). intro. omega.
    exploit size_positive. instantiate (1 := b). intro. omega.
Qed.

Lemma concat_all_exec_bblock (ge: Genv.t fundef unit) (f: function) :
  forall a bb rs m lbb rs'' m'', 
  lbb <> nil ->
  concat_all (a :: lbb) = OK bb ->
  exec_bblock ge f bb rs m = Next rs'' m'' ->
  exists bb' rs' m',
       concat_all lbb = OK bb'
    /\ exec_bblock ge f a rs m = Next rs' m'
    /\ rs' PC = Val.offset_ptr (rs PC) (Ptrofs.repr (size a))
    /\ exec_bblock ge f bb' rs' m' = Next rs'' m''.
Proof.
  intros until m''. intros Hnonil CONC EXEB.
  simpl in CONC.
  destruct lbb as [|b lbb]; try contradiction. clear Hnonil.
  monadInv CONC. exploit concat2_straight; eauto. intros (rs' & m' & EXEB1 & PCeq & EXEB2).
  exists x. repeat econstructor. all: eauto.
Qed.

Lemma ptrofs_add_repr :
  forall a b,
  Ptrofs.unsigned (Ptrofs.add (Ptrofs.repr a) (Ptrofs.repr b)) = Ptrofs.unsigned (Ptrofs.repr (a + b)).
Proof.
  intros a b.
  rewrite Ptrofs.add_unsigned. repeat (rewrite Ptrofs.unsigned_repr_eq).
  rewrite <- Zplus_mod. auto.
Qed.

Section PRESERVATION_ASMBLOCK.

Variables prog tprog: program.
Hypothesis TRANSL: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Lemma transf_function_no_overflow:
  forall f tf,
  transf_function f = OK tf -> size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned.
Proof.
  intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0.
  omega.
Qed.

Lemma symbols_preserved:
  forall id,
  Genv.find_symbol tge id = Genv.find_symbol ge id.
Proof (Genv.find_symbol_match TRANSL).

Lemma senv_preserved:
  Senv.equiv ge tge.
Proof (Genv.senv_match TRANSL).

Lemma functions_translated:
  forall v f,
  Genv.find_funct ge v = Some f ->
  exists tf,
  Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.
Proof (Genv.find_funct_transf_partial TRANSL).

Lemma function_ptr_translated:
  forall v f,
  Genv.find_funct_ptr ge v = Some f ->
  exists tf,
  Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf.
Proof (Genv.find_funct_ptr_transf_partial TRANSL).

Lemma functions_transl:
  forall fb f tf,
  Genv.find_funct_ptr ge fb = Some (Internal f) ->
  transf_function f = OK tf ->
  Genv.find_funct_ptr tge fb = Some (Internal tf).
Proof.
  intros. exploit function_ptr_translated; eauto.
  intros (tf' & A & B). monadInv B. rewrite H0 in EQ. inv EQ. auto.
Qed.

Inductive match_states: state -> state -> Prop :=
  | match_states_intro:
      forall s1 s2, s1 = s2 -> match_states s1 s2.

Lemma prog_main_preserved:
  prog_main tprog = prog_main prog.
Proof (match_program_main TRANSL).

Lemma prog_main_address_preserved:
  (Genv.symbol_address (Genv.globalenv prog) (prog_main prog) Ptrofs.zero) =
  (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Ptrofs.zero).
Proof.
  unfold Genv.symbol_address. rewrite symbols_preserved.
  rewrite prog_main_preserved. auto.
Qed.

Lemma transf_initial_states:
  forall st1, initial_state prog st1 ->
  exists st2, initial_state tprog st2 /\ match_states st1 st2.
Proof.
  intros. inv H.
  econstructor; split.
  - eapply initial_state_intro.
    eapply (Genv.init_mem_transf_partial TRANSL); eauto.
  - econstructor; eauto. subst ge0. subst rs0. rewrite prog_main_address_preserved. auto.
Qed.

Lemma transf_final_states:
  forall st1 st2 r,
  match_states st1 st2 -> final_state st1 r -> final_state st2 r.
Proof.
  intros. inv H0. inv H. econstructor; eauto.
Qed.

Lemma tail_find_bblock:
  forall lbb pos bb,
  find_bblock pos lbb = Some bb ->
  exists c, code_tail pos lbb (bb::c).
Proof.
  induction lbb.
  - intros. simpl in H. inv H.
  - intros. simpl in H.
    destruct (zlt pos 0); try (inv H; fail).
    destruct (zeq pos 0).
    + inv H. exists lbb. constructor; auto.
    + apply IHlbb in H. destruct H as (c & TAIL). exists c.
      cutrewrite (pos = pos - size a + size a). apply code_tail_S; auto.
      omega.
Qed.

Lemma code_tail_head_app:
  forall l pos c1 c2,
  code_tail pos c1 c2 ->
  code_tail (pos + size_blocks l) (l++c1) c2.
Proof.
  induction l.
  - intros. simpl. rewrite Z.add_0_r. auto.
  - intros. apply IHl in H. simpl. rewrite (Z.add_comm (size a)). rewrite Z.add_assoc. apply code_tail_S. assumption.
Qed.

Lemma transf_blocks_verified:
  forall c tc pos bb c',
  transf_blocks c = OK tc ->
  code_tail pos c (bb::c') ->
  exists lbb,
     verified_schedule bb = OK lbb
  /\ exists tc', code_tail pos tc (lbb ++ tc').
Proof.
  induction c; intros.
  - simpl in H. inv H. inv H0.
  - inv H0.
    + monadInv H. exists x0.
      split; simpl; auto. eexists; eauto. econstructor; eauto.
    + unfold transf_blocks in H. fold transf_blocks in H. monadInv H.
      exploit IHc; eauto.
      intros (lbb & TRANS & tc' & TAIL).
(*       monadInv TRANS. *)
      repeat eexists; eauto.
      erewrite verified_schedule_size; eauto.
      apply code_tail_head_app.
      eauto.
Qed.

Lemma transf_find_bblock:
  forall ofs f bb tf,
  find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb ->
  transf_function f = OK tf ->
  exists lbb,
     verified_schedule bb = OK lbb
  /\ exists c, code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) (lbb ++ c).
Proof.
  intros.
  monadInv H0. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x))); try (inv EQ0; fail). inv EQ0.
  monadInv EQ. apply tail_find_bblock in H. destruct H as (c & TAIL).
  eapply transf_blocks_verified; eauto.
Qed.

Lemma symbol_address_preserved:
  forall l ofs, Genv.symbol_address ge l ofs = Genv.symbol_address tge l ofs.
Proof.
  intros. unfold Genv.symbol_address. repeat (rewrite symbols_preserved). reflexivity.
Qed.

Lemma head_tail {A: Type}:
  forall (l: list A) hd, hd::l = hd :: (tail (hd::l)).
Proof.
  intros. simpl. auto.
Qed.

Lemma verified_schedule_not_empty:
  forall bb lbb,
  verified_schedule bb = OK lbb -> lbb <> nil.
Proof.
  intros. apply verified_schedule_size in H.
  pose (size_positive bb). assert (size_blocks lbb > 0) by omega. clear H g.
  destruct lbb; simpl in *; discriminate.
Qed.

Lemma header_nil_label_pos_none:
  forall lbb l p,
  Forall (fun b => header b = nil) lbb -> label_pos l p lbb = None.
Proof.
  induction lbb.
  - intros. simpl. auto.
  - intros. inv H. simpl. unfold is_label. rewrite H2. destruct (in_dec l nil). { inv i. }
    auto.
Qed.

Lemma verified_schedule_label:
  forall bb tbb lbb l,
  verified_schedule bb = OK (tbb :: lbb) ->
     is_label l bb = is_label l tbb
  /\ label_pos l 0 lbb = None.
Proof.
  intros. exploit verified_schedule_header; eauto.
  intros (HdrEq & HdrNil).
  split.
  - unfold is_label. rewrite HdrEq. reflexivity.
  - apply header_nil_label_pos_none. assumption.
Qed.

Lemma label_pos_app_none:
  forall c c' l p p',
  label_pos l p c = None ->
  label_pos l (p' + size_blocks c) c' = label_pos l p' (c ++ c').
Proof.
  induction c.
  - intros. simpl in *. rewrite Z.add_0_r. reflexivity.
  - intros. simpl in *. destruct (is_label _ _) eqn:ISLABEL.
    + discriminate.
    + eapply IHc in H. rewrite Z.add_assoc. eauto.
Qed.

Remark label_pos_pvar_none_add:
  forall tc l p p' k,
  label_pos l (p+k) tc = None -> label_pos l (p'+k) tc = None.
Proof.
  induction tc.
  - intros. simpl. auto.
  - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL.
    + discriminate.
    + pose (IHtc l p p' (k + size a)). repeat (rewrite Z.add_assoc in e). auto.
Qed.

Lemma label_pos_pvar_none:
  forall tc l p p',
  label_pos l p tc = None -> label_pos l p' tc = None.
Proof.
  intros. rewrite (Zplus_0_r_reverse p') at 1. rewrite (Zplus_0_r_reverse p) in H at 1.
  eapply label_pos_pvar_none_add; eauto.
Qed.

Remark label_pos_pvar_some_add_add:
  forall tc l p p' k k',
  label_pos l (p+k') tc = Some (p+k) -> label_pos l (p'+k') tc = Some (p'+k).
Proof.
  induction tc.
  - intros. simpl in H. discriminate.
  - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL.
    + inv H. assert (k = k') by omega. subst. reflexivity.
    + pose (IHtc l p p' k (k' + size a)). repeat (rewrite Z.add_assoc in e). auto.
Qed.

Lemma label_pos_pvar_some_add:
  forall tc l p p' k,
  label_pos l p tc = Some (p+k) -> label_pos l p' tc = Some (p'+k).
Proof.
  intros. rewrite (Zplus_0_r_reverse p') at 1. rewrite (Zplus_0_r_reverse p) in H at 1.
  eapply label_pos_pvar_some_add_add; eauto.
Qed.

Remark label_pos_pvar_add:
  forall c tc l p p' k,
  label_pos l (p+k) c = label_pos l p tc ->
  label_pos l (p'+k) c = label_pos l p' tc.
Proof.
  induction c.
  - intros. simpl in *.
    exploit label_pos_pvar_none; eauto.
  - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL.
    + exploit label_pos_pvar_some_add; eauto.
    + pose (IHc tc l p p' (k+size a)). repeat (rewrite Z.add_assoc in e). auto.
Qed.

Lemma label_pos_pvar:
  forall c tc l p p',
  label_pos l p c = label_pos l p tc ->
  label_pos l p' c = label_pos l p' tc.
Proof.
  intros. rewrite (Zplus_0_r_reverse p') at 1. rewrite (Zplus_0_r_reverse p) in H at 1.
  eapply label_pos_pvar_add; eauto.
Qed.

Lemma label_pos_head_app:
  forall c bb lbb l tc p,
  verified_schedule bb = OK lbb ->
  label_pos l p c = label_pos l p tc ->
  label_pos l p (bb :: c) = label_pos l p (lbb ++ tc).
Proof.
  intros. simpl. destruct lbb as [|tbb lbb].
  - apply verified_schedule_not_empty in H. contradiction.
  - simpl. exploit verified_schedule_label; eauto. intros (ISLBL & LBLPOS).
    rewrite ISLBL.
    destruct (is_label l tbb) eqn:ISLBL'; simpl; auto.
    eapply label_pos_pvar in H0. erewrite H0.
    erewrite verified_schedule_size; eauto. simpl size_blocks. rewrite Z.add_assoc.
    erewrite label_pos_app_none; eauto.
Qed.

Lemma label_pos_preserved:
  forall c tc l,
  transf_blocks c = OK tc -> label_pos l 0 c = label_pos l 0 tc.
Proof.
  induction c.
  - intros. simpl in *. inv H. reflexivity.
  - intros. unfold transf_blocks in H; fold transf_blocks in H. monadInv H. eapply IHc in EQ.
    eapply label_pos_head_app; eauto.
Qed.

Lemma label_pos_preserved_blocks:
  forall l f tf,
  transf_function f = OK tf ->
  label_pos l 0 (fn_blocks f) = label_pos l 0 (fn_blocks tf).
Proof.
  intros. monadInv H. monadInv EQ.
  destruct (zlt Ptrofs.max_unsigned _); try discriminate.
  monadInv EQ0. simpl. eapply label_pos_preserved; eauto.
Qed.

Lemma transf_exec_control:
  forall f tf ex rs m,
  transf_function f = OK tf ->
  exec_control ge f ex rs m = exec_control tge tf ex rs m.
Proof.
  intros. destruct ex; simpl; auto.
  assert (ge = Genv.globalenv prog). auto.
  assert (tge = Genv.globalenv tprog). auto.
  pose symbol_address_preserved.
  exploreInst; simpl; auto; try congruence;
    unfold par_goto_label; unfold par_eval_branch; unfold par_goto_label; erewrite label_pos_preserved_blocks; eauto.
Qed.

Lemma transf_exec_basic_instr:
  forall i rs m, exec_basic_instr ge i rs m = exec_basic_instr tge i rs m.
Proof.
  intros. pose symbol_address_preserved.
  unfold exec_basic_instr. unfold bstep. exploreInst; simpl; auto; try congruence.
  unfold parexec_arith_instr; unfold arith_eval_r; exploreInst; simpl; auto; try congruence.
Qed.

Lemma transf_exec_body:
  forall bdy rs m, exec_body ge bdy rs m = exec_body tge bdy rs m.
Proof.
  induction bdy; intros.
  - simpl. reflexivity.
  - simpl. rewrite transf_exec_basic_instr.
    destruct (exec_basic_instr _ _ _); auto.
Qed.

Lemma transf_exec_bblock:
  forall f tf bb rs m,
  transf_function f = OK tf ->
  exec_bblock ge f bb rs m = exec_bblock tge tf bb rs m.
Proof.
  intros. unfold exec_bblock. rewrite transf_exec_body. destruct (exec_body _ _ _ _); auto.
  eapply transf_exec_control; eauto.
Qed.

Lemma transf_step_simu:
  forall tf b lbb ofs c tbb rs m rs' m',
  Genv.find_funct_ptr tge b = Some (Internal tf) ->
  size_blocks (fn_blocks tf) <= Ptrofs.max_unsigned ->
  rs PC = Vptr b ofs ->
  code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) (lbb ++ c) ->
  concat_all lbb = OK tbb ->
  exec_bblock tge tf tbb rs m = Next rs' m' ->
  plus step tge (State rs m) E0 (State rs' m').
Proof.
  induction lbb.
  - intros until m'. simpl. intros. discriminate.
  - intros until m'. intros GFIND SIZE PCeq TAIL CONC EXEB.
    destruct lbb.
    + simpl in *. clear IHlbb. inv CONC. eapply plus_one. econstructor; eauto. eapply find_bblock_tail; eauto.
    + exploit concat_all_exec_bblock; eauto; try discriminate.
    intros (tbb0 & rs0 & m0 & CONC0 & EXEB0 & PCeq' & EXEB1).
    eapply plus_left.
    econstructor.
      3: eapply find_bblock_tail. rewrite <- app_comm_cons in TAIL. 3: eauto.
      all: eauto.
    eapply plus_star. eapply IHlbb; eauto. rewrite PCeq in PCeq'. simpl in PCeq'. all: eauto.
    eapply code_tail_next_int; eauto.
Qed.

Theorem transf_step_correct:
  forall s1 t s2, step ge s1 t s2 ->
  forall s1' (MS: match_states s1 s1'),
  (exists s2', plus step tge s1' t s2' /\ match_states s2 s2').
Proof.
  induction 1; intros; inv MS.
  - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF.
    exploit transf_find_bblock; eauto. intros (lbb & VES & c & TAIL).
    exploit verified_schedule_correct; eauto. intros (tbb & CONC & BBEQ). inv CONC. rename H3 into CONC.
    assert (NOOV: size_blocks x.(fn_blocks) <= Ptrofs.max_unsigned).
      eapply transf_function_no_overflow; eauto. 

    erewrite transf_exec_bblock in H2; eauto.
    unfold bblock_simu in BBEQ. rewrite BBEQ in H2; try congruence.
    exists (State rs' m'). split; try (constructor; auto).
    eapply transf_step_simu; eauto.

  - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF.
    exploit transf_find_bblock; eauto. intros (lbb & VES & c & TAIL).
    exploit verified_schedule_builtin_idem; eauto. intros. subst lbb.

    remember (State (nextblock _ _) _) as s'. exists s'.
    split; try constructor; auto.
    eapply plus_one. subst s'.
    eapply exec_step_builtin.
      3: eapply find_bblock_tail. simpl in TAIL. 3: eauto.
      all: eauto.
    eapply eval_builtin_args_preserved with (ge1 := ge). exact symbols_preserved. eauto.
    eapply external_call_symbols_preserved; eauto. apply senv_preserved.

  - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF.
    remember (State _ m') as s'. exists s'. split; try constructor; auto.
    subst s'. eapply plus_one. eapply exec_step_external; eauto.
    eapply external_call_symbols_preserved; eauto. apply senv_preserved.
Qed.

Theorem transf_program_correct_Asmblock: 
  forward_simulation (Asmblock.semantics prog) (Asmblock.semantics tprog).
Proof.
  eapply forward_simulation_plus.
  - apply senv_preserved.
  - apply transf_initial_states.
  - apply transf_final_states.
  - apply transf_step_correct.
Qed.

End PRESERVATION_ASMBLOCK.




Require Import Asmvliw.


Lemma verified_par_checks_alls_bundles lb x: forall bundle,
  verify_par lb = OK x ->
  List.In bundle lb -> verify_par_bblock bundle = OK tt.
Proof.
  induction lb; simpl; try tauto.
  intros bundle H; monadInv H.
  destruct 1; subst; eauto.
  destruct x0; auto.
Qed.


Lemma verified_schedule_nob_checks_alls_bundles bb lb bundle:
  verified_schedule_nob bb = OK lb ->
  List.In bundle lb -> verify_par_bblock bundle = OK tt.
Proof.
  unfold verified_schedule_nob. intros H;
  monadInv H. destruct x4.
  intros; eapply verified_par_checks_alls_bundles; eauto.
Qed.

Lemma verify_par_bblock_PExpand bb i:
  exit bb = Some (PExpand i) -> verify_par_bblock bb = OK tt.
Proof.
  destruct bb as [h bdy ext H]; simpl.
  intros; subst. destruct i.
  generalize H.
  rewrite <- wf_bblock_refl in H.
  destruct H as [H H0].
  unfold builtin_alone in H0. erewrite H0; eauto.
Qed.

Local Hint Resolve verified_schedule_nob_checks_alls_bundles.

Lemma verified_schedule_checks_alls_bundles bb lb bundle:
  verified_schedule bb = OK lb ->
  List.In bundle lb -> verify_par_bblock bundle = OK tt.
Proof.
  unfold verified_schedule. remember (exit bb) as exb.
  destruct exb as [c|]; eauto.
  destruct c as [i|]; eauto.
  destruct i; intros H. inversion_clear H; simpl.
  intuition subst.
  intros; eapply verify_par_bblock_PExpand; eauto.
Qed.

Lemma transf_blocks_checks_all_bundles lbb: forall lb bundle,
  transf_blocks lbb = OK lb ->
  List.In bundle lb -> verify_par_bblock bundle = OK tt.
Proof.
  induction lbb; simpl.
  - intros lb bundle H; inversion_clear H. simpl; try tauto.
  - intros lb bundle H0.
    monadInv H0.
    rewrite in_app. destruct 1; eauto.
    eapply verified_schedule_checks_alls_bundles; eauto.
Qed.

Lemma find_bblock_Some_in lb: 
  forall ofs b, find_bblock ofs lb = Some b -> List.In b lb.
Proof.
  induction lb; simpl; try congruence.
  intros ofs b.
  destruct (zlt ofs 0); try congruence.
  destruct (zeq ofs 0); eauto.
  intros X; inversion X; eauto.
Qed.

Section PRESERVATION_ASMVLIW.

Variables prog tprog: program.
Hypothesis TRANSL: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Lemma all_bundles_are_checked b ofs f bundle:
  Genv.find_funct_ptr (globalenv (Asmblock.semantics tprog)) b = Some (Internal f) ->
  find_bblock ofs (fn_blocks f) = Some bundle ->
  verify_par_bblock bundle = OK tt. 
Proof.
  unfold match_prog, match_program in TRANSL.
  unfold Genv.find_funct_ptr; simpl; intros X.
  destruct (Genv.find_def_match_2 TRANSL b) as [|f0 y H]; try congruence.
  destruct y as [tf0|]; try congruence.
  inversion X as [H1]. subst. clear X.
  remember (@Gfun fundef unit (Internal f)) as f2.
  destruct H as [ctx' f1 f2 H0|]; try congruence.
  inversion Heqf2 as [H2]. subst; clear Heqf2.
  unfold transf_fundef, transf_partial_fundef in H.
  destruct f1 as [f1|f1]; try congruence.
  unfold transf_function, transl_function in H.
  monadInv H. monadInv EQ.
  destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks _))); simpl in *|-; try congruence.
  injection EQ1; intros; subst.
  monadInv EQ0. simpl in * |-.
  intros; exploit transf_blocks_checks_all_bundles; eauto.
  intros; eapply find_bblock_Some_in; eauto.
Qed.

Lemma checked_bundles_are_parexec_equiv f bundle rs rs' m m':
  exec_bblock (globalenv (Asmblock.semantics tprog)) f bundle rs m = Next rs' m' ->
  verify_par_bblock bundle = OK tt ->
  det_parexec (globalenv (semantics tprog)) f bundle rs m rs' m'.
Proof.
  intros. unfold verify_par_bblock in H0. destruct (Asmblockdeps.bblock_para_check _) eqn:BPC; try discriminate. clear H0.
  simpl in H.
  eapply Asmblockdeps.bblock_para_check_correct; eauto.
Qed.

Lemma seqexec_parexec_equiv b ofs f bundle rs rs' m m':
  Genv.find_funct_ptr (globalenv (Asmblock.semantics tprog)) b = Some (Internal f) ->
  find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bundle ->
  exec_bblock (globalenv (Asmblock.semantics tprog)) f bundle rs m = Next rs' m' ->
  det_parexec (globalenv (semantics tprog)) f bundle rs m rs' m'.
Proof.
  intros; eapply checked_bundles_are_parexec_equiv; eauto.
  eapply all_bundles_are_checked; eauto.
Qed.

Theorem transf_program_correct_Asmvliw: 
  forward_simulation (Asmblock.semantics tprog) (Asmvliw.semantics tprog).
Proof.
  eapply forward_simulation_step with (match_states:=fun (s1:Asmvliw.state) s2 => s1=s2); eauto.
  - intros; subst; auto.
  - intros s1 t s1' H s2 H0; subst; inversion H; clear H; subst; eexists; split; eauto.
    + eapply exec_step_internal; eauto.
      intros; eapply seqexec_parexec_equiv; eauto.
    + eapply exec_step_builtin; eauto.
    + eapply exec_step_external; eauto.
Qed.

End PRESERVATION_ASMVLIW.




Section PRESERVATION.

Variables prog tprog: program.
Hypothesis TRANSL: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Theorem transf_program_correct: 
  forward_simulation (Asmblock.semantics prog) (Asmvliw.semantics tprog).
Proof.
  eapply compose_forward_simulations.
  eapply transf_program_correct_Asmblock; eauto.
  eapply transf_program_correct_Asmvliw; eauto.
Qed.

End PRESERVATION.