(* *********************************************************************)
(*                                                                     *)
(*              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.     *)
(*                                                                     *)
(* *********************************************************************)

(** Animating the CompCert C semantics *)

Require Import FunInd.
Require Import Axioms Classical.
Require Import String Coqlib Decidableplus.
Require Import Errors Maps Integers Floats.
Require Import AST Values Memory Events Globalenvs Determinism.
Require Import Ctypes Cop Csyntax Csem.
Require Cstrategy.

Local Open Scope string_scope.
Local Open Scope list_scope.

(** Error monad with options or lists *)

Notation "'do' X <- A ; B" := (match A with Some X => B | None => None end)
  (at level 200, X ident, A at level 100, B at level 200)
  : option_monad_scope.

Notation "'do' X , Y <- A ; B" := (match A with Some (X, Y) => B | None => None end)
  (at level 200, X ident, Y ident, A at level 100, B at level 200)
  : option_monad_scope.

Notation "'do' X , Y , Z <- A ; B" := (match A with Some (X, Y, Z) => B | None => None end)
  (at level 200, X ident, Y ident, Z ident, A at level 100, B at level 200)
  : option_monad_scope.

Notation " 'check' A ; B" := (if A then B else None)
  (at level 200, A at level 100, B at level 200)
  : option_monad_scope.

Notation "'do' X <- A ; B" := (match A with Some X => B | None => nil end)
  (at level 200, X ident, A at level 100, B at level 200)
  : list_monad_scope.

Notation " 'check' A ; B" := (if A then B else nil)
  (at level 200, A at level 100, B at level 200)
  : list_monad_scope.

Definition is_val (a: expr) : option (val * type) :=
  match a with
  | Eval v ty => Some(v, ty)
  | _ => None
  end.

Lemma is_val_inv:
  forall a v ty, is_val a = Some(v, ty) -> a = Eval v ty.
Proof.
(* Goal: forall (a : expr) (b : block) (ofs : Ptrofs.int) (ty : type) (_ : @eq (option (prod (prod block Ptrofs.int) type)) (is_loc a) (@Some (prod (prod block Ptrofs.int) type) (@pair (prod block Ptrofs.int) type (@pair block Ptrofs.int b ofs) ty))), @eq expr a (Eloc b ofs ty) *)
  intros until ty. destruct a; simpl; congruence.
Qed.

Definition is_loc (a: expr) : option (block * ptrofs * type) :=
  match a with
  | Eloc b ofs ty => Some(b, ofs, ty)
  | _ => None
  end.

Lemma is_loc_inv:
  forall a b ofs ty, is_loc a = Some(b, ofs, ty) -> a = Eloc b ofs ty.
Proof.
(* Goal: forall (a : expr) (b : block) (ofs : Ptrofs.int) (ty : type) (_ : @eq (option (prod (prod block Ptrofs.int) type)) (is_loc a) (@Some (prod (prod block Ptrofs.int) type) (@pair (prod block Ptrofs.int) type (@pair block Ptrofs.int b ofs) ty))), @eq expr a (Eloc b ofs ty) *)
  intros until ty. destruct a; simpl; congruence.
Qed.

Local Open Scope option_monad_scope.

Fixpoint is_val_list (al: exprlist) : option (list (val * type)) :=
  match al with
  | Enil => Some nil
  | Econs a1 al => do vt1 <- is_val a1; do vtl <- is_val_list al; Some(vt1::vtl)
  end.

Definition is_skip (s: statement) : {s = Sskip} + {s <> Sskip}.
Proof.
(* Goal: sumbool (@eq statement s Sskip) (not (@eq statement s Sskip)) *)
  destruct s; (left; congruence) || (right; congruence).
Defined.

(** * Events, volatile memory accesses, and external functions. *)

Section EXEC.

Variable ge: genv.

Definition eventval_of_val (v: val) (t: typ) : option eventval :=
  match v with
  | Vint i => check (typ_eq t AST.Tint); Some (EVint i)
  | Vfloat f => check (typ_eq t AST.Tfloat); Some (EVfloat f)
  | Vsingle f => check (typ_eq t AST.Tsingle); Some (EVsingle f)
  | Vlong n => check (typ_eq t AST.Tlong); Some (EVlong n)
  | Vptr b ofs =>
      do id <- Genv.invert_symbol ge b;
      check (Genv.public_symbol ge id);
      check (typ_eq t AST.Tptr);
      Some (EVptr_global id ofs)
  | _ => None
  end.

Fixpoint list_eventval_of_val (vl: list val) (tl: list typ) : option (list eventval) :=
  match vl, tl with
  | nil, nil => Some nil
  | v1::vl, t1::tl =>
      do ev1 <- eventval_of_val v1 t1;
      do evl <- list_eventval_of_val vl tl;
      Some (ev1 :: evl)
  | _, _ => None
  end.

Definition val_of_eventval (ev: eventval) (t: typ) : option val :=
  match ev with
  | EVint i => check (typ_eq t AST.Tint); Some (Vint i)
  | EVfloat f => check (typ_eq t AST.Tfloat); Some (Vfloat f)
  | EVsingle f => check (typ_eq t AST.Tsingle); Some (Vsingle f)
  | EVlong n => check (typ_eq t AST.Tlong); Some (Vlong n)
  | EVptr_global id ofs =>
      check (Genv.public_symbol ge id);
      check (typ_eq t AST.Tptr);
      do b <- Genv.find_symbol ge id;
      Some (Vptr b ofs)
  end.

Ltac mydestr :=
  match goal with
  | [ |- None = Some _ -> _ ] => let X := fresh "X" in intro X; discriminate
  | [ |- Some _ = Some _ -> _ ] => let X := fresh "X" in intro X; inv X
  | [ |- match ?x with Some _ => _ | None => _ end = Some _ -> _ ] => destruct x eqn:?; mydestr
  | [ |- match ?x with true => _ | false => _ end = Some _ -> _ ] => destruct x eqn:?; mydestr
  | [ |- match ?x with left _ => _ | right _ => _ end = Some _ -> _ ] => destruct x; mydestr
  | _ => idtac
  end.

Lemma eventval_of_val_sound:
  forall v t ev, eventval_of_val v t = Some ev -> eventval_match ge ev t v.
Proof.
(* Goal: forall (v : val) (t : typ) (ev : eventval) (_ : @eq (option eventval) (eventval_of_val v t) (@Some eventval ev)), eventval_match (@Genv.to_senv fundef type (genv_genv ge)) ev t v *)
  intros until ev. destruct v; simpl; mydestr; constructor.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  auto. apply Genv.invert_find_symbol; auto.
Qed.

Lemma eventval_of_val_complete:
  forall ev t v, eventval_match ge ev t v -> eventval_of_val v t = Some ev.
Proof.
(* Goal: forall (e1 : env) (m1 : Mem.mem) (l : list (prod ident type)) (e2 : env) (m2 : Mem.mem) (_ : alloc_variables ge e1 m1 l e2 m2), @eq (prod env Mem.mem) (do_alloc_variables e1 m1 l) (@pair env Mem.mem e2 m2) *)
  induction 1; simpl.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
- auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
- auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
- auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
- auto.
- rewrite (Genv.find_invert_symbol _ _ H0). simpl in H; rewrite H.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  rewrite dec_eq_true. auto. 
Qed.

Lemma list_eventval_of_val_sound:
  forall vl tl evl, list_eventval_of_val vl tl = Some evl -> eventval_list_match ge evl tl vl.
Proof with try discriminate.
  induction vl; destruct tl; simpl; intros; inv H.
(* Goal: imm_safe ge e RV (Eval v ty) m *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  constructor.
  destruct (eventval_of_val a t) as [ev1|] eqn:?...
  destruct (list_eventval_of_val vl tl) as [evl'|] eqn:?...
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  inv H1. constructor. apply eventval_of_val_sound; auto. eauto.
Qed.

Lemma list_eventval_of_val_complete:
  forall evl tl vl, eventval_list_match ge evl tl vl -> list_eventval_of_val vl tl = Some evl.
Proof.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  induction 1; simpl. auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  rewrite (eventval_of_val_complete _ _ _ H). rewrite IHeventval_list_match. auto.
Qed.

Lemma val_of_eventval_sound:
  forall ev t v, val_of_eventval ev t = Some v -> eventval_match ge ev t v.
Proof.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  intros until v. destruct ev; simpl; mydestr; constructor; auto.
Qed.

Lemma val_of_eventval_complete:
  forall ev t v, eventval_match ge ev t v -> val_of_eventval ev t = Some v.
Proof.
(* Goal: forall (e1 : env) (m1 : Mem.mem) (l : list (prod ident type)) (e2 : env) (m2 : Mem.mem) (_ : alloc_variables ge e1 m1 l e2 m2), @eq (prod env Mem.mem) (do_alloc_variables e1 m1 l) (@pair env Mem.mem e2 m2) *)
  induction 1; simpl.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
- auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
- auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
- auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
- auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
- simpl in *. rewrite H, H0. rewrite dec_eq_true. auto.  
Qed.

(** Volatile memory accesses. *)

Definition do_volatile_load (w: world) (chunk: memory_chunk) (m: mem) (b: block) (ofs: ptrofs)
                             : option (world * trace * val) :=
  if Genv.block_is_volatile ge b then
    do id <- Genv.invert_symbol ge b;
    match nextworld_vload w chunk id ofs with
    | None => None
    | Some(res, w') =>
        do vres <- val_of_eventval res (type_of_chunk chunk);
        Some(w', Event_vload chunk id ofs res :: nil, Val.load_result chunk vres)
    end
  else
    do v <- Mem.load chunk m b (Ptrofs.unsigned ofs);
    Some(w, E0, v).

Definition do_volatile_store (w: world) (chunk: memory_chunk) (m: mem) (b: block) (ofs: ptrofs) (v: val)
                             : option (world * trace * mem) :=
  if Genv.block_is_volatile ge b then
    do id <- Genv.invert_symbol ge b;
    do ev <- eventval_of_val (Val.load_result chunk v) (type_of_chunk chunk);
    do w' <- nextworld_vstore w chunk id ofs ev;
    Some(w', Event_vstore chunk id ofs ev :: nil, m)
  else
    do m' <- Mem.store chunk m b (Ptrofs.unsigned ofs) v;
    Some(w, E0, m').

Lemma do_volatile_load_sound:
  forall w chunk m b ofs w' t v,
  do_volatile_load w chunk m b ofs = Some(w', t, v) ->
  volatile_load ge chunk m b ofs t v /\ possible_trace w t w'.
Proof.
(* Goal: forall (ev : eventval) (t : typ) (v : val) (_ : @eq (option val) (val_of_eventval ev t) (@Some val v)), eventval_match (@Genv.to_senv fundef type (genv_genv ge)) ev t v *)
  intros until v. unfold do_volatile_load. mydestr.
  destruct p as [ev w'']. mydestr.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  split. constructor; auto. apply Genv.invert_find_symbol; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply val_of_eventval_sound; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  econstructor. constructor; eauto. constructor.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  split. constructor; auto. constructor.
Qed.

Lemma do_volatile_load_complete:
  forall w chunk m b ofs w' t v,
  volatile_load ge chunk m b ofs t v -> possible_trace w t w' ->
  do_volatile_load w chunk m b ofs = Some(w', t, v).
Proof.
(* Goal: @eq (option val) (if @Genv.public_symbol fundef type (genv_genv ge) id then if typ_eq Tptr Tptr then match @Genv.find_symbol fundef type (genv_genv ge) id with | Some b => @Some val (Vptr b ofs) | None => @None val end else @None val else @None val) (@Some val (Vptr b ofs)) *)
  unfold do_volatile_load; intros. inv H; simpl in *.
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) match Mem.load Mptr m b (Z.sub (Ptrofs.unsigned lo) (size_chunk Mptr)) with | Some vsz => match do_alloc_size vsz with | Some sz => if zlt Z0 (Ptrofs.unsigned sz) then match Mem.free m b (Z.sub (Ptrofs.unsigned lo) (size_chunk Mptr)) (Z.add (Ptrofs.unsigned lo) (Ptrofs.unsigned sz)) with | Some m' => @Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' E0) Vundef) m') | None => @None (prod (prod (prod world trace) val) Mem.mem) end else @None (prod (prod (prod world trace) val) Mem.mem) | None => @None (prod (prod (prod world trace) val) Mem.mem) end | None => @None (prod (prod (prod world trace) val) Mem.mem) end (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' E0) Vundef) m')) *)
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_ef_memcpy sz al w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_ef_annot text targs w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_ef_annot_val text targ w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_inline_assembly text sg (@Genv.to_senv fundef type (genv_genv ge)) w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_ef_debug kind text targs w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
  rewrite H1. rewrite (Genv.find_invert_symbol _ _ H2). inv H0. inv H8. inv H6. rewrite H9.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  rewrite (val_of_eventval_complete _ _ _ H3). auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  rewrite H1. rewrite H2. inv H0. auto.
Qed.

Lemma do_volatile_store_sound:
  forall w chunk m b ofs v w' t m',
  do_volatile_store w chunk m b ofs v = Some(w', t, m') ->
  volatile_store ge chunk m b ofs v t m' /\ possible_trace w t w'.
Proof.
  intros until m'. unfold do_volatile_store. mydestr.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  split. constructor; auto. apply Genv.invert_find_symbol; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply eventval_of_val_sound; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  econstructor. constructor; eauto. constructor.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  split. constructor; auto. constructor.
Qed.

Lemma do_volatile_store_complete:
  forall w chunk m b ofs v w' t m',
  volatile_store ge chunk m b ofs v t m' -> possible_trace w t w' ->
  do_volatile_store w chunk m b ofs v = Some(w', t, m').
Proof.
(* Goal: @eq (option val) (if @Genv.public_symbol fundef type (genv_genv ge) id then if typ_eq Tptr Tptr then match @Genv.find_symbol fundef type (genv_genv ge) id with | Some b => @Some val (Vptr b ofs) | None => @None val end else @None val else @None val) (@Some val (Vptr b ofs)) *)
  unfold do_volatile_store; intros. inv H; simpl in *.
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) match Mem.load Mptr m b (Z.sub (Ptrofs.unsigned lo) (size_chunk Mptr)) with | Some vsz => match do_alloc_size vsz with | Some sz => if zlt Z0 (Ptrofs.unsigned sz) then match Mem.free m b (Z.sub (Ptrofs.unsigned lo) (size_chunk Mptr)) (Z.add (Ptrofs.unsigned lo) (Ptrofs.unsigned sz)) with | Some m' => @Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' E0) Vundef) m') | None => @None (prod (prod (prod world trace) val) Mem.mem) end else @None (prod (prod (prod world trace) val) Mem.mem) | None => @None (prod (prod (prod world trace) val) Mem.mem) end | None => @None (prod (prod (prod world trace) val) Mem.mem) end (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' E0) Vundef) m')) *)
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_ef_memcpy sz al w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_ef_annot text targs w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_ef_annot_val text targ w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_inline_assembly text sg (@Genv.to_senv fundef type (genv_genv ge)) w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_ef_debug kind text targs w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
  rewrite H1. rewrite (Genv.find_invert_symbol _ _ H2).
(* Goal: @eq (option (prod (prod world trace) Mem.mem)) match eventval_of_val (Val.load_result chunk v) (type_of_chunk chunk) with | Some ev => match nextworld_vstore w chunk id ofs ev with | Some w' => @Some (prod (prod world (list event)) Mem.mem) (@pair (prod world (list event)) Mem.mem (@pair world (list event) w' (@cons event (Event_vstore chunk id ofs ev) (@nil event))) m') | None => @None (prod (prod world trace) Mem.mem) end | None => @None (prod (prod world trace) Mem.mem) end (@Some (prod (prod world trace) Mem.mem) (@pair (prod world trace) Mem.mem (@pair world trace w' (@cons event (Event_vstore chunk id ofs ev) (@nil event))) m')) *)
(* Goal: @eq (option (prod (prod world trace) Mem.mem)) (if @Genv.block_is_volatile fundef type (genv_genv ge) b then match @Genv.invert_symbol fundef type (genv_genv ge) b with | Some id => match eventval_of_val (Val.load_result chunk v) (type_of_chunk chunk) with | Some ev => match nextworld_vstore w chunk id ofs ev with | Some w' => @Some (prod (prod world (list event)) Mem.mem) (@pair (prod world (list event)) Mem.mem (@pair world (list event) w' (@cons event (Event_vstore chunk id ofs ev) (@nil event))) m) | None => @None (prod (prod world trace) Mem.mem) end | None => @None (prod (prod world trace) Mem.mem) end | None => @None (prod (prod world trace) Mem.mem) end else match Mem.store chunk m b (Ptrofs.unsigned ofs) v with | Some m' => @Some (prod (prod world trace) Mem.mem) (@pair (prod world trace) Mem.mem (@pair world trace w E0) m') | None => @None (prod (prod world trace) Mem.mem) end) (@Some (prod (prod world trace) Mem.mem) (@pair (prod world trace) Mem.mem (@pair world trace w' E0) m')) *)
  rewrite (eventval_of_val_complete _ _ _ H3).
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  inv H0. inv H8. inv H6. rewrite H9. auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  rewrite H1. rewrite H2. inv H0. auto.
Qed.

(** Accessing locations *)

Definition do_deref_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: ptrofs) : option (world * trace * val) :=
  match access_mode ty with
  | By_value chunk =>
      match type_is_volatile ty with
      | false => do v <- Mem.loadv chunk m (Vptr b ofs); Some(w, E0, v)
      | true => do_volatile_load w chunk m b ofs
      end
  | By_reference => Some(w, E0, Vptr b ofs)
  | By_copy => Some(w, E0, Vptr b ofs)
  | _ => None
  end.

