Require Import VST.msl.msl_standard.
Require Import VST.veric.Clight_base.
Require Import VST.veric.compcert_rmaps.
Require Import VST.veric.Clight_lemmas.
Require Import VST.veric.mpred.
Require Import VST.veric.tycontext.
Require Import VST.veric.expr.
Require Import VST.veric.expr2.
Require Export VST.veric.environ_lemmas.


Import Cop.
Import Cop2.
Import Clight_Cop2.

(* Goal: tc_val pt match @Map.get block ge i with | Some b => Vptr b Ptrofs.zero | None => Vundef end *)
Lemma eval_lvalue_ptr : forall {CS: compspecs} rho m e (Delta: tycontext) te ve ge,
mkEnviron ge ve te = rho ->
typecheck_var_environ ve (var_types Delta) ->
typecheck_glob_environ ge (glob_types Delta) ->
denote_tc_assert (typecheck_lvalue Delta e) rho m ->
exists base, exists ofs, eval_lvalue e rho  = Vptr base ofs.
Proof.
(* Goal: forall (CS : compspecs) (Delta : tycontext) (rho : environ) (m : rmap) (i : ident) (t : type) (_ : typecheck_environ Delta rho) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_expr CS Delta (Etempvar i t)) rho) m), tc_val (typeof (Etempvar i t)) (@eval_expr CS (Etempvar i t) rho) *)
intros.
induction e; eauto;
try now inversion H2.
*
(* Goal: tc_val pt (@eval_lvalue CS (Ederef e t) rho) *)
simpl. unfold eval_var.
(* Goal: @ex block (fun base : block => @ex Ptrofs.int (fun ofs : Ptrofs.int => @eq val (@eval_lvalue CS (Ederef e t) rho) (Vptr base ofs))) *)
simpl in H2.
(* Goal: @ex block (fun base : block => @ex Ptrofs.int (fun ofs : Ptrofs.int => @eq val match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end (Vptr base ofs))) *)
unfold get_var_type in H2.
(* Goal: @ex block (fun base : block => @ex Ptrofs.int (fun ofs : Ptrofs.int => @eq val match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end (Vptr base ofs))) *)
subst rho; simpl ve_of; simpl ge_of.
destruct_var_types i eqn:H4&?H; rewrite H4 in H2;
 [| destruct_glob_types i eqn:?H&?H; rewrite H6 in H2 ].
+ apply tc_bool_e in H2.
(* Goal: @ex block (fun base : block => @ex Ptrofs.int (fun ofs : Ptrofs.int => @eq val match @Map.get (prod block type) ve i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block ge i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end (Vptr base ofs))) *)
  exists b, Ptrofs.zero.
(* Goal: @eq val match @Map.get (prod block type) ve i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block ge i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end (Vptr b Ptrofs.zero) *)
  rewrite H3, H2.
(* Goal: @eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero) *)
  auto.
+ apply tc_bool_e in H2.
(* Goal: @ex block (fun base : block => @ex Ptrofs.int (fun ofs : Ptrofs.int => @eq val match @Map.get (prod block type) ve i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block ge i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end (Vptr base ofs))) *)
  exists b, Ptrofs.zero.
(* Goal: @eq val match @Map.get (prod block type) ve i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block ge i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end (Vptr b Ptrofs.zero) *)
  rewrite H3, H5.
(* Goal: @eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero) *)
  auto.
