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

Require Import VST.veric.mpred.

Lemma neutral_cast_lemma: forall t1 t2 v,
  is_neutral_cast t1 t2 = true ->
  tc_val t1 v -> eval_cast t1 t2 v = v.
Proof.
(* Goal: forall (CS : compspecs) (b : bool) (a : tc_error) (rho : environ) (m : rmap) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (tc_bool b a) rho) m), @eq bool b true *)
intros.
(* Goal: tc_val t2 v *)
assert (- two_p (16-1) < Byte.min_signed) by (compute; congruence).
(* Goal: tc_val t2 v *)
assert (two_p (16-1) > Byte.max_signed) by (compute; congruence).
(* Goal: tc_val t2 v *)
assert (two_p 16 > Byte.max_unsigned) by (compute; congruence).
(* Goal: tc_val t2 v *)
assert (- two_p (8-1) = Byte.min_signed) by reflexivity.
(* Goal: tc_val t2 v *)
assert (two_p (8-1) - 1 = Byte.max_signed) by reflexivity.
(* Goal: tc_val t2 v *)
assert (two_p 8 - 1 = Byte.max_unsigned) by reflexivity.
 destruct t1 as [ | [ | | | ] [ | ] | | [ | ] | | | | | ],
 t2 as [ | [ | | | ] [ | ] | | [ | ] | | | | | ];
 unfold eval_cast, sem_cast, classify_cast,
  sem_cast_pointer, sem_cast_i2bool, sem_cast_l2bool;
try solve [
 try match goal with |- context [Archi.ptr64] => destruct Archi.ptr64 end;
 inversion H; clear H; try reflexivity;
 destruct v; unfold tc_val, is_int in H0; try contradiction;
 simpl; f_equal;
 try (first [apply sign_ext_inrange| apply zero_ext_inrange];
       try omega;
    match type of H0 with _ \/ _ =>
       destruct H0; subst i; simpl;
       try  rewrite Int.signed_zero;
       try  rewrite Int.unsigned_zero;
       try change (Int.signed Int.one) with 1;
       try change (Int.unsigned Int.one) with 1;
       clear; compute; split; congruence
    end);
 try (destruct H0; subst i; try rewrite Int.eq_true; auto)].
Qed.

Lemma neutral_cast_subsumption: forall t1 t2 v,
  is_neutral_cast t1 t2 = true ->
  tc_val t1 v -> tc_val t2 v.
Proof.
(* Goal: forall (CS : compspecs) (b : bool) (a : tc_error) (rho : environ) (m : rmap) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (tc_bool b a) rho) m), @eq bool b true *)
intros.
(* Goal: tc_val t2 v *)
assert (- two_p (16-1) < Byte.min_signed) by (compute; congruence).
(* Goal: tc_val t2 v *)
assert (two_p (16-1) > Byte.max_signed) by (compute; congruence).
(* Goal: tc_val t2 v *)
assert (two_p 16 > Byte.max_unsigned) by (compute; congruence).
(* Goal: tc_val t2 v *)
assert (- two_p (8-1) = Byte.min_signed) by reflexivity.
(* Goal: tc_val t2 v *)
assert (two_p (8-1) - 1 = Byte.max_signed) by reflexivity.
(* Goal: tc_val t2 v *)
assert (two_p 8 - 1 = Byte.max_unsigned) by reflexivity.
destruct t1 as [ | [ | | | ] [ | ] | | [ | ] | | | | | ],
 t2   as [ | [ | | | ] [ | ] | | [ | ] | | | | | ]; inv H;
 destruct v; try solve [contradiction H0]; try apply I;
 unfold tc_val, is_int in *;
  auto;
 try omega;
 try
    match type of H0 with _ \/ _ =>
       destruct H0; subst i; simpl;
       try  rewrite Int.signed_zero;
       try  rewrite Int.unsigned_zero;
       try change (Int.signed Int.one) with 1;
       try change (Int.unsigned Int.one) with 1;
       clear; compute; try split; congruence
    end;
 try match type of H0 with context [if ?A then _ else _] => destruct A; contradiction H0 end.
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 destruct (eqb_type (Tpointer t2 a0) int_or_ptr_type) eqn:?H.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if orb (andb (negb false) (negb false)) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb false ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb false (negb false) then tc_TT else if andb false (negb false) then tc_isptr v else if andb false ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
 apply I.
