(** 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.
Local Hint Unfold regs_lessdef: core.

Lemma fsem2cfgsem_ibistep_simu ge sp rs1 m1 rs1' m1' of ib
  (ISTEP: iblock_istep ge sp rs1 m1 ib rs1' m1' of): forall
   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; intros.
  - (* Bop *)
    exploit (@eval_operation_lessdef _ _ ge sp op (rs ## args)); eauto.
    intros (v1 & EVAL' & LESSDEF).
    do 2 eexists; rewrite EVAL'. repeat (split; eauto).
    eapply set_reg_lessdef; eauto.
  - (* Bload *)
    inv LOAD.
    + exploit (@eval_addressing_lessdef _ _ ge sp addr (rs ## args)); eauto.
      intros (v2 & EVAL' & LESSDEF). exploit Mem.loadv_extends; eauto.
      intros (v3 & LOAD' & LESSDEF'); autodestruct;
      do 2 eexists; rewrite EVAL', LOAD';
      repeat (split; eauto); eapply set_reg_lessdef; eauto.
    + destruct (eval_addressing ge sp addr rs ## args) eqn:EQA;
      repeat autodestruct; do 2 eexists;
      repeat (split; eauto); eapply set_reg_lessdef; eauto.
  - (* Bstore *)
    exploit (@eval_addressing_lessdef _ _ ge sp addr (rs ## args)); eauto.
    intros (v2 & EVAL' & LESSDEF). exploit Mem.storev_extends; eauto.
    intros (v3 & STORE' & LESSDEF').
    do 2 eexists; rewrite EVAL', STORE'. repeat (split; eauto).
  - (* Bseq stop *)
    exploit IHISTEP; eauto. intros (rs2' & m2' & IBIS & REGS' & MEMS').
    destruct (iblock_istep_run _ _ _ _ _); try congruence.
    destruct o, _fin; simpl in *; try congruence. eauto.
  - (* Bseq continue *)
    exploit IHISTEP1; eauto.
    clear ISTEP1 REGS MEMS.
    intros (rs3 & m3 & ISTEP3 & REGS3 & MEMS3).
    rewrite ISTEP3; simpl. rewrite iblock_istep_run_equiv in ISTEP2.
    exploit IHISTEP2; eauto.
  - (* Bcond *)
    erewrite (@eval_condition_lessdef cond (rs ## args)); eauto.
Qed.

Local Hint Constructors lessdef_stackframe lessdef_state final_step list_forall2 step: 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' trap 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'
}.

(** * 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 tm') 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 chunk in Bload")
          else Error (msg "BTL.verify_block: different trapping_mode 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 chunk 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.
    destruct (trapping_mode_eq _ _); 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.
  - (* 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.