+ inv H2.
*
(* Goal: @ex block (fun base : block => @ex Ptrofs.int (fun ofs : Ptrofs.int => @eq val (@eval_lvalue CS (Ederef e t) rho) (Vptr base ofs))) *)
simpl in H2.
(* Goal: @ex block (fun base : block => @ex Ptrofs.int (fun ofs : Ptrofs.int => @eq val (@eval_lvalue CS (Ederef e t) rho) (Vptr base ofs))) *)
rewrite !denote_tc_assert_andp in H2.
(* Goal: @ex block (fun base : block => @ex Ptrofs.int (fun ofs : Ptrofs.int => @eq val (@eval_lvalue CS (Ederef e t) rho) (Vptr base ofs))) *)
destruct H2 as [[? ?] ?].
(* Goal: @ex block (fun base : block => @ex Ptrofs.int (fun ofs : Ptrofs.int => @eq val (@eval_lvalue CS (Ederef e t) rho) (Vptr base ofs))) *)
simpl in H4.
(* Goal: tc_val pt (@eval_lvalue CS (Ederef e t) rho) *)
simpl.
(* Goal: @eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero) *)
destruct (eval_expr e rho); simpl; try now inversion H4; eauto.
*
simpl in *. super_unfold_lift.
(* Goal: @ex block (fun base : block => @ex Ptrofs.int (fun ofs : Ptrofs.int => @eq val (@eval_field CS (typeof e) i (@eval_lvalue CS e rho)) (Vptr base ofs))) *)
rewrite denote_tc_assert_andp in H2.
(* Goal: @ex block (fun base : block => @ex Ptrofs.int (fun ofs : Ptrofs.int => @eq val (@eval_field CS (typeof e) i (@eval_lvalue CS e rho)) (Vptr base ofs))) *)
destruct H2.
(* Goal: @eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero) *)
spec IHe; auto. destruct IHe.
(* Goal: @ex block (fun base : block => @ex Ptrofs.int (fun ofs : Ptrofs.int => @eq val (@eval_field CS (typeof e) i (@eval_lvalue CS e rho)) (Vptr base ofs))) *)
unfold eval_field.
(* Goal: @ex block (fun base : block => @ex Ptrofs.int (fun ofs : Ptrofs.int => @eq val (match typeof e with | Tvoid => @always val val Vundef | Tint i s a => @always val val Vundef | Tlong s a => @always val val Vundef | Tfloat f a => @always val val Vundef | Tpointer t a => @always val val Vundef | Tarray t z a => @always val val Vundef | Tfunction t t0 c => @always val val Vundef | Tstruct id att => match @PTree.get composite id (@cenv_cs CS) with | Some co => match field_offset (@cenv_cs CS) i (co_members co) with | Errors.OK delta => offset_val delta | Errors.Error e => @always val val Vundef end | None => @always val val Vundef end | Tunion id att => match @PTree.get composite id (@cenv_cs CS) with | Some co => force_ptr | None => @always val val Vundef end end (@eval_lvalue CS e rho)) (Vptr base ofs))) *)
destruct H4 as [ofs ?].
(* Goal: @ex block (fun base : block => @ex Ptrofs.int (fun ofs : Ptrofs.int => @eq val (match typeof e with | Tvoid => @always val val Vundef | Tint i s a => @always val val Vundef | Tlong s a => @always val val Vundef | Tfloat f a => @always val val Vundef | Tpointer t a => @always val val Vundef | Tarray t z a => @always val val Vundef | Tfunction t t0 c => @always val val Vundef | Tstruct id att => match @PTree.get composite id (@cenv_cs CS) with | Some co => match field_offset (@cenv_cs CS) i (co_members co) with | Errors.OK delta => offset_val delta | Errors.Error e => @always val val Vundef end | None => @always val val Vundef end | Tunion id att => match @PTree.get composite id (@cenv_cs CS) with | Some co => force_ptr | None => @always val val Vundef end end (@eval_lvalue CS e rho)) (Vptr base ofs))) *)
destruct (eval_lvalue e rho); try congruence.
(* Goal: @ex block (fun base : block => @ex Ptrofs.int (fun ofs : Ptrofs.int => @eq val (match typeof e with | Tvoid => @always val val Vundef | Tint i s a => @always val val Vundef | Tlong s a => @always val val Vundef | Tfloat f a => @always val val Vundef | Tpointer t a => @always val val Vundef | Tarray t z a => @always val val Vundef | Tfunction t t0 c => @always val val Vundef | Tstruct id att => match @PTree.get composite id (@cenv_cs CS) with | Some co => match field_offset (@cenv_cs CS) i (co_members co) with | Errors.OK delta => offset_val delta | Errors.Error e => @always val val Vundef end | None => @always val val Vundef end | Tunion id att => match @PTree.get composite id (@cenv_cs CS) with | Some co => force_ptr | None => @always val val Vundef end end (Vptr b i0)) (Vptr base ofs))) *)
inversion H4; subst x i0; clear H4.
(* Goal: @ex block (fun base : block => @ex Ptrofs.int (fun ofs0 : Ptrofs.int => @eq val (match typeof e with | Tvoid => @always val val Vundef | Tint i s a => @always val val Vundef | Tlong s a => @always val val Vundef | Tfloat f a => @always val val Vundef | Tpointer t a => @always val val Vundef | Tarray t z a => @always val val Vundef | Tfunction t t0 c => @always val val Vundef | Tstruct id att => match @PTree.get composite id (@cenv_cs CS) with | Some co => match field_offset (@cenv_cs CS) i (co_members co) with | Errors.OK delta => offset_val delta | Errors.Error e => @always val val Vundef end | None => @always val val Vundef end | Tunion id att => match @PTree.get composite id (@cenv_cs CS) with | Some co => force_ptr | None => @always val val Vundef end end (Vptr b ofs)) (Vptr base ofs0))) *)
destruct (typeof e); try now inversion H3.
+
(* Goal: @ex block (fun base : block => @ex Ptrofs.int (fun ofs0 : Ptrofs.int => @eq val (match @PTree.get composite i0 (@cenv_cs CS) with | Some co => force_ptr | None => @always val val Vundef end (Vptr b ofs)) (Vptr base ofs0))) *)
destruct (cenv_cs ! i0) as [co |]; [| inv H3].
(* Goal: @ex block (fun base : block => @ex Ptrofs.int (fun ofs0 : Ptrofs.int => @eq val (match field_offset (@cenv_cs CS) i (co_members co) with | Errors.OK delta => offset_val delta | Errors.Error e => @always val val Vundef end (Vptr b ofs)) (Vptr base ofs0))) *)
destruct (field_offset cenv_cs i (co_members co)); [| inv H3].
(* Goal: @eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero) *)
unfold offset_val; eauto.
+
(* Goal: @ex block (fun base : block => @ex Ptrofs.int (fun ofs0 : Ptrofs.int => @eq val (match @PTree.get composite i0 (@cenv_cs CS) with | Some co => force_ptr | None => @always val val Vundef end (Vptr b ofs)) (Vptr base ofs0))) *)
destruct (cenv_cs ! i0) as [co |]; [| inv H3].
(* Goal: tc_val pt (@eval_lvalue CS (Ederef e t) rho) *)
simpl.
(* Goal: @eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero) *)
eauto.
Qed.

Ltac unfold_tc_denote :=
unfold denote_tc_nonzero in *;
unfold isptr in *;
unfold denote_tc_igt in *;
unfold denote_tc_Zle in *;
unfold denote_tc_Zge in *;
unfold denote_tc_samebase in *;
unfold denote_tc_nodivover in *;
unfold denote_tc_initialized in *.

Lemma typecheck_lvalue_Evar:
(* Goal: tc_val pt match @Map.get block ge i with | Some b => Vptr b Ptrofs.zero | None => Vundef end *)
  forall {CS: compspecs} i t pt Delta rho m, typecheck_environ Delta rho ->
           denote_tc_assert (typecheck_lvalue Delta (Evar i t)) rho m ->
           is_pointer_type pt = true ->
           tc_val pt (eval_lvalue (Evar i t) rho).
Proof.
(* Goal: forall (CS : compspecs) (Delta : tycontext) (rho : environ) (m : rmap) (i : ident) (t : type) (_ : typecheck_environ Delta rho) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_expr CS Delta (Etempvar i t)) rho) m), tc_val (typeof (Etempvar i t)) (@eval_expr CS (Etempvar i t) rho) *)
intros.
simpl in *. unfold eval_var.

(* Goal: tc_val t (eval_var i t rho) *)
unfold typecheck_environ in H.
(* Goal: tc_val t (eval_var i t rho) *)
intuition.
(* Goal: tc_val t (eval_id i rho) *)
destruct rho.
unfold get_var_type in *.

