Add new block generation for Gible

1 files changed, 1011 insertions, 0 deletions

diff --git a/src/hls/GibleSeqgenproof.v b/src/hls/GibleSeqgenproof.v
new file mode 100644
index 0000000..55b25d1
--- /dev/null
+++ b/src/hls/GibleSeqgenproof.v
@@ -0,0 +1,1011 @@
+(*|
+..
+   Vericert: Verified high-level synthesis.
+   Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com>
+
+   This program is free software: you can redistribute it and/or modify
+   it under the terms of the GNU General Public License as published by
+   the Free Software Foundation, either version 3 of the License, or
+   (at your option) any later version.
+
+   This program is distributed in the hope that it will be useful,
+   but WITHOUT ANY WARRANTY; without even the implied warranty of
+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+   GNU General Public License for more details.
+
+   You should have received a copy of the GNU General Public License
+   along with this program.  If not, see <https://www.gnu.org/licenses/>.
+
+================
+RTLBlockgenproof
+================
+
+.. coq:: none
+|*)
+
+Require compcert.backend.RTL.
+Require Import compcert.common.AST.
+Require Import compcert.common.Errors.
+Require Import compcert.common.Globalenvs.
+Require Import compcert.lib.Maps.
+Require Import compcert.backend.Registers.
+Require Import compcert.common.Smallstep.
+Require Import compcert.common.Events.
+Require Import compcert.common.Memory.
+Require Import compcert.common.Values.
+
+Require Import vericert.common.Vericertlib.
+Require Import vericert.common.DecEq.
+Require Import vericert.hls.Gible.
+Require Import vericert.hls.GibleSeq.
+Require Import vericert.hls.GibleSeqgen.
+
+#[local] Open Scope positive.
+
+(*|
+Defining a find block specification
+===================================
+
+Basically, it should be able to find the location of the block without using the
+``find_block`` function, so that this is more useful for the proofs.  There are
+various different types of options that could come up though:
+
+1. The instruction is a standard instruction present inside of a basic block.
+2. The instruction is a standard instruction which ends with a ``goto``.
+3. The instruction is a control-flow instruction.
+
+For case number 1, there should exist a value in the list of instructions, such
+that the instructions match exactly, and the indices match as well.  In the
+original code, this instruction must have been going from the current node to
+the node - 1.
+
+For case number 2, there should be an instruction at the right index again,
+however, this time there will also be a ``goto`` instruction in the control-flow
+part of the basic block.
+
+For case number 3, there should be a ``nop`` instruction in the basic block, and
+then the equivalent control-flow instruction ending the basic block.
+
+In the end though, it seems like two cases are actually enough, as the last two
+cases are similar enough that they can be merged into one.
+|*)
+
+Definition all_max {A} (c: PTree.t A) p: Prop :=
+  Forall (fun x => x <= p) (map fst (PTree.elements c)).
+
+Definition offset (pc pc': positive): nat := Pos.to_nat pc' - Pos.to_nat pc.
+
+Section CORRECTNESS.
+
+  Context (prog : RTL.program).
+  Context (tprog : GibleSeq.program).
+
+  Let ge : RTL.genv := Globalenvs.Genv.globalenv prog.
+  Let tge : genv := Globalenvs.Genv.globalenv tprog.
+
+(*|
+Matches the basic block that should be present in the state.  This simulates the
+small step execution of the basic block from the big step semantics that are
+currently present.
+
+Why does it not need to find the pc' value using ``find_block``?
+
+It doesn't have to find the value because it's given as an input, and the
+finding is actually done at that higher level already.
+|*)
+
+(*  Variant match_bblock (tc: code) (pc pc': node): list instr -> Prop :=
+    | match_bblock_intro :
+      forall bb cf,
+        tc ! pc' = Some (mk_bblock bb cf) ->
+        match_bblock tc pc pc' (list_drop (offset pc pc') bb).*)
+
+  Definition imm_succ (pc pc': node) : Prop := pc' = Pos.pred pc.
+
+  Definition valid_succ (tc: code) (pc: node) : Prop := exists b, tc ! pc = Some b.
+
+  Inductive match_block (c: RTL.code) (tc: code) (pc: node): BB.t -> Prop :=
+  (*
+   * Basic Block Instructions
+   *)
+  | match_block_nop b pc':
+    c ! pc = Some (RTL.Inop pc') ->
+    match_block c tc pc' b ->
+    match_block c tc pc (RBnop :: b)
+  | match_block_op b op args dst pc':
+    c ! pc = Some (RTL.Iop op args dst pc') ->
+    match_block c tc pc' b ->
+    match_block c tc pc (RBop None op args dst :: b)
+  | match_block_load b chunk addr args dst pc':
+    c ! pc = Some (RTL.Iload chunk addr args dst pc') ->
+    match_block c tc pc' b ->
+    match_block c tc pc (RBload None chunk addr args dst :: b)
+  | match_block_store b chunk addr args src pc':
+    c ! pc = Some (RTL.Istore chunk addr args src pc') ->
+    match_block c tc pc' b ->
+    match_block c tc pc (RBstore None chunk addr args src :: b)
+  (*
+   * Control flow instructions using goto
+   *)
+  | match_block_goto pc':
+    c ! pc = Some (RTL.Inop pc') ->
+    valid_succ tc pc' ->
+    match_block c tc pc (RBnop :: RBexit None (RBgoto pc') :: nil)
+  | match_block_op_cf pc' op args dst:
+    c ! pc = Some (RTL.Iop op args dst pc') ->
+    valid_succ tc pc' ->
+    match_block c tc pc (RBop None op args dst :: RBexit None (RBgoto pc') :: nil)
+  | match_block_load_cf pc' chunk addr args dst:
+    c ! pc = Some (RTL.Iload chunk addr args dst pc') ->
+    valid_succ tc pc' ->
+    match_block c tc pc (RBload None chunk addr args dst :: RBexit None (RBgoto pc') :: nil)
+  | match_block_store_cf pc' chunk addr args src:
+    c ! pc = Some (RTL.Istore chunk addr args src pc') ->
+    valid_succ tc pc' ->
+    match_block c tc pc (RBstore None chunk addr args src :: RBexit None (RBgoto pc') :: nil)
+  (*
+   * Standard control flow instructions
+   *)
+  | match_block_call sig ident args dst pc' :
+    c ! pc = Some (RTL.Icall sig ident args dst pc') ->
+    valid_succ tc pc' ->
+    match_block c tc pc (RBnop :: RBexit None (RBcall sig ident args dst pc') :: nil)
+  | match_block_tailcall sig ident args :
+    c ! pc = Some (RTL.Itailcall sig ident args) ->
+    match_block c tc pc (RBnop :: RBexit None (RBtailcall sig ident args) :: nil)
+  | match_block_builtin ident args dst pc' :
+    c ! pc = Some (RTL.Ibuiltin ident args dst pc') ->
+    valid_succ tc pc' ->
+    match_block c tc pc (RBnop :: RBexit None (RBbuiltin ident args dst pc') :: nil)
+  | match_block_cond cond args pct pcf :
+    c ! pc = Some (RTL.Icond cond args pct pcf) ->
+    valid_succ tc pct ->
+    valid_succ tc pcf ->
+    match_block c tc pc (RBnop :: RBexit None (RBcond cond args pct pcf) :: nil)
+  | match_block_jumptable r ns :
+    c ! pc = Some (RTL.Ijumptable r ns) ->
+    Forall (valid_succ tc) ns ->
+    match_block c tc pc (RBnop :: RBexit None (RBjumptable r ns) :: nil)
+  | match_block_return r :
+    c ! pc = Some (RTL.Ireturn r) ->
+    match_block c tc pc (RBnop :: RBexit None (RBreturn r) :: nil)
+  .
+
+(*|
+Match the code
+~~~~~~~~~~~~~~
+
+The ``match_code`` predicate asserts that for any node in the original
+control-flow graph, there is now a basic block in the new control- and data-flow
+graph that contains the same instruction, but also that the whole basic block
+matches some sequence of instructions starting at the node that corresponds to
+the basic block.
+|*)
+
+  Definition match_code (c: RTL.code) (tc: code) : Prop :=
+    forall pc b, tc ! pc = Some b -> match_block c tc pc b.
+
+  Variant match_stackframe : RTL.stackframe -> stackframe -> Prop :=
+    | match_stackframe_init :
+      forall res f tf sp pc rs
+        (TF: transl_function f = OK tf)
+        (VALID: valid_succ tf.(fn_code) pc),
+        match_stackframe (RTL.Stackframe res f sp pc rs)
+                         (Stackframe res tf sp pc rs (PMap.init false)).
+
+  Definition sem_extrap f pc sp in_s in_s' block :=
+    forall out_s block2,
+      BB.step tge sp in_s block out_s ->
+      f.(fn_code) ! pc = Some block2 ->
+      BB.step tge sp in_s' block2 out_s.
+
+  Lemma match_block_exists_instr :
+    forall c tc pc a,
+      match_block c tc pc a ->
+      exists i, c ! pc = Some i.
+  Proof. inversion 1; eexists; eauto. Qed.
+
+  Lemma match_block_not_nil :
+    forall c tc pc a,
+      match_block c tc pc a -> a <> nil.
+  Proof. inversion 1; crush. Qed.
+
+(*|
+Matching states
+~~~~~~~~~~~~~~~
+
+Initially, the idea was to define the ``match_states`` predicate normally to
+defines how to find the correct ``bb`` that should be executed, as well as the
+value of ``pc``.  However, this does not quite work when proving the equivalence
+of the translation from ``RTL`` to ``RTLBlock``, because one cannot match one
+transition to a transition in RTLBlock.  The alternative to this is to include a
+proof inside of the ``match_states`` that shows that the execution from the
+``pc`` of the start of the basic block to the current point is the same as the
+whole execution (in one big step) of the basic block.
+|*)
+
+  Variant match_states : option BB.t -> RTL.state -> state -> Prop :=
+    | match_state :
+      forall stk stk' f tf sp pc rs m pc0 b rs0 m0
+        (TF: transl_function f = OK tf)
+        (* TODO: I can remove the following [match_code]. *)
+        (CODE: match_code f.(RTL.fn_code) tf.(fn_code))
+        (BLOCK: exists b', tf.(fn_code) ! pc0 = Some b'
+                           /\ match_block f.(RTL.fn_code) tf.(fn_code) pc b)
+        (STK: Forall2 match_stackframe stk stk')
+        (STARSIMU: star RTL.step ge (RTL.State stk f sp pc0 rs0 m0)
+                                  E0 (RTL.State stk f sp pc rs m))
+        (BB: sem_extrap tf pc0 sp (Iexec (mk_instr_state rs (PMap.init false) m))
+                        (Iexec (mk_instr_state rs0 (PMap.init false) m0)) b),
+        match_states (Some b) (RTL.State stk f sp pc rs m)
+                     (State stk' tf sp pc0 rs0 (PMap.init false) m0)
+    | match_callstate :
+      forall cs cs' f tf args m
+        (TF: transl_fundef f = OK tf)
+        (STK: Forall2 match_stackframe cs cs'),
+        match_states None (RTL.Callstate cs f args m) (Callstate cs' tf args m)
+    | match_returnstate :
+      forall cs cs' v m
+        (STK: Forall2 match_stackframe cs cs'),
+        match_states None (RTL.Returnstate cs v m) (Returnstate cs' v m)
+  .
+
+  Definition match_prog (p: RTL.program) (tp: GibleSeq.program) :=
+    Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp.
+
+  Context (TRANSL : match_prog prog tprog).
+
+  Lemma symbols_preserved:
+    forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
+  Proof using TRANSL. intros. eapply (Genv.find_symbol_match TRANSL). Qed.
+
+  Lemma senv_preserved:
+    Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge).
+  Proof using TRANSL. intros; eapply (Genv.senv_transf_partial TRANSL). Qed.
+  #[local] Hint Resolve senv_preserved : rtlbg.
+
+  Lemma function_ptr_translated:
+    forall b f,
+      Genv.find_funct_ptr ge b = Some f ->
+      exists tf, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf.
+  Proof (Genv.find_funct_ptr_transf_partial TRANSL).
+
+  Lemma sig_transl_function:
+    forall (f: RTL.fundef) (tf: GibleSeq.fundef),
+      transl_fundef f = OK tf ->
+      GibleSeq.funsig tf = RTL.funsig f.
+  Proof using.
+    unfold transl_fundef. unfold transf_partial_fundef.
+    intros. destruct_match. unfold bind in *. destruct_match; try discriminate.
+    inv H. unfold transl_function in Heqr.
+    repeat (destruct_match; try discriminate). inv Heqr. auto.
+    inv H; auto.
+  Qed.
+
+  Definition measure (b: option BB.t): nat :=
+    match b with
+    | None => 0
+    | Some b' => 1 + length b'
+    end.
+
+  Lemma check_valid_node_correct :
+    forall a b, check_valid_node a b = true -> valid_succ a b.
+  Proof.
+    intros. unfold valid_succ, check_valid_node in *.
+    destruct_match; try discriminate; eauto.
+  Qed.
+
+  Lemma transl_entrypoint_exists :
+    forall f tf,
+      transl_function f = OK tf ->
+      valid_succ (fn_code tf) (fn_entrypoint tf).
+  Proof.
+    unfold transl_function; intros.
+    repeat (destruct_match; try discriminate; []). inv H. simplify.
+    eauto using check_valid_node_correct.
+  Qed.
+
+  Lemma ceq_eq :
+    forall A a (b: A) c,
+      ceq a b c = true ->
+      b = c.
+  Proof.
+    intros. unfold ceq in H. destruct_match; try discriminate. auto.
+  Qed.
+
+  Ltac unfold_ands :=
+    repeat match goal with
+           | H: _ && _ = true |- _ => apply andb_prop in H
+           | H: _ /\ _ |- _ => inv H
+           | H: ceq _ _ _ = true |- _ => apply ceq_eq in H; subst
+           end.
+
+  Lemma transl_match_code' :
+    forall c tc b pc,
+      check_code c tc pc b = true ->
+      match_block c tc pc b.
+  Proof.
+    induction b; [crush|].
+    - repeat (destruct_match; try discriminate).
+    - intros.
+      unfold check_code in H.
+      do 2 (destruct_match; try discriminate); subst; fold check_code in H.
+      + repeat (destruct_match; try discriminate); try solve [econstructor; eauto].
+        unfold_ands.
+        eapply match_block_goto; eauto. eauto using check_valid_node_correct.
+      + repeat (destruct_match; try discriminate); subst; try solve [unfold_ands; econstructor; eauto].
+        unfold_ands.
+        eapply match_block_op_cf; eauto. eauto using check_valid_node_correct.
+      + repeat (destruct_match; try discriminate); subst; try solve [unfold_ands; econstructor; eauto].
+        unfold_ands.
+        eapply match_block_load_cf; eauto. eauto using check_valid_node_correct.
+      + repeat (destruct_match; try discriminate); subst; try solve [unfold_ands; econstructor; eauto].
+        unfold_ands.
+        eapply match_block_store_cf; eauto. eauto using check_valid_node_correct.
+      + repeat (destruct_match; try discriminate); subst; try solve [unfold_ands; econstructor; eauto].
+        unfold_ands. eapply match_block_call; eauto using check_valid_node_correct.
+        unfold_ands. eapply match_block_call; eauto using check_valid_node_correct.
+      + repeat (destruct_match; try discriminate); subst; try solve [unfold_ands; econstructor; eauto].
+      + repeat (destruct_match; try discriminate); subst; try solve [unfold_ands; econstructor; eauto].
+        unfold_ands. eapply match_block_cond; eauto using check_valid_node_correct.
+      + repeat (destruct_match; try discriminate); subst; try solve [unfold_ands; econstructor; eauto].
+        unfold_ands. eapply match_block_jumptable; eauto using check_valid_node_correct.
+        apply Forall_forall; intros. eapply forallb_forall in H1; eauto using check_valid_node_correct.
+      + repeat (destruct_match; try discriminate); subst; try solve [unfold_ands; econstructor; eauto].
+  Qed.
+
+  Lemma transl_match_code :
+    forall f tf,
+      transl_function f = OK tf ->
+      match_code f.(RTL.fn_code) tf.(fn_code).
+  Proof.
+    unfold transl_function; intros.
+    repeat (destruct_match; try discriminate; []). inv H. simplify.
+    unfold match_code; intros.
+    eapply forall_ptree_true in Heqb0; eauto.
+    unfold check_code in *.
+    eauto using transl_match_code'.
+  Qed.
+
+  Lemma transl_initial_states :
+    forall s1, RTL.initial_state prog s1 ->
+      exists s2, GibleSeq.initial_state tprog s2 /\ match_states None s1 s2.
+  Proof using TRANSL.
+    induction 1.
+    exploit function_ptr_translated; eauto. intros [tf [A B]].
+    do 2 econstructor. simplify. econstructor.
+    apply (Genv.init_mem_transf_partial TRANSL); eauto.
+    replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved; eauto.
+    symmetry; eapply Linking.match_program_main; eauto. eauto.
+    erewrite sig_transl_function; eauto. constructor. auto. auto.
+  Qed.
+
+  Lemma transl_final_states :
+    forall s1 s2 r b,
+      match_states b s1 s2 ->
+      RTL.final_state s1 r ->
+      GibleSeq.final_state s2 r.
+  Proof using.
+    inversion 2; crush. subst. inv H. inv STK. econstructor.
+  Qed.
+
+  Lemma hd_nth_equiv:
+    forall A n (l: list A), hd_error (list_drop n l) = nth_error l n.
+  Proof. induction n; destruct l; crush. Qed.
+
+  Lemma hd_error_Some_exists:
+    forall A (l: list A) n, hd_error l = Some n -> l = n :: tl l.
+  Proof. induction l; crush. Qed.
+
+  Definition imm_succ_dec pc pc' : {imm_succ pc pc'} + {~ imm_succ pc pc'}.
+  Proof.
+    unfold imm_succ. pose proof peq.
+    decide equality.
+  Defined.
+
+  Lemma imm_succ_refl pc : imm_succ pc (Pos.pred pc).
+  Proof. unfold imm_succ; auto. Qed.
+
+  Lemma imm_succ_refl2 pc : imm_succ (Pos.succ pc) pc.
+  Proof. unfold imm_succ; auto using Pos.pred_succ. Qed.
+
+  Lemma sim_star :
+    forall s1 b t s,
+      (exists b' s2,
+        star step tge s1 t s2 /\ ltof _ measure b' b
+        /\ match_states b' s s2) ->
+      exists b' s2,
+        (plus step tge s1 t s2 \/
+           star step tge s1 t s2 /\ ltof _ measure b' b) /\
+          match_states b' s s2.
+  Proof. intros; simplify. do 3 econstructor; eauto. Qed.
+
+  Lemma sim_plus :
+    forall s1 b t s,
+      (exists b' s2, plus step tge s1 t s2 /\ match_states b' s s2) ->
+      exists b' s2,
+        (plus step tge s1 t s2 \/
+           star step tge s1 t s2 /\ ltof _ measure b' b) /\
+          match_states b' s s2.
+  Proof. intros; simplify. do 3 econstructor; eauto. Qed.
+
+  Lemma transl_Inop_correct:
+    forall s f sp pc rs m pc',
+      (RTL.fn_code f) ! pc = Some (RTL.Inop pc') ->
+      forall b s2, match_states b (RTL.State s f sp pc rs m) s2 ->
+        exists b' s2',
+          (plus step tge s2 E0 s2'
+           \/ star step tge s2 E0 s2' /\ ltof _ measure b' b)
+          /\ match_states b' (RTL.State s f sp pc' rs m) s2'.
+  Proof.
+    intros * H.
+    inversion 1; subst; simplify.
+    unfold match_code in *.
+    match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify.
+    { apply sim_star.
+      do 3 econstructor. eapply star_refl. constructor.
+      instantiate (1 := Some b); unfold ltof; auto.
+
+      constructor; try eassumption. econstructor; eauto.
+      eapply star_right; eauto.
+      eapply RTL.exec_Inop; eauto. auto.
+
+      unfold sem_extrap in *. intros.
+      eapply BB. econstructor; eauto.
+      econstructor; eauto. auto.
+    }
+    { apply sim_plus.
+      inv H0. simplify.
+      unfold valid_succ in *; simplify.
+      do 3 econstructor. apply plus_one. econstructor.
+      eassumption. eapply BB; [| eassumption ].
+      econstructor; econstructor; eauto.
+      econstructor. econstructor. econstructor.
+
+      econstructor; try eassumption. eauto.
+      eapply star_refl.
+      unfold sem_extrap. intros. setoid_rewrite H6 in H0.
+      crush.
+    }
+  Qed.
+
+  Lemma eval_op_eq:
+    forall (sp0 : Values.val) (op : Op.operation) (vl : list Values.val) m,
+      Op.eval_operation ge sp0 op vl m = Op.eval_operation tge sp0 op vl m.
+  Proof using TRANSL.
+    intros.
+    destruct op; auto; unfold Op.eval_operation, Genv.symbol_address, Op.eval_addressing32;
+    [| destruct a; unfold Genv.symbol_address ];
+    try rewrite symbols_preserved; auto.
+  Qed.
+
+  Lemma eval_addressing_eq:
+    forall sp addr vl,
+      Op.eval_addressing ge sp addr vl = Op.eval_addressing tge sp addr vl.
+  Proof using TRANSL.
+    intros.
+    destruct addr;
+      unfold Op.eval_addressing, Op.eval_addressing32;
+      unfold Genv.symbol_address;
+      try rewrite symbols_preserved; auto.
+  Qed.
+
+  Lemma transl_Iop_correct_nj:
+    forall s f sp pc rs m op args res pc' v stk' tf pc1 rs1 m1 b x,
+      (RTL.fn_code f) ! pc = Some (RTL.Iop op args res pc') ->
+      Op.eval_operation ge sp op rs ## args m = Some v ->
+      transl_function f = OK tf ->
+      (forall pc0 b0,
+          (fn_code tf) ! pc0 = Some b0 -> match_block (RTL.fn_code f) (fn_code tf) pc0 b0) ->
+      Forall2 match_stackframe s stk' ->
+      star RTL.step ge (RTL.State s f sp pc1 rs1 m1) E0 (RTL.State s f sp pc rs m) ->
+      sem_extrap tf pc1 sp (Iexec {| is_rs := rs; is_ps := PMap.init false; is_mem := m |})
+                 (Iexec {| is_rs := rs1; is_ps := PMap.init false; is_mem := m1 |}) (RBop None op args res :: b) ->
+      (fn_code tf) ! pc1 = Some x ->
+      match_block (RTL.fn_code f) (fn_code tf) pc' b ->
+      exists b' s2',
+        star step tge (State stk' tf sp pc1 rs1 (PMap.init false) m1) E0 s2'
+        /\ ltof _ measure b' (Some (RBop None op args res :: b))
+        /\ match_states b' (RTL.State s f sp pc' rs # res <- v m) s2'.
+  Proof.
+    intros * IOP EVAL TR MATCHB STK STAR BB INCODE MATCHB2.
+    do 3 econstructor. eapply star_refl. constructor.
+    instantiate (1 := Some b); unfold ltof; auto.
+
+    constructor; try eassumption. econstructor; eauto.
+    eapply star_right; eauto.
+    eapply RTL.exec_Iop; eauto. auto.
+
+    unfold sem_extrap in *. intros.
+    eapply BB. econstructor; eauto.
+    econstructor; eauto.
+    rewrite <- eval_op_eq; eassumption.
+    constructor. auto.
+  Qed.
+
+  Lemma transl_Iop_correct_j:
+    forall s f sp pc rs m op args res pc' v stk' tf pc1 rs1 m1 x,
+      (RTL.fn_code f) ! pc = Some (RTL.Iop op args res pc') ->
+      Op.eval_operation ge sp op rs ## args m = Some v ->
+      transl_function f = OK tf ->
+      (forall (pc0 : positive) (b : BB.t),
+          (fn_code tf) ! pc0 = Some b -> match_block (RTL.fn_code f) (fn_code tf) pc0 b) ->
+      Forall2 match_stackframe s stk' ->
+      star RTL.step ge (RTL.State s f sp pc1 rs1 m1) E0 (RTL.State s f sp pc rs m) ->
+      sem_extrap tf pc1 sp (Iexec {| is_rs := rs; is_ps := PMap.init false; is_mem := m |})
+                 (Iexec {| is_rs := rs1; is_ps := PMap.init false; is_mem := m1 |}) (RBop None op args res :: RBexit None (RBgoto pc') :: nil) ->
+      (fn_code tf) ! pc1 = Some x ->
+      valid_succ (fn_code tf) pc' ->
+      exists b' s2,
+        plus step tge (State stk' tf sp pc1 rs1 (PMap.init false) m1) E0 s2 /\
+          match_states b' (RTL.State s f sp pc' rs # res <- v m) s2.
+  Proof.
+    intros * H H0 TF CODE STK STARSIMU BB H3 H7.
+    inv H0. simplify.
+    unfold valid_succ in H7; simplify.
+    do 3 econstructor. apply plus_one. econstructor.
+    eassumption. eapply BB; [| eassumption ].
+    econstructor; econstructor; eauto.
+    rewrite <- eval_op_eq; eassumption.
+    constructor. econstructor. econstructor.
+    econstructor.
+
+    econstructor; try eassumption. eauto.
+    eapply star_refl.
+    unfold sem_extrap. intros. setoid_rewrite H0 in H4.
+    crush.
+  Qed.
+
+  Lemma transl_Iop_correct:
+    forall s f sp pc rs m op args res pc' v,
+      (RTL.fn_code f) ! pc = Some (RTL.Iop op args res pc') ->
+      Op.eval_operation ge sp op rs##args m = Some v ->
+      forall b s2, match_states b (RTL.State s f sp pc rs m) s2 ->
+        exists b' s2',
+          (plus step tge s2 E0 s2'
+           \/ star step tge s2 E0 s2' /\ ltof _ measure b' b)
+          /\ match_states b' (RTL.State s f sp pc' (rs # res <- v) m) s2'.
+  Proof.
+    intros * H H0.
+    inversion 1; subst; simplify.
+    unfold match_code in *.
+    match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify.
+    { apply sim_star; eapply transl_Iop_correct_nj; eassumption. }
+    { apply sim_plus. eapply transl_Iop_correct_j; eassumption. }
+  Qed.
+
+  Lemma transl_Iload_correct:
+    forall s f sp pc rs m chunk addr args dst pc' a v,
+      (RTL.fn_code f) ! pc = Some (RTL.Iload chunk addr args dst pc') ->
+      Op.eval_addressing ge sp addr rs##args = Some a ->
+      Mem.loadv chunk m a = Some v ->
+      forall b s2, match_states b (RTL.State s f sp pc rs m) s2 ->
+        exists b' s2',
+          (plus step tge s2 E0 s2'
+           \/ star step tge s2 E0 s2' /\ ltof _ measure b' b)
+          /\ match_states b' (RTL.State s f sp pc' (rs # dst <- v) m) s2'.
+  Proof.
+    intros * H H0 H1.
+    inversion 1; subst; simplify.
+    unfold match_code in *.
+    match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify.
+    { apply sim_star.
+      do 3 econstructor. eapply star_refl. constructor.
+      instantiate (1 := Some b); unfold ltof; auto.
+
+      constructor; try eassumption. econstructor; eauto.
+      eapply star_right; eauto.
+      eapply RTL.exec_Iload; eauto. auto.
+
+      unfold sem_extrap in *. intros.
+      eapply BB. econstructor; eauto.
+      econstructor; eauto.
+      rewrite <- eval_addressing_eq; eassumption.
+      constructor. auto.
+    }
+    { apply sim_plus.
+      inv H0. simplify.
+      unfold valid_succ in H6; simplify.
+      do 3 econstructor. apply plus_one. econstructor.
+      eassumption. eapply BB; [| eassumption ].
+      econstructor; econstructor; eauto.
+      rewrite <- eval_addressing_eq; eassumption.
+      constructor. econstructor. econstructor.
+      econstructor.
+
+      econstructor; try eassumption. eauto.
+      eapply star_refl.
+      unfold sem_extrap. intros. setoid_rewrite H0 in H6.
+      crush.
+    }
+  Qed.
+
+  Lemma transl_Istore_correct:
+    forall s f sp pc rs m chunk addr args src pc' a m',
+      (RTL.fn_code f) ! pc = Some (RTL.Istore chunk addr args src pc') ->
+      Op.eval_addressing ge sp addr rs##args = Some a ->
+      Mem.storev chunk m a rs#src = Some m' ->
+      forall b s2, match_states b (RTL.State s f sp pc rs m) s2 ->
+        exists b' s2',
+          (plus step tge s2 E0 s2'
+           \/ star step tge s2 E0 s2' /\ ltof _ measure b' b)
+          /\ match_states b' (RTL.State s f sp pc' rs m') s2'.
+  Proof.
+    intros * H H0 H1.
+    inversion 1; subst; simplify.
+    unfold match_code in *.
+    match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify.
+    { apply sim_star.
+      do 3 econstructor. eapply star_refl. constructor.
+      instantiate (1 := Some b); unfold ltof; auto.
+
+      constructor; try eassumption. econstructor; eauto.
+      eapply star_right; eauto.
+      eapply RTL.exec_Istore; eauto. auto.
+
+      unfold sem_extrap in *. intros.
+      eapply BB. econstructor; eauto.
+      econstructor; eauto.
+      rewrite <- eval_addressing_eq; eassumption.
+      constructor. auto.
+    }
+    { apply sim_plus.
+      inv H0. simplify.
+      unfold valid_succ in H6; simplify.
+      do 3 econstructor. apply plus_one. econstructor.
+      eassumption. eapply BB; [| eassumption ].
+      econstructor; econstructor; eauto.
+      rewrite <- eval_addressing_eq; eassumption.
+      constructor. econstructor. econstructor.
+      econstructor.
+
+      econstructor; try eassumption. eauto.
+      eapply star_refl.
+      unfold sem_extrap. intros. setoid_rewrite H0 in H6.
+      crush.
+    }
+  Qed.
+
+  Lemma functions_translated:
+    forall (v: Values.val) (f: RTL.fundef),
+      Genv.find_funct ge v = Some f ->
+      exists tf,
+        Genv.find_funct tge v = Some tf /\ transl_fundef f = Errors.OK tf.
+  Proof using TRANSL.
+    intros. exploit (Genv.find_funct_match TRANSL); eauto.
+    intros (cu & tf & P & Q & R); exists tf; auto.
+  Qed.
+
+  Lemma find_function_translated:
+    forall ros rs rs' f,
+      (forall x, rs !! x = rs' !! x) ->
+      RTL.find_function ge ros rs = Some f ->
+      exists tf, find_function tge ros rs' = Some tf
+                 /\ transl_fundef f = OK tf.
+  Proof using TRANSL.
+    Ltac ffts := match goal with
+                 | [ H: forall _, Val.lessdef _ _, r: Registers.reg |- _ ] =>
+                   specialize (H r); inv H
+                 | [ H: Vundef = ?r, H1: Genv.find_funct _ ?r = Some _ |- _ ] =>
+                   rewrite <- H in H1
+                 | [ H: Genv.find_funct _ Vundef = Some _ |- _] => solve [inv H]
+                 | _ => solve [exploit functions_translated; eauto]
+                 end.
+    destruct ros; simplify; try rewrite <- H;
+    [| rewrite symbols_preserved; destruct_match;
+      try (apply function_ptr_translated); crush ];
+    intros;
+    repeat ffts.
+  Qed.
+
+  Lemma transl_Icall_correct:
+    forall s f sp pc rs m sig ros args res pc' fd,
+      (RTL.fn_code f) ! pc = Some (RTL.Icall sig ros args res pc') ->
+      RTL.find_function ge ros rs = Some fd ->
+      RTL.funsig fd = sig ->
+      forall b s2, match_states b (RTL.State s f sp pc rs m) s2 ->
+        exists b' s2',
+          (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof _ measure b' b) /\
+            match_states b' (RTL.Callstate (RTL.Stackframe res f sp pc' rs :: s) fd rs ## args m) s2'.
+  Proof.
+    intros * H H0 H1.
+    inversion 1; subst; simplify.
+    unfold match_code in *.
+    match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify;
+    apply sim_plus.
+    inv H0. simplify.
+    unfold valid_succ in H5; simplify.
+    exploit find_function_translated; eauto; simplify.
+    do 3 econstructor. apply plus_one. econstructor.
+    eassumption. eapply BB; [| eassumption ].
+    econstructor; econstructor; eauto.
+    econstructor. econstructor.
+    econstructor; eauto.
+    apply sig_transl_function; auto.
+
+    econstructor; try eassumption.
+    constructor. constructor; auto.
+    unfold valid_succ; eauto. auto.
+  Qed.
+
+  Lemma transl_Itailcall_correct:
+    forall s f stk pc rs m sig ros args fd m',
+      (RTL.fn_code f) ! pc = Some (RTL.Itailcall sig ros args) ->
+      RTL.find_function ge ros rs = Some fd ->
+      RTL.funsig fd = sig ->
+      Mem.free m stk 0 (RTL.fn_stacksize f) = Some m' ->
+      forall b s2,
+        match_states b (RTL.State s f (Vptr stk Integers.Ptrofs.zero) pc rs m) s2 ->
+        exists b' s2',
+          (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b) /\
+            match_states b' (RTL.Callstate s fd rs ## args m') s2'.
+  Proof.
+    intros * H H0 H1 H2.
+    inversion 1; subst; simplify.
+    unfold match_code in *.
+    match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify;
+    apply sim_plus.
+    inv H0. simplify.
+    unfold valid_succ in H6; simplify.
+    exploit find_function_translated; eauto; simplify.
+    do 3 econstructor. apply plus_one. econstructor.
+    eassumption. eapply BB; [| eassumption ].
+    econstructor; econstructor; eauto.
+    econstructor. econstructor.
+    econstructor; eauto.
+    apply sig_transl_function; auto.
+    assert (fn_stacksize tf = RTL.fn_stacksize f).
+    { unfold transl_function in TF.
+      repeat (destruct_match; try discriminate; []).
+      inv TF; auto. }
+    rewrite H5. eassumption.
+
+    econstructor; try eassumption.
+  Qed.
+
+  Lemma transl_Ibuiltin_correct:
+    forall s f sp pc rs m ef args res pc' vargs t vres m',
+      (RTL.fn_code f) ! pc = Some (RTL.Ibuiltin ef args res pc') ->
+      eval_builtin_args ge (fun r : positive => rs # r) sp m args vargs ->
+      external_call ef ge vargs m t vres m' ->
+      forall b s2,
+        match_states b (RTL.State s f sp pc rs m) s2 ->
+        exists b' s2',
+          (plus step tge s2 t s2' \/ star step tge s2 t s2' /\ ltof _ measure b' b) /\
+            match_states b' (RTL.State s f sp pc' (regmap_setres res vres rs) m') s2'.
+  Proof.
+    intros * H H0 H1.
+    inversion 1; subst; simplify.
+    unfold match_code in *.
+    match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify.
+    eapply sim_plus.
+    unfold valid_succ in H6; simplify.
+    do 3 econstructor. apply plus_one. econstructor.
+    eassumption. eapply BB; [| eassumption ].
+    econstructor; econstructor; eauto.
+    econstructor. econstructor. econstructor; eauto.
+    eauto using eval_builtin_args_preserved, symbols_preserved.
+    eauto using external_call_symbols_preserved, senv_preserved.
+
+    econstructor; try eassumption. eauto.
+    eapply star_refl.
+    unfold sem_extrap. intros. setoid_rewrite H5 in H7. crush.
+  Qed.
+
+  Lemma init_regs_equiv :
+    forall b a, init_regs a b = RTL.init_regs a b.
+  Proof. induction b; crush. Qed.
+
+  Lemma transl_initcall_correct:
+    forall s f args m m' stk,
+      Mem.alloc m 0 (RTL.fn_stacksize f) = (m', stk) ->
+      forall b s2,
+        match_states b (RTL.Callstate s (Internal f) args m) s2 ->
+        exists b' s2',
+          (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b) /\
+            match_states b'
+                         (RTL.State s f (Vptr stk Integers.Ptrofs.zero) (RTL.fn_entrypoint f) (RTL.init_regs args (RTL.fn_params f)) m') s2'.
+  Proof.
+    intros * H.
+    inversion 1; subst; simplify.
+    monadInv TF. inv H0.
+    pose proof (transl_match_code _ _ EQ).
+    pose proof (transl_entrypoint_exists _ _ EQ). unfold valid_succ in H1.
+    simplify.
+    apply sim_plus. do 3 econstructor.
+    assert (fn_stacksize x = RTL.fn_stacksize f).
+    { unfold transl_function in EQ.
+      repeat (destruct_match; try discriminate; []).
+      inv EQ; auto. }
+    apply plus_one. econstructor; eauto.
+    rewrite H1. eauto.
+
+    assert (fn_entrypoint x = RTL.fn_entrypoint f).
+    { unfold transl_function in EQ.
+      repeat (destruct_match; try discriminate; []).
+      inv EQ; auto. }
+    assert (fn_params x = RTL.fn_params f).
+    { unfold transl_function in EQ.
+      repeat (destruct_match; try discriminate; []).
+      inv EQ; auto. }
+    unfold match_code in H0.
+    pose proof (H0 _ _ H2).
+    econstructor; eauto.
+    rewrite <- H1. eauto.
+    rewrite H1.
+    rewrite init_regs_equiv. rewrite H3. eapply star_refl.
+    unfold sem_extrap; intros.
+    setoid_rewrite H2 in H6; simplify.
+    rewrite H3. eauto.
+  Qed.
+
+  Lemma transl_externalcall_correct:
+    forall s ef args res t m m',
+      external_call ef ge args m t res m' ->
+      forall b s2,
+        match_states b (RTL.Callstate s (External ef) args m) s2 ->
+        exists b' s2',
+          (plus step tge s2 t s2' \/ star step tge s2 t s2' /\ ltof (option BB.t) measure b' b) /\
+            match_states b' (RTL.Returnstate s res m') s2'.
+  Proof.
+    intros * H.
+    inversion 1; subst; simplify.
+    inv TF.
+    apply sim_plus. do 3 econstructor.
+    apply plus_one.
+    econstructor; eauto using external_call_symbols_preserved, senv_preserved.
+    econstructor; eauto.
+  Qed.
+
+  Lemma transl_returnstate_correct:
+    forall res f sp pc rs s vres m b s2,
+      match_states b (RTL.Returnstate (RTL.Stackframe res f sp pc rs :: s) vres m) s2 ->
+      exists b' s2',
+        (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b) /\
+          match_states b' (RTL.State s f sp pc rs # res <- vres m) s2'.
+  Proof.
+    intros.
+    inv H. inv STK. inv H1.
+    pose proof (transl_match_code _ _ TF).
+    unfold valid_succ in VALID. simplify.
+    unfold match_code in H.
+    pose proof (H _ _ H0).
+    apply sim_plus. do 3 econstructor. apply plus_one.
+    constructor. constructor; eauto using star_refl.
+    unfold sem_extrap; intros.
+    setoid_rewrite H0 in H4; crush.
+  Qed.
+
+  Lemma transl_Icond_correct:
+    forall s f sp pc rs m cond args ifso ifnot b pc',
+      (RTL.fn_code f) ! pc = Some (RTL.Icond cond args ifso ifnot) ->
+      Op.eval_condition cond rs ## args m = Some b ->
+      pc' = (if b then ifso else ifnot) ->
+      forall b0 s2,
+        match_states b0 (RTL.State s f sp pc rs m) s2 ->
+        exists b' s2',
+          (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b0) /\
+            match_states b' (RTL.State s f sp pc' rs m) s2'.
+  Proof.
+    intros * H H0 H1.
+    inversion 1; subst; simplify.
+    unfold match_code in *.
+    match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify;
+    apply sim_plus.
+    inv H0. simplify.
+    unfold valid_succ in *; simplify.
+    destruct b.
+    { do 3 econstructor. apply plus_one.
+      econstructor; eauto. eapply BB. econstructor. econstructor.
+      econstructor. econstructor. econstructor. eauto.
+      econstructor; eauto.
+      constructor; eauto using star_refl.
+      unfold sem_extrap; intros. setoid_rewrite H4 in H6. inv H6. auto.
+    }
+    { do 3 econstructor. apply plus_one.
+      econstructor; eauto. eapply BB.
+      econstructor. econstructor.
+      econstructor. econstructor. econstructor. eauto.
+      econstructor; eauto.
+      constructor; eauto using star_refl.
+      unfold sem_extrap; intros. setoid_rewrite H0 in H6. inv H6. auto.
+    }
+  Qed.
+
+  Lemma transl_Ijumptable_correct:
+    forall s f sp pc rs m arg tbl n pc',
+      (RTL.fn_code f) ! pc = Some (RTL.Ijumptable arg tbl) ->
+      rs # arg = Vint n ->
+      list_nth_z tbl (Integers.Int.unsigned n) = Some pc' ->
+      forall b s2,
+        match_states b (RTL.State s f sp pc rs m) s2 ->
+        exists b' s2',
+          (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b) /\
+            match_states b' (RTL.State s f sp pc' rs m) s2'.
+  Proof.
+    intros * H H0 H1.
+    inversion 1; subst; simplify.
+    unfold match_code in *.
+    match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify;
+    apply sim_plus.
+    eapply Forall_forall with (x:=pc') in H6; eauto using list_nth_z_in.
+    unfold valid_succ in H6; simplify.
+    do 3 econstructor. apply plus_one.
+    econstructor; eauto. eapply BB.
+    econstructor. econstructor. econstructor. econstructor. econstructor.
+    eauto.
+    econstructor; eauto.
+
+    constructor; eauto using star_refl.
+    unfold sem_extrap; intros. setoid_rewrite H5 in H7. inv H7. auto.
+  Qed.
+
+  Lemma transl_Ireturn_correct:
+    forall s f stk pc rs m or m',
+      (RTL.fn_code f) ! pc = Some (RTL.Ireturn or) ->
+      Mem.free m stk 0 (RTL.fn_stacksize f) = Some m' ->
+      forall b s2,
+        match_states b (RTL.State s f (Vptr stk Integers.Ptrofs.zero) pc rs m) s2 ->
+        exists b' s2',
+          (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b) /\
+            match_states b' (RTL.Returnstate s (regmap_optget or Vundef rs) m') s2'.
+  Proof.
+    intros * H H0.
+    inversion 1; subst; simplify.
+    unfold match_code in *.
+    match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify;
+    apply sim_plus.
+    assert (fn_stacksize tf = RTL.fn_stacksize f).
+    { unfold transl_function in TF.
+      repeat (destruct_match; try discriminate; []).
+      inv TF; auto. }
+    do 3 econstructor. apply plus_one. econstructor; eauto.
+    eapply BB.
+    econstructor. econstructor. econstructor. econstructor.
+    econstructor. eauto.
+    econstructor; eauto.
+        rewrite H4. eauto.
+    constructor; eauto.
+  Qed.
+
+  Lemma transl_correct:
+    forall s1 t s1',
+      RTL.step ge s1 t s1' ->
+      forall b s2, match_states b s1 s2 ->
+        exists b' s2',
+          (plus step tge s2 t s2' \/
+             (star step tge s2 t s2' /\ ltof _ measure b' b))
+          /\ match_states b' s1' s2'.
+  Proof.
+    induction 1.
+    - eauto using transl_Inop_correct.
+    - eauto using transl_Iop_correct.
+    - eauto using transl_Iload_correct.
+    - eauto using transl_Istore_correct.
+    - eauto using transl_Icall_correct.
+    - eauto using transl_Itailcall_correct.
+    - eauto using transl_Ibuiltin_correct.
+    - eauto using transl_Icond_correct.
+    - eauto using transl_Ijumptable_correct.
+    - eauto using transl_Ireturn_correct.
+    - eauto using transl_initcall_correct.
+    - eauto using transl_externalcall_correct.
+    - eauto using transl_returnstate_correct.
+  Qed.
+
+  Theorem transf_program_correct:
+    forward_simulation (RTL.semantics prog) (GibleSeq.semantics tprog).
+  Proof using TRANSL.
+    eapply (Forward_simulation
+              (L1:=RTL.semantics prog)
+              (L2:=GibleSeq.semantics tprog)
+              (ltof _ measure) match_states).
+    constructor.
+    - apply well_founded_ltof.
+    - eauto using transl_initial_states.
+    - intros; eapply transl_final_states; eauto.
+    - eapply transl_correct.
+    - apply senv_preserved.
+  Qed.
+
+End CORRECTNESS.