Definition assign_copy_ok (ty: type) (b: block) (ofs: ptrofs) (b': block) (ofs': ptrofs) : Prop :=
  (alignof_blockcopy ge ty | Ptrofs.unsigned ofs') /\ (alignof_blockcopy ge ty | Ptrofs.unsigned ofs) /\
  (b' <> b \/ Ptrofs.unsigned ofs' = Ptrofs.unsigned ofs
           \/ Ptrofs.unsigned ofs' + sizeof ge ty <= Ptrofs.unsigned ofs
           \/ Ptrofs.unsigned ofs + sizeof ge ty <= Ptrofs.unsigned ofs').

Remark check_assign_copy:
  forall (ty: type) (b: block) (ofs: ptrofs) (b': block) (ofs': ptrofs),
(* Goal: forall n : Ptrofs.int, @eq (option Ptrofs.int) (do_alloc_size (Vptrofs n)) (@Some Ptrofs.int n) *)
(* Goal: forall (ef : external_function) (w : world) (vargs : list val) (m : Mem.mem) (w' : world) (t : trace) (vres : val) (m' : Mem.mem) (_ : external_call ef (@Genv.to_senv fundef type (genv_genv ge)) vargs m t vres m') (_ : possible_trace w t w'), @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_external ef w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
  { assign_copy_ok ty b ofs b' ofs' } + {~ assign_copy_ok ty b ofs b' ofs' }.
Proof with try (right; intuition omega).
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  intros. unfold assign_copy_ok.
  assert (alignof_blockcopy ge ty > 0) by apply alignof_blockcopy_pos.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (Zdivide_dec (alignof_blockcopy ge ty) (Ptrofs.unsigned ofs')); auto...
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (Zdivide_dec (alignof_blockcopy ge ty) (Ptrofs.unsigned ofs)); auto...
(* Goal: forall n : Ptrofs.int, @eq (option Ptrofs.int) (do_alloc_size (Vptrofs n)) (@Some Ptrofs.int n) *)
(* Goal: forall (ef : external_function) (w : world) (vargs : list val) (m : Mem.mem) (w' : world) (t : trace) (vres : val) (m' : Mem.mem) (_ : external_call ef (@Genv.to_senv fundef type (genv_genv ge)) vargs m t vres m') (_ : possible_trace w t w'), @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_external ef w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
  assert (Y: {b' <> b \/
              Ptrofs.unsigned ofs' = Ptrofs.unsigned ofs \/
              Ptrofs.unsigned ofs' + sizeof ge ty <= Ptrofs.unsigned ofs \/
              Ptrofs.unsigned ofs + sizeof ge ty <= Ptrofs.unsigned ofs'} +
(* Goal: forall n : Ptrofs.int, @eq (option Ptrofs.int) (do_alloc_size (Vptrofs n)) (@Some Ptrofs.int n) *)
(* Goal: forall (ef : external_function) (w : world) (vargs : list val) (m : Mem.mem) (w' : world) (t : trace) (vres : val) (m' : Mem.mem) (_ : external_call ef (@Genv.to_senv fundef type (genv_genv ge)) vargs m t vres m') (_ : possible_trace w t w'), @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_external ef w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
           {~(b' <> b \/
              Ptrofs.unsigned ofs' = Ptrofs.unsigned ofs \/
              Ptrofs.unsigned ofs' + sizeof ge ty <= Ptrofs.unsigned ofs \/
              Ptrofs.unsigned ofs + sizeof ge ty <= Ptrofs.unsigned ofs')}).
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (eq_block b' b); auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (zeq (Ptrofs.unsigned ofs') (Ptrofs.unsigned ofs)); auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (zle (Ptrofs.unsigned ofs' + sizeof ge ty) (Ptrofs.unsigned ofs)); auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (zle (Ptrofs.unsigned ofs + sizeof ge ty) (Ptrofs.unsigned ofs')); auto.
  right; intuition omega.
  destruct Y... left; intuition omega.
Defined.

Definition do_assign_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: ptrofs) (v: val): option (world * trace * mem) :=
  match access_mode ty with
  | By_value chunk =>
      match type_is_volatile ty with
      | false => do m' <- Mem.storev chunk m (Vptr b ofs) v; Some(w, E0, m')
      | true => do_volatile_store w chunk m b ofs v
      end
  | By_copy =>
      match v with
      | Vptr b' ofs' =>
          if check_assign_copy ty b ofs b' ofs' then
            do bytes <- Mem.loadbytes m b' (Ptrofs.unsigned ofs') (sizeof ge ty);
            do m' <- Mem.storebytes m b (Ptrofs.unsigned ofs) bytes;
            Some(w, E0, m')
          else None
      | _ => None
      end
  | _ => None
  end.

Lemma do_deref_loc_sound:
  forall w ty m b ofs w' t v,
  do_deref_loc w ty m b ofs = Some(w', t, v) ->
  deref_loc ge ty m b ofs t v /\ possible_trace w t w'.
Proof.
(* Goal: forall (ev : eventval) (t : typ) (v : val) (_ : @eq (option val) (val_of_eventval ev t) (@Some val v)), eventval_match (@Genv.to_senv fundef type (genv_genv ge)) ev t v *)
  unfold do_deref_loc; intros until v.
  destruct (access_mode ty) eqn:?; mydestr.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  intros. exploit do_volatile_load_sound; eauto. intuition. eapply deref_loc_volatile; eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  split. eapply deref_loc_value; eauto. constructor.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  split. eapply deref_loc_reference; eauto. constructor.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  split. eapply deref_loc_copy; eauto. constructor.
Qed.

Lemma do_deref_loc_complete:
  forall w ty m b ofs w' t v,
  deref_loc ge ty m b ofs t v -> possible_trace w t w' ->
  do_deref_loc w ty m b ofs = Some(w', t, v).
Proof.
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  unfold do_deref_loc; intros. inv H.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  inv H0. rewrite H1; rewrite H2; rewrite H3; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  rewrite H1; rewrite H2. apply do_volatile_load_complete; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  inv H0. rewrite H1. auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  inv H0. rewrite H1. auto.
Qed.

Lemma do_assign_loc_sound:
  forall w ty m b ofs v w' t m',
  do_assign_loc w ty m b ofs v = Some(w', t, m') ->
  assign_loc ge ty m b ofs v t m' /\ possible_trace w t w'.
Proof.
  unfold do_assign_loc; intros until m'.
  destruct (access_mode ty) eqn:?; mydestr.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  intros. exploit do_volatile_store_sound; eauto. intuition. eapply assign_loc_volatile; eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  split. eapply assign_loc_value; eauto. constructor.
  destruct v; mydestr. destruct a as [P [Q R]].
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  split. eapply assign_loc_copy; eauto. constructor.
Qed.

Lemma do_assign_loc_complete:
  forall w ty m b ofs v w' t m',
  assign_loc ge ty m b ofs v t m' -> possible_trace w t w' ->
  do_assign_loc w ty m b ofs v = Some(w', t, m').
Proof.
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  unfold do_assign_loc; intros. inv H.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  inv H0. rewrite H1; rewrite H2; rewrite H3; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  rewrite H1; rewrite H2. apply do_volatile_store_complete; auto.
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) match Mem.load Mptr m b (Z.sub (Ptrofs.unsigned lo) (size_chunk Mptr)) with | Some vsz => match do_alloc_size vsz with | Some sz => if zlt Z0 (Ptrofs.unsigned sz) then match Mem.free m b (Z.sub (Ptrofs.unsigned lo) (size_chunk Mptr)) (Z.add (Ptrofs.unsigned lo) (Ptrofs.unsigned sz)) with | Some m' => @Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' E0) Vundef) m') | None => @None (prod (prod (prod world trace) val) Mem.mem) end else @None (prod (prod (prod world trace) val) Mem.mem) | None => @None (prod (prod (prod world trace) val) Mem.mem) end | None => @None (prod (prod (prod world trace) val) Mem.mem) end (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' E0) Vundef) m')) *)
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_ef_memcpy sz al w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_ef_annot text targs w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_ef_annot_val text targ w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_inline_assembly text sg (@Genv.to_senv fundef type (genv_genv ge)) w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_ef_debug kind text targs w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
  rewrite H1. destruct (check_assign_copy ty b ofs b' ofs').
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  inv H0. rewrite H5; rewrite H6; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  elim n. red; tauto.
Qed.

(** External calls *)

Variable do_external_function:
  string -> signature -> Senv.t -> world -> list val -> mem -> option (world * trace * val * mem).

Hypothesis do_external_function_sound:
  forall id sg ge vargs m t vres m' w w',
  do_external_function id sg ge w vargs m = Some(w', t, vres, m') ->
  external_functions_sem id sg ge vargs m t vres m' /\ possible_trace w t w'.

Hypothesis do_external_function_complete:
  forall id sg ge vargs m t vres m' w w',
  external_functions_sem id sg ge vargs m t vres m' ->
  possible_trace w t w' ->
  do_external_function id sg ge w vargs m = Some(w', t, vres, m').

Variable do_inline_assembly:
  string -> signature -> Senv.t -> world -> list val -> mem -> option (world * trace * val * mem).

Hypothesis do_inline_assembly_sound:
  forall txt sg ge vargs m t vres m' w w',
  do_inline_assembly txt sg ge w vargs m = Some(w', t, vres, m') ->
  inline_assembly_sem txt sg ge vargs m t vres m' /\ possible_trace w t w'.

Hypothesis do_inline_assembly_complete:
  forall txt sg ge vargs m t vres m' w w',
  inline_assembly_sem txt sg ge vargs m t vres m' ->
  possible_trace w t w' ->
  do_inline_assembly txt sg ge w vargs m = Some(w', t, vres, m').

Definition do_ef_volatile_load (chunk: memory_chunk)
       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
  match vargs with
  | Vptr b ofs :: nil => do w',t,v <- do_volatile_load w chunk m b ofs; Some(w',t,v,m)
  | _ => None
  end.

Definition do_ef_volatile_store (chunk: memory_chunk)
       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
  match vargs with
  | Vptr b ofs :: v :: nil => do w',t,m' <- do_volatile_store w chunk m b ofs v; Some(w',t,Vundef,m')
  | _ => None
  end.

Definition do_ef_volatile_load_global (chunk: memory_chunk) (id: ident) (ofs: ptrofs)
       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
  do b <- Genv.find_symbol ge id; do_ef_volatile_load chunk w (Vptr b ofs :: vargs) m.

Definition do_ef_volatile_store_global (chunk: memory_chunk) (id: ident) (ofs: ptrofs)
       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
  do b <- Genv.find_symbol ge id; do_ef_volatile_store chunk w (Vptr b ofs :: vargs) m.

Definition do_alloc_size (v: val) : option ptrofs :=
  match v with
  | Vint n => if Archi.ptr64 then None else Some (Ptrofs.of_int n)
  | Vlong n => if Archi.ptr64 then Some (Ptrofs.of_int64 n) else None
  | _ => None
  end.

Definition do_ef_malloc
       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
  match vargs with
  | v :: nil =>
      do sz <- do_alloc_size v;
      let (m', b) := Mem.alloc m (- size_chunk Mptr) (Ptrofs.unsigned sz) in
      do m'' <- Mem.store Mptr m' b (- size_chunk Mptr) v;
      Some(w, E0, Vptr b Ptrofs.zero, m'')
  | _ => None
  end.

Definition do_ef_free
       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
  match vargs with
  | Vptr b lo :: nil =>
      do vsz <- Mem.load Mptr m b (Ptrofs.unsigned lo - size_chunk Mptr);
      do sz <- do_alloc_size vsz;
      check (zlt 0 (Ptrofs.unsigned sz));
      do m' <- Mem.free m b (Ptrofs.unsigned lo - size_chunk Mptr) (Ptrofs.unsigned lo + Ptrofs.unsigned sz);
      Some(w, E0, Vundef, m')
  | _ => None
  end.

Definition memcpy_args_ok
  (sz al: Z) (bdst: block) (odst: Z) (bsrc: block) (osrc: Z) : Prop :=
      (al = 1 \/ al = 2 \/ al = 4 \/ al = 8)
   /\ sz >= 0 /\ (al | sz)
   /\ (sz > 0 -> (al | osrc))
   /\ (sz > 0 -> (al | odst))
   /\ (bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc).

Definition do_ef_memcpy (sz al: Z)
       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
  match vargs with
  | Vptr bdst odst :: Vptr bsrc osrc :: nil =>
      if decide (memcpy_args_ok sz al bdst (Ptrofs.unsigned odst) bsrc (Ptrofs.unsigned osrc)) then
        do bytes <- Mem.loadbytes m bsrc (Ptrofs.unsigned osrc) sz;
        do m' <- Mem.storebytes m bdst (Ptrofs.unsigned odst) bytes;
        Some(w, E0, Vundef, m')
      else None
  | _ => None
  end.

Definition do_ef_annot (text: string) (targs: list typ)
       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
  do args <- list_eventval_of_val vargs targs;
  Some(w, Event_annot text args :: E0, Vundef, m).

Definition do_ef_annot_val (text: string) (targ: typ)
       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
  match vargs with
  | varg :: nil =>
      do arg <- eventval_of_val varg targ;
      Some(w, Event_annot text (arg :: nil) :: E0, varg, m)
  | _ => None
  end.

Definition do_ef_debug (kind: positive) (text: ident) (targs: list typ)
       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
  Some(w, E0, Vundef, m).

Definition do_external (ef: external_function):
       world -> list val -> mem -> option (world * trace * val * mem) :=
  match ef with
  | EF_external name sg => do_external_function name sg ge
  | EF_builtin name sg => do_external_function name sg ge
  | EF_runtime name sg => do_external_function name sg ge
  | EF_vload chunk => do_ef_volatile_load chunk
  | EF_vstore chunk => do_ef_volatile_store chunk
  | EF_malloc => do_ef_malloc
  | EF_free => do_ef_free
  | EF_memcpy sz al => do_ef_memcpy sz al
  | EF_annot kind text targs => do_ef_annot text targs
  | EF_annot_val kind text targ => do_ef_annot_val text targ
  | EF_inline_asm text sg clob => do_inline_assembly text sg ge
  | EF_debug kind text targs => do_ef_debug kind text targs
  end.

Lemma do_ef_external_sound:
  forall ef w vargs m w' t vres m',
  do_external ef w vargs m = Some(w', t, vres, m') ->
  external_call ef ge vargs m t vres m' /\ possible_trace w t w'.
Proof with try congruence.
  assert (SIZE: forall v sz, do_alloc_size v = Some sz -> v = Vptrofs sz).
(* Goal: forall n : Ptrofs.int, @eq (option Ptrofs.int) (do_alloc_size (Vptrofs n)) (@Some Ptrofs.int n) *)
(* Goal: forall (ef : external_function) (w : world) (vargs : list val) (m : Mem.mem) (w' : world) (t : trace) (vres : val) (m' : Mem.mem) (_ : external_call ef (@Genv.to_senv fundef type (genv_genv ge)) vargs m t vres m') (_ : possible_trace w t w'), @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_external ef w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
  { intros until sz; unfold Vptrofs; destruct v; simpl; destruct Archi.ptr64 eqn:SF; 
    intros EQ; inv EQ; f_equal; symmetry; eauto with ptrofs. }
  intros until m'.
  destruct ef; simpl.
(* EF_external *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply do_external_function_sound; eauto.
(* EF_builtin *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply do_external_function_sound; eauto.
(* EF_runtime *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply do_external_function_sound; eauto.
(* EF_vload *)
  unfold do_ef_volatile_load. destruct vargs... destruct v... destruct vargs...
  mydestr. destruct p as [[w'' t''] v]; mydestr.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit do_volatile_load_sound; eauto. intuition. econstructor; eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  auto.
(* EF_vstore *)
  unfold do_ef_volatile_store. destruct vargs... destruct v... destruct vargs... destruct vargs...
  mydestr. destruct p as [[w'' t''] m'']. mydestr.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit do_volatile_store_sound; eauto. intuition. econstructor; eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  auto.
(* EF_malloc *)
  unfold do_ef_malloc. destruct vargs... destruct vargs... mydestr.
  destruct (Mem.alloc m (- size_chunk Mptr) (Ptrofs.unsigned i)) as [m1 b] eqn:?. mydestr.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  split. apply SIZE in Heqo. subst v. econstructor; eauto. constructor.
(* EF_free *)
  unfold do_ef_free. destruct vargs... destruct v... destruct vargs...
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  mydestr. split. apply SIZE in Heqo0. econstructor; eauto. congruence. omega. constructor.
(* EF_memcpy *)
  unfold do_ef_memcpy. destruct vargs... destruct v... destruct vargs...
  destruct v... destruct vargs... mydestr. 
  apply Decidable_sound in Heqb1. red in Heqb1.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  split. econstructor; eauto; tauto. constructor.
(* EF_annot *)
  unfold do_ef_annot. mydestr.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  split. constructor. apply list_eventval_of_val_sound; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  econstructor. constructor; eauto. constructor.
(* EF_annot_val *)
  unfold do_ef_annot_val. destruct vargs... destruct vargs... mydestr.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  split. constructor. apply eventval_of_val_sound; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  econstructor. constructor; eauto. constructor.
(* EF_inline_asm *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply do_inline_assembly_sound; eauto.
(* EF_debug *)
(* Goal: imm_safe ge e RV (Eval v ty) m *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  unfold do_ef_debug. mydestr. split; constructor.
Qed.

Lemma do_ef_external_complete:
  forall ef w vargs m w' t vres m',
  external_call ef ge vargs m t vres m' -> possible_trace w t w' ->
  do_external ef w vargs m = Some(w', t, vres, m').
Proof.
(* Goal: forall (ef : external_function) (w : world) (vargs : list val) (m : Mem.mem) (w' : world) (t : trace) (vres : val) (m' : Mem.mem) (_ : external_call ef (@Genv.to_senv fundef type (genv_genv ge)) vargs m t vres m') (_ : possible_trace w t w'), @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_external ef w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
  assert (SIZE: forall n, do_alloc_size (Vptrofs n) = Some n).
(* Goal: forall n : Ptrofs.int, @eq (option Ptrofs.int) (do_alloc_size (Vptrofs n)) (@Some Ptrofs.int n) *)
(* Goal: forall (ef : external_function) (w : world) (vargs : list val) (m : Mem.mem) (w' : world) (t : trace) (vres : val) (m' : Mem.mem) (_ : external_call ef (@Genv.to_senv fundef type (genv_genv ge)) vargs m t vres m') (_ : possible_trace w t w'), @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_external ef w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
  { unfold Vptrofs, do_alloc_size; intros; destruct Archi.ptr64 eqn:SF. 
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
    rewrite Ptrofs.of_int64_to_int64; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
    rewrite Ptrofs.of_int_to_int; auto. }
(* Goal: @eq (option val) (if @Genv.public_symbol fundef type (genv_genv ge) id then if typ_eq Tptr Tptr then match @Genv.find_symbol fundef type (genv_genv ge) id with | Some b => @Some val (Vptr b ofs) | None => @None val end else @None val else @None val) (@Some val (Vptr b ofs)) *)
  intros. destruct ef; simpl in *.
(* EF_external *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply do_external_function_complete; eauto.
(* EF_builtin *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply do_external_function_complete; eauto.
(* EF_runtime *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply do_external_function_complete; eauto.
(* EF_vload *)
  inv H; unfold do_ef_volatile_load.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit do_volatile_load_complete; eauto. intros EQ; rewrite EQ; auto.
(* EF_vstore *)
  inv H; unfold do_ef_volatile_store.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit do_volatile_store_complete; eauto. intros EQ; rewrite EQ; auto.
(* EF_malloc *)
  inv H; unfold do_ef_malloc.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  inv H0. erewrite SIZE by eauto. rewrite H1, H2. auto.
(* EF_free *)
  inv H; unfold do_ef_free.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  inv H0. rewrite H1. erewrite SIZE by eauto. rewrite zlt_true. rewrite H3. auto. omega.
(* EF_memcpy *)
  inv H; unfold do_ef_memcpy.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  inv H0. rewrite Decidable_complete. rewrite H7; rewrite H8; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  red. tauto.
(* EF_annot *)
(* Goal: @ex string (fun rule : string => @eq (reducts expr) match sem_cast v1 ty1 ty2 m with | Some v => topred (Rred (String (Ascii.Ascii false true false false true 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 true true true true false true false) (String (Ascii.Ascii false false false 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 true false false true true false) (String (Ascii.Ascii false true true true false true true false) EmptyString))))))))) (Eval v ty) m E0) | None => stuck end (topred (Rred rule (Eval v ty) m E0))) *)
(* Goal: @ex string (fun rule : string => @eq (reducts expr) match is_val_list el with | Some vtl => match sem_cast_arguments vtl tyargs m with | Some vargs => match do_external ef w vargs m with | Some (pair (pair (pair w' t as p1) v as p0) m' as p) => topred (Rred (String (Ascii.Ascii false true false false true 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 true true true true false true false) (String (Ascii.Ascii false true false false false true true false) (String (Ascii.Ascii true false true false true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii false false true false true 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) EmptyString))))))))))) (Eval v ty) m' t) | None => stuck end | None => stuck end | None => @incontext exprlist expr (fun x : exprlist => Ebuiltin ef tyargs x ty) (step_exprlist el m) end (topred (Rred rule (Eval vres ty) m' t))) *)
  inv H; unfold do_ef_annot. inv H0. inv H6. inv H4.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  rewrite (list_eventval_of_val_complete _ _ _ H1). auto.
(* EF_annot_val *)
(* Goal: @ex string (fun rule : string => @eq (reducts expr) match sem_cast v1 ty1 ty2 m with | Some v => topred (Rred (String (Ascii.Ascii false true false false true 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 true true true true false true false) (String (Ascii.Ascii false false false 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 true false false true true false) (String (Ascii.Ascii false true true true false true true false) EmptyString))))))))) (Eval v ty) m E0) | None => stuck end (topred (Rred rule (Eval v ty) m E0))) *)
(* Goal: @ex string (fun rule : string => @eq (reducts expr) match is_val_list el with | Some vtl => match sem_cast_arguments vtl tyargs m with | Some vargs => match do_external ef w vargs m with | Some (pair (pair (pair w' t as p1) v as p0) m' as p) => topred (Rred (String (Ascii.Ascii false true false false true 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 true true true true false true false) (String (Ascii.Ascii false true false false false true true false) (String (Ascii.Ascii true false true false true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii false false true false true 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) EmptyString))))))))))) (Eval v ty) m' t) | None => stuck end | None => stuck end | None => @incontext exprlist expr (fun x : exprlist => Ebuiltin ef tyargs x ty) (step_exprlist el m) end (topred (Rred rule (Eval vres ty) m' t))) *)
  inv H; unfold do_ef_annot_val. inv H0. inv H6. inv H4.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  rewrite (eventval_of_val_complete _ _ _ H1). auto.
(* EF_inline_asm *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply do_inline_assembly_complete; eauto.
(* EF_debug *)
(* Goal: @ex string (fun rule : string => @eq (reducts expr) match sem_cast v1 ty1 ty2 m with | Some v => topred (Rred (String (Ascii.Ascii false true false false true 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 true true true true false true false) (String (Ascii.Ascii false false false 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 true false false true true false) (String (Ascii.Ascii false true true true false true true false) EmptyString))))))))) (Eval v ty) m E0) | None => stuck end (topred (Rred rule (Eval v ty) m E0))) *)
(* Goal: @ex string (fun rule : string => @eq (reducts expr) match is_val_list el with | Some vtl => match sem_cast_arguments vtl tyargs m with | Some vargs => match do_external ef w vargs m with | Some (pair (pair (pair w' t as p1) v as p0) m' as p) => topred (Rred (String (Ascii.Ascii false true false false true 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 true true true true false true false) (String (Ascii.Ascii false true false false false true true false) (String (Ascii.Ascii true false true false true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii false false true false true 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) EmptyString))))))))))) (Eval v ty) m' t) | None => stuck end | None => stuck end | None => @incontext exprlist expr (fun x : exprlist => Ebuiltin ef tyargs x ty) (step_exprlist el m) end (topred (Rred rule (Eval vres ty) m' t))) *)
  inv H. inv H0. reflexivity.
Qed.

(** * Reduction of expressions *)