destruct_var_types i; rewrite ?Heqo, ?Heqo0 in *; try rewrite eqb_type_eq in *; simpl in *; intuition.
(* Goal: tc_val t (eval_var i t rho) *)
remember (type_eq t t0). destruct s; intuition.
(* Goal: tc_val pt match @Map.get block ge i with | Some b => Vptr b Ptrofs.zero | None => Vundef end *)
{
simpl in *.
(* Goal: (if eqb_type (Tpointer pt a) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 unfold is_pointer_type in H1.
(* Goal: tc_val pt (Vptr b Ptrofs.zero) *)
 destruct pt; try solve [inv H1; auto].
(* Goal: tc_val (Tpointer pt a) (Vptr b i) *)
 unfold tc_val.
(* Goal: (if eqb_type (Tpointer t a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b (Ptrofs.add i1 (Ptrofs.repr z))) *)
 simple_if_tac; apply I.
}
{destruct_glob_types i; rewrite ?Heqo1, ?Heqo2 in *; [| inv H0].
(* Goal: tc_val t (Vptr b Ptrofs.zero) *)
remember (eqb_type t t0).
symmetry in Heqb0. destruct b0; simpl in *; [| inv H0]. apply eqb_type_true in Heqb0.
(* Goal: tc_val t (Vptr b Ptrofs.zero) *)
subst.

unfold tc_val; unfold is_pointer_type in H1;
(* Goal: tc_val pt (Vptr b i) *)
 destruct pt; try solve [inv H1; reflexivity].
(* Goal: (if eqb_type (Tpointer t a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b (Ptrofs.add i1 (Ptrofs.repr z))) *)
 simple_if_tac; apply I.
}
Qed.

Lemma typecheck_expr_sound_Efield:
(* Goal: tc_val pt match @Map.get block ge i with | Some b => Vptr b Ptrofs.zero | None => Vundef end *)
  forall {CS: compspecs} Delta rho e i t m
  (H: typecheck_environ Delta rho)
  (IHe: (denote_tc_assert (typecheck_expr Delta e) rho m ->
          tc_val (typeof e) (eval_expr e rho)) /\
          (forall pt : type,
          denote_tc_assert (typecheck_lvalue Delta e) rho m ->
          is_pointer_type pt = true ->
          tc_val pt (eval_lvalue e rho)))
  (H0: denote_tc_assert (typecheck_expr Delta (Efield e i t)) rho m),
  tc_val (typeof (Efield e i t)) (eval_expr (Efield e i t) rho).
Proof.
(* Goal: forall (CS : compspecs) (Delta : tycontext) (rho : environ) (m : rmap) (i : ident) (t : type) (_ : typecheck_environ Delta rho) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_expr CS Delta (Etempvar i t)) rho) m), tc_val (typeof (Etempvar i t)) (@eval_expr CS (Etempvar i t) rho) *)
intros.
simpl in *. super_unfold_lift.
 unfold eval_field, offset_val, deref_noload in *.
(* Goal: tc_val t (match typeof e with | Tvoid => @always val val Vundef | Tint i s a => @always val val Vundef | Tlong s a => @always val val Vundef | Tfloat f a => @always val val Vundef | Tpointer t a => @always val val Vundef | Tarray t z a => @always val val Vundef | Tfunction t t0 c => @always val val Vundef | Tstruct id att => match @PTree.get composite id (@cenv_cs CS) with | Some co => match field_offset (@cenv_cs CS) i (co_members co) with | Errors.OK delta => fun v : val => match v with | Vundef => Vundef | Vint i => Vundef | Vlong i => Vundef | Vfloat f => Vundef | Vsingle f => Vundef | Vptr b z => Vptr b (Ptrofs.add z (Ptrofs.repr delta)) end | Errors.Error e => @always val val Vundef end | None => @always val val Vundef end | Tunion id att => match @PTree.get composite id (@cenv_cs CS) with | Some co => force_ptr | None => @always val val Vundef end end (@eval_lvalue CS e rho)) *)
assert (MODE: access_mode t = By_reference) by (destruct (access_mode t); auto; hnf in H0; try contradiction).
rewrite MODE in *.
(* Goal: tc_val t (match typeof e with | Tvoid => @always val val Vundef | Tint i s a => @always val val Vundef | Tlong s a => @always val val Vundef | Tfloat f a => @always val val Vundef | Tpointer t a => @always val val Vundef | Tarray t z a => @always val val Vundef | Tfunction t t0 c => @always val val Vundef | Tstruct id att => match @PTree.get composite id (@cenv_cs CS) with | Some co => match field_offset (@cenv_cs CS) i (co_members co) with | Errors.OK delta => fun v : val => match v with | Vundef => Vundef | Vint i => Vundef | Vlong i => Vundef | Vfloat f => Vundef | Vsingle f => Vundef | Vptr b z => Vptr b (Ptrofs.add z (Ptrofs.repr delta)) end | Errors.Error e => @always val val Vundef end | None => @always val val Vundef end | Tunion id att => match @PTree.get composite id (@cenv_cs CS) with | Some co => force_ptr | None => @always val val Vundef end end (@eval_lvalue CS e rho)) *)
destruct IHe.
(* Goal: tc_val t (eval_id i rho) *)
destruct rho.
(* Goal: tc_val pt (@liftx (Tarrow val (LiftEnviron val)) (@eval_field CS (typeof e) i) (@eval_lvalue CS e) rho) *)
rewrite denote_tc_assert_andp in H0. destruct H0.
(* Goal: tc_val t (eval_var i t rho) *)
unfold typecheck_environ in H.
(* Goal: tc_val t (match typeof e with | Tvoid => @always val val Vundef | Tint i s a => @always val val Vundef | Tlong s a => @always val val Vundef | Tfloat f a => @always val val Vundef | Tpointer t a => @always val val Vundef | Tarray t z a => @always val val Vundef | Tfunction t t0 c => @always val val Vundef | Tstruct id att => match @PTree.get composite id (@cenv_cs CS) with | Some co => match field_offset (@cenv_cs CS) i (co_members co) with | Errors.OK delta => fun v : val => match v with | Vundef => Vundef | Vint i => Vundef | Vlong i => Vundef | Vfloat f => Vundef | Vsingle f => Vundef | Vptr b z => Vptr b (Ptrofs.add z (Ptrofs.repr delta)) end | Errors.Error e => @always val val Vundef end | None => @always val val Vundef end | Tunion id att => match @PTree.get composite id (@cenv_cs CS) with | Some co => force_ptr | None => @always val val Vundef end end (@eval_lvalue CS e (mkEnviron ge ve te))) *)
destruct H as [_ [Hve Hge]].
(* Goal: tc_val t (match typeof e with | Tvoid => @always val val Vundef | Tint i s a => @always val val Vundef | Tlong s a => @always val val Vundef | Tfloat f a => @always val val Vundef | Tpointer t a => @always val val Vundef | Tarray t z a => @always val val Vundef | Tfunction t t0 c => @always val val Vundef | Tstruct id att => match @PTree.get composite id (@cenv_cs CS) with | Some co => match field_offset (@cenv_cs CS) i (co_members co) with | Errors.OK delta => fun v : val => match v with | Vundef => Vundef | Vint i => Vundef | Vlong i => Vundef | Vfloat f => Vundef | Vsingle f => Vundef | Vptr b z => Vptr b (Ptrofs.add z (Ptrofs.repr delta)) end | Errors.Error e => @always val val Vundef end | None => @always val val Vundef end | Tunion id att => match @PTree.get composite id (@cenv_cs CS) with | Some co => force_ptr | None => @always val val Vundef end end (@eval_lvalue CS e (mkEnviron ge ve te))) *)
assert (PTR := eval_lvalue_ptr _ _ e Delta te ve ge (eq_refl _) Hve Hge H0).
(* Goal: tc_val t (match typeof e with | Tvoid => @always val val Vundef | Tint i s a => @always val val Vundef | Tlong s a => @always val val Vundef | Tfloat f a => @always val val Vundef | Tpointer t a => @always val val Vundef | Tarray t z a => @always val val Vundef | Tfunction t t0 c => @always val val Vundef | Tstruct id att => match @PTree.get composite id (@cenv_cs CS) with | Some co => match field_offset (@cenv_cs CS) i (co_members co) with | Errors.OK delta => fun v : val => match v with | Vundef => Vundef | Vint i => Vundef | Vlong i => Vundef | Vfloat f => Vundef | Vsingle f => Vundef | Vptr b z => Vptr b (Ptrofs.add z (Ptrofs.repr delta)) end | Errors.Error e => @always val val Vundef end | None => @always val val Vundef end | Tunion id att => match @PTree.get composite id (@cenv_cs CS) with | Some co => force_ptr | None => @always val val Vundef end end (@eval_lvalue CS e (mkEnviron ge ve te))) *)
specialize (H2 t H0).
(* Goal: @eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero) *)
spec H2. clear - MODE; destruct t; try destruct i; try destruct s; try destruct f; inv MODE; simpl; auto.
(* Goal: tc_val t (match typeof e with | Tvoid => @always val val Vundef | Tint i s a => @always val val Vundef | Tlong s a => @always val val Vundef | Tfloat f a => @always val val Vundef | Tpointer t a => @always val val Vundef | Tarray t z a => @always val val Vundef | Tfunction t t0 c => @always val val Vundef | Tstruct id att => match @PTree.get composite id (@cenv_cs CS) with | Some co => match field_offset (@cenv_cs CS) i (co_members co) with | Errors.OK delta => fun v : val => match v with | Vundef => Vundef | Vint i => Vundef | Vlong i => Vundef | Vfloat f => Vundef | Vsingle f => Vundef | Vptr b z => Vptr b (Ptrofs.add z (Ptrofs.repr delta)) end | Errors.Error e => @always val val Vundef end | None => @always val val Vundef end | Tunion id att => match @PTree.get composite id (@cenv_cs CS) with | Some co => force_ptr | None => @always val val Vundef end end (@eval_lvalue CS e (mkEnviron ge ve te))) *)
destruct PTR.
(* Goal: tc_val t (match typeof e with | Tvoid => @always val val Vundef | Tint i s a => @always val val Vundef | Tlong s a => @always val val Vundef | Tfloat f a => @always val val Vundef | Tpointer t a => @always val val Vundef | Tarray t z a => @always val val Vundef | Tfunction t t0 c => @always val val Vundef | Tstruct id att => match @PTree.get composite id (@cenv_cs CS) with | Some co => match field_offset (@cenv_cs CS) i (co_members co) with | Errors.OK delta => fun v : val => match v with | Vundef => Vundef | Vint i => Vundef | Vlong i => Vundef | Vfloat f => Vundef | Vsingle f => Vundef | Vptr b z => Vptr b (Ptrofs.add z (Ptrofs.repr delta)) end | Errors.Error e => @always val val Vundef end | None => @always val val Vundef end | Tunion id att => match @PTree.get composite id (@cenv_cs CS) with | Some co => force_ptr | None => @always val val Vundef end end (@eval_lvalue CS e (mkEnviron ge ve te))) *)
destruct (typeof e); try now inv H3.
+ destruct (cenv_cs ! i0) as [co |]; try now inv H3.
(* Goal: tc_val t (match field_offset (@cenv_cs CS) i (co_members co) with | Errors.OK delta => fun v : val => match v with | Vundef => Vundef | Vint i => Vundef | Vlong i => Vundef | Vfloat f => Vundef | Vsingle f => Vundef | Vptr b z => Vptr b (Ptrofs.add z (Ptrofs.repr delta)) end | Errors.Error e => @always val val Vundef end (@eval_lvalue CS e (mkEnviron ge ve te))) *)
  destruct (field_offset cenv_cs i (co_members co)); try now inv H3.
