Proving the trans_block_header axioms

1 files changed, 672 insertions, 672 deletions

diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index 2c3b8454..2ecb494d 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -10,675 +10,675 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-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: Asmblock.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 verified_schedule_builtin_idem:

-  forall bb ef args res lbb,

-  exit bb = Some (PExpand (Pbuiltin ef args res)) ->

-  verified_schedule bb = OK lbb ->

-  lbb = bb :: nil.

-Proof.

-  intros. exploit builtin_body_nil; eauto. intros.

-  rewrite verified_schedule_single_inst in H0.

-  - inv H0. auto.

-  - unfold size. rewrite H. rewrite H1. simpl. auto.

-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 {A: Type}:

-  forall (rs rs':A) m m',

-  rs = rs' -> m = m' -> Next rs m = Next rs' m'.

-Proof.

-  intros. congruence.

-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_pc_var:

-  forall ge t rs m rd ra ofs rs' m' v,

-  exec_load ge t rs m rd ra ofs = Next rs' m' ->

-  exec_load ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.

-Proof.

-  intros. unfold exec_load in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge 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_store_pc_var:

-  forall ge t rs m rd ra ofs rs' m' v,

-  exec_store ge t rs m rd ra ofs = Next rs' m' ->

-  exec_store ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.

-Proof.

-  intros. unfold exec_store in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); 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 *. 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).

-  - exploreInst; apply exec_load_pc_var; auto.

-  - exploreInst; apply exec_store_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 GPR14 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).

-  repeat eexists.

-    unfold exec_bblock. rewrite EXEB1. rewrite EXA. simpl. eauto.

-    exploit exec_body_pc. eapply EXEB1. intros. rewrite <- H. auto.

-    unfold exec_bblock. unfold nextblock. 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 AB.size_positive. instantiate (1 := a). intro. omega.

-    exploit AB.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.

-

-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 goto_label. erewrite label_pos_preserved_blocks; eauto.

-  - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.

-  - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.

-  - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.

-  - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.

-Qed.

-

-Lemma eval_offset_preserved:

-  forall ofs, eval_offset ge ofs = eval_offset tge ofs.

-Proof.

-  intros. unfold eval_offset. destruct ofs; auto. erewrite symbol_address_preserved; eauto.

-Qed.

-

-Lemma transf_exec_load:

-  forall t rs m rd ra ofs, exec_load ge t rs m rd ra ofs = exec_load tge t rs m rd ra ofs.

-Proof.

-  intros. unfold exec_load. rewrite eval_offset_preserved. reflexivity.

-Qed.

-

-Lemma transf_exec_store:

-  forall t rs m rs0 ra ofs, exec_store ge t rs m rs0 ra ofs = exec_store tge t rs m rs0 ra ofs.

-Proof.

-  intros. unfold exec_store. rewrite eval_offset_preserved. reflexivity.

-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. exploreInst; simpl; auto; try congruence.

-  1: unfold exec_arith_instr; exploreInst; simpl; auto; try congruence.

-  1-10: apply transf_exec_load.

-  all: apply transf_exec_store.

-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).

-    assert (NOOV: size_blocks x.(fn_blocks) <= Ptrofs.max_unsigned).

-      eapply transf_function_no_overflow; eauto. 

-

-    erewrite transf_exec_bblock in H2; eauto.

-    inv BBEQ. rewrite H3 in H2.

-    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:

-  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.

+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: Asmblock.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 verified_schedule_builtin_idem  (ge: Genv.t fundef unit) (fn: function):
+  forall bb ef args res lbb,
+  exit bb = Some (PExpand (Pbuiltin ef args res)) ->
+  verified_schedule bb = OK lbb ->
+  lbb = bb :: nil.
+Proof.
+  intros. exploit builtin_body_nil; eauto. intros.
+  rewrite verified_schedule_single_inst in H0; auto.
+  - inv H0. auto.
+  - unfold size. rewrite H. rewrite H1. simpl. auto.
+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 {A: Type}:
+  forall (rs rs':A) m m',
+  rs = rs' -> m = m' -> Next rs m = Next rs' m'.
+Proof.
+  intros. congruence.
+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_pc_var:
+  forall ge t rs m rd ra ofs rs' m' v,
+  exec_load ge t rs m rd ra ofs = Next rs' m' ->
+  exec_load ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
+Proof.
+  intros. unfold exec_load in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge 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_store_pc_var:
+  forall ge t rs m rd ra ofs rs' m' v,
+  exec_store ge t rs m rd ra ofs = Next rs' m' ->
+  exec_store ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
+Proof.
+  intros. unfold exec_store in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); 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 *. 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).
+  - exploreInst; apply exec_load_pc_var; auto.
+  - exploreInst; apply exec_store_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 GPR14 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).
+  repeat eexists.
+    unfold exec_bblock. rewrite EXEB1. rewrite EXA. simpl. eauto.
+    exploit exec_body_pc. eapply EXEB1. intros. rewrite <- H. auto.
+    unfold exec_bblock. unfold nextblock. 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 AB.size_positive. instantiate (1 := a). intro. omega.
+    exploit AB.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.
+
+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 goto_label. erewrite label_pos_preserved_blocks; eauto.
+  - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
+  - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
+  - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
+  - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
+Qed.
+
+Lemma eval_offset_preserved:
+  forall ofs, eval_offset ge ofs = eval_offset tge ofs.
+Proof.
+  intros. unfold eval_offset. destruct ofs; auto. erewrite symbol_address_preserved; eauto.
+Qed.
+
+Lemma transf_exec_load:
+  forall t rs m rd ra ofs, exec_load ge t rs m rd ra ofs = exec_load tge t rs m rd ra ofs.
+Proof.
+  intros. unfold exec_load. rewrite eval_offset_preserved. reflexivity.
+Qed.
+
+Lemma transf_exec_store:
+  forall t rs m rs0 ra ofs, exec_store ge t rs m rs0 ra ofs = exec_store tge t rs m rs0 ra ofs.
+Proof.
+  intros. unfold exec_store. rewrite eval_offset_preserved. reflexivity.
+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. exploreInst; simpl; auto; try congruence.
+  1: unfold exec_arith_instr; exploreInst; simpl; auto; try congruence.
+  1-10: apply transf_exec_load.
+  all: apply transf_exec_store.
+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).
+    assert (NOOV: size_blocks x.(fn_blocks) <= Ptrofs.max_unsigned).
+      eapply transf_function_no_overflow; eauto. 
+
+    erewrite transf_exec_bblock in H2; eauto.
+    inv BBEQ. rewrite H3 in H2.
+    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:
+  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.