splitting BTL by introducing BTLmatchRTL

reduce also copy-paste between BTLtoRTLproof and RTLtoBTLproof
sharing is done in BTLmatchRTL

1 files changed, 6 insertions, 559 deletions

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index 2c1dda5b..6536addb 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -90,8 +90,6 @@ Coercion BF: final >-> Funclass.
         - the same trick appears for all "basic" instructions and [Icond].
 *)
 
-
-
 Record iblock_info := { 
   entry: iblock;
   input_regs: Regset.t; (* extra liveness information for BTL functional semantics *)
@@ -187,6 +185,8 @@ Section RELSEM.
     Here, [or] is an optional register that will be assigned after exiting the iblock, but before entering in [pc]: e.g. the register set by a function call
     before entering in return address.
 
+    See [tr_inputs] implementation below.
+
 *)
 
 Variable tr_exit: function -> list exit -> option reg -> regset -> regset.
@@ -390,14 +390,6 @@ Inductive final_state: state -> int -> Prop :=
   | final_state_intro: forall r m,
       final_state (Returnstate nil (Vint r) m) r.
 
-(** The "raw" CFG small-step semantics for a BTL program (e.g. close to RTL semantics) *)
-
-(* tid = transfer_identity *)
-Definition tid (_:function) (_:list exit) (_: option reg) (rs:regset) := rs.
-
-Definition cfgsem (p: program) :=
-  Semantics (step tid) (initial_state p) final_state (Genv.globalenv p).
-
 (** The full "functional" small-step semantics for a BTL program.
     at each exit, we only transfer register in "input_regs" (i.e. "alive" registers).
 *)
@@ -633,9 +625,9 @@ Proof.
   - repeat (rewrite Regmap.gso); auto.
 Qed.
 