(* Goal: tc_val t (force_ptr (@eval_lvalue CS e (mkEnviron ge ve te))) *)
  destruct (eval_lvalue e (mkEnviron ge ve te)); try now inv H.
(* Goal: tc_val t (Vptr b (Ptrofs.add i1 (Ptrofs.repr z))) *)
  destruct t; auto; try inversion H2.
(* Goal: @ex block (fun base : block => @ex Ptrofs.int (fun ofs : Ptrofs.int => @eq val match @Map.get (prod block type) ve i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block ge i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end (Vptr base ofs))) *)
  destruct f; inv H2.
(* Goal: (if eqb_type (Tpointer t a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b (Ptrofs.add i1 (Ptrofs.repr z))) *)
  red. simple_if_tac; apply I.
+ destruct (cenv_cs ! i0) as [co |]; try now inv H3.
(* Goal: tc_val t (force_ptr (@eval_lvalue CS e (mkEnviron ge ve te))) *)
  destruct (eval_lvalue e (mkEnviron ge ve te)); try now inv H.
Qed.

Lemma typecheck_lvalue_sound_Efield:
(* Goal: tc_val pt match @Map.get block ge i with | Some b => Vptr b Ptrofs.zero | None => Vundef end *)
 forall {CS: compspecs} Delta rho m e i t pt
 (H: typecheck_environ Delta rho)
 (IHe: (denote_tc_assert (typecheck_expr Delta e) rho m ->
          tc_val (typeof e) (eval_expr e rho)) /\
        (forall pt0 : type, denote_tc_assert (typecheck_lvalue Delta e) rho m ->
           is_pointer_type pt0 = true ->
         tc_val pt0 (eval_lvalue e rho)))
  (H0: denote_tc_assert (typecheck_lvalue Delta (Efield e i t)) rho m)
  (H1: is_pointer_type pt = true),
  tc_val pt (eval_lvalue (Efield e i t) rho).
Proof.
(* Goal: forall (CS : compspecs) (Delta : tycontext) (rho : environ) (m : rmap) (i : ident) (t : type) (_ : typecheck_environ Delta rho) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_expr CS Delta (Etempvar i t)) rho) m), tc_val (typeof (Etempvar i t)) (@eval_expr CS (Etempvar i t) rho) *)
intros.
simpl in *.
(* Goal: tc_val pt (@liftx (Tarrow val (LiftEnviron val)) (@eval_field CS (typeof e) i) (@eval_lvalue CS e) rho) *)
rewrite denote_tc_assert_andp in H0. destruct H0.
(* Goal: tc_val t (eval_var i t rho) *)
super_unfold_lift.
 unfold eval_field,offset_val in *; intuition.
