splitting BTL by introducing BTLmatchRTL

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

1 files changed, 587 insertions, 0 deletions

diff --git a/scheduling/BTLmatchRTL.v b/scheduling/BTLmatchRTL.v
new file mode 100644
index 00000000..23ff6681
--- /dev/null
+++ b/scheduling/BTLmatchRTL.v
@@ -0,0 +1,587 @@
+(** General notions about the bisimulation BTL <-> RTL.
+
+This bisimulation is proved on the "CFG semantics" of BTL called [cfgsem] defined below,
+such that the full state of registers is preserved when exiting blocks.
+
+*)
+
+Require Import Coqlib Maps.
+Require Import AST Integers Values Events Memory Globalenvs Smallstep.
+Require Import RTL Op Registers OptionMonad Lia.
+Require Export BTL.
+
+(* 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).
+
+(* * Simulation of BTL fsem by BTL cfgsem: a lock-step less-def simulation.
+*)
+
+
+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 init_regs_lessdef_preserv find_function_lessdef regs_lessdef_regs
+  lessdef_state_refl: 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 lessdef_stackframe lessdef_state final_step list_forall2 step: 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.
+
+(** * Matching BTL (for cfgsem) and RTL code
+
+We define a single verifier able to prove a bisimulation between BTL and RTL code.
+
+Hence, in a sense, our verifier imitates the approach of Duplicate, where [dupmap] maps the BTL nodes to the RTL nodes.
+
+The [match_function] definition gives a "relational" specification of the verifier...
+*)
+
+Require Import Errors.
+
+Inductive match_final_inst (dupmap: PTree.t node): final -> instruction -> Prop :=
+  | 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
+      (* here [b2] is dead code ! Our verifier rejects 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: BTL.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.
+
+Record match_function dupmap f f': Prop := {
+  dupmap_correct: match_cfg dupmap (BTL.fn_code f) (RTL.fn_code f');
+  dupmap_entrypoint: dupmap!(fn_entrypoint f) = Some (RTL.fn_entrypoint f');
+  preserv_fnsig: fn_sig f = RTL.fn_sig f';
+  preserv_fnparams: fn_params f = RTL.fn_params f';
+  preserv_fnstacksize: fn_stacksize f = RTL.fn_stacksize f'
+}.
+
+Inductive match_fundef: BTL.fundef -> RTL.fundef -> Prop :=
+  | match_Internal dupmap f f': match_function dupmap f f' -> match_fundef (Internal f) (Internal f')
+  | match_External ef: match_fundef (External ef) (External ef).
+
+Inductive match_stackframes: stackframe -> RTL.stackframe -> Prop :=
+  | match_stackframe_intro 
+      dupmap res f sp pc rs f' pc'
+      (TRANSF: match_function dupmap f f')
+      (DUPLIC: dupmap!pc = Some pc')
+      : match_stackframes (BTL.Stackframe res f sp pc rs) (RTL.Stackframe res f' sp pc' rs).
+
+
+(** * 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').
+
+Lemma verify_function_correct dupmap f f' tt:
+  verify_function dupmap f f' = OK tt ->
+  fn_sig f = RTL.fn_sig f' ->
+  fn_params f = RTL.fn_params f' ->
+  fn_stacksize f = RTL.fn_stacksize f' ->
+  match_function dupmap f f'.
+Proof.
+  unfold verify_function; intro VERIF. monadInv VERIF.
+  constructor; eauto.
+  eapply verify_cfg_correct; eauto.
+Qed.
+