start the new "BTL" IR.

1 files changed, 575 insertions, 0 deletions

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
new file mode 100644
index 00000000..8bdafb89
--- /dev/null
+++ b/scheduling/BTL.v
@@ -0,0 +1,575 @@
+(** The BTL intermediate language: abstract syntax and semantics.
+
+  BTL stands for "Block Transfer Language".
+
+  Informally, a block is a piece of "loop-free" code, with a single entry-point,
+  hence, such that transformation preserving locally the semantics of each block,
+  preserve also globally the semantics of the function.
+
+  a BTL function is a CFG where each node is such a block, represented by structured code.
+
+  BTL gives a structured view of RTL code.
+  It is dedicated to optimizations validated by "symbolic simulation" over blocks.
+
+
+*)
+
+Require Import Coqlib Maps.
+Require Import AST Integers Values Events Memory Globalenvs Smallstep.
+Require Import RTL Op Registers OptionMonad.
+
+(** * Abstract syntax *)
+
+Definition exit := node.  (* we may generalize this with register renamings at exit, 
+                             like in "phi" nodes of SSA-form *)
+
+(** final instructions (that stops block execution) *)
+Inductive final: Type :=
+  | Bgoto (succ:exit) (** No operation -- just branch to [succ]. *)
+  | Breturn (res: option reg)
+      (** terminates the execution of the current function.  It returns the value of the given
+          register, or [Vundef] if none is given. *)
+  | Bcall (sig: signature) (fn: reg + ident) (args:list reg) (dest:reg) (succ:exit)
+      (** invokes the function determined by [fn] (either a function pointer found in a register or a
+          function name), giving it the values of registers [args] as arguments.
+          It stores the return value in [dest] and branches to [succ]. *)
+  | Btailcall (sig:signature) (fn: reg + ident) (args: list reg)
+      (**  performs a function invocation in tail-call position 
+          (the current function terminates after the call, returning the result of the callee)  
+      *)
+  | Bbuiltin (ef:external_function) (args:list (builtin_arg reg)) (dest:builtin_res reg) (succ:exit)
+      (** calls the built-in function identified by [ef], giving it the values of [args] as arguments.
+          It stores the return value in [dest] and branches to [succ]. *)
+  | Bjumptable (arg:reg) (tbl:list exit)
+      (** [Bjumptable arg tbl] transitions to the node that is the [n]-th
+          element of the list [tbl], where [n] is the unsigned integer value of register [arg]. *)
+  .
+
+(* instruction block *)
+Inductive iblock: Type :=
+(* final instructions that stops block execution *)
+  | BF (fi: final)
+(* basic instructions that continues block execution, except when aborting *)
+  | Bnop (* nop instruction *)
+  | Bop (op:operation) (args:list reg) (dest:reg) 
+      (** performs the arithmetic operation [op] over the values of registers [args], stores the result in [dest] *)
+  | Bload (trap:trapping_mode) (chunk:memory_chunk) (addr:addressing) (args:list reg) (dest:reg)
+      (** loads a [chunk] quantity from the address determined by the addressing mode [addr] 
+          and the values of the [args] registers, stores the quantity just read into [dest].
+          If trap=NOTRAP, then failures lead to a default value written to [dest]. *)
+  | Bstore (chunk:memory_chunk) (addr:addressing) (args:list reg) (src:reg)
+      (** stores the value of register [src] in the [chunk] quantity at the
+          the address determined by the addressing mode [addr] and the
+          values of the [args] registers. *)
+(* composed instructions *)
+  | Bseq (b1 b2: iblock)
+      (** starts by running [b1] and stops here if execution of [b1] has reached a final instruction or aborted
+          or continue with [b2] otherwise *)
+  | Bcond (cond:condition) (args:list reg) (ifso ifnot: iblock) (info:option bool)
+      (** evaluates the boolean condition [cond] over the values of registers [args].  
+          If the condition is true, it continues on [ifso].
+          If the condition is false, it continues on [ifnot].
+          [info] is a ghost field there to provide information relative to branch prediction. *)
+  .
+Coercion BF: final >-> iblock.
+
+
+(** NB: - a RTL [(Inop pc)] ending a branch of block is encoded by [(Bseq Bnop (Bgoto pc))].
+        - a RTL [(Inop pc)] in the middle of a branch is simply encoded by [Bnop].
+        - the same trick appears for all "basic" instructions and [Icond].
+*)
+
+
+
+Record iblock_info := { 
+  entry: iblock;
+  input_regs: Regset.t (* extra liveness information ignored by BTL semantics *)
+}.
+
+Definition code: Type := PTree.t iblock_info.
+
+Record function: Type := mkfunction {
+  fn_sig: signature;
+  fn_params: list reg;
+  fn_stacksize: Z;
+  fn_code: code;
+  fn_entrypoint: node
+}.
+
+(** A function description comprises a control-flow graph (CFG) [fn_code]
+    (a partial finite mapping from nodes to instructions).  As in Cminor,
+    [fn_sig] is the function signature and [fn_stacksize] the number of bytes
+    for its stack-allocated activation record.  [fn_params] is the list
+    of registers that are bound to the values of arguments at call time.
+    [fn_entrypoint] is the node of the first instruction of the function
+    in the CFG. *)
+
+Definition fundef := AST.fundef function.
+
+Definition program := AST.program fundef unit.
+
+Definition funsig (fd: fundef) :=
+  match fd with
+  | Internal f => fn_sig f
+  | External ef => ef_sig ef
+  end.
+
+(** * Operational semantics *)
+
+Definition genv := Genv.t fundef unit.
+
+(** The dynamic semantics of BTL is similar to RTL,
+    except that the step of one instruction is generalized into the run of one [iblock].
+*)
+
+Inductive stackframe : Type :=
+  | Stackframe:
+      forall (res: reg)            (**r where to store the result *)
+             (f: function)         (**r calling function *)
+             (sp: val)             (**r stack pointer in calling function *)
+             (succ: exit)          (**r program point in calling function *)
+             (rs: regset),         (**r register state in calling function *)
+      stackframe.
+
+Inductive state : Type :=
+  | State:
+      forall (stack: list stackframe) (**r call stack *)
+             (f: function)            (**r current function *)
+             (sp: val)                (**r stack pointer *)
+             (pc: node)               (**r current program point in [c] *)
+             (rs: regset)             (**r register state *)
+             (m: mem),                (**r memory state *)
+      state
+  | Callstate:
+      forall (stack: list stackframe) (**r call stack *)
+             (f: fundef)              (**r function to call *)
+             (args: list val)         (**r arguments to the call *)
+             (m: mem),                (**r memory state *)
+      state
+  | Returnstate:
+      forall (stack: list stackframe) (**r call stack *)
+             (v: val)                 (**r return value for the call *)
+             (m: mem),                (**r memory state *)
+      state.
+
+(** outcome of a block execution *)
+Record outcome := {
+   _rs: regset;
+   _m: mem;
+   _fin: option final 
+}.
+
+Section RELSEM.
+
+Variable ge: genv.
+
+Definition find_function (ros: reg + ident) (rs: regset) : option fundef :=
+  match ros with
+  | inl r => Genv.find_funct ge rs#r
+  | inr symb =>
+      match Genv.find_symbol ge symb with
+      | None => None
+      | Some b => Genv.find_funct_ptr ge b
+      end
+  end.
+
+Local Open Scope option_monad_scope.
+
+(** internal big-step execution of one iblock *)
+Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option final -> Prop :=
+  | exec_final rs m fin: iblock_istep sp rs m (BF fin) rs m (Some fin)
+  | exec_nop rs m: iblock_istep sp rs m Bnop rs m None
+  | exec_op rs m op args res v
+     (EVAL: eval_operation ge sp op rs##args m = Some v)
+     : iblock_istep sp rs m (Bop op args res) (rs#res <- v) m None
+  | exec_load_TRAP rs m chunk addr args dst a v
+     (EVAL: eval_addressing ge sp addr rs##args = Some a)
+     (LOAD: Mem.loadv chunk m a = Some v)
+     : iblock_istep sp rs m (Bload TRAP chunk addr args dst) (rs#dst <- v) m None
+  | exec_store rs m chunk addr args src a m' 
+     (EVAL: eval_addressing ge sp addr rs##args = Some a)
+     (STORE: Mem.storev chunk m a rs#src = Some m')
+     : iblock_istep sp rs m (Bstore chunk addr args src) rs m' None
+  | exec_seq_stop rs m b1 b2 rs' m' fin
+     (EXEC: iblock_istep sp rs m b1 rs' m' (Some fin))
+     : iblock_istep sp rs m (Bseq b1 b2) rs' m' (Some fin)
+  | exec_seq_continue rs m b1 b2 rs1 m1 rs' m' ofin
+     (EXEC1: iblock_istep sp rs m b1 rs1 m1 None)
+     (EXEC2: iblock_istep sp rs1 m1 b2 rs' m' ofin)
+     : iblock_istep sp rs m (Bseq b1 b2) rs' m' ofin
+  | exec_cond rs m cond args ifso ifnot i b rs' m' ofin
+     (EVAL: eval_condition cond rs##args m = Some b)
+     (EXEC: iblock_istep sp rs m (if b then ifso else ifnot) rs' m' ofin)
+     : iblock_istep sp rs m (Bcond cond args ifso ifnot i) rs' m' ofin
+  .
+Local Hint Constructors iblock_istep: core.
+
+(** A functional variant of [iblock_istep_run] of [iblock_istep].
+Lemma [iblock_istep_run_equiv] below provides a proof that "relation" [iblock_istep] is a "partial function".
+*)
+Fixpoint iblock_istep_run sp ib rs m: option outcome := 
+  match ib with
+  | BF fin =>
+      Some {| _rs := rs; _m := m; _fin := Some fin |}
+  (* basic instructions *)
+  | Bnop =>
+      Some {| _rs := rs; _m:= m; _fin := None |}
+  | Bop op args res =>
+      SOME v <- eval_operation ge sp op rs##args m IN
+      Some {| _rs := rs#res <- v; _m:= m; _fin := None |}
+  | Bload TRAP chunk addr args dst =>
+      SOME a <- eval_addressing ge sp addr rs##args IN
+      SOME v <- Mem.loadv chunk m a IN
+      Some {| _rs := rs#dst <- v; _m:= m; _fin := None |}
+  | Bload NOTRAP chunk addr args dst =>
+      None (* TODO *)
+  | Bstore chunk addr args src =>
+      SOME a <- eval_addressing ge sp addr rs##args IN
+      SOME m' <- Mem.storev chunk m a rs#src IN
+      Some {| _rs := rs; _m:= m'; _fin := None |}
+ (* composed instructions *)
+  | Bseq b1 b2 =>
+      SOME out1 <- iblock_istep_run sp b1 rs m IN
+      match out1.(_fin) with
+      | None => iblock_istep_run sp b2 out1.(_rs) out1.(_m)
+      | _ => Some out1 (* stop execution on the 1st final instruction *)
+      end
+  | Bcond cond args ifso ifnot _ =>
+      SOME b <- eval_condition cond rs##args m IN
+      iblock_istep_run sp (if b then ifso else ifnot) rs m
+  end.
+
+Lemma iblock_istep_run_equiv sp rs m ib rs' m' ofin:
+  iblock_istep sp rs m ib rs' m' ofin <-> iblock_istep_run sp ib rs m = Some {| _rs := rs'; _m:= m'; _fin := ofin |}.
+Proof.
+  constructor.
+  - induction 1; simpl; try autodestruct; try_simplify_someHyps.
+  - generalize rs m rs' m' ofin; clear rs m rs' m' ofin.
+    induction ib; simpl; repeat (try autodestruct; try_simplify_someHyps).
+    destruct o; try_simplify_someHyps; subst; eauto.
+Qed.
+
+Inductive final_step stack f sp rs m: final -> trace -> state -> Prop :=
+  | exec_Bgoto pc:
+      final_step stack f sp rs m (Bgoto pc) E0
+                 (State stack f sp pc rs m)
+  | exec_Breturn or stk m':
+      sp = (Vptr stk Ptrofs.zero) ->
+      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
+      final_step stack f sp rs m (Breturn or)
+        E0 (Returnstate stack (regmap_optget or Vundef rs) m')
+  | exec_Bcall sig ros args res pc' fd:
+      find_function ros rs = Some fd ->
+      funsig fd = sig ->
+      final_step stack f sp rs m (Bcall sig ros args res pc')
+        E0 (Callstate (Stackframe res f sp pc' rs :: stack) fd rs##args m)
+  | exec_Btailcall sig ros args stk m' fd:
+      find_function ros rs = Some fd ->
+      funsig fd = sig ->
+      sp = (Vptr stk Ptrofs.zero) ->
+      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
+      final_step stack f sp rs m (Btailcall sig ros args)
+        E0 (Callstate stack fd rs##args m')
+  | exec_Bbuiltin ef args res pc' vargs t vres m':
+      eval_builtin_args ge (fun r => rs#r) sp m args vargs ->
+      external_call ef ge vargs m t vres m' ->
+      final_step stack f sp rs m (Bbuiltin ef args res pc')
+         t (State stack f sp pc' (regmap_setres res vres rs) m')
+  | exec_Bjumptable arg tbl n pc':
+      rs#arg = Vint n ->
+      list_nth_z tbl (Int.unsigned n) = Some pc' ->
+      final_step stack f sp rs m (Bjumptable arg tbl)
+        E0 (State stack f sp pc' rs m)
+.
+
+(** big-step execution of one iblock *)
+Definition iblock_step stack f sp rs m ib t s: Prop :=
+  exists rs' m' fin, iblock_istep sp rs m ib rs' m' (Some fin) /\ final_step stack f sp rs' m' fin t s.
+
+(** The transitions are presented as an inductive predicate
+  [step ge st1 t st2], where [ge] is the global environment,
+  [st1] the initial state, [st2] the final state, and [t] the trace
+  of system calls performed during this transition. *)
+
+Inductive step: state -> trace -> state -> Prop :=
+  | exec_iblock stack ib f sp pc rs m t s:
+      (fn_code f)!pc = Some ib ->
+      iblock_step stack f sp rs m ib.(entry) t s ->
+      step (State stack f sp pc rs m) t s
+  | exec_function_internal stack f args m m' stk:
+      Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
+      step (Callstate stack (Internal f) args m)
+        E0 (State stack
+                  f
+                  (Vptr stk Ptrofs.zero)
+                  f.(fn_entrypoint)
+                  (init_regs args f.(fn_params))
+                  m')
+  | exec_function_external stack ef args res t m m':
+      external_call ef ge args m t res m' ->
+      step (Callstate stack (External ef) args m)
+         t (Returnstate stack res m')
+  | exec_return stack res f sp pc rs vres m:
+      step (Returnstate (Stackframe res f sp pc rs :: stack) vres m)
+        E0 (State stack f sp pc (rs#res <- vres) m)
+.
+
+End RELSEM.
+
+(** Execution of whole programs are described as sequences of transitions
+  from an initial state to a final state.  An initial state is a [Callstate]
+  corresponding to the invocation of the ``main'' function of the program
+  without arguments and with an empty call stack. *)
+
+Inductive initial_state (p: program): state -> Prop :=
+  | initial_state_intro: forall b f m0,
+      let ge := Genv.globalenv p in
+      Genv.init_mem p = Some m0 ->
+      Genv.find_symbol ge p.(prog_main) = Some b ->
+      Genv.find_funct_ptr ge b = Some f ->
+      funsig f = signature_main ->
+      initial_state p (Callstate nil f nil m0).
+
+(** A final state is a [Returnstate] with an empty call stack. *)
+
+Inductive final_state: state -> int -> Prop :=
+  | final_state_intro: forall r m,
+      final_state (Returnstate nil (Vint r) m) r.
+
+(** The small-step semantics for a program. *)
+
+Definition semantics (p: program) :=
+  Semantics step (initial_state p) final_state (Genv.globalenv p).
+
+
+(** 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:
+      cfg!pc = Some i ->
+      match_final_inst dupmap fi i ->
+      match_iblock dupmap cfg isfst pc (BF fi) None
+  | mib_nop isfst pc pc':
+      cfg!pc = Some (Inop pc') ->
+      match_iblock dupmap cfg isfst pc Bnop (Some pc')
+  | mib_op isfst pc pc' op lr r:
+      cfg!pc = Some (Iop op lr r pc') ->
+      match_iblock dupmap cfg isfst pc (Bop op lr r) (Some pc')
+  | mib_load isfst pc pc' tm m a lr r:
+      cfg!pc = Some (Iload tm m a lr r pc') -> 
+      match_iblock dupmap cfg isfst pc (Bload tm m a lr r) (Some pc')
+  | mib_store isfst pc pc' m a lr r:
+      cfg!pc = Some (Istore m a lr r pc') -> 
+      match_iblock dupmap cfg isfst pc (Bstore m a lr r) (Some pc')
+  | mib_exit pc pc': 
+      dupmap!pc = (Some pc') ->
+      match_iblock dupmap cfg false pc' (Bgoto pc) 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 i':
+      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 i) opc
+  .
+
+(* Partial copy of Duplicate and Duplicateproof. *)
+
+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.
+
+Record match_function dupmap f f': Prop := {
+  dupmap_correct: match_cfg dupmap (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: 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 (Stackframe res f sp pc rs) (RTL.Stackframe res f' sp pc' rs).
+
+Inductive match_states: state -> RTL.state -> Prop :=
+  | match_states_intro 
+      dupmap st f sp pc rs m st' f' pc'
+      (STACKS: list_forall2 match_stackframes st st')
+      (TRANSF: match_function dupmap f f')
+      (DUPLIC: dupmap!pc' = Some pc)
+      : match_states (State st f sp pc rs m) (RTL.State st' f' sp pc' rs m)
+  | match_states_call
+      st st' f f' args m
+      (STACKS: list_forall2 match_stackframes st st')
+      (TRANSF: match_fundef f f')
+      : match_states (Callstate st f args m) (RTL.Callstate st' f' args m)
+  | match_states_return
+      st st' v m
+      (STACKS: list_forall2 match_stackframes st st')
+      : match_states (Returnstate st v m) (RTL.Returnstate st' v m)
+   .
+
+(** 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 "verify_is_copy None")
+  | Some revn => match (Pos.compare n' revn) with Eq => OK tt | _ => Error(msg "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 "verify_is_copy_list: ln' bigger than ln") end
+  | nil => match ln' with
+          | n :: ln' => Error (msg "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: deuxième étape (après BTLtoRTLproof.plus_simulation) *)
+Parameter verify_block: PTree.t node -> RTL.code -> bool -> node -> iblock -> res (option node).
+
+(* This property expresses that "relation" [match_iblock] is a partial function (see also [iblock_istep_run_equiv] above) *)
+Lemma verify_block_correct: forall dupmap cfg isfst pc ib fin,
+   verify_block dupmap cfg isfst pc ib = (OK fin) -> match_iblock dupmap cfg isfst pc ib fin.
+Admitted.
+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 "verify_blocks.end")
+                 end
+    | _ => Error(msg "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.