specialize  (H4 pt).
(* Goal: tc_val t (eval_id i rho) *)
destruct rho.
unfold typecheck_environ in *. intuition.
(* Goal: tc_val pt (match typeof e with | Tvoid => @always val val Vundef | Tint i s a => @always val val Vundef | Tlong s a => @always val val Vundef | Tfloat f a => @always val val Vundef | Tpointer t a => @always val val Vundef | Tarray t z a => @always val val Vundef | Tfunction t t0 c => @always val val Vundef | Tstruct id att => match @PTree.get composite id (@cenv_cs CS) with | Some co => match field_offset (@cenv_cs CS) i (co_members co) with | Errors.OK delta => fun v : val => match v with | Vundef => Vundef | Vint i => Vundef | Vlong i => Vundef | Vfloat f => Vundef | Vsingle f => Vundef | Vptr b z => Vptr b (Ptrofs.add z (Ptrofs.repr delta)) end | Errors.Error e => @always val val Vundef end | None => @always val val Vundef end | Tunion id att => match @PTree.get composite id (@cenv_cs CS) with | Some co => force_ptr | None => @always val val Vundef end end (@eval_lvalue CS e (mkEnviron ge ve te))) *)
assert (PTR := eval_lvalue_ptr _ m e _ te _ _ (eq_refl _) H H7 H0).
simpl in *.
remember (eval_lvalue e (mkEnviron ge ve te)). unfold isptr in *.
(* Goal: tc_val pt (match typeof e with | Tvoid => @always val val Vundef | Tint i s a => @always val val Vundef | Tlong s a => @always val val Vundef | Tfloat f a => @always val val Vundef | Tpointer t a => @always val val Vundef | Tarray t z a => @always val val Vundef | Tfunction t t0 c => @always val val Vundef | Tstruct id att => match @PTree.get composite id (@cenv_cs CS) with | Some co => match field_offset (@cenv_cs CS) i (co_members co) with | Errors.OK delta => fun v : val => match v with | Vundef => Vundef | Vint i => Vundef | Vlong i => Vundef | Vfloat f => Vundef | Vsingle f => Vundef | Vptr b z => Vptr b (Ptrofs.add z (Ptrofs.repr delta)) end | Errors.Error e => @always val val Vundef end | None => @always val val Vundef end | Tunion id att => match @PTree.get composite id (@cenv_cs CS) with | Some co => force_ptr | None => @always val val Vundef end end v) *)
subst v.
(* Goal: tc_val pt (match typeof e with | Tvoid => @always val val Vundef | Tint i s a => @always val val Vundef | Tlong s a => @always val val Vundef | Tfloat f a => @always val val Vundef | Tpointer t a => @always val val Vundef | Tarray t z a => @always val val Vundef | Tfunction t t0 c => @always val val Vundef | Tstruct id att => match @PTree.get composite id (@cenv_cs CS) with | Some co => match field_offset (@cenv_cs CS) i (co_members co) with | Errors.OK delta => fun v : val => match v with | Vundef => Vundef | Vint i => Vundef | Vlong i => Vundef | Vfloat f => Vundef | Vsingle f => Vundef | Vptr b z => Vptr b (Ptrofs.add z (Ptrofs.repr delta)) end | Errors.Error e => @always val val Vundef end | None => @always val val Vundef end | Tunion id att => match @PTree.get composite id (@cenv_cs CS) with | Some co => force_ptr | None => @always val val Vundef end end (@eval_lvalue CS e (mkEnviron ge ve te))) *)
destruct PTR as [b [ofs ?]].
(* Goal: @ex block (fun base : block => @ex Ptrofs.int (fun ofs : Ptrofs.int => @eq val match @Map.get (prod block type) ve i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block ge i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end (Vptr base ofs))) *)
destruct (typeof e); try now inv H2.
+ destruct (cenv_cs ! i0) as [co |]; try now inv H2.
(* Goal: @ex block (fun base : block => @ex Ptrofs.int (fun ofs : Ptrofs.int => @eq val match @Map.get (prod block type) ve i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block ge i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end (Vptr base ofs))) *)
  destruct (field_offset cenv_cs i (co_members co)); try now inv H2.
