(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(** Correctness proof for Cminor generation. *)

Require Import Coq.Program.Equality FSets Permutation.
Require Import FSets FSetAVL Orders Mergesort.
Require Import Coqlib Maps Ordered Errors Integers Floats.
Require Intv.
Require Import AST Linking.
Require Import Values Memory Events Globalenvs Smallstep.
Require Import Csharpminor Switch Cminor Cminorgen.

Local Open Scope error_monad_scope.

Definition match_prog (p: Csharpminor.program) (tp: Cminor.program) :=
  match_program (fun cu f tf => transl_fundef f = OK tf) eq p tp.

Lemma transf_program_match:
  forall p tp, transl_program p = OK tp -> match_prog p tp.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. apply match_transform_partial_program; auto.
Qed.

Section TRANSLATION.

Variable prog: Csharpminor.program.
Variable tprog: program.
Hypothesis TRANSL: match_prog prog tprog.
Let ge : Csharpminor.genv := Genv.globalenv prog.
Let tge: genv := Genv.globalenv tprog.

Lemma symbols_preserved:
  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof (Genv.find_symbol_transf_partial TRANSL).

Lemma senv_preserved:
  Senv.equiv ge tge.
Proof (Genv.senv_transf_partial TRANSL).

Lemma function_ptr_translated:
  forall (b: block) (f: Csharpminor.fundef),
  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 functions_translated:
  forall (v: val) (f: Csharpminor.fundef),
  Genv.find_funct ge v = Some f ->
  exists tf,
  Genv.find_funct tge v = Some tf /\ transl_fundef f = OK tf.
Proof (Genv.find_funct_transf_partial TRANSL).

Lemma sig_preserved_body:
  forall f tf cenv size,
  transl_funbody cenv size f = OK tf ->
  tf.(fn_sig) = Csharpminor.fn_sig f.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. unfold transl_funbody in H. monadInv H; reflexivity.
Qed.

Lemma sig_preserved:
  forall f tf,
  transl_fundef f = OK tf ->
  Cminor.funsig tf = Csharpminor.funsig f.
Proof.
(* Goal: forall (f : Csharpminor.fundef) (tf : fundef) (_ : @eq (res fundef) (transl_fundef f) (@OK fundef tf)), @eq signature (funsig tf) (Csharpminor.funsig f) *)
  intros until tf; destruct f; simpl.
(* Goal: forall _ : @eq (res fundef) (@bind function (AST.fundef function) (transl_function f) (fun f' : function => @OK (AST.fundef function) (@Internal function f'))) (@OK fundef tf), @eq signature (funsig tf) (Csharpminor.fn_sig f) *)
(* Goal: forall _ : @eq (res fundef) (@OK (AST.fundef function) (@External function e)) (@OK fundef tf), @eq signature (funsig tf) (ef_sig e) *)
  unfold transl_function. destruct (build_compilenv f).