-(* * Simulation of BTL fsem by BTL cfgsem: a lock-step less-def simulation.
+(* * Comparing BTL semantics modulo [regs_lessdef].
 
-We start by extending the previous [equiv_*] stuff for [Val.lessdef]: we need to also compare memories 
+This extends the previous [equiv_*] stuff for [Val.lessdef]. Here, we need to also compare memories
 for Mem.extends, because Vundef values are propagated in memory through stores, allocation, etc.
 
 *)
@@ -721,16 +713,6 @@ Proof.
   eapply set_reg_lessdef; eauto.
   intros r2; eauto.
 Qed.
-Local Hint Resolve init_regs_lessdef_preserv: core.
-
-Lemma tr_inputs_lessdef f rs1 rs2 tbl or r
-  (REGS: forall r, Val.lessdef rs1#r rs2#r)
-  :Val.lessdef (tr_inputs f tbl or rs1)#r (tid f tbl or rs2)#r.
-Proof.
-  unfold tid; rewrite tr_inputs_get.
-  autodestruct.
-Qed.
-Local Hint Resolve tr_inputs_lessdef: core.
 
 Lemma find_function_lessdef ge ros rs1 rs2 fd
   (FIND: find_function ge ros rs1 = Some fd)
@@ -742,547 +724,12 @@ Proof.
   intros (b & EQ).
   destruct (REGS r); try congruence.
 Qed.
-Local Hint Resolve find_function_lessdef regs_lessdef_regs: core.
-
-
-Lemma fsem2cfgsem_ibistep_simu ge sp rs1 m1 ib rs1' m1' of
-  (ISTEP: iblock_istep ge sp rs1 m1 ib rs1' m1' of)
-  rs2 m2
-  (REGS: forall r, Val.lessdef rs1#r rs2#r)
-  (MEMS: Mem.extends m1 m2)
-  : exists rs2' m2', iblock_istep_run ge sp ib rs2 m2 = Some (out rs2' m2' of) 
-     /\ (forall r, Val.lessdef rs1'#r rs2'#r)
-     /\ (Mem.extends m1' m2').
-Proof.
-  induction ISTEP; simpl; try_simplify_someHyps.
-Admitted.
-
-Local Hint Constructors final_step list_forall2: core.
-Local Hint Unfold regs_lessdef: core.
-
-Lemma fsem2cfgsem_finalstep_simu ge stk1 f sp rs1 m1 fin t s1 stk2 rs2 m2
-  (FSTEP: final_step tr_inputs ge stk1 f sp rs1 m1 fin t s1)
-  (STACKS: list_forall2 lessdef_stackframe stk1 stk2)
-  (REGS: forall r, Val.lessdef rs1#r rs2#r)
-  (MEMS: Mem.extends m1 m2)
-  : exists s2, final_step tid ge stk2 f sp rs2 m2 fin t s2
-               /\ lessdef_state s1 s2.
-Proof.
-  destruct FSTEP; try (eexists; split; simpl; econstructor; eauto; fail).
-  - (* return *)
-    exploit Mem.free_parallel_extends; eauto.
-    intros (m2' & FREE & MEMS2).
-    eexists; split; simpl; econstructor; eauto.
-    destruct or; simpl; auto.
-  - (* tailcall *)
-    exploit Mem.free_parallel_extends; eauto.
-    intros (m2' & FREE & MEMS2).
-    eexists; split; simpl; econstructor; eauto.
-  - (* builtin *)
-    exploit (eval_builtin_args_lessdef (ge:=ge) (e1:=(fun r => rs1 # r)) (fun r => rs2 # r)); eauto.
-    intros (vl2' & BARGS & VARGS).
-    exploit external_call_mem_extends; eauto.
-    intros (vres' & m2' & CALL2 & REGS2 & MEMS2 & UNCHANGED).
-    eexists; split; simpl; econstructor; eauto.
-    intros; apply set_res_lessdef; eauto.
-  - (* jumptable *)
-    eexists; split; simpl; econstructor; eauto.
-    destruct (REGS arg); try congruence.
-Qed.
-
-Lemma fsem2cfgsem_ibstep_simu ge stk1 stk2 f sp rs1 m1 ib t s1 rs2 m2
-  (STEP: iblock_step tr_inputs ge stk1 f sp rs1 m1 ib t s1)
-  (STACKS : list_forall2 lessdef_stackframe stk1 stk2)
-  (REGS: forall r, Val.lessdef rs1#r rs2#r)
-  (MEMS : Mem.extends m1 m2)
-  : exists s2, iblock_step tid ge stk2 f sp rs2 m2 ib t s2
-               /\ lessdef_state s1 s2.
-Proof.
-  destruct STEP as (rs1' & m1' & fin & ISTEP & FSTEP).
-  exploit fsem2cfgsem_ibistep_simu; eauto.
-  intros (rs2' & m2' & ISTEP2 & REGS2 & MEMS2).
-  rewrite <- iblock_istep_run_equiv in ISTEP2. clear ISTEP REGS MEMS.
-  exploit fsem2cfgsem_finalstep_simu; eauto.
-  intros (s2 & FSTEP2 & LESSDEF). clear FSTEP.
-  unfold iblock_step; eexists; split; eauto.
-Qed.
-
-Local Hint Constructors step: core.
-
-Lemma fsem2cfgsem_step_simu ge s1 t s1' s2
- (STEP: step tr_inputs ge s1 t s1')
- (REGS: lessdef_state s1 s2)
- :exists s2' : state,
-   step tid ge s2 t s2' /\
-   lessdef_state s1' s2'.
-Proof.
-  destruct STEP; inv REGS.
-  - (* iblock *)
-    intros; exploit fsem2cfgsem_ibstep_simu; eauto. clear STEP.
-    intros (s2 & STEP2 & REGS2).
-    eexists; split; eauto.
-  - (* internal call *)
-    exploit (Mem.alloc_extends m m2 0 (fn_stacksize f) stk m' 0 (fn_stacksize f)); eauto.
-    1-2: lia.
-    intros (m2' & ALLOC2 & MEMS2). clear ALLOC MEMS.
-    eexists; split; econstructor; eauto.
-  - (* external call *)
-    exploit external_call_mem_extends; eauto.
-    intros (vres' & m2' & CALL2 & REGS2 & MEMS2 & UNCHANGED). clear EXTCALL MEMS.
-    eexists; split; econstructor; eauto.
-  - (* return *)
-    inversion STACKS as [|d1 d2 d3 d4 STF2 STK2]. subst.
-    inv STF2.
-    eexists; split; econstructor; eauto.
-    intros; eapply set_reg_lessdef; eauto.
-Qed.
-
-Theorem fsem2cfgsem prog:
-  forward_simulation (fsem prog) (cfgsem prog).
-Proof.
-  eapply forward_simulation_step with lessdef_state; simpl; auto.
-  - destruct 1; intros; eexists; intuition eauto. econstructor; eauto.
-  - intros s1 s2 r REGS FINAL; destruct FINAL.
-     inv REGS; inv STACKS; inv REGS0.
-     econstructor; eauto.
-  - intros; eapply fsem2cfgsem_step_simu; eauto.
-Qed.
-
-(** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *)
-
-(** Matching BTL and RTL code 
-
-We should be able to define a single verifier able to prove a bisimulation between BTL and RTL code.
-
-NB 1: the proof of BTL -> RTL (plus simulation) should be much easier than RTL -> BTL (star simulation).
-
-NB 2: our scheme allows the BTL to duplicate some RTL code.
-- in other words: RTL -> BTL allows tail duplication, loop unrolling, etc. Exactly like "Duplicate" on RTL.
-- BTL -> RTL allows to "undo" some duplications (e.g. remove duplications that have not enabled interesting optimizations) !
-
-Hence, in a sense, our verifier imitates the approach of Duplicate, where [dupmap] maps the BTL nodes to the RTL nodes.
-
-The [match_*] definitions gives a "relational" specification of the verifier...
-*)
-
-Require Import Errors.
-
-Inductive match_final_inst (dupmap: PTree.t node): final -> instruction -> Prop :=
-(* TODO: it may be simplify the oracle for BTL -> RTL, but may makes the verifier more complex ?
-  | mfi_goto pc pc':
-      dupmap!pc = (Some pc') -> match_final_inst dupmap (Bgoto pc) (Inop pc')
-*)
-  | mfi_return or: match_final_inst dupmap (Breturn or) (Ireturn or)
-  | mfi_call pc pc' s ri lr r:
-      dupmap!pc = (Some pc') -> match_final_inst dupmap (Bcall s ri lr r pc) (Icall s ri lr r pc')
-  | mfi_tailcall s ri lr:
-      match_final_inst dupmap (Btailcall s ri lr) (Itailcall s ri lr)
-  | mfi_builtin pc pc' ef la br:
-      dupmap!pc = (Some pc') -> match_final_inst dupmap (Bbuiltin ef la br pc) (Ibuiltin ef la br pc')
-  | mfi_jumptable ln ln' r:
-      list_forall2 (fun pc pc' => (dupmap!pc = (Some pc'))) ln ln' ->
-      match_final_inst dupmap (Bjumptable r ln) (Ijumptable r ln')
-.
-
-Inductive is_join_opt {A}: (option A) -> (option A) -> (option A) -> Prop :=
-  | ijo_None_left o: is_join_opt None o o
-  | ijo_None_right o: is_join_opt o None o
-  | ijo_Some x: is_join_opt (Some x) (Some x) (Some x)
-  .
-
-(* [match_iblock dupmap cfg isfst pc ib opc] means that [ib] match a block in a RTL code starting at [pc], with:
-   - [isfst] (in "input") indicates that no step in the surrounding block has been executed before entering [pc]
-   - if [opc] (in "ouput") is [None], this means that all branches of the block ends on a final instruction
-   - if [opc] is [Some pc'], this means that all branches of the block that do not exit, join on [pc'].
-*)
-Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> iblock -> (option node) -> Prop :=
-  | mib_BF isfst fi pc i iinfo:
-      cfg!pc = Some i ->
-      match_final_inst dupmap fi i ->
-      match_iblock dupmap cfg isfst pc (BF fi iinfo) None
-  | mib_nop_on_rtl isfst pc pc' iinfo:
-      cfg!pc = Some (Inop pc') ->
-      match_iblock dupmap cfg isfst pc (Bnop (Some iinfo)) (Some pc')
-  | mib_nop_skip pc:
-      match_iblock dupmap cfg false pc (Bnop None) (Some pc)
-  | mib_op isfst pc pc' op lr r iinfo:
-      cfg!pc = Some (Iop op lr r pc') ->
-      match_iblock dupmap cfg isfst pc (Bop op lr r iinfo) (Some pc')
-  | mib_load isfst pc pc' m a lr r iinfo:
-      cfg!pc = Some (Iload TRAP m a lr r pc') -> 
-      match_iblock dupmap cfg isfst pc (Bload TRAP m a lr r iinfo) (Some pc')
-  | mib_store isfst pc pc' m a lr r iinfo:
-      cfg!pc = Some (Istore m a lr r pc') -> 
-      match_iblock dupmap cfg isfst pc (Bstore m a lr r iinfo) (Some pc')
-  | mib_exit pc pc' iinfo: 
-      dupmap!pc = (Some pc') ->
-      match_iblock dupmap cfg false pc' (BF (Bgoto pc) iinfo) None
-      (* NB: on RTL side, we exit the block by a "basic" instruction (or Icond). 
-         Thus some step should have been executed before [pc'] in the RTL code *)
-  | mib_seq_Some isfst b1 b2 pc1 pc2 opc:
-      match_iblock dupmap cfg isfst pc1 b1 (Some pc2) ->
-      match_iblock dupmap cfg false pc2 b2 opc ->
-      match_iblock dupmap cfg isfst pc1 (Bseq b1 b2) opc
-(*  | mib_seq_None isfst b1 b2 pc:
-      match_iblock dupmap cfg isfst pc b1 None -> 
-      match_iblock dupmap cfg isfst (Bseq b1 b2) pc None
-      (* TODO: here [b2] is dead code ! Is this case really useful ? 
-         The oracle could remove this dead code.
-         And the verifier could fail if there is such dead code!
-      *)
-*)
-  | mib_cond isfst c lr bso bnot pcso pcnot pc opc1 opc2 opc i iinfo:
-      cfg!pc = Some (Icond c lr pcso pcnot i) ->
-      match_iblock dupmap cfg false pcso bso opc1 ->
-      match_iblock dupmap cfg false pcnot bnot opc2 ->
-      is_join_opt opc1 opc2 opc ->
-      match_iblock dupmap cfg isfst pc (Bcond c lr bso bnot iinfo) opc
-  .
-
-Definition match_cfg dupmap (cfg: code) (cfg':RTL.code): Prop :=
-    forall pc pc', dupmap!pc = Some pc' ->
-    exists ib, cfg!pc = Some ib /\ match_iblock dupmap cfg' true pc' ib.(entry) None.
-
-(** Shared verifier between RTL -> BTL and BTL -> RTL *)
-
-Local Open Scope error_monad_scope.
-
-Definition verify_is_copy dupmap n n' :=
-  match dupmap!n with
-  | None => Error(msg "BTL.verify_is_copy None")
-  | Some revn => match (Pos.compare n' revn) with Eq => OK tt | _ => Error(msg "BTL.verify_is_copy invalid map") end
-  end.
-
-Fixpoint verify_is_copy_list dupmap ln ln' :=
-  match ln with
-  | n::ln => match ln' with
-             | n'::ln' => do _ <- verify_is_copy dupmap n n';
-                          verify_is_copy_list dupmap ln ln'
-             | nil => Error (msg "BTL.verify_is_copy_list: ln' bigger than ln") end
-  | nil => match ln' with
-          | n :: ln' => Error (msg "BTL.verify_is_copy_list: ln bigger than ln'")
-          | nil => OK tt end
-  end.
-
-Lemma verify_is_copy_correct dupmap n n' tt:
-  verify_is_copy dupmap n n' = OK tt ->
-  dupmap ! n = Some n'.
-Proof.
-  unfold verify_is_copy; repeat autodestruct.
-  intros NP H; destruct (_ ! n) eqn:REVM; [|inversion H].
-  eapply Pos.compare_eq in NP. congruence.
-Qed.
-Local Hint Resolve verify_is_copy_correct: core.
-
-Lemma verify_is_copy_list_correct dupmap ln: forall ln' tt,
-  verify_is_copy_list dupmap ln ln' = OK tt ->
-  list_forall2 (fun n n' => dupmap ! n = Some n') ln ln'.
-Proof.
-  induction ln.
-  - intros. destruct ln'; monadInv H. constructor.
-  - intros. destruct ln'; monadInv H. constructor; eauto.
-Qed.
-
-(* TODO Copied from duplicate, should we import ? *)
-Lemma product_eq {A B: Type} :
-  (forall (a b: A), {a=b} + {a<>b}) ->
-  (forall (c d: B), {c=d} + {c<>d}) ->
-  forall (x y: A+B), {x=y} + {x<>y}.
-Proof.
-  intros H H'. intros. decide equality.
-Qed.
-
-(* TODO Copied from duplicate, should we import ? *)
-(** FIXME Ideally i would like to put this in AST.v but i get an "illegal application"
- * error when doing so *)
-Remark builtin_arg_eq_pos: forall (a b: builtin_arg positive), {a=b} + {a<>b}.
-Proof.
-  intros.
-  apply (builtin_arg_eq Pos.eq_dec).
-Defined.
-Global Opaque builtin_arg_eq_pos.
-
-(* TODO Copied from duplicate, should we import ? *)
-Remark builtin_res_eq_pos: forall (a b: builtin_res positive), {a=b} + {a<>b}.
-Proof. intros. apply (builtin_res_eq Pos.eq_dec). Qed.
-Global Opaque builtin_res_eq_pos.
-
-Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) :=
-  match ib with
-  | BF fi _ =>
-      match fi with
-      | Bgoto pc1 =>
-          do u <- verify_is_copy dupmap pc1 pc;
-          if negb isfst then
-            OK None
-          else Error (msg "BTL.verify_block: isfst is true Bgoto")
-      | Breturn or =>
-          match cfg!pc with
-          | Some (Ireturn or') =>
-              if option_eq Pos.eq_dec or or' then OK None
-              else Error (msg "BTL.verify_block: different opt reg in Breturn")
-          | _ => Error (msg "BTL.verify_block: incorrect cfg Breturn")
-          end
-      | Bcall s ri lr r pc1 =>
-          match cfg!pc with
-          | Some (Icall s' ri' lr' r' pc2) =>
-              do u <- verify_is_copy dupmap pc1 pc2;
-              if (signature_eq s s') then
-                if (product_eq Pos.eq_dec ident_eq ri ri') then
-                  if (list_eq_dec Pos.eq_dec lr lr') then
-                    if (Pos.eq_dec r r') then OK None
-                    else Error (msg "BTL.verify_block: different r r' in Bcall")
-                  else Error (msg "BTL.verify_block: different lr in Bcall")
-                else Error (msg "BTL.verify_block: different ri in Bcall")
-              else Error (msg "BTL.verify_block: different signatures in Bcall")
-          | _ => Error (msg "BTL.verify_block: incorrect cfg Bcall")
-          end
-      | Btailcall s ri lr =>
-          match cfg!pc with
-          | Some (Itailcall s' ri' lr') =>
-              if (signature_eq s s') then
-                if (product_eq Pos.eq_dec ident_eq ri ri') then
-                  if (list_eq_dec Pos.eq_dec lr lr') then OK None
-                  else Error (msg "BTL.verify_block: different lr in Btailcall")
-                else Error (msg "BTL.verify_block: different ri in Btailcall")
-              else Error (msg "BTL.verify_block: different signatures in Btailcall")
-          | _ => Error (msg "BTL.verify_block: incorrect cfg Btailcall")
-          end
-      | Bbuiltin ef la br pc1 =>
-          match cfg!pc with
-          | Some (Ibuiltin ef' la' br' pc2) =>
-              do u <- verify_is_copy dupmap pc1 pc2;
-              if (external_function_eq ef ef') then
-                if (list_eq_dec builtin_arg_eq_pos la la') then
-                  if (builtin_res_eq_pos br br') then OK None
-                  else Error (msg "BTL.verify_block: different brr in Bbuiltin")
-                else Error (msg "BTL.verify_block: different lbar in Bbuiltin")
-              else Error (msg "BTL.verify_block: different ef in Bbuiltin")
-          | _ => Error (msg "BTL.verify_block: incorrect cfg Bbuiltin")
-          end
-      | Bjumptable r ln =>
-          match cfg!pc with
-          | Some (Ijumptable r' ln') =>
-              do u <- verify_is_copy_list dupmap ln ln';
-              if (Pos.eq_dec r r') then OK None
-              else Error (msg "BTL.verify_block: different r in Bjumptable")
-          | _ => Error (msg "BTL.verify_block: incorrect cfg Bjumptable")
-          end
-      end
-  | Bnop oiinfo =>
-      match oiinfo with
-      | Some _ =>
-          match cfg!pc with
-          | Some (Inop pc') => OK (Some pc')
-          | _ => Error (msg "BTL.verify_block: incorrect cfg Bnop")
-          end
-      | None =>
-          if negb isfst then OK (Some pc)
-          else Error (msg "BTL.verify_block: isfst is true Bnop (on_rtl is false)")
-      end
-  | Bop op lr r _ =>
-      match cfg!pc with
-      | Some (Iop op' lr' r' pc') =>
-          if (eq_operation op op') then
-            if (list_eq_dec Pos.eq_dec lr lr') then
-              if (Pos.eq_dec r r') then
-                OK (Some pc')
-              else Error (msg "BTL.verify_block: different r in Bop")
-            else Error (msg "BTL.verify_block: different lr in Bop")
-          else Error (msg "BTL.verify_block: different operations in Bop")
-      | _ => Error (msg "BTL.verify_block: incorrect cfg Bop")
-      end
-  | Bload tm m a lr r _ =>
-      match cfg!pc with
-      | Some (Iload tm' m' a' lr' r' pc') =>
-          if (trapping_mode_eq tm TRAP && trapping_mode_eq tm' TRAP) then
-            if (chunk_eq m m') then
-              if (eq_addressing a a') then
-                if (list_eq_dec Pos.eq_dec lr lr') then
-                  if (Pos.eq_dec r r') then
-                    OK (Some pc')
-                  else Error (msg "BTL.verify_block: different r in Bload")
-                else Error (msg "BTL.verify_block: different lr in Bload")
-              else Error (msg "BTL.verify_block: different addressing in Bload")
-            else Error (msg "BTL.verify_block: different mchunk in Bload")
-          else Error (msg "BTL.verify_block: NOTRAP trapping_mode unsupported in Bload")
-      | _ => Error (msg "BTL.verify_block: incorrect cfg Bload")
-      end
-  | Bstore m a lr r _ =>
-      match cfg!pc with
-      | Some (Istore m' a' lr' r' pc') =>
-          if (chunk_eq m m') then
-            if (eq_addressing a a') then
-              if (list_eq_dec Pos.eq_dec lr lr') then
-                if (Pos.eq_dec r r') then OK (Some pc')
-                else Error (msg "BTL.verify_block: different r in Bstore")
-              else Error (msg "BTL.verify_block: different lr in Bstore")
-            else Error (msg "BTL.verify_block: different addressing in Bstore")
-          else Error (msg "BTL.verify_block: different mchunk in Bstore")
-      | _ => Error (msg "BTL.verify_block: incorrect cfg Bstore")
-      end
-  | Bseq b1 b2 =>
-      do opc <- verify_block dupmap cfg isfst pc b1;
-      match opc with
-      | Some pc' =>
-          verify_block dupmap cfg false pc' b2
-      | None => Error (msg "BTL.verify_block: None next pc in Bseq (deadcode)")
-      end
-  | Bcond c lr bso bnot _ =>
-      match cfg!pc with
-      | Some (Icond c' lr' pcso pcnot i') =>
-          if (list_eq_dec Pos.eq_dec lr lr') then
-            if (eq_condition c c') then
-              do opc1 <- verify_block dupmap cfg false pcso bso;
-              do opc2 <- verify_block dupmap cfg false pcnot bnot;
-              match opc1, opc2 with
-              | None, o => OK o
-              | o, None => OK o
-              | Some x, Some x' =>
-                  if Pos.eq_dec x x' then OK (Some x)
-                  else Error (msg "BTL.verify_block: is_join_opt incorrect for Bcond")
-              end
-            else Error (msg "BTL.verify_block: incompatible conditions in Bcond")
-          else Error (msg "BTL.verify_block: different lr in Bcond")
-      | _ => Error (msg "BTL.verify_block: incorrect cfg Bcond")
-      end
-  end.
-
-(* This property expresses that "relation" [match_iblock] is a partial function (see also [iblock_istep_run_equiv] above) *)
-Lemma verify_block_correct dupmap cfg ib: forall pc isfst fin,
-   verify_block dupmap cfg isfst pc ib = (OK fin) -> match_iblock dupmap cfg isfst pc ib fin.
-Proof.
-  induction ib; intros;
-  try (unfold verify_block in H; destruct (cfg!pc) eqn:EQCFG; [ idtac | discriminate; fail ]).
-  - (* BF *)
-    destruct fi; unfold verify_block in H.
-    + (* Bgoto *)
-      monadInv H.
-      destruct (isfst); simpl in EQ0; inv EQ0.
-      eapply verify_is_copy_correct in EQ.
-      constructor; assumption.
-    + (* Breturn *)
-      destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate.
-      destruct (option_eq _ _ _); try discriminate. inv H.
-      eapply mib_BF; eauto. constructor.
-    + (* Bcall *)
-      destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate.
-      monadInv H.
-      eapply verify_is_copy_correct in EQ.
-      destruct (signature_eq _ _); try discriminate.
-      destruct (product_eq _ _ _ _); try discriminate.
-      destruct (list_eq_dec _ _ _); try discriminate.
-      destruct (Pos.eq_dec _ _); try discriminate. subst.
-      inv EQ0. eapply mib_BF; eauto. constructor; assumption.
-    + (* Btailcall *)
-      destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate.
-      destruct (signature_eq _ _); try discriminate.
-      destruct (product_eq _ _ _ _); try discriminate.
-      destruct (list_eq_dec _ _ _); try discriminate. subst.
-      inv H. eapply mib_BF; eauto. constructor.
-    + (* Bbuiltin *)
-      destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate.
-      monadInv H.
-      eapply verify_is_copy_correct in EQ.
-      destruct (external_function_eq _ _); try discriminate.
-      destruct (list_eq_dec _ _ _); try discriminate.
-      destruct (builtin_res_eq_pos _ _); try discriminate. subst.
-      inv EQ0. eapply mib_BF; eauto. constructor; assumption.
-    + (* Bjumptable *)
-      destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate.
-      monadInv H.
-      eapply verify_is_copy_list_correct in EQ.
-      destruct (Pos.eq_dec _ _); try discriminate. subst.
-      inv EQ0. eapply mib_BF; eauto. constructor; assumption.
-  - (* Bnop *)
-    destruct oiinfo; simpl in *.
-    + destruct (cfg!pc) eqn:EQCFG; try discriminate.
-      destruct i0; inv H. constructor; assumption.
-    + destruct isfst; try discriminate. inv H.
-      constructor; assumption.
-  - (* Bop *)
-    destruct i; try discriminate.
-    destruct (eq_operation _ _); try discriminate.
-    destruct (list_eq_dec _ _ _); try discriminate.
-    destruct (Pos.eq_dec _ _); try discriminate. inv H.
-    constructor; assumption.
-  - (* Bload *)
-    destruct i; try discriminate.
-    do 2 (destruct (trapping_mode_eq _ _); try discriminate).
-    simpl in H.
-    destruct (chunk_eq _ _); try discriminate.
-    destruct (eq_addressing _ _); try discriminate.
-    destruct (list_eq_dec _ _ _); try discriminate.
-    destruct (Pos.eq_dec _ _); try discriminate. inv H.
-    constructor; assumption.
-  - (* Bstore *)
-    destruct i; try discriminate.
-    destruct (chunk_eq _ _); try discriminate.
-    destruct (eq_addressing _ _); try discriminate.
-    destruct (list_eq_dec _ _ _); try discriminate.
-    destruct (Pos.eq_dec _ _); try discriminate. inv H.
-    constructor; assumption.
-  - (* Bseq *)
-    monadInv H.
-    destruct x; try discriminate.
-    eapply mib_seq_Some.
-    eapply IHib1; eauto.
-    eapply IHib2; eauto.
-  - (* Bcond *)
-    destruct i; try discriminate.
-    destruct (list_eq_dec _ _ _); try discriminate.
-    destruct (eq_condition _ _); try discriminate.
-    fold (verify_block dupmap cfg false n ib1) in H.
-    fold (verify_block dupmap cfg false n0 ib2) in H.
-    monadInv H.
-    destruct x, x0; try destruct (Pos.eq_dec _ _); try discriminate.
-    all: inv EQ2; eapply mib_cond; eauto; econstructor.
-Qed.
-Local Hint Resolve verify_block_correct: core.
-
-Fixpoint verify_blocks dupmap (cfg: code) (cfg':RTL.code) l: res unit :=
-  match l with
-  | nil => OK tt
-  | (pc, pc')::l =>
-    match cfg!pc with
-    | Some ib => do o <- verify_block dupmap cfg' true pc' ib.(entry);
-                 match o with
-                 | None => verify_blocks dupmap cfg cfg' l
-                 | _ => Error(msg "BTL.verify_blocks.end")
-                 end
-    | _ => Error(msg "BTL.verify_blocks.entry")
-    end
-  end.
 
-Definition verify_cfg dupmap (cfg: code) (cfg':RTL.code): res unit :=
-  verify_blocks dupmap cfg cfg' (PTree.elements dupmap).
-
-Lemma verify_cfg_correct dupmap cfg cfg' tt:
-  verify_cfg dupmap cfg cfg' = OK tt ->
-  match_cfg dupmap cfg cfg'.
-Proof.
-  unfold verify_cfg. 
-  intros X pc pc' H; generalize X; clear X.
-  exploit PTree.elements_correct; eauto.
-  generalize tt pc pc' H; clear tt pc pc' H.
-  generalize (PTree.elements dupmap).
-  induction l as [|[pc1 pc1']l]; simpl.
-  - tauto.
-  - intros pc pc' DUP u H. 
-    unfold bind. 
-    repeat autodestruct.
-    intros; subst.
-    destruct H as [H|H]; eauto.
-    inversion H; subst.
-    eexists; split; eauto.
-Qed.
-
-Definition verify_function dupmap f f' : res unit :=
-  do _ <- verify_is_copy dupmap (fn_entrypoint f) (RTL.fn_entrypoint f');
-  verify_cfg dupmap (fn_code f) (RTL.fn_code f').
+(** * Auxiliary general purpose functions on BTL *)
 
 Definition is_goto (ib: iblock): bool :=
   match ib with
   | BF (Bgoto _) _ => true
   | _ => false
   end.
+