(* Goal: tc_val pt (force_ptr (@eval_lvalue CS e (mkEnviron ge ve te))) *)
  destruct (eval_lvalue e (mkEnviron ge ve te)); try now inv H6.
(* Goal: @eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero) *)
  destruct pt; inv H1; auto.
(* Goal: (if eqb_type (Tpointer t a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b (Ptrofs.add i1 (Ptrofs.repr z))) *)
  red; simple_if_tac; apply I.
+ destruct (cenv_cs ! i0) as [co |]; try now inv H2.
(* Goal: tc_val pt (force_ptr (@eval_lvalue CS e (mkEnviron ge ve te))) *)
  destruct (eval_lvalue e (mkEnviron ge ve te)); try now inv H6.
Qed.

Lemma typecheck_expr_sound_Evar:
(* Goal: tc_val pt match @Map.get block ge i with | Some b => Vptr b Ptrofs.zero | None => Vundef end *)
  forall {CS: compspecs} Delta rho m i t,
  typecheck_environ Delta rho ->
  denote_tc_assert (typecheck_expr Delta (Evar i t)) rho m ->
  tc_val (typeof (Evar i t)) (eval_expr (Evar i t) rho).
Proof.
(* Goal: forall (CS : compspecs) (Delta : tycontext) (rho : environ) (m : rmap) (i : ident) (t : type) (_ : typecheck_environ Delta rho) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_expr CS Delta (Etempvar i t)) rho) m), tc_val (typeof (Etempvar i t)) (@eval_expr CS (Etempvar i t) rho) *)
intros.
assert (MODE: access_mode t = By_reference)
 by (unfold typecheck_expr in H0; destruct (access_mode t); try (hnf in H0; contradiction); auto).
(* Goal: tc_val pt (@eval_lvalue CS (Ederef e t) rho) *)
simpl. super_unfold_lift. unfold deref_noload.

(* Goal: tc_val t (eval_var i t rho) *)
unfold typecheck_environ in H. intuition.
(* Goal: tc_val t (eval_id i rho) *)
destruct rho.
(* Goal: tc_val pt (@eval_expr CS e rho) *)
simpl in H0. rewrite MODE in H0.
unfold get_var_type in *.

(* Goal: tc_val t (eval_var i t (mkEnviron ge ve te)) *)
unfold eval_var.
destruct_var_types i; rewrite ?Heqo, ?Heqo0 in *;
try rewrite eqb_type_eq in *; simpl in *; intuition.
(* Goal: tc_val t (eval_var i t rho) *)
- remember (type_eq t t0). destruct s; intuition.
(* Goal: tc_val t (Vptr b Ptrofs.zero) *)
 subst.
(* Goal: tc_val pt (@eval_lvalue CS (Ederef e t) rho) *)
 simpl.
(* Goal: tc_val pt (@eval_lvalue CS (Ederef e t) rho) *)
simpl. destruct t0; try destruct i0; try destruct s; try destruct f; inv MODE; simpl; auto.
- destruct_glob_types i; rewrite ?Heqo1, ?Heqo2 in *; [| inv H0].
simpl in *.
(* Goal: tc_val t (Vptr b Ptrofs.zero) *)
remember (eqb_type t t0).
symmetry in Heqb0. destruct b0; simpl in *; [| inv H0].
(* Goal: tc_val t (Vptr b Ptrofs.zero) *)
apply eqb_type_true in Heqb0.
(* Goal: tc_val t (Vptr b Ptrofs.zero) *)
subst.
unfold typecheck_glob_environ in *.
(* Goal: @eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero) *)
destruct t0 as [| [| | |] [|] | | [|] | | | | |]; inv MODE; simpl; auto.
Qed.

Definition unOp_result_type op t :=
match op with
  | Cop.Onotbool =>match t with
                                | Tint _ _ _ => Tint IBool Signed noattr
                                | Tlong _ _ => Tint IBool Signed noattr
                                | Tpointer _ _ => Tint I32 Signed noattr
                                | Tfloat _ _ => Tint IBool Signed noattr
                                | Tarray _ _ _ => Tint IBool Signed noattr
                                | Tfunction _ _ _ => Tint IBool Signed noattr
                                | _ => Tvoid
                                end
  | Cop.Onotint => match t with
                                | Tint _ _ _ => Tint I32 Signed noattr
                                | Tlong _ _ => Tlong Signed noattr
                                | _ => Tvoid
                                end
  | Cop.Oneg => match t with
                           | Tint _ _ _ => Tint I32 Signed noattr
                           | Tlong _ _ => Tlong Signed noattr
                           | Tfloat _ _ => t
                           | _ => Tvoid
                           end
  | Cop.Oabsfloat => t
end.


Lemma tc_bool_e: forall {CS: compspecs} b a rho m, (* copied from binop_lemmas.v *)
  app_pred (denote_tc_assert (tc_bool b a) rho) m ->
  b = true.
Proof.
(* Goal: forall (CS : compspecs) (Delta : tycontext) (rho : environ) (m : rmap) (i : ident) (t : type) (_ : typecheck_environ Delta rho) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_expr CS Delta (Etempvar i t)) rho) m), tc_val (typeof (Etempvar i t)) (@eval_expr CS (Etempvar i t) rho) *)
intros.
(* Goal: @eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero) *)
destruct b; simpl in H; auto.
Qed.