(* Goal: forall _ : @eq (res fundef) (@bind function (AST.fundef function) (if zle z Ptrofs.max_unsigned then transl_funbody c z f else @Error function (msg (String (Ascii.Ascii true true false false false false true false) (String (Ascii.Ascii true false true true false true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false true true true false true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false true false false true true true false) (String (Ascii.Ascii true true true false false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false true true true false true true false) (String (Ascii.Ascii false true false true true true false false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii false false true false true true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true false true true false true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true true true false true true false) (String (Ascii.Ascii true false false true true true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii true true false false false true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii false true true false true true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true false false true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true false false false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii true true false false true true true false) (String (Ascii.Ascii false false true true false true false false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true false false true true true false) (String (Ascii.Ascii false false true false true true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii true true false false false true true false) (String (Ascii.Ascii true true false true false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true false false true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false true false true true true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false false true true true true false) (String (Ascii.Ascii true true false false false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true false false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true false false true true false) EmptyString)))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (fun f' : function => @OK (AST.fundef function) (@Internal function f'))) (@OK fundef tf), @eq signature (funsig tf) (Csharpminor.fn_sig f) *)
(* Goal: forall _ : @eq (res fundef) (@OK (AST.fundef function) (@External function e)) (@OK fundef tf), @eq signature (funsig tf) (ef_sig e) *)
  case (zle z Ptrofs.max_unsigned); simpl bind; try congruence.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. monadInv H. simpl. eapply sig_preserved_body; eauto.
(* Goal: forall _ : @eq (res fundef) (@OK (AST.fundef function) (@External function e)) (@OK fundef tf), @eq signature (funsig tf) (ef_sig e) *)
  intro. inv H. reflexivity.
Qed.

(** * Derived properties of memory operations *)

Lemma load_freelist:
  forall fbl chunk m b ofs m',
  (forall b' lo hi, In (b', lo, hi) fbl -> b' <> b) ->
  Mem.free_list m fbl = Some m' ->
  Mem.load chunk m' b ofs = Mem.load chunk m b ofs.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  induction fbl; intros.
  simpl in H0. congruence.
(* Goal: forall (_ : @eq (option Mem.mem) (let (p, hi) := a in let (b, lo) := p in match Mem.free m b lo hi with | Some m' => Mem.free_list m' fbl | None => @None Mem.mem end) (@Some Mem.mem m')) (_ : Mem.perm m' b ofs k p), Mem.perm m b ofs k p *)
  destruct a as [[b' lo] hi].
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  generalize H0. simpl. case_eq (Mem.free m b' lo hi); try congruence.
  intros m1 FR1 FRL.
  transitivity (Mem.load chunk m1 b ofs).
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  eapply IHfbl; eauto. intros. eapply H. eauto with coqlib.
  eapply Mem.load_free; eauto. left. apply not_eq_sym. eapply H. auto with coqlib.
Qed.

Lemma perm_freelist:
  forall fbl m m' b ofs k p,
  Mem.free_list m fbl = Some m' ->
  Mem.perm m' b ofs k p ->
  Mem.perm m b ofs k p.
Proof.
(* Goal: forall (fbl : list (prod (prod block Z) Z)) (m m' : Mem.mem) (b : block) (ofs : Z) (k : perm_kind) (p : permission) (_ : @eq (option Mem.mem) (Mem.free_list m fbl) (@Some Mem.mem m')) (_ : Mem.perm m' b ofs k p), Mem.perm m b ofs k p *)
  induction fbl; simpl; intros until p.
(* Goal: lbl_stmt_tail sl (@snd (list (prod Z nat)) nat (switch_table sl O)) (select_switch_default sl) *)
  congruence.
(* Goal: lbl_stmt_tail sl (@snd (list (prod Z nat)) nat (switch_table sl O)) (select_switch_default sl) *)
  destruct a as [[b' lo] hi]. case_eq (Mem.free m b' lo hi); try congruence.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. eauto with mem.
Qed.

Lemma nextblock_freelist:
  forall fbl m m',
  Mem.free_list m fbl = Some m' ->
  Mem.nextblock m' = Mem.nextblock m.
Proof.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  induction fbl; intros until m'; simpl.
(* Goal: lbl_stmt_tail sl (@snd (list (prod Z nat)) nat (switch_table sl O)) (select_switch_default sl) *)
  congruence.
(* Goal: forall _ : @eq (option Mem.mem) (let (p, hi) := a in let (b, lo) := p in match Mem.free m b lo hi with | Some m' => Mem.free_list m' fbl | None => @None Mem.mem end) (@Some Mem.mem m'), @eq block (Mem.nextblock m') (Mem.nextblock m) *)
  destruct a as [[b lo] hi].
(* Goal: lbl_stmt_tail sl (@snd (list (prod Z nat)) nat (switch_table sl O)) (select_switch_default sl) *)
  case_eq (Mem.free m b lo hi); intros; try congruence.
(* Goal: @eq block (Mem.nextblock m') (Mem.nextblock m) *)
  transitivity (Mem.nextblock m0). eauto. eapply Mem.nextblock_free; eauto.
Qed.

Lemma free_list_freeable:
  forall l m m',
  Mem.free_list m l = Some m' ->
  forall b lo hi,
  In (b, lo, hi) l -> Mem.range_perm m b lo hi Cur Freeable.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  induction l; simpl; intros.
(* Goal: @eq (option val) (@PTree.get val id e) (@Some val Vundef) *)
(* Goal: @eq (option val) (@PTree.get val id (@PTree.set val a Vundef (set_locals il e))) (@Some val Vundef) *)
  contradiction.
(* Goal: Mem.range_perm m b lo hi Cur Freeable *)
  revert H. destruct a as [[b' lo'] hi'].
(* Goal: lbl_stmt_tail sl (@snd (list (prod Z nat)) nat (switch_table sl O)) (select_switch_default sl) *)
  caseEq (Mem.free m b' lo' hi'); try congruence.
(* Goal: forall (m0 : Mem.mem) (_ : @eq (option Mem.mem) (Mem.free m b' lo' hi') (@Some Mem.mem m0)) (_ : @eq (option Mem.mem) (Mem.free_list m0 l) (@Some Mem.mem m')), Mem.range_perm m b lo hi Cur Freeable *)
  intros m1 FREE1 FREE2.
(* Goal: final_state R r *)
  destruct H0. inv H.
(* Goal: match_callstack f2 m2 m2' cs lo sp *)
  eauto with mem.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  red; intros. eapply Mem.perm_free_3; eauto. exploit IHl; eauto.
Qed.

Lemma nextblock_storev:
  forall chunk m addr v m',
  Mem.storev chunk m addr v = Some m' -> Mem.nextblock m' = Mem.nextblock m.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  unfold Mem.storev; intros. destruct addr; try discriminate.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply Mem.nextblock_store; eauto.
Qed.

(** * Correspondence between C#minor's and Cminor's environments and memory states *)

(** In C#minor, every variable is stored in a separate memory block.
  In the corresponding Cminor code, these variables become sub-blocks
  of the stack data block.  We capture these changes in memory via a
  memory injection [f]:
  [f b = Some(b', ofs)] means that C#minor block [b] corresponds
  to a sub-block of Cminor block [b] at offset [ofs].

  A memory injection [f] defines a relation [Val.inject f] between
  values and a relation [Mem.inject f] between memory states.  These
  relations will be used intensively in our proof of simulation
  between C#minor and Cminor executions. *)

(** ** Matching between Cshaprminor's temporaries and Cminor's variables *)

Definition match_temps (f: meminj) (le: Csharpminor.temp_env) (te: env) : Prop :=
  forall id v, le!id = Some v -> exists v', te!(id) = Some v' /\ Val.inject f v v'.

Lemma match_temps_invariant:
  forall f f' le te,
  match_temps f le te ->
  inject_incr f f' ->
  match_temps f' le te.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros; red; intros. destruct (H _ _ H1) as [v' [A B]]. exists v'; eauto.
Qed.

Lemma match_temps_assign:
  forall f le te id v tv,
  match_temps f le te ->
  Val.inject f v tv ->
  match_temps f (PTree.set id v le) (PTree.set id tv te).
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros; red; intros. rewrite PTree.gsspec in *. destruct (peq id0 id).
(* Goal: @eq val tv (Vptr b Ptrofs.zero) *)
  inv H1. exists tv; auto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eauto.
Qed.

(** ** Matching between C#minor's variable environment and Cminor's stack pointer *)

Inductive match_var (f: meminj) (sp: block): option (block * Z) -> option Z -> Prop :=
  | match_var_local: forall b sz ofs,
      Val.inject f (Vptr b Ptrofs.zero) (Vptr sp (Ptrofs.repr ofs)) ->
      match_var f sp (Some(b, sz)) (Some ofs)
  | match_var_global:
      match_var f sp None None.

(** Matching between a C#minor environment [e] and a Cminor
  stack pointer [sp]. The [lo] and [hi] parameters delimit the range
  of addresses for the blocks referenced from [te]. *)

Record match_env (f: meminj) (cenv: compilenv)
                 (e: Csharpminor.env) (sp: block)
                 (lo hi: block) : Prop :=
  mk_match_env {

(** C#minor local variables match sub-blocks of the Cminor stack data block. *)
    me_vars:
      forall id, match_var f sp (e!id) (cenv!id);

(** [lo, hi] is a proper interval. *)
    me_low_high:
      Ple lo hi;

(** Every block appearing in the C#minor environment [e] must be
  in the range [lo, hi]. *)
    me_bounded:
      forall id b sz, PTree.get id e = Some(b, sz) -> Ple lo b /\ Plt b hi;

(** All blocks mapped to sub-blocks of the Cminor stack data must be
    images of variables from the C#minor environment [e] *)
    me_inv:
      forall b delta,
      f b = Some(sp, delta) ->
      exists id, exists sz, PTree.get id e = Some(b, sz);

(** All C#minor blocks below [lo] (i.e. allocated before the blocks
  referenced from [e]) must map to blocks that are below [sp]
  (i.e. allocated before the stack data for the current Cminor function). *)
    me_incr:
      forall b tb delta,
      f b = Some(tb, delta) -> Plt b lo -> Plt tb sp
  }.

Ltac geninv x :=
  let H := fresh in (generalize x; intro H; inv H).

Lemma match_env_invariant:
  forall f1 cenv e sp lo hi f2,
  match_env f1 cenv e sp lo hi ->
  inject_incr f1 f2 ->
  (forall b delta, f2 b = Some(sp, delta) -> f1 b = Some(sp, delta)) ->
  (forall b, Plt b lo -> f2 b = f1 b) ->
  match_env f2 cenv e sp lo hi.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. destruct H. constructor; auto.
(* vars *)
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. geninv (me_vars0 id); econstructor; eauto.
(* bounded *)
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. eauto.
(* below *)
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. rewrite H2 in H; eauto.
Qed.

(** [match_env] and external calls *)

Remark inject_incr_separated_same:
  forall f1 f2 m1 m1',
  inject_incr f1 f2 -> inject_separated f1 f2 m1 m1' ->
  forall b, Mem.valid_block m1 b -> f2 b = f1 b.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. case_eq (f1 b).
(* Goal: forall (p : prod block Z) (_ : @eq (option (prod block Z)) (f1 b) (@Some (prod block Z) p)), @eq (option (prod block Z)) (f2 b) (@Some (prod block Z) p) *)
(* Goal: forall _ : @eq (option (prod block Z)) (f1 b) (@None (prod block Z)), @eq (option (prod block Z)) (f2 b) (@None (prod block Z)) *)
  intros [b' delta] EQ. apply H; auto.
(* Goal: forall _ : @eq (option (prod block Z)) (f1 b) (@None (prod block Z)), @eq (option (prod block Z)) (f2 b) (@None (prod block Z)) *)
  intros EQ. case_eq (f2 b).
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  intros [b'1 delta1] EQ1. exploit H0; eauto. intros [C D]. contradiction.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  auto.
Qed.

Remark inject_incr_separated_same':
  forall f1 f2 m1 m1',
  inject_incr f1 f2 -> inject_separated f1 f2 m1 m1' ->
  forall b b' delta,
  f2 b = Some(b', delta) -> Mem.valid_block m1' b' -> f1 b = Some(b', delta).
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. case_eq (f1 b).
(* Goal: lbl_stmt_tail sl (@snd (list (prod Z nat)) nat (switch_table sl O)) (select_switch_default sl) *)
  intros [b'1 delta1] EQ. exploit H; eauto. congruence.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. exploit H0; eauto. intros [C D]. contradiction.
Qed.

Lemma match_env_external_call:
  forall f1 cenv e sp lo hi f2 m1 m1',
  match_env f1 cenv e sp lo hi ->
  inject_incr f1 f2 ->
  inject_separated f1 f2 m1 m1' ->
  Ple hi (Mem.nextblock m1) -> Plt sp (Mem.nextblock m1') ->
  match_env f2 cenv e sp lo hi.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. apply match_env_invariant with f1; auto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. eapply inject_incr_separated_same'; eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. eapply inject_incr_separated_same; eauto. red. destruct H. xomega.
Qed.

(** [match_env] and allocations *)

Lemma match_env_alloc:
  forall f1 id cenv e sp lo m1 sz m2 b ofs f2,
  match_env f1 (PTree.remove id cenv) e sp lo (Mem.nextblock m1) ->
  Mem.alloc m1 0 sz = (m2, b) ->
  cenv!id = Some ofs ->
  inject_incr f1 f2 ->
  f2 b = Some(sp, ofs) ->
  (forall b', b' <> b -> f2 b' = f1 b') ->
  e!id = None ->
  match_env f2 cenv (PTree.set id (b, sz) e) sp lo (Mem.nextblock m2).
Proof.
  intros until f2; intros ME ALLOC CENV INCR SAME OTHER ENV.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit Mem.nextblock_alloc; eauto. intros NEXTBLOCK.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit Mem.alloc_result; eauto. intros RES.
  inv ME; constructor.
(* vars *)
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. rewrite PTree.gsspec. destruct (peq id0 id).
  (* the new var *)
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  subst id0. rewrite CENV. constructor. econstructor. eauto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  rewrite Ptrofs.add_commut; rewrite Ptrofs.add_zero; auto.
  (* old vars *)
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  generalize (me_vars0 id0). rewrite PTree.gro; auto. intros M; inv M.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  constructor; eauto.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
  constructor.
(* low-high *)
(* Goal: Ple (Mem.nextblock m) (Mem.nextblock m) *)
(* Goal: and (Ple (Mem.nextblock m) b) (Plt b (Mem.nextblock m)) *)
(* Goal: @ex positive (fun id : positive => @ex Z (fun sz : Z => @eq (option (prod block Z)) (@PTree.get (prod block Z) id empty_env) (@Some (prod block Z) (@pair block Z b sz)))) *)
(* Goal: Plt tb sp *)
(* Goal: match_bounds empty_env m *)
(* Goal: padding_freeable f empty_env tm' sp (fn_stackspace tf) *)
(* Goal: match_callstack f m tm' cs (Mem.nextblock m) sp *)
  rewrite NEXTBLOCK; xomega.
(* bounded *)
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. rewrite PTree.gsspec in H. destruct (peq id0 id).
(* Goal: final_state R r *)
  inv H. rewrite NEXTBLOCK; xomega.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit me_bounded0; eauto. rewrite NEXTBLOCK; xomega.
(* inv *)
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. destruct (eq_block b (Mem.nextblock m1)).
(* Goal: final_state R r *)
  subst b. rewrite SAME in H; inv H. exists id; exists sz. apply PTree.gss.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  rewrite OTHER in H; auto. exploit me_inv0; eauto.
(* Goal: lbl_stmt_tail sl (@snd (list (prod Z nat)) nat (switch_table sl O)) (select_switch_default sl) *)
  intros [id1 [sz1 EQ]]. exists id1; exists sz1. rewrite PTree.gso; auto. congruence.
(* incr *)
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. rewrite OTHER in H. eauto. unfold block in *; xomega.
Qed.

(** The sizes of blocks appearing in [e] are respected. *)

Definition match_bounds (e: Csharpminor.env) (m: mem) : Prop :=
  forall id b sz ofs p,
  PTree.get id e = Some(b, sz) -> Mem.perm m b ofs Max p -> 0 <= ofs < sz.

Lemma match_bounds_invariant:
  forall e m1 m2,
  match_bounds e m1 ->
  (forall id b sz ofs p,
   PTree.get id e = Some(b, sz) -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) ->
  match_bounds e m2.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros; red; intros. eapply H; eauto.
Qed.

(** ** Permissions on the Cminor stack block *)

(** The parts of the Cminor stack data block that are not images of
    C#minor local variable blocks remain freeable at all times. *)

Inductive is_reachable_from_env (f: meminj) (e: Csharpminor.env) (sp: block) (ofs: Z) : Prop :=
  | is_reachable_intro: forall id b sz delta,
      e!id = Some(b, sz) ->
      f b = Some(sp, delta) ->
      delta <= ofs < delta + sz ->
      is_reachable_from_env f e sp ofs.

Definition padding_freeable (f: meminj) (e: Csharpminor.env) (tm: mem) (sp: block) (sz: Z) : Prop :=
  forall ofs,
  0 <= ofs < sz -> Mem.perm tm sp ofs Cur Freeable \/ is_reachable_from_env f e sp ofs.

Lemma padding_freeable_invariant:
  forall f1 e tm1 sp sz cenv lo hi f2 tm2,
  padding_freeable f1 e tm1 sp sz ->
  match_env f1 cenv e sp lo hi ->
  (forall ofs, Mem.perm tm1 sp ofs Cur Freeable -> Mem.perm tm2 sp ofs Cur Freeable) ->
  (forall b, Plt b hi -> f2 b = f1 b) ->
  padding_freeable f2 e tm2 sp sz.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros; red; intros.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit H; eauto. intros [A | A].
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  left; auto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  right. inv A. exploit me_bounded; eauto. intros [D E].
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; eauto. rewrite H2; auto.
Qed.

(** Decidability of the [is_reachable_from_env] predicate. *)

Lemma is_reachable_from_env_dec:
  forall f e sp ofs, is_reachable_from_env f e sp ofs \/ ~is_reachable_from_env f e sp ofs.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros.
  set (pred := fun id_b_sz : ident * (block * Z) =>
                 match id_b_sz with
                 | (id, (b, sz)) =>
                      match f b with
                           | None => false
                           | Some(sp', delta) =>
                               if eq_block sp sp'
                               then zle delta ofs && zlt ofs (delta + sz)
                               else false
                      end
                 end).
(* Goal: or (is_reachable_from_env f e sp ofs) (not (is_reachable_from_env f e sp ofs)) *)
  destruct (List.existsb pred (PTree.elements e)) eqn:?.
  (* yes *)
(* Goal: or (is_reachable_from_env f e sp ofs) (not (is_reachable_from_env f e sp ofs)) *)
(* Goal: or (is_reachable_from_env f e sp ofs) (not (is_reachable_from_env f e sp ofs)) *)
  rewrite List.existsb_exists in Heqb.
(* Goal: or (is_reachable_from_env f e sp ofs) (not (is_reachable_from_env f e sp ofs)) *)
(* Goal: or (is_reachable_from_env f e sp ofs) (not (is_reachable_from_env f e sp ofs)) *)
  destruct Heqb as [[id [b sz]] [A B]].
(* Goal: or (is_reachable_from_env f e sp ofs) (not (is_reachable_from_env f e sp ofs)) *)
(* Goal: or (is_reachable_from_env f e sp ofs) (not (is_reachable_from_env f e sp ofs)) *)
  simpl in B. destruct (f b) as [[sp' delta] |] eqn:?; try discriminate.
(* Goal: or (is_reachable_from_env f e sp ofs) (not (is_reachable_from_env f e sp ofs)) *)
(* Goal: or (is_reachable_from_env f e sp ofs) (not (is_reachable_from_env f e sp ofs)) *)
  destruct (eq_block sp sp'); try discriminate.
(* Goal: or (is_reachable_from_env f e sp ofs) (not (is_reachable_from_env f e sp ofs)) *)
(* Goal: or (is_reachable_from_env f e sp ofs) (not (is_reachable_from_env f e sp ofs)) *)
  destruct (andb_prop _ _ B).
(* Goal: or (Z.le (Z.add ofs1 sz0) (align sz1 (block_alignment sz))) (Z.le (Z.add (align sz1 (block_alignment sz)) sz) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
  left. apply is_reachable_intro with id b sz delta.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  apply PTree.elements_complete; auto.
(* Goal: lbl_stmt_tail sl (@snd (list (prod Z nat)) nat (switch_table sl O)) (select_switch_default sl) *)
  congruence.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  split; eapply proj_sumbool_true; eauto.
  (* no *)
(* Goal: or (is_reachable_from_env f e sp ofs) (not (is_reachable_from_env f e sp ofs)) *)
  right; red; intro NE; inv NE.
(* Goal: False *)
  assert (existsb pred (PTree.elements e) = true).
(* Goal: @eq bool (@existsb (prod ident (prod block Z)) pred (@PTree.elements (prod block Z) e)) true *)
(* Goal: False *)
  rewrite List.existsb_exists. exists (id, (b, sz)); split.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  apply PTree.elements_correct; auto.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  simpl. rewrite H0. rewrite dec_eq_true.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  unfold proj_sumbool. destruct H1. rewrite zle_true; auto. rewrite zlt_true; auto.
(* Goal: lbl_stmt_tail sl (@snd (list (prod Z nat)) nat (switch_table sl O)) (select_switch_default sl) *)
  congruence.
Qed.

(** * Correspondence between global environments *)

(** Global environments match if the memory injection [f] leaves unchanged
  the references to global symbols and functions. *)

Inductive match_globalenvs (f: meminj) (bound: block): Prop :=
  | mk_match_globalenvs
      (DOMAIN: forall b, Plt b bound -> f b = Some(b, 0))
      (IMAGE: forall b1 b2 delta, f b1 = Some(b2, delta) -> Plt b2 bound -> b1 = b2)
      (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> Plt b bound)
      (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> Plt b bound)
      (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> Plt b bound).

Remark inj_preserves_globals:
  forall f hi,
  match_globalenvs f hi ->
  meminj_preserves_globals ge f.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. inv H.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  split. intros. apply DOMAIN. eapply SYMBOLS. eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  split. intros. apply DOMAIN. eapply VARINFOS. eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. symmetry. eapply IMAGE; eauto.
Qed.

(** * Invariant on abstract call stacks  *)

(** Call stacks represent abstractly the execution state of the current
  C#minor and Cminor functions, as well as the states of the
  calling functions.  A call stack is a list of frames, each frame
  collecting information on the current execution state of a C#minor
  function and its Cminor translation. *)

Inductive frame : Type :=
  Frame(cenv: compilenv)
       (tf: Cminor.function)
       (e: Csharpminor.env)
       (le: Csharpminor.temp_env)
       (te: Cminor.env)
       (sp: block)
       (lo hi: block).

Definition callstack : Type := list frame.

(** Matching of call stacks imply:
- matching of environments for each of the frames
- matching of the global environments
- separation conditions over the memory blocks allocated for C#minor local variables;
- separation conditions over the memory blocks allocated for Cminor stack data;
- freeable permissions on the parts of the Cminor stack data blocks
  that are not images of C#minor local variable blocks.
*)

Inductive match_callstack (f: meminj) (m: mem) (tm: mem):
                          callstack -> block -> block -> Prop :=
  | mcs_nil:
      forall hi bound tbound,
      match_globalenvs f hi ->
      Ple hi bound -> Ple hi tbound ->
      match_callstack f m tm nil bound tbound
  | mcs_cons:
      forall cenv tf e le te sp lo hi cs bound tbound
        (BOUND: Ple hi bound)
        (TBOUND: Plt sp tbound)
        (MTMP: match_temps f le te)
        (MENV: match_env f cenv e sp lo hi)
        (BOUND: match_bounds e m)
        (PERM: padding_freeable f e tm sp tf.(fn_stackspace))
        (MCS: match_callstack f m tm cs lo sp),
      match_callstack f m tm (Frame cenv tf e le te sp lo hi :: cs) bound tbound.

(** [match_callstack] implies [match_globalenvs]. *)

Lemma match_callstack_match_globalenvs:
  forall f m tm cs bound tbound,
  match_callstack f m tm cs bound tbound ->
  exists hi, match_globalenvs f hi.
Proof.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  induction 1; eauto.
Qed.

(** Invariance properties for [match_callstack]. *)

Lemma match_callstack_invariant:
  forall f1 m1 tm1 f2 m2 tm2 cs bound tbound,
  match_callstack f1 m1 tm1 cs bound tbound ->
  inject_incr f1 f2 ->
  (forall b ofs p, Plt b bound -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) ->
  (forall sp ofs, Plt sp tbound -> Mem.perm tm1 sp ofs Cur Freeable -> Mem.perm tm2 sp ofs Cur Freeable) ->
  (forall b, Plt b bound -> f2 b = f1 b) ->
  (forall b b' delta, f2 b = Some(b', delta) -> Plt b' tbound -> f1 b = Some(b', delta)) ->
  match_callstack f2 m2 tm2 cs bound tbound.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  induction 1; intros.
  (* base case *)
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; eauto.
(* Goal: final_state R r *)
  inv H. constructor; intros; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply IMAGE; eauto. eapply H6; eauto. xomega.
  (* inductive case *)
(* Goal: @eq (option (prod block Z)) (f2 b) (f1 b) *)
(* Goal: match_bounds e m2 *)
(* Goal: padding_freeable f2 e m2' sp (fn_stackspace tf) *)
(* Goal: match_callstack f2 m2 m2' cs lo sp *)
  assert (Ple lo hi) by (eapply me_low_high; eauto).
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply match_temps_invariant; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply match_env_invariant; eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
    intros. apply H3. xomega.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply match_bounds_invariant; eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
    intros. eapply H1; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
    exploit me_bounded; eauto. xomega.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply padding_freeable_invariant; eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
    intros. apply H3. xomega.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply IHmatch_callstack; eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
    intros. eapply H1; eauto. xomega.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
    intros. eapply H2; eauto. xomega.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
    intros. eapply H3; eauto. xomega.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
    intros. eapply H4; eauto. xomega.
Qed.

Lemma match_callstack_incr_bound:
  forall f m tm cs bound tbound bound' tbound',
  match_callstack f m tm cs bound tbound ->
  Ple bound bound' -> Ple tbound tbound' ->
  match_callstack f m tm cs bound' tbound'.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. inv H.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; eauto. xomega. xomega.
(* Goal: lbl_stmt_tail (LScons (@None Z) s sl) (S x) l *)
(* Goal: @eq nat (switch_target i dfl tbl1) (Init.Nat.add (S x) base) *)
(* Goal: @eq nat (switch_target i dfl tbl1) dfl *)
  constructor; auto. xomega. xomega.
Qed.

(** Assigning a temporary variable. *)

Lemma match_callstack_set_temp:
  forall f cenv e le te sp lo hi cs bound tbound m tm tf id v tv,
  Val.inject f v tv ->
  match_callstack f m tm (Frame cenv tf e le te sp lo hi :: cs) bound tbound ->
  match_callstack f m tm (Frame cenv tf e (PTree.set id v le) (PTree.set id tv te) sp lo hi :: cs) bound tbound.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. inv H0. constructor; auto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply match_temps_assign; eauto.
Qed.

(** Preservation of [match_callstack] by freeing all blocks allocated
  for local variables at function entry (on the C#minor side)
  and simultaneously freeing the Cminor stack data block. *)

Lemma in_blocks_of_env:
  forall e id b sz,
  e!id = Some(b, sz) -> In (b, 0, sz) (blocks_of_env e).
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  unfold blocks_of_env; intros.
(* Goal: @In (prod (prod block Z) Z) (@pair (prod block Z) Z (@pair block Z b Z0) sz) (@map (prod ident (prod block Z)) (prod (prod block Z) Z) block_of_binding (@PTree.elements (prod block Z) e)) *)
  change (b, 0, sz) with (block_of_binding (id, (b, sz))).
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  apply List.in_map. apply PTree.elements_correct. auto.
Qed.

Lemma in_blocks_of_env_inv:
  forall b lo hi e,
  In (b, lo, hi) (blocks_of_env e) ->
  exists id, e!id = Some(b, hi) /\ lo = 0.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  unfold blocks_of_env; intros.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit list_in_map_inv; eauto. intros [[id [b' sz]] [A B]].
(* Goal: @ex positive (fun id : positive => and (@eq (option (prod block Z)) (@PTree.get (prod block Z) id e) (@Some (prod block Z) (@pair block Z b hi))) (@eq Z lo Z0)) *)
  unfold block_of_binding in A. inv A.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  exists id; intuition. apply PTree.elements_complete. auto.
Qed.

Lemma match_callstack_freelist:
  forall f cenv tf e le te sp lo hi cs m m' tm,
  Mem.inject f m tm ->
  Mem.free_list m (blocks_of_env e) = Some m' ->
  match_callstack f m tm (Frame cenv tf e le te sp lo hi :: cs) (Mem.nextblock m) (Mem.nextblock tm) ->
  exists tm',
  Mem.free tm sp 0 tf.(fn_stackspace) = Some tm'
  /\ match_callstack f m' tm' cs (Mem.nextblock m') (Mem.nextblock tm')
  /\ Mem.inject f m' tm'.
Proof.
  intros until tm; intros INJ FREELIST MCS. inv MCS. inv MENV.
  assert ({tm' | Mem.free tm sp 0 (fn_stackspace tf) = Some tm'}).
  apply Mem.range_perm_free.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  red; intros.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit PERM; eauto. intros [A | A].
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  auto.
(* Goal: @ex positive (fun id : positive => and (@eq (option (prod block Z)) (@PTree.get (prod block Z) id e) (@Some (prod block Z) (@pair block Z b hi))) (@eq Z lo Z0)) *)
  inv A. assert (Mem.range_perm m b 0 sz Cur Freeable).
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply free_list_freeable; eauto. eapply in_blocks_of_env; eauto.
  replace ofs with ((ofs - delta) + delta) by omega.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply Mem.perm_inject; eauto. apply H3. omega.
  destruct X as  [tm' FREE].
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit nextblock_freelist; eauto. intro NEXT.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit Mem.nextblock_free; eauto. intro NEXT'.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  exists tm'. split. auto. split.
  rewrite NEXT; rewrite NEXT'.
(* Goal: @eq nat (switch_target i dfl tbl1) (Init.Nat.add (S x) base) *)
(* Goal: @eq nat (switch_target i dfl tbl1) dfl *)
  apply match_callstack_incr_bound with lo sp; try omega.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  apply match_callstack_invariant with f m tm; auto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. eapply perm_freelist; eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. eapply Mem.perm_free_1; eauto. left; unfold block; xomega. xomega. xomega.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply Mem.free_inject; eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. exploit me_inv0; eauto. intros [id [sz A]].
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  exists 0; exists sz; split.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply in_blocks_of_env; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply BOUND0; eauto. eapply Mem.perm_max. eauto.
Qed.

(** Preservation of [match_callstack] by external calls. *)

Lemma match_callstack_external_call:
  forall f1 f2 m1 m2 m1' m2',
  Mem.unchanged_on (loc_unmapped f1) m1 m2 ->
  Mem.unchanged_on (loc_out_of_reach f1 m1) m1' m2' ->
  inject_incr f1 f2 ->
  inject_separated f1 f2 m1 m1' ->
  (forall b ofs p, Mem.valid_block m1 b -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) ->
  forall cs bound tbound,
  match_callstack f1 m1 m1' cs bound tbound ->
  Ple bound (Mem.nextblock m1) -> Ple tbound (Mem.nextblock m1') ->
  match_callstack f2 m2 m2' cs bound tbound.
Proof.
(* Goal: forall (f1 f2 : Val.meminj) (m1 m2 m1' m2' : Mem.mem) (_ : Mem.unchanged_on (loc_unmapped f1) m1 m2) (_ : Mem.unchanged_on (loc_out_of_reach f1 m1) m1' m2') (_ : inject_incr f1 f2) (_ : inject_separated f1 f2 m1 m1') (_ : forall (b : block) (ofs : Z) (p : permission) (_ : Mem.valid_block m1 b) (_ : Mem.perm m2 b ofs Max p), Mem.perm m1 b ofs Max p) (cs : callstack) (bound tbound : block) (_ : match_callstack f1 m1 m1' cs bound tbound) (_ : Ple bound (Mem.nextblock m1)) (_ : Ple tbound (Mem.nextblock m1')), match_callstack f2 m2 m2' cs bound tbound *)
  intros until m2'.
(* Goal: forall (_ : Mem.unchanged_on (loc_unmapped f1) m1 m2) (_ : Mem.unchanged_on (loc_out_of_reach f1 m1) m1' m2') (_ : inject_incr f1 f2) (_ : inject_separated f1 f2 m1 m1') (_ : forall (b : block) (ofs : Z) (p : permission) (_ : Mem.valid_block m1 b) (_ : Mem.perm m2 b ofs Max p), Mem.perm m1 b ofs Max p) (cs : callstack) (bound tbound : block) (_ : match_callstack f1 m1 m1' cs bound tbound) (_ : Ple bound (Mem.nextblock m1)) (_ : Ple tbound (Mem.nextblock m1')), match_callstack f2 m2 m2' cs bound tbound *)
  intros UNMAPPED OUTOFREACH INCR SEPARATED MAXPERMS.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  induction 1; intros.
(* base case *)
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  apply mcs_nil with hi; auto.
(* Goal: final_state R r *)
  inv H. constructor; auto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. case_eq (f1 b1).
(* Goal: final_state R r *)
  intros [b2' delta'] EQ. rewrite (INCR _ _ _ EQ) in H. inv H. eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  intro EQ. exploit SEPARATED; eauto. intros [A B]. elim B. red. xomega.
(* inductive case *)
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  constructor. auto. auto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply match_temps_invariant; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply match_env_invariant; eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  red in SEPARATED. intros. destruct (f1 b) as [[b' delta']|] eqn:?.
(* Goal: lbl_stmt_tail sl (@snd (list (prod Z nat)) nat (switch_table sl O)) (select_switch_default sl) *)
  exploit INCR; eauto. congruence.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit SEPARATED; eauto. intros [A B]. elim B. red. xomega.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. assert (Ple lo hi) by (eapply me_low_high; eauto).
(* Goal: @eq (option (prod block Z)) (f2 b) (f1 b) *)
(* Goal: match_bounds e m2 *)
(* Goal: padding_freeable f2 e m2' sp (fn_stackspace tf) *)
(* Goal: match_callstack f2 m2 m2' cs lo sp *)
  destruct (f1 b) as [[b' delta']|] eqn:?.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  apply INCR; auto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  destruct (f2 b) as [[b' delta']|] eqn:?; auto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit SEPARATED; eauto. intros [A B]. elim A. red. xomega.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply match_bounds_invariant; eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. eapply MAXPERMS; eauto. red. exploit me_bounded; eauto. xomega.
  (* padding-freeable *)
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  red; intros.
(* Goal: or (Mem.perm m2' sp ofs Cur Freeable) (is_reachable_from_env f2 e sp ofs) *)
(* Goal: match_callstack f2 m2 m2' cs lo sp *)
  destruct (is_reachable_from_env_dec f1 e sp ofs).
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  inv H3. right. apply is_reachable_intro with id b sz delta; auto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit PERM; eauto. intros [A|A]; try contradiction.
(* Goal: or (Z.le (Z.add ofs1 sz0) (align sz1 (block_alignment sz))) (Z.le (Z.add (align sz1 (block_alignment sz)) sz) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
  left. eapply Mem.perm_unchanged_on; eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  red; intros; red; intros. elim H3.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit me_inv; eauto. intros [id [lv B]].
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit BOUND0; eauto. intros C.
(* Goal: @eq nat (switch_target i dfl tbl1) (Init.Nat.add (S x) base) *)
(* Goal: @eq nat (switch_target i dfl tbl1) dfl *)
  apply is_reachable_intro with id b0 lv delta; auto; omega.
(* Goal: match_callstack f2 m2 m2' cs lo sp *)
  eauto with mem.
  (* induction *)
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply IHmatch_callstack; eauto. inv MENV; xomega. xomega.
Qed.

(** [match_callstack] and allocations *)

Lemma match_callstack_alloc_right:
  forall f m tm cs tf tm' sp le te cenv,
  match_callstack f m tm cs (Mem.nextblock m) (Mem.nextblock tm) ->
  Mem.alloc tm 0 tf.(fn_stackspace) = (tm', sp) ->
  Mem.inject f m tm ->
  match_temps f le te ->
  (forall id, cenv!id = None) ->
  match_callstack f m tm'
      (Frame cenv tf empty_env le te sp (Mem.nextblock m) (Mem.nextblock m) :: cs)
      (Mem.nextblock m) (Mem.nextblock tm').
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit Mem.nextblock_alloc; eauto. intros NEXTBLOCK.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit Mem.alloc_result; eauto. intros RES.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
  constructor.
(* Goal: Ple (Mem.nextblock m) (Mem.nextblock m) *)
(* Goal: and (Ple (Mem.nextblock m) b) (Plt b (Mem.nextblock m)) *)
(* Goal: @ex positive (fun id : positive => @ex Z (fun sz : Z => @eq (option (prod block Z)) (@PTree.get (prod block Z) id empty_env) (@Some (prod block Z) (@pair block Z b sz)))) *)
(* Goal: Plt tb sp *)
(* Goal: match_bounds empty_env m *)
(* Goal: padding_freeable f empty_env tm' sp (fn_stackspace tf) *)
(* Goal: match_callstack f m tm' cs (Mem.nextblock m) sp *)
  xomega.
(* Goal: Ple (Mem.nextblock m) (Mem.nextblock m) *)
(* Goal: and (Ple (Mem.nextblock m) b) (Plt b (Mem.nextblock m)) *)
(* Goal: @ex positive (fun id : positive => @ex Z (fun sz : Z => @eq (option (prod block Z)) (@PTree.get (prod block Z) id empty_env) (@Some (prod block Z) (@pair block Z b sz)))) *)
(* Goal: Plt tb sp *)
(* Goal: match_bounds empty_env m *)
(* Goal: padding_freeable f empty_env tm' sp (fn_stackspace tf) *)
(* Goal: match_callstack f m tm' cs (Mem.nextblock m) sp *)
  unfold block in *; xomega.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  auto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  constructor; intros.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
    rewrite H3. rewrite PTree.gempty. constructor.
(* Goal: Ple (Mem.nextblock m) (Mem.nextblock m) *)
(* Goal: and (Ple (Mem.nextblock m) b) (Plt b (Mem.nextblock m)) *)
(* Goal: @ex positive (fun id : positive => @ex Z (fun sz : Z => @eq (option (prod block Z)) (@PTree.get (prod block Z) id empty_env) (@Some (prod block Z) (@pair block Z b sz)))) *)
(* Goal: Plt tb sp *)
(* Goal: match_bounds empty_env m *)
(* Goal: padding_freeable f empty_env tm' sp (fn_stackspace tf) *)
(* Goal: match_callstack f m tm' cs (Mem.nextblock m) sp *)
    xomega.
(* Goal: and (Ple (Mem.nextblock m) b) (Plt b (Mem.nextblock m)) *)
(* Goal: @ex positive (fun id : positive => @ex Z (fun sz : Z => @eq (option (prod block Z)) (@PTree.get (prod block Z) id empty_env) (@Some (prod block Z) (@pair block Z b sz)))) *)
(* Goal: Plt tb sp *)
(* Goal: match_bounds empty_env m *)
(* Goal: padding_freeable f empty_env tm' sp (fn_stackspace tf) *)
(* Goal: match_callstack f m tm' cs (Mem.nextblock m) sp *)
    rewrite PTree.gempty in H4; discriminate.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
    eelim Mem.fresh_block_alloc; eauto. eapply Mem.valid_block_inject_2; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
    rewrite RES. change (Mem.valid_block tm tb). eapply Mem.valid_block_inject_2; eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  red; intros. rewrite PTree.gempty in H4. discriminate.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  red; intros. left. eapply Mem.perm_alloc_2; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply match_callstack_invariant with (tm1 := tm); eauto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  rewrite RES; auto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. eapply Mem.perm_alloc_1; eauto.
Qed.

Lemma match_callstack_alloc_left:
  forall f1 m1 tm id cenv tf e le te sp lo cs sz m2 b f2 ofs,
  match_callstack f1 m1 tm
    (Frame (PTree.remove id cenv) tf e le te sp lo (Mem.nextblock m1) :: cs)
    (Mem.nextblock m1) (Mem.nextblock tm) ->
  Mem.alloc m1 0 sz = (m2, b) ->
  cenv!id = Some ofs ->
  inject_incr f1 f2 ->
  f2 b = Some(sp, ofs) ->
  (forall b', b' <> b -> f2 b' = f1 b') ->
  e!id = None ->
  match_callstack f2 m2 tm
    (Frame cenv tf (PTree.set id (b, sz) e) le te sp lo (Mem.nextblock m2) :: cs)
    (Mem.nextblock m2) (Mem.nextblock tm).
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. inv H.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit Mem.nextblock_alloc; eauto. intros NEXTBLOCK.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit Mem.alloc_result; eauto. intros RES.
  assert (LO: Ple lo (Mem.nextblock m1)) by (eapply me_low_high; eauto).
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
  constructor.
(* Goal: Ple (Mem.nextblock m) (Mem.nextblock m) *)
(* Goal: and (Ple (Mem.nextblock m) b) (Plt b (Mem.nextblock m)) *)
(* Goal: @ex positive (fun id : positive => @ex Z (fun sz : Z => @eq (option (prod block Z)) (@PTree.get (prod block Z) id empty_env) (@Some (prod block Z) (@pair block Z b sz)))) *)
(* Goal: Plt tb sp *)
(* Goal: match_bounds empty_env m *)
(* Goal: padding_freeable f empty_env tm' sp (fn_stackspace tf) *)
(* Goal: match_callstack f m tm' cs (Mem.nextblock m) sp *)
  xomega.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  auto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply match_temps_invariant; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply match_env_alloc; eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  red; intros. rewrite PTree.gsspec in H. destruct (peq id0 id).
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  inversion H. subst b0 sz0 id0. eapply Mem.perm_alloc_3; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply BOUND0; eauto. eapply Mem.perm_alloc_4; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit me_bounded; eauto. unfold block in *; xomega.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  red; intros. exploit PERM; eauto. intros [A|A]. auto. right.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  inv A. apply is_reachable_intro with id0 b0 sz0 delta; auto.
(* Goal: lbl_stmt_tail sl (@snd (list (prod Z nat)) nat (switch_table sl O)) (select_switch_default sl) *)
  rewrite PTree.gso. auto. congruence.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply match_callstack_invariant with (m1 := m1); eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. eapply Mem.perm_alloc_4; eauto.
(* Goal: Ple (Mem.nextblock m) (Mem.nextblock m) *)
(* Goal: and (Ple (Mem.nextblock m) b) (Plt b (Mem.nextblock m)) *)
(* Goal: @ex positive (fun id : positive => @ex Z (fun sz : Z => @eq (option (prod block Z)) (@PTree.get (prod block Z) id empty_env) (@Some (prod block Z) (@pair block Z b sz)))) *)
(* Goal: Plt tb sp *)
(* Goal: match_bounds empty_env m *)
(* Goal: padding_freeable f empty_env tm' sp (fn_stackspace tf) *)
(* Goal: match_callstack f m tm' cs (Mem.nextblock m) sp *)
  unfold block in *; xomega.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. apply H4. unfold block in *; xomega.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. destruct (eq_block b0 b).
(* Goal: final_state R r *)
  subst b0. rewrite H3 in H. inv H. xomegaContradiction.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  rewrite H4 in H; auto.
Qed.

(** * Correctness of stack allocation of local variables *)

(** This section shows the correctness of the translation of Csharpminor
  local variables as sub-blocks of the Cminor stack data.  This is the most difficult part of the proof. *)

Definition cenv_remove (cenv: compilenv) (vars: list (ident * Z)) : compilenv :=
  fold_right (fun id_lv ce => PTree.remove (fst id_lv) ce) cenv vars.

Remark cenv_remove_gso:
  forall id vars cenv,
  ~In id (map fst vars) ->
  PTree.get id (cenv_remove cenv vars) = PTree.get id cenv.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  induction vars; simpl; intros.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  auto.
(* Goal: @eq (option Z) (@PTree.get Z id (@PTree.remove Z (@fst positive Z a) (cenv_remove cenv vars))) (@PTree.get Z id cenv) *)
  rewrite PTree.gro. apply IHvars. intuition. intuition.
Qed.

Remark cenv_remove_gss:
  forall id vars cenv,
  In id (map fst vars) ->
  PTree.get id (cenv_remove cenv vars) = None.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  induction vars; simpl; intros.
(* Goal: @eq (option val) (@PTree.get val id e) (@Some val Vundef) *)
(* Goal: @eq (option val) (@PTree.get val id (@PTree.set val a Vundef (set_locals il e))) (@Some val Vundef) *)
  contradiction.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  rewrite PTree.grspec. destruct (PTree.elt_eq id (fst a)). auto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  destruct H. intuition. eauto.
Qed.

Definition cenv_compat (cenv: compilenv) (vars: list (ident * Z)) (tsz: Z) : Prop :=
  forall id sz,
  In (id, sz) vars ->
  exists ofs,
      PTree.get id cenv = Some ofs
   /\ Mem.inj_offset_aligned ofs sz
   /\ 0 <= ofs
   /\ ofs + Z.max 0 sz <= tsz.

Definition cenv_separated (cenv: compilenv) (vars: list (ident * Z)) : Prop :=
  forall id1 sz1 ofs1 id2 sz2 ofs2,
  In (id1, sz1) vars -> In (id2, sz2) vars ->
  PTree.get id1 cenv = Some ofs1 -> PTree.get id2 cenv = Some ofs2 ->
  id1 <> id2 ->
  ofs1 + sz1 <= ofs2 \/ ofs2 + sz2 <= ofs1.

Definition cenv_mem_separated (cenv: compilenv) (vars: list (ident * Z)) (f: meminj) (sp: block) (m: mem) : Prop :=
  forall id sz ofs b delta ofs' k p,
  In (id, sz) vars -> PTree.get id cenv = Some ofs ->
  f b = Some (sp, delta) ->
  Mem.perm m b ofs' k p ->
  ofs <= ofs' + delta < sz + ofs -> False.

Lemma match_callstack_alloc_variables_rec:
  forall tm sp tf cenv le te lo cs,
  Mem.valid_block tm sp ->
  fn_stackspace tf <= Ptrofs.max_unsigned ->
  (forall ofs k p, Mem.perm tm sp ofs k p -> 0 <= ofs < fn_stackspace tf) ->
  (forall ofs k p, 0 <= ofs < fn_stackspace tf -> Mem.perm tm sp ofs k p) ->
  forall e1 m1 vars e2 m2,
  alloc_variables e1 m1 vars e2 m2 ->
  forall f1,
  list_norepet (map fst vars) ->
  cenv_compat cenv vars (fn_stackspace tf) ->
  cenv_separated cenv vars ->
  cenv_mem_separated cenv vars f1 sp m1 ->
  (forall id sz, In (id, sz) vars -> e1!id = None) ->
  match_callstack f1 m1 tm
    (Frame (cenv_remove cenv vars) tf e1 le te sp lo (Mem.nextblock m1) :: cs)
    (Mem.nextblock m1) (Mem.nextblock tm) ->
  Mem.inject f1 m1 tm ->
  exists f2,
    match_callstack f2 m2 tm
      (Frame cenv tf e2 le te sp lo (Mem.nextblock m2) :: cs)
      (Mem.nextblock m2) (Mem.nextblock tm)
  /\ Mem.inject f2 m2 tm.
Proof.
  intros until cs; intros VALID REPRES STKSIZE STKPERMS.
  induction 1; intros f1 NOREPET COMPAT SEP1 SEP2 UNBOUND MCS MINJ.
  (* base case *)
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  simpl in MCS. exists f1; auto.
  (* inductive case *)
  simpl in NOREPET. inv NOREPET.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
(* exploit Mem.alloc_result; eauto. intros RES.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit Mem.nextblock_alloc; eauto. intros NB.*)
  exploit (COMPAT id sz). auto with coqlib. intros [ofs [CENV [ALIGNED [LOB HIB]]]].
  exploit Mem.alloc_left_mapped_inject.
    eexact MINJ.
    eexact H.
    eexact VALID.
(* Goal: @eq nat (switch_target i dfl tbl1) (Init.Nat.add (S x) base) *)
(* Goal: @eq nat (switch_target i dfl tbl1) dfl *)
    instantiate (1 := ofs). zify. omega.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
    intros. exploit STKSIZE; eauto. omega.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
    intros. apply STKPERMS. zify. omega.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
    replace (sz - 0) with sz by omega. auto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
    intros. eapply SEP2. eauto with coqlib. eexact CENV. eauto. eauto. omega.
  intros [f2 [A [B [C D]]]].
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit (IHalloc_variables f2); eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
    red; intros. eapply COMPAT. auto with coqlib.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
    red; intros. eapply SEP1; eauto with coqlib.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
    red; intros. exploit Mem.perm_alloc_inv; eauto. destruct (eq_block b b1); intros P.
    subst b. rewrite C in H5; inv H5.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
    exploit SEP1. eapply in_eq. eapply in_cons; eauto. eauto. eauto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
    red; intros; subst id0. elim H3. change id with (fst (id, sz0)). apply in_map; auto.
(* Goal: @eq nat (switch_target i dfl tbl1) (Init.Nat.add (S x) base) *)
(* Goal: @eq nat (switch_target i dfl tbl1) dfl *)
    omega.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
    eapply SEP2. apply in_cons; eauto. eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
    rewrite D in H5; eauto. eauto. auto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
    intros. rewrite PTree.gso. eapply UNBOUND; eauto with coqlib.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
    red; intros; subst id0. elim H3. change id with (fst (id, sz0)). apply in_map; auto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
    eapply match_callstack_alloc_left; eauto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
    rewrite cenv_remove_gso; auto.
    apply UNBOUND with sz; auto with coqlib.
Qed.

Lemma match_callstack_alloc_variables:
  forall tm1 sp tm2 m1 vars e m2 cenv f1 cs fn le te,
  Mem.alloc tm1 0 (fn_stackspace fn) = (tm2, sp) ->
  fn_stackspace fn <= Ptrofs.max_unsigned ->
  alloc_variables empty_env m1 vars e m2 ->
  list_norepet (map fst vars) ->
  cenv_compat cenv vars (fn_stackspace fn) ->
  cenv_separated cenv vars ->
  (forall id ofs, cenv!id = Some ofs -> In id (map fst vars)) ->
  Mem.inject f1 m1 tm1 ->
  match_callstack f1 m1 tm1 cs (Mem.nextblock m1) (Mem.nextblock tm1) ->
  match_temps f1 le te ->
  exists f2,
    match_callstack f2 m2 tm2 (Frame cenv fn e le te sp (Mem.nextblock m1) (Mem.nextblock m2) :: cs)
                    (Mem.nextblock m2) (Mem.nextblock tm2)
  /\ Mem.inject f2 m2 tm2.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply match_callstack_alloc_variables_rec; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply Mem.valid_new_block; eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. eapply Mem.perm_alloc_3; eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. apply Mem.perm_implies with Freeable; auto with mem. eapply Mem.perm_alloc_2; eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  instantiate (1 := f1). red; intros. eelim Mem.fresh_block_alloc; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply Mem.valid_block_inject_2; eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. apply PTree.gempty.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply match_callstack_alloc_right; eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. destruct (In_dec peq id (map fst vars)).
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  apply cenv_remove_gss; auto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  rewrite cenv_remove_gso; auto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  destruct (cenv!id) as [ofs|] eqn:?; auto. elim n; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply Mem.alloc_right_inject; eauto.
Qed.

(** Properties of the compilation environment produced by [build_compilenv] *)

Remark block_alignment_pos:
  forall sz, block_alignment sz > 0.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  unfold block_alignment; intros.
(* Goal: @eq nat (switch_target i dfl tbl1) (Init.Nat.add (S x) base) *)
(* Goal: @eq nat (switch_target i dfl tbl1) dfl *)
  destruct (zlt sz 2). omega.
(* Goal: @eq nat (switch_target i dfl tbl1) (Init.Nat.add (S x) base) *)
(* Goal: @eq nat (switch_target i dfl tbl1) dfl *)
  destruct (zlt sz 4). omega.
(* Goal: @eq nat (switch_target i dfl tbl1) (Init.Nat.add (S x) base) *)
(* Goal: @eq nat (switch_target i dfl tbl1) dfl *)
  destruct (zlt sz 8); omega.
Qed.

Remark assign_variable_incr:
  forall id sz cenv stksz cenv' stksz',
  assign_variable (cenv, stksz) (id, sz) = (cenv', stksz') -> stksz <= stksz'.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  simpl; intros. inv H.
(* Goal: Z.le stksz (Z.add (align stksz (block_alignment sz)) (Z.max Z0 sz)) *)
  generalize (align_le stksz (block_alignment sz) (block_alignment_pos sz)).
(* Goal: @eq nat (switch_target i dfl tbl1) (Init.Nat.add (S x) base) *)
(* Goal: @eq nat (switch_target i dfl tbl1) dfl *)
  assert (0 <= Z.max 0 sz). apply Zmax_bound_l. omega.
(* Goal: @eq nat (switch_target i dfl tbl1) (Init.Nat.add (S x) base) *)
(* Goal: @eq nat (switch_target i dfl tbl1) dfl *)
  omega.
Qed.

Remark assign_variables_incr:
  forall vars cenv sz cenv' sz',
  assign_variables (cenv, sz) vars = (cenv', sz') -> sz <= sz'.
Proof.
  induction vars; intros until sz'.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  simpl; intros. inv H. omega.
Opaque assign_variable.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  destruct a as [id s]. simpl. intros.
  destruct (assign_variable (cenv, sz) (id, s)) as [cenv1 sz1] eqn:?.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  apply Z.le_trans with sz1. eapply assign_variable_incr; eauto. eauto.
Transparent assign_variable.
Qed.

Remark inj_offset_aligned_block:
  forall stacksize sz,
  Mem.inj_offset_aligned (align stacksize (block_alignment sz)) sz.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros; red; intros.
(* Goal: Z.divide (align_chunk chunk) (align stacksize (block_alignment sz)) *)
  apply Zdivides_trans with (block_alignment sz).
(* Goal: Z.divide (align_chunk chunk) (block_alignment sz) *)
(* Goal: Z.divide (block_alignment sz) (align stacksize (block_alignment sz)) *)
  unfold align_chunk.  unfold block_alignment.
(* Goal: forall _ : @eq (res fundef) (@OK (AST.fundef function) (@External function e)) (@OK fundef tf), @eq signature (funsig tf) (ef_sig e) *)
  generalize Z.divide_1_l; intro.
(* Goal: forall _ : @eq (res fundef) (@OK (AST.fundef function) (@External function e)) (@OK fundef tf), @eq signature (funsig tf) (ef_sig e) *)
  generalize Z.divide_refl; intro.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  assert (2 | 4). exists 2; auto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  assert (2 | 8). exists 4; auto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  assert (4 | 8). exists 2; auto.
(* Goal: Z.divide match chunk with | Mint8signed => Zpos xH | Mint8unsigned => Zpos xH | Mint16signed => Zpos (xO xH) | Mint16unsigned => Zpos (xO xH) | Mint32 => Zpos (xO (xO xH)) | Mint64 => Zpos (xO (xO (xO xH))) | Mfloat32 => Zpos (xO (xO xH)) | Mfloat64 => Zpos (xO (xO xH)) | Many32 => Zpos (xO (xO xH)) | Many64 => Zpos (xO (xO xH)) end (if zlt sz (Zpos (xO xH)) then Zpos xH else if zlt sz (Zpos (xO (xO xH))) then Zpos (xO xH) else if zlt sz (Zpos (xO (xO (xO xH)))) then Zpos (xO (xO xH)) else Zpos (xO (xO (xO xH)))) *)
(* Goal: Z.divide (block_alignment sz) (align stacksize (block_alignment sz)) *)
  destruct (zlt sz 2).
(* Goal: Z.divide match chunk with | Mint8signed => Zpos xH | Mint8unsigned => Zpos xH | Mint16signed => Zpos (xO xH) | Mint16unsigned => Zpos (xO xH) | Mint32 => Zpos (xO (xO xH)) | Mint64 => Zpos (xO (xO (xO xH))) | Mfloat32 => Zpos (xO (xO xH)) | Mfloat64 => Zpos (xO (xO xH)) | Many32 => Zpos (xO (xO xH)) | Many64 => Zpos (xO (xO xH)) end (Zpos (xO (xO xH))) *)
(* Goal: Z.divide match chunk with | Mint8signed => Zpos xH | Mint8unsigned => Zpos xH | Mint16signed => Zpos (xO xH) | Mint16unsigned => Zpos (xO xH) | Mint32 => Zpos (xO (xO xH)) | Mint64 => Zpos (xO (xO (xO xH))) | Mfloat32 => Zpos (xO (xO xH)) | Mfloat64 => Zpos (xO (xO xH)) | Many32 => Zpos (xO (xO xH)) | Many64 => Zpos (xO (xO xH)) end (Zpos (xO (xO (xO xH)))) *)
(* Goal: Z.divide (block_alignment sz) (align stacksize (block_alignment sz)) *)
  destruct chunk; simpl in *; auto; omegaContradiction.
(* Goal: Z.divide match chunk with | Mint8signed => Zpos xH | Mint8unsigned => Zpos xH | Mint16signed => Zpos (xO xH) | Mint16unsigned => Zpos (xO xH) | Mint32 => Zpos (xO (xO xH)) | Mint64 => Zpos (xO (xO (xO xH))) | Mfloat32 => Zpos (xO (xO xH)) | Mfloat64 => Zpos (xO (xO xH)) | Many32 => Zpos (xO (xO xH)) | Many64 => Zpos (xO (xO xH)) end (if zlt sz (Zpos (xO (xO xH))) then Zpos (xO xH) else if zlt sz (Zpos (xO (xO (xO xH)))) then Zpos (xO (xO xH)) else Zpos (xO (xO (xO xH)))) *)
(* Goal: Z.divide (block_alignment sz) (align stacksize (block_alignment sz)) *)
  destruct (zlt sz 4).
(* Goal: Z.divide match chunk with | Mint8signed => Zpos xH | Mint8unsigned => Zpos xH | Mint16signed => Zpos (xO xH) | Mint16unsigned => Zpos (xO xH) | Mint32 => Zpos (xO (xO xH)) | Mint64 => Zpos (xO (xO (xO xH))) | Mfloat32 => Zpos (xO (xO xH)) | Mfloat64 => Zpos (xO (xO xH)) | Many32 => Zpos (xO (xO xH)) | Many64 => Zpos (xO (xO xH)) end (Zpos (xO (xO xH))) *)
(* Goal: Z.divide match chunk with | Mint8signed => Zpos xH | Mint8unsigned => Zpos xH | Mint16signed => Zpos (xO xH) | Mint16unsigned => Zpos (xO xH) | Mint32 => Zpos (xO (xO xH)) | Mint64 => Zpos (xO (xO (xO xH))) | Mfloat32 => Zpos (xO (xO xH)) | Mfloat64 => Zpos (xO (xO xH)) | Many32 => Zpos (xO (xO xH)) | Many64 => Zpos (xO (xO xH)) end (Zpos (xO (xO (xO xH)))) *)
(* Goal: Z.divide (block_alignment sz) (align stacksize (block_alignment sz)) *)
  destruct chunk; simpl in *; auto; omegaContradiction.
(* Goal: Z.divide match chunk with | Mint8signed => Zpos xH | Mint8unsigned => Zpos xH | Mint16signed => Zpos (xO xH) | Mint16unsigned => Zpos (xO xH) | Mint32 => Zpos (xO (xO xH)) | Mint64 => Zpos (xO (xO (xO xH))) | Mfloat32 => Zpos (xO (xO xH)) | Mfloat64 => Zpos (xO (xO xH)) | Many32 => Zpos (xO (xO xH)) | Many64 => Zpos (xO (xO xH)) end (if zlt sz (Zpos (xO (xO (xO xH)))) then Zpos (xO (xO xH)) else Zpos (xO (xO (xO xH)))) *)
(* Goal: Z.divide (block_alignment sz) (align stacksize (block_alignment sz)) *)
  destruct (zlt sz 8).
(* Goal: Z.divide match chunk with | Mint8signed => Zpos xH | Mint8unsigned => Zpos xH | Mint16signed => Zpos (xO xH) | Mint16unsigned => Zpos (xO xH) | Mint32 => Zpos (xO (xO xH)) | Mint64 => Zpos (xO (xO (xO xH))) | Mfloat32 => Zpos (xO (xO xH)) | Mfloat64 => Zpos (xO (xO xH)) | Many32 => Zpos (xO (xO xH)) | Many64 => Zpos (xO (xO xH)) end (Zpos (xO (xO xH))) *)
(* Goal: Z.divide match chunk with | Mint8signed => Zpos xH | Mint8unsigned => Zpos xH | Mint16signed => Zpos (xO xH) | Mint16unsigned => Zpos (xO xH) | Mint32 => Zpos (xO (xO xH)) | Mint64 => Zpos (xO (xO (xO xH))) | Mfloat32 => Zpos (xO (xO xH)) | Mfloat64 => Zpos (xO (xO xH)) | Many32 => Zpos (xO (xO xH)) | Many64 => Zpos (xO (xO xH)) end (Zpos (xO (xO (xO xH)))) *)
(* Goal: Z.divide (block_alignment sz) (align stacksize (block_alignment sz)) *)
  destruct chunk; simpl in *; auto; omegaContradiction.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  destruct chunk; simpl; auto.
(* Goal: Z.divide (block_alignment sz) (align stacksize (block_alignment sz)) *)
  apply align_divides. apply block_alignment_pos.
Qed.

Remark inj_offset_aligned_block':
  forall stacksize sz,
  Mem.inj_offset_aligned (align stacksize (block_alignment sz)) (Z.max 0 sz).
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros.
(* Goal: Mem.inj_offset_aligned (align stacksize (block_alignment sz)) (Z.max Z0 sz) *)
  replace (block_alignment sz) with (block_alignment (Z.max 0 sz)).
(* Goal: Mem.inj_offset_aligned (align sz1 (block_alignment sz)) sz *)
(* Goal: and (Z.le Z0 (align sz1 (block_alignment sz))) (Z.le (Z.add (align sz1 (block_alignment sz)) (Z.max Z0 sz)) (Z.add (align sz1 (block_alignment sz)) (Z.max Z0 sz))) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
  apply inj_offset_aligned_block.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  rewrite Zmax_spec. destruct (zlt sz 0); auto.
(* Goal: @eq val (Vptr b2 (Ptrofs.add Ptrofs.zero (Ptrofs.repr Z0))) (Vptr b2 Ptrofs.zero) *)
  transitivity 1. reflexivity. unfold block_alignment. rewrite zlt_true. auto. omega.
Qed.

Lemma assign_variable_sound:
  forall cenv1 sz1 id sz cenv2 sz2 vars,
  assign_variable (cenv1, sz1) (id, sz) = (cenv2, sz2) ->
  ~In id (map fst vars) ->
  0 <= sz1 ->
  cenv_compat cenv1 vars sz1 ->
  cenv_separated cenv1 vars ->
  cenv_compat cenv2 (vars ++ (id, sz) :: nil) sz2
  /\ cenv_separated cenv2 (vars ++ (id, sz) :: nil).
Proof.
(* Goal: forall (cenv1 : compilenv) (sz1 : Z) (id : ident) (sz : Z) (cenv2 : compilenv) (sz2 : Z) (vars : list (prod ident Z)) (_ : @eq (prod compilenv Z) (assign_variable (@pair compilenv Z cenv1 sz1) (@pair ident Z id sz)) (@pair compilenv Z cenv2 sz2)) (_ : not (@In ident id (@map (prod ident Z) ident (@fst ident Z) vars))) (_ : Z.le Z0 sz1) (_ : cenv_compat cenv1 vars sz1) (_ : cenv_separated cenv1 vars), and (cenv_compat cenv2 (@app (prod ident Z) vars (@cons (prod ident Z) (@pair ident Z id sz) (@nil (prod ident Z)))) sz2) (cenv_separated cenv2 (@app (prod ident Z) vars (@cons (prod ident Z) (@pair ident Z id sz) (@nil (prod ident Z))))) *)
  unfold assign_variable; intros until vars; intros ASV NOREPET POS COMPAT SEP.
(* Goal: and (cenv_compat cenv2 (@app (prod ident Z) vars (@cons (prod ident Z) (@pair ident Z id sz) (@nil (prod ident Z)))) sz2) (cenv_separated cenv2 (@app (prod ident Z) vars (@cons (prod ident Z) (@pair ident Z id sz) (@nil (prod ident Z))))) *)
  inv ASV.
(* Goal: Z.gt (block_alignment sz) Z0 *)
(* Goal: and (cenv_compat (@PTree.set Z id (align sz1 (block_alignment sz)) cenv1) (@app (prod ident Z) vars (@cons (prod ident Z) (@pair ident Z id sz) (@nil (prod ident Z)))) (Z.add (align sz1 (block_alignment sz)) (Z.max Z0 sz))) (cenv_separated (@PTree.set Z id (align sz1 (block_alignment sz)) cenv1) (@app (prod ident Z) vars (@cons (prod ident Z) (@pair ident Z id sz) (@nil (prod ident Z))))) *)
  assert (LE: sz1 <= align sz1 (block_alignment sz)). apply align_le. apply block_alignment_pos.
  assert (EITHER: forall id' sz',
             In (id', sz') (vars ++ (id, sz) :: nil) ->
             In (id', sz') vars /\ id' <> id \/ (id', sz') = (id, sz)).
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
    intros. rewrite in_app in H. destruct H.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
    left; split; auto. red; intros; subst id'. elim NOREPET.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
    change id with (fst (id, sz')). apply in_map; auto.
(* Goal: @eq (option val) (@PTree.get val id e) (@Some val Vundef) *)
(* Goal: @eq (option val) (@PTree.get val id (@PTree.set val a Vundef (set_locals il e))) (@Some val Vundef) *)
    simpl in H. destruct H. auto. contradiction.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  split; red; intros.
(* Goal: @ex Z (fun ofs : Z => and (@eq (option Z) (@PTree.get Z id0 (@PTree.set Z id (align sz1 (block_alignment sz)) cenv1)) (@Some Z ofs)) (and (Mem.inj_offset_aligned ofs sz0) (and (Z.le Z0 ofs) (Z.le (Z.add ofs (Z.max Z0 sz0)) (Z.add (align sz1 (block_alignment sz)) (Z.max Z0 sz)))))) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
  apply EITHER in H. destruct H as [[P Q] | P].
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit COMPAT; eauto. intros [ofs [A [B [C D]]]].
(* Goal: @ex Z (fun ofs : Z => and (@eq (option Z) (@PTree.get Z id0 (@PTree.set Z id (align sz1 (block_alignment sz)) cenv1)) (@Some Z ofs)) (and (Mem.inj_offset_aligned ofs sz0) (and (Z.le Z0 ofs) (Z.le (Z.add ofs (Z.max Z0 sz0)) (Z.add (align sz1 (block_alignment sz)) (Z.max Z0 sz)))))) *)
(* Goal: @ex Z (fun ofs : Z => and (@eq (option Z) (@PTree.get Z id0 (@PTree.set Z id (align sz1 (block_alignment sz)) cenv1)) (@Some Z ofs)) (and (Mem.inj_offset_aligned ofs sz0) (and (Z.le Z0 ofs) (Z.le (Z.add ofs (Z.max Z0 sz0)) (Z.add (align sz1 (block_alignment sz)) (Z.max Z0 sz)))))) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
  exists ofs.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  split. rewrite PTree.gso; auto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  split. auto. split. auto. zify; omega.
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
  inv P. exists (align sz1 (block_alignment sz)).
(* Goal: @eq (option val) (@PTree.get val id (@PTree.set val id Vundef (set_locals il e))) (@Some val Vundef) *)
(* Goal: @eq (option val) (@PTree.get val id (@PTree.set val a Vundef (set_locals il e))) (@Some val Vundef) *)
  split. apply PTree.gss.
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  split. apply inj_offset_aligned_block.
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  split. omega.
(* Goal: @eq nat (switch_target i dfl tbl1) (Init.Nat.add (S x) base) *)
(* Goal: @eq nat (switch_target i dfl tbl1) dfl *)
  omega.
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
  apply EITHER in H; apply EITHER in H0.
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
  destruct H as [[P Q] | P]; destruct H0 as [[R S] | R].
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  rewrite PTree.gso in *; auto. eapply SEP; eauto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  inv R. rewrite PTree.gso in H1; auto. rewrite PTree.gss in H2; inv H2.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit COMPAT; eauto. intros [ofs [A [B [C D]]]].
(* Goal: lbl_stmt_tail sl (@snd (list (prod Z nat)) nat (switch_table sl O)) (select_switch_default sl) *)
  assert (ofs = ofs1) by congruence. subst ofs.
(* Goal: or (Z.le (Z.add ofs1 sz0) (align sz1 (block_alignment sz))) (Z.le (Z.add (align sz1 (block_alignment sz)) sz) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
  left. zify; omega.
(* Goal: @eq val tv (Vptr b Ptrofs.zero) *)
  inv P. rewrite PTree.gso in H2; auto. rewrite PTree.gss in H1; inv H1.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit COMPAT; eauto. intros [ofs [A [B [C D]]]].
(* Goal: lbl_stmt_tail sl (@snd (list (prod Z nat)) nat (switch_table sl O)) (select_switch_default sl) *)
  assert (ofs = ofs2) by congruence. subst ofs.
(* Goal: or (Z.le (Z.add (align sz1 (block_alignment sz)) sz) ofs2) (Z.le (Z.add ofs2 sz2) (align sz1 (block_alignment sz))) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
  right. zify; omega.
(* Goal: lbl_stmt_tail sl (@snd (list (prod Z nat)) nat (switch_table sl O)) (select_switch_default sl) *)
  congruence.
Qed.

Lemma assign_variables_sound:
  forall vars' cenv1 sz1 cenv2 sz2 vars,
  assign_variables (cenv1, sz1) vars' = (cenv2, sz2) ->
  list_norepet (map fst vars' ++ map fst vars) ->
  0 <= sz1 ->
  cenv_compat cenv1 vars sz1 ->
  cenv_separated cenv1 vars ->
  cenv_compat cenv2 (vars ++ vars') sz2 /\ cenv_separated cenv2 (vars ++ vars').
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  induction vars'; simpl; intros.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  rewrite app_nil_r. inv H; auto.
  destruct a as [id sz].
  simpl in H0. inv H0. rewrite in_app in H6.
  rewrite list_norepet_app in H7. destruct H7 as [P [Q R]].
  destruct (assign_variable (cenv1, sz1) (id, sz)) as [cenv' sz'] eqn:?.
  exploit assign_variable_sound.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
    eauto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
    instantiate (1 := vars). tauto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
    auto. auto. auto.
(* Goal: forall _ : and (not (Mem.valid_block m1 b)) (not (Mem.valid_block m1' b')), @eq (option (prod block Z)) (@Some (prod block Z) (@pair block Z b' delta')) (@None (prod block Z)) *)
(* Goal: match_bounds e m2 *)
(* Goal: padding_freeable f2 e m2' sp (fn_stackspace tf) *)
(* Goal: match_callstack f2 m2 m2' cs lo sp *)
  intros [A B].
  exploit IHvars'.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
    eauto.
    instantiate (1 := vars ++ ((id, sz) :: nil)).
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
    rewrite list_norepet_app. split. auto.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
    split. rewrite map_app. apply list_norepet_append_commut. simpl. constructor; auto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
    rewrite map_app. simpl. red; intros. rewrite in_app in H4. destruct H4.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
    eauto. simpl in H4. destruct H4. subst y. red; intros; subst x. tauto. tauto.
(* Goal: @eq nat (switch_target i dfl tbl1) (Init.Nat.add (S x) base) *)
(* Goal: @eq nat (switch_target i dfl tbl1) dfl *)
    generalize (assign_variable_incr _ _ _ _ _ _ Heqp). omega.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
    auto. auto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  rewrite app_ass. auto.
Qed.

Remark permutation_norepet:
  forall (A: Type) (l l': list A), Permutation l l' -> list_norepet l -> list_norepet l'.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  induction 1; intros.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
  constructor.
(* Goal: lbl_stmt_tail (LScons (@None Z) s sl) (S x) l *)
(* Goal: @eq nat (switch_target i dfl tbl1) (Init.Nat.add (S x) base) *)
(* Goal: @eq nat (switch_target i dfl tbl1) dfl *)
  inv H0. constructor; auto. red; intros; elim H3. apply Permutation_in with l'; auto. apply Permutation_sym; auto.
(* Goal: final_state R r *)
  inv H. simpl in H2. inv H3. constructor. simpl; intuition. constructor. intuition. auto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eauto.
Qed.

Lemma build_compilenv_sound:
  forall f cenv sz,
  build_compilenv f = (cenv, sz) ->
  list_norepet (map fst (Csharpminor.fn_vars f)) ->
  cenv_compat cenv (Csharpminor.fn_vars f) sz /\ cenv_separated cenv (Csharpminor.fn_vars f).
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  unfold build_compilenv; intros.
(* Goal: @In positive id (@map (prod ident Z) ident (@fst ident Z) (Csharpminor.fn_vars f)) *)
  set (vars1 := Csharpminor.fn_vars f) in *.
(* Goal: @In positive id (@map (prod ident Z) ident (@fst ident Z) vars1) *)
  generalize (VarSort.Permuted_sort vars1). intros P.
(* Goal: @In positive id (@map (prod ident Z) ident (@fst ident Z) vars1) *)
  set (vars2 := VarSort.sort vars1) in *.
  assert (cenv_compat cenv vars2 sz /\ cenv_separated cenv vars2).
    change vars2 with (nil ++ vars2).
    eapply assign_variables_sound.
    eexact H.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
    simpl. rewrite app_nil_r. apply permutation_norepet with (map fst vars1); auto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
    apply Permutation_map. auto.
(* Goal: @eq nat (switch_target i dfl tbl1) (Init.Nat.add (S x) base) *)
(* Goal: @eq nat (switch_target i dfl tbl1) dfl *)
    omega.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
    red; intros. contradiction.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
    red; intros. contradiction.
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  destruct H1 as [A B]. split.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  red; intros. apply A. apply Permutation_in with vars1; auto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  red; intros. eapply B; eauto; apply Permutation_in with vars1; auto.
Qed.

Lemma assign_variables_domain:
  forall id vars cesz,
  (fst (assign_variables cesz vars))!id <> None ->
  (fst cesz)!id <> None \/ In id (map fst vars).
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  induction vars; simpl; intros.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  auto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit IHvars; eauto. unfold assign_variable. destruct a as [id1 sz1].
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  destruct cesz as [cenv stksz]. simpl.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  rewrite PTree.gsspec. destruct (peq id id1). auto. tauto.
Qed.

Lemma build_compilenv_domain:
  forall f cenv sz id ofs,
  build_compilenv f = (cenv, sz) ->
  cenv!id = Some ofs -> In id (map fst (Csharpminor.fn_vars f)).
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  unfold build_compilenv; intros.
(* Goal: @In positive id (@map (prod ident Z) ident (@fst ident Z) (Csharpminor.fn_vars f)) *)
  set (vars1 := Csharpminor.fn_vars f) in *.
(* Goal: @In positive id (@map (prod ident Z) ident (@fst ident Z) vars1) *)
  generalize (VarSort.Permuted_sort vars1). intros P.
(* Goal: @In positive id (@map (prod ident Z) ident (@fst ident Z) vars1) *)
  set (vars2 := VarSort.sort vars1) in *.
(* Goal: @In positive id (@map (prod ident Z) ident (@fst ident Z) vars1) *)
  generalize (assign_variables_domain id vars2 (PTree.empty Z, 0)).
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  rewrite H. simpl. intros. destruct H1. congruence.
(* Goal: lbl_stmt_tail sl (@snd (list (prod Z nat)) nat (switch_table sl O)) (select_switch_default sl) *)
  rewrite PTree.gempty in H1. congruence.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  apply Permutation_in with (map fst vars2); auto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  apply Permutation_map. apply Permutation_sym; auto.
Qed.

(** Initialization of C#minor temporaries and Cminor local variables. *)

Lemma create_undef_temps_val:
  forall id v temps, (create_undef_temps temps)!id = Some v -> In id temps /\ v = Vundef.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  induction temps; simpl; intros.
(* Goal: lbl_stmt_tail sl (@snd (list (prod Z nat)) nat (switch_table sl O)) (select_switch_default sl) *)
  rewrite PTree.gempty in H. congruence.
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  rewrite PTree.gsspec in H. destruct (peq id a).
(* Goal: lbl_stmt_tail sl (@snd (list (prod Z nat)) nat (switch_table sl O)) (select_switch_default sl) *)
  split. auto. congruence.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit IHtemps; eauto. tauto.
Qed.

Fixpoint set_params' (vl: list val) (il: list ident) (te: Cminor.env) : Cminor.env :=
  match il, vl with
  | i1 :: is, v1 :: vs => set_params' vs is (PTree.set i1 v1 te)
  | i1 :: is, nil => set_params' nil is (PTree.set i1 Vundef te)
  | _, _ => te
  end.

Lemma bind_parameters_agree_rec:
  forall f vars vals tvals le1 le2 te,
  bind_parameters vars vals le1 = Some le2 ->
  Val.inject_list f vals tvals ->
  match_temps f le1 te ->
  match_temps f le2 (set_params' tvals vars te).
Proof.
Opaque PTree.set.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  induction vars; simpl; intros.
(* Goal: final_state R r *)
  destruct vals; try discriminate. inv H. auto.
(* Goal: final_state R r *)
  destruct vals; try discriminate. inv H0.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  simpl. eapply IHvars; eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  red; intros. rewrite PTree.gsspec in *. destruct (peq id a).
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  inv H0. exists v'; auto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  apply H1; auto.
Qed.

Lemma set_params'_outside:
  forall id il vl te, ~In id il -> (set_params' vl il te)!id = te!id.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  induction il; simpl; intros. auto.
(* Goal: @eq (option val) (@PTree.get val id match vl with | nil => set_params' (@nil val) il (@PTree.set val a Vundef te) | cons v1 vs => set_params' vs il (@PTree.set val a v1 te) end) (@PTree.get val id te) *)
  destruct vl; rewrite IHil.
(* Goal: not (@eq positive id a) *)
  apply PTree.gso. intuition. intuition.
(* Goal: not (@eq positive id a) *)
  apply PTree.gso. intuition. intuition.
Qed.

Lemma set_params'_inside:
  forall id il vl te1 te2,
  In id il ->
  (set_params' vl il te1)!id = (set_params' vl il te2)!id.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  induction il; simpl; intros.
(* Goal: @eq (option val) (@PTree.get val id e) (@Some val Vundef) *)
(* Goal: @eq (option val) (@PTree.get val id (@PTree.set val a Vundef (set_locals il e))) (@Some val Vundef) *)
  contradiction.
  destruct vl; destruct (List.in_dec peq id il); auto;
  repeat rewrite set_params'_outside; auto;
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  assert (a = id) by intuition; subst a; repeat rewrite PTree.gss; auto.
Qed.

Lemma set_params_set_params':
  forall il vl id,
  list_norepet il ->
  (set_params vl il)!id = (set_params' vl il (PTree.empty val))!id.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  induction il; simpl; intros.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  auto.
(* Goal: final_state R r *)
  inv H. destruct vl.
(* Goal: @eq (option val) (@PTree.get val id (@PTree.set val a Vundef (set_locals il e))) (@Some val Vundef) *)
  rewrite PTree.gsspec. destruct (peq id a).
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  subst a. rewrite set_params'_outside; auto. rewrite PTree.gss; auto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  rewrite IHil; auto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  destruct (List.in_dec peq id il). apply set_params'_inside; auto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  repeat rewrite set_params'_outside; auto. rewrite PTree.gso; auto.
(* Goal: @eq (option val) (@PTree.get val id (@PTree.set val a Vundef (set_locals il e))) (@Some val Vundef) *)
  rewrite PTree.gsspec. destruct (peq id a).
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  subst a. rewrite set_params'_outside; auto. rewrite PTree.gss; auto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  rewrite IHil; auto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  destruct (List.in_dec peq id il). apply set_params'_inside; auto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  repeat rewrite set_params'_outside; auto. rewrite PTree.gso; auto.
Qed.

Lemma set_locals_outside:
  forall e id il,
  ~In id il -> (set_locals il e)!id = e!id.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  induction il; simpl; intros.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  auto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  rewrite PTree.gso. apply IHil. tauto. intuition.
Qed.

Lemma set_locals_inside:
  forall e id il,
  In id il -> (set_locals il e)!id = Some Vundef.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  induction il; simpl; intros.
(* Goal: @eq (option val) (@PTree.get val id e) (@Some val Vundef) *)
(* Goal: @eq (option val) (@PTree.get val id (@PTree.set val a Vundef (set_locals il e))) (@Some val Vundef) *)
  contradiction.
(* Goal: @eq (option val) (@PTree.get val id (@PTree.set val a Vundef (set_locals il e))) (@Some val Vundef) *)
  destruct H. subst a. apply PTree.gss.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  rewrite PTree.gsspec. destruct (peq id a). auto. auto.
Qed.

Lemma set_locals_set_params':
  forall vars vals params id,
  list_norepet params ->
  list_disjoint params vars ->
  (set_locals vars (set_params vals params)) ! id =
  (set_params' vals params (set_locals vars (PTree.empty val))) ! id.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. destruct (in_dec peq id vars).
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  assert (~In id params). apply list_disjoint_notin with vars; auto. apply list_disjoint_sym; auto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  rewrite set_locals_inside; auto. rewrite set_params'_outside; auto. rewrite set_locals_inside; auto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  rewrite set_locals_outside; auto. rewrite set_params_set_params'; auto.
(* Goal: @eq (option val) (@PTree.get val id (set_params' vals params (PTree.empty val))) (@PTree.get val id (set_params' vals params (set_locals vars (PTree.empty val)))) *)
  destruct (in_dec peq id params).
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  apply set_params'_inside; auto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  repeat rewrite set_params'_outside; auto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  rewrite set_locals_outside; auto.
Qed.

Lemma bind_parameters_agree:
  forall f params temps vals tvals le,
  bind_parameters params vals (create_undef_temps temps) = Some le ->
  Val.inject_list f vals tvals ->
  list_norepet params ->
  list_disjoint params temps ->
  match_temps f le (set_locals temps (set_params tvals params)).
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros; red; intros.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit bind_parameters_agree_rec; eauto.
  instantiate (1 := set_locals temps (PTree.empty val)).
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  red; intros. exploit create_undef_temps_val; eauto. intros [A B]. subst v0.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  exists Vundef; split. apply set_locals_inside; auto. auto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  intros [v' [A B]]. exists v'; split; auto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  rewrite <- A. apply set_locals_set_params'; auto.
Qed.

(** The main result in this section. *)

Theorem match_callstack_function_entry:
  forall fn cenv tf m e m' tm tm' sp f cs args targs le,
  build_compilenv fn = (cenv, tf.(fn_stackspace)) ->
  tf.(fn_stackspace) <= Ptrofs.max_unsigned ->
  list_norepet (map fst (Csharpminor.fn_vars fn)) ->
  list_norepet (Csharpminor.fn_params fn) ->
  list_disjoint (Csharpminor.fn_params fn) (Csharpminor.fn_temps fn) ->
  alloc_variables Csharpminor.empty_env m (Csharpminor.fn_vars fn) e m' ->
  bind_parameters (Csharpminor.fn_params fn) args (create_undef_temps fn.(fn_temps)) = Some le ->
  Val.inject_list f args targs ->
  Mem.alloc tm 0 tf.(fn_stackspace) = (tm', sp) ->
  match_callstack f m tm cs (Mem.nextblock m) (Mem.nextblock tm) ->
  Mem.inject f m tm ->
  let te := set_locals (Csharpminor.fn_temps fn) (set_params targs (Csharpminor.fn_params fn)) in
  exists f',
     match_callstack f' m' tm'
                     (Frame cenv tf e le te sp (Mem.nextblock m) (Mem.nextblock m') :: cs)
                     (Mem.nextblock m') (Mem.nextblock tm')
  /\ Mem.inject f' m' tm'.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit build_compilenv_sound; eauto. intros [C1 C2].
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply match_callstack_alloc_variables; eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. eapply build_compilenv_domain; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply bind_parameters_agree; eauto.
Qed.

(** * Compatibility of evaluation functions with respect to memory injections. *)

Remark val_inject_val_of_bool:
  forall f b, Val.inject f (Val.of_bool b) (Val.of_bool b).
Proof.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
  intros; destruct b; constructor.
Qed.

Remark val_inject_val_of_optbool:
  forall f ob, Val.inject f (Val.of_optbool ob) (Val.of_optbool ob).
Proof.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  intros; destruct ob; simpl. destruct b; constructor. constructor.
Qed.

Ltac TrivialExists :=
  match goal with
  | [ |- exists y, Some ?x = Some y /\ Val.inject _ _ _ ] =>
      exists x; split; [auto | try(econstructor; eauto)]
  | [ |- exists y, _ /\ Val.inject _ (Vint ?x) _ ] =>
      exists (Vint x); split; [eauto with evalexpr | constructor]
  | [ |- exists y, _ /\ Val.inject _ (Vfloat ?x) _ ] =>
      exists (Vfloat x); split; [eauto with evalexpr | constructor]
  | [ |- exists y, _ /\ Val.inject _ (Vlong ?x) _ ] =>
      exists (Vlong x); split; [eauto with evalexpr | constructor]
  | _ => idtac
  end.

(** Compatibility of [eval_unop] with respect to [Val.inject]. *)

Lemma eval_unop_compat:
  forall f op v1 tv1 v,
  eval_unop op v1 = Some v ->
  Val.inject f v1 tv1 ->
  exists tv,
     eval_unop op tv1 = Some tv
  /\ Val.inject f v tv.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  destruct op; simpl; intros.
(* Goal: @ex val (fun tv : val => and (@eq (option val) (@Some val (Val.longofintu tv1)) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
  inv H; inv H0; simpl; TrivialExists.
(* Goal: @ex val (fun tv : val => and (@eq (option val) (@Some val (Val.longofintu tv1)) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
  inv H; inv H0; simpl; TrivialExists.
(* Goal: @ex val (fun tv : val => and (@eq (option val) (@Some val (Val.longofintu tv1)) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
  inv H; inv H0; simpl; TrivialExists.
(* Goal: @ex val (fun tv : val => and (@eq (option val) (@Some val (Val.longofintu tv1)) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
  inv H; inv H0; simpl; TrivialExists.
(* Goal: @ex val (fun tv : val => and (@eq (option val) (@Some val (Val.longofintu tv1)) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
  inv H; inv H0; simpl; TrivialExists.
(* Goal: @ex val (fun tv : val => and (@eq (option val) (@Some val (Val.longofintu tv1)) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
  inv H; inv H0; simpl; TrivialExists.
(* Goal: @ex val (fun tv : val => and (@eq (option val) (@Some val (Val.longofintu tv1)) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
  inv H; inv H0; simpl; TrivialExists.
(* Goal: @ex val (fun tv : val => and (@eq (option val) (@Some val (Val.longofintu tv1)) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
  inv H; inv H0; simpl; TrivialExists.
(* Goal: @ex val (fun tv : val => and (@eq (option val) (@Some val (Val.longofintu tv1)) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
  inv H; inv H0; simpl; TrivialExists.
(* Goal: @ex val (fun tv : val => and (@eq (option val) (@Some val (Val.longofintu tv1)) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
  inv H; inv H0; simpl; TrivialExists.
(* Goal: @ex val (fun tv : val => and (@eq (option val) (@Some val (Val.longofintu tv1)) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
  inv H; inv H0; simpl; TrivialExists.
(* Goal: @ex val (fun tv : val => and (@eq (option val) (@Some val (Val.longofintu tv1)) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
  inv H; inv H0; simpl; TrivialExists.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  inv H0; simpl in H; inv H. simpl. destruct (Float.to_int f0); simpl in *; inv H1. TrivialExists.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  inv H0; simpl in H; inv H. simpl. destruct (Float.to_intu f0); simpl in *; inv H1. TrivialExists.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  inv H0; simpl in H; inv H. simpl. TrivialExists.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  inv H0; simpl in H; inv H. simpl. TrivialExists.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  inv H0; simpl in H; inv H. simpl. destruct (Float32.to_int f0); simpl in *; inv H1. TrivialExists.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  inv H0; simpl in H; inv H. simpl. destruct (Float32.to_intu f0); simpl in *; inv H1. TrivialExists.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  inv H0; simpl in H; inv H. simpl. TrivialExists.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  inv H0; simpl in H; inv H. simpl. TrivialExists.
(* Goal: @ex val (fun tv : val => and (@eq (option val) (@Some val (Val.longofintu tv1)) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
  inv H; inv H0; simpl; TrivialExists.
(* Goal: @ex val (fun tv : val => and (@eq (option val) (@Some val (Val.longofintu tv1)) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
  inv H; inv H0; simpl; TrivialExists.
(* Goal: @ex val (fun tv : val => and (@eq (option val) (@Some val (Val.longofintu tv1)) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
  inv H; inv H0; simpl; TrivialExists.
(* Goal: @ex val (fun tv : val => and (@eq (option val) (@Some val (Val.longofintu tv1)) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
  inv H; inv H0; simpl; TrivialExists.
(* Goal: @ex val (fun tv : val => and (@eq (option val) (@Some val (Val.longofintu tv1)) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuoffloat tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.floatoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.longuofsingle tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflong tv1) (@Some val tv)) (Val.inject f v tv)) *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (Val.singleoflongu tv1) (@Some val tv)) (Val.inject f v tv)) *)
  inv H; inv H0; simpl; TrivialExists.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  inv H0; simpl in H; inv H. simpl. destruct (Float.to_long f0); simpl in *; inv H1. TrivialExists.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  inv H0; simpl in H; inv H. simpl. destruct (Float.to_longu f0); simpl in *; inv H1. TrivialExists.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  inv H0; simpl in H; inv H. simpl. TrivialExists.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  inv H0; simpl in H; inv H. simpl. TrivialExists.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  inv H0; simpl in H; inv H. simpl. destruct (Float32.to_long f0); simpl in *; inv H1. TrivialExists.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  inv H0; simpl in H; inv H. simpl. destruct (Float32.to_longu f0); simpl in *; inv H1. TrivialExists.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  inv H0; simpl in H; inv H. simpl. TrivialExists.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  inv H0; simpl in H; inv H. simpl. TrivialExists.
Qed.

(** Compatibility of [eval_binop] with respect to [Val.inject]. *)

Lemma eval_binop_compat:
  forall f op v1 tv1 v2 tv2 v m tm,
  eval_binop op v1 v2 m = Some v ->
  Val.inject f v1 tv1 ->
  Val.inject f v2 tv2 ->
  Mem.inject f m tm ->
  exists tv,
     eval_binop op tv1 tv2 tm = Some tv
  /\ Val.inject f v tv.
Proof.
(* Goal: final_state R r *)
  destruct op; simpl; intros; inv H.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
- TrivialExists. apply Val.add_inject; auto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
- TrivialExists. apply Val.sub_inject; auto.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
- TrivialExists. inv H0; inv H1; constructor.
(* Goal: and (Z.le Z0 ofs) (Z.lt ofs sz) *)
(* Goal: padding_freeable f empty_env tm' sp (fn_stackspace tf) *)
(* Goal: match_callstack f m tm' cs (Mem.nextblock m) sp *)
- inv H0; try discriminate; inv H1; try discriminate. simpl in *.
    destruct (Int.eq i0 Int.zero
(* Goal: @ex val (fun tv : val => and (@eq (option val) (@Some val (Vsingle (Float32.of_longu i))) (@Some val tv)) (Val.inject f (Vsingle (Float32.of_longu i)) tv)) *)
      || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H4; TrivialExists.
(* Goal: and (Z.le Z0 ofs) (Z.lt ofs sz) *)
(* Goal: padding_freeable f empty_env tm' sp (fn_stackspace tf) *)
(* Goal: match_callstack f m tm' cs (Mem.nextblock m) sp *)
- inv H0; try discriminate; inv H1; try discriminate. simpl in *.
(* Goal: @ex val (fun tv : val => and (@eq (option val) (@Some val (Vsingle (Float32.of_longu i))) (@Some val tv)) (Val.inject f (Vsingle (Float32.of_longu i)) tv)) *)
    destruct (Int.eq i0 Int.zero); inv H4. TrivialExists.
(* Goal: and (Z.le Z0 ofs) (Z.lt ofs sz) *)
(* Goal: padding_freeable f empty_env tm' sp (fn_stackspace tf) *)
(* Goal: match_callstack f m tm' cs (Mem.nextblock m) sp *)
- inv H0; try discriminate; inv H1; try discriminate. simpl in *.
    destruct (Int.eq i0 Int.zero
(* Goal: @ex val (fun tv : val => and (@eq (option val) (@Some val (Vsingle (Float32.of_longu i))) (@Some val tv)) (Val.inject f (Vsingle (Float32.of_longu i)) tv)) *)
      || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H4; TrivialExists.
(* Goal: and (Z.le Z0 ofs) (Z.lt ofs sz) *)
(* Goal: padding_freeable f empty_env tm' sp (fn_stackspace tf) *)
(* Goal: match_callstack f m tm' cs (Mem.nextblock m) sp *)
- inv H0; try discriminate; inv H1; try discriminate. simpl in *.
(* Goal: @ex val (fun tv : val => and (@eq (option val) (@Some val (Vsingle (Float32.of_longu i))) (@Some val tv)) (Val.inject f (Vsingle (Float32.of_longu i)) tv)) *)
    destruct (Int.eq i0 Int.zero); inv H4. TrivialExists.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
- TrivialExists; inv H0; inv H1; constructor.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
- TrivialExists; inv H0; inv H1; constructor.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
- TrivialExists; inv H0; inv H1; constructor.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
- TrivialExists; inv H0; inv H1; simpl; auto.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
  destruct (Int.ltu i0 Int.iwordsize); constructor.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
- TrivialExists; inv H0; inv H1; simpl; auto.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
  destruct (Int.ltu i0 Int.iwordsize); constructor.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
- TrivialExists; inv H0; inv H1; simpl; auto.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
  destruct (Int.ltu i0 Int.iwordsize); constructor.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
- TrivialExists; inv H0; inv H1; constructor.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
- TrivialExists; inv H0; inv H1; constructor.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
- TrivialExists; inv H0; inv H1; constructor.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
- TrivialExists; inv H0; inv H1; constructor.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
- TrivialExists; inv H0; inv H1; constructor.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
- TrivialExists; inv H0; inv H1; constructor.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
- TrivialExists; inv H0; inv H1; constructor.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
- TrivialExists; inv H0; inv H1; constructor.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
- TrivialExists. apply Val.addl_inject; auto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
- TrivialExists. apply Val.subl_inject; auto.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
- TrivialExists. inv H0; inv H1; constructor.
(* Goal: and (Z.le Z0 ofs) (Z.lt ofs sz) *)
(* Goal: padding_freeable f empty_env tm' sp (fn_stackspace tf) *)
(* Goal: match_callstack f m tm' cs (Mem.nextblock m) sp *)
- inv H0; try discriminate; inv H1; try discriminate. simpl in *.
    destruct (Int64.eq i0 Int64.zero
(* Goal: @ex val (fun tv : val => and (@eq (option val) (@Some val (Vsingle (Float32.of_longu i))) (@Some val tv)) (Val.inject f (Vsingle (Float32.of_longu i)) tv)) *)
      || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H4; TrivialExists.
(* Goal: and (Z.le Z0 ofs) (Z.lt ofs sz) *)
(* Goal: padding_freeable f empty_env tm' sp (fn_stackspace tf) *)
(* Goal: match_callstack f m tm' cs (Mem.nextblock m) sp *)
- inv H0; try discriminate; inv H1; try discriminate. simpl in *.
(* Goal: @ex val (fun tv : val => and (@eq (option val) (@Some val (Vsingle (Float32.of_longu i))) (@Some val tv)) (Val.inject f (Vsingle (Float32.of_longu i)) tv)) *)
    destruct (Int64.eq i0 Int64.zero); inv H4. TrivialExists.
(* Goal: and (Z.le Z0 ofs) (Z.lt ofs sz) *)
(* Goal: padding_freeable f empty_env tm' sp (fn_stackspace tf) *)
(* Goal: match_callstack f m tm' cs (Mem.nextblock m) sp *)
- inv H0; try discriminate; inv H1; try discriminate. simpl in *.
    destruct (Int64.eq i0 Int64.zero
(* Goal: @ex val (fun tv : val => and (@eq (option val) (@Some val (Vsingle (Float32.of_longu i))) (@Some val tv)) (Val.inject f (Vsingle (Float32.of_longu i)) tv)) *)
      || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H4; TrivialExists.
(* Goal: and (Z.le Z0 ofs) (Z.lt ofs sz) *)
(* Goal: padding_freeable f empty_env tm' sp (fn_stackspace tf) *)
(* Goal: match_callstack f m tm' cs (Mem.nextblock m) sp *)
- inv H0; try discriminate; inv H1; try discriminate. simpl in *.
(* Goal: @ex val (fun tv : val => and (@eq (option val) (@Some val (Vsingle (Float32.of_longu i))) (@Some val tv)) (Val.inject f (Vsingle (Float32.of_longu i)) tv)) *)
    destruct (Int64.eq i0 Int64.zero); inv H4. TrivialExists.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
- TrivialExists; inv H0; inv H1; constructor.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
- TrivialExists; inv H0; inv H1; constructor.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
- TrivialExists; inv H0; inv H1; constructor.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
- TrivialExists; inv H0; inv H1; simpl; auto.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
  destruct (Int.ltu i0 Int64.iwordsize'); constructor.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
- TrivialExists; inv H0; inv H1; simpl; auto.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
  destruct (Int.ltu i0 Int64.iwordsize'); constructor.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
- TrivialExists; inv H0; inv H1; simpl; auto.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
  destruct (Int.ltu i0 Int64.iwordsize'); constructor.
- (* cmp *)
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  TrivialExists. inv H0; inv H1; auto. apply val_inject_val_of_optbool.
- (* cmpu *)
(* Goal: @ex val (fun tv : val => and (@eq (option val) (@Some val (Vsingle (Float32.of_longu i))) (@Some val tv)) (Val.inject f (Vsingle (Float32.of_longu i)) tv)) *)
  TrivialExists. unfold Val.cmpu.
  destruct (Val.cmpu_bool (Mem.valid_pointer m) c v1 v2) as [b|] eqn:E.
  replace (Val.cmpu_bool (Mem.valid_pointer tm) c tv1 tv2) with (Some b).
  apply val_inject_val_of_optbool.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  symmetry. eapply Val.cmpu_bool_inject; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  intros; eapply Mem.valid_pointer_inject_val; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  intros; eapply Mem.different_pointers_inject; eauto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  simpl; auto.
- (* cmpf *)
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  TrivialExists. inv H0; inv H1; auto. apply val_inject_val_of_optbool.
- (* cmpfs *)
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  TrivialExists. inv H0; inv H1; auto. apply val_inject_val_of_optbool.
- (* cmpl *)
  unfold Val.cmpl in *. inv H0; inv H1; simpl in H4; inv H4.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; split. simpl; eauto. apply val_inject_val_of_bool.
- (* cmplu *)
  unfold Val.cmplu in *.
  destruct (Val.cmplu_bool (Mem.valid_pointer m) c v1 v2) as [b|] eqn:E.
  simpl in H4; inv H4.
  replace (Val.cmplu_bool (Mem.valid_pointer tm) c tv1 tv2) with (Some b).
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; split. simpl; eauto. apply val_inject_val_of_bool.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  symmetry. eapply Val.cmplu_bool_inject; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  intros; eapply Mem.valid_pointer_inject_val; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  intros; eapply Mem.different_pointers_inject; eauto.
(* Goal: and (Z.le Z0 ofs) (Z.lt ofs sz) *)
(* Goal: padding_freeable f empty_env tm' sp (fn_stackspace tf) *)
(* Goal: match_callstack f m tm' cs (Mem.nextblock m) sp *)
  discriminate.
Qed.

(** * Correctness of Cminor construction functions *)

(** Correctness of the variable accessor [var_addr] *)

Lemma var_addr_correct:
  forall cenv id f tf e le te sp lo hi m cs tm b,
  match_callstack f m tm (Frame cenv tf e le te sp lo hi :: cs) (Mem.nextblock m) (Mem.nextblock tm) ->
  eval_var_addr ge e id b ->
  exists tv,
     eval_expr tge (Vptr sp Ptrofs.zero) te tm (var_addr cenv id) tv
  /\ Val.inject f (Vptr b Ptrofs.zero) tv.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  unfold var_addr; intros.
(* Goal: @ex val (fun tv : val => and (eval_expr tge (Vptr sp Ptrofs.zero) te tm match @PTree.get Z id cenv with | Some ofs => Econst (Oaddrstack (Ptrofs.repr ofs)) | None => Econst (Oaddrsymbol id Ptrofs.zero) end tv) (Val.inject f (Vptr b Ptrofs.zero) tv)) *)
  assert (match_var f sp e!id cenv!id).
(* Goal: final_state R r *)
    inv H. inv MENV. auto.
(* Goal: lbl_stmt_tail sl (@snd (list (prod Z nat)) nat (switch_table sl O)) (select_switch_default sl) *)
  inv H1; inv H0; try congruence.
  (* local *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  exists (Vptr sp (Ptrofs.repr ofs)); split.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  constructor. simpl. rewrite Ptrofs.add_zero_l; auto.
(* Goal: lbl_stmt_tail sl (@snd (list (prod Z nat)) nat (switch_table sl O)) (select_switch_default sl) *)
  congruence.
  (* global *)
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit match_callstack_match_globalenvs; eauto. intros [bnd MG]. inv MG.
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  exists (Vptr b Ptrofs.zero); split.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  constructor. simpl. unfold Genv.symbol_address. 
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  rewrite symbols_preserved. rewrite H2. auto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; eauto.
Qed.

(** * Semantic preservation for the translation *)

(** The proof of semantic preservation uses simulation diagrams of the
  following form:
<<
       e, m1, s ----------------- sp, te1, tm1, ts
          |                                |
         t|                                |t
          v                                v
       e, m2, out --------------- sp, te2, tm2, tout
>>
  where [ts] is the Cminor statement obtained by translating the
  C#minor statement [s].  The left vertical arrow is an execution
  of a C#minor statement.  The right vertical arrow is an execution
  of a Cminor statement.  The precondition (top vertical bar)
  includes a [mem_inject] relation between the memory states [m1] and [tm1],
  and a [match_callstack] relation for any callstack having
  [e], [te1], [sp] as top frame.  The postcondition (bottom vertical bar)
  is the existence of a memory injection [f2] that extends the injection
  [f1] we started with, preserves the [match_callstack] relation for
  the transformed callstack at the final state, and validates a
  [outcome_inject] relation between the outcomes [out] and [tout].
*)

(** ** Semantic preservation for expressions *)

Remark bool_of_val_inject:
  forall f v tv b,
  Val.bool_of_val v b -> Val.inject f v tv -> Val.bool_of_val tv b.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. inv H0; inv H; constructor; auto.
Qed.

Lemma transl_constant_correct:
  forall f sp cst v,
  Csharpminor.eval_constant cst = Some v ->
  exists tv,
     eval_constant tge sp (transl_constant cst) = Some tv
  /\ Val.inject f v tv.
Proof.
(* Goal: final_state R r *)
  destruct cst; simpl; intros; inv H.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  exists (Vint i); auto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  exists (Vfloat f0); auto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  exists (Vsingle f0); auto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  exists (Vlong i); auto.
Qed.

Lemma transl_expr_correct:
  forall f m tm cenv tf e le te sp lo hi cs
    (MINJ: Mem.inject f m tm)
    (MATCH: match_callstack f m tm
             (Frame cenv tf e le te sp lo hi :: cs)
             (Mem.nextblock m) (Mem.nextblock tm)),
  forall a v,
  Csharpminor.eval_expr ge e le m a v ->
  forall ta
    (TR: transl_expr cenv a = OK ta),
  exists tv,
     eval_expr tge (Vptr sp Ptrofs.zero) te tm ta tv
  /\ Val.inject f v tv.
Proof.
  induction 3; intros; simpl in TR; try (monadInv TR).
  (* Etempvar *)
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  inv MATCH. exploit MTMP; eauto. intros [tv [A B]].
(* Goal: lbl_stmt_tail (LScons (@None Z) s sl) (S x) l *)
(* Goal: @eq nat (switch_target i dfl tbl1) (Init.Nat.add (S x) base) *)
(* Goal: @eq nat (switch_target i dfl tbl1) dfl *)
  exists tv; split. constructor; auto. auto.
  (* Eaddrof *)
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply var_addr_correct; eauto.
  (* Econst *)
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit transl_constant_correct; eauto. intros [tv [A B]].
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exists tv; split; eauto. constructor; eauto.
  (* Eunop *)
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit IHeval_expr; eauto. intros [tv1 [EVAL1 INJ1]].
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit eval_unop_compat; eauto. intros [tv [EVAL INJ]].
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exists tv; split; auto. econstructor; eauto.
  (* Ebinop *)
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit IHeval_expr1; eauto. intros [tv1 [EVAL1 INJ1]].
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit IHeval_expr2; eauto. intros [tv2 [EVAL2 INJ2]].
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit eval_binop_compat; eauto. intros [tv [EVAL INJ]].
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exists tv; split. econstructor; eauto. auto.
  (* Eload *)
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit IHeval_expr; eauto. intros [tv1 [EVAL1 INJ1]].
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit Mem.loadv_inject; eauto. intros [tv [LOAD INJ]].
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exists tv; split. econstructor; eauto. auto.
Qed.

Lemma transl_exprlist_correct:
  forall f m tm cenv tf e le te sp lo hi cs
    (MINJ: Mem.inject f m tm)
    (MATCH: match_callstack f m tm
             (Frame cenv tf e le te sp lo hi :: cs)
             (Mem.nextblock m) (Mem.nextblock tm)),
  forall a v,
  Csharpminor.eval_exprlist ge e le m a v ->
  forall ta
    (TR: transl_exprlist cenv a = OK ta),
  exists tv,
     eval_exprlist tge (Vptr sp Ptrofs.zero) te tm ta tv
  /\ Val.inject_list f v tv.
Proof.
(* Goal: forall (f : Val.meminj) (m tm : Mem.mem) (cenv : compilenv) (tf : function) (e : Csharpminor.env) (le : temp_env) (te : env) (sp lo hi : block) (cs : list frame) (_ : Mem.inject f m tm) (_ : match_callstack f m tm (@cons frame (Frame cenv tf e le te sp lo hi) cs) (Mem.nextblock m) (Mem.nextblock tm)) (a : list Csharpminor.expr) (v : list val) (_ : Csharpminor.eval_exprlist ge e le m a v) (ta : list expr) (_ : @eq (res (list expr)) (transl_exprlist cenv a) (@OK (list expr) ta)), @ex (list val) (fun tv : list val => and (eval_exprlist tge (Vptr sp Ptrofs.zero) te tm ta tv) (Val.inject_list f v tv)) *)
  induction 3; intros; monadInv TR.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
  exists (@nil val); split. constructor. constructor.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit transl_expr_correct; eauto. intros [tv1 [EVAL1 VINJ1]].
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit IHeval_exprlist; eauto. intros [tv2 [EVAL2 VINJ2]].
(* Goal: lbl_stmt_tail (LScons (@None Z) s sl) (S x) l *)
(* Goal: @eq nat (switch_target i dfl tbl1) (Init.Nat.add (S x) base) *)
(* Goal: @eq nat (switch_target i dfl tbl1) dfl *)
  exists (tv1 :: tv2); split. constructor; auto. constructor; auto.
Qed.

(** ** Semantic preservation for statements and functions *)

Inductive match_cont: Csharpminor.cont -> Cminor.cont -> compilenv -> exit_env -> callstack -> Prop :=
  | match_Kstop: forall cenv xenv,
      match_cont Csharpminor.Kstop Kstop cenv xenv nil
  | match_Kseq: forall s k ts tk cenv xenv cs,
      transl_stmt cenv xenv s = OK ts ->
      match_cont k tk cenv xenv cs ->
      match_cont (Csharpminor.Kseq s k) (Kseq ts tk) cenv xenv cs
  | match_Kseq2: forall s1 s2 k ts1 tk cenv xenv cs,
      transl_stmt cenv xenv s1 = OK ts1 ->
      match_cont (Csharpminor.Kseq s2 k) tk cenv xenv cs ->
      match_cont (Csharpminor.Kseq (Csharpminor.Sseq s1 s2) k)
                 (Kseq ts1 tk) cenv xenv cs
  | match_Kblock: forall k tk cenv xenv cs,
      match_cont k tk cenv xenv cs ->
      match_cont (Csharpminor.Kblock k) (Kblock tk) cenv (true :: xenv) cs
  | match_Kblock2: forall k tk cenv xenv cs,
      match_cont k tk cenv xenv cs ->
      match_cont k (Kblock tk) cenv (false :: xenv) cs
  | match_Kcall: forall optid fn e le k tfn sp te tk cenv xenv lo hi cs sz cenv',
      transl_funbody cenv sz fn = OK tfn ->
      match_cont k tk cenv xenv cs ->
      match_cont (Csharpminor.Kcall optid fn e le k)
                 (Kcall optid tfn (Vptr sp Ptrofs.zero) te tk)
                 cenv' nil
                 (Frame cenv tfn e le te sp lo hi :: cs).

Inductive match_states: Csharpminor.state -> Cminor.state -> Prop :=
  | match_state:
      forall fn s k e le m tfn ts tk sp te tm cenv xenv f lo hi cs sz
      (TRF: transl_funbody cenv sz fn = OK tfn)
      (TR: transl_stmt cenv xenv s = OK ts)
      (MINJ: Mem.inject f m tm)
      (MCS: match_callstack f m tm
               (Frame cenv tfn e le te sp lo hi :: cs)
               (Mem.nextblock m) (Mem.nextblock tm))
      (MK: match_cont k tk cenv xenv cs),
      match_states (Csharpminor.State fn s k e le m)
                   (State tfn ts tk (Vptr sp Ptrofs.zero) te tm)
  | match_state_seq:
      forall fn s1 s2 k e le m tfn ts1 tk sp te tm cenv xenv f lo hi cs sz
      (TRF: transl_funbody cenv sz fn = OK tfn)
      (TR: transl_stmt cenv xenv s1 = OK ts1)
      (MINJ: Mem.inject f m tm)
      (MCS: match_callstack f m tm
               (Frame cenv tfn e le te sp lo hi :: cs)
               (Mem.nextblock m) (Mem.nextblock tm))
      (MK: match_cont (Csharpminor.Kseq s2 k) tk cenv xenv cs),
      match_states (Csharpminor.State fn (Csharpminor.Sseq s1 s2) k e le m)
                   (State tfn ts1 tk (Vptr sp Ptrofs.zero) te tm)
  | match_callstate:
      forall fd args k m tfd targs tk tm f cs cenv
      (TR: transl_fundef fd = OK tfd)
      (MINJ: Mem.inject f m tm)
      (MCS: match_callstack f m tm cs (Mem.nextblock m) (Mem.nextblock tm))
      (MK: match_cont k tk cenv nil cs)
      (ISCC: Csharpminor.is_call_cont k)
      (ARGSINJ: Val.inject_list f args targs),
      match_states (Csharpminor.Callstate fd args k m)
                   (Callstate tfd targs tk tm)
  | match_returnstate:
      forall v k m tv tk tm f cs cenv
      (MINJ: Mem.inject f m tm)
      (MCS: match_callstack f m tm cs (Mem.nextblock m) (Mem.nextblock tm))
      (MK: match_cont k tk cenv nil cs)
      (RESINJ: Val.inject f v tv),
      match_states (Csharpminor.Returnstate v k m)
                   (Returnstate tv tk tm).

Remark val_inject_function_pointer:
  forall bound v fd f tv,
  Genv.find_funct ge v = Some fd ->
  match_globalenvs f bound ->
  Val.inject f v tv ->
  tv = v.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. exploit Genv.find_funct_inv; eauto. intros [b EQ]. subst v.
(* Goal: @eq val tv (Vptr b Ptrofs.zero) *)
  rewrite Genv.find_funct_find_funct_ptr in H.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  assert (f b = Some(b, 0)). inv H0. apply DOMAIN. eapply FUNCTIONS; eauto.
(* Goal: @eq val (Vptr b2 (Ptrofs.add Ptrofs.zero (Ptrofs.repr Z0))) (Vptr b2 Ptrofs.zero) *)
  inv H1. rewrite H2 in H5; inv H5. reflexivity.
Qed.

Lemma match_call_cont:
  forall k tk cenv xenv cs,
  match_cont k tk cenv xenv cs ->
  match_cont (Csharpminor.call_cont k) (call_cont tk) cenv nil cs.
Proof.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  induction 1; simpl; auto; econstructor; eauto.
Qed.

Lemma match_is_call_cont:
  forall tfn te sp tm k tk cenv xenv cs,
  match_cont k tk cenv xenv cs ->
  Csharpminor.is_call_cont k ->
  exists tk',
    star step tge (State tfn Sskip tk sp te tm)
               E0 (State tfn Sskip tk' sp te tm)
    /\ is_call_cont tk'
    /\ match_cont k tk' cenv nil cs.
Proof.
(* Goal: @eq (option val) (@PTree.get val id e) (@Some val Vundef) *)
(* Goal: @eq (option val) (@PTree.get val id (@PTree.set val a Vundef (set_locals il e))) (@Some val Vundef) *)
  induction 1; simpl; intros; try contradiction.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; split. apply star_refl. split. exact I. econstructor; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit IHmatch_cont; eauto.
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  intros [tk' [A B]]. exists tk'; split.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply star_left; eauto. constructor. traceEq. auto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; split. apply star_refl. split. exact I. econstructor; eauto.
Qed.

(** Properties of [switch] compilation *)

Inductive lbl_stmt_tail: lbl_stmt -> nat -> lbl_stmt -> Prop :=
  | lstail_O: forall sl,
      lbl_stmt_tail sl O sl
  | lstail_S: forall c s sl n sl',
      lbl_stmt_tail sl n sl' ->
      lbl_stmt_tail (LScons c s sl) (S n) sl'.

Lemma switch_table_default:
  forall sl base,
  exists n,
     lbl_stmt_tail sl n (select_switch_default sl)
  /\ snd (switch_table sl base) = (n + base)%nat.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  induction sl; simpl; intros.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
- exists O; split. constructor. omega.
- destruct o.
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  + destruct (IHsl (S base)) as (n & P & Q). exists (S n); split.
(* Goal: lbl_stmt_tail (LScons (@None Z) s sl) (S x) l *)
(* Goal: @eq nat (switch_target i dfl tbl1) (Init.Nat.add (S x) base) *)
(* Goal: @eq nat (switch_target i dfl tbl1) dfl *)
    constructor; auto.
(* Goal: @eq nat (switch_target i dfl tbl1) (Init.Nat.add (S x) base) *)
(* Goal: @eq nat (switch_target i dfl tbl1) dfl *)
    destruct (switch_table sl (S base)) as [tbl dfl]; simpl in *. omega.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
  + exists O; split. constructor.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
    destruct (switch_table sl (S base)) as [tbl dfl]; simpl in *. auto.
Qed.

Lemma switch_table_case:
  forall i sl base dfl,
  match select_switch_case i sl with
  | None =>
      switch_target i dfl (fst (switch_table sl base)) = dfl
  | Some sl' =>
      exists n,
         lbl_stmt_tail sl n sl'
      /\ switch_target i dfl (fst (switch_table sl base)) = (n + base)%nat
  end.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  induction sl; simpl; intros.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
- auto.
- destruct (switch_table sl (S base)) as [tbl1 dfl1] eqn:ST.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  destruct o; simpl.
(* Goal: match (if zeq z i then @Some lbl_stmt (LScons (@Some Z z) s sl) else select_switch_case i sl) with | Some sl' => @ex nat (fun n : nat => and (lbl_stmt_tail (LScons (@Some Z z) s sl) n sl') (@eq nat (if zeq i z then base else switch_target i dfl tbl1) (Init.Nat.add n base))) | None => @eq nat (if zeq i z then base else switch_target i dfl tbl1) dfl end *)
(* Goal: match select_switch_case i sl with | Some sl' => @ex nat (fun n : nat => and (lbl_stmt_tail (LScons (@None Z) s sl) n sl') (@eq nat (switch_target i dfl tbl1) (Init.Nat.add n base))) | None => @eq nat (switch_target i dfl tbl1) dfl end *)
  rewrite dec_eq_sym. destruct (zeq i z).
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  exists O; split; auto. constructor.
(* Goal: match select_switch_case i sl with | Some sl' => @ex nat (fun n : nat => and (lbl_stmt_tail (LScons (@None Z) s sl) n sl') (@eq nat (switch_target i dfl tbl1) (Init.Nat.add n base))) | None => @eq nat (switch_target i dfl tbl1) dfl end *)
  specialize (IHsl (S base) dfl). rewrite ST in IHsl. simpl in *.
(* Goal: match select_switch_case i sl with | Some sl' => @ex nat (fun n : nat => and (lbl_stmt_tail (LScons (@None Z) s sl) n sl') (@eq nat (switch_target i dfl tbl1) (Init.Nat.add n base))) | None => @eq nat (switch_target i dfl tbl1) dfl end *)
  destruct (select_switch_case i sl).
(* Goal: lbl_stmt_tail (LScons (@None Z) s sl) (S x) l *)
(* Goal: @eq nat (switch_target i dfl tbl1) (Init.Nat.add (S x) base) *)
(* Goal: @eq nat (switch_target i dfl tbl1) dfl *)
  destruct IHsl as (x & P & Q). exists (S x); split. constructor; auto. omega.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  auto.
(* Goal: match select_switch_case i sl with | Some sl' => @ex nat (fun n : nat => and (lbl_stmt_tail (LScons (@None Z) s sl) n sl') (@eq nat (switch_target i dfl tbl1) (Init.Nat.add n base))) | None => @eq nat (switch_target i dfl tbl1) dfl end *)
  specialize (IHsl (S base) dfl). rewrite ST in IHsl. simpl in *.
(* Goal: match select_switch_case i sl with | Some sl' => @ex nat (fun n : nat => and (lbl_stmt_tail (LScons (@None Z) s sl) n sl') (@eq nat (switch_target i dfl tbl1) (Init.Nat.add n base))) | None => @eq nat (switch_target i dfl tbl1) dfl end *)
  destruct (select_switch_case i sl).
(* Goal: lbl_stmt_tail (LScons (@None Z) s sl) (S x) l *)
(* Goal: @eq nat (switch_target i dfl tbl1) (Init.Nat.add (S x) base) *)
(* Goal: @eq nat (switch_target i dfl tbl1) dfl *)
  destruct IHsl as (x & P & Q). exists (S x); split. constructor; auto. omega.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  auto.
Qed.

Lemma switch_table_select:
  forall i sl,
  lbl_stmt_tail sl
                (switch_target i (snd (switch_table sl O)) (fst (switch_table sl O)))
                (select_switch i sl).
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  unfold select_switch; intros.
(* Goal: lbl_stmt_tail sl (switch_target i (@snd (list (prod Z nat)) nat (switch_table sl O)) (@fst (list (prod Z nat)) nat (switch_table sl O))) match select_switch_case i sl with | Some sl' => sl' | None => select_switch_default sl end *)
  generalize (switch_table_case i sl O (snd (switch_table sl O))).
(* Goal: forall _ : match select_switch_case i sl with | Some sl' => @ex nat (fun n : nat => and (lbl_stmt_tail sl n sl') (@eq nat (switch_target i (@snd (list (prod Z nat)) nat (switch_table sl O)) (@fst (list (prod Z nat)) nat (switch_table sl O))) (Init.Nat.add n O))) | None => @eq nat (switch_target i (@snd (list (prod Z nat)) nat (switch_table sl O)) (@fst (list (prod Z nat)) nat (switch_table sl O))) (@snd (list (prod Z nat)) nat (switch_table sl O)) end, lbl_stmt_tail sl (switch_target i (@snd (list (prod Z nat)) nat (switch_table sl O)) (@fst (list (prod Z nat)) nat (switch_table sl O))) match select_switch_case i sl with | Some sl' => sl' | None => select_switch_default sl end *)
  destruct (select_switch_case i sl) as [sl'|].
(* Goal: lbl_stmt_tail sl (@snd (list (prod Z nat)) nat (switch_table sl O)) (select_switch_default sl) *)
  intros (n & P & Q). replace (n + O)%nat with n in Q by omega. congruence.
(* Goal: forall _ : @eq nat (switch_target i (@snd (list (prod Z nat)) nat (switch_table sl O)) (@fst (list (prod Z nat)) nat (switch_table sl O))) (@snd (list (prod Z nat)) nat (switch_table sl O)), lbl_stmt_tail sl (switch_target i (@snd (list (prod Z nat)) nat (switch_table sl O)) (@fst (list (prod Z nat)) nat (switch_table sl O))) (select_switch_default sl) *)
  intros E; rewrite E.
(* Goal: lbl_stmt_tail sl (@snd (list (prod Z nat)) nat (switch_table sl O)) (select_switch_default sl) *)
  destruct (switch_table_default sl O) as (n & P & Q).
(* Goal: lbl_stmt_tail sl (@snd (list (prod Z nat)) nat (switch_table sl O)) (select_switch_default sl) *)
  replace (n + O)%nat with n in Q by omega. congruence.
Qed.

Inductive transl_lblstmt_cont(cenv: compilenv) (xenv: exit_env): lbl_stmt -> cont -> cont -> Prop :=
  | tlsc_default: forall k,
      transl_lblstmt_cont cenv xenv LSnil k (Kblock (Kseq Sskip k))
  | tlsc_case: forall i s ls k ts k',
      transl_stmt cenv (switch_env (LScons i s ls) xenv) s = OK ts ->
      transl_lblstmt_cont cenv xenv ls k k' ->
      transl_lblstmt_cont cenv xenv (LScons i s ls) k (Kblock (Kseq ts k')).

Lemma switch_descent:
  forall cenv xenv k ls body s,
  transl_lblstmt cenv (switch_env ls xenv) ls body = OK s ->
  exists k',
  transl_lblstmt_cont cenv xenv ls k k'
  /\ (forall f sp e m,
      plus step tge (State f s k sp e m) E0 (State f body k' sp e m)).
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  induction ls; intros.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl ts tk1) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
- monadInv H. econstructor; split.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
  econstructor.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. eapply plus_two. constructor. constructor. auto.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl ts tk1) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
- monadInv H. exploit IHls; eauto. intros [k' [A B]].
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  econstructor; split.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. eapply plus_star_trans. eauto.
(* Goal: or (Z.le (Z.add ofs1 sz0) (align sz1 (block_alignment sz))) (Z.le (Z.add (align sz1 (block_alignment sz)) sz) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
  eapply star_left. constructor. apply star_one. constructor.
(* Goal: @eq val (Vptr b2 (Ptrofs.add Ptrofs.zero (Ptrofs.repr Z0))) (Vptr b2 Ptrofs.zero) *)
  reflexivity. traceEq.
Qed.

Lemma switch_ascent:
  forall f sp e m cenv xenv ls n ls',
  lbl_stmt_tail ls n ls' ->
  forall k k1,
  transl_lblstmt_cont cenv xenv ls k k1 ->
  exists k2,
  star step tge (State f (Sexit n) k1 sp e m)
             E0 (State f (Sexit O) k2 sp e m)
  /\ transl_lblstmt_cont cenv xenv ls' k k2.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  induction 1; intros.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
- exists k1; split; auto. apply star_refl.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
- inv H0. exploit IHlbl_stmt_tail; eauto. intros (k2 & P & Q).
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  exists k2; split; auto.
(* Goal: or (Z.le (Z.add ofs1 sz0) (align sz1 (block_alignment sz))) (Z.le (Z.add (align sz1 (block_alignment sz)) sz) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
  eapply star_left. constructor. eapply star_left. constructor. eexact P.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eauto. auto.
Qed.

Lemma switch_match_cont:
  forall cenv xenv k cs tk ls tk',
  match_cont k tk cenv xenv cs ->
  transl_lblstmt_cont cenv xenv ls tk tk' ->
  match_cont (Csharpminor.Kseq (seq_of_lbl_stmt ls) k) tk' cenv (false :: switch_env ls xenv) cs.
Proof.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  induction ls; intros; simpl.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  inv H0. apply match_Kblock2. econstructor; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  inv H0. apply match_Kblock2. eapply match_Kseq2. auto. eauto.
Qed.

Lemma switch_match_states:
  forall fn k e le m tfn ts tk sp te tm cenv xenv f lo hi cs sz ls body tk'
    (TRF: transl_funbody cenv sz fn = OK tfn)
    (TR: transl_lblstmt cenv (switch_env ls xenv) ls body = OK ts)
    (MINJ: Mem.inject f m tm)
    (MCS: match_callstack f m tm
               (Frame cenv tfn e le te sp lo hi :: cs)
               (Mem.nextblock m) (Mem.nextblock tm))
    (MK: match_cont k tk cenv xenv cs)
    (TK: transl_lblstmt_cont cenv xenv ls tk tk'),
  exists S,
  plus step tge (State tfn (Sexit O) tk' (Vptr sp Ptrofs.zero) te tm) E0 S
  /\ match_states (Csharpminor.State fn (seq_of_lbl_stmt ls) k e le m) S.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. inv TK.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
- econstructor; split. eapply plus_two. constructor. constructor. auto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply match_state; eauto.
(* Goal: or (Z.le (Z.add ofs1 sz0) (align sz1 (block_alignment sz))) (Z.le (Z.add (align sz1 (block_alignment sz)) sz) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
- econstructor; split. eapply plus_left. constructor. apply star_one. constructor. auto.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  simpl. eapply match_state_seq; eauto. simpl. eapply switch_match_cont; eauto.
Qed.

Lemma transl_lblstmt_suffix:
  forall cenv xenv ls n ls',
  lbl_stmt_tail ls n ls' ->
  forall body ts, transl_lblstmt cenv (switch_env ls xenv) ls body = OK ts ->
  exists body', exists ts', transl_lblstmt cenv (switch_env ls' xenv) ls' body' = OK ts'.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  induction 1; intros.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
- exists body, ts; auto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
- monadInv H0. eauto.
Qed.

(** Commutation between [find_label] and compilation *)

Section FIND_LABEL.

Variable lbl: label.
Variable cenv: compilenv.
Variable cs: callstack.

Lemma transl_lblstmt_find_label_context:
  forall xenv ls body ts tk1 tk2 ts' tk',
  transl_lblstmt cenv (switch_env ls xenv) ls body = OK ts ->
  transl_lblstmt_cont cenv xenv ls tk1 tk2 ->
  find_label lbl body tk2 = Some (ts', tk') ->
  find_label lbl ts tk1 = Some (ts', tk').
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  induction ls; intros.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl ts tk1) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
- monadInv H. inv H0. simpl. rewrite H1. auto.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl ts tk1) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
- monadInv H. inv H0. simpl in H6. eapply IHls; eauto.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  replace x with ts0 by congruence. simpl. rewrite H1. auto.
Qed.

Lemma transl_find_label:
  forall s k xenv ts tk,
  transl_stmt cenv xenv s = OK ts ->
  match_cont k tk cenv xenv cs ->
  match Csharpminor.find_label lbl s k with
  | None => find_label lbl ts tk = None
  | Some(s', k') =>
      exists ts', exists tk', exists xenv',
        find_label lbl ts tk = Some(ts', tk')
     /\ transl_stmt cenv xenv' s' = OK ts'
     /\ match_cont k' tk' cenv xenv' cs
  end

with transl_lblstmt_find_label:
  forall ls xenv body k ts tk tk1,
  transl_lblstmt cenv (switch_env ls xenv) ls body = OK ts ->
  match_cont k tk cenv xenv cs ->
  transl_lblstmt_cont cenv xenv ls tk tk1 ->
  find_label lbl body tk1 = None ->
  match Csharpminor.find_label_ls lbl ls k with
  | None => find_label lbl ts tk = None
  | Some(s', k') =>
      exists ts', exists tk', exists xenv',
        find_label lbl ts tk = Some(ts', tk')
     /\ transl_stmt cenv xenv' s' = OK ts'
     /\ match_cont k' tk' cenv xenv' cs
  end.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. destruct s; try (monadInv H); simpl; auto.
  (* seq *)
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit (transl_find_label s1). eauto. eapply match_Kseq. eexact EQ1. eauto.
  destruct (Csharpminor.find_label lbl s1 (Csharpminor.Kseq s2 k)) as [[s' k'] | ].
  intros [ts' [tk' [xenv' [A [B C]]]]].
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  exists ts'; exists tk'; exists xenv'. intuition. rewrite A; auto.
(* Goal: forall _ : @eq (res fundef) (@OK (AST.fundef function) (@External function e)) (@OK fundef tf), @eq signature (funsig tf) (ef_sig e) *)
  intro. rewrite H. apply transl_find_label with xenv; auto.
  (* ifthenelse *)
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit (transl_find_label s1). eauto. eauto.
  destruct (Csharpminor.find_label lbl s1 k) as [[s' k'] | ].
  intros [ts' [tk' [xenv' [A [B C]]]]].
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  exists ts'; exists tk'; exists xenv'. intuition. rewrite A; auto.
(* Goal: forall _ : @eq (res fundef) (@OK (AST.fundef function) (@External function e)) (@OK fundef tf), @eq signature (funsig tf) (ef_sig e) *)
  intro. rewrite H. apply transl_find_label with xenv; auto.
  (* loop *)
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  apply transl_find_label with xenv. auto. econstructor; eauto. simpl. rewrite EQ; auto.
  (* block *)
(* Goal: lbl_stmt_tail (LScons (@None Z) s sl) (S x) l *)
(* Goal: @eq nat (switch_target i dfl tbl1) (Init.Nat.add (S x) base) *)
(* Goal: @eq nat (switch_target i dfl tbl1) dfl *)
  apply transl_find_label with (true :: xenv). auto. constructor; auto.
  (* switch *)
(* Goal: @eq (option (prod stmt cont)) (find_label lbl ts tk1) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  simpl in H. destruct (switch_table l O) as [tbl dfl]. monadInv H.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit switch_descent; eauto. intros [k' [A B]].
(* Goal: @eq val (Vptr b2 (Ptrofs.add Ptrofs.zero (Ptrofs.repr Z0))) (Vptr b2 Ptrofs.zero) *)
  eapply transl_lblstmt_find_label. eauto. eauto. eauto. reflexivity.
  (* return *)
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  destruct o; monadInv H; auto.
  (* label *)
  destruct (ident_eq lbl l).
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  exists x; exists tk; exists xenv; auto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  apply transl_find_label with xenv; auto.

(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. destruct ls; monadInv H; simpl.
  (* nil *)
(* Goal: @eq val tv (Vptr b Ptrofs.zero) *)
  inv H1. rewrite H2. auto.
  (* cons *)
(* Goal: @eq val tv (Vptr b Ptrofs.zero) *)
  inv H1. simpl in H7.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit (transl_find_label s). eauto. eapply switch_match_cont; eauto.
  destruct (Csharpminor.find_label lbl s (Csharpminor.Kseq (seq_of_lbl_stmt ls) k)) as [[s' k''] | ].
  intros [ts' [tk' [xenv' [A [B C]]]]].
(* Goal: not (@eq positive id a) *)
  exists ts'; exists tk'; exists xenv'; intuition.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply transl_lblstmt_find_label_context; eauto.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  simpl. replace x with ts0 by congruence. rewrite H2. auto.
(* Goal: forall _ : @eq (res fundef) (@OK (AST.fundef function) (@External function e)) (@OK fundef tf), @eq signature (funsig tf) (ef_sig e) *)
  intro. eapply transl_lblstmt_find_label. eauto. auto. eauto.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  simpl. replace x with ts0 by congruence. rewrite H2. auto.
Qed.

End FIND_LABEL.

Lemma transl_find_label_body:
  forall cenv xenv size f tf k tk cs lbl s' k',
  transl_funbody cenv size f = OK tf ->
  match_cont k tk cenv xenv cs ->
  Csharpminor.find_label lbl f.(Csharpminor.fn_body) (Csharpminor.call_cont k) = Some (s', k') ->
  exists ts', exists tk', exists xenv',
     find_label lbl tf.(fn_body) (call_cont tk) = Some(ts', tk')
  /\ transl_stmt cenv xenv' s' = OK ts'
  /\ match_cont k' tk' cenv xenv' cs.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. monadInv H. simpl.
  exploit transl_find_label. eexact EQ. eapply match_call_cont. eexact H0.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  instantiate (1 := lbl). rewrite H1. auto.
Qed.

(** The simulation diagram. *)

Fixpoint seq_left_depth (s: Csharpminor.stmt) : nat :=
  match s with
  | Csharpminor.Sseq s1 s2 => S (seq_left_depth s1)
  | _ => O
  end.

Definition measure (S: Csharpminor.state) : nat :=
  match S with
  | Csharpminor.State fn s k e le m => seq_left_depth s
  | _ => O
  end.

Lemma transl_step_correct:
  forall S1 t S2, Csharpminor.step ge S1 t S2 ->
  forall T1, match_states S1 T1 ->
  (exists T2, plus step tge T1 t T2 /\ match_states S2 T2)
  \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 T1)%nat.
Proof.
  induction 1; intros T1 MSTATE; inv MSTATE.

(* skip seq *)
(* Goal: or (Z.le (Z.add ofs1 sz0) (align sz1 (block_alignment sz))) (Z.le (Z.add (align sz1 (block_alignment sz)) sz) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
  monadInv TR. left.
  dependent induction MK.
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  econstructor; split.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
  apply plus_one. constructor.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; eauto.
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  econstructor; split.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
  apply plus_one. constructor.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply match_state_seq; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit IHMK; eauto. intros [T2 [A B]].
(* Goal: or (Z.le (Z.add ofs1 sz0) (align sz1 (block_alignment sz))) (Z.le (Z.add (align sz1 (block_alignment sz)) sz) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
  exists T2; split. eapply plus_left. constructor. apply plus_star; eauto. traceEq.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  auto.
(* skip block *)
(* Goal: or (Z.le (Z.add ofs1 sz0) (align sz1 (block_alignment sz))) (Z.le (Z.add (align sz1 (block_alignment sz)) sz) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
  monadInv TR. left.
  dependent induction MK.
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  econstructor; split.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
  apply plus_one. constructor.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit IHMK; eauto. intros [T2 [A B]].
(* Goal: or (Z.le (Z.add ofs1 sz0) (align sz1 (block_alignment sz))) (Z.le (Z.add (align sz1 (block_alignment sz)) sz) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
  exists T2; split. eapply plus_left. constructor. apply plus_star; eauto. traceEq.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  auto.
(* skip call *)
(* Goal: or (Z.le (Z.add ofs1 sz0) (align sz1 (block_alignment sz))) (Z.le (Z.add (align sz1 (block_alignment sz)) sz) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
  monadInv TR. left.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit match_is_call_cont; eauto. intros [tk' [A [B C]]].
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit match_callstack_freelist; eauto. intros [tm' [P [Q R]]].
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  econstructor; split.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply plus_right. eexact A. apply step_skip_call. auto. eauto. traceEq.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; eauto.

(* set *)
  monadInv TR.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]].
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  left; econstructor; split.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  apply plus_one. econstructor; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply match_callstack_set_temp; eauto.

(* store *)
  monadInv TR.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit transl_expr_correct. eauto. eauto. eexact H. eauto.
(* Goal: forall _ : @ex val (fun tv : val => and (eval_expr tge (Vptr sp Ptrofs.zero) te tm x tv) (Val.inject f v1 tv)), @ex (list val) (fun tv : list val => and (eval_exprlist tge (Vptr sp Ptrofs.zero) te tm (@cons expr x x0) tv) (Val.inject_list f (@cons val v1 vl) tv)) *)
  intros [tv1 [EVAL1 VINJ1]].
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit transl_expr_correct. eauto. eauto. eexact H0. eauto.
(* Goal: forall _ : @ex (list val) (fun tv : list val => and (eval_exprlist tge (Vptr sp Ptrofs.zero) te tm x0 tv) (Val.inject_list f vl tv)), @ex (list val) (fun tv : list val => and (eval_exprlist tge (Vptr sp Ptrofs.zero) te tm (@cons expr x x0) tv) (Val.inject_list f (@cons val v1 vl) tv)) *)
  intros [tv2 [EVAL2 VINJ2]].
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit Mem.storev_mapped_inject; eauto. intros [tm' [STORE' MINJ']].
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  left; econstructor; split.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  apply plus_one. econstructor; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; eauto.
(* Goal: and (Z.le Z0 ofs) (Z.lt ofs sz) *)
(* Goal: padding_freeable f empty_env tm' sp (fn_stackspace tf) *)
(* Goal: match_callstack f m tm' cs (Mem.nextblock m) sp *)
  inv VINJ1; simpl in H1; try discriminate. unfold Mem.storev in STORE'.
  rewrite (Mem.nextblock_store _ _ _ _ _ _ H1).
  rewrite (Mem.nextblock_store _ _ _ _ _ _ STORE').
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply match_callstack_invariant with f0 m tm; eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. eapply Mem.perm_store_2; eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. eapply Mem.perm_store_1; eauto.

(* call *)
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  simpl in H1. exploit functions_translated; eauto. intros [tfd [FIND TRANS]].
  monadInv TR.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit transl_expr_correct; eauto. intros [tvf [EVAL1 VINJ1]].
  assert (tvf = vf).
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
    exploit match_callstack_match_globalenvs; eauto. intros [bnd MG].
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
    eapply val_inject_function_pointer; eauto.
  subst tvf.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit transl_exprlist_correct; eauto.
  intros [tvargs [EVAL2 VINJ2]].
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  left; econstructor; split.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  apply plus_one. eapply step_call; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  apply sig_preserved; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply match_Kcall with (cenv' := cenv); eauto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  red; auto.

(* builtin *)
  monadInv TR.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit transl_exprlist_correct; eauto.
  intros [tvargs [EVAL2 VINJ2]].
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit match_callstack_match_globalenvs; eauto. intros [hi' MG].
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit external_call_mem_inject; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply inj_preserves_globals; eauto.
  intros [f' [vres' [tm' [EC [VINJ [MINJ' [UNMAPPED [OUTOFREACH [INCR SEPARATED]]]]]]]]].
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  left; econstructor; split.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  apply plus_one. econstructor. eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
  assert (MCS': match_callstack f' m' tm'
                 (Frame cenv tfn e le te sp lo hi :: cs)
                 (Mem.nextblock m') (Mem.nextblock tm')).
    apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm).
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
    eapply match_callstack_external_call; eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
    intros. eapply external_call_max_perm; eauto.
(* Goal: Ple (Mem.nextblock m) (Mem.nextblock m) *)
(* Goal: and (Ple (Mem.nextblock m) b) (Plt b (Mem.nextblock m)) *)
(* Goal: @ex positive (fun id : positive => @ex Z (fun sz : Z => @eq (option (prod block Z)) (@PTree.get (prod block Z) id empty_env) (@Some (prod block Z) (@pair block Z b sz)))) *)
(* Goal: Plt tb sp *)
(* Goal: match_bounds empty_env m *)
(* Goal: padding_freeable f empty_env tm' sp (fn_stackspace tf) *)
(* Goal: match_callstack f m tm' cs (Mem.nextblock m) sp *)
    xomega. xomega.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
    eapply external_call_nextblock; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
    eapply external_call_nextblock; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; eauto.
Opaque PTree.set.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  unfold set_optvar. destruct optid; simpl.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply match_callstack_set_temp; eauto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  auto.

(* seq *)
  monadInv TR.
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  left; econstructor; split.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
  apply plus_one. constructor.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; eauto.
(* seq 2 *)
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  right. split. auto. split. auto. econstructor; eauto.

(* ifthenelse *)
  monadInv TR.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]].
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  left; exists (State tfn (if b then x0 else x1) tk (Vptr sp Ptrofs.zero) te tm); split.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  apply plus_one. eapply step_ifthenelse; eauto. eapply bool_of_val_inject; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; eauto. destruct b; auto.

(* loop *)
  monadInv TR.
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  left; econstructor; split.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
  apply plus_one. constructor.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; eauto.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  econstructor; eauto. simpl. rewrite EQ; auto.

(* block *)
  monadInv TR.
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  left; econstructor; split.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
  apply plus_one. constructor.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; eauto.

(* exit seq *)
(* Goal: or (Z.le (Z.add ofs1 sz0) (align sz1 (block_alignment sz))) (Z.le (Z.add (align sz1 (block_alignment sz)) sz) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
  monadInv TR. left.
  dependent induction MK.
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  econstructor; split.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
  apply plus_one. constructor.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  econstructor; eauto. simpl. auto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit IHMK; eauto. intros [T2 [A B]].
(* Goal: or (Z.le (Z.add ofs1 sz0) (align sz1 (block_alignment sz))) (Z.le (Z.add (align sz1 (block_alignment sz)) sz) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
  exists T2; split; auto. eapply plus_left. constructor. apply plus_star; eauto. traceEq.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit IHMK; eauto. intros [T2 [A B]].
(* Goal: or (Z.le (Z.add ofs1 sz0) (align sz1 (block_alignment sz))) (Z.le (Z.add (align sz1 (block_alignment sz)) sz) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
  exists T2; split; auto. eapply plus_left.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  simpl. constructor. apply plus_star; eauto. traceEq.

(* exit block 0 *)
(* Goal: or (Z.le (Z.add ofs1 sz0) (align sz1 (block_alignment sz))) (Z.le (Z.add (align sz1 (block_alignment sz)) sz) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
  monadInv TR. left.
  dependent induction MK.
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  econstructor; split.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  simpl. apply plus_one. constructor.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit IHMK; eauto. intros [T2 [A B]].
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  exists T2; split; auto. simpl.
(* Goal: or (Z.le (Z.add ofs1 sz0) (align sz1 (block_alignment sz))) (Z.le (Z.add (align sz1 (block_alignment sz)) sz) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
  eapply plus_left. constructor. apply plus_star; eauto. traceEq.

(* exit block n+1 *)
(* Goal: or (Z.le (Z.add ofs1 sz0) (align sz1 (block_alignment sz))) (Z.le (Z.add (align sz1 (block_alignment sz)) sz) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
  monadInv TR. left.
  dependent induction MK.
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  econstructor; split.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  simpl. apply plus_one. constructor.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; eauto. auto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit IHMK; eauto. intros [T2 [A B]].
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  exists T2; split; auto. simpl.
(* Goal: or (Z.le (Z.add ofs1 sz0) (align sz1 (block_alignment sz))) (Z.le (Z.add (align sz1 (block_alignment sz)) sz) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
  eapply plus_left. constructor. apply plus_star; eauto. traceEq.

(* switch *)
  simpl in TR. destruct (switch_table cases O) as [tbl dfl] eqn:STBL. monadInv TR.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]].
  assert (SA: switch_argument islong tv n).
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
  { inv H0; inv VINJ; constructor. }
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit switch_descent; eauto. intros [k1 [A B]].
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit switch_ascent; eauto. eapply (switch_table_select n).
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  rewrite STBL; simpl. intros [k2 [C D]].
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit transl_lblstmt_suffix; eauto. eapply (switch_table_select n).
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  simpl. intros [body' [ts' E]].
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit switch_match_states; eauto. intros [T2 [F G]].
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  left; exists T2; split.
  eapply plus_star_trans. eapply B.
(* Goal: or (Z.le (Z.add ofs1 sz0) (align sz1 (block_alignment sz))) (Z.le (Z.add (align sz1 (block_alignment sz)) sz) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
  eapply star_left. econstructor; eauto.
  eapply star_trans. eexact C.
  apply plus_star. eexact F.
(* Goal: @eq val (Vptr b2 (Ptrofs.add Ptrofs.zero (Ptrofs.repr Z0))) (Vptr b2 Ptrofs.zero) *)
  reflexivity. reflexivity. traceEq.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  auto.

(* return none *)
(* Goal: or (Z.le (Z.add ofs1 sz0) (align sz1 (block_alignment sz))) (Z.le (Z.add (align sz1 (block_alignment sz)) sz) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
  monadInv TR. left.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit match_callstack_freelist; eauto. intros [tm' [A [B C]]].
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  econstructor; split.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  apply plus_one. eapply step_return_0. eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; eauto. eapply match_call_cont; eauto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  simpl; auto.

(* return some *)
(* Goal: or (Z.le (Z.add ofs1 sz0) (align sz1 (block_alignment sz))) (Z.le (Z.add (align sz1 (block_alignment sz)) sz) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
(* Goal: or (Z.le (Z.add ofs1 sz0) ofs2) (Z.le (Z.add ofs2 sz2) ofs1) *)
  monadInv TR. left.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]].
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit match_callstack_freelist; eauto. intros [tm' [A [B C]]].
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  econstructor; split.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  apply plus_one. eapply step_return_1. eauto. eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; eauto. eapply match_call_cont; eauto.

(* label *)
  monadInv TR.
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  left; econstructor; split.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
  apply plus_one. constructor.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; eauto.

(* goto *)
  monadInv TR.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit transl_find_label_body; eauto.
  intros [ts' [tk' [xenv' [A [B C]]]]].
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  left; econstructor; split.
  apply plus_one. apply step_goto. eexact A.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; eauto.

(* internal call *)
(* Goal: forall _ : @eq (res fundef) (@bind function (AST.fundef function) (transl_function f) (fun f' : function => @OK (AST.fundef function) (@Internal function f'))) (@OK fundef tf), @eq signature (funsig tf) (Csharpminor.fn_sig f) *)
(* Goal: forall _ : @eq (res fundef) (@OK (AST.fundef function) (@External function e)) (@OK fundef tf), @eq signature (funsig tf) (ef_sig e) *)
  monadInv TR. generalize EQ; clear EQ; unfold transl_function.
  caseEq (build_compilenv f). intros ce sz BC.
(* Goal: lbl_stmt_tail sl (@snd (list (prod Z nat)) nat (switch_table sl O)) (select_switch_default sl) *)
  destruct (zle sz Ptrofs.max_unsigned); try congruence.
  intro TRBODY.
  generalize TRBODY; intro TMP. monadInv TMP.
  set (tf := mkfunction (Csharpminor.fn_sig f)
                        (Csharpminor.fn_params f)
                        (Csharpminor.fn_temps f)
                        sz
                        x0) in *.
  caseEq (Mem.alloc tm 0 (fn_stackspace tf)). intros tm' sp ALLOC'.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit match_callstack_function_entry; eauto. simpl; eauto. simpl; auto.
  intros [f2 [MCS2 MINJ2]].
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  left; econstructor; split.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  apply plus_one. constructor; simpl; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor. eexact TRBODY. eauto. eexact MINJ2. eexact MCS2.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  inv MK; simpl in ISCC; contradiction || econstructor; eauto.

(* external call *)
  monadInv TR.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit match_callstack_match_globalenvs; eauto. intros [hi MG].
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit external_call_mem_inject; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply inj_preserves_globals; eauto.
  intros [f' [vres' [tm' [EC [VINJ [MINJ' [UNMAPPED [OUTOFREACH [INCR SEPARATED]]]]]]]]].
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  left; econstructor; split.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
  apply plus_one. econstructor.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  econstructor; eauto.
  apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm).
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply match_callstack_external_call; eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. eapply external_call_max_perm; eauto.
(* Goal: Ple (Mem.nextblock m) (Mem.nextblock m) *)
(* Goal: and (Ple (Mem.nextblock m) b) (Plt b (Mem.nextblock m)) *)
(* Goal: @ex positive (fun id : positive => @ex Z (fun sz : Z => @eq (option (prod block Z)) (@PTree.get (prod block Z) id empty_env) (@Some (prod block Z) (@pair block Z b sz)))) *)
(* Goal: Plt tb sp *)
(* Goal: match_bounds empty_env m *)
(* Goal: padding_freeable f empty_env tm' sp (fn_stackspace tf) *)
(* Goal: match_callstack f m tm' cs (Mem.nextblock m) sp *)
  xomega. xomega.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply external_call_nextblock; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply external_call_nextblock; eauto.

(* return *)
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  inv MK. simpl.
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  left; econstructor; split.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  apply plus_one. econstructor; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  unfold set_optvar. destruct optid; simpl; econstructor; eauto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply match_callstack_set_temp; eauto.
Qed.

Lemma match_globalenvs_init:
  forall m,
  Genv.init_mem prog = Some m ->
  match_globalenvs (Mem.flat_inj (Mem.nextblock m)) (Mem.nextblock m).
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. constructor.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. unfold Mem.flat_inj. apply pred_dec_true; auto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. unfold Mem.flat_inj in H0.
(* Goal: lbl_stmt_tail sl (@snd (list (prod Z nat)) nat (switch_table sl O)) (select_switch_default sl) *)
  destruct (plt b1 (Mem.nextblock m)); congruence.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. eapply Genv.find_symbol_not_fresh; eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. eapply Genv.find_funct_ptr_not_fresh; eauto.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. eapply Genv.find_var_info_not_fresh; eauto.
Qed.

Lemma transl_initial_states:
  forall S, Csharpminor.initial_state prog S ->
  exists R, Cminor.initial_state tprog R /\ match_states S R.
Proof.
  induction 1.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  exploit function_ptr_translated; eauto. intros [tf [FIND TR]].
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
(* Goal: and (or (@eq positive a id) (@In positive id temps)) (@eq val v Vundef) *)
  econstructor; split.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
  econstructor.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  apply (Genv.init_mem_transf_partial TRANSL). eauto.
(* Goal: @eq (option (prod stmt cont)) (find_label lbl (Sseq (Sblock body) ts0) k') (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  simpl. fold tge. rewrite symbols_preserved.
  replace (prog_main tprog) with (prog_main prog). eexact H0.
  symmetry. unfold transl_program in TRANSL.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply match_program_main; eauto. 
  eexact FIND.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  rewrite <- H2. apply sig_preserved; auto.
  eapply match_callstate with (f := Mem.flat_inj (Mem.nextblock m0)) (cs := @nil frame) (cenv := PTree.empty Z).
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  auto.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply Genv.initmem_inject; eauto.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  apply mcs_nil with (Mem.nextblock m0). apply match_globalenvs_init; auto. xomega. xomega.
(* Goal: @eq (option (prod stmt cont)) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) (@Some (prod stmt cont) (@pair stmt cont ts' tk')) *)
  constructor. red; auto.
(* Goal: final_state (Returnstate (Vint r) Kstop tm) r *)
  constructor.
Qed.

Lemma transl_final_states:
  forall S R r,
  match_states S R -> Csharpminor.final_state S r -> Cminor.final_state R r.
Proof.
(* Goal: forall (S : Csharpminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Csharpminor.final_state S r), final_state R r *)
  intros. inv H0. inv H. inv MK. inv RESINJ. constructor.
Qed.

Theorem transl_program_correct:
  forward_simulation (Csharpminor.semantics prog) (Cminor.semantics tprog).
Proof.
(* Goal: @ex stmt (fun body' : stmt => @ex stmt (fun ts' : stmt => @eq (res stmt) (transl_lblstmt cenv (switch_env sl' xenv) sl' body') (@OK stmt ts'))) *)
  eapply forward_simulation_star; eauto.
  apply senv_preserved.
  eexact transl_initial_states.
  eexact transl_final_states.
  eexact transl_step_correct.
Qed.

End TRANSLATION.

