Main part of postpasssch proof now completed

1 files changed, 91 insertions, 338 deletions

diff --git a/aarch64/PostpassSchedulingproof.v b/aarch64/PostpassSchedulingproof.v
index 22daede9..c32579a2 100644
--- a/aarch64/PostpassSchedulingproof.v
+++ b/aarch64/PostpassSchedulingproof.v
@@ -5,6 +5,7 @@
 (*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
 (*           David Monniaux     CNRS, VERIMAG                  *)
 (*           Cyril Six          Kalray                         *)
+(*           Léo Gourdin        UGA, VERIMAG                   *)
 (*                                                             *)
 (*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
 (*  This file is distributed under the terms of the INRIA      *)
@@ -16,7 +17,7 @@ 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 Asmblockprops.
+Require Import Asmblockprops.
 Require Import PostpassScheduling.
 Require Import Asmblockgenproof.
 Require Import Axioms.
@@ -32,103 +33,6 @@ Proof.
   intros. eapply match_transform_partial_program; eauto.
 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_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.
-    enough (Ptrofs.repr (x + y) = Ptrofs.add (Ptrofs.repr x) (Ptrofs.repr y)) as ->; auto.
-    unfold Ptrofs.add.
-    enough (x + y = Ptrofs.unsigned (Ptrofs.repr x) + Ptrofs.unsigned (Ptrofs.repr y)) as ->; 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.
@@ -136,15 +40,7 @@ Variable lk: aarch64_linker.
 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.
@@ -153,31 +49,14 @@ 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.
@@ -212,48 +91,6 @@ 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.
-      enough (pos = pos - size a + size a) as ->.
-      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.
-Proof.
-  induction c; intros.
-  - simpl in H. inv H. inv H0.
-  - inv H0.
-    + monadInv H. exists x0; eauto.
-    + unfold transf_blocks in H. fold transf_blocks in H. monadInv H.
-      exploit IHc; eauto.
-Qed. *)
-
 Lemma transf_find_bblock:
   forall ofs f bb tf,
   find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb ->
@@ -269,97 +106,43 @@ Proof.
   induction (fn_blocks f).
   - intros. simpl in *. discriminate.
   - intros. simpl in *.
-  monadInv EQ0. simpl.
-  destruct (zlt z 0); try discriminate.
-  destruct (zeq z 0).
-  + inv H. eauto.
-  + monadInv EQ0.
-   exploit IHb; eauto.
-    intros (tbb & SCH & FIND).
-    eexists; split; eauto.
-    inv FIND.
-    unfold verify_size in EQ0.
-    destruct (size a =? size (stick_header (header a) x)) eqn:EQSIZE; try discriminate.
-    rewrite Z.eqb_eq in EQSIZE; rewrite EQSIZE.
-    reflexivity.
-Qed.
-
-Lemma transf_exec_bblock:
-  forall f tf bb ofs t rs m rs' m',
-  find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb ->
-  transf_function f = OK tf ->
-  exec_bblock lk ge f bb rs m t rs' m' ->
-  exists tbb,
-    exec_bblock lk tge tf tbb rs m t rs' m'
-    /\ find_bblock (Ptrofs.unsigned ofs) (fn_blocks tf) = Some tbb.
+    monadInv EQ0. simpl.
+    destruct (zlt z 0); try discriminate.
+    destruct (zeq z 0).
+    + inv H. eauto.
+    + monadInv EQ0.
+      exploit IHb; eauto.
+      intros (tbb & SCH & FIND).
+      eexists; split; eauto.
+      inv FIND.
+      unfold verify_size in EQ0.
+      destruct (size a =? size (stick_header (header a) x)) eqn:EQSIZE; try discriminate.
+      rewrite Z.eqb_eq in EQSIZE; rewrite EQSIZE.
+      reflexivity.
+Qed.
+
+Lemma stick_header_neutral: forall a,
+  a = (stick_header (header a) (no_header a)).
 Proof.
-  intros. inv H1.
-  monadInv H0. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x0))); try (inv EQ0; fail). inv EQ0.
-  monadInv EQ. simpl in *.
-  generalize (Ptrofs.unsigned ofs) H x0 g EQ0; clear ofs H x0 g EQ0.
-  induction (fn_blocks f).
-  - intros. simpl in *. discriminate.
-  - intros. simpl in *.
-  monadInv EQ0. simpl.
-  destruct (zlt z 0); try discriminate.
-  destruct (zeq z 0).
-  + inv H.
-Admitted.
+  intros.
+  unfold stick_header. unfold Asmblock.stick_header_obligation_1. simpl. destruct a.
+  simpl. reflexivity.
+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').
+  forall bb tbb l,
+  verified_schedule bb = OK (tbb) ->
+     is_label l bb = is_label l tbb.
 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.