Lemma tc_val_of_bool_int_type:
 forall b t, is_int_type t = true ->
  tc_val t (Val.of_bool b).
Proof.
(* Goal: forall (CS : compspecs) (Delta : tycontext) (rho : environ) (m : rmap) (i : ident) (t : type) (_ : typecheck_environ Delta rho) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_expr CS Delta (Etempvar i t)) rho) m), tc_val (typeof (Etempvar i t)) (@eval_expr CS (Etempvar i t) rho) *)
 intros.
 destruct t as [ | [ | | | ] [ | ] | | [ | ] | | | | | ];
 try inv H; destruct b; simpl; try split; auto;
rewrite <- Z.leb_le; reflexivity.
Qed.

Lemma typecheck_unop_sound:
(* Goal: tc_val pt match @Map.get block ge i with | Some b => Vptr b Ptrofs.zero | None => Vundef end *)
 forall {CS: compspecs} Delta rho m u e t
 (H: typecheck_environ Delta rho)
 (IHe: (denote_tc_assert (typecheck_expr Delta e) rho m ->
          tc_val (typeof e) (eval_expr e rho)) /\
          (forall pt : type,
           denote_tc_assert (typecheck_lvalue Delta e) rho m ->
           is_pointer_type pt = true ->
           tc_val pt (eval_lvalue e rho)))
  (H0: denote_tc_assert (typecheck_expr Delta (Eunop u e t)) rho m),
  tc_val t (eval_expr (Eunop u e t) rho).
Proof.
(* Goal: forall (CS : compspecs) (Delta : tycontext) (rho : environ) (m : rmap) (i : ident) (t : type) (_ : typecheck_environ Delta rho) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_expr CS Delta (Etempvar i t)) rho) m), tc_val (typeof (Etempvar i t)) (@eval_expr CS (Etempvar i t) rho) *)
intros.
(* Goal: tc_val pt (@liftx (Tarrow val (LiftEnviron val)) (@eval_field CS (typeof e) i) (@eval_lvalue CS e) rho) *)
simpl in H0. rewrite denote_tc_assert_andp in H0. destruct H0.
(* Goal: tc_val pt (@eval_expr CS e rho) *)
destruct IHe as [? _].
specialize (H2 H1).
simpl eval_expr.
(* Goal: tc_val pt (@eval_expr CS e rho) *)
unfold_lift.
clear - H2 H0. 
unfold eval_unop, sem_unary_operation, force_val1.
destruct u; unfold tc_val in H2; simpl in H0;
unfold sem_notbool, sem_notint, sem_neg, sem_absfloat, bool_val in *;
super_unfold_lift; simpl;
destruct (typeof e) as [ | [ | | | ] [ | ] | | [ | ] | | | | | ];
 try contradiction;
 repeat match goal with
 | H:  app_pred (denote_tc_assert (tc_andp _ _) _) _ |- _ =>
        rewrite denote_tc_assert_andp in H; destruct H
 | H: app_pred (denote_tc_assert (tc_bool _ _) _) _ |- _ => 
      apply tc_bool_e in H
 | H: app_pred (denote_tc_assert (tc_int_or_ptr_type _) _) _ |- _ => 
      apply tc_bool_e in H
| H: (if eqb_type ?T1 ?T2 then _ else _) _ |- _ =>
   let J := fresh "J" in
   destruct (eqb_type T1 T2) eqn:J;
   [apply eqb_type_true in J | apply eqb_type_false in J]
end;
 destruct (eval_expr e rho) eqn:?; try contradiction;
 try discriminate;
 try solve [apply tc_val_of_bool_int_type; auto].
all: try solve [
  destruct t as [ | [ | | | ] [ | ] | | [ | ] | | | | | ]; 
  match goal with H: _ _ = true |- _ => inv H end;
            try reflexivity; auto;
             simpl tc_val; try split; auto;
             rewrite <- Z.leb_le; reflexivity].
Qed.

Lemma same_base_tc_val : forall v t1 t2,
same_base_type t1 t2 = true ->
tc_val t1 v ->
 tc_val t2 v.
Proof.
(* Goal: forall (CS : compspecs) (Delta : tycontext) (rho : environ) (m : rmap) (i : ident) (t : type) (_ : typecheck_environ Delta rho) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_expr CS Delta (Etempvar i t)) rho) m), tc_val (typeof (Etempvar i t)) (@eval_expr CS (Etempvar i t) rho) *)
intros. destruct t1; destruct t2;
    try destruct f; try destruct f0; try destruct f1;
   unfold tc_val in *; 
 try match type of H0 with (if ?A then _ else _) _ => 
         destruct A eqn:?J;
         [apply  eqb_type_true in J | apply eqb_type_false in J]
    end;
   try solve [inv H]; destruct v; auto;
   try solve [inv H0];
   try solve [simple_if_tac; apply I].
(* Goal: (if eqb_type (Tpointer t2 a) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vint i) *)
   unfold same_base_type in H.
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vint i) *)
(* Goal: (if eqb_type (Tpointer t2 a) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vint i) *)
   destruct (eqb_type (Tpointer t2 a0) int_or_ptr_type).
(* Goal: is_pointer_or_null (Vptr b i) *)
   apply I. inv H0. reflexivity.
(* Goal: (if eqb_type (Tpointer t2 a) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vint i) *)
   unfold same_base_type in H.
(* Goal: (if eqb_type (Tpointer t2 a) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vint i) *)
   destruct (eqb_type (Tpointer t2 a) int_or_ptr_type).
(* Goal: is_pointer_or_null (Vptr b i) *)
   apply I. inv H0. reflexivity.
Qed.

Lemma typecheck_temp_sound:
(* Goal: tc_val pt match @Map.get block ge i with | Some b => Vptr b Ptrofs.zero | None => Vundef end *)
  forall {CS: compspecs} Delta rho m i t,
  typecheck_environ Delta rho ->
  denote_tc_assert (typecheck_expr Delta (Etempvar i t)) rho m ->
  tc_val (typeof (Etempvar i t)) (eval_expr (Etempvar i t) rho).