(* Goal: is_pointer_or_null (Vint i) *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 apply eqb_type_false in H.
(* Goal: is_pointer_or_null (Vint i) *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
(* 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 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 destruct (eqb_type (Tpointer t1 a) int_or_ptr_type) eqn:?H; auto.
(* Goal: is_pointer_or_null (Vint i) *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
(* 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 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 apply eqb_type_true in H7. inv H7. simpl in *.
(* Goal: if Archi.ptr64 then False else @eq Int.int i Int.zero *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
(* 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 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 rewrite orb_false_r in H8. 
(* Goal: if Archi.ptr64 then False else @eq Int.int i Int.zero *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
(* 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 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 rewrite andb_true_iff in H8. destruct H8.
(* Goal: is_pointer_or_null (Vint i) *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
(* 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 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 destruct t2; inv H7.
(* Goal: if Archi.ptr64 then False else @eq Int.int i Int.zero *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
(* 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 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 destruct a0.
(* Goal: if Archi.ptr64 then False else @eq Int.int i Int.zero *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
(* 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 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 destruct attr_volatile; try solve [inv H8].
(* Goal: if Archi.ptr64 then False else @eq Int.int i Int.zero *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
(* 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 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 simpl in H8.
(* Goal: if Archi.ptr64 then False else @eq Int.int i Int.zero *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
(* 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 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 destruct attr_alignas; try solve [inv H8].
(* Goal: if Archi.ptr64 then False else @eq Int.int i Int.zero *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
(* 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 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 destruct n as [ | ]; try solve [inv H8].
(* Goal: if Archi.ptr64 then False else @eq Int.int i Int.zero *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
(* 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 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 apply Peqb_true_eq in H8. subst p.
(* Goal: if Archi.ptr64 then False else @eq Int.int i Int.zero *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
(* 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 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 contradiction H. reflexivity.
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 destruct (eqb_type (Tpointer t2 a0) int_or_ptr_type) eqn:?H.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if orb (andb (negb false) (negb false)) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb false ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb false (negb false) then tc_TT else if andb false (negb false) then tc_isptr v else if andb false ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
 apply I.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if orb (andb (negb false) (negb false)) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb false ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb false (negb false) then tc_TT else if andb false (negb false) then tc_isptr v else if andb false ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
 apply I.
Qed.

Lemma neutral_cast_subsumption': forall t1 t2 v,
  is_neutral_cast (implicit_deref t1) t2 = true ->
  tc_val t1 v -> tc_val t2 v.
Proof.
(* Goal: forall (CS : compspecs) (b : bool) (a : tc_error) (rho : environ) (m : rmap) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (tc_bool b a) rho) m), @eq bool b true *)
intros.
(* Goal: tc_val t2 v *)
assert (- two_p (16-1) < Byte.min_signed) by (compute; congruence).
(* Goal: tc_val t2 v *)
assert (two_p (16-1) > Byte.max_signed) by (compute; congruence).
(* Goal: tc_val t2 v *)
assert (two_p 16 > Byte.max_unsigned) by (compute; congruence).
(* Goal: tc_val t2 v *)
assert (- two_p (8-1) = Byte.min_signed) by reflexivity.
(* Goal: tc_val t2 v *)
assert (two_p (8-1) - 1 = Byte.max_signed) by reflexivity.
(* Goal: tc_val t2 v *)
assert (two_p 8 - 1 = Byte.max_unsigned) by reflexivity.
destruct t1 as [ | [ | | | ] [ | ] | | [ | ] | | | | | ],
 t2   as [ | [ | | | ] [ | ] | | [ | ] | | | | | ]; inv H;
 destruct v; try solve [contradiction H0]; try apply I;
 unfold tc_val, is_int in *;
  auto;
 try omega;
 try
    match type of H0 with _ \/ _ =>
       destruct H0; subst i; simpl;
       try  rewrite Int.signed_zero;
       try  rewrite Int.unsigned_zero;
       try change (Int.signed Int.one) with 1;
       try change (Int.unsigned Int.one) with 1;
       clear; compute; try split; congruence
    end;
 try match type of H0 with context [if ?A then _ else _] => destruct A; contradiction H0 end.
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 destruct (eqb_type (Tpointer t2 a0) int_or_ptr_type) eqn:?H.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if orb (andb (negb false) (negb false)) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb false ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb false (negb false) then tc_TT else if andb false (negb false) then tc_isptr v else if andb false ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
 apply I.
(* Goal: is_pointer_or_null (Vint i) *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 apply eqb_type_false in H.
(* Goal: is_pointer_or_null (Vint i) *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
(* 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 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 destruct (eqb_type (Tpointer t1 a) int_or_ptr_type) eqn:?H; auto.
(* Goal: is_pointer_or_null (Vint i) *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
(* 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 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 apply eqb_type_true in H7. inv H7. simpl in *.
(* Goal: if Archi.ptr64 then False else @eq Int.int i Int.zero *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
(* 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 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 rewrite orb_false_r in H8. 
(* Goal: if Archi.ptr64 then False else @eq Int.int i Int.zero *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
(* 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 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 rewrite andb_true_iff in H8. destruct H8.
(* Goal: is_pointer_or_null (Vint i) *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
(* 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 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 destruct t2; inv H7.
(* Goal: if Archi.ptr64 then False else @eq Int.int i Int.zero *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
(* 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 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 destruct a0.
(* Goal: if Archi.ptr64 then False else @eq Int.int i Int.zero *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
(* 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 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 destruct attr_volatile; try solve [inv H8].
(* Goal: if Archi.ptr64 then False else @eq Int.int i Int.zero *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
(* 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 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 simpl in H8.
(* Goal: if Archi.ptr64 then False else @eq Int.int i Int.zero *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
(* 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 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 destruct attr_alignas; try solve [inv H8].
(* Goal: if Archi.ptr64 then False else @eq Int.int i Int.zero *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
(* 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 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 destruct n as [ | ]; try solve [inv H8].
(* Goal: if Archi.ptr64 then False else @eq Int.int i Int.zero *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
(* 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 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 apply Peqb_true_eq in H8. subst p.
(* Goal: if Archi.ptr64 then False else @eq Int.int i Int.zero *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
(* 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 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 contradiction H. reflexivity.
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 destruct (eqb_type (Tpointer t2 a0) int_or_ptr_type) eqn:?H.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if orb (andb (negb false) (negb false)) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb false ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb false (negb false) then tc_TT else if andb false (negb false) then tc_isptr v else if andb false ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
 apply I.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if orb (andb (negb false) (negb false)) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb false ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb false (negb false) then tc_TT else if andb false (negb false) then tc_isptr v else if andb false ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
 apply I.
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 destruct (eqb_type (Tpointer t2 a0) int_or_ptr_type) eqn:?H.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if orb (andb (negb false) (negb false)) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb false ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb false (negb false) then tc_TT else if andb false (negb false) then tc_isptr v else if andb false ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
 apply I.
(* Goal: is_pointer_or_null (Vint i) *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 apply eqb_type_false in H.
(* Goal: is_pointer_or_null (Vint i) *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 auto.
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 destruct (eqb_type (Tpointer t2 a0) int_or_ptr_type) eqn:?H.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if orb (andb (negb false) (negb false)) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb false ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb false (negb false) then tc_TT else if andb false (negb false) then tc_isptr v else if andb false ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
 apply I.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if orb (andb (negb false) (negb false)) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb false ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb false (negb false) then tc_TT else if andb false (negb false) then tc_isptr v else if andb false ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
 apply I.
Qed.

(** Denotation functions for each of the assertions that can be produced by the typechecker **)

Definition denote_tc_iszero v : mpred :=
         match v with
         | Vint i => prop (is_true (Int.eq i Int.zero))
         | Vlong i => prop (is_true (Int64.eq i Int64.zero))
         | _ => FF
         end.

Definition denote_tc_nonzero v : mpred :=
         match v with
         | Vint i => prop (i <> Int.zero)
         | Vlong i =>prop (i <> Int64.zero)
         | _ => FF end.

Definition denote_tc_igt i v : mpred :=
     match v with
     | Vint i1 => prop (Int.unsigned i1 < Int.unsigned i)
     | _ => FF
     end.

Definition denote_tc_lgt l v : mpred :=
     match v with
     | Vlong l1 => prop (Int64.unsigned l1 < Int64.unsigned l)
     | _ => FF
     end.

Definition Zoffloat (f:float): option Z := (**r conversion to Z *)
  match f with
    | Fappli_IEEE.B754_finite s m (Zpos e) _ =>
       Some (Fcore_Zaux.cond_Zopp s (Zpos m) * Zpower_pos 2 e)
    | Fappli_IEEE.B754_finite s m 0 _ => Some (Fcore_Zaux.cond_Zopp s (Zpos m))
    | Fappli_IEEE.B754_finite s m (Zneg e) _ => Some (Fcore_Zaux.cond_Zopp s (Zpos m / Zpower_pos 2 e))
    | Fappli_IEEE.B754_zero _ => Some 0
    | _ => None
  end.  (* copied from CompCert 2.3, because it's missing in CompCert 2.4 *)

Definition Zofsingle (f: float32): option Z := (**r conversion to Z *)
  match f with
    | Fappli_IEEE.B754_finite s m (Zpos e) _ =>
       Some (Fcore_Zaux.cond_Zopp s (Zpos m) * Zpower_pos 2 e)
    | Fappli_IEEE.B754_finite s m 0 _ => Some (Fcore_Zaux.cond_Zopp s (Zpos m))
    | Fappli_IEEE.B754_finite s m (Zneg e) _ => Some (Fcore_Zaux.cond_Zopp s (Zpos m / Zpower_pos 2 e))
    | Fappli_IEEE.B754_zero _ => Some 0
    | _ => None
  end.  (* copied from CompCert 2.3, because it's missing in CompCert 2.4 *)


Definition denote_tc_Zge z v : mpred :=
          match v with
                     | Vfloat f => match Zoffloat f with
                                    | Some n => prop (z >= n)
                                    | None => FF
                                   end
                     | Vsingle f => match Zofsingle f with
                                    | Some n => prop (z >= n)
                                    | None => FF
                                   end
                     | _ => FF
                  end.

Definition denote_tc_Zle z v : mpred :=
          match v with
                     | Vfloat f => match Zoffloat f with
                                    | Some n => prop (z <= n)
                                    | None => FF
                                   end
                     | Vsingle f => match Zofsingle f with
                                    | Some n => prop (z <= n)
                                    | None => FF
                                   end
                     | _ => FF
                  end.

Definition sameblock v1 v2 : bool :=
         match v1, v2 with
          | Vptr b1 _, Vptr b2 _ => peq b1 b2
          | _, _ => false
         end.

Definition denote_tc_samebase v1 v2 : mpred :=
       prop (is_true (sameblock v1 v2)).

(** Case for division of int min by -1, which would cause overflow **)
Definition denote_tc_nodivover v1 v2 : mpred :=
match v1, v2 with
          | Vint n1, Vint n2 => prop (~(n1 = Int.repr Int.min_signed /\ n2 = Int.mone))
          | Vlong n1, Vlong n2 => prop (~(n1 = Int64.repr Int64.min_signed /\ n2 = Int64.mone))
          | Vint n1, Vlong n2 => TT
          | Vlong n1, Vint n2 => prop (~ (n1 = Int64.repr Int64.min_signed  /\ n2 = Int.mone))
          | _ , _ => FF
        end.

Definition denote_tc_nosignedover (op: Z->Z->Z) v1 v2 : mpred :=
 match v1,v2 with
 | Vint n1, Vint n2 => 
   prop (Int.min_signed <= op (Int.signed n1) (Int.signed n2) <= Int.max_signed)
 | Vlong n1, Vlong n2 =>
   prop (Int64.min_signed <= op (Int64.signed n1) (Int64.signed n2) <= Int64.max_signed)
 | Vint n1, Vlong n2 =>
   prop (Int64.min_signed <= op (Int.signed n1) (Int64.signed n2) <= Int64.max_signed)
 | Vlong n1, Vint n2 =>
   prop (Int64.min_signed <= op (Int64.signed n1) (Int.signed n2) <= Int64.max_signed)
 | _, _ => FF
 end.

Definition denote_tc_initialized id ty rho : mpred :=
    prop (exists v, Map.get (te_of rho) id = Some v
               /\ tc_val ty v).

Definition denote_tc_isptr v : mpred :=
  prop (isptr v).

Definition denote_tc_isint v : mpred :=
  prop (is_int I32 Signed v).

Definition denote_tc_islong v : mpred :=
  prop (is_long v).

Definition test_eq_ptrs v1 v2 : mpred :=
  if sameblock v1 v2
  then (andp (weak_valid_pointer v1) (weak_valid_pointer v2))
  else (andp (valid_pointer v1) (valid_pointer v2)).

Definition test_order_ptrs v1 v2 : mpred :=
  if sameblock v1 v2
  then (andp (weak_valid_pointer v1) (weak_valid_pointer v2))
  else FF.

Definition denote_tc_test_eq v1 v2 : mpred :=
 match v1, v2 with
 | Vint i, Vint j => 
     if Archi.ptr64 then FF else andp (prop (i = Int.zero)) (prop (j = Int.zero))
 | Vlong i, Vlong j => 
     if Archi.ptr64 then andp (prop (i = Int64.zero)) (prop (j = Int64.zero)) else FF
 | Vint i, Vptr _ _ =>
      if Archi.ptr64 then FF else andp (prop (i = Int.zero)) (weak_valid_pointer v2)
 | Vlong i, Vptr _ _ =>
      if Archi.ptr64 then andp (prop (i = Int64.zero)) (weak_valid_pointer v2) else FF
 | Vptr _ _, Vint i =>
      if Archi.ptr64 then FF else andp (prop (i = Int.zero)) (weak_valid_pointer v1)
 | Vptr _ _, Vlong i =>
      if Archi.ptr64 then andp (prop (i = Int64.zero)) (weak_valid_pointer v1) else FF
 | Vptr _ _, Vptr _ _ =>
      test_eq_ptrs v1 v2
 | _, _ => FF
 end.

Definition denote_tc_test_order v1 v2 : mpred :=
 match v1, v2 with
 | Vint i, Vint j => if Archi.ptr64 then FF else andp (prop (i = Int.zero)) (prop (j = Int.zero))
 | Vlong i, Vlong j => if Archi.ptr64 then andp (prop (i = Int64.zero)) (prop (j = Int64.zero)) else FF
 | Vptr _ _, Vptr _ _ =>
      test_order_ptrs v1 v2
 | _, _ => FF
 end.

Definition typecheck_error (e: tc_error) : Prop := False.

Fixpoint denote_tc_assert {CS: compspecs}(a: tc_assert) : environ -> mpred :=
  match a with
  | tc_FF msg => `(prop (typecheck_error msg))
  | tc_TT => `TT
  | tc_andp' b c => `andp (denote_tc_assert b) (denote_tc_assert c)
  | tc_orp' b c => `orp (denote_tc_assert b) (denote_tc_assert c)
  | tc_nonzero' e => `denote_tc_nonzero (eval_expr e)
  | tc_isptr e => `denote_tc_isptr (eval_expr e)
  | tc_isint e => `denote_tc_isint (eval_expr e)
  | tc_islong e => `denote_tc_islong (eval_expr e)
  | tc_test_eq' e1 e2 => `denote_tc_test_eq (eval_expr e1) (eval_expr e2)
  | tc_test_order' e1 e2 => `denote_tc_test_order (eval_expr e1) (eval_expr e2)
  | tc_ilt' e i => `(denote_tc_igt i) (eval_expr e)
  | tc_llt' e l => `(denote_tc_lgt l) (eval_expr e)
  | tc_Zle e z => `(denote_tc_Zge z) (eval_expr e)
  | tc_Zge e z => `(denote_tc_Zle z) (eval_expr e)
  | tc_samebase e1 e2 => `denote_tc_samebase (eval_expr e1) (eval_expr e2)
  | tc_nodivover' v1 v2 => `denote_tc_nodivover (eval_expr v1) (eval_expr v2)
  | tc_initialized id ty => denote_tc_initialized id ty
  | tc_iszero' e => `denote_tc_iszero (eval_expr e)
  | tc_nosignedover op e1 e2 => `(denote_tc_nosignedover op) (eval_expr e1) (eval_expr e2)
 end.

Lemma and_False: forall x, (x /\ False) = False.
Proof.
(* Goal: forall x : Prop, @eq Prop (and False x) False *)
intros; apply prop_ext; intuition.
Qed.

Lemma and_True: forall x, (x /\ True) = x.
Proof.
(* Goal: forall x : Prop, @eq Prop (and False x) False *)
intros; apply prop_ext; intuition.
Qed.

Lemma True_and: forall x, (True /\ x) = x.
Proof.
(* Goal: forall x : Prop, @eq Prop (and False x) False *)
intros; apply prop_ext; intuition.
Qed.

Lemma False_and: forall x, (False /\ x) = False.
Proof.
(* Goal: forall x : Prop, @eq Prop (and False x) False *)
intros; apply prop_ext; intuition.
Qed.

Lemma tc_andp_sound : forall {CS: compspecs} a1 a2 rho m,
    denote_tc_assert  (tc_andp a1 a2) rho m <->
    denote_tc_assert  (tc_andp' a1 a2) rho m.
Proof.
(* Goal: forall (CS : compspecs) (b : bool) (a : tc_error) (rho : environ) (m : rmap) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (tc_bool b a) rho) m), @eq bool b true *)
intros.
(* Goal: iff (@app_pred rmap ag_rmap (@denote_tc_assert CS (tc_andp a1 a2) rho) m) (@app_pred rmap ag_rmap (@denote_tc_assert CS (tc_andp' a1 a2) rho) m) *)
 unfold tc_andp.
 destruct a1; simpl; unfold_lift;
 repeat first [rewrite False_and | rewrite True_and
                    | rewrite and_False | rewrite and_True ];
  try apply iff_refl;
  destruct a2; simpl in *; unfold_lift;
 repeat first [rewrite False_and | rewrite True_and
                    | rewrite and_False | rewrite and_True ];
  try apply iff_refl.
Qed.

Lemma denote_tc_assert_andp:
  forall {CS: compspecs} a b rho, denote_tc_assert (tc_andp a b) rho =
             andp (denote_tc_assert a rho) (denote_tc_assert b rho).
Proof.
(* Goal: forall (CS : compspecs) (b : bool) (a : tc_error) (rho : environ) (m : rmap) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (tc_bool b a) rho) m), @eq bool b true *)
 intros.
(* Goal: @eq mpred (@denote_tc_assert CS (tc_andp a b) rho) (@andp rmap ag_rmap (@denote_tc_assert CS a rho) (@denote_tc_assert CS b rho)) *)
 apply pred_ext.
(* Goal: is_pointer_or_null (Vint i) *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 intro m. rewrite tc_andp_sound. intros [? ?]; split; auto.
(* Goal: is_pointer_or_null (Vint i) *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
 intros m [? ?]. rewrite tc_andp_sound; split; auto.
Qed.

Lemma neutral_isCastResultType:
  forall {CS: compspecs} t t' v rho,
   is_neutral_cast t' t = true ->
   forall m, denote_tc_assert (isCastResultType t' t v) rho m.
Proof.
(* Goal: forall (CS : compspecs) (b : bool) (a : tc_error) (rho : environ) (m : rmap) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (tc_bool b a) rho) m), @eq bool b true *)
intros.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (@isCastResultType CS t' t v) rho) m *)
  unfold isCastResultType.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS match classify_cast t' t with | cast_case_pointer => if eqb_type t' t then tc_TT else if orb (andb (is_pointer_type t) (is_pointer_type t')) (if Archi.ptr64 then andb (is_long_type t) (is_long_type t') else andb (is_int_type t) (is_int_type t')) then tc_TT else if andb (eqb_type t int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) t') then tc_TT else if andb (eqb_type t int_or_ptr_type) (is_pointer_type t') then tc_TT else if andb (eqb_type t' int_or_ptr_type) (is_pointer_type t) then tc_isptr v else if andb (eqb_type t' int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) t) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v | cast_case_i2i sz2 si2 => match t with | Tvoid => tc_FF (invalid_cast t' t) | Tint i s a => tc_bool (is_int_type t') (invalid_cast_result t t) | Tlong s a => tc_FF (invalid_cast t' t) | Tfloat (F32 as f) a => tc_bool (is_anyfloat_type t') (invalid_cast_result t t) | Tfloat (F64 as f) a => tc_bool (is_anyfloat_type t') (invalid_cast_result t t) | Tpointer t0 a => tc_FF (invalid_cast t' t) | Tarray t0 z a => tc_FF (invalid_cast t' t) | Tfunction t0 t1 c => tc_FF (invalid_cast t' t) | Tstruct i a => tc_FF (invalid_cast t' t) | Tunion i a => tc_FF (invalid_cast t' t) end | cast_case_f2f => match t with | Tvoid => tc_FF (invalid_cast t' t) | Tint i s a => tc_bool (is_int_type t') (invalid_cast_result t t) | Tlong s a => tc_FF (invalid_cast t' t) | Tfloat (F32 as f) a => tc_bool (is_anyfloat_type t') (invalid_cast_result t t) | Tfloat (F64 as f) a => tc_bool (is_anyfloat_type t') (invalid_cast_result t t) | Tpointer t0 a => tc_FF (invalid_cast t' t) | Tarray t0 z a => tc_FF (invalid_cast t' t) | Tfunction t0 t1 c => tc_FF (invalid_cast t' t) | Tstruct i a => tc_FF (invalid_cast t' t) | Tunion i a => tc_FF (invalid_cast t' t) end | cast_case_s2s => match t with | Tvoid => tc_FF (invalid_cast t' t) | Tint i s a => tc_bool (is_int_type t') (invalid_cast_result t t) | Tlong s a => tc_FF (invalid_cast t' t) | Tfloat (F32 as f) a => tc_bool (is_anyfloat_type t') (invalid_cast_result t t) | Tfloat (F64 as f) a => tc_bool (is_anyfloat_type t') (invalid_cast_result t t) | Tpointer t0 a => tc_FF (invalid_cast t' t) | Tarray t0 z a => tc_FF (invalid_cast t' t) | Tfunction t0 t1 c => tc_FF (invalid_cast t' t) | Tstruct i a => tc_FF (invalid_cast t' t) | Tunion i a => tc_FF (invalid_cast t' t) end | cast_case_f2s => match t with | Tvoid => tc_FF (invalid_cast t' t) | Tint i s a => tc_bool (is_int_type t') (invalid_cast_result t t) | Tlong s a => tc_FF (invalid_cast t' t) | Tfloat (F32 as f) a => tc_bool (is_anyfloat_type t') (invalid_cast_result t t) | Tfloat (F64 as f) a => tc_bool (is_anyfloat_type t') (invalid_cast_result t t) | Tpointer t0 a => tc_FF (invalid_cast t' t) | Tarray t0 z a => tc_FF (invalid_cast t' t) | Tfunction t0 t1 c => tc_FF (invalid_cast t' t) | Tstruct i a => tc_FF (invalid_cast t' t) | Tunion i a => tc_FF (invalid_cast t' t) end | cast_case_s2f => match t with | Tvoid => tc_FF (invalid_cast t' t) | Tint i s a => tc_bool (is_int_type t') (invalid_cast_result t t) | Tlong s a => tc_FF (invalid_cast t' t) | Tfloat (F32 as f) a => tc_bool (is_anyfloat_type t') (invalid_cast_result t t) | Tfloat (F64 as f) a => tc_bool (is_anyfloat_type t') (invalid_cast_result t t) | Tpointer t0 a => tc_FF (invalid_cast t' t) | Tarray t0 z a => tc_FF (invalid_cast t' t) | Tfunction t0 t1 c => tc_FF (invalid_cast t' t) | Tstruct i a => tc_FF (invalid_cast t' t) | Tunion i a => tc_FF (invalid_cast t' t) end | cast_case_i2f si1 => match t with | Tvoid => tc_FF (invalid_cast t' t) | Tint i s a => tc_bool (is_int_type t') (invalid_cast_result t t) | Tlong s a => tc_FF (invalid_cast t' t) | Tfloat (F32 as f) a => tc_bool (is_anyfloat_type t') (invalid_cast_result t t) | Tfloat (F64 as f) a => tc_bool (is_anyfloat_type t') (invalid_cast_result t t) | Tpointer t0 a => tc_FF (invalid_cast t' t) | Tarray t0 z a => tc_FF (invalid_cast t' t) | Tfunction t0 t1 c => tc_FF (invalid_cast t' t) | Tstruct i a => tc_FF (invalid_cast t' t) | Tunion i a => tc_FF (invalid_cast t' t) end | cast_case_i2s si1 => match t with | Tvoid => tc_FF (invalid_cast t' t) | Tint i s a => tc_bool (is_int_type t') (invalid_cast_result t t) | Tlong s a => tc_FF (invalid_cast t' t) | Tfloat (F32 as f) a => tc_bool (is_anyfloat_type t') (invalid_cast_result t t) | Tfloat (F64 as f) a => tc_bool (is_anyfloat_type t') (invalid_cast_result t t) | Tpointer t0 a => tc_FF (invalid_cast t' t) | Tarray t0 z a => tc_FF (invalid_cast t' t) | Tfunction t0 t1 c => tc_FF (invalid_cast t' t) | Tstruct i a => tc_FF (invalid_cast t' t) | Tunion i a => tc_FF (invalid_cast t' t) end | cast_case_f2i sz2 (Signed as si2) => tc_andp (tc_Zge v Int.min_signed) (tc_Zle v Int.max_signed) | cast_case_f2i sz2 (Unsigned as si2) => tc_andp (tc_Zge v Z0) (tc_Zle v Int.max_unsigned) | cast_case_s2i sz2 (Signed as si2) => tc_andp (tc_Zge v Int.min_signed) (tc_Zle v Int.max_signed) | cast_case_s2i sz2 (Unsigned as si2) => tc_andp (tc_Zge v Z0) (tc_Zle v Int.max_unsigned) | cast_case_l2l => tc_bool (andb (is_long_type t') (is_long_type t)) (invalid_cast_result t t) | cast_case_i2l si1 => tc_andp (tc_bool (is_int_type t') (invalid_cast_result t' t)) (if is_pointer_type t then @tc_iszero CS v else tc_TT) | cast_case_l2i sz2 si2 => tc_andp (tc_bool (is_long_type t') (invalid_cast_result t' t)) (if is_pointer_type t then @tc_iszero CS v else tc_TT) | cast_case_l2f si1 => match t with | Tvoid => tc_FF (invalid_cast t' t) | Tint i s a => tc_bool (is_int_type t') (invalid_cast_result t t) | Tlong s a => tc_FF (invalid_cast t' t) | Tfloat (F32 as f) a => tc_bool (is_anyfloat_type t') (invalid_cast_result t t) | Tfloat (F64 as f) a => tc_bool (is_anyfloat_type t') (invalid_cast_result t t) | Tpointer t0 a => tc_FF (invalid_cast t' t) | Tarray t0 z a => tc_FF (invalid_cast t' t) | Tfunction t0 t1 c => tc_FF (invalid_cast t' t) | Tstruct i a => tc_FF (invalid_cast t' t) | Tunion i a => tc_FF (invalid_cast t' t) end | cast_case_l2s si1 => match t with | Tvoid => tc_FF (invalid_cast t' t) | Tint i s a => tc_bool (is_int_type t') (invalid_cast_result t t) | Tlong s a => tc_FF (invalid_cast t' t) | Tfloat (F32 as f) a => tc_bool (is_anyfloat_type t') (invalid_cast_result t t) | Tfloat (F64 as f) a => tc_bool (is_anyfloat_type t') (invalid_cast_result t t) | Tpointer t0 a => tc_FF (invalid_cast t' t) | Tarray t0 z a => tc_FF (invalid_cast t' t) | Tfunction t0 t1 c => tc_FF (invalid_cast t' t) | Tstruct i a => tc_FF (invalid_cast t' t) | Tunion i a => tc_FF (invalid_cast t' t) end | cast_case_f2l si2 => match t with | Tvoid => tc_FF (invalid_cast t' t) | Tint i s a => tc_bool (is_int_type t') (invalid_cast_result t t) | Tlong s a => tc_FF (invalid_cast t' t) | Tfloat (F32 as f) a => tc_bool (is_anyfloat_type t') (invalid_cast_result t t) | Tfloat (F64 as f) a => tc_bool (is_anyfloat_type t') (invalid_cast_result t t) | Tpointer t0 a => tc_FF (invalid_cast t' t) | Tarray t0 z a => tc_FF (invalid_cast t' t) | Tfunction t0 t1 c => tc_FF (invalid_cast t' t) | Tstruct i a => tc_FF (invalid_cast t' t) | Tunion i a => tc_FF (invalid_cast t' t) end | cast_case_s2l si2 => match t with | Tvoid => tc_FF (invalid_cast t' t) | Tint i s a => tc_bool (is_int_type t') (invalid_cast_result t t) | Tlong s a => tc_FF (invalid_cast t' t) | Tfloat (F32 as f) a => tc_bool (is_anyfloat_type t') (invalid_cast_result t t) | Tfloat (F64 as f) a => tc_bool (is_anyfloat_type t') (invalid_cast_result t t) | Tpointer t0 a => tc_FF (invalid_cast t' t) | Tarray t0 z a => tc_FF (invalid_cast t' t) | Tfunction t0 t1 c => tc_FF (invalid_cast t' t) | Tstruct i a => tc_FF (invalid_cast t' t) | Tunion i a => tc_FF (invalid_cast t' t) end | cast_case_i2bool => if is_pointer_type t' then @tc_test_eq CS v (Econst_int Int.zero (Tint I32 Unsigned noattr)) else tc_TT | cast_case_l2bool => if is_pointer_type t' then @tc_test_eq CS v (Econst_long Int64.zero (Tlong Unsigned noattr)) else tc_TT | cast_case_f2bool => tc_bool (is_float_type t') (invalid_cast_result t' t) | cast_case_s2bool => tc_bool (is_single_type t') (invalid_cast_result t' t) | cast_case_struct id1 id2 => match t with | Tvoid => tc_FF (invalid_cast t' t) | Tint i s a => tc_bool (is_int_type t') (invalid_cast_result t t) | Tlong s a => tc_FF (invalid_cast t' t) | Tfloat (F32 as f) a => tc_bool (is_anyfloat_type t') (invalid_cast_result t t) | Tfloat (F64 as f) a => tc_bool (is_anyfloat_type t') (invalid_cast_result t t) | Tpointer t0 a => tc_FF (invalid_cast t' t) | Tarray t0 z a => tc_FF (invalid_cast t' t) | Tfunction t0 t1 c => tc_FF (invalid_cast t' t) | Tstruct i a => tc_FF (invalid_cast t' t) | Tunion i a => tc_FF (invalid_cast t' t) end | cast_case_union id1 id2 => match t with | Tvoid => tc_FF (invalid_cast t' t) | Tint i s a => tc_bool (is_int_type t') (invalid_cast_result t t) | Tlong s a => tc_FF (invalid_cast t' t) | Tfloat (F32 as f) a => tc_bool (is_anyfloat_type t') (invalid_cast_result t t) | Tfloat (F64 as f) a => tc_bool (is_anyfloat_type t') (invalid_cast_result t t) | Tpointer t0 a => tc_FF (invalid_cast t' t) | Tarray t0 z a => tc_FF (invalid_cast t' t) | Tfunction t0 t1 c => tc_FF (invalid_cast t' t) | Tstruct i a => tc_FF (invalid_cast t' t) | Tunion i a => tc_FF (invalid_cast t' t) end | cast_case_void => tc_noproof | cast_case_default => tc_FF (invalid_cast t' t) end rho) m *)
  unfold is_neutral_cast in H; simpl classify_cast.
  destruct t'  as [ | [ | | | ] [ | ] | | [ | ] | | | | |],
   t  as [ | [ | | | ] [ | ] | | [ | ] | | | | |];
   try solve [inv H; try apply I; simpl; simple_if_tac; apply I];
  try (rewrite denote_tc_assert_andp; split);
  try solve [unfold eval_cast, sem_cast, classify_cast,
     sem_cast_pointer, sem_cast_i2bool, sem_cast_l2bool;
      destruct Archi.ptr64; simpl; try simple_if_tac; try apply I].
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
  apply orb_true_iff in H.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
  unfold classify_cast.
  destruct (Bool.eqb (eqb_type (Tpointer t a0) int_or_ptr_type)
         (eqb_type (Tpointer t' a) int_or_ptr_type)) eqn:J.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
  destruct (eqb_type (Tpointer t' a) (Tpointer t a0)) eqn:?H.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if orb (andb (negb false) (negb false)) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb false ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb false (negb false) then tc_TT else if andb false (negb false) then tc_isptr v else if andb false ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
  apply I.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
  destruct H. inv H.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
  apply andb_true_iff in H. destruct H.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
  rewrite eqb_true_iff in J.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
  unfold is_pointer_type.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if orb (andb (negb (eqb_type (Tpointer t a0) int_or_ptr_type)) (negb (eqb_type (Tpointer t' a) int_or_ptr_type))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (negb (eqb_type (Tpointer t' a) int_or_ptr_type)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (negb (eqb_type (Tpointer t a0) int_or_ptr_type)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
  rewrite <- J in *. apply eqb_type_false in H0.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
  destruct (eqb_type (Tpointer t a0) int_or_ptr_type); inv H.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if orb (andb (negb false) (negb false)) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb false ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb false (negb false) then tc_TT else if andb false (negb false) then tc_isptr v else if andb false ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
  apply I.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
  destruct H.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
  apply eqb_type_true in H. rewrite <- H in *.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if eqb_type (Tpointer t' a) (Tpointer t' a) then tc_TT else if orb (andb (is_pointer_type (Tpointer t' a)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t' a)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t' a)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
  rewrite eqb_reflx in J. inv J.
  destruct (eqb_type (Tpointer t' a) int_or_ptr_type),
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if eqb_type (Tpointer t' a) (Tpointer t' a) then tc_TT else if orb (andb (is_pointer_type (Tpointer t' a)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t' a)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t' a)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (if Archi.ptr64 then andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a)) else andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (Tpointer t a0)) then (if Archi.ptr64 then tc_islong else tc_isint) v else @tc_iszero CS v) rho) m *)
     (eqb_type (Tpointer t a0) int_or_ptr_type); inv H; inv J.
Qed.

Lemma is_true_e: forall b, is_true b -> b=true.
(* Goal: forall (CS : compspecs) (b : bool) (a : tc_error) (rho : environ) (m : rmap) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (tc_bool b a) rho) m), @eq bool b true *)
Proof. intros. destruct b; try contradiction; auto.
Qed.

Lemma tc_bool_e: forall {CS: compspecs} b a rho m,
  app_pred (denote_tc_assert (tc_bool b a) rho) m ->
  b = true.
Proof.
(* Goal: forall (CS : compspecs) (b : bool) (a : tc_error) (rho : environ) (m : rmap) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (tc_bool b a) rho) m), @eq bool b true *)
intros.
(* Goal: is_pointer_or_null (Vint i) *)
(* Goal: (if eqb_type (Tpointer t2 a0) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (Vptr b i) *)
destruct b; simpl in H; auto.
Qed.