+  intros.
+  unfold is_label.
+  monadInv H. simpl. auto.
 Qed.
 
 Remark label_pos_pvar_none_add:
@@ -422,20 +205,18 @@ Proof.
   eapply label_pos_pvar_add; eauto.
 Qed.
 
-Lemma label_pos_head_app:
-  forall c bb lbb l tc p,
-  verified_schedule bb = OK lbb ->
+Lemma label_pos_head_cons:
+  forall c bb tbb l tc p,
+  verified_schedule bb = OK tbb ->
   label_pos l p c = label_pos l p tc ->
-  label_pos l p (bb :: c) = label_pos l p (lbb ++ tc).
+  label_pos l p (bb :: c) = label_pos l p (tbb :: 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.
+  intros. simpl.
+  exploit verified_schedule_label; eauto. intros ISLBL.
+  rewrite ISLBL.
+  destruct (is_label l tbb) eqn:ISLBL'; simpl; auto.
+  eapply label_pos_pvar in H0. erewrite H0.
+  erewrite verified_schedule_size; eauto.
 Qed.
 
 Lemma label_pos_preserved:
@@ -444,8 +225,8 @@ Lemma label_pos_preserved:
 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.
+  - intros. unfold transf_blocks in H; fold transf_blocks in H. monadInv H.
+    eapply IHc in EQ. eapply label_pos_head_cons; eauto.
 Qed.
 
 Lemma label_pos_preserved_blocks:
@@ -458,38 +239,6 @@ Proof.
   monadInv EQ0. simpl. eapply label_pos_preserved; eauto.
 Qed.
 
-Lemma transf_exec_exit:
-  forall f sz cfi t rs m rs' m',
-  (exec_cfi ge f cfi (incrPC sz rs) m = Next rs' m') ->
-  exec_exit ge f sz rs m (Some (PCtlFlow cfi)) t rs' m'.
-Proof.
-  intros.
-  destruct t.
-  - constructor; auto.
-  - congruence.
-  destruct ex; try destruct c; simpl.
-  - generalize cfi_step. intros. apply H0.
-  
-  monadInv H. monadInv EQ.
-  destruct (zlt Ptrofs.max_unsigned _); try discriminate.
-  monadInv EQ0. simpl.
-   assert (ge = Genv.globalenv prog). auto.
-  assert (tge = Genv.globalenv tprog). auto.
-  pose symbol_address_preserved.
-  
-
-  exists rs; exists m. apply cfi_step. inv H.
-  destruct cfi; simpl; eauto.
-  assert (ge = Genv.globalenv prog); auto;
-  assert (tge = Genv.globalenv tprog); auto;
-  pose symbol_address_preserved; simpl.
-  - 
-  constructor.
-  unfold exec_exit.
-  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:
   forall i rs m, exec_basic lk ge i rs m = exec_basic lk tge i rs m.
 Proof.
@@ -507,55 +256,59 @@ Proof.
     destruct (exec_basic _ _ _); auto.
 Qed.
 
-(* Lemma transf_exec_bblock:
-  forall f tf bb b ofs t rs m rs' m',
-  rs PC = Vptr b ofs ->
+Lemma transf_exec_cfi: forall f tf cfi rs m,
   transf_function f = OK tf ->
-  exec_bblock lk ge f bb rs m t rs' m' -> exec_bblock lk tge tf bb rs m t rs' m'.
-Proof.
-  intros. monadInv H. monadInv EQ. pose symbol_address_preserved.
-  simpl in *.
-  destruct (zlt Ptrofs.max_unsigned (size_blocks x0)); try discriminate.
-  monadInv EQ0. unfold transf_blocks in *. destruct f. simpl in *.
-  generalize H0 EQ1; clear H0 EQ1.
-  induction (fn_blocks).
-  - intros. monadInv EQ1. auto. admit.
-  - intros. apply IHb.
-Qed. *)
-(*
-Lemma transf_step_simu:
-  forall f b bb ofs c rs m t rs' m' rs1 m1,
-  Genv.find_funct_ptr tge b = Some (Internal tf) ->
-  (* size_blocks (fn_blocks tf) <= Ptrofs.max_unsigned -> *)
-  rs PC = Vptr b ofs ->
-  exec_body lk ge (body bi) rs m = Next rs1 m1 ->
-  exec_exit ge f (Ptrofs.repr (size bb)) rs1 m1 (exit bb) t rs' m' ->
-  plus (step lk) tge (State rs m) t (State rs' m').
-Proof.
-  induction bb'.
-  - 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.
-*)
+  exec_cfi ge f cfi rs m = exec_cfi tge tf cfi rs m.
+Proof.
+  intros. destruct cfi; simpl; auto;
+  assert (ge = Genv.globalenv prog); auto;
+  assert (tge = Genv.globalenv tprog); auto;
+  pose symbol_address_preserved.
+  all: try unfold eval_branch; try unfold eval_neg_branch; try unfold goto_label;
+       try erewrite label_pos_preserved_blocks; try rewrite e; eauto.
+  destruct (rs # X16 <- Vundef r1); auto.
+  destruct (list_nth_z tbl (Int.unsigned i)); auto.
+  erewrite label_pos_preserved_blocks; eauto.
+Qed.
+
+Lemma transf_exec_exit:
+  forall f tf sz ex t rs m rs' m',
+  transf_function f = OK tf ->
+  exec_exit ge f sz rs m ex t rs' m' ->
+  exec_exit tge tf sz rs m ex t rs' m'.
+Proof.
+  intros. induction H0.
+  - econstructor.
+  - econstructor. erewrite <- transf_exec_cfi; eauto.
+  - econstructor; eauto.
+    eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
+    eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+Qed.
+
+Lemma transf_exec_bblock:
+  forall f tf bb t rs m rs' m',
+  transf_function f = OK tf ->
+  exec_bblock lk ge f bb rs m t rs' m' ->
+  exec_bblock lk tge tf bb rs m t rs' m'.
+Proof.
+  intros.
+  destruct H0 as [rs1[m1[BDY EXIT]]].
+  unfold exec_bblock.
+  eexists; eexists; split.
+  rewrite <- transf_exec_body; eauto.
+  eapply transf_exec_exit; eauto.
+Qed.
+
 Theorem transf_step_correct:
   forall s1 t s2, step lk ge s1 t s2 ->
   forall s1' (MS: match_states s1 s1'),
   (exists s2', step lk tge s1' t s2' /\ match_states s2 s2').
 Proof.
   induction 1; intros; inv MS.
-  - inversion H2.
-  exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF.
-    exploit transf_exec_bblock; eauto. intros (lbb & EBB & FIND).
+  - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF.
+    exploit transf_find_bblock; eauto. intros (tbb & VES & FIND).
+    exploit verified_schedule_correct; eauto. intros EBB.
+    eapply transf_exec_bblock in EBB; eauto. 
     exists (State rs' m').
     split; try (econstructor; eauto).
   - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF.
@@ -576,9 +329,9 @@ Qed.
 
 End PRESERVATION_ASMBLOCK.
 
+(*
 Require Import Asm.
 
-(*
 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.