Proof.
(* Goal: forall (CS : compspecs) (Delta : tycontext) (rho : environ) (m : rmap) (i : ident) (t : type) (_ : typecheck_environ Delta rho) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_expr CS Delta (Etempvar i t)) rho) m), tc_val (typeof (Etempvar i t)) (@eval_expr CS (Etempvar i t) rho) *)
intros.
simpl in *. destruct rho.
(* Goal: tc_val t (eval_id i (mkEnviron ge ve te)) *)
destruct H as [H1 _].
unfold typecheck_temp_environ in *.
unfold eval_id, force_val in *.

(* Goal: tc_val pt (@eval_lvalue CS (Ederef e t) rho) *)
simpl.
destruct Delta; simpl in *.
unfold temp_types in *. simpl in *.
(* Goal: tc_val t match @Map.get val te i with | Some v' => v' | None => Vundef end *)
specialize (H1 i).
(* Goal: tc_val t match @Map.get val te i with | Some v' => v' | None => Vundef end *)
destruct (tyc_temps ! i); try (contradiction H0).
(* Goal: tc_val t match @Map.get val te i with | Some v' => v' | None => Vundef end *)
destruct (H1 _ (eq_refl _)) as [v ?]. clear H1.
(* Goal: tc_val t match @Map.get val te i with | Some v' => v' | None => Vundef end *)
destruct H.
(* Goal: tc_val t match @Map.get val te i with | Some v' => v' | None => Vundef end *)
rewrite H.
(* Goal: tc_val pt (@eval_expr CS e rho) *)
simpl in H0.
(* Goal: tc_val t v *)
destruct (is_neutral_cast t0 t) eqn:?.
+ simpl in H0.
(* Goal: tc_val t v *)
  rewrite H in H0.
(* Goal: tc_val t v *)
  destruct H0 as [? [? ?]].
(* Goal: tc_val t v *)
  inv H0.
(* Goal: @eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero) *)
  symmetry in Heqb; eapply neutral_cast_subsumption; eauto.
+ destruct (same_base_type t0 t) eqn:?; [ | inv H0].
(* Goal: tc_val pt (@eval_expr CS e rho) *)
  simpl in H0.
(* Goal: tc_val t v *)
  rewrite H in H0.
(* Goal: tc_val t v *)
  destruct H0 as [? [? ?]].
(* Goal: tc_val t v *)
  inv H0.
(* Goal: @eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero) *)
  eapply same_base_tc_val; eauto.
Qed.

Lemma typecheck_deref_sound:
(* Goal: tc_val pt match @Map.get block ge i with | Some b => Vptr b Ptrofs.zero | None => Vundef end *)
  forall {CS: compspecs} Delta rho m e t pt,
   typecheck_environ Delta rho ->
   (denote_tc_assert (typecheck_expr Delta e) rho m ->
    tc_val (typeof e) (eval_expr e rho)) /\
    (forall pt0 : type,
     denote_tc_assert (typecheck_lvalue Delta e) rho m ->
     is_pointer_type pt0 = true -> tc_val pt0 (eval_lvalue e rho)) ->
     denote_tc_assert (typecheck_lvalue Delta (Ederef e t)) rho m ->
    is_pointer_type pt = true ->
    tc_val pt (eval_lvalue (Ederef e t) rho).
Proof.
(* Goal: forall (CS : compspecs) (Delta : tycontext) (rho : environ) (m : rmap) (e : expr) (t pt : type) (_ : typecheck_environ Delta rho) (_ : and (forall _ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_expr CS Delta e) rho) m, tc_val (typeof e) (@eval_expr CS e rho)) (forall (pt0 : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_lvalue CS Delta e) rho) m) (_ : @eq bool (is_pointer_type pt0) true), tc_val pt0 (@eval_lvalue CS e rho))) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_lvalue CS Delta (Ederef e t)) rho) m) (_ : @eq bool (is_pointer_type pt) true), tc_val pt (@eval_lvalue CS (Ederef e t) rho) *)
intros until pt. intros H IHe H0 H1.
(* Goal: tc_val pt (@eval_lvalue CS (Ederef e t) rho) *)
simpl. unfold lift.
(* Goal: tc_val pt (@eval_expr CS e rho) *)
simpl in H0.
(* Goal: tc_val pt (@liftx (Tarrow val (LiftEnviron val)) (@eval_field CS (typeof e) i) (@eval_lvalue CS e) rho) *)
repeat rewrite denote_tc_assert_andp in H0.
(* Goal: tc_val pt (@eval_expr CS e rho) *)
destruct H0 as [[? ?] ?].
(* Goal: tc_val pt (@eval_expr CS e rho) *)
destruct IHe as[ ? _].
(* Goal: tc_val pt (@eval_expr CS e rho) *)
specialize (H4 H0).
(* Goal: tc_val pt (@eval_expr CS e rho) *)
revert H2; case_eq (is_pointer_type (typeof e)); intros; hnf in H2; try contradiction.
(* Goal: tc_val pt (@eval_expr CS e rho) *)
clear H H5 H4.
(* Goal: tc_val pt (@eval_expr CS e rho) *)
hnf in H3. unfold_lift in H3; hnf in H3.
(* Goal: tc_val pt (@eval_expr CS e rho) *)
unfold_lift.
(* Goal: tc_val pt (@eval_expr CS e rho) *)
destruct (eval_expr e rho); try contradiction.
(* Goal: tc_val pt (Vptr b i) *)
destruct pt; try solve [inv H1; reflexivity].
(* Goal: tc_val (Tpointer pt a) (Vptr b i) *)
unfold tc_val.
(* Goal: (if eqb_type (Tpointer pt a) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
unfold is_pointer_type in H1.
(* Goal: (if eqb_type (Tpointer pt a) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
destruct (eqb_type (Tpointer pt a) int_or_ptr_type); inv H1.
(* Goal: is_pointer_or_null (Vptr b i) *)
apply I.
Qed.