Inductive reduction: Type :=
  | Lred (rule: string) (l': expr) (m': mem)
  | Rred (rule: string) (r': expr) (m': mem) (t: trace)
  | Callred (rule: string) (fd: fundef) (args: list val) (tyres: type) (m': mem)
(* Goal: reduction_ok k a m Stuckred *)
(* Goal: match k with | LV => not (@eq (option (prod (prod block Ptrofs.int) type)) (is_loc a) (@None (prod (prod block Ptrofs.int) type))) | RV => not (@eq (option (prod val type)) (is_val a) (@None (prod val type))) end *)
  | Stuckred.

Section EXPRS.

Variable e: env.
Variable w: world.

Fixpoint sem_cast_arguments (vtl: list (val * type)) (tl: typelist) (m: mem) : option (list val) :=
  match vtl, tl with
  | nil, Tnil => Some nil
  | (v1,t1)::vtl, Tcons t1' tl =>
      do v <- sem_cast v1 t1 t1' m; do vl <- sem_cast_arguments vtl tl m; Some(v::vl)
  | _, _ => None
  end.

(** The result of stepping an expression is a list [ll] of possible reducts.
  Each element of [ll] is a pair of a context and the result of reducing
  inside this context (see type [reduction] above).
  The list [ll] is empty if the expression is fully reduced
   (it's [Eval] for a r-value and [Eloc] for a l-value).
*)

Definition reducts (A: Type): Type := list ((expr -> A) * reduction).

Definition topred (r: reduction) : reducts expr :=
  ((fun (x: expr) => x), r) :: nil.

Definition stuck : reducts expr :=
  ((fun (x: expr) => x), Stuckred) :: nil.

Definition incontext {A B: Type} (ctx: A -> B) (ll: reducts A) : reducts B :=
  map (fun z => ((fun (x: expr) => ctx(fst z x)), snd z)) ll.

(* Goal: forall n : Ptrofs.int, @eq (option Ptrofs.int) (do_alloc_size (Vptrofs n)) (@Some Ptrofs.int n) *)
(* Goal: forall (ef : external_function) (w : world) (vargs : list val) (m : Mem.mem) (w' : world) (t : trace) (vres : val) (m' : Mem.mem) (_ : external_call ef (@Genv.to_senv fundef type (genv_genv ge)) vargs m t vres m') (_ : possible_trace w t w'), @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_external ef w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
Definition incontext2 {A1 A2 B: Type}
                     (ctx1: A1 -> B) (ll1: reducts A1)
                     (ctx2: A2 -> B) (ll2: reducts A2) : reducts B :=
  incontext ctx1 ll1 ++ incontext ctx2 ll2.

Notation "'do' X <- A ; B" := (match A with Some X => B | None => stuck end)
  (at level 200, X ident, A at level 100, B at level 200)
  : reducts_monad_scope.

Notation "'do' X , Y <- A ; B" := (match A with Some (X, Y) => B | None => stuck end)
  (at level 200, X ident, Y ident, A at level 100, B at level 200)
  : reducts_monad_scope.

Notation "'do' X , Y , Z <- A ; B" := (match A with Some (X, Y, Z) => B | None => stuck end)
  (at level 200, X ident, Y ident, Z ident, A at level 100, B at level 200)
  : reducts_monad_scope.

Notation " 'check' A ; B" := (if A then B else stuck)
  (at level 200, A at level 100, B at level 200)
  : reducts_monad_scope.

Local Open Scope reducts_monad_scope.

Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
  match k, a with
  | LV, Eloc b ofs ty =>
      nil
  | LV, Evar x ty =>
      match e!x with
      | Some(b, ty') =>
          check type_eq ty ty';
          topred (Lred "red_var_local" (Eloc b Ptrofs.zero ty) m)
      | None =>
          do b <- Genv.find_symbol ge x;
          topred (Lred "red_var_global" (Eloc b Ptrofs.zero ty) m)
      end
  | LV, Ederef r ty =>
      match is_val r with
      | Some(Vptr b ofs, ty') =>
          topred (Lred "red_deref" (Eloc b ofs ty) m)
      | Some _ =>
          stuck
      | None =>
          incontext (fun x => Ederef x ty) (step_expr RV r m)
      end
  | LV, Efield r f ty =>
      match is_val r with
      | Some(Vptr b ofs, ty') =>
          match ty' with
          | Tstruct id _ =>
              do co <- ge.(genv_cenv)!id;
              match field_offset ge f (co_members co) with
              | Error _ => stuck
              | OK delta => topred (Lred "red_field_struct" (Eloc b (Ptrofs.add ofs (Ptrofs.repr delta)) ty) m)
              end
          | Tunion id _ =>
              do co <- ge.(genv_cenv)!id;
              topred (Lred "red_field_union" (Eloc b ofs ty) m)
          | _ => stuck
          end
      | Some _ =>
          stuck
      | None =>
          incontext (fun x => Efield x f ty) (step_expr RV r m)
      end
  | RV, Eval v ty =>
      nil
  | RV, Evalof l ty =>
      match is_loc l with
      | Some(b, ofs, ty') =>
          check type_eq ty ty';
          do w',t,v <- do_deref_loc w ty m b ofs;
          topred (Rred "red_rvalof" (Eval v ty) m t)
      | None =>
          incontext (fun x => Evalof x ty) (step_expr LV l m)
      end
  | RV, Eaddrof l ty =>
      match is_loc l with
      | Some(b, ofs, ty') => topred (Rred "red_addrof" (Eval (Vptr b ofs) ty) m E0)
      | None => incontext (fun x => Eaddrof x ty) (step_expr LV l m)
      end
  | RV, Eunop op r1 ty =>
      match is_val r1 with
      | Some(v1, ty1) =>
          do v <- sem_unary_operation op v1 ty1 m;
          topred (Rred "red_unop" (Eval v ty) m E0)
      | None =>
          incontext (fun x => Eunop op x ty) (step_expr RV r1 m)
      end
  | RV, Ebinop op r1 r2 ty =>
      match is_val r1, is_val r2 with
      | Some(v1, ty1), Some(v2, ty2) =>
          do v <- sem_binary_operation ge op v1 ty1 v2 ty2 m;
          topred (Rred "red_binop" (Eval v ty) m E0)
      | _, _ =>
         incontext2 (fun x => Ebinop op x r2 ty) (step_expr RV r1 m)
                    (fun x => Ebinop op r1 x ty) (step_expr RV r2 m)
      end
  | RV, Ecast r1 ty =>
      match is_val r1 with
      | Some(v1, ty1) =>
          do v <- sem_cast v1 ty1 ty m;
          topred (Rred "red_cast" (Eval v ty) m E0)
      | None =>
          incontext (fun x => Ecast x ty) (step_expr RV r1 m)
      end
  | RV, Eseqand r1 r2 ty =>
      match is_val r1 with
      | Some(v1, ty1) =>
          do b <- bool_val v1 ty1 m;
          if b then topred (Rred "red_seqand_true" (Eparen r2 type_bool ty) m E0)
               else topred (Rred "red_seqand_false" (Eval (Vint Int.zero) ty) m E0)
      | None =>
          incontext (fun x => Eseqand x r2 ty) (step_expr RV r1 m)
      end
  | RV, Eseqor r1 r2 ty =>
      match is_val r1 with
      | Some(v1, ty1) =>
          do b <- bool_val v1 ty1 m;
          if b then topred (Rred "red_seqor_true" (Eval (Vint Int.one) ty) m E0)
               else topred (Rred "red_seqor_false" (Eparen r2 type_bool ty) m E0)
      | None =>
          incontext (fun x => Eseqor x r2 ty) (step_expr RV r1 m)
      end
  | RV, Econdition r1 r2 r3 ty =>
      match is_val r1 with
      | Some(v1, ty1) =>
          do b <- bool_val v1 ty1 m;
          topred (Rred "red_condition" (Eparen (if b then r2 else r3) ty ty) m E0)
      | None =>
          incontext (fun x => Econdition x r2 r3 ty) (step_expr RV r1 m)
      end
  | RV, Esizeof ty' ty =>
      topred (Rred "red_sizeof" (Eval (Vptrofs (Ptrofs.repr (sizeof ge ty'))) ty) m E0)
  | RV, Ealignof ty' ty =>
      topred (Rred "red_alignof" (Eval (Vptrofs (Ptrofs.repr (alignof ge ty'))) ty) m E0)
  | RV, Eassign l1 r2 ty =>
      match is_loc l1, is_val r2 with
      | Some(b, ofs, ty1), Some(v2, ty2) =>
          check type_eq ty1 ty;
          do v <- sem_cast v2 ty2 ty1 m;
          do w',t,m' <- do_assign_loc w ty1 m b ofs v;
          topred (Rred "red_assign" (Eval v ty) m' t)
      | _, _ =>
         incontext2 (fun x => Eassign x r2 ty) (step_expr LV l1 m)
                    (fun x => Eassign l1 x ty) (step_expr RV r2 m)
      end
  | RV, Eassignop op l1 r2 tyres ty =>
      match is_loc l1, is_val r2 with
      | Some(b, ofs, ty1), Some(v2, ty2) =>
          check type_eq ty1 ty;
          do w',t,v1 <- do_deref_loc w ty1 m b ofs;
          let r' := Eassign (Eloc b ofs ty1)
                           (Ebinop op (Eval v1 ty1) (Eval v2 ty2) tyres) ty1 in
          topred (Rred "red_assignop" r' m t)
      | _, _ =>
         incontext2 (fun x => Eassignop op x r2 tyres ty) (step_expr LV l1 m)
                    (fun x => Eassignop op l1 x tyres ty) (step_expr RV r2 m)
      end
  | RV, Epostincr id l ty =>
      match is_loc l with
      | Some(b, ofs, ty1) =>
          check type_eq ty1 ty;
          do w',t, v1 <- do_deref_loc w ty m b ofs;
          let op := match id with Incr => Oadd | Decr => Osub end in
          let r' :=
            Ecomma (Eassign (Eloc b ofs ty)
                           (Ebinop op (Eval v1 ty) (Eval (Vint Int.one) type_int32s) (incrdecr_type ty))
                           ty)
                   (Eval v1 ty) ty in
          topred (Rred "red_postincr" r' m t)
      | None =>
          incontext (fun x => Epostincr id x ty) (step_expr LV l m)
      end
  | RV, Ecomma r1 r2 ty =>
      match is_val r1 with
      | Some _ =>
          check type_eq (typeof r2) ty;
          topred (Rred "red_comma" r2 m E0)
      | None =>
          incontext (fun x => Ecomma x r2 ty) (step_expr RV r1 m)
      end
  | RV, Eparen r1 tycast ty =>
      match is_val r1 with
      | Some (v1, ty1) =>
          do v <- sem_cast v1 ty1 tycast m;
          topred (Rred "red_paren" (Eval v ty) m E0)
      | None =>
          incontext (fun x => Eparen x tycast ty) (step_expr RV r1 m)
      end
  | RV, Ecall r1 rargs ty =>
      match is_val r1, is_val_list rargs with
      | Some(vf, tyf), Some vtl =>
          match classify_fun tyf with
          | fun_case_f tyargs tyres cconv =>
              do fd <- Genv.find_funct ge vf;
              do vargs <- sem_cast_arguments vtl tyargs m;
              check type_eq (type_of_fundef fd) (Tfunction tyargs tyres cconv);
              topred (Callred "red_call" fd vargs ty m)
          | _ => stuck
          end
      | _, _ =>
          incontext2 (fun x => Ecall x rargs ty) (step_expr RV r1 m)
                     (fun x => Ecall r1 x ty) (step_exprlist rargs m)
      end
  | RV, Ebuiltin ef tyargs rargs ty =>
      match is_val_list rargs with
      | Some vtl =>
          do vargs <- sem_cast_arguments vtl tyargs m;
          match do_external ef w vargs m with
          | None => stuck
          | Some(w',t,v,m') => topred (Rred "red_builtin" (Eval v ty) m' t)
          end
      | _ =>
          incontext (fun x => Ebuiltin ef tyargs x ty) (step_exprlist rargs m)
      end
  | _, _ => stuck
  end

with step_exprlist (rl: exprlist) (m: mem): reducts exprlist :=
  match rl with
  | Enil =>
      nil
  | Econs r1 rs =>
      incontext2 (fun x => Econs x rs) (step_expr RV r1 m)
                 (fun x => Econs r1 x) (step_exprlist rs m)
  end.

(** Technical properties on safe expressions. *)

Inductive imm_safe_t: kind -> expr -> mem -> Prop :=
  | imm_safe_t_val: forall v ty m,
      imm_safe_t RV (Eval v ty) m
  | imm_safe_t_loc: forall b ofs ty m,
      imm_safe_t LV (Eloc b ofs ty) m
  | imm_safe_t_lred: forall to C l m l' m',
      lred ge e l m l' m' ->
      context LV to C ->
      imm_safe_t to (C l) m
  | imm_safe_t_rred: forall to C r m t r' m' w',
      rred ge r m t r' m' -> possible_trace w t w' ->
      context RV to C ->
      imm_safe_t to (C r) m
  | imm_safe_t_callred: forall to C r m fd args ty,
      callred ge r m fd args ty ->
      context RV to C ->
      imm_safe_t to (C r) m.

Remark imm_safe_t_imm_safe:
  forall k a m, imm_safe_t k a m -> imm_safe ge e k a m.
Proof.
(* Goal: forall (m : Mem.mem) (al : exprlist) (tyl : typelist) (vl : list val) (_ : cast_arguments m al tyl vl), @ex (list (prod val type)) (fun vtl : list (prod val type) => and (@eq (option (list (prod val type))) (is_val_list al) (@Some (list (prod val type)) vtl)) (@eq (option (list val)) (sem_cast_arguments vtl tyl m) (@Some (list val) vl))) *)
  induction 1.
(* Goal: imm_safe ge e RV (Eval v ty) m *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  constructor.
(* Goal: imm_safe ge e RV (Eval v ty) m *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  constructor.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply imm_safe_lred; eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply imm_safe_rred; eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply imm_safe_callred; eauto.
Qed.

Fixpoint exprlist_all_values (rl: exprlist) : Prop :=
  match rl with
  | Enil => True
  | Econs (Eval v ty) rl' => exprlist_all_values rl'
  | Econs _ _ => False
  end.

Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
  match a with
  | Eloc b ofs ty => False
  | Evar x ty =>
      exists b,
      e!x = Some(b, ty)
      \/ (e!x = None /\ Genv.find_symbol ge x = Some b)
  | Ederef (Eval v ty1) ty =>
      exists b, exists ofs, v = Vptr b ofs
  | Efield (Eval v ty1) f ty =>
      exists b, exists ofs, v = Vptr b ofs /\
      match ty1 with
      | Tstruct id _ => exists co delta, ge.(genv_cenv)!id = Some co /\ field_offset ge f (co_members co) = OK delta
      | Tunion  id _ => exists co, ge.(genv_cenv)!id = Some co
      | _ => False
      end
  | Eval v ty => False
  | Evalof (Eloc b ofs ty') ty =>
      ty' = ty /\ exists t, exists v, exists w', deref_loc ge ty m b ofs t v /\ possible_trace w t w'
  | Eunop op (Eval v1 ty1) ty =>
      exists v, sem_unary_operation op v1 ty1 m = Some v
  | Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty =>
      exists v, sem_binary_operation ge op v1 ty1 v2 ty2 m = Some v
  | Ecast (Eval v1 ty1) ty =>
      exists v, sem_cast v1 ty1 ty m = Some v
  | Eseqand (Eval v1 ty1) r2 ty =>
      exists b, bool_val v1 ty1 m = Some b
  | Eseqor (Eval v1 ty1) r2 ty =>
      exists b, bool_val v1 ty1 m = Some b
  | Econdition (Eval v1 ty1) r1 r2 ty =>
      exists b, bool_val v1 ty1 m = Some b
  | Eassign (Eloc b ofs ty1) (Eval v2 ty2) ty =>
      exists v, exists m', exists t, exists w',
      ty = ty1 /\ sem_cast v2 ty2 ty1 m = Some v /\ assign_loc ge ty1 m b ofs v t m' /\ possible_trace w t w'
  | Eassignop op (Eloc b ofs ty1) (Eval v2 ty2) tyres ty =>
      exists t, exists v1, exists w',
      ty = ty1 /\ deref_loc ge ty1 m b ofs t v1 /\ possible_trace w t w'
  | Epostincr id (Eloc b ofs ty1) ty =>
      exists t, exists v1, exists w',
      ty = ty1 /\ deref_loc ge ty m b ofs t v1 /\ possible_trace w t w'
  | Ecomma (Eval v ty1) r2 ty =>
      typeof r2 = ty
  | Eparen (Eval v1 ty1) tycast ty =>
      exists v, sem_cast v1 ty1 tycast m = Some v
  | Ecall (Eval vf tyf) rargs ty =>
      exprlist_all_values rargs ->
      exists tyargs tyres cconv fd vl,
         classify_fun tyf = fun_case_f tyargs tyres cconv
      /\ Genv.find_funct ge vf = Some fd
      /\ cast_arguments m rargs tyargs vl
      /\ type_of_fundef fd = Tfunction tyargs tyres cconv
  | Ebuiltin ef tyargs rargs ty =>
      exprlist_all_values rargs ->
      exists vargs t vres m' w',
         cast_arguments m rargs tyargs vargs
      /\ external_call ef ge vargs m t vres m'
      /\ possible_trace w t w'
  | _ => True
  end.

Lemma lred_invert:
  forall l m l' m', lred ge e l m l' m' -> invert_expr_prop l m.
Proof.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  induction 1; red; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exists b; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exists b; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exists b; exists ofs; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exists b; exists ofs; split; auto. exists co, delta; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exists b; exists ofs; split; auto. exists co; auto.
Qed.

Lemma rred_invert:
  forall w' r m t r' m', rred ge r m t r' m' -> possible_trace w t w' -> invert_expr_prop r m.
Proof.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  induction 1; intros; red; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  split; auto; exists t; exists v; exists w'; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exists v; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exists v; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exists v; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exists true; auto. exists false; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exists true; auto. exists false; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exists b; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exists v; exists m'; exists t; exists w'; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exists t; exists v1; exists w'; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exists t; exists v1; exists w'; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exists v; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  intros; exists vargs; exists t; exists vres; exists m'; exists w'; auto.
Qed.

Lemma callred_invert:
  forall r fd args ty m,
  callred ge r m fd args ty ->
  invert_expr_prop r m.
Proof.
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  intros. inv H. simpl.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  intros. exists tyargs, tyres, cconv, fd, args; auto.
Qed.

Scheme context_ind2 := Minimality for context Sort Prop
  with contextlist_ind2 := Minimality for contextlist Sort Prop.
Combined Scheme context_contextlist_ind from context_ind2, contextlist_ind2.

Lemma invert_expr_context:
  (forall from to C, context from to C ->
   forall a m,
   invert_expr_prop a m ->
   invert_expr_prop (C a) m)
/\(forall from C, contextlist from C ->
  forall a m,
  invert_expr_prop a m ->
  ~exprlist_all_values (C a)).
Proof.
(* Goal: @eq (option Mem.mem) match E0 with | nil => sem_bind_parameters w e m1 params vl | cons e l => @None Mem.mem end (@Some Mem.mem m2) *)
  apply context_contextlist_ind; intros; try (exploit H0; [eauto|intros]); simpl.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  auto.
(* Goal: match C a with | Eval v1 ty1 => @ex val (fun v : val => @eq (option val) (sem_cast v1 ty1 tycast m) (@Some val v)) | Evar x ty => True | Efield l f ty => True | Evalof l ty => True | Ederef r ty => True | Eaddrof l ty => True | Eunop op r ty => True | Ebinop op r1 r2 ty => True | Ecast r ty => True | Eseqand r1 r2 ty => True | Eseqor r1 r2 ty => True | Econdition r1 r2 r3 ty => True | Esizeof ty' ty => True | Ealignof ty' ty => True | Eassign l r ty => True | Eassignop op l r tyres ty => True | Epostincr id l ty => True | Ecomma r1 r2 ty => True | Ecall r1 rargs ty => True | Ebuiltin ef tyargs rargs ty => True | Eloc b ofs ty => True | Eparen r tycast ty => True end *)
(* Goal: not match C a with | Eval v ty => exprlist_all_values el | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
(* Goal: not match e1 with | Eval v ty => exprlist_all_values (C a) | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
  destruct (C a); auto; contradiction.
(* Goal: match C a with | Eval v1 ty1 => @ex val (fun v : val => @eq (option val) (sem_cast v1 ty1 tycast m) (@Some val v)) | Evar x ty => True | Efield l f ty => True | Evalof l ty => True | Ederef r ty => True | Eaddrof l ty => True | Eunop op r ty => True | Ebinop op r1 r2 ty => True | Ecast r ty => True | Eseqand r1 r2 ty => True | Eseqor r1 r2 ty => True | Econdition r1 r2 r3 ty => True | Esizeof ty' ty => True | Ealignof ty' ty => True | Eassign l r ty => True | Eassignop op l r tyres ty => True | Epostincr id l ty => True | Ecomma r1 r2 ty => True | Ecall r1 rargs ty => True | Ebuiltin ef tyargs rargs ty => True | Eloc b ofs ty => True | Eparen r tycast ty => True end *)
(* Goal: not match C a with | Eval v ty => exprlist_all_values el | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
(* Goal: not match e1 with | Eval v ty => exprlist_all_values (C a) | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
  destruct (C a); auto; contradiction.
(* Goal: match C a with | Eval v1 ty1 => @ex val (fun v : val => @eq (option val) (sem_cast v1 ty1 tycast m) (@Some val v)) | Evar x ty => True | Efield l f ty => True | Evalof l ty => True | Ederef r ty => True | Eaddrof l ty => True | Eunop op r ty => True | Ebinop op r1 r2 ty => True | Ecast r ty => True | Eseqand r1 r2 ty => True | Eseqor r1 r2 ty => True | Econdition r1 r2 r3 ty => True | Esizeof ty' ty => True | Ealignof ty' ty => True | Eassign l r ty => True | Eassignop op l r tyres ty => True | Epostincr id l ty => True | Ecomma r1 r2 ty => True | Ecall r1 rargs ty => True | Ebuiltin ef tyargs rargs ty => True | Eloc b ofs ty => True | Eparen r tycast ty => True end *)
(* Goal: not match C a with | Eval v ty => exprlist_all_values el | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
(* Goal: not match e1 with | Eval v ty => exprlist_all_values (C a) | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
  destruct (C a); auto; contradiction.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  auto.
(* Goal: match C a with | Eval v1 ty1 => @ex val (fun v : val => @eq (option val) (sem_cast v1 ty1 tycast m) (@Some val v)) | Evar x ty => True | Efield l f ty => True | Evalof l ty => True | Ederef r ty => True | Eaddrof l ty => True | Eunop op r ty => True | Ebinop op r1 r2 ty => True | Ecast r ty => True | Eseqand r1 r2 ty => True | Eseqor r1 r2 ty => True | Econdition r1 r2 r3 ty => True | Esizeof ty' ty => True | Ealignof ty' ty => True | Eassign l r ty => True | Eassignop op l r tyres ty => True | Epostincr id l ty => True | Ecomma r1 r2 ty => True | Ecall r1 rargs ty => True | Ebuiltin ef tyargs rargs ty => True | Eloc b ofs ty => True | Eparen r tycast ty => True end *)
(* Goal: not match C a with | Eval v ty => exprlist_all_values el | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
(* Goal: not match e1 with | Eval v ty => exprlist_all_values (C a) | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
  destruct (C a); auto; contradiction.
(* Goal: match C a with | Eval v1 ty1 => @ex val (fun v : val => @eq (option val) (sem_cast v1 ty1 tycast m) (@Some val v)) | Evar x ty => True | Efield l f ty => True | Evalof l ty => True | Ederef r ty => True | Eaddrof l ty => True | Eunop op r ty => True | Ebinop op r1 r2 ty => True | Ecast r ty => True | Eseqand r1 r2 ty => True | Eseqor r1 r2 ty => True | Econdition r1 r2 r3 ty => True | Esizeof ty' ty => True | Ealignof ty' ty => True | Eassign l r ty => True | Eassignop op l r tyres ty => True | Epostincr id l ty => True | Ecomma r1 r2 ty => True | Ecall r1 rargs ty => True | Ebuiltin ef tyargs rargs ty => True | Eloc b ofs ty => True | Eparen r tycast ty => True end *)
(* Goal: not match C a with | Eval v ty => exprlist_all_values el | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
(* Goal: not match e1 with | Eval v ty => exprlist_all_values (C a) | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
  destruct (C a); auto; contradiction.
(* Goal: match C a with | Eval v1 ty1 => @ex val (fun v : val => @eq (option val) (sem_cast v1 ty1 tycast m) (@Some val v)) | Evar x ty => True | Efield l f ty => True | Evalof l ty => True | Ederef r ty => True | Eaddrof l ty => True | Eunop op r ty => True | Ebinop op r1 r2 ty => True | Ecast r ty => True | Eseqand r1 r2 ty => True | Eseqor r1 r2 ty => True | Econdition r1 r2 r3 ty => True | Esizeof ty' ty => True | Ealignof ty' ty => True | Eassign l r ty => True | Eassignop op l r tyres ty => True | Epostincr id l ty => True | Ecomma r1 r2 ty => True | Ecall r1 rargs ty => True | Ebuiltin ef tyargs rargs ty => True | Eloc b ofs ty => True | Eparen r tycast ty => True end *)
(* Goal: not match C a with | Eval v ty => exprlist_all_values el | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
(* Goal: not match e1 with | Eval v ty => exprlist_all_values (C a) | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
  destruct e1; auto; destruct (C a); auto; contradiction.
(* Goal: match C a with | Eval v1 ty1 => @ex val (fun v : val => @eq (option val) (sem_cast v1 ty1 tycast m) (@Some val v)) | Evar x ty => True | Efield l f ty => True | Evalof l ty => True | Ederef r ty => True | Eaddrof l ty => True | Eunop op r ty => True | Ebinop op r1 r2 ty => True | Ecast r ty => True | Eseqand r1 r2 ty => True | Eseqor r1 r2 ty => True | Econdition r1 r2 r3 ty => True | Esizeof ty' ty => True | Ealignof ty' ty => True | Eassign l r ty => True | Eassignop op l r tyres ty => True | Epostincr id l ty => True | Ecomma r1 r2 ty => True | Ecall r1 rargs ty => True | Ebuiltin ef tyargs rargs ty => True | Eloc b ofs ty => True | Eparen r tycast ty => True end *)
(* Goal: not match C a with | Eval v ty => exprlist_all_values el | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
(* Goal: not match e1 with | Eval v ty => exprlist_all_values (C a) | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
  destruct (C a); auto; contradiction.
(* Goal: match C a with | Eval v1 ty1 => @ex val (fun v : val => @eq (option val) (sem_cast v1 ty1 tycast m) (@Some val v)) | Evar x ty => True | Efield l f ty => True | Evalof l ty => True | Ederef r ty => True | Eaddrof l ty => True | Eunop op r ty => True | Ebinop op r1 r2 ty => True | Ecast r ty => True | Eseqand r1 r2 ty => True | Eseqor r1 r2 ty => True | Econdition r1 r2 r3 ty => True | Esizeof ty' ty => True | Ealignof ty' ty => True | Eassign l r ty => True | Eassignop op l r tyres ty => True | Epostincr id l ty => True | Ecomma r1 r2 ty => True | Ecall r1 rargs ty => True | Ebuiltin ef tyargs rargs ty => True | Eloc b ofs ty => True | Eparen r tycast ty => True end *)
(* Goal: not match C a with | Eval v ty => exprlist_all_values el | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
(* Goal: not match e1 with | Eval v ty => exprlist_all_values (C a) | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
  destruct (C a); auto; contradiction.
(* Goal: match C a with | Eval v1 ty1 => @ex val (fun v : val => @eq (option val) (sem_cast v1 ty1 tycast m) (@Some val v)) | Evar x ty => True | Efield l f ty => True | Evalof l ty => True | Ederef r ty => True | Eaddrof l ty => True | Eunop op r ty => True | Ebinop op r1 r2 ty => True | Ecast r ty => True | Eseqand r1 r2 ty => True | Eseqor r1 r2 ty => True | Econdition r1 r2 r3 ty => True | Esizeof ty' ty => True | Ealignof ty' ty => True | Eassign l r ty => True | Eassignop op l r tyres ty => True | Epostincr id l ty => True | Ecomma r1 r2 ty => True | Ecall r1 rargs ty => True | Ebuiltin ef tyargs rargs ty => True | Eloc b ofs ty => True | Eparen r tycast ty => True end *)
(* Goal: not match C a with | Eval v ty => exprlist_all_values el | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
(* Goal: not match e1 with | Eval v ty => exprlist_all_values (C a) | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
  destruct (C a); auto; contradiction.
(* Goal: match C a with | Eval v1 ty1 => @ex val (fun v : val => @eq (option val) (sem_cast v1 ty1 tycast m) (@Some val v)) | Evar x ty => True | Efield l f ty => True | Evalof l ty => True | Ederef r ty => True | Eaddrof l ty => True | Eunop op r ty => True | Ebinop op r1 r2 ty => True | Ecast r ty => True | Eseqand r1 r2 ty => True | Eseqor r1 r2 ty => True | Econdition r1 r2 r3 ty => True | Esizeof ty' ty => True | Ealignof ty' ty => True | Eassign l r ty => True | Eassignop op l r tyres ty => True | Epostincr id l ty => True | Ecomma r1 r2 ty => True | Ecall r1 rargs ty => True | Ebuiltin ef tyargs rargs ty => True | Eloc b ofs ty => True | Eparen r tycast ty => True end *)
(* Goal: not match C a with | Eval v ty => exprlist_all_values el | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
(* Goal: not match e1 with | Eval v ty => exprlist_all_values (C a) | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
  destruct (C a); auto; contradiction.
(* Goal: match C a with | Eval v1 ty1 => @ex val (fun v : val => @eq (option val) (sem_cast v1 ty1 tycast m) (@Some val v)) | Evar x ty => True | Efield l f ty => True | Evalof l ty => True | Ederef r ty => True | Eaddrof l ty => True | Eunop op r ty => True | Ebinop op r1 r2 ty => True | Ecast r ty => True | Eseqand r1 r2 ty => True | Eseqor r1 r2 ty => True | Econdition r1 r2 r3 ty => True | Esizeof ty' ty => True | Ealignof ty' ty => True | Eassign l r ty => True | Eassignop op l r tyres ty => True | Epostincr id l ty => True | Ecomma r1 r2 ty => True | Ecall r1 rargs ty => True | Ebuiltin ef tyargs rargs ty => True | Eloc b ofs ty => True | Eparen r tycast ty => True end *)
(* Goal: not match C a with | Eval v ty => exprlist_all_values el | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
(* Goal: not match e1 with | Eval v ty => exprlist_all_values (C a) | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
  destruct (C a); auto; contradiction.
(* Goal: match C a with | Eval v1 ty1 => @ex val (fun v : val => @eq (option val) (sem_cast v1 ty1 tycast m) (@Some val v)) | Evar x ty => True | Efield l f ty => True | Evalof l ty => True | Ederef r ty => True | Eaddrof l ty => True | Eunop op r ty => True | Ebinop op r1 r2 ty => True | Ecast r ty => True | Eseqand r1 r2 ty => True | Eseqor r1 r2 ty => True | Econdition r1 r2 r3 ty => True | Esizeof ty' ty => True | Ealignof ty' ty => True | Eassign l r ty => True | Eassignop op l r tyres ty => True | Epostincr id l ty => True | Ecomma r1 r2 ty => True | Ecall r1 rargs ty => True | Ebuiltin ef tyargs rargs ty => True | Eloc b ofs ty => True | Eparen r tycast ty => True end *)
(* Goal: not match C a with | Eval v ty => exprlist_all_values el | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
(* Goal: not match e1 with | Eval v ty => exprlist_all_values (C a) | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
  destruct e1; auto; destruct (C a); auto; contradiction.
(* Goal: match C a with | Eval v1 ty1 => @ex val (fun v : val => @eq (option val) (sem_cast v1 ty1 tycast m) (@Some val v)) | Evar x ty => True | Efield l f ty => True | Evalof l ty => True | Ederef r ty => True | Eaddrof l ty => True | Eunop op r ty => True | Ebinop op r1 r2 ty => True | Ecast r ty => True | Eseqand r1 r2 ty => True | Eseqor r1 r2 ty => True | Econdition r1 r2 r3 ty => True | Esizeof ty' ty => True | Ealignof ty' ty => True | Eassign l r ty => True | Eassignop op l r tyres ty => True | Epostincr id l ty => True | Ecomma r1 r2 ty => True | Ecall r1 rargs ty => True | Ebuiltin ef tyargs rargs ty => True | Eloc b ofs ty => True | Eparen r tycast ty => True end *)
(* Goal: not match C a with | Eval v ty => exprlist_all_values el | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
(* Goal: not match e1 with | Eval v ty => exprlist_all_values (C a) | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
  destruct (C a); auto; contradiction.
(* Goal: match C a with | Eval v1 ty1 => @ex val (fun v : val => @eq (option val) (sem_cast v1 ty1 tycast m) (@Some val v)) | Evar x ty => True | Efield l f ty => True | Evalof l ty => True | Ederef r ty => True | Eaddrof l ty => True | Eunop op r ty => True | Ebinop op r1 r2 ty => True | Ecast r ty => True | Eseqand r1 r2 ty => True | Eseqor r1 r2 ty => True | Econdition r1 r2 r3 ty => True | Esizeof ty' ty => True | Ealignof ty' ty => True | Eassign l r ty => True | Eassignop op l r tyres ty => True | Epostincr id l ty => True | Ecomma r1 r2 ty => True | Ecall r1 rargs ty => True | Ebuiltin ef tyargs rargs ty => True | Eloc b ofs ty => True | Eparen r tycast ty => True end *)
(* Goal: not match C a with | Eval v ty => exprlist_all_values el | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
(* Goal: not match e1 with | Eval v ty => exprlist_all_values (C a) | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
  destruct e1; auto; destruct (C a); auto; contradiction.
(* Goal: match C a with | Eval v1 ty1 => @ex val (fun v : val => @eq (option val) (sem_cast v1 ty1 tycast m) (@Some val v)) | Evar x ty => True | Efield l f ty => True | Evalof l ty => True | Ederef r ty => True | Eaddrof l ty => True | Eunop op r ty => True | Ebinop op r1 r2 ty => True | Ecast r ty => True | Eseqand r1 r2 ty => True | Eseqor r1 r2 ty => True | Econdition r1 r2 r3 ty => True | Esizeof ty' ty => True | Ealignof ty' ty => True | Eassign l r ty => True | Eassignop op l r tyres ty => True | Epostincr id l ty => True | Ecomma r1 r2 ty => True | Ecall r1 rargs ty => True | Ebuiltin ef tyargs rargs ty => True | Eloc b ofs ty => True | Eparen r tycast ty => True end *)
(* Goal: not match C a with | Eval v ty => exprlist_all_values el | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
(* Goal: not match e1 with | Eval v ty => exprlist_all_values (C a) | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
  destruct (C a); auto; contradiction.
(* Goal: match C a with | Eval v1 ty1 => @ex val (fun v : val => @eq (option val) (sem_cast v1 ty1 tycast m) (@Some val v)) | Evar x ty => True | Efield l f ty => True | Evalof l ty => True | Ederef r ty => True | Eaddrof l ty => True | Eunop op r ty => True | Ebinop op r1 r2 ty => True | Ecast r ty => True | Eseqand r1 r2 ty => True | Eseqor r1 r2 ty => True | Econdition r1 r2 r3 ty => True | Esizeof ty' ty => True | Ealignof ty' ty => True | Eassign l r ty => True | Eassignop op l r tyres ty => True | Epostincr id l ty => True | Ecomma r1 r2 ty => True | Ecall r1 rargs ty => True | Ebuiltin ef tyargs rargs ty => True | Eloc b ofs ty => True | Eparen r tycast ty => True end *)
(* Goal: not match C a with | Eval v ty => exprlist_all_values el | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
(* Goal: not match e1 with | Eval v ty => exprlist_all_values (C a) | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
  destruct (C a); auto; contradiction.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct e1; auto. intros. elim (H0 a m); auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  intros. elim (H0 a m); auto.
(* Goal: match C a with | Eval v1 ty1 => @ex val (fun v : val => @eq (option val) (sem_cast v1 ty1 tycast m) (@Some val v)) | Evar x ty => True | Efield l f ty => True | Evalof l ty => True | Ederef r ty => True | Eaddrof l ty => True | Eunop op r ty => True | Ebinop op r1 r2 ty => True | Ecast r ty => True | Eseqand r1 r2 ty => True | Eseqor r1 r2 ty => True | Econdition r1 r2 r3 ty => True | Esizeof ty' ty => True | Ealignof ty' ty => True | Eassign l r ty => True | Eassignop op l r tyres ty => True | Epostincr id l ty => True | Ecomma r1 r2 ty => True | Ecall r1 rargs ty => True | Ebuiltin ef tyargs rargs ty => True | Eloc b ofs ty => True | Eparen r tycast ty => True end *)
(* Goal: not match C a with | Eval v ty => exprlist_all_values el | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
(* Goal: not match e1 with | Eval v ty => exprlist_all_values (C a) | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
  destruct (C a); auto; contradiction.
(* Goal: match C a with | Eval v1 ty1 => @ex val (fun v : val => @eq (option val) (sem_cast v1 ty1 tycast m) (@Some val v)) | Evar x ty => True | Efield l f ty => True | Evalof l ty => True | Ederef r ty => True | Eaddrof l ty => True | Eunop op r ty => True | Ebinop op r1 r2 ty => True | Ecast r ty => True | Eseqand r1 r2 ty => True | Eseqor r1 r2 ty => True | Econdition r1 r2 r3 ty => True | Esizeof ty' ty => True | Ealignof ty' ty => True | Eassign l r ty => True | Eassignop op l r tyres ty => True | Epostincr id l ty => True | Ecomma r1 r2 ty => True | Ecall r1 rargs ty => True | Ebuiltin ef tyargs rargs ty => True | Eloc b ofs ty => True | Eparen r tycast ty => True end *)
(* Goal: not match C a with | Eval v ty => exprlist_all_values el | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
(* Goal: not match e1 with | Eval v ty => exprlist_all_values (C a) | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
  destruct (C a); auto; contradiction.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  red; intros. destruct (C a); auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  red; intros. destruct e1; auto. elim (H0 a m); auto.
Qed.

Lemma imm_safe_t_inv:
  forall k a m,
  imm_safe_t k a m ->
  match a with
  | Eloc _ _ _ => True
  | Eval _ _ => True
  | _ => invert_expr_prop a m
  end.
Proof.
(* Goal: forall (k : kind) (a : expr) (m : Mem.mem) (_ : imm_safe_t k a m), match a with | Eval v ty => True | Evar x ty => invert_expr_prop a m | Efield l f ty => invert_expr_prop a m | Evalof l ty => invert_expr_prop a m | Ederef r ty => invert_expr_prop a m | Eaddrof l ty => invert_expr_prop a m | Eunop op r ty => invert_expr_prop a m | Ebinop op r1 r2 ty => invert_expr_prop a m | Ecast r ty => invert_expr_prop a m | Eseqand r1 r2 ty => invert_expr_prop a m | Eseqor r1 r2 ty => invert_expr_prop a m | Econdition r1 r2 r3 ty => invert_expr_prop a m | Esizeof ty' ty => invert_expr_prop a m | Ealignof ty' ty => invert_expr_prop a m | Eassign l r ty => invert_expr_prop a m | Eassignop op l r tyres ty => invert_expr_prop a m | Epostincr id l ty => invert_expr_prop a m | Ecomma r1 r2 ty => invert_expr_prop a m | Ecall r1 rargs ty => invert_expr_prop a m | Ebuiltin ef tyargs rargs ty => invert_expr_prop a m | Eloc b ofs ty => True | Eparen r tycast ty => invert_expr_prop a m end *)
  destruct invert_expr_context as [A B].
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  intros. inv H.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  auto.
(* Goal: match C l with | Eval v ty => True | Evar x ty => invert_expr_prop (C l) m | Efield l0 f ty => invert_expr_prop (C l) m | Evalof l0 ty => invert_expr_prop (C l) m | Ederef r ty => invert_expr_prop (C l) m | Eaddrof l0 ty => invert_expr_prop (C l) m | Eunop op r ty => invert_expr_prop (C l) m | Ebinop op r1 r2 ty => invert_expr_prop (C l) m | Ecast r ty => invert_expr_prop (C l) m | Eseqand r1 r2 ty => invert_expr_prop (C l) m | Eseqor r1 r2 ty => invert_expr_prop (C l) m | Econdition r1 r2 r3 ty => invert_expr_prop (C l) m | Esizeof ty' ty => invert_expr_prop (C l) m | Ealignof ty' ty => invert_expr_prop (C l) m | Eassign l0 r ty => invert_expr_prop (C l) m | Eassignop op l0 r tyres ty => invert_expr_prop (C l) m | Epostincr id l0 ty => invert_expr_prop (C l) m | Ecomma r1 r2 ty => invert_expr_prop (C l) m | Ecall r1 rargs ty => invert_expr_prop (C l) m | Ebuiltin ef tyargs rargs ty => invert_expr_prop (C l) m | Eloc b ofs ty => True | Eparen r tycast ty => invert_expr_prop (C l) m end *)
(* Goal: match C r with | Eval v ty => True | Evar x ty => invert_expr_prop (C r) m | Efield l f ty => invert_expr_prop (C r) m | Evalof l ty => invert_expr_prop (C r) m | Ederef r0 ty => invert_expr_prop (C r) m | Eaddrof l ty => invert_expr_prop (C r) m | Eunop op r0 ty => invert_expr_prop (C r) m | Ebinop op r1 r2 ty => invert_expr_prop (C r) m | Ecast r0 ty => invert_expr_prop (C r) m | Eseqand r1 r2 ty => invert_expr_prop (C r) m | Eseqor r1 r2 ty => invert_expr_prop (C r) m | Econdition r1 r2 r3 ty => invert_expr_prop (C r) m | Esizeof ty' ty => invert_expr_prop (C r) m | Ealignof ty' ty => invert_expr_prop (C r) m | Eassign l r0 ty => invert_expr_prop (C r) m | Eassignop op l r0 tyres ty => invert_expr_prop (C r) m | Epostincr id l ty => invert_expr_prop (C r) m | Ecomma r1 r2 ty => invert_expr_prop (C r) m | Ecall r1 rargs ty => invert_expr_prop (C r) m | Ebuiltin ef tyargs rargs ty => invert_expr_prop (C r) m | Eloc b ofs ty => True | Eparen r0 tycast ty => invert_expr_prop (C r) m end *)
(* Goal: match C r with | Eval v ty => True | Evar x ty => invert_expr_prop (C r) m | Efield l f ty => invert_expr_prop (C r) m | Evalof l ty => invert_expr_prop (C r) m | Ederef r0 ty => invert_expr_prop (C r) m | Eaddrof l ty => invert_expr_prop (C r) m | Eunop op r0 ty => invert_expr_prop (C r) m | Ebinop op r1 r2 ty => invert_expr_prop (C r) m | Ecast r0 ty => invert_expr_prop (C r) m | Eseqand r1 r2 ty => invert_expr_prop (C r) m | Eseqor r1 r2 ty => invert_expr_prop (C r) m | Econdition r1 r2 r3 ty => invert_expr_prop (C r) m | Esizeof ty' ty => invert_expr_prop (C r) m | Ealignof ty' ty => invert_expr_prop (C r) m | Eassign l r0 ty => invert_expr_prop (C r) m | Eassignop op l r0 tyres ty => invert_expr_prop (C r) m | Epostincr id l ty => invert_expr_prop (C r) m | Ecomma r1 r2 ty => invert_expr_prop (C r) m | Ecall r1 rargs ty => invert_expr_prop (C r) m | Ebuiltin ef tyargs rargs ty => invert_expr_prop (C r) m | Eloc b ofs ty => True | Eparen r0 tycast ty => invert_expr_prop (C r) m end *)
  assert (invert_expr_prop (C l) m).
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
    eapply A; eauto. eapply lred_invert; eauto.
(* Goal: match C r with | Eval v ty => True | Evar x ty => invert_expr_prop (C r) m | Efield l f ty => invert_expr_prop (C r) m | Evalof l ty => invert_expr_prop (C r) m | Ederef r0 ty => invert_expr_prop (C r) m | Eaddrof l ty => invert_expr_prop (C r) m | Eunop op r0 ty => invert_expr_prop (C r) m | Ebinop op r1 r2 ty => invert_expr_prop (C r) m | Ecast r0 ty => invert_expr_prop (C r) m | Eseqand r1 r2 ty => invert_expr_prop (C r) m | Eseqor r1 r2 ty => invert_expr_prop (C r) m | Econdition r1 r2 r3 ty => invert_expr_prop (C r) m | Esizeof ty' ty => invert_expr_prop (C r) m | Ealignof ty' ty => invert_expr_prop (C r) m | Eassign l r0 ty => invert_expr_prop (C r) m | Eassignop op l r0 tyres ty => invert_expr_prop (C r) m | Epostincr id l ty => invert_expr_prop (C r) m | Ecomma r1 r2 ty => invert_expr_prop (C r) m | Ecall r1 rargs ty => invert_expr_prop (C r) m | Ebuiltin ef tyargs rargs ty => invert_expr_prop (C r) m | Eloc b ofs ty => True | Eparen r0 tycast ty => invert_expr_prop (C r) m end *)
  red in H. destruct (C l); auto; contradiction.
(* Goal: match C r with | Eval v ty => True | Evar x ty => invert_expr_prop (C r) m | Efield l f ty => invert_expr_prop (C r) m | Evalof l ty => invert_expr_prop (C r) m | Ederef r0 ty => invert_expr_prop (C r) m | Eaddrof l ty => invert_expr_prop (C r) m | Eunop op r0 ty => invert_expr_prop (C r) m | Ebinop op r1 r2 ty => invert_expr_prop (C r) m | Ecast r0 ty => invert_expr_prop (C r) m | Eseqand r1 r2 ty => invert_expr_prop (C r) m | Eseqor r1 r2 ty => invert_expr_prop (C r) m | Econdition r1 r2 r3 ty => invert_expr_prop (C r) m | Esizeof ty' ty => invert_expr_prop (C r) m | Ealignof ty' ty => invert_expr_prop (C r) m | Eassign l r0 ty => invert_expr_prop (C r) m | Eassignop op l r0 tyres ty => invert_expr_prop (C r) m | Epostincr id l ty => invert_expr_prop (C r) m | Ecomma r1 r2 ty => invert_expr_prop (C r) m | Ecall r1 rargs ty => invert_expr_prop (C r) m | Ebuiltin ef tyargs rargs ty => invert_expr_prop (C r) m | Eloc b ofs ty => True | Eparen r0 tycast ty => invert_expr_prop (C r) m end *)
  assert (invert_expr_prop (C r) m).
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
    eapply A; eauto. eapply rred_invert; eauto.
(* Goal: match C r with | Eval v ty => True | Evar x ty => invert_expr_prop (C r) m | Efield l f ty => invert_expr_prop (C r) m | Evalof l ty => invert_expr_prop (C r) m | Ederef r0 ty => invert_expr_prop (C r) m | Eaddrof l ty => invert_expr_prop (C r) m | Eunop op r0 ty => invert_expr_prop (C r) m | Ebinop op r1 r2 ty => invert_expr_prop (C r) m | Ecast r0 ty => invert_expr_prop (C r) m | Eseqand r1 r2 ty => invert_expr_prop (C r) m | Eseqor r1 r2 ty => invert_expr_prop (C r) m | Econdition r1 r2 r3 ty => invert_expr_prop (C r) m | Esizeof ty' ty => invert_expr_prop (C r) m | Ealignof ty' ty => invert_expr_prop (C r) m | Eassign l r0 ty => invert_expr_prop (C r) m | Eassignop op l r0 tyres ty => invert_expr_prop (C r) m | Epostincr id l ty => invert_expr_prop (C r) m | Ecomma r1 r2 ty => invert_expr_prop (C r) m | Ecall r1 rargs ty => invert_expr_prop (C r) m | Ebuiltin ef tyargs rargs ty => invert_expr_prop (C r) m | Eloc b ofs ty => True | Eparen r0 tycast ty => invert_expr_prop (C r) m end *)
  red in H. destruct (C r); auto; contradiction.
(* Goal: match C r with | Eval v ty => True | Evar x ty => invert_expr_prop (C r) m | Efield l f ty => invert_expr_prop (C r) m | Evalof l ty => invert_expr_prop (C r) m | Ederef r0 ty => invert_expr_prop (C r) m | Eaddrof l ty => invert_expr_prop (C r) m | Eunop op r0 ty => invert_expr_prop (C r) m | Ebinop op r1 r2 ty => invert_expr_prop (C r) m | Ecast r0 ty => invert_expr_prop (C r) m | Eseqand r1 r2 ty => invert_expr_prop (C r) m | Eseqor r1 r2 ty => invert_expr_prop (C r) m | Econdition r1 r2 r3 ty => invert_expr_prop (C r) m | Esizeof ty' ty => invert_expr_prop (C r) m | Ealignof ty' ty => invert_expr_prop (C r) m | Eassign l r0 ty => invert_expr_prop (C r) m | Eassignop op l r0 tyres ty => invert_expr_prop (C r) m | Epostincr id l ty => invert_expr_prop (C r) m | Ecomma r1 r2 ty => invert_expr_prop (C r) m | Ecall r1 rargs ty => invert_expr_prop (C r) m | Ebuiltin ef tyargs rargs ty => invert_expr_prop (C r) m | Eloc b ofs ty => True | Eparen r0 tycast ty => invert_expr_prop (C r) m end *)
  assert (invert_expr_prop (C r) m).
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
    eapply A; eauto. eapply callred_invert; eauto.
(* Goal: match C r with | Eval v ty => True | Evar x ty => invert_expr_prop (C r) m | Efield l f ty => invert_expr_prop (C r) m | Evalof l ty => invert_expr_prop (C r) m | Ederef r0 ty => invert_expr_prop (C r) m | Eaddrof l ty => invert_expr_prop (C r) m | Eunop op r0 ty => invert_expr_prop (C r) m | Ebinop op r1 r2 ty => invert_expr_prop (C r) m | Ecast r0 ty => invert_expr_prop (C r) m | Eseqand r1 r2 ty => invert_expr_prop (C r) m | Eseqor r1 r2 ty => invert_expr_prop (C r) m | Econdition r1 r2 r3 ty => invert_expr_prop (C r) m | Esizeof ty' ty => invert_expr_prop (C r) m | Ealignof ty' ty => invert_expr_prop (C r) m | Eassign l r0 ty => invert_expr_prop (C r) m | Eassignop op l r0 tyres ty => invert_expr_prop (C r) m | Epostincr id l ty => invert_expr_prop (C r) m | Ecomma r1 r2 ty => invert_expr_prop (C r) m | Ecall r1 rargs ty => invert_expr_prop (C r) m | Ebuiltin ef tyargs rargs ty => invert_expr_prop (C r) m | Eloc b ofs ty => True | Eparen r0 tycast ty => invert_expr_prop (C r) m end *)
  red in H. destruct (C r); auto; contradiction.
Qed.

(** Soundness: if [step_expr] returns [Some ll], then every element
  of [ll] is a reduct. *)

Lemma context_compose:
  forall k2 k3 C2, context k2 k3 C2 ->
  forall k1 C1, context k1 k2 C1 ->
  context k1 k3 (fun x => C2(C1 x))
with contextlist_compose:
  forall k2 C2, contextlist k2 C2 ->
  forall k1 C1, context k1 k2 C1 ->
  contextlist k1 (fun x => C2(C1 x)).
Proof.
  induction 1; intros; try (constructor; eauto).
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  replace (fun x => C1 x) with C1. auto. apply extensionality; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  induction 1; intros; constructor; eauto.
Qed.

Hint Constructors context contextlist.
Hint Resolve context_compose contextlist_compose.

Definition reduction_ok (k: kind) (a: expr) (m: mem) (rd: reduction) : Prop :=
  match k, rd with
  | LV, Lred _ l' m' => lred ge e a m l' m'
  | RV, Rred _ r' m' t => rred ge a m t r' m' /\ exists w', possible_trace w t w'
  | RV, Callred _ fd args tyres m' => callred ge a m fd args tyres /\ m' = m
  | LV, Stuckred => ~imm_safe_t k a m
  | RV, Stuckred => ~imm_safe_t k a m
  | _, _ => False
  end.

Definition reducts_ok (k: kind) (a: expr) (m: mem) (ll: reducts expr) : Prop :=
  (forall C rd,
      In (C, rd) ll ->
      exists a', exists k', context k' k C /\ a = C a' /\ reduction_ok k' a' m rd)
  /\ (ll = nil -> match k with LV => is_loc a <> None | RV => is_val a <> None end).

Definition list_reducts_ok (al: exprlist) (m: mem) (ll: reducts exprlist) : Prop :=
  (forall C rd,
      In (C, rd) ll ->
      exists a', exists k', contextlist k' C /\ al = C a' /\ reduction_ok k' a' m rd)
  /\ (ll = nil -> is_val_list al <> None).

Ltac monadInv :=
  match goal with
  | [ H: match ?x with Some _ => _ | None => None end = Some ?y |- _ ] =>
      destruct x eqn:?; [monadInv|discriminate]
  | [ H: match ?x with left _ => _ | right _ => None end = Some ?y |- _ ] =>
      destruct x; [monadInv|discriminate]
  | _ => idtac
  end.

Lemma sem_cast_arguments_sound:
  forall m rargs vtl tyargs vargs,
  is_val_list rargs = Some vtl ->
  sem_cast_arguments vtl tyargs m = Some vargs ->
  cast_arguments m rargs tyargs vargs.
Proof.
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  induction rargs; simpl; intros.
(* Goal: imm_safe ge e RV (Eval v ty) m *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  inv H. destruct tyargs; simpl in H0; inv H0. constructor.
(* Goal: @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  monadInv. inv H. simpl in H0. destruct p as [v1 t1]. destruct tyargs; try congruence. monadInv.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  inv H0. rewrite (is_val_inv _ _ _ Heqo). constructor. auto. eauto.
Qed.

Lemma sem_cast_arguments_complete:
  forall m al tyl vl,
  cast_arguments m al tyl vl ->
  exists vtl, is_val_list al = Some vtl /\ sem_cast_arguments vtl tyl m = Some vl.
Proof.
(* Goal: forall (m : Mem.mem) (al : exprlist) (tyl : typelist) (vl : list val) (_ : cast_arguments m al tyl vl), @ex (list (prod val type)) (fun vtl : list (prod val type) => and (@eq (option (list (prod val type))) (is_val_list al) (@Some (list (prod val type)) vtl)) (@eq (option (list val)) (sem_cast_arguments vtl tyl m) (@Some (list val) vl))) *)
  induction 1.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exists (@nil (val * type)); auto.
(* Goal: @ex (list (prod val type)) (fun vtl : list (prod val type) => and (@eq (option (list (prod val type))) (is_val_list (Econs (Eval v ty) el)) (@Some (list (prod val type)) vtl)) (@eq (option (list val)) (sem_cast_arguments vtl (Tcons targ1 targs) m) (@Some (list val) (@cons val v1 vl)))) *)
  destruct IHcast_arguments as [vtl [A B]].
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exists ((v, ty) :: vtl); simpl. rewrite A; rewrite B; rewrite H. auto.
Qed.

Lemma topred_ok:
  forall k a m rd,
  reduction_ok k a m rd ->
  reducts_ok k a m (topred rd).
Proof.
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  intros. unfold topred; split; simpl; intros.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct H0; try contradiction. inv H0. exists a; exists k; auto.
(* Goal: not (@eq (option (list (prod val type))) (is_val_list a) (@None (list (prod val type)))) *)
  congruence.
Qed.

Lemma stuck_ok:
  forall k a m,
  ~imm_safe_t k a m ->
  reducts_ok k a m stuck.
Proof.
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  intros. unfold stuck; split; simpl; intros.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct H0; try contradiction. inv H0. exists a; exists k; intuition. red. destruct k; auto.
(* Goal: not (@eq (option (list (prod val type))) (is_val_list a) (@None (list (prod val type)))) *)
  congruence.
Qed.

Lemma wrong_kind_ok:
  forall k a m,
  k <> Cstrategy.expr_kind a ->
  reducts_ok k a m stuck.
Proof.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  intros. apply stuck_ok. red; intros. exploit Cstrategy.imm_safe_kind; eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply imm_safe_t_imm_safe; eauto.
Qed.

Lemma not_invert_ok:
  forall k a m,
  match a with
  | Eloc _ _ _ => False
  | Eval _ _ => False
  | _ => invert_expr_prop a m -> False
  end ->
  reducts_ok k a m stuck.
Proof.
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  intros. apply stuck_ok. red; intros.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit imm_safe_t_inv; eauto. destruct a; auto.
Qed.

Lemma incontext_ok:
  forall k a m C res k' a',
  reducts_ok k' a' m res ->
  a = C a' ->
  context k' k C ->
  match k' with LV => is_loc a' = None | RV => is_val a' = None end ->
  reducts_ok k a m (incontext C res).
Proof.
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  unfold reducts_ok, incontext; intros. destruct H. split; intros.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit list_in_map_inv; eauto. intros [[C1 rd1] [P Q]]. inv P.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit H; eauto. intros [a'' [k'' [U [V W]]]].
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exists a''; exists k''. split. eapply context_compose; eauto. rewrite V; auto.
(* Goal: not (@eq (option (list (prod val type))) (is_val_list a) (@None (list (prod val type)))) *)
  destruct res; simpl in H4; try congruence. destruct k'; intuition congruence.
Qed.

Lemma incontext2_ok:
  forall k a m k1 a1 res1 k2 a2 res2 C1 C2,
  reducts_ok k1 a1 m res1 ->
  reducts_ok k2 a2 m res2 ->
  a = C1 a1 -> a = C2 a2 ->
  context k1 k C1 -> context k2 k C2 ->
  match k1 with LV => is_loc a1 = None | RV => is_val a1 = None end
  \/ match k2 with LV => is_loc a2 = None | RV => is_val a2 = None end ->
  reducts_ok k a m (incontext2 C1 res1 C2 res2).
Proof.
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  unfold reducts_ok, incontext2, incontext; intros. destruct H; destruct H0; split; intros.
(* Goal: @ex expr (fun a' : expr => @ex kind (fun k' : kind => and (context k' k C) (and (@eq expr a (C a')) (reduction_ok k' a' m rd)))) *)
(* Goal: match k with | LV => not (@eq (option (prod (prod block Ptrofs.int) type)) (is_loc a) (@None (prod (prod block Ptrofs.int) type))) | RV => not (@eq (option (prod val type)) (is_val a) (@None (prod val type))) end *)
  destruct (in_app_or _ _ _ H8).
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit H; eauto. intros [a'' [k'' [U [V W]]]].
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exists a''; exists k''. split. eapply context_compose; eauto. rewrite V; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit H0; eauto. intros [a'' [k'' [U [V W]]]].
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exists a''; exists k''. split. eapply context_compose; eauto. rewrite H2; rewrite V; auto.
(* Goal: not (@eq (option (list (prod val type))) (is_val_list a) (@None (list (prod val type)))) *)
  destruct res1; simpl in H8; try congruence. destruct res2; simpl in H8; try congruence.
(* Goal: not (@eq (option (list (prod val type))) (is_val_list a) (@None (list (prod val type)))) *)
  destruct H5. destruct k1; intuition congruence. destruct k2; intuition congruence.
Qed.

Lemma incontext_list_ok:
  forall ef tyargs al ty m res,
  list_reducts_ok al m res ->
  is_val_list al = None ->
  reducts_ok RV (Ebuiltin ef tyargs al ty) m
                (incontext (fun x => Ebuiltin ef tyargs x ty) res).
Proof.
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  unfold reducts_ok, incontext; intros. destruct H. split; intros.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit list_in_map_inv; eauto. intros [[C1 rd1] [P Q]]. inv P.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit H; eauto. intros [a'' [k'' [U [V W]]]].
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exists a''; exists k''. split. eauto. rewrite V; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct res; simpl in H2. elim H1; auto. congruence.
Qed.

Lemma incontext2_list_ok:
  forall a1 a2 ty m res1 res2,
  reducts_ok RV a1 m res1 ->
  list_reducts_ok a2 m res2 ->
  is_val a1 = None \/ is_val_list a2 = None ->
  reducts_ok RV (Ecall a1 a2 ty) m
               (incontext2 (fun x => Ecall x a2 ty) res1
                           (fun x => Ecall a1 x ty) res2).
Proof.
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  unfold reducts_ok, incontext2, incontext; intros. destruct H; destruct H0; split; intros.
(* Goal: @ex expr (fun a' : expr => @ex kind (fun k' : kind => and (context k' RV C) (and (@eq expr (Ecall a1 a2 ty) (C a')) (reduction_ok k' a' m rd)))) *)
(* Goal: not (@eq (option (prod val type)) (is_val (Ecall a1 a2 ty)) (@None (prod val type))) *)
  destruct (in_app_or _ _ _ H4).
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit H; eauto. intros [a'' [k'' [U [V W]]]].
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exists a''; exists k''. split. eauto. rewrite V; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit H0; eauto. intros [a'' [k'' [U [V W]]]].
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exists a''; exists k''. split. eauto. rewrite V; auto.
(* Goal: not (@eq (option (list (prod val type))) (is_val_list a) (@None (list (prod val type)))) *)
  destruct res1; simpl in H4; try congruence. destruct res2; simpl in H4; try congruence.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  tauto.
Qed.

Lemma incontext2_list_ok':
  forall a1 a2 m res1 res2,
  reducts_ok RV a1 m res1 ->
  list_reducts_ok a2 m res2 ->
  list_reducts_ok (Econs a1 a2) m
               (incontext2 (fun x => Econs x a2) res1
                           (fun x => Econs a1 x) res2).
Proof.
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  unfold reducts_ok, list_reducts_ok, incontext2, incontext; intros.
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  destruct H; destruct H0. split; intros.
(* Goal: @ex expr (fun a' : expr => @ex kind (fun k' : kind => and (contextlist k' C) (and (@eq exprlist (Econs a1 a2) (C a')) (reduction_ok k' a' m rd)))) *)
(* Goal: not (@eq (option (list (prod val type))) (is_val_list (Econs a1 a2)) (@None (list (prod val type)))) *)
  destruct (in_app_or _ _ _ H3).
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit H; eauto. intros [a'' [k'' [U [V W]]]].
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exists a''; exists k''. split. eauto. rewrite V; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit H0; eauto. intros [a'' [k'' [U [V W]]]].
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exists a''; exists k''. split. eauto. rewrite V; auto.
(* Goal: not (@eq (option (list (prod val type))) (is_val_list a) (@None (list (prod val type)))) *)
  destruct res1; simpl in H3; try congruence. destruct res2; simpl in H3; try congruence.
(* Goal: not (@eq (option (list (prod val type))) (is_val_list a) (@None (list (prod val type)))) *)
  simpl. destruct (is_val a1). destruct (is_val_list a2). congruence. intuition congruence. intuition congruence.
Qed.

Lemma is_val_list_all_values:
  forall al vtl, is_val_list al = Some vtl -> exprlist_all_values al.
Proof.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  induction al; simpl; intros. auto.
(* Goal: match r1 with | Eval v ty => exprlist_all_values al | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
  destruct (is_val r1) as [[v ty]|] eqn:?; try discriminate.
(* Goal: match r1 with | Eval v ty => exprlist_all_values al | Evar x ty => False | Efield l f ty => False | Evalof l ty => False | Ederef r ty => False | Eaddrof l ty => False | Eunop op r ty => False | Ebinop op r1 r2 ty => False | Ecast r ty => False | Eseqand r1 r2 ty => False | Eseqor r1 r2 ty => False | Econdition r1 r2 r3 ty => False | Esizeof ty' ty => False | Ealignof ty' ty => False | Eassign l r ty => False | Eassignop op l r tyres ty => False | Epostincr id l ty => False | Ecomma r1 r2 ty => False | Ecall r1 rargs ty => False | Ebuiltin ef tyargs rargs ty => False | Eloc b ofs ty => False | Eparen r tycast ty => False end *)
  destruct (is_val_list al) as [vtl'|] eqn:?; try discriminate.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  rewrite (is_val_inv _ _ _ Heqo). eauto.
Qed.

Ltac myinv :=
  match goal with
  | [ H: False |- _ ] => destruct H
  | [ H: _ /\ _ |- _ ] => destruct H; myinv
  | [ H: exists _, _ |- _ ] => destruct H; myinv
  | _ => idtac
  end.

Theorem step_expr_sound:
  forall a k m, reducts_ok k a m (step_expr k a m)
with step_exprlist_sound:
  forall al m, list_reducts_ok al m (step_exprlist al m).
Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; fail)).
  induction a; intros; simpl; destruct k; try (apply wrong_kind_ok; simpl; congruence).
(* Eval *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  split; intros. tauto. simpl; congruence.
(* Evar *)
  destruct (e!x) as [[b ty']|] eqn:?.
  destruct (type_eq ty ty')...
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  subst. apply topred_ok; auto. apply red_var_local; auto.
  destruct (Genv.find_symbol ge x) as [b|] eqn:?...
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply topred_ok; auto. apply red_var_global; auto.
(* Efield *)
  destruct (is_val a) as [[v ty'] | ] eqn:?.
(* Goal: @eq (reducts exprlist) (@incontext2 expr exprlist exprlist (fun x : expr => Econs x al) (step_expr RV r1 m) (fun x : exprlist => Econs r1 x) (step_exprlist al m)) (@nil (prod (forall _ : expr, exprlist) reduction)) *)
  rewrite (is_val_inv _ _ _ Heqo).
  destruct v...
  destruct ty'...
  (* top struct *)
  destruct (ge.(genv_cenv)!i0) as [co|] eqn:?...
  destruct (field_offset ge f (co_members co)) as [delta|] eqn:?...
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply topred_ok; auto. eapply red_field_struct; eauto.
  (* top union *)
  destruct (ge.(genv_cenv)!i0) as [co|] eqn:?...
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply topred_ok; auto. eapply red_field_union; eauto.
  (* in depth *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply incontext_ok; eauto.
(* Evalof *)
  destruct (is_loc a) as [[[b ofs] ty'] | ] eqn:?. rewrite (is_loc_inv _ _ _ _ Heqo).
  (* top *)
  destruct (type_eq ty ty')... subst ty'.
  destruct (do_deref_loc w ty m b ofs) as [[[w' t] v] | ] eqn:?.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit do_deref_loc_sound; eauto. intros [A B].
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply topred_ok; auto. red. split. apply red_rvalof; auto. exists w'; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply not_invert_ok; simpl; intros; myinv. exploit do_deref_loc_complete; eauto. congruence.
  (* depth *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply incontext_ok; eauto.
(* Ederef *)
(* Goal: @eq (reducts exprlist) (@incontext2 expr exprlist exprlist (fun x : expr => Econs x al) (step_expr RV r1 m) (fun x : exprlist => Econs r1 x) (step_exprlist al m)) (@nil (prod (forall _ : expr, exprlist) reduction)) *)
  destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo).
  (* top *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct v... apply topred_ok; auto. apply red_deref; auto.
  (* depth *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply incontext_ok; eauto.
(* Eaddrof *)
  destruct (is_loc a) as [[[b ofs] ty'] | ] eqn:?. rewrite (is_loc_inv _ _ _ _ Heqo).
  (* top *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply topred_ok; auto. split. apply red_addrof; auto. exists w; constructor.
  (* depth *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply incontext_ok; eauto.
(* unop *)
(* Goal: @eq (reducts exprlist) (@incontext2 expr exprlist exprlist (fun x : expr => Econs x al) (step_expr RV r1 m) (fun x : exprlist => Econs r1 x) (step_exprlist al m)) (@nil (prod (forall _ : expr, exprlist) reduction)) *)
  destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo).
  (* top *)
  destruct (sem_unary_operation op v ty' m) as [v'|] eqn:?...
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply topred_ok; auto. split. apply red_unop; auto. exists w; constructor.
  (* depth *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply incontext_ok; eauto.
(* binop *)
  destruct (is_val a1) as [[v1 ty1] | ] eqn:?.
  destruct (is_val a2) as [[v2 ty2] | ] eqn:?.
(* Goal: @eq (reducts exprlist) (@incontext2 expr exprlist exprlist (fun x : expr => Econs x al) (step_expr RV r1 m) (fun x : exprlist => Econs r1 x) (step_exprlist al m)) (@nil (prod (forall _ : expr, exprlist) reduction)) *)
  rewrite (is_val_inv _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0).
  (* top *)
  destruct (sem_binary_operation ge op v1 ty1 v2 ty2 m) as [v|] eqn:?...
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply topred_ok; auto. split. apply red_binop; auto. exists w; constructor.
  (* depth *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply incontext2_ok; eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply incontext2_ok; eauto.
(* cast *)
(* Goal: @eq (reducts exprlist) (@incontext2 expr exprlist exprlist (fun x : expr => Econs x al) (step_expr RV r1 m) (fun x : exprlist => Econs r1 x) (step_exprlist al m)) (@nil (prod (forall _ : expr, exprlist) reduction)) *)
  destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo).
  (* top *)
  destruct (sem_cast v ty' ty m) as [v'|] eqn:?...
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply topred_ok; auto. split. apply red_cast; auto. exists w; constructor.
  (* depth *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply incontext_ok; eauto.
(* seqand *)
(* Goal: @eq (reducts exprlist) (@incontext2 expr exprlist exprlist (fun x : expr => Econs x al) (step_expr RV r1 m) (fun x : exprlist => Econs r1 x) (step_exprlist al m)) (@nil (prod (forall _ : expr, exprlist) reduction)) *)
  destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo).
  (* top *)
  destruct (bool_val v ty' m) as [v'|] eqn:?... destruct v'.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply topred_ok; auto. split. eapply red_seqand_true; eauto. exists w; constructor.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply topred_ok; auto. split. eapply red_seqand_false; eauto. exists w; constructor.
  (* depth *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply incontext_ok; eauto.
(* seqor *)
(* Goal: @eq (reducts exprlist) (@incontext2 expr exprlist exprlist (fun x : expr => Econs x al) (step_expr RV r1 m) (fun x : exprlist => Econs r1 x) (step_exprlist al m)) (@nil (prod (forall _ : expr, exprlist) reduction)) *)
  destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo).
  (* top *)
  destruct (bool_val v ty' m) as [v'|] eqn:?... destruct v'.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply topred_ok; auto. split. eapply red_seqor_true; eauto. exists w; constructor.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply topred_ok; auto. split. eapply red_seqor_false; eauto. exists w; constructor.
  (* depth *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply incontext_ok; eauto.
(* condition *)
(* Goal: @eq (reducts exprlist) (@incontext2 expr exprlist exprlist (fun x : expr => Econs x al) (step_expr RV r1 m) (fun x : exprlist => Econs r1 x) (step_exprlist al m)) (@nil (prod (forall _ : expr, exprlist) reduction)) *)
  destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo).
  (* top *)
  destruct (bool_val v ty' m) as [v'|] eqn:?...
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply topred_ok; auto. split. eapply red_condition; eauto. exists w; constructor.
  (* depth *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply incontext_ok; eauto.
(* sizeof *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply topred_ok; auto. split. apply red_sizeof. exists w; constructor.
(* alignof *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply topred_ok; auto. split. apply red_alignof. exists w; constructor.
(* assign *)
  destruct (is_loc a1) as [[[b ofs] ty1] | ] eqn:?.
  destruct (is_val a2) as [[v2 ty2] | ] eqn:?.
  rewrite (is_loc_inv _ _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0).
  (* top *)
  destruct (type_eq ty1 ty)... subst ty1.
  destruct (sem_cast v2 ty2 ty m) as [v|] eqn:?...
  destruct (do_assign_loc w ty m b ofs v) as [[[w' t] m']|] eqn:?.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit do_assign_loc_sound; eauto. intros [P Q].
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply topred_ok; auto. split. apply red_assign; auto. exists w'; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply not_invert_ok; simpl; intros; myinv. exploit do_assign_loc_complete; eauto. congruence.
  (* depth *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply incontext2_ok; eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply incontext2_ok; eauto.
(* assignop *)
  destruct (is_loc a1) as [[[b ofs] ty1] | ] eqn:?.
  destruct (is_val a2) as [[v2 ty2] | ] eqn:?.
  rewrite (is_loc_inv _ _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0).
  (* top *)
  destruct (type_eq ty1 ty)... subst ty1.
  destruct (do_deref_loc w ty m b ofs) as [[[w' t] v] | ] eqn:?.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit do_deref_loc_sound; eauto. intros [A B].
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply topred_ok; auto. red. split. apply red_assignop; auto. exists w'; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply not_invert_ok; simpl; intros; myinv. exploit do_deref_loc_complete; eauto. congruence.
  (* depth *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply incontext2_ok; eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply incontext2_ok; eauto.
(* postincr *)
  destruct (is_loc a) as [[[b ofs] ty'] | ] eqn:?. rewrite (is_loc_inv _ _ _ _ Heqo).
  (* top *)
  destruct (type_eq ty' ty)... subst ty'.
  destruct (do_deref_loc w ty m b ofs) as [[[w' t] v] | ] eqn:?.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit do_deref_loc_sound; eauto. intros [A B].
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply topred_ok; auto. red. split. apply red_postincr; auto. exists w'; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply not_invert_ok; simpl; intros; myinv. exploit do_deref_loc_complete; eauto. congruence.
  (* depth *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply incontext_ok; eauto.
(* comma *)
(* Goal: @eq (reducts exprlist) (@incontext2 expr exprlist exprlist (fun x : expr => Econs x al) (step_expr RV r1 m) (fun x : exprlist => Econs r1 x) (step_exprlist al m)) (@nil (prod (forall _ : expr, exprlist) reduction)) *)
  destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo).
  (* top *)
  destruct (type_eq (typeof a2) ty)... subst ty.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply topred_ok; auto. split. apply red_comma; auto. exists w; constructor.
  (* depth *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply incontext_ok; eauto.
(* call *)
  destruct (is_val a) as [[vf tyf] | ] eqn:?.
  destruct (is_val_list rargs) as [vtl | ] eqn:?.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  rewrite (is_val_inv _ _ _ Heqo). exploit is_val_list_all_values; eauto. intros ALLVAL.
  (* top *)
  destruct (classify_fun tyf) as [tyargs tyres cconv|] eqn:?...
  destruct (Genv.find_funct ge vf) as [fd|] eqn:?...
  destruct (sem_cast_arguments vtl tyargs m) as [vargs|] eqn:?...
  destruct (type_eq (type_of_fundef fd) (Tfunction tyargs tyres cconv))...
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply topred_ok; auto. red. split; auto. eapply red_call; eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply sem_cast_arguments_sound; eauto.
(* Goal: not (@eq (option (list (prod val type))) (is_val_list a) (@None (list (prod val type)))) *)
  apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv. congruence.
  apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit sem_cast_arguments_complete; eauto. intros [vtl' [P Q]]. congruence.
(* Goal: not (@eq (option (list (prod val type))) (is_val_list a) (@None (list (prod val type)))) *)
  apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv. congruence.
(* Goal: not (@eq (option (list (prod val type))) (is_val_list a) (@None (list (prod val type)))) *)
  apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv. congruence.
  (* depth *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply incontext2_list_ok; eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply incontext2_list_ok; eauto.
(* builtin *)
  destruct (is_val_list rargs) as [vtl | ] eqn:?.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit is_val_list_all_values; eauto. intros ALLVAL.
  (* top *)
  destruct (sem_cast_arguments vtl tyargs m) as [vargs|] eqn:?...
  destruct (do_external ef w vargs m) as [[[[? ?] v] m'] | ] eqn:?...
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit do_ef_external_sound; eauto. intros [EC PT].
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply topred_ok; auto. red. split; auto. eapply red_builtin; eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply sem_cast_arguments_sound; eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exists w0; auto.
  apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv.
  assert (x = vargs).
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
    exploit sem_cast_arguments_complete; eauto. intros [vtl' [A B]]. congruence.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  subst x. exploit do_ef_external_complete; eauto. congruence.
  apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit sem_cast_arguments_complete; eauto. intros [vtl' [A B]]. congruence.
  (* depth *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply incontext_list_ok; eauto.

(* loc *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  split; intros. tauto. simpl; congruence.
(* paren *)
(* Goal: @eq (reducts exprlist) (@incontext2 expr exprlist exprlist (fun x : expr => Econs x al) (step_expr RV r1 m) (fun x : exprlist => Econs r1 x) (step_exprlist al m)) (@nil (prod (forall _ : expr, exprlist) reduction)) *)
  destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo).
  (* top *)
  destruct (sem_cast v ty' tycast m) as [v'|] eqn:?...
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply topred_ok; auto. split. apply red_paren; auto. exists w; constructor.
  (* depth *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply incontext_ok; eauto.

(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  induction al; simpl; intros.
(* nil *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  split; intros. tauto. simpl; congruence.
(* cons *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply incontext2_list_ok'; eauto.
Qed.

Lemma step_exprlist_val_list:
  forall m al, is_val_list al <> None -> step_exprlist al m = nil.
Proof.
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  induction al; simpl; intros.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  auto.
(* Goal: not (@eq (option (list (prod val type))) (is_val_list a) (@None (list (prod val type)))) *)
  destruct (is_val r1) as [[v1 ty1]|] eqn:?; try congruence.
(* Goal: not (@eq (option (list (prod val type))) (is_val_list a) (@None (list (prod val type)))) *)
  destruct (is_val_list al) eqn:?; try congruence.
(* Goal: @eq (reducts exprlist) (@incontext2 expr exprlist exprlist (fun x : expr => Econs x al) (step_expr RV r1 m) (fun x : exprlist => Econs r1 x) (step_exprlist al m)) (@nil (prod (forall _ : expr, exprlist) reduction)) *)
  rewrite (is_val_inv _ _ _ Heqo).
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  rewrite IHal. auto. congruence.
Qed.

(** Completeness part 1: [step_expr] contains all possible non-error reducts. *)

Lemma lred_topred:
  forall l1 m1 l2 m2,
  lred ge e l1 m1 l2 m2 ->
  exists rule, step_expr LV l1 m1 = topred (Lred rule l2 m2).
Proof.
(* Goal: forall (e1 : env) (m1 : Mem.mem) (l : list (prod ident type)) (e2 : env) (m2 : Mem.mem) (_ : alloc_variables ge e1 m1 l e2 m2), @eq (prod env Mem.mem) (do_alloc_variables e1 m1 l) (@pair env Mem.mem e2 m2) *)
  induction 1; simpl.
(* var local *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  rewrite H. rewrite dec_eq_true. econstructor; eauto.
(* var global *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  rewrite H; rewrite H0. econstructor; eauto.
(* deref *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  econstructor; eauto.
(* field struct *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  rewrite H, H0; econstructor; eauto.
(* field union *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  rewrite H; econstructor; eauto.
Qed.

Lemma rred_topred:
  forall w' r1 m1 t r2 m2,
  rred ge r1 m1 t r2 m2 -> possible_trace w t w' ->
  exists rule, step_expr RV r1 m1 = topred (Rred rule r2 m2 t).
Proof.
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  induction 1; simpl; intros.
(* valof *)
(* Goal: @eq (option Mem.mem) (if type_eq ty ty then match do_assign_loc w ty m b Ptrofs.zero v1 with | Some (pair (pair w' (nil as t) as p0) m1 as p) => sem_bind_parameters w e m1 params vl | Some (pair (pair w' (cons e l as t) as p0) m1 as p) => @None Mem.mem | None => @None Mem.mem end else @None Mem.mem) (@Some Mem.mem m2) *)
  rewrite dec_eq_true.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H0). econstructor; eauto.
(* addrof *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  inv H. econstructor; eauto.
(* unop *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  inv H0. rewrite H; econstructor; eauto.
(* binop *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  inv H0. rewrite H; econstructor; eauto.
(* cast *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  inv H0. rewrite H; econstructor; eauto.
(* seqand *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  inv H0. rewrite H; econstructor; eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  inv H0. rewrite H; econstructor; eauto.
(* seqor *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  inv H0. rewrite H; econstructor; eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  inv H0. rewrite H; econstructor; eauto.
(* condition *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  inv H0. rewrite H; econstructor; eauto.
(* sizeof *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  inv H. econstructor; eauto.
(* alignof *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  inv H. econstructor; eauto.
(* assign *)
(* Goal: @eq (option Mem.mem) (if type_eq ty ty then match do_assign_loc w ty m b Ptrofs.zero v1 with | Some (pair (pair w' (nil as t) as p0) m1 as p) => sem_bind_parameters w e m1 params vl | Some (pair (pair w' (cons e l as t) as p0) m1 as p) => @None Mem.mem | None => @None Mem.mem end else @None Mem.mem) (@Some Mem.mem m2) *)
  rewrite dec_eq_true. rewrite H. rewrite (do_assign_loc_complete _ _ _ _ _ _ _ _ _ H0 H1).
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  econstructor; eauto.
(* assignop *)
(* Goal: @eq (option Mem.mem) (if type_eq ty ty then match do_assign_loc w ty m b Ptrofs.zero v1 with | Some (pair (pair w' (nil as t) as p0) m1 as p) => sem_bind_parameters w e m1 params vl | Some (pair (pair w' (cons e l as t) as p0) m1 as p) => @None Mem.mem | None => @None Mem.mem end else @None Mem.mem) (@Some Mem.mem m2) *)
  rewrite dec_eq_true. rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H0).
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  econstructor; eauto.
(* postincr *)
(* Goal: @eq (option Mem.mem) (if type_eq ty ty then match do_assign_loc w ty m b Ptrofs.zero v1 with | Some (pair (pair w' (nil as t) as p0) m1 as p) => sem_bind_parameters w e m1 params vl | Some (pair (pair w' (cons e l as t) as p0) m1 as p) => @None Mem.mem | None => @None Mem.mem end else @None Mem.mem) (@Some Mem.mem m2) *)
  rewrite dec_eq_true. subst. rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H1).
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  econstructor; eauto.
(* comma *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  inv H0. rewrite dec_eq_true. econstructor; eauto.
(* paren *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  inv H0. rewrite H; econstructor; eauto.
(* builtin *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit sem_cast_arguments_complete; eauto. intros [vtl [A B]].
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit do_ef_external_complete; eauto. intros C.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  rewrite A. rewrite B. rewrite C. econstructor; eauto.
Qed.

Lemma callred_topred:
  forall a fd args ty m,
  callred ge a m fd args ty ->
  exists rule, step_expr RV a m = topred (Callred rule fd args ty m).
Proof.
(* Goal: forall (e1 : env) (m1 : Mem.mem) (l : list (prod ident type)) (e2 : env) (m2 : Mem.mem) (_ : alloc_variables ge e1 m1 l e2 m2), @eq (prod env Mem.mem) (do_alloc_variables e1 m1 l) (@pair env Mem.mem e2 m2) *)
  induction 1; simpl.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  rewrite H2. exploit sem_cast_arguments_complete; eauto. intros [vtl [A B]].
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  rewrite A; rewrite H; rewrite B; rewrite H1; rewrite dec_eq_true. econstructor; eauto.
Qed.

Definition reducts_incl {A B: Type} (C: A -> B) (res1: reducts A) (res2: reducts B) : Prop :=
  forall C1 rd, In (C1, rd) res1 -> In ((fun x => C(C1 x)), rd) res2.

Lemma reducts_incl_trans:
  forall (A1 A2: Type) (C: A1 -> A2) res1 res2, reducts_incl C res1 res2 ->
  forall (A3: Type) (C': A2 -> A3) res3,
  reducts_incl C' res2 res3 ->
  reducts_incl (fun x => C'(C x)) res1 res3.
Proof.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  unfold reducts_incl; intros. auto.
Qed.

Lemma reducts_incl_nil:
  forall (A B: Type) (C: A -> B) res,
  reducts_incl C nil res.
Proof.
(* Goal: reduction_ok k a m Stuckred *)
(* Goal: match k with | LV => not (@eq (option (prod (prod block Ptrofs.int) type)) (is_loc a) (@None (prod (prod block Ptrofs.int) type))) | RV => not (@eq (option (prod val type)) (is_val a) (@None (prod val type))) end *)
  intros; red. intros; contradiction.
Qed.

Lemma reducts_incl_val:
  forall (A: Type) a m v ty (C: expr -> A) res,
  is_val a = Some(v, ty) -> reducts_incl C (step_expr RV a m) res.
Proof.
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  intros. rewrite (is_val_inv _ _ _ H). apply reducts_incl_nil.
Qed.

Lemma reducts_incl_loc:
  forall (A: Type) a m b ofs ty (C: expr -> A) res,
  is_loc a = Some(b, ofs, ty) -> reducts_incl C (step_expr LV a m) res.
Proof.
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  intros. rewrite (is_loc_inv _ _ _ _ H). apply reducts_incl_nil.
Qed.

Lemma reducts_incl_listval:
  forall (A: Type) a m vtl (C: exprlist -> A) res,
  is_val_list a = Some vtl -> reducts_incl C (step_exprlist a m) res.
Proof.
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  intros. rewrite step_exprlist_val_list. apply reducts_incl_nil. congruence.
Qed.

Lemma reducts_incl_incontext:
  forall (A B: Type) (C: A -> B) res,
  reducts_incl C res (incontext C res).
Proof.
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  unfold reducts_incl, incontext. intros.
  set (f := fun z : (expr -> A) * reduction => (fun x : expr => C (fst z x), snd z)).
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  change (In (f (C1, rd)) (map f res)). apply in_map. auto.
Qed.

Lemma reducts_incl_incontext2_left:
  forall (A1 A2 B: Type) (C1: A1 -> B) res1 (C2: A2 -> B) res2,
  reducts_incl C1 res1 (incontext2 C1 res1 C2 res2).
Proof.
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  unfold reducts_incl, incontext2, incontext. intros.
(* Goal: @In (prod (forall _ : expr, B) reduction) (@pair (forall _ : expr, B) reduction (fun x : expr => C2 (C0 x)) rd) (@app (prod (forall _ : expr, B) reduction) (@map (prod (forall _ : expr, A1) reduction) (prod (forall _ : expr, B) reduction) (fun z : prod (forall _ : expr, A1) reduction => @pair (forall _ : expr, B) reduction (fun x : expr => C1 (@fst (forall _ : expr, A1) reduction z x)) (@snd (forall _ : expr, A1) reduction z)) res1) (@map (prod (forall _ : expr, A2) reduction) (prod (forall _ : expr, B) reduction) (fun z : prod (forall _ : expr, A2) reduction => @pair (forall _ : expr, B) reduction (fun x : expr => C2 (@fst (forall _ : expr, A2) reduction z x)) (@snd (forall _ : expr, A2) reduction z)) res2)) *)
  rewrite in_app_iff. left.
  set (f := fun z : (expr -> A1) * reduction => (fun x : expr => C1 (fst z x), snd z)).
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  change (In (f (C0, rd)) (map f res1)). apply in_map; auto.
Qed.

Lemma reducts_incl_incontext2_right:
  forall (A1 A2 B: Type) (C1: A1 -> B) res1 (C2: A2 -> B) res2,
  reducts_incl C2 res2 (incontext2 C1 res1 C2 res2).
Proof.
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  unfold reducts_incl, incontext2, incontext. intros.
(* Goal: @In (prod (forall _ : expr, B) reduction) (@pair (forall _ : expr, B) reduction (fun x : expr => C2 (C0 x)) rd) (@app (prod (forall _ : expr, B) reduction) (@map (prod (forall _ : expr, A1) reduction) (prod (forall _ : expr, B) reduction) (fun z : prod (forall _ : expr, A1) reduction => @pair (forall _ : expr, B) reduction (fun x : expr => C1 (@fst (forall _ : expr, A1) reduction z x)) (@snd (forall _ : expr, A1) reduction z)) res1) (@map (prod (forall _ : expr, A2) reduction) (prod (forall _ : expr, B) reduction) (fun z : prod (forall _ : expr, A2) reduction => @pair (forall _ : expr, B) reduction (fun x : expr => C2 (@fst (forall _ : expr, A2) reduction z x)) (@snd (forall _ : expr, A2) reduction z)) res2)) *)
  rewrite in_app_iff. right.
  set (f := fun z : (expr -> A2) * reduction => (fun x : expr => C2 (fst z x), snd z)).
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  change (In (f (C0, rd)) (map f res2)). apply in_map; auto.
Qed.

Hint Resolve reducts_incl_val reducts_incl_loc reducts_incl_listval
(* Goal: or (imm_safe_t k (C e0) m) (@ex (forall _ : expr, expr) (fun C0 : forall _ : expr, expr => @ex expr (fun a1 : expr => @ex trace (fun t : trace => @ex expr (fun a1' : expr => @ex Mem.mem (fun m' : Mem.mem => and (context RV k C0) (and (@eq expr (C e0) (C0 a1)) (and (rred ge a1 m t a1' m') (forall w' : world, not (possible_trace w t w')))))))))) *)
(* Goal: or (imm_safe_t k (C e0) m) (@ex (forall _ : expr, expr) (fun C0 : forall _ : expr, expr => @ex expr (fun a1 : expr => @ex trace (fun t : trace => @ex expr (fun a1' : expr => @ex Mem.mem (fun m' : Mem.mem => and (context RV k C0) (and (@eq expr (C e0) (C0 a1)) (and (rred ge a1 m t a1' m') (forall w' : world, not (possible_trace w t w')))))))))) *)
             reducts_incl_incontext reducts_incl_incontext2_left reducts_incl_incontext2_right.

Lemma step_expr_context:
  forall from to C, context from to C ->
  forall a m, reducts_incl C (step_expr from a m) (step_expr to (C a) m)
with step_exprlist_context:
  forall from C, contextlist from C ->
  forall a m, reducts_incl C (step_expr from a m) (step_exprlist (C a) m).
Proof.
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  induction 1; simpl; intros.
(* top *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  red. destruct (step_expr k a m); auto.
  try (* no eta in 8.3 *)
   (intros;
    replace (fun x => C1 x) with C1 by (apply extensionality; auto);
    auto).
(* deref *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply reducts_incl_trans with (C' := fun x => Ederef x ty); eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto.
(* field *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply reducts_incl_trans with (C' := fun x => Efield x f ty); eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto.
(* valof *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply reducts_incl_trans with (C' := fun x => Evalof x ty); eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (is_loc (C a)) as [[[b ofs] ty']|] eqn:?; eauto.
(* addrof *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply reducts_incl_trans with (C' := fun x => Eaddrof x ty); eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (is_loc (C a)) as [[[b ofs] ty']|] eqn:?; eauto.
(* unop *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply reducts_incl_trans with (C' := fun x => Eunop op x ty); eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto.
(* binop left *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply reducts_incl_trans with (C' := fun x => Ebinop op x e2 ty); eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto.
(* binop right *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply reducts_incl_trans with (C' := fun x => Ebinop op e1 x ty); eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (is_val e1) as [[v1 ty1]|] eqn:?; eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (is_val (C a)) as [[v2 ty2]|] eqn:?; eauto.
(* cast *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply reducts_incl_trans with (C' := fun x => Ecast x ty); eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto.
(* seqand *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply reducts_incl_trans with (C' := fun x => Eseqand x r2 ty); eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto.
(* seqor *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply reducts_incl_trans with (C' := fun x => Eseqor x r2 ty); eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto.
(* condition *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply reducts_incl_trans with (C' := fun x => Econdition x r2 r3 ty); eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto.
(* assign left *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply reducts_incl_trans with (C' := fun x => Eassign x e2 ty); eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (is_loc (C a)) as [[[b ofs] ty']|] eqn:?; eauto.
(* assign right *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply reducts_incl_trans with (C' := fun x => Eassign e1 x ty); eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (is_loc e1) as [[[b ofs] ty1]|] eqn:?; eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (is_val (C a)) as [[v2 ty2]|] eqn:?; eauto.
(* assignop left *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply reducts_incl_trans with (C' := fun x => Eassignop op x e2 tyres ty); eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (is_loc (C a)) as [[[b ofs] ty']|] eqn:?; eauto.
(* assignop right *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply reducts_incl_trans with (C' := fun x => Eassignop op e1 x tyres ty); eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (is_loc e1) as [[[b ofs] ty1]|] eqn:?; eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (is_val (C a)) as [[v2 ty2]|] eqn:?; eauto.
(* postincr *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply reducts_incl_trans with (C' := fun x => Epostincr id x ty); eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (is_loc (C a)) as [[[b ofs] ty']|] eqn:?; eauto.
(* call left *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply reducts_incl_trans with (C' := fun x => Ecall x el ty); eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto.
(* call right *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply reducts_incl_trans with (C' := fun x => Ecall e1 x ty). apply step_exprlist_context. auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (is_val e1) as [[v1 ty1]|] eqn:?; eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (is_val_list (C a)) as [vl|] eqn:?; eauto.
(* builtin *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply reducts_incl_trans with (C' := fun x => Ebuiltin ef tyargs x ty). apply step_exprlist_context. auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (is_val_list (C a)) as [vl|] eqn:?; eauto.
(* comma *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply reducts_incl_trans with (C' := fun x => Ecomma x e2 ty); eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto.
(* paren *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply reducts_incl_trans with (C' := fun x => Eparen x tycast ty); eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto.

(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  induction 1; simpl; intros.
(* cons left *)
  eapply reducts_incl_trans with (C' := fun x => Econs x el).
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply step_expr_context; eauto. eauto.
(* binop right *)
  eapply reducts_incl_trans with (C' := fun x => Econs e1 x).
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply step_exprlist_context; eauto. eauto.
Qed.

(** Completeness part 2: if we can reduce to [Stuckstate], [step_expr]
    contains at least one [Stuckred] reduction. *)

Lemma not_stuckred_imm_safe:
  forall m a k,
  (forall C, ~In (C, Stuckred) (step_expr k a m)) -> imm_safe_t k a m.
Proof.
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  intros. generalize (step_expr_sound a k m). intros [A B].
  destruct (step_expr k a m) as [|[C rd] res] eqn:?.
  specialize (B (eq_refl _)). destruct k.
(* Goal: imm_safe ge e RV (Eval v ty) m *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct a; simpl in B; try congruence. constructor.
(* Goal: imm_safe ge e RV (Eval v ty) m *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct a; simpl in B; try congruence. constructor.
  assert (NOTSTUCK: rd <> Stuckred).
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
    red; intros. elim (H C); subst rd; auto with coqlib.
  exploit A. eauto with coqlib. intros [a' [k' [P [Q R]]]].
(* Goal: forall _ : and (volatile_store (@Genv.to_senv fundef type (genv_genv ge)) m0 m b ofs v t m') (possible_trace w t w'), and (assign_loc ge ty m b ofs v t m') (possible_trace w t w') *)
(* Goal: and (assign_loc ge ty m b ofs v E0 m') (possible_trace w' E0 w') *)
(* Goal: forall _ : @eq (option (prod (prod world trace) Mem.mem)) match v with | Vundef => @None (prod (prod world trace) Mem.mem) | Vint i => @None (prod (prod world trace) Mem.mem) | Vlong i => @None (prod (prod world trace) Mem.mem) | Vfloat f => @None (prod (prod world trace) Mem.mem) | Vsingle f => @None (prod (prod world trace) Mem.mem) | Vptr b' ofs' => if check_assign_copy ty b ofs b' ofs' then match Mem.loadbytes m b' (Ptrofs.unsigned ofs') (sizeof (genv_cenv ge) ty) with | Some bytes => match Mem.storebytes m b (Ptrofs.unsigned ofs) bytes with | Some m' => @Some (prod (prod world trace) Mem.mem) (@pair (prod world trace) Mem.mem (@pair world trace w E0) m') | None => @None (prod (prod world trace) Mem.mem) end | None => @None (prod (prod world trace) Mem.mem) end else @None (prod (prod world trace) Mem.mem) end (@Some (prod (prod world trace) Mem.mem) (@pair (prod world trace) Mem.mem (@pair world trace w' t) m')), and (assign_loc ge ty m b ofs v t m') (possible_trace w t w') *)
  destruct k'; destruct rd; simpl in R; intuition.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  subst a. eapply imm_safe_t_lred; eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  subst a. destruct H1 as [w' PT]. eapply imm_safe_t_rred; eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  subst. eapply imm_safe_t_callred; eauto.
Qed.

Lemma not_imm_safe_stuck_red:
  forall m a k C,
  context k RV C ->
  ~imm_safe_t k a m ->
  exists C', In (C', Stuckred) (step_expr RV (C a) m).
Proof.
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  intros.
(* Goal: @ex (forall _ : expr, expr) (fun C' : forall _ : expr, expr => @In (prod (forall _ : expr, expr) reduction) (@pair (forall _ : expr, expr) reduction C' Stuckred) (step_expr RV (C a) m)) *)
  assert (exists C', In (C', Stuckred) (step_expr k a m)).
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
    destruct (classic (exists C', In (C', Stuckred) (step_expr k a m))); auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
    elim H0. apply not_stuckred_imm_safe. apply not_ex_all_not. auto.
(* Goal: @ex (forall _ : expr, expr) (fun C' : forall _ : expr, expr => @In (prod (forall _ : expr, expr) reduction) (@pair (forall _ : expr, expr) reduction C' Stuckred) (step_expr RV (C a) m)) *)
  destruct H1 as [C' IN].
(* Goal: @ex (forall _ : expr, expr) (fun C' : forall _ : expr, expr => @In (prod (forall _ : expr, expr) reduction) (@pair (forall _ : expr, expr) reduction C' Stuckred) (step_expr RV (C a) m)) *)
  specialize (step_expr_context _ _ _ H a m). unfold reducts_incl.
(* Goal: forall _ : forall (C1 : forall _ : expr, expr) (rd : reduction) (_ : @In (prod (forall _ : expr, expr) reduction) (@pair (forall _ : expr, expr) reduction C1 rd) (step_expr k a m)), @In (prod (forall _ : expr, expr) reduction) (@pair (forall _ : expr, expr) reduction (fun x : expr => C (C1 x)) rd) (step_expr RV (C a) m), @ex (forall _ : expr, expr) (fun C' : forall _ : expr, expr => @In (prod (forall _ : expr, expr) reduction) (@pair (forall _ : expr, expr) reduction C' Stuckred) (step_expr RV (C a) m)) *)
  intro.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exists (fun x => (C (C' x))). apply H1; auto.
Qed.

(** Connections between [imm_safe_t] and [imm_safe] *)

Lemma imm_safe_imm_safe_t:
  forall k a m,
  imm_safe ge e k a m ->
  imm_safe_t k a m \/
  exists C, exists a1, exists t, exists a1', exists m',
    context RV k C /\ a = C a1 /\ rred ge a1 m t a1' m' /\ forall w', ~possible_trace w t w'.
Proof.
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  intros. inv H.
(* Goal: or (imm_safe_t k (C e0) m) (@ex (forall _ : expr, expr) (fun C0 : forall _ : expr, expr => @ex expr (fun a1 : expr => @ex trace (fun t : trace => @ex expr (fun a1' : expr => @ex Mem.mem (fun m' : Mem.mem => and (context RV k C0) (and (@eq expr (C e0) (C0 a1)) (and (rred ge a1 m t a1' m') (forall w' : world, not (possible_trace w t w')))))))))) *)
  left. apply imm_safe_t_val.
(* Goal: or (imm_safe_t k (C e0) m) (@ex (forall _ : expr, expr) (fun C0 : forall _ : expr, expr => @ex expr (fun a1 : expr => @ex trace (fun t : trace => @ex expr (fun a1' : expr => @ex Mem.mem (fun m' : Mem.mem => and (context RV k C0) (and (@eq expr (C e0) (C0 a1)) (and (rred ge a1 m t a1' m') (forall w' : world, not (possible_trace w t w')))))))))) *)
  left. apply imm_safe_t_loc.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  left. eapply imm_safe_t_lred; eauto.
(* Goal: or (imm_safe_t k (C e0) m) (@ex (forall _ : expr, expr) (fun C0 : forall _ : expr, expr => @ex expr (fun a1 : expr => @ex trace (fun t : trace => @ex expr (fun a1' : expr => @ex Mem.mem (fun m' : Mem.mem => and (context RV k C0) (and (@eq expr (C e0) (C0 a1)) (and (rred ge a1 m t a1' m') (forall w' : world, not (possible_trace w t w')))))))))) *)
(* Goal: or (imm_safe_t k (C e0) m) (@ex (forall _ : expr, expr) (fun C0 : forall _ : expr, expr => @ex expr (fun a1 : expr => @ex trace (fun t : trace => @ex expr (fun a1' : expr => @ex Mem.mem (fun m' : Mem.mem => and (context RV k C0) (and (@eq expr (C e0) (C0 a1)) (and (rred ge a1 m t a1' m') (forall w' : world, not (possible_trace w t w')))))))))) *)
  destruct (classic (exists w', possible_trace w t w')) as [[w' A] | A].
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  left. eapply imm_safe_t_rred; eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  right. exists C; exists e0; exists t; exists e'; exists m'; intuition. apply A; exists w'; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  left. eapply imm_safe_t_callred; eauto.
Qed.

(** A state can "crash the world" if it can make an observable transition
  whose trace is not accepted by the external world. *)

Definition can_crash_world (w: world) (S: state) : Prop :=
  exists t, exists S', Csem.step ge S t S' /\ forall w', ~possible_trace w t w'.

Theorem not_imm_safe_t:
  forall K C a m f k,
  context K RV C ->
  ~imm_safe_t K a m ->
  Csem.step ge (ExprState f (C a) k e m) E0 Stuckstate \/ can_crash_world w (ExprState f (C a) k e m).
Proof.
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  intros. destruct (classic (imm_safe ge e K a m)).
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit imm_safe_imm_safe_t; eauto.
  intros [A | [C1 [a1 [t [a1' [m' [A [B [D E]]]]]]]]]. contradiction.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  right. red. exists t; econstructor; split; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  left. rewrite B. eapply step_rred with (C := fun x => C(C1 x)). eauto. eauto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  left. left. eapply step_stuck; eauto.
Qed.

End EXPRS.

(** * Transitions over states. *)

(* Goal: forall n : Ptrofs.int, @eq (option Ptrofs.int) (do_alloc_size (Vptrofs n)) (@Some Ptrofs.int n) *)
(* Goal: forall (ef : external_function) (w : world) (vargs : list val) (m : Mem.mem) (w' : world) (t : trace) (vres : val) (m' : Mem.mem) (_ : external_call ef (@Genv.to_senv fundef type (genv_genv ge)) vargs m t vres m') (_ : possible_trace w t w'), @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_external ef w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
Fixpoint do_alloc_variables (e: env) (m: mem) (l: list (ident * type)) {struct l} : env * mem :=
  match l with
  | nil => (e,m)
  | (id, ty) :: l' =>
      let (m1,b1) := Mem.alloc m 0 (sizeof ge ty) in
      do_alloc_variables (PTree.set id (b1, ty) e) m1 l'
end.

Lemma do_alloc_variables_sound:
  forall l e m, alloc_variables ge e m l (fst (do_alloc_variables e m l)) (snd (do_alloc_variables e m l)).
Proof.
(* Goal: @eq (option Mem.mem) match E0 with | nil => sem_bind_parameters w e m1 params vl | cons e l => @None Mem.mem end (@Some Mem.mem m2) *)
  induction l; intros; simpl.
(* Goal: imm_safe ge e RV (Eval v ty) m *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  constructor.
(* Goal: @eq (option Mem.mem) match E0 with | nil => sem_bind_parameters w e m1 params vl | cons e l => @None Mem.mem end (@Some Mem.mem m2) *)
  destruct a as [id ty]. destruct (Mem.alloc m 0 (sizeof ge ty)) as [m1 b1] eqn:?; simpl.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  econstructor; eauto.
Qed.

Lemma do_alloc_variables_complete:
  forall e1 m1 l e2 m2, alloc_variables ge e1 m1 l e2 m2 ->
  do_alloc_variables e1 m1 l = (e2, m2).
Proof.
(* Goal: forall (e1 : env) (m1 : Mem.mem) (l : list (prod ident type)) (e2 : env) (m2 : Mem.mem) (_ : alloc_variables ge e1 m1 l e2 m2), @eq (prod env Mem.mem) (do_alloc_variables e1 m1 l) (@pair env Mem.mem e2 m2) *)
  induction 1; simpl.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  rewrite H; rewrite IHalloc_variables; auto.
Qed.

Function sem_bind_parameters (w: world) (e: env) (m: mem) (l: list (ident * type)) (lv: list val)
(* Goal: forall n : Ptrofs.int, @eq (option Ptrofs.int) (do_alloc_size (Vptrofs n)) (@Some Ptrofs.int n) *)
(* Goal: forall (ef : external_function) (w : world) (vargs : list val) (m : Mem.mem) (w' : world) (t : trace) (vres : val) (m' : Mem.mem) (_ : external_call ef (@Genv.to_senv fundef type (genv_genv ge)) vargs m t vres m') (_ : possible_trace w t w'), @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_external ef w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
                          {struct l} : option mem :=
  match l, lv  with
  | nil, nil => Some m
  | (id, ty) :: params, v1::lv =>
      match PTree.get id e with
         | Some (b, ty') =>
             check (type_eq ty ty');
             do w', t, m1 <- do_assign_loc w ty m b Ptrofs.zero v1;
             match t with nil => sem_bind_parameters w e m1 params lv | _ => None end
        | None => None
      end
   | _, _ => None
end.

Lemma sem_bind_parameters_sound : forall w e m l lv m',
  sem_bind_parameters w e m l lv = Some m' ->
  bind_parameters ge e m l lv m'.
Proof.
(* Goal: forall (w : world) (e : env) (m : Mem.mem) (l : list (prod ident type)) (lv : list val) (m' : Mem.mem) (_ : @eq (option Mem.mem) (sem_bind_parameters w e m l lv) (@Some Mem.mem m')), bind_parameters ge e m l lv m' *)
   intros; functional induction (sem_bind_parameters w e m l lv); try discriminate.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
   inversion H; constructor; auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
   exploit do_assign_loc_sound; eauto. intros [A B]. econstructor; eauto.
Qed.

Lemma sem_bind_parameters_complete : forall w e m l lv m',
  bind_parameters ge e m l lv m' ->
  sem_bind_parameters w e m l lv = Some m'.
Proof.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
   induction 1; simpl; auto.
(* Goal: @eq (option Mem.mem) (if type_eq ty ty then match do_assign_loc w ty m b Ptrofs.zero v1 with | Some (pair (pair w' (nil as t) as p0) m1 as p) => sem_bind_parameters w e m1 params vl | Some (pair (pair w' (cons e l as t) as p0) m1 as p) => @None Mem.mem | None => @None Mem.mem end else @None Mem.mem) (@Some Mem.mem m2) *)
   rewrite H. rewrite dec_eq_true.
(* Goal: imm_safe ge e RV (Eval v ty) m *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
   assert (possible_trace w E0 w) by constructor.
(* Goal: @eq (option Mem.mem) match do_assign_loc w ty m b Ptrofs.zero v1 with | Some (pair (pair w' (nil as t) as p0) m1 as p) => sem_bind_parameters w e m1 params vl | Some (pair (pair w' (cons e l as t) as p0) m1 as p) => @None Mem.mem | None => @None Mem.mem end (@Some Mem.mem m2) *)
   rewrite (do_assign_loc_complete _ _ _ _ _ _ _ _ _ H0 H2).
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
   simpl. auto.
Qed.

Inductive transition : Type := TR (rule: string) (t: trace) (S': state).

Definition expr_final_state (f: function) (k: cont) (e: env) (C_rd: (expr -> expr) * reduction) :=
  match snd C_rd with
  | Lred rule a m => TR rule E0 (ExprState f (fst C_rd a) k e m)
  | Rred rule a m t => TR rule t (ExprState f (fst C_rd a) k e m)
  | Callred rule fd vargs ty m => TR rule E0 (Callstate fd vargs (Kcall f e (fst C_rd) ty k) m)
  | Stuckred => TR "step_stuck" E0 Stuckstate
  end.

Local Open Scope list_monad_scope.

Definition ret (rule: string) (S: state) : list transition :=
  TR rule E0 S :: nil.

Definition do_step (w: world) (s: state) : list transition :=
  match s with

  | ExprState f a k e m =>
      match is_val a with
      | Some(v, ty) =>
        match k with
        | Kdo k => ret "step_do_2" (State f Sskip k e m )
        | Kifthenelse s1 s2 k =>
            do b <- bool_val v ty m;
            ret "step_ifthenelse_2" (State f (if b then s1 else s2) k e m)
        | Kwhile1 x s k =>
            do b <- bool_val v ty m;
            if b
            then ret "step_while_true" (State f s (Kwhile2 x s k) e m)
            else ret "step_while_false" (State f Sskip k e m)
        | Kdowhile2 x s k =>
            do b <- bool_val v ty m;
            if b
            then ret "step_dowhile_true" (State f (Sdowhile x s) k e m)
            else ret "step_dowhile_false" (State f Sskip k e m)
        | Kfor2 a2 a3 s k =>
            do b <- bool_val v ty m;
            if b
            then ret "step_for_true" (State f s (Kfor3 a2 a3 s k) e m)
            else ret "step_for_false" (State f Sskip k e m)
        | Kreturn k =>
            do v' <- sem_cast v ty f.(fn_return) m;
            do m' <- Mem.free_list m (blocks_of_env ge e);
            ret "step_return_2" (Returnstate v' (call_cont k) m')
        | Kswitch1 sl k =>
            do n <- sem_switch_arg v ty;
            ret "step_expr_switch" (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch2 k) e m)
        | _ => nil
        end

      | None =>
          map (expr_final_state f k e) (step_expr e w RV a m)
      end

  | State f (Sdo x) k e m =>
      ret "step_do_1" (ExprState f x (Kdo k) e m)
  | State f (Ssequence s1 s2) k e m =>
      ret "step_seq" (State f s1 (Kseq s2 k) e m)
  | State f Sskip (Kseq s k) e m =>
      ret "step_skip_seq" (State f s k e m)
  | State f Scontinue (Kseq s k) e m =>
      ret "step_continue_seq" (State f Scontinue k e m)
  | State f Sbreak (Kseq s k) e m =>
      ret "step_break_seq" (State f Sbreak k e m)

  | State f (Sifthenelse a s1 s2) k e m =>
      ret "step_ifthenelse_1" (ExprState f a (Kifthenelse s1 s2 k) e m)

  | State f (Swhile x s) k e m =>
      ret "step_while" (ExprState f x (Kwhile1 x s k) e m)
  | State f (Sskip|Scontinue) (Kwhile2 x s k) e m =>
      ret "step_skip_or_continue_while" (State f (Swhile x s) k e m)
  | State f Sbreak (Kwhile2 x s k) e m =>
      ret "step_break_while" (State f Sskip k e m)

  | State f (Sdowhile a s) k e m =>
      ret "step_dowhile" (State f s (Kdowhile1 a s k) e m)
  | State f (Sskip|Scontinue) (Kdowhile1 x s k) e m =>
      ret "step_skip_or_continue_dowhile" (ExprState f x (Kdowhile2 x s k) e m)
  | State f Sbreak (Kdowhile1 x s k) e m =>
      ret "step_break_dowhile" (State f Sskip k e m)

  | State f (Sfor a1 a2 a3 s) k e m =>
      if is_skip a1
      then ret "step_for" (ExprState f a2 (Kfor2 a2 a3 s k) e m)
      else ret "step_for_start" (State f a1 (Kseq (Sfor Sskip a2 a3 s) k) e m)
  | State f (Sskip|Scontinue) (Kfor3 a2 a3 s k) e m =>
      ret "step_skip_or_continue_for3" (State f a3 (Kfor4 a2 a3 s k) e m)
  | State f Sbreak (Kfor3 a2 a3 s k) e m =>
      ret "step_break_for3" (State f Sskip k e m)
  | State f Sskip (Kfor4 a2 a3 s k) e m =>
      ret "step_skip_for4" (State f (Sfor Sskip a2 a3 s) k e m)

  | State f (Sreturn None) k e m =>
      do m' <- Mem.free_list m (blocks_of_env ge e);
      ret "step_return_0" (Returnstate Vundef (call_cont k) m')
  | State f (Sreturn (Some x)) k e m =>
      ret "step_return_1" (ExprState f x (Kreturn k) e m)
  | State f Sskip ((Kstop | Kcall _ _ _ _ _) as k) e m =>
      do m' <- Mem.free_list m (blocks_of_env ge e);
      ret "step_skip_call" (Returnstate Vundef k m')

  | State f (Sswitch x sl) k e m =>
      ret "step_switch" (ExprState f x (Kswitch1 sl k) e m)
  | State f (Sskip|Sbreak) (Kswitch2 k) e m =>
      ret "step_skip_break_switch" (State f Sskip k e m)
  | State f Scontinue (Kswitch2 k) e m =>
      ret "step_continue_switch" (State f Scontinue k e m)

  | State f (Slabel lbl s) k e m =>
      ret "step_label" (State f s k e m)
  | State f (Sgoto lbl) k e m =>
      match find_label lbl f.(fn_body) (call_cont k) with
      | Some(s', k') => ret "step_goto" (State f s' k' e m)
      | None => nil
      end

  | Callstate (Internal f) vargs k m =>
      check (list_norepet_dec ident_eq (var_names (fn_params f) ++ var_names (fn_vars f)));
      let (e,m1) := do_alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) in
      do m2 <- sem_bind_parameters w e m1 f.(fn_params) vargs;
      ret "step_internal_function" (State f f.(fn_body) k e m2)
  | Callstate (External ef _ _ _) vargs k m =>
      match do_external ef w vargs m with
      | None => nil
      | Some(w',t,v,m') => TR "step_external_function" t (Returnstate v k m') :: nil
      end

  | Returnstate v (Kcall f e C ty k) m =>
      ret "step_returnstate" (ExprState f (C (Eval v ty)) k e m)

  | _ => nil
  end.

Ltac myinv :=
  match goal with
  | [ |- In _ nil -> _ ] => let X := fresh "X" in intro X; elim X
  | [ |- In _ (ret _ _) -> _ ] =>
        let X := fresh "X" in
        intro X; elim X; clear X;
        [let EQ := fresh "EQ" in intro EQ; unfold ret in EQ; inv EQ; myinv | myinv]
  | [ |- In _ (_ :: nil) -> _ ] =>
        let X := fresh "X" in
        intro X; elim X; clear X; [let EQ := fresh "EQ" in intro EQ; inv EQ; myinv | myinv]
  | [ |- In _ (match ?x with Some _ => _ | None => _ end) -> _ ] => destruct x eqn:?; myinv
  | [ |- In _ (match ?x with false => _ | true => _ end) -> _ ] => destruct x eqn:?; myinv
  | [ |- In _ (match ?x with left _ => _ | right _ => _ end) -> _ ] => destruct x; myinv
  | _ => idtac
  end.

Hint Extern 3 => exact I.

Theorem do_step_sound:
  forall w S rule t S',
  In (TR rule t S') (do_step w S) ->
  Csem.step ge S t S' \/ (t = E0 /\ S' = Stuckstate /\ can_crash_world w S).
Proof with try (left; right; econstructor; eauto; fail).
(* Goal: @eq (option Mem.mem) match E0 with | nil => sem_bind_parameters w e m1 params vl | cons e l => @None Mem.mem end (@Some Mem.mem m2) *)
  intros until S'. destruct S; simpl.
(* State *)
  destruct s; myinv...
  (* skip *)
  destruct k; myinv...
  (* break *)
  destruct k; myinv...
  (* continue *)
  destruct k; myinv...
  (* goto *)
  destruct p as [s' k']. myinv...
(* ExprState *)
  destruct (is_val r) as [[v ty]|] eqn:?.
  (* expression is a value *)
(* Goal: @eq (reducts exprlist) (@incontext2 expr exprlist exprlist (fun x : expr => Econs x al) (step_expr RV r1 m) (fun x : exprlist => Econs r1 x) (step_exprlist al m)) (@nil (prod (forall _ : expr, exprlist) reduction)) *)
  rewrite (is_val_inv _ _ _ Heqo).
  destruct k; myinv...
  (* expression reduces *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  intros. exploit list_in_map_inv; eauto. intros [[C rd] [A B]].
  generalize (step_expr_sound e w r RV m). unfold reducts_ok. intros [P Q].
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit P; eauto. intros [a' [k' [CTX [EQ RD]]]].
  unfold expr_final_state in A. simpl in A.
  destruct k'; destruct rd; inv A; simpl in RD; try contradiction.
  (* lred *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  left; left; apply step_lred; auto.
  (* stuck lred *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit not_imm_safe_t; eauto. intros [R | R]; eauto.
  (* rred *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct RD. left; left; apply step_rred; auto.
  (* callred *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct RD; subst m'. left; left; apply step_call; eauto.
  (* stuck rred *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit not_imm_safe_t; eauto. intros [R | R]; eauto.
(* callstate *)
  destruct fd; myinv.
  (* internal *)
  destruct (do_alloc_variables empty_env m (fn_params f ++ fn_vars f)) as [e m1] eqn:?.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  myinv. left; right; apply step_internal_function with m1. auto.
  change e with (fst (e,m1)). change m1 with (snd (e,m1)) at 2. rewrite <- Heqp.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply do_alloc_variables_sound. eapply sem_bind_parameters_sound; eauto.
  (* external *)
(* Goal: imm_safe ge e RV (Eval v ty) m *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct p as [[[w' tr] v] m']. myinv. left; right; constructor.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  eapply do_ef_external_sound; eauto.
(* returnstate *)
  destruct k; myinv...
(* stuckstate *)
  contradiction.
Qed.

Remark estep_not_val:
  forall f a k e m t S, estep ge (ExprState f a k e m) t S -> is_val a = None.
Proof.
(* Goal: forall (f : function) (a : expr) (k : cont) (e : env) (m : Mem.mem) (t : trace) (S : state) (_ : estep ge (ExprState f a k e m) t S), @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  intros.
  assert (forall b from to C, context from to C -> (from = to /\ C = fun x => x) \/ is_val (C b) = None).
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
    induction 1; simpl; auto.
(* Goal: @eq (option (prod val type)) (is_val a) (@None (prod val type)) *)
  inv H.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (H0 a0 _ _ _ H9) as [[A B] | A]. subst. inv H8; auto. auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (H0 a0 _ _ _ H9) as [[A B] | A]. subst. inv H8; auto. auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (H0 a0 _ _ _ H9) as [[A B] | A]. subst. inv H8; auto. auto.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  destruct (H0 a0 _ _ _ H8) as [[A B] | A]. subst. destruct a0; auto. elim H9. constructor. auto.
Qed.

Theorem do_step_complete:
  forall w S t S' w',
  possible_trace w t w' -> Csem.step ge S t S' -> exists rule, In (TR rule t S') (do_step w S).
Proof with (unfold ret; eauto with coqlib).
  intros until w'; intros PT H.
(* Goal: and (forall (C : forall _ : expr, expr) (rd : reduction) (_ : @In (prod (forall _ : expr, expr) reduction) (@pair (forall _ : expr, expr) reduction C rd) (@map (prod (forall _ : expr, exprlist) reduction) (prod (forall _ : expr, expr) reduction) (fun z : prod (forall _ : expr, exprlist) reduction => @pair (forall _ : expr, expr) reduction (fun x : expr => Ebuiltin ef tyargs (@fst (forall _ : expr, exprlist) reduction z x) ty) (@snd (forall _ : expr, exprlist) reduction z)) res)), @ex expr (fun a' : expr => @ex kind (fun k' : kind => and (context k' RV C) (and (@eq expr (Ebuiltin ef tyargs al ty) (C a')) (reduction_ok k' a' m rd))))) (forall _ : @eq (reducts expr) (@map (prod (forall _ : expr, exprlist) reduction) (prod (forall _ : expr, expr) reduction) (fun z : prod (forall _ : expr, exprlist) reduction => @pair (forall _ : expr, expr) reduction (fun x : expr => Ebuiltin ef tyargs (@fst (forall _ : expr, exprlist) reduction z x) ty) (@snd (forall _ : expr, exprlist) reduction z)) res) (@nil (prod (forall _ : expr, expr) reduction)), not (@eq (option (prod val type)) (is_val (Ebuiltin ef tyargs al ty)) (@None (prod val type)))) *)
  destruct H.
  (* Expression step *)
  inversion H; subst; exploit estep_not_val; eauto; intro NOTVAL.
(* lred *)
  unfold do_step; rewrite NOTVAL.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit lred_topred; eauto. instantiate (1 := w). intros (rule & STEP).
  exists rule. change (TR rule E0 (ExprState f (C a') k e m')) with (expr_final_state f k e (C, Lred rule a' m')).
(* Goal: @In (prod (forall _ : expr, B) reduction) (f (@pair (forall _ : expr, A) reduction C1 rd)) (@map (prod (forall _ : expr, A) reduction) (prod (forall _ : expr, B) reduction) f res) *)
  apply in_map.
(* Goal: forall _ : @reducts_incl expr expr C (step_expr k a m) (step_expr RV (C a) m), @ex (forall _ : expr, expr) (fun C' : forall _ : expr, expr => @In (prod (forall _ : expr, expr) reduction) (@pair (forall _ : expr, expr) reduction C' Stuckred) (step_expr RV (C a) m)) *)
  generalize (step_expr_context e w _ _ _ H1 a m). unfold reducts_incl.
(* Goal: forall _ : forall (C1 : forall _ : expr, expr) (rd : reduction) (_ : @In (prod (forall _ : expr, expr) reduction) (@pair (forall _ : expr, expr) reduction C1 rd) (step_expr k a m)), @In (prod (forall _ : expr, expr) reduction) (@pair (forall _ : expr, expr) reduction (fun x : expr => C (C1 x)) rd) (step_expr RV (C a) m), @ex (forall _ : expr, expr) (fun C' : forall _ : expr, expr => @In (prod (forall _ : expr, expr) reduction) (@pair (forall _ : expr, expr) reduction C' Stuckred) (step_expr RV (C a) m)) *)
  intro. replace C with (fun x => C x). apply H2.
  rewrite STEP. unfold topred; auto with coqlib.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply extensionality; auto.
(* rred *)
  unfold do_step; rewrite NOTVAL.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit rred_topred; eauto. instantiate (1 := e). intros (rule & STEP).
  exists rule.
  change (TR rule t (ExprState f (C a') k e m')) with (expr_final_state f k e (C, Rred rule a' m' t)).
(* Goal: @In (prod (forall _ : expr, B) reduction) (f (@pair (forall _ : expr, A) reduction C1 rd)) (@map (prod (forall _ : expr, A) reduction) (prod (forall _ : expr, B) reduction) f res) *)
  apply in_map.
(* Goal: forall _ : @reducts_incl expr expr C (step_expr k a m) (step_expr RV (C a) m), @ex (forall _ : expr, expr) (fun C' : forall _ : expr, expr => @In (prod (forall _ : expr, expr) reduction) (@pair (forall _ : expr, expr) reduction C' Stuckred) (step_expr RV (C a) m)) *)
  generalize (step_expr_context e w _ _ _ H1 a m). unfold reducts_incl.
(* Goal: forall _ : forall (C1 : forall _ : expr, expr) (rd : reduction) (_ : @In (prod (forall _ : expr, expr) reduction) (@pair (forall _ : expr, expr) reduction C1 rd) (step_expr k a m)), @In (prod (forall _ : expr, expr) reduction) (@pair (forall _ : expr, expr) reduction (fun x : expr => C (C1 x)) rd) (step_expr RV (C a) m), @ex (forall _ : expr, expr) (fun C' : forall _ : expr, expr => @In (prod (forall _ : expr, expr) reduction) (@pair (forall _ : expr, expr) reduction C' Stuckred) (step_expr RV (C a) m)) *)
  intro. replace C with (fun x => C x). apply H2.
  rewrite STEP; unfold topred; auto with coqlib.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply extensionality; auto.
(* callred *)
  unfold do_step; rewrite NOTVAL.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit callred_topred; eauto. instantiate (1 := w). instantiate (1 := e).
  intros (rule & STEP). exists rule.
  change (TR rule E0 (Callstate fd vargs (Kcall f e C ty k) m)) with (expr_final_state f k e (C, Callred rule fd vargs ty m)).
(* Goal: @In (prod (forall _ : expr, B) reduction) (f (@pair (forall _ : expr, A) reduction C1 rd)) (@map (prod (forall _ : expr, A) reduction) (prod (forall _ : expr, B) reduction) f res) *)
  apply in_map.
(* Goal: forall _ : @reducts_incl expr expr C (step_expr k a m) (step_expr RV (C a) m), @ex (forall _ : expr, expr) (fun C' : forall _ : expr, expr => @In (prod (forall _ : expr, expr) reduction) (@pair (forall _ : expr, expr) reduction C' Stuckred) (step_expr RV (C a) m)) *)
  generalize (step_expr_context e w _ _ _ H1 a m). unfold reducts_incl.
(* Goal: forall _ : forall (C1 : forall _ : expr, expr) (rd : reduction) (_ : @In (prod (forall _ : expr, expr) reduction) (@pair (forall _ : expr, expr) reduction C1 rd) (step_expr k a m)), @In (prod (forall _ : expr, expr) reduction) (@pair (forall _ : expr, expr) reduction (fun x : expr => C (C1 x)) rd) (step_expr RV (C a) m), @ex (forall _ : expr, expr) (fun C' : forall _ : expr, expr => @In (prod (forall _ : expr, expr) reduction) (@pair (forall _ : expr, expr) reduction C' Stuckred) (step_expr RV (C a) m)) *)
  intro. replace C with (fun x => C x). apply H2.
  rewrite STEP; unfold topred; auto with coqlib.
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply extensionality; auto.
(* stuck *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit not_imm_safe_stuck_red. eauto. red; intros; elim H1. eapply imm_safe_t_imm_safe. eauto.
  instantiate (1 := w). intros [C' IN].
  simpl do_step. rewrite NOTVAL.
  exists "step_stuck".
  change (TR "step_stuck" E0 Stuckstate) with (expr_final_state f k e (C', Stuckred)).
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  apply in_map. auto.

  (* Statement step *)
(* Goal: imm_safe ge e RV (Eval v ty) m *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  inv H; simpl; econstructor...
  rewrite H0...
  rewrite H0...
  rewrite H0...
  destruct H0; subst s0...
  destruct H0; subst s0...
  rewrite H0...
  rewrite H0...
  rewrite pred_dec_false...
  rewrite H0...
  rewrite H0...
  destruct H0; subst x...
  rewrite H0...
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) match Mem.load Mptr m b (Z.sub (Ptrofs.unsigned lo) (size_chunk Mptr)) with | Some vsz => match do_alloc_size vsz with | Some sz => if zlt Z0 (Ptrofs.unsigned sz) then match Mem.free m b (Z.sub (Ptrofs.unsigned lo) (size_chunk Mptr)) (Z.add (Ptrofs.unsigned lo) (Ptrofs.unsigned sz)) with | Some m' => @Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' E0) Vundef) m') | None => @None (prod (prod (prod world trace) val) Mem.mem) end else @None (prod (prod (prod world trace) val) Mem.mem) | None => @None (prod (prod (prod world trace) val) Mem.mem) end | None => @None (prod (prod (prod world trace) val) Mem.mem) end (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' E0) Vundef) m')) *)
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_ef_memcpy sz al w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_ef_annot text targs w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_ef_annot_val text targ w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_inline_assembly text sg (@Genv.to_senv fundef type (genv_genv ge)) w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_ef_debug kind text targs w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
  rewrite H0; rewrite H1...
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) match Mem.load Mptr m b (Z.sub (Ptrofs.unsigned lo) (size_chunk Mptr)) with | Some vsz => match do_alloc_size vsz with | Some sz => if zlt Z0 (Ptrofs.unsigned sz) then match Mem.free m b (Z.sub (Ptrofs.unsigned lo) (size_chunk Mptr)) (Z.add (Ptrofs.unsigned lo) (Ptrofs.unsigned sz)) with | Some m' => @Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' E0) Vundef) m') | None => @None (prod (prod (prod world trace) val) Mem.mem) end else @None (prod (prod (prod world trace) val) Mem.mem) | None => @None (prod (prod (prod world trace) val) Mem.mem) end | None => @None (prod (prod (prod world trace) val) Mem.mem) end (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' E0) Vundef) m')) *)
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_ef_memcpy sz al w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_ef_annot text targs w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_ef_annot_val text targ w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_inline_assembly text sg (@Genv.to_senv fundef type (genv_genv ge)) w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
(* Goal: @eq (option (prod (prod (prod world trace) val) Mem.mem)) (do_ef_debug kind text targs w vargs m) (@Some (prod (prod (prod world trace) val) Mem.mem) (@pair (prod (prod world trace) val) Mem.mem (@pair (prod world trace) val (@pair world trace w' t) vres) m')) *)
  rewrite H1. red in H0. destruct k; try contradiction...
  rewrite H0...
  destruct H0; subst x...
  rewrite H0...

  (* Call step *)
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  rewrite pred_dec_true; auto. rewrite (do_alloc_variables_complete _ _ _ _ _ H1).
  rewrite (sem_bind_parameters_complete _ _ _ _ _ _ H2)...
(* Goal: @eq (option (prod val type)) (is_val (C a0)) (@None (prod val type)) *)
  exploit do_ef_external_complete; eauto. intro EQ; rewrite EQ. auto with coqlib.
Qed.

End EXEC.

Local Open Scope option_monad_scope.

Definition do_initial_state (p: program): option (genv * state) :=
  let ge := globalenv p in
  do m0 <- Genv.init_mem p;
  do b <- Genv.find_symbol ge p.(prog_main);
  do f <- Genv.find_funct_ptr ge b;
  check (type_eq (type_of_fundef f) (Tfunction Tnil type_int32s cc_default));
  Some (ge, Callstate f nil Kstop m0).

Definition at_final_state (S: state): option int :=
  match S with
  | Returnstate (Vint r) Kstop m => Some r
  | _ => None
  end.
