Require Import VST.floyd.base.
Require Import VST.floyd.val_lemmas.
Require Import VST.floyd.typecheck_lemmas.

Definition const_only_isUnOpResultType {CS: compspecs} op typeof_a valueof_a ty : bool :=
match op with
  | Cop.Onotbool => match typeof_a with
                    | Tint _ _ _
                    | Tlong _ _
                    | Tfloat _ _ => is_int_type ty
                    | Tpointer _ _ =>
                        if Archi.ptr64 
                        then match valueof_a with
                             | Vlong v =>
                                andb (negb (eqb_type (typeof_a) int_or_ptr_type))
                                     (andb (is_int_type ty) (Z.eqb 0 (Int64.unsigned v)))
                             | _ => false
                             end
                        else match valueof_a with
                             | Vint v => 
                                andb (negb (eqb_type typeof_a int_or_ptr_type))
                                     (andb (is_int_type ty) (Z.eqb 0 (Int.unsigned v)))
                             | _ => false
                             end
                    | _ => false
                    end
  | Cop.Onotint => match Cop.classify_notint (typeof_a) with
                   | Cop.notint_default => false
                   | Cop.notint_case_i _ => (is_int32_type ty)
                   | Cop.notint_case_l _ => (is_long_type ty)
                   end
  | Cop.Oneg => match Cop.classify_neg (typeof_a) with
                    | Cop.neg_case_i sg => 
                          andb (is_int32_type ty)
                          match (typeof_a) with
                          | Tint _ Signed _ =>
                            match valueof_a with
                            | Vint v => negb (Z.eqb (Int.signed v) Int.min_signed)
                            | _ => false
                            end
                          | Tlong Signed _ =>
                            match valueof_a with
                            | Vlong v => negb (Z.eqb (Int64.signed v) Int64.min_signed)
                            | _ => false
                            end
                          | _ => true
                          end
                    | Cop.neg_case_f => is_float_type ty
                    | Cop.neg_case_s => is_single_type ty
                    | _ => false
                    end
  | Cop.Oabsfloat =>match Cop.classify_neg (typeof_a) with
                    | Cop.neg_case_i sg => is_float_type ty
                    | Cop.neg_case_l _ => is_float_type ty
                    | Cop.neg_case_f => is_float_type ty
                    | Cop.neg_case_s => is_float_type ty
                    | _ => false
                    end
end.

(* TODO: binarithType would better be bool type *)
Definition const_only_isBinOpResultType {CS: compspecs} op typeof_a1 valueof_a1 typeof_a2 valueof_a2 ty : bool :=
  match op with
  | Cop.Oadd =>
      match Cop.classify_add (typeof_a1) (typeof_a2) with
      | Cop.add_case_pi t _ | Cop.add_case_pl t =>
        andb
          (andb
             (andb (match valueof_a1 with Vptr _ _ => true | _ => false end) (complete_type cenv_cs t))
             (negb (eqb_type (typeof_a1) int_or_ptr_type)))
          (is_pointer_type ty)
    | Cop.add_case_ip _ t | Cop.add_case_lp t =>
        andb
          (andb
             (andb (match valueof_a2 with Vptr _ _ => true | _ => false end) (complete_type cenv_cs t))
             (negb (eqb_type (typeof_a2) int_or_ptr_type)))
          (is_pointer_type ty)
    | Cop.add_default => false
                           (*
        andb (binarithType (typeof a1) (typeof a2) ty deferr reterr)
          (tc_nobinover Z.add a1 a2) *)
      end
  | _ => false (* TODO *)
  end.

Definition const_only_isCastResultType {CS: compspecs} (t1 t2: type) (valueof_a: val)  : bool := false. (* TODO *)

Fixpoint const_only_eval_expr {cs: compspecs} (e: Clight.expr): option val :=
  match e with
  | Econst_int i (Tint I32 _ _) => Some (Vint i)
  | Econst_int _ _ => None
  | Econst_long i ty => None (*Some (Vlong i) *)
  | Econst_float f (Tfloat F64 _) => Some (Vfloat f)
  | Econst_float _ _ => None
  | Econst_single f (Tfloat F32 _) => Some (Vsingle f)
  | Econst_single _ _ => None
  | Etempvar id ty => None
  | Evar _ _ => None
  | Eaddrof a ty => None
  | Eunop op a ty =>
      match const_only_eval_expr a with
      | Some v => if const_only_isUnOpResultType op (typeof a) v ty
                  then Some (eval_unop op (typeof a) v)
                  else None
      | None => None
      end
  | Ebinop op a1 a2 ty =>
      match (const_only_eval_expr a1), (const_only_eval_expr a2) with
      | Some v1, Some v2 =>
          if const_only_isBinOpResultType op (typeof a1) v1 (typeof a2) v2 ty
          then Some (eval_binop op (typeof a1) (typeof a2) v1 v2)
          else None
      | _, _ => None
      end
  | Ecast a ty =>
      match const_only_eval_expr a with
      | Some v => if const_only_isCastResultType (typeof a) ty v
                  then Some (eval_cast (typeof a) ty v)
                  else None
      | None => None
      end
  | Ederef a ty => None
  | Efield a i ty => None
  | Esizeof t t0 =>
    if andb (complete_type cenv_cs t) (eqb_type t0 size_t)
    then Some (Vptrofs (Ptrofs.repr (sizeof t)))
    else None
  | Ealignof t t0 =>
    if andb (complete_type cenv_cs t) (eqb_type t0 size_t)
    then Some (Vptrofs (Ptrofs.repr (alignof t)))
    else None
  end.

Lemma const_only_isUnOpResultType_spec: forall {cs: compspecs} rho u e t P,
  const_only_isUnOpResultType u (typeof e) (eval_expr e rho) t = true ->
  P |-- denote_tc_assert (isUnOpResultType u e t) rho.
Proof.
(* Goal: forall (v : val) (_ : @eq (option val) (@const_only_eval_expr cs (Ealignof t t0)) (@Some val v)), @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
  intros.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (@isUnOpResultType cs u e t) rho) *)
  unfold isUnOpResultType.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs match u with | Cop.Onotbool => match typeof e with | Tvoid => tc_FF (op_result_type e) | Tint i s a => tc_bool (is_int_type t) (op_result_type e) | Tlong s a => tc_bool (is_int_type t) (op_result_type e) | Tfloat f a => tc_bool (is_int_type t) (op_result_type e) | Tpointer t0 a => tc_andp (tc_int_or_ptr_type (typeof e)) (tc_andp (tc_bool (is_int_type t) (op_result_type e)) (@tc_test_eq cs e (if Archi.ptr64 then Econst_long Int64.zero (Tlong Signed noattr) else Econst_int Int.zero (Tint I32 Signed noattr)))) | Tarray t z a => tc_FF (op_result_type e) | Tfunction t t0 c => tc_FF (op_result_type e) | Tstruct i a => tc_FF (op_result_type e) | Tunion i a => tc_FF (op_result_type e) end | Cop.Onotint => match Cop.classify_notint (typeof e) with | Cop.notint_case_i s => tc_bool (is_int32_type t) (op_result_type e) | Cop.notint_case_l s => tc_bool (is_long_type t) (op_result_type e) | Cop.notint_default => tc_FF (op_result_type e) end | Cop.Oneg => match Cop.classify_neg (typeof e) with | Cop.neg_case_i sg => tc_andp (tc_bool (is_int32_type t) (op_result_type e)) match typeof e with | Tvoid => tc_TT | Tint i (Signed as s) a => tc_nosignedover Z.sub (Econst_int Int.zero (typeof e)) e | Tint i (Unsigned as s) a => tc_TT | Tlong (Signed as s) a => tc_nosignedover Z.sub (Econst_long Int64.zero (typeof e)) e | Tlong (Unsigned as s) a => tc_TT | Tfloat f a => tc_TT | Tpointer t a => tc_TT | Tarray t z a => tc_TT | Tfunction t t0 c => tc_TT | Tstruct i a => tc_TT | Tunion i a => tc_TT end | Cop.neg_case_f => tc_bool (is_float_type t) (op_result_type e) | Cop.neg_case_s => tc_bool (is_single_type t) (op_result_type e) | Cop.neg_case_l s => tc_FF (op_result_type e) | Cop.neg_default => tc_FF (op_result_type e) end | Cop.Oabsfloat => match Cop.classify_neg (typeof e) with | Cop.neg_case_i sg => tc_bool (is_float_type t) (op_result_type e) | Cop.neg_case_f => tc_bool (is_float_type t) (op_result_type e) | Cop.neg_case_s => tc_bool (is_float_type t) (op_result_type e) | Cop.neg_case_l s => tc_bool (is_float_type t) (op_result_type e) | Cop.neg_default => tc_FF (op_result_type e) end end rho) *)
  unfold const_only_isUnOpResultType in H.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs match u with | Cop.Onotbool => match typeof e with | Tvoid => tc_FF (op_result_type e) | Tint i s a => tc_bool (is_int_type t) (op_result_type e) | Tlong s a => tc_bool (is_int_type t) (op_result_type e) | Tfloat f a => tc_bool (is_int_type t) (op_result_type e) | Tpointer t0 a => tc_andp (tc_int_or_ptr_type (typeof e)) (tc_andp (tc_bool (is_int_type t) (op_result_type e)) (@tc_test_eq cs e (if Archi.ptr64 then Econst_long Int64.zero (Tlong Signed noattr) else Econst_int Int.zero (Tint I32 Signed noattr)))) | Tarray t z a => tc_FF (op_result_type e) | Tfunction t t0 c => tc_FF (op_result_type e) | Tstruct i a => tc_FF (op_result_type e) | Tunion i a => tc_FF (op_result_type e) end | Cop.Onotint => match Cop.classify_notint (typeof e) with | Cop.notint_case_i s => tc_bool (is_int32_type t) (op_result_type e) | Cop.notint_case_l s => tc_bool (is_long_type t) (op_result_type e) | Cop.notint_default => tc_FF (op_result_type e) end | Cop.Oneg => match Cop.classify_neg (typeof e) with | Cop.neg_case_i sg => tc_andp (tc_bool (is_int32_type t) (op_result_type e)) match typeof e with | Tvoid => tc_TT | Tint i (Signed as s) a => tc_nosignedover Z.sub (Econst_int Int.zero (typeof e)) e | Tint i (Unsigned as s) a => tc_TT | Tlong (Signed as s) a => tc_nosignedover Z.sub (Econst_long Int64.zero (typeof e)) e | Tlong (Unsigned as s) a => tc_TT | Tfloat f a => tc_TT | Tpointer t a => tc_TT | Tarray t z a => tc_TT | Tfunction t t0 c => tc_TT | Tstruct i a => tc_TT | Tunion i a => tc_TT end | Cop.neg_case_f => tc_bool (is_float_type t) (op_result_type e) | Cop.neg_case_s => tc_bool (is_single_type t) (op_result_type e) | Cop.neg_case_l s => tc_FF (op_result_type e) | Cop.neg_default => tc_FF (op_result_type e) end | Cop.Oabsfloat => match Cop.classify_neg (typeof e) with | Cop.neg_case_i sg => tc_bool (is_float_type t) (op_result_type e) | Cop.neg_case_f => tc_bool (is_float_type t) (op_result_type e) | Cop.neg_case_s => tc_bool (is_float_type t) (op_result_type e) | Cop.neg_case_l s => tc_bool (is_float_type t) (op_result_type e) | Cop.neg_default => tc_FF (op_result_type e) end end rho) *)
  destruct u.
  + destruct (typeof e);
      try solve [inv H | rewrite H; exact (@prop_right mpred _ True _ I)].
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (tc_andp (tc_int_or_ptr_type (Tpointer t0 a)) (tc_andp (tc_bool (is_int_type t) (op_result_type e)) (@tc_test_eq cs e (if Archi.ptr64 then Econst_long Int64.zero (Tlong Signed noattr) else Econst_int Int.zero (Tint I32 Signed noattr))))) rho) *)
    rewrite !denote_tc_assert_andp.
    match goal with
    | |- context [denote_tc_assert (tc_test_eq ?a ?b)] =>
      change (denote_tc_assert (tc_test_eq a b)) with (expr2.denote_tc_assert (tc_test_eq a b))
    end.
(* Goal: @derives mpred Nveric P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@denote_tc_assert cs (tc_int_or_ptr_type (Tpointer t0 a))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@denote_tc_assert cs (tc_bool (is_int_type t) (op_result_type e))) (@expr2.denote_tc_assert cs (@tc_test_eq cs e (if Archi.ptr64 then Econst_long Int64.zero (Tlong Signed noattr) else Econst_int Int.zero (Tint I32 Signed noattr))))) rho) *)
    rewrite binop_lemmas2.denote_tc_assert_test_eq'.
(* Goal: @derives mpred Nveric P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@denote_tc_assert cs (tc_int_or_ptr_type (Tpointer t0 a))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@denote_tc_assert cs (tc_bool (is_int_type t) (op_result_type e))) (@expr2.denote_tc_assert cs (tc_test_eq' e (if Archi.ptr64 then Econst_long Int64.zero (Tlong Signed noattr) else Econst_int Int.zero (Tint I32 Signed noattr))))) rho) *)
    simpl expr2.denote_tc_assert.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_andp (@isBinOpResultType cs b e1 e2 t) (@typecheck_expr cs Delta e1)) (@typecheck_expr cs Delta e2)) rho) *)
    unfold_lift. simpl.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@denote_tc_assert cs (tc_int_or_ptr_type (Tpointer t0 a)) rho) (@andp mpred Nveric (@denote_tc_assert cs (tc_bool (is_int_type t) (op_result_type e)) rho) (expr2.denote_tc_test_eq (@eval_expr cs e rho) (@eval_expr cs (if Archi.ptr64 then Econst_long Int64.zero (Tlong Signed noattr) else Econst_int Int.zero (Tint I32 Signed noattr)) rho)))) *)
    unfold tc_int_or_ptr_type.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@denote_tc_assert cs (tc_bool (negb (eqb_type (Tpointer t0 a) int_or_ptr_type)) int_or_ptr_type_error) rho) (@andp mpred Nveric (@denote_tc_assert cs (tc_bool (is_int_type t) (op_result_type e)) rho) (expr2.denote_tc_test_eq (@eval_expr cs e rho) (@eval_expr cs (if Archi.ptr64 then Econst_long Int64.zero (Tlong Signed noattr) else Econst_int Int.zero (Tint I32 Signed noattr)) rho)))) *)
    destruct Archi.ptr64 eqn:HH.
    - destruct (eval_expr e rho); try solve [inv H].
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (tc_andp (tc_bool (is_int32_type t) (op_result_type e)) match typeof e with | Tvoid => tc_TT | Tint i (Signed as s) a => tc_nosignedover Z.sub (Econst_int Int.zero (typeof e)) e | Tint i (Unsigned as s) a => tc_TT | Tlong (Signed as s) a => tc_nosignedover Z.sub (Econst_long Int64.zero (typeof e)) e | Tlong (Unsigned as s) a => tc_TT | Tfloat f a => tc_TT | Tpointer t a => tc_TT | Tarray t z a => tc_TT | Tfunction t t0 c => tc_TT | Tstruct i a => tc_TT | Tunion i a => tc_TT end) rho) *)
      rewrite !andb_true_iff in H.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@denote_tc_assert cs (tc_bool (negb (eqb_type (Tpointer t0 a) int_or_ptr_type)) int_or_ptr_type_error) rho) (@andp mpred Nveric (@denote_tc_assert cs (tc_bool (is_int_type t) (op_result_type e)) rho) (expr2.denote_tc_test_eq (Vint i) (@eval_expr cs (Econst_int Int.zero (Tint I32 Signed noattr)) rho)))) *)
      destruct H as [? [? ?]].
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool (complete_type (@cenv_cs cs) t) (invalid_expression (Ealignof t t0))) (tc_bool (eqb_type t0 size_t) (invalid_expression (Ealignof t t0)))) rho) *)
      rewrite H, H0.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@denote_tc_assert cs (tc_bool true int_or_ptr_type_error) rho) (@andp mpred Nveric (@denote_tc_assert cs (tc_bool true (op_result_type e)) rho) (expr2.denote_tc_test_eq (Vint i) (@eval_expr cs (Econst_int Int.zero (Tint I32 Signed noattr)) rho)))) *)
      rewrite Z.eqb_eq in H1.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@denote_tc_assert cs (tc_bool true (op_result_type e)) rho) (expr2.denote_tc_test_eq (Vint i) (@eval_expr cs (Econst_int Int.zero (Tint I32 Signed noattr)) rho))) *)
      apply andp_right; [exact (@prop_right mpred _ True _ I) |].
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@denote_tc_assert cs (tc_bool true (op_result_type e)) rho) (expr2.denote_tc_test_eq (Vint i) (@eval_expr cs (Econst_int Int.zero (Tint I32 Signed noattr)) rho))) *)
      apply andp_right; [exact (@prop_right mpred _ True _ I) |].
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool (complete_type (@cenv_cs cs) t) (invalid_expression (Ealignof t t0))) (tc_bool (eqb_type t0 size_t) (invalid_expression (Ealignof t t0)))) rho) *)
      simpl.
(* Goal: @eq bool (@const_only_isUnOpResultType cs u (typeof e) (@eval_expr cs e rho) t) true *)
      rewrite HH.
      change (P |-- (!! (i = Int64.zero)) && (!! (Int64.zero = Int64.zero)))%logic.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@prop mpred Nveric (@eq Int.int i Int.zero)) (@prop mpred Nveric (@eq Int.int Int.zero Int.zero))) *)
      apply andp_right; apply prop_right; auto.
      rewrite <- (Int64.repr_unsigned i), <- H1.
(* Goal: @eq val (@liftx (LiftEnviron val) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) rho) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) *)
      auto.
    - destruct (eval_expr e rho); try solve [inv H].
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (tc_andp (tc_bool (is_int32_type t) (op_result_type e)) match typeof e with | Tvoid => tc_TT | Tint i (Signed as s) a => tc_nosignedover Z.sub (Econst_int Int.zero (typeof e)) e | Tint i (Unsigned as s) a => tc_TT | Tlong (Signed as s) a => tc_nosignedover Z.sub (Econst_long Int64.zero (typeof e)) e | Tlong (Unsigned as s) a => tc_TT | Tfloat f a => tc_TT | Tpointer t a => tc_TT | Tarray t z a => tc_TT | Tfunction t t0 c => tc_TT | Tstruct i a => tc_TT | Tunion i a => tc_TT end) rho) *)
      rewrite !andb_true_iff in H.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@denote_tc_assert cs (tc_bool (negb (eqb_type (Tpointer t0 a) int_or_ptr_type)) int_or_ptr_type_error) rho) (@andp mpred Nveric (@denote_tc_assert cs (tc_bool (is_int_type t) (op_result_type e)) rho) (expr2.denote_tc_test_eq (Vint i) (@eval_expr cs (Econst_int Int.zero (Tint I32 Signed noattr)) rho)))) *)
      destruct H as [? [? ?]].
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool (complete_type (@cenv_cs cs) t) (invalid_expression (Ealignof t t0))) (tc_bool (eqb_type t0 size_t) (invalid_expression (Ealignof t t0)))) rho) *)
      rewrite H, H0.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@denote_tc_assert cs (tc_bool true int_or_ptr_type_error) rho) (@andp mpred Nveric (@denote_tc_assert cs (tc_bool true (op_result_type e)) rho) (expr2.denote_tc_test_eq (Vint i) (@eval_expr cs (Econst_int Int.zero (Tint I32 Signed noattr)) rho)))) *)
      rewrite Z.eqb_eq in H1.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@denote_tc_assert cs (tc_bool true (op_result_type e)) rho) (expr2.denote_tc_test_eq (Vint i) (@eval_expr cs (Econst_int Int.zero (Tint I32 Signed noattr)) rho))) *)
      apply andp_right; [exact (@prop_right mpred _ True _ I) |].
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@denote_tc_assert cs (tc_bool true (op_result_type e)) rho) (expr2.denote_tc_test_eq (Vint i) (@eval_expr cs (Econst_int Int.zero (Tint I32 Signed noattr)) rho))) *)
      apply andp_right; [exact (@prop_right mpred _ True _ I) |].
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool (complete_type (@cenv_cs cs) t) (invalid_expression (Ealignof t t0))) (tc_bool (eqb_type t0 size_t) (invalid_expression (Ealignof t t0)))) rho) *)
      simpl.
(* Goal: @eq bool (@const_only_isUnOpResultType cs u (typeof e) (@eval_expr cs e rho) t) true *)
      rewrite HH.
      change (P |-- (!! (i = Int.zero)) && (!! (Int.zero = Int.zero)))%logic.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@prop mpred Nveric (@eq Int.int i Int.zero)) (@prop mpred Nveric (@eq Int.int Int.zero Int.zero))) *)
      apply andp_right; apply prop_right; auto.
      rewrite <- (Int.repr_unsigned i), <- H1.
(* Goal: @eq val (@liftx (LiftEnviron val) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) rho) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) *)
      auto.
  + destruct (Cop.classify_notint (typeof e));
      try solve [inv H | rewrite H; exact (@prop_right mpred _ True _ I)].
  + destruct (Cop.classify_neg (typeof e));
      try solve [inv H | rewrite H; exact (@prop_right mpred _ True _ I)].
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (tc_andp (tc_bool (is_int32_type t) (op_result_type e)) match typeof e with | Tvoid => tc_TT | Tint i (Signed as s) a => tc_nosignedover Z.sub (Econst_int Int.zero (typeof e)) e | Tint i (Unsigned as s) a => tc_TT | Tlong (Signed as s) a => tc_nosignedover Z.sub (Econst_long Int64.zero (typeof e)) e | Tlong (Unsigned as s) a => tc_TT | Tfloat f a => tc_TT | Tpointer t a => tc_TT | Tarray t z a => tc_TT | Tfunction t t0 c => tc_TT | Tstruct i a => tc_TT | Tunion i a => tc_TT end) rho) *)
    rewrite !andb_true_iff in H.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (tc_andp (tc_bool (is_int32_type t) (op_result_type e)) match typeof e with | Tvoid => tc_TT | Tint i (Signed as s) a => tc_nosignedover Z.sub (Econst_int Int.zero (typeof e)) e | Tint i (Unsigned as s) a => tc_TT | Tlong (Signed as s) a => tc_nosignedover Z.sub (Econst_long Int64.zero (typeof e)) e | Tlong (Unsigned as s) a => tc_TT | Tfloat f a => tc_TT | Tpointer t a => tc_TT | Tarray t z a => tc_TT | Tfunction t t0 c => tc_TT | Tstruct i a => tc_TT | Tunion i a => tc_TT end) rho) *)
    destruct H.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool (complete_type (@cenv_cs cs) t) (invalid_expression (Ealignof t t0))) (tc_bool (eqb_type t0 size_t) (invalid_expression (Ealignof t t0)))) rho) *)
    rewrite H; simpl.
    destruct (typeof e) as [| ? [|] | [|] | | | | | |];
      try solve [exact (@prop_right mpred _ True _ I)].
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool (complete_type (@cenv_cs cs) t) (invalid_expression (Ealignof t t0))) (tc_bool (eqb_type t0 size_t) (invalid_expression (Ealignof t t0)))) rho) *)
    - simpl.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_andp (@isBinOpResultType cs b e1 e2 t) (@typecheck_expr cs Delta e1)) (@typecheck_expr cs Delta e2)) rho) *)
      unfold_lift.
(* Goal: @derives mpred Nveric P (denote_tc_nosignedover Z.sub (Vlong Int64.zero) (@eval_expr cs e rho)) *)
      unfold denote_tc_nosignedover.
(* Goal: @derives mpred Nveric P match @eval_expr cs e rho with | Vundef => @FF mpred Nveric | Vint n2 => @prop mpred Nveric (and (Z.le Int64.min_signed (Z.sub (Int64.signed Int64.zero) (Int.signed n2))) (Z.le (Z.sub (Int64.signed Int64.zero) (Int.signed n2)) Int64.max_signed)) | Vlong n2 => @prop mpred Nveric (and (Z.le Int64.min_signed (Z.sub (Int64.signed Int64.zero) (Int64.signed n2))) (Z.le (Z.sub (Int64.signed Int64.zero) (Int64.signed n2)) Int64.max_signed)) | Vfloat f => @FF mpred Nveric | Vsingle f => @FF mpred Nveric | Vptr b i => @FF mpred Nveric end *)
      destruct (eval_expr e rho); try solve [inv H0].
(* Goal: @derives mpred Nveric P (@prop mpred Nveric (and (Z.le Int64.min_signed (Z.sub (Int64.signed Int64.zero) (Int64.signed i))) (Z.le (Z.sub (Int64.signed Int64.zero) (Int64.signed i)) Int64.max_signed))) *)
      rewrite negb_true_iff in H0.
(* Goal: @derives mpred Nveric P (@prop mpred Nveric (and (Z.le Int64.min_signed (Z.sub (Int64.signed Int64.zero) (Int64.signed i))) (Z.le (Z.sub (Int64.signed Int64.zero) (Int64.signed i)) Int64.max_signed))) *)
      rewrite Z.eqb_neq in H0.
(* Goal: @derives mpred Nveric P (@prop mpred Nveric (and (Z.le Int64.min_signed (Z.sub (Int64.signed Int64.zero) (Int64.signed i))) (Z.le (Z.sub (Int64.signed Int64.zero) (Int64.signed i)) Int64.max_signed))) *)
      apply prop_right.
(* Goal: and (Z.le Int.min_signed (Z.sub (Int.signed Int.zero) (Int.signed i0))) (Z.le (Z.sub (Int.signed Int.zero) (Int.signed i0)) Int.max_signed) *)
      change (Int.signed Int.zero) with 0.
(* Goal: and (Z.le Int64.min_signed (Z.sub Z0 (Int64.signed i))) (Z.le (Z.sub Z0 (Int64.signed i)) Int64.max_signed) *)
      rep_omega.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool (complete_type (@cenv_cs cs) t) (invalid_expression (Ealignof t t0))) (tc_bool (eqb_type t0 size_t) (invalid_expression (Ealignof t t0)))) rho) *)
    - simpl.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_andp (@isBinOpResultType cs b e1 e2 t) (@typecheck_expr cs Delta e1)) (@typecheck_expr cs Delta e2)) rho) *)
      unfold_lift.
(* Goal: @derives mpred Nveric P (denote_tc_nosignedover Z.sub (Vlong Int64.zero) (@eval_expr cs e rho)) *)
      unfold denote_tc_nosignedover.
(* Goal: @derives mpred Nveric P match @eval_expr cs e rho with | Vundef => @FF mpred Nveric | Vint n2 => @prop mpred Nveric (and (Z.le Int64.min_signed (Z.sub (Int64.signed Int64.zero) (Int.signed n2))) (Z.le (Z.sub (Int64.signed Int64.zero) (Int.signed n2)) Int64.max_signed)) | Vlong n2 => @prop mpred Nveric (and (Z.le Int64.min_signed (Z.sub (Int64.signed Int64.zero) (Int64.signed n2))) (Z.le (Z.sub (Int64.signed Int64.zero) (Int64.signed n2)) Int64.max_signed)) | Vfloat f => @FF mpred Nveric | Vsingle f => @FF mpred Nveric | Vptr b i => @FF mpred Nveric end *)
      destruct (eval_expr e rho); try solve [inv H0].
(* Goal: @derives mpred Nveric P (@prop mpred Nveric (and (Z.le Int64.min_signed (Z.sub (Int64.signed Int64.zero) (Int64.signed i))) (Z.le (Z.sub (Int64.signed Int64.zero) (Int64.signed i)) Int64.max_signed))) *)
      rewrite negb_true_iff in H0.
(* Goal: @derives mpred Nveric P (@prop mpred Nveric (and (Z.le Int64.min_signed (Z.sub (Int64.signed Int64.zero) (Int64.signed i))) (Z.le (Z.sub (Int64.signed Int64.zero) (Int64.signed i)) Int64.max_signed))) *)
      rewrite Z.eqb_neq in H0.
(* Goal: @derives mpred Nveric P (@prop mpred Nveric (and (Z.le Int64.min_signed (Z.sub (Int64.signed Int64.zero) (Int64.signed i))) (Z.le (Z.sub (Int64.signed Int64.zero) (Int64.signed i)) Int64.max_signed))) *)
      apply prop_right.
(* Goal: and (Z.le Int64.min_signed (Z.sub (Int64.signed Int64.zero) (Int64.signed i))) (Z.le (Z.sub (Int64.signed Int64.zero) (Int64.signed i)) Int64.max_signed) *)
      change (Int64.signed Int64.zero) with 0.
(* Goal: and (Z.le Int64.min_signed (Z.sub Z0 (Int64.signed i))) (Z.le (Z.sub Z0 (Int64.signed i)) Int64.max_signed) *)
      rep_omega.
  + destruct (Cop.classify_neg (typeof e)); try solve [inv H | rewrite H; exact (@prop_right mpred _ True _ I)].
Qed.

Lemma const_only_isBinOpResultType_spec: forall {cs: compspecs} rho b e1 e2 t P,
  const_only_isBinOpResultType b (typeof e1) (eval_expr e1 rho) (typeof e2) (eval_expr e2 rho) t = true ->
  P |-- denote_tc_assert (isBinOpResultType b e1 e2 t) rho.
Proof.
(* Goal: forall (v : val) (_ : @eq (option val) (@const_only_eval_expr cs (Ealignof t t0)) (@Some val v)), @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
  intros.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (@isBinOpResultType cs b e1 e2 t) rho) *)
  unfold isBinOpResultType.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs match b with | Cop.Oadd => match Cop.classify_add (typeof e1) (typeof e2) with | Cop.add_case_pi t0 si => tc_andp (tc_andp (tc_andp (tc_isptr e1) (tc_bool (complete_type (@cenv_cs cs) t0) (op_result_type (Ebinop b e1 e2 t)))) (tc_int_or_ptr_type (typeof e1))) (tc_bool (is_pointer_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.add_case_pl t0 => tc_andp (tc_andp (tc_andp (tc_isptr e1) (tc_bool (complete_type (@cenv_cs cs) t0) (op_result_type (Ebinop b e1 e2 t)))) (tc_int_or_ptr_type (typeof e1))) (tc_bool (is_pointer_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.add_case_ip si t0 => tc_andp (tc_andp (tc_andp (tc_isptr e2) (tc_bool (complete_type (@cenv_cs cs) t0) (op_result_type (Ebinop b e1 e2 t)))) (tc_int_or_ptr_type (typeof e2))) (tc_bool (is_pointer_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.add_case_lp t0 => tc_andp (tc_andp (tc_andp (tc_isptr e2) (tc_bool (complete_type (@cenv_cs cs) t0) (op_result_type (Ebinop b e1 e2 t)))) (tc_int_or_ptr_type (typeof e2))) (tc_bool (is_pointer_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.add_default => tc_andp (binarithType (typeof e1) (typeof e2) t (arg_type (Ebinop b e1 e2 t)) (op_result_type (Ebinop b e1 e2 t))) (@tc_nobinover Z.add cs e1 e2) end | Cop.Osub => match Cop.classify_sub (typeof e1) (typeof e2) with | Cop.sub_case_pi t0 si => tc_andp (tc_andp (tc_andp (tc_isptr e1) (tc_bool (complete_type (@cenv_cs cs) t0) (op_result_type (Ebinop b e1 e2 t)))) (tc_int_or_ptr_type (typeof e1))) (tc_bool (is_pointer_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.sub_case_pp t0 => tc_andp (tc_andp (tc_andp (tc_andp (tc_andp (tc_andp (tc_andp (tc_andp (tc_samebase e1 e2) (tc_isptr e1)) (tc_isptr e2)) (tc_int_or_ptr_type (typeof e1))) (tc_int_or_ptr_type (typeof e2))) (tc_bool (is_ptrofs_type t) (op_result_type (Ebinop b e1 e2 t)))) (tc_bool (negb (Z.eqb (@sizeof (@cenv_cs cs) t0) Z0)) (pp_compare_size_0 t0))) (tc_bool (complete_type (@cenv_cs cs) t0) (op_result_type (Ebinop b e1 e2 t)))) (tc_bool (Z.leb (@sizeof (@cenv_cs cs) t0) Ptrofs.max_signed) (pp_compare_size_exceed t0)) | Cop.sub_case_pl t0 => tc_andp (tc_andp (tc_andp (tc_isptr e1) (tc_bool (complete_type (@cenv_cs cs) t0) (op_result_type (Ebinop b e1 e2 t)))) (tc_int_or_ptr_type (typeof e1))) (tc_bool (is_pointer_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.sub_default => tc_andp (binarithType (typeof e1) (typeof e2) t (arg_type (Ebinop b e1 e2 t)) (op_result_type (Ebinop b e1 e2 t))) (@tc_nobinover Z.sub cs e1 e2) end | Cop.Omul => tc_andp (binarithType (typeof e1) (typeof e2) t (arg_type (Ebinop b e1 e2 t)) (op_result_type (Ebinop b e1 e2 t))) (@tc_nobinover Z.mul cs e1 e2) | Cop.Odiv => match Cop.classify_binarith (typeof e1) (typeof e2) with | Cop.bin_case_i (Signed as s) => tc_andp (tc_andp (@tc_nonzero cs e2) (@tc_nodivover cs e1 e2)) (tc_bool (is_int32_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.bin_case_i (Unsigned as s) => tc_andp (@tc_nonzero cs e2) (tc_bool (is_int32_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.bin_case_l (Signed as s) => tc_andp (tc_andp (@tc_nonzero cs e2) (@tc_nodivover cs e1 e2)) (tc_bool (is_long_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.bin_case_l (Unsigned as s) => tc_andp (@tc_nonzero cs e2) (tc_bool (is_long_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.bin_case_f => tc_bool (is_float_type t) (op_result_type (Ebinop b e1 e2 t)) | Cop.bin_case_s => tc_bool (is_single_type t) (op_result_type (Ebinop b e1 e2 t)) | Cop.bin_default => tc_FF (arg_type (Ebinop b e1 e2 t)) end | Cop.Omod => match Cop.classify_binarith (typeof e1) (typeof e2) with | Cop.bin_case_i (Signed as s) => tc_andp (tc_andp (@tc_nonzero cs e2) (@tc_nodivover cs e1 e2)) (tc_bool (is_int32_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.bin_case_i (Unsigned as s) => tc_andp (@tc_nonzero cs e2) (tc_bool (is_int32_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.bin_case_l (Signed as s) => tc_andp (tc_andp (@tc_nonzero cs e2) (@tc_nodivover cs e1 e2)) (tc_bool (is_long_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.bin_case_l (Unsigned as s) => tc_andp (@tc_nonzero cs e2) (tc_bool (is_long_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.bin_case_f => tc_FF (arg_type (Ebinop b e1 e2 t)) | Cop.bin_case_s => tc_FF (arg_type (Ebinop b e1 e2 t)) | Cop.bin_default => tc_FF (arg_type (Ebinop b e1 e2 t)) end | Cop.Oand => match Cop.classify_binarith (typeof e1) (typeof e2) with | Cop.bin_case_i s => tc_bool (is_int32_type t) (op_result_type (Ebinop b e1 e2 t)) | Cop.bin_case_l s => tc_bool (is_long_type t) (op_result_type (Ebinop b e1 e2 t)) | Cop.bin_case_f => tc_FF (arg_type (Ebinop b e1 e2 t)) | Cop.bin_case_s => tc_FF (arg_type (Ebinop b e1 e2 t)) | Cop.bin_default => tc_FF (arg_type (Ebinop b e1 e2 t)) end | Cop.Oor => match Cop.classify_binarith (typeof e1) (typeof e2) with | Cop.bin_case_i s => tc_bool (is_int32_type t) (op_result_type (Ebinop b e1 e2 t)) | Cop.bin_case_l s => tc_bool (is_long_type t) (op_result_type (Ebinop b e1 e2 t)) | Cop.bin_case_f => tc_FF (arg_type (Ebinop b e1 e2 t)) | Cop.bin_case_s => tc_FF (arg_type (Ebinop b e1 e2 t)) | Cop.bin_default => tc_FF (arg_type (Ebinop b e1 e2 t)) end | Cop.Oxor => match Cop.classify_binarith (typeof e1) (typeof e2) with | Cop.bin_case_i s => tc_bool (is_int32_type t) (op_result_type (Ebinop b e1 e2 t)) | Cop.bin_case_l s => tc_bool (is_long_type t) (op_result_type (Ebinop b e1 e2 t)) | Cop.bin_case_f => tc_FF (arg_type (Ebinop b e1 e2 t)) | Cop.bin_case_s => tc_FF (arg_type (Ebinop b e1 e2 t)) | Cop.bin_default => tc_FF (arg_type (Ebinop b e1 e2 t)) end | Cop.Oshl => match Cop.classify_shift (typeof e1) (typeof e2) with | Cop.shift_case_ii s => tc_andp (@tc_ilt cs e2 Int.iwordsize) (tc_bool (is_int32_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.shift_case_ll s => tc_andp (@tc_llt cs e2 Int64.iwordsize) (tc_bool (is_long_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.shift_case_il s => tc_andp (@tc_llt cs e2 (Int64.repr (Zpos (xO (xO (xO (xO (xO xH)))))))) (tc_bool (is_int32_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.shift_case_li s => tc_andp (@tc_ilt cs e2 Int64.iwordsize') (tc_bool (is_long_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.shift_default => tc_FF (arg_type (Ebinop b e1 e2 t)) end | Cop.Oshr => match Cop.classify_shift (typeof e1) (typeof e2) with | Cop.shift_case_ii s => tc_andp (@tc_ilt cs e2 Int.iwordsize) (tc_bool (is_int32_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.shift_case_ll s => tc_andp (@tc_llt cs e2 Int64.iwordsize) (tc_bool (is_long_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.shift_case_il s => tc_andp (@tc_llt cs e2 (Int64.repr (Zpos (xO (xO (xO (xO (xO xH)))))))) (tc_bool (is_int32_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.shift_case_li s => tc_andp (@tc_ilt cs e2 Int64.iwordsize') (tc_bool (is_long_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.shift_default => tc_FF (arg_type (Ebinop b e1 e2 t)) end | Cop.Oeq => match Cop.classify_cmp (typeof e1) (typeof e2) with | Cop.cmp_case_pp => tc_andp (tc_andp (tc_int_or_ptr_type (typeof e1)) (tc_int_or_ptr_type (typeof e2))) (@check_pp_int cs e1 e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_case_pi si => tc_andp (tc_int_or_ptr_type (typeof e1)) (@check_pp_int cs e1 (Ecast e2 size_t) b t (Ebinop b e1 e2 t)) | Cop.cmp_case_ip si => tc_andp (tc_int_or_ptr_type (typeof e2)) (@check_pp_int cs (Ecast e1 size_t) e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_case_pl => tc_andp (tc_int_or_ptr_type (typeof e1)) (@check_pp_int cs e1 (Ecast e2 size_t) b t (Ebinop b e1 e2 t)) | Cop.cmp_case_lp => tc_andp (tc_int_or_ptr_type (typeof e2)) (@check_pp_int cs (Ecast e1 size_t) e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_default => tc_bool (andb (andb (is_numeric_type (typeof e1)) (is_numeric_type (typeof e2))) (is_int_type t)) (arg_type (Ebinop b e1 e2 t)) end | Cop.One => match Cop.classify_cmp (typeof e1) (typeof e2) with | Cop.cmp_case_pp => tc_andp (tc_andp (tc_int_or_ptr_type (typeof e1)) (tc_int_or_ptr_type (typeof e2))) (@check_pp_int cs e1 e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_case_pi si => tc_andp (tc_int_or_ptr_type (typeof e1)) (@check_pp_int cs e1 (Ecast e2 size_t) b t (Ebinop b e1 e2 t)) | Cop.cmp_case_ip si => tc_andp (tc_int_or_ptr_type (typeof e2)) (@check_pp_int cs (Ecast e1 size_t) e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_case_pl => tc_andp (tc_int_or_ptr_type (typeof e1)) (@check_pp_int cs e1 (Ecast e2 size_t) b t (Ebinop b e1 e2 t)) | Cop.cmp_case_lp => tc_andp (tc_int_or_ptr_type (typeof e2)) (@check_pp_int cs (Ecast e1 size_t) e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_default => tc_bool (andb (andb (is_numeric_type (typeof e1)) (is_numeric_type (typeof e2))) (is_int_type t)) (arg_type (Ebinop b e1 e2 t)) end | Cop.Olt => match Cop.classify_cmp (typeof e1) (typeof e2) with | Cop.cmp_case_pp => tc_andp (tc_andp (tc_int_or_ptr_type (typeof e1)) (tc_int_or_ptr_type (typeof e2))) (@check_pp_int cs e1 e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_case_pi si => tc_andp (tc_int_or_ptr_type (typeof e1)) (@check_pp_int cs e1 (Ecast e2 size_t) b t (Ebinop b e1 e2 t)) | Cop.cmp_case_ip si => tc_andp (tc_int_or_ptr_type (typeof e2)) (@check_pp_int cs (Ecast e1 size_t) e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_case_pl => tc_andp (tc_int_or_ptr_type (typeof e1)) (@check_pp_int cs e1 (Ecast e2 size_t) b t (Ebinop b e1 e2 t)) | Cop.cmp_case_lp => tc_andp (tc_int_or_ptr_type (typeof e2)) (@check_pp_int cs (Ecast e1 size_t) e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_default => tc_bool (andb (andb (is_numeric_type (typeof e1)) (is_numeric_type (typeof e2))) (is_int_type t)) (arg_type (Ebinop b e1 e2 t)) end | Cop.Ogt => match Cop.classify_cmp (typeof e1) (typeof e2) with | Cop.cmp_case_pp => tc_andp (tc_andp (tc_int_or_ptr_type (typeof e1)) (tc_int_or_ptr_type (typeof e2))) (@check_pp_int cs e1 e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_case_pi si => tc_andp (tc_int_or_ptr_type (typeof e1)) (@check_pp_int cs e1 (Ecast e2 size_t) b t (Ebinop b e1 e2 t)) | Cop.cmp_case_ip si => tc_andp (tc_int_or_ptr_type (typeof e2)) (@check_pp_int cs (Ecast e1 size_t) e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_case_pl => tc_andp (tc_int_or_ptr_type (typeof e1)) (@check_pp_int cs e1 (Ecast e2 size_t) b t (Ebinop b e1 e2 t)) | Cop.cmp_case_lp => tc_andp (tc_int_or_ptr_type (typeof e2)) (@check_pp_int cs (Ecast e1 size_t) e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_default => tc_bool (andb (andb (is_numeric_type (typeof e1)) (is_numeric_type (typeof e2))) (is_int_type t)) (arg_type (Ebinop b e1 e2 t)) end | Cop.Ole => match Cop.classify_cmp (typeof e1) (typeof e2) with | Cop.cmp_case_pp => tc_andp (tc_andp (tc_int_or_ptr_type (typeof e1)) (tc_int_or_ptr_type (typeof e2))) (@check_pp_int cs e1 e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_case_pi si => tc_andp (tc_int_or_ptr_type (typeof e1)) (@check_pp_int cs e1 (Ecast e2 size_t) b t (Ebinop b e1 e2 t)) | Cop.cmp_case_ip si => tc_andp (tc_int_or_ptr_type (typeof e2)) (@check_pp_int cs (Ecast e1 size_t) e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_case_pl => tc_andp (tc_int_or_ptr_type (typeof e1)) (@check_pp_int cs e1 (Ecast e2 size_t) b t (Ebinop b e1 e2 t)) | Cop.cmp_case_lp => tc_andp (tc_int_or_ptr_type (typeof e2)) (@check_pp_int cs (Ecast e1 size_t) e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_default => tc_bool (andb (andb (is_numeric_type (typeof e1)) (is_numeric_type (typeof e2))) (is_int_type t)) (arg_type (Ebinop b e1 e2 t)) end | Cop.Oge => match Cop.classify_cmp (typeof e1) (typeof e2) with | Cop.cmp_case_pp => tc_andp (tc_andp (tc_int_or_ptr_type (typeof e1)) (tc_int_or_ptr_type (typeof e2))) (@check_pp_int cs e1 e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_case_pi si => tc_andp (tc_int_or_ptr_type (typeof e1)) (@check_pp_int cs e1 (Ecast e2 size_t) b t (Ebinop b e1 e2 t)) | Cop.cmp_case_ip si => tc_andp (tc_int_or_ptr_type (typeof e2)) (@check_pp_int cs (Ecast e1 size_t) e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_case_pl => tc_andp (tc_int_or_ptr_type (typeof e1)) (@check_pp_int cs e1 (Ecast e2 size_t) b t (Ebinop b e1 e2 t)) | Cop.cmp_case_lp => tc_andp (tc_int_or_ptr_type (typeof e2)) (@check_pp_int cs (Ecast e1 size_t) e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_default => tc_bool (andb (andb (is_numeric_type (typeof e1)) (is_numeric_type (typeof e2))) (is_int_type t)) (arg_type (Ebinop b e1 e2 t)) end end rho) *)
  unfold const_only_isBinOpResultType in H.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs match b with | Cop.Oadd => match Cop.classify_add (typeof e1) (typeof e2) with | Cop.add_case_pi t0 si => tc_andp (tc_andp (tc_andp (tc_isptr e1) (tc_bool (complete_type (@cenv_cs cs) t0) (op_result_type (Ebinop b e1 e2 t)))) (tc_int_or_ptr_type (typeof e1))) (tc_bool (is_pointer_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.add_case_pl t0 => tc_andp (tc_andp (tc_andp (tc_isptr e1) (tc_bool (complete_type (@cenv_cs cs) t0) (op_result_type (Ebinop b e1 e2 t)))) (tc_int_or_ptr_type (typeof e1))) (tc_bool (is_pointer_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.add_case_ip si t0 => tc_andp (tc_andp (tc_andp (tc_isptr e2) (tc_bool (complete_type (@cenv_cs cs) t0) (op_result_type (Ebinop b e1 e2 t)))) (tc_int_or_ptr_type (typeof e2))) (tc_bool (is_pointer_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.add_case_lp t0 => tc_andp (tc_andp (tc_andp (tc_isptr e2) (tc_bool (complete_type (@cenv_cs cs) t0) (op_result_type (Ebinop b e1 e2 t)))) (tc_int_or_ptr_type (typeof e2))) (tc_bool (is_pointer_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.add_default => tc_andp (binarithType (typeof e1) (typeof e2) t (arg_type (Ebinop b e1 e2 t)) (op_result_type (Ebinop b e1 e2 t))) (@tc_nobinover Z.add cs e1 e2) end | Cop.Osub => match Cop.classify_sub (typeof e1) (typeof e2) with | Cop.sub_case_pi t0 si => tc_andp (tc_andp (tc_andp (tc_isptr e1) (tc_bool (complete_type (@cenv_cs cs) t0) (op_result_type (Ebinop b e1 e2 t)))) (tc_int_or_ptr_type (typeof e1))) (tc_bool (is_pointer_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.sub_case_pp t0 => tc_andp (tc_andp (tc_andp (tc_andp (tc_andp (tc_andp (tc_andp (tc_andp (tc_samebase e1 e2) (tc_isptr e1)) (tc_isptr e2)) (tc_int_or_ptr_type (typeof e1))) (tc_int_or_ptr_type (typeof e2))) (tc_bool (is_ptrofs_type t) (op_result_type (Ebinop b e1 e2 t)))) (tc_bool (negb (Z.eqb (@sizeof (@cenv_cs cs) t0) Z0)) (pp_compare_size_0 t0))) (tc_bool (complete_type (@cenv_cs cs) t0) (op_result_type (Ebinop b e1 e2 t)))) (tc_bool (Z.leb (@sizeof (@cenv_cs cs) t0) Ptrofs.max_signed) (pp_compare_size_exceed t0)) | Cop.sub_case_pl t0 => tc_andp (tc_andp (tc_andp (tc_isptr e1) (tc_bool (complete_type (@cenv_cs cs) t0) (op_result_type (Ebinop b e1 e2 t)))) (tc_int_or_ptr_type (typeof e1))) (tc_bool (is_pointer_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.sub_default => tc_andp (binarithType (typeof e1) (typeof e2) t (arg_type (Ebinop b e1 e2 t)) (op_result_type (Ebinop b e1 e2 t))) (@tc_nobinover Z.sub cs e1 e2) end | Cop.Omul => tc_andp (binarithType (typeof e1) (typeof e2) t (arg_type (Ebinop b e1 e2 t)) (op_result_type (Ebinop b e1 e2 t))) (@tc_nobinover Z.mul cs e1 e2) | Cop.Odiv => match Cop.classify_binarith (typeof e1) (typeof e2) with | Cop.bin_case_i (Signed as s) => tc_andp (tc_andp (@tc_nonzero cs e2) (@tc_nodivover cs e1 e2)) (tc_bool (is_int32_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.bin_case_i (Unsigned as s) => tc_andp (@tc_nonzero cs e2) (tc_bool (is_int32_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.bin_case_l (Signed as s) => tc_andp (tc_andp (@tc_nonzero cs e2) (@tc_nodivover cs e1 e2)) (tc_bool (is_long_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.bin_case_l (Unsigned as s) => tc_andp (@tc_nonzero cs e2) (tc_bool (is_long_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.bin_case_f => tc_bool (is_float_type t) (op_result_type (Ebinop b e1 e2 t)) | Cop.bin_case_s => tc_bool (is_single_type t) (op_result_type (Ebinop b e1 e2 t)) | Cop.bin_default => tc_FF (arg_type (Ebinop b e1 e2 t)) end | Cop.Omod => match Cop.classify_binarith (typeof e1) (typeof e2) with | Cop.bin_case_i (Signed as s) => tc_andp (tc_andp (@tc_nonzero cs e2) (@tc_nodivover cs e1 e2)) (tc_bool (is_int32_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.bin_case_i (Unsigned as s) => tc_andp (@tc_nonzero cs e2) (tc_bool (is_int32_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.bin_case_l (Signed as s) => tc_andp (tc_andp (@tc_nonzero cs e2) (@tc_nodivover cs e1 e2)) (tc_bool (is_long_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.bin_case_l (Unsigned as s) => tc_andp (@tc_nonzero cs e2) (tc_bool (is_long_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.bin_case_f => tc_FF (arg_type (Ebinop b e1 e2 t)) | Cop.bin_case_s => tc_FF (arg_type (Ebinop b e1 e2 t)) | Cop.bin_default => tc_FF (arg_type (Ebinop b e1 e2 t)) end | Cop.Oand => match Cop.classify_binarith (typeof e1) (typeof e2) with | Cop.bin_case_i s => tc_bool (is_int32_type t) (op_result_type (Ebinop b e1 e2 t)) | Cop.bin_case_l s => tc_bool (is_long_type t) (op_result_type (Ebinop b e1 e2 t)) | Cop.bin_case_f => tc_FF (arg_type (Ebinop b e1 e2 t)) | Cop.bin_case_s => tc_FF (arg_type (Ebinop b e1 e2 t)) | Cop.bin_default => tc_FF (arg_type (Ebinop b e1 e2 t)) end | Cop.Oor => match Cop.classify_binarith (typeof e1) (typeof e2) with | Cop.bin_case_i s => tc_bool (is_int32_type t) (op_result_type (Ebinop b e1 e2 t)) | Cop.bin_case_l s => tc_bool (is_long_type t) (op_result_type (Ebinop b e1 e2 t)) | Cop.bin_case_f => tc_FF (arg_type (Ebinop b e1 e2 t)) | Cop.bin_case_s => tc_FF (arg_type (Ebinop b e1 e2 t)) | Cop.bin_default => tc_FF (arg_type (Ebinop b e1 e2 t)) end | Cop.Oxor => match Cop.classify_binarith (typeof e1) (typeof e2) with | Cop.bin_case_i s => tc_bool (is_int32_type t) (op_result_type (Ebinop b e1 e2 t)) | Cop.bin_case_l s => tc_bool (is_long_type t) (op_result_type (Ebinop b e1 e2 t)) | Cop.bin_case_f => tc_FF (arg_type (Ebinop b e1 e2 t)) | Cop.bin_case_s => tc_FF (arg_type (Ebinop b e1 e2 t)) | Cop.bin_default => tc_FF (arg_type (Ebinop b e1 e2 t)) end | Cop.Oshl => match Cop.classify_shift (typeof e1) (typeof e2) with | Cop.shift_case_ii s => tc_andp (@tc_ilt cs e2 Int.iwordsize) (tc_bool (is_int32_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.shift_case_ll s => tc_andp (@tc_llt cs e2 Int64.iwordsize) (tc_bool (is_long_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.shift_case_il s => tc_andp (@tc_llt cs e2 (Int64.repr (Zpos (xO (xO (xO (xO (xO xH)))))))) (tc_bool (is_int32_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.shift_case_li s => tc_andp (@tc_ilt cs e2 Int64.iwordsize') (tc_bool (is_long_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.shift_default => tc_FF (arg_type (Ebinop b e1 e2 t)) end | Cop.Oshr => match Cop.classify_shift (typeof e1) (typeof e2) with | Cop.shift_case_ii s => tc_andp (@tc_ilt cs e2 Int.iwordsize) (tc_bool (is_int32_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.shift_case_ll s => tc_andp (@tc_llt cs e2 Int64.iwordsize) (tc_bool (is_long_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.shift_case_il s => tc_andp (@tc_llt cs e2 (Int64.repr (Zpos (xO (xO (xO (xO (xO xH)))))))) (tc_bool (is_int32_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.shift_case_li s => tc_andp (@tc_ilt cs e2 Int64.iwordsize') (tc_bool (is_long_type t) (op_result_type (Ebinop b e1 e2 t))) | Cop.shift_default => tc_FF (arg_type (Ebinop b e1 e2 t)) end | Cop.Oeq => match Cop.classify_cmp (typeof e1) (typeof e2) with | Cop.cmp_case_pp => tc_andp (tc_andp (tc_int_or_ptr_type (typeof e1)) (tc_int_or_ptr_type (typeof e2))) (@check_pp_int cs e1 e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_case_pi si => tc_andp (tc_int_or_ptr_type (typeof e1)) (@check_pp_int cs e1 (Ecast e2 size_t) b t (Ebinop b e1 e2 t)) | Cop.cmp_case_ip si => tc_andp (tc_int_or_ptr_type (typeof e2)) (@check_pp_int cs (Ecast e1 size_t) e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_case_pl => tc_andp (tc_int_or_ptr_type (typeof e1)) (@check_pp_int cs e1 (Ecast e2 size_t) b t (Ebinop b e1 e2 t)) | Cop.cmp_case_lp => tc_andp (tc_int_or_ptr_type (typeof e2)) (@check_pp_int cs (Ecast e1 size_t) e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_default => tc_bool (andb (andb (is_numeric_type (typeof e1)) (is_numeric_type (typeof e2))) (is_int_type t)) (arg_type (Ebinop b e1 e2 t)) end | Cop.One => match Cop.classify_cmp (typeof e1) (typeof e2) with | Cop.cmp_case_pp => tc_andp (tc_andp (tc_int_or_ptr_type (typeof e1)) (tc_int_or_ptr_type (typeof e2))) (@check_pp_int cs e1 e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_case_pi si => tc_andp (tc_int_or_ptr_type (typeof e1)) (@check_pp_int cs e1 (Ecast e2 size_t) b t (Ebinop b e1 e2 t)) | Cop.cmp_case_ip si => tc_andp (tc_int_or_ptr_type (typeof e2)) (@check_pp_int cs (Ecast e1 size_t) e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_case_pl => tc_andp (tc_int_or_ptr_type (typeof e1)) (@check_pp_int cs e1 (Ecast e2 size_t) b t (Ebinop b e1 e2 t)) | Cop.cmp_case_lp => tc_andp (tc_int_or_ptr_type (typeof e2)) (@check_pp_int cs (Ecast e1 size_t) e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_default => tc_bool (andb (andb (is_numeric_type (typeof e1)) (is_numeric_type (typeof e2))) (is_int_type t)) (arg_type (Ebinop b e1 e2 t)) end | Cop.Olt => match Cop.classify_cmp (typeof e1) (typeof e2) with | Cop.cmp_case_pp => tc_andp (tc_andp (tc_int_or_ptr_type (typeof e1)) (tc_int_or_ptr_type (typeof e2))) (@check_pp_int cs e1 e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_case_pi si => tc_andp (tc_int_or_ptr_type (typeof e1)) (@check_pp_int cs e1 (Ecast e2 size_t) b t (Ebinop b e1 e2 t)) | Cop.cmp_case_ip si => tc_andp (tc_int_or_ptr_type (typeof e2)) (@check_pp_int cs (Ecast e1 size_t) e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_case_pl => tc_andp (tc_int_or_ptr_type (typeof e1)) (@check_pp_int cs e1 (Ecast e2 size_t) b t (Ebinop b e1 e2 t)) | Cop.cmp_case_lp => tc_andp (tc_int_or_ptr_type (typeof e2)) (@check_pp_int cs (Ecast e1 size_t) e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_default => tc_bool (andb (andb (is_numeric_type (typeof e1)) (is_numeric_type (typeof e2))) (is_int_type t)) (arg_type (Ebinop b e1 e2 t)) end | Cop.Ogt => match Cop.classify_cmp (typeof e1) (typeof e2) with | Cop.cmp_case_pp => tc_andp (tc_andp (tc_int_or_ptr_type (typeof e1)) (tc_int_or_ptr_type (typeof e2))) (@check_pp_int cs e1 e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_case_pi si => tc_andp (tc_int_or_ptr_type (typeof e1)) (@check_pp_int cs e1 (Ecast e2 size_t) b t (Ebinop b e1 e2 t)) | Cop.cmp_case_ip si => tc_andp (tc_int_or_ptr_type (typeof e2)) (@check_pp_int cs (Ecast e1 size_t) e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_case_pl => tc_andp (tc_int_or_ptr_type (typeof e1)) (@check_pp_int cs e1 (Ecast e2 size_t) b t (Ebinop b e1 e2 t)) | Cop.cmp_case_lp => tc_andp (tc_int_or_ptr_type (typeof e2)) (@check_pp_int cs (Ecast e1 size_t) e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_default => tc_bool (andb (andb (is_numeric_type (typeof e1)) (is_numeric_type (typeof e2))) (is_int_type t)) (arg_type (Ebinop b e1 e2 t)) end | Cop.Ole => match Cop.classify_cmp (typeof e1) (typeof e2) with | Cop.cmp_case_pp => tc_andp (tc_andp (tc_int_or_ptr_type (typeof e1)) (tc_int_or_ptr_type (typeof e2))) (@check_pp_int cs e1 e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_case_pi si => tc_andp (tc_int_or_ptr_type (typeof e1)) (@check_pp_int cs e1 (Ecast e2 size_t) b t (Ebinop b e1 e2 t)) | Cop.cmp_case_ip si => tc_andp (tc_int_or_ptr_type (typeof e2)) (@check_pp_int cs (Ecast e1 size_t) e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_case_pl => tc_andp (tc_int_or_ptr_type (typeof e1)) (@check_pp_int cs e1 (Ecast e2 size_t) b t (Ebinop b e1 e2 t)) | Cop.cmp_case_lp => tc_andp (tc_int_or_ptr_type (typeof e2)) (@check_pp_int cs (Ecast e1 size_t) e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_default => tc_bool (andb (andb (is_numeric_type (typeof e1)) (is_numeric_type (typeof e2))) (is_int_type t)) (arg_type (Ebinop b e1 e2 t)) end | Cop.Oge => match Cop.classify_cmp (typeof e1) (typeof e2) with | Cop.cmp_case_pp => tc_andp (tc_andp (tc_int_or_ptr_type (typeof e1)) (tc_int_or_ptr_type (typeof e2))) (@check_pp_int cs e1 e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_case_pi si => tc_andp (tc_int_or_ptr_type (typeof e1)) (@check_pp_int cs e1 (Ecast e2 size_t) b t (Ebinop b e1 e2 t)) | Cop.cmp_case_ip si => tc_andp (tc_int_or_ptr_type (typeof e2)) (@check_pp_int cs (Ecast e1 size_t) e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_case_pl => tc_andp (tc_int_or_ptr_type (typeof e1)) (@check_pp_int cs e1 (Ecast e2 size_t) b t (Ebinop b e1 e2 t)) | Cop.cmp_case_lp => tc_andp (tc_int_or_ptr_type (typeof e2)) (@check_pp_int cs (Ecast e1 size_t) e2 b t (Ebinop b e1 e2 t)) | Cop.cmp_default => tc_bool (andb (andb (is_numeric_type (typeof e1)) (is_numeric_type (typeof e2))) (is_int_type t)) (arg_type (Ebinop b e1 e2 t)) end end rho) *)
  destruct b.
  + destruct (Cop.classify_add (typeof e1) (typeof e2)).
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool (complete_type (@cenv_cs cs) t) (invalid_expression (Ealignof t t0))) (tc_bool (eqb_type t0 size_t) (invalid_expression (Ealignof t t0)))) rho) *)
    - rewrite !denote_tc_assert_andp; simpl.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_andp (@isBinOpResultType cs b e1 e2 t) (@typecheck_expr cs Delta e1)) (@typecheck_expr cs Delta e2)) rho) *)
      unfold_lift.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (denote_tc_isptr (@eval_expr cs e2 rho)) (@denote_tc_assert cs (tc_bool (complete_type (@cenv_cs cs) ty) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) (@denote_tc_assert cs (tc_int_or_ptr_type (typeof e2)) rho)) (@denote_tc_assert cs (tc_bool (is_pointer_type t) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) *)
      unfold tc_int_or_ptr_type, denote_tc_isptr.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (isptr (@eval_expr cs e1 rho))) (@denote_tc_assert cs (tc_bool (complete_type (@cenv_cs cs) ty) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) (@denote_tc_assert cs (tc_bool (negb (eqb_type (typeof e1) int_or_ptr_type)) int_or_ptr_type_error) rho)) (@denote_tc_assert cs (tc_bool (is_pointer_type t) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) *)
      destruct (eval_expr e1 rho); inv H.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (isptr (Vptr b i))) (@denote_tc_assert cs (tc_bool (complete_type (@cenv_cs cs) ty) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) (@denote_tc_assert cs (tc_bool (negb (eqb_type (typeof e2) int_or_ptr_type)) int_or_ptr_type_error) rho)) (@denote_tc_assert cs (tc_bool (is_pointer_type t) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) *)
      rewrite !andb_true_iff in H1.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (isptr (Vptr b i))) (@denote_tc_assert cs (tc_bool (complete_type (@cenv_cs cs) ty) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) (@denote_tc_assert cs (tc_bool (negb (eqb_type (typeof e2) int_or_ptr_type)) int_or_ptr_type_error) rho)) (@denote_tc_assert cs (tc_bool (is_pointer_type t) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) *)
      destruct H1 as [[? ?] ?].
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (isptr (Vptr b i))) (@denote_tc_assert cs (tc_bool (complete_type (@cenv_cs cs) ty) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) (@denote_tc_assert cs (tc_bool (negb (eqb_type (typeof e2) int_or_ptr_type)) int_or_ptr_type_error) rho)) (@denote_tc_assert cs (tc_bool (is_pointer_type t) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) *)
      rewrite H, H0, H1.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool (complete_type (@cenv_cs cs) t) (invalid_expression (Ealignof t t0))) (tc_bool (eqb_type t0 size_t) (invalid_expression (Ealignof t t0)))) rho) *)
      simpl.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@prop mpred Nveric (@eq Int.int i Int.zero)) (@prop mpred Nveric (@eq Int.int Int.zero Int.zero))) *)
      repeat apply andp_right; apply prop_right; auto.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool (complete_type (@cenv_cs cs) t) (invalid_expression (Ealignof t t0))) (tc_bool (eqb_type t0 size_t) (invalid_expression (Ealignof t t0)))) rho) *)
    - rewrite !denote_tc_assert_andp; simpl.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_andp (@isBinOpResultType cs b e1 e2 t) (@typecheck_expr cs Delta e1)) (@typecheck_expr cs Delta e2)) rho) *)
      unfold_lift.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (denote_tc_isptr (@eval_expr cs e2 rho)) (@denote_tc_assert cs (tc_bool (complete_type (@cenv_cs cs) ty) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) (@denote_tc_assert cs (tc_int_or_ptr_type (typeof e2)) rho)) (@denote_tc_assert cs (tc_bool (is_pointer_type t) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) *)
      unfold tc_int_or_ptr_type, denote_tc_isptr.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (isptr (@eval_expr cs e1 rho))) (@denote_tc_assert cs (tc_bool (complete_type (@cenv_cs cs) ty) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) (@denote_tc_assert cs (tc_bool (negb (eqb_type (typeof e1) int_or_ptr_type)) int_or_ptr_type_error) rho)) (@denote_tc_assert cs (tc_bool (is_pointer_type t) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) *)
      destruct (eval_expr e1 rho); inv H.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (isptr (Vptr b i))) (@denote_tc_assert cs (tc_bool (complete_type (@cenv_cs cs) ty) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) (@denote_tc_assert cs (tc_bool (negb (eqb_type (typeof e2) int_or_ptr_type)) int_or_ptr_type_error) rho)) (@denote_tc_assert cs (tc_bool (is_pointer_type t) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) *)
      rewrite !andb_true_iff in H1.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (isptr (Vptr b i))) (@denote_tc_assert cs (tc_bool (complete_type (@cenv_cs cs) ty) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) (@denote_tc_assert cs (tc_bool (negb (eqb_type (typeof e2) int_or_ptr_type)) int_or_ptr_type_error) rho)) (@denote_tc_assert cs (tc_bool (is_pointer_type t) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) *)
      destruct H1 as [[? ?] ?].
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (isptr (Vptr b i))) (@denote_tc_assert cs (tc_bool (complete_type (@cenv_cs cs) ty) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) (@denote_tc_assert cs (tc_bool (negb (eqb_type (typeof e2) int_or_ptr_type)) int_or_ptr_type_error) rho)) (@denote_tc_assert cs (tc_bool (is_pointer_type t) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) *)
      rewrite H, H0, H1.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool (complete_type (@cenv_cs cs) t) (invalid_expression (Ealignof t t0))) (tc_bool (eqb_type t0 size_t) (invalid_expression (Ealignof t t0)))) rho) *)
      simpl.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@prop mpred Nveric (@eq Int.int i Int.zero)) (@prop mpred Nveric (@eq Int.int Int.zero Int.zero))) *)
      repeat apply andp_right; apply prop_right; auto.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool (complete_type (@cenv_cs cs) t) (invalid_expression (Ealignof t t0))) (tc_bool (eqb_type t0 size_t) (invalid_expression (Ealignof t t0)))) rho) *)
    - rewrite !denote_tc_assert_andp; simpl.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_andp (@isBinOpResultType cs b e1 e2 t) (@typecheck_expr cs Delta e1)) (@typecheck_expr cs Delta e2)) rho) *)
      unfold_lift.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (denote_tc_isptr (@eval_expr cs e2 rho)) (@denote_tc_assert cs (tc_bool (complete_type (@cenv_cs cs) ty) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) (@denote_tc_assert cs (tc_int_or_ptr_type (typeof e2)) rho)) (@denote_tc_assert cs (tc_bool (is_pointer_type t) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) *)
      unfold tc_int_or_ptr_type, denote_tc_isptr.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (isptr (@eval_expr cs e2 rho))) (@denote_tc_assert cs (tc_bool (complete_type (@cenv_cs cs) ty) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) (@denote_tc_assert cs (tc_bool (negb (eqb_type (typeof e2) int_or_ptr_type)) int_or_ptr_type_error) rho)) (@denote_tc_assert cs (tc_bool (is_pointer_type t) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) *)
      destruct (eval_expr e2 rho); inv H.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (isptr (Vptr b i))) (@denote_tc_assert cs (tc_bool (complete_type (@cenv_cs cs) ty) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) (@denote_tc_assert cs (tc_bool (negb (eqb_type (typeof e2) int_or_ptr_type)) int_or_ptr_type_error) rho)) (@denote_tc_assert cs (tc_bool (is_pointer_type t) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) *)
      rewrite !andb_true_iff in H1.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (isptr (Vptr b i))) (@denote_tc_assert cs (tc_bool (complete_type (@cenv_cs cs) ty) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) (@denote_tc_assert cs (tc_bool (negb (eqb_type (typeof e2) int_or_ptr_type)) int_or_ptr_type_error) rho)) (@denote_tc_assert cs (tc_bool (is_pointer_type t) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) *)
      destruct H1 as [[? ?] ?].
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (isptr (Vptr b i))) (@denote_tc_assert cs (tc_bool (complete_type (@cenv_cs cs) ty) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) (@denote_tc_assert cs (tc_bool (negb (eqb_type (typeof e2) int_or_ptr_type)) int_or_ptr_type_error) rho)) (@denote_tc_assert cs (tc_bool (is_pointer_type t) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) *)
      rewrite H, H0, H1.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool (complete_type (@cenv_cs cs) t) (invalid_expression (Ealignof t t0))) (tc_bool (eqb_type t0 size_t) (invalid_expression (Ealignof t t0)))) rho) *)
      simpl.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@prop mpred Nveric (@eq Int.int i Int.zero)) (@prop mpred Nveric (@eq Int.int Int.zero Int.zero))) *)
      repeat apply andp_right; apply prop_right; auto.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool (complete_type (@cenv_cs cs) t) (invalid_expression (Ealignof t t0))) (tc_bool (eqb_type t0 size_t) (invalid_expression (Ealignof t t0)))) rho) *)
    - rewrite !denote_tc_assert_andp; simpl.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_andp (@isBinOpResultType cs b e1 e2 t) (@typecheck_expr cs Delta e1)) (@typecheck_expr cs Delta e2)) rho) *)
      unfold_lift.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (denote_tc_isptr (@eval_expr cs e2 rho)) (@denote_tc_assert cs (tc_bool (complete_type (@cenv_cs cs) ty) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) (@denote_tc_assert cs (tc_int_or_ptr_type (typeof e2)) rho)) (@denote_tc_assert cs (tc_bool (is_pointer_type t) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) *)
      unfold tc_int_or_ptr_type, denote_tc_isptr.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (isptr (@eval_expr cs e2 rho))) (@denote_tc_assert cs (tc_bool (complete_type (@cenv_cs cs) ty) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) (@denote_tc_assert cs (tc_bool (negb (eqb_type (typeof e2) int_or_ptr_type)) int_or_ptr_type_error) rho)) (@denote_tc_assert cs (tc_bool (is_pointer_type t) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) *)
      destruct (eval_expr e2 rho); inv H.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (isptr (Vptr b i))) (@denote_tc_assert cs (tc_bool (complete_type (@cenv_cs cs) ty) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) (@denote_tc_assert cs (tc_bool (negb (eqb_type (typeof e2) int_or_ptr_type)) int_or_ptr_type_error) rho)) (@denote_tc_assert cs (tc_bool (is_pointer_type t) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) *)
      rewrite !andb_true_iff in H1.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (isptr (Vptr b i))) (@denote_tc_assert cs (tc_bool (complete_type (@cenv_cs cs) ty) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) (@denote_tc_assert cs (tc_bool (negb (eqb_type (typeof e2) int_or_ptr_type)) int_or_ptr_type_error) rho)) (@denote_tc_assert cs (tc_bool (is_pointer_type t) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) *)
      destruct H1 as [[? ?] ?].
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (isptr (Vptr b i))) (@denote_tc_assert cs (tc_bool (complete_type (@cenv_cs cs) ty) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) (@denote_tc_assert cs (tc_bool (negb (eqb_type (typeof e2) int_or_ptr_type)) int_or_ptr_type_error) rho)) (@denote_tc_assert cs (tc_bool (is_pointer_type t) (op_result_type (Ebinop Cop.Oadd e1 e2 t))) rho)) *)
      rewrite H, H0, H1.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool (complete_type (@cenv_cs cs) t) (invalid_expression (Ealignof t t0))) (tc_bool (eqb_type t0 size_t) (invalid_expression (Ealignof t t0)))) rho) *)
      simpl.
(* Goal: @derives mpred Nveric P (@andp mpred Nveric (@prop mpred Nveric (@eq Int.int i Int.zero)) (@prop mpred Nveric (@eq Int.int Int.zero Int.zero))) *)
      repeat apply andp_right; apply prop_right; auto.
    - inv H.
  + inv H.
  + inv H.
  + inv H.
  + inv H.
  + inv H.
  + inv H.
  + inv H.
  + inv H.
  + inv H.
  + inv H.
  + inv H.
  + inv H.
  + inv H.
  + inv H.
  + inv H.
Qed.

Lemma const_only_isCastResultType_spec: forall {cs: compspecs} rho e t P,
  const_only_isCastResultType (typeof e) t (eval_expr e rho) = true ->
  P |-- denote_tc_assert (isCastResultType (typeof e) t e) rho.
Proof.
(* Goal: forall (v : val) (_ : @eq (option val) (@const_only_eval_expr cs (Ealignof t t0)) (@Some val v)), @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
  intros.
(* Goal: @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
  inv H.
Qed.

Lemma const_only_eval_expr_eq: forall {cs: compspecs} rho e v,
  const_only_eval_expr e = Some v ->
  eval_expr e rho = v.  
Proof.
(* Goal: forall (v : val) (_ : @eq (option val) (@const_only_eval_expr cs (Ealignof t t0)) (@Some val v)), @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
  intros.
(* Goal: @eq val (@eval_expr cs e rho) v *)
  revert v H; induction e; try solve [intros; inv H; auto].
(* Goal: forall (v : val) (_ : @eq (option val) (@const_only_eval_expr cs (Ealignof t t0)) (@Some val v)), @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
  + intros.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (@typecheck_expr cs Delta (Ecast e t)) rho) *)
    simpl in *.
(* Goal: @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
    destruct t as [| [| | |] | | | | | | |]; inv H.
(* Goal: @eq val (@liftx (LiftEnviron val) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) rho) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) *)
    auto.
(* Goal: forall (v : val) (_ : @eq (option val) (@const_only_eval_expr cs (Ealignof t t0)) (@Some val v)), @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
  + intros.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (@typecheck_expr cs Delta (Ecast e t)) rho) *)
    simpl in *.
(* Goal: @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
    destruct t as [| | | [|] | | | | |]; inv H.
(* Goal: @eq val (@liftx (LiftEnviron val) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) rho) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) *)
    auto.
(* Goal: forall (v : val) (_ : @eq (option val) (@const_only_eval_expr cs (Ealignof t t0)) (@Some val v)), @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
  + intros.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (@typecheck_expr cs Delta (Ecast e t)) rho) *)
    simpl in *.
(* Goal: @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
    destruct t as [| | | [|] | | | | |]; inv H.
(* Goal: @eq val (@liftx (LiftEnviron val) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) rho) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) *)
    auto.
(* Goal: forall (v : val) (_ : @eq (option val) (@const_only_eval_expr cs (Ealignof t t0)) (@Some val v)), @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
  + intros.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (@typecheck_expr cs Delta (Ecast e t)) rho) *)
    simpl in *.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (@typecheck_expr cs Delta e) (@isCastResultType cs (typeof e) t e)) rho) *)
    unfold option_map in H.
(* Goal: @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
    destruct (const_only_eval_expr e); inv H.
(* Goal: @eq val (@liftx (Tarrow val (LiftEnviron val)) (eval_unop u (typeof e)) (@eval_expr cs e) rho) v *)
    destruct (const_only_isUnOpResultType u (typeof e) v0 t); inv H1.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (@isUnOpResultType cs u e t) (@typecheck_expr cs Delta e)) rho) *)
    specialize (IHe _ eq_refl).
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_andp (@isBinOpResultType cs b e1 e2 t) (@typecheck_expr cs Delta e1)) (@typecheck_expr cs Delta e2)) rho) *)
    unfold_lift.
(* Goal: @eq val (@liftx (LiftEnviron val) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) rho) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) *)
    rewrite IHe; auto.
(* Goal: forall (v : val) (_ : @eq (option val) (@const_only_eval_expr cs (Ealignof t t0)) (@Some val v)), @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
  + intros.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (@typecheck_expr cs Delta (Ecast e t)) rho) *)
    simpl in *.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (@typecheck_expr cs Delta e) (@isCastResultType cs (typeof e) t e)) rho) *)
    unfold option_map in H.
(* Goal: @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
    destruct (const_only_eval_expr e1); inv H.
(* Goal: @eq val (@liftx (Tarrow val (Tarrow val (LiftEnviron val))) (force_val2 (@sem_binary_operation' cs b (typeof e1) (typeof e2))) (@eval_expr cs e1) (@eval_expr cs e2) rho) v *)
    destruct (const_only_eval_expr e2); inv H1.
(* Goal: @eq val (@liftx (Tarrow val (Tarrow val (LiftEnviron val))) (force_val2 (@sem_binary_operation' cs b (typeof e1) (typeof e2))) (@eval_expr cs e1) (@eval_expr cs e2) rho) v *)
    destruct (const_only_isBinOpResultType b (typeof e1) v0 (typeof e2) v1 t); inv H0.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_andp (@isBinOpResultType cs b e1 e2 t) (@typecheck_expr cs Delta e1)) (@typecheck_expr cs Delta e2)) rho) *)
    specialize (IHe1 _ eq_refl).
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_andp (@isBinOpResultType cs b e1 e2 t) (@typecheck_expr cs Delta e1)) (@typecheck_expr cs Delta e2)) rho) *)
    specialize (IHe2 _ eq_refl).
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_andp (@isBinOpResultType cs b e1 e2 t) (@typecheck_expr cs Delta e1)) (@typecheck_expr cs Delta e2)) rho) *)
    unfold_lift.
(* Goal: @eq val (@liftx (LiftEnviron val) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) rho) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) *)
    rewrite IHe1, IHe2; auto.
(* Goal: forall (v : val) (_ : @eq (option val) (@const_only_eval_expr cs (Ealignof t t0)) (@Some val v)), @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
  + intros.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (@typecheck_expr cs Delta (Ecast e t)) rho) *)
    simpl in *.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (@typecheck_expr cs Delta e) (@isCastResultType cs (typeof e) t e)) rho) *)
    unfold option_map in H.
(* Goal: @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
    destruct (const_only_eval_expr e); inv H. (*
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (@isUnOpResultType cs u e t) (@typecheck_expr cs Delta e)) rho) *)
    specialize (IHe _ eq_refl).
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_andp (@isBinOpResultType cs b e1 e2 t) (@typecheck_expr cs Delta e1)) (@typecheck_expr cs Delta e2)) rho) *)
    unfold_lift.
(* Goal: @eq val (@liftx (LiftEnviron val) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) rho) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) *)
    rewrite IHe; auto.*)
(* Goal: forall (v : val) (_ : @eq (option val) (@const_only_eval_expr cs (Ealignof t t0)) (@Some val v)), @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
  + intros.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (@typecheck_expr cs Delta (Ecast e t)) rho) *)
    simpl in *.
(* Goal: @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
    destruct (complete_type cenv_cs t && eqb_type t0 size_t); inv H.
(* Goal: @eq val (@liftx (LiftEnviron val) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) rho) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) *)
    auto.
(* Goal: forall (v : val) (_ : @eq (option val) (@const_only_eval_expr cs (Ealignof t t0)) (@Some val v)), @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
  + intros.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (@typecheck_expr cs Delta (Ecast e t)) rho) *)
    simpl in *.
(* Goal: @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
    destruct (complete_type cenv_cs t && eqb_type t0 size_t); inv H.
(* Goal: @eq val (@liftx (LiftEnviron val) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) rho) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) *)
    auto.
Qed.

Lemma const_only_eval_expr_tc: forall {cs: compspecs} Delta e v P,
  const_only_eval_expr e = Some v ->
  P |-- tc_expr Delta e.
Proof.
(* Goal: forall (v : val) (_ : @eq (option val) (@const_only_eval_expr cs (Ealignof t t0)) (@Some val v)), @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
  intros.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@tc_expr cs Delta e) *)
  intro rho.
(* Goal: @derives mpred Nveric (P rho) (@tc_expr cs Delta e rho) *)
  revert v H; induction e; try solve [intros; inv H].
(* Goal: forall (v : val) (_ : @eq (option val) (@const_only_eval_expr cs (Ealignof t t0)) (@Some val v)), @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
  + intros.
(* Goal: @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
    inv H.
(* Goal: @derives mpred Nveric (P rho) (@tc_expr cs Delta (Econst_int i t) rho) *)
    destruct t as [| [| | |] | | | | | | |]; inv H1.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool true (invalid_expression (Ealignof t t0))) (tc_bool true (invalid_expression (Ealignof t t0)))) rho) *)
    exact (@prop_right mpred _ True _ I).
(* Goal: forall (v : val) (_ : @eq (option val) (@const_only_eval_expr cs (Ealignof t t0)) (@Some val v)), @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
  + intros.
(* Goal: @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
    inv H.
(* Goal: @derives mpred Nveric (P rho) (@tc_expr cs Delta (Econst_single f t) rho) *)
    destruct t as [| | | [|] | | | | |]; inv H1.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool true (invalid_expression (Ealignof t t0))) (tc_bool true (invalid_expression (Ealignof t t0)))) rho) *)
    exact (@prop_right mpred _ True _ I).
(* Goal: forall (v : val) (_ : @eq (option val) (@const_only_eval_expr cs (Ealignof t t0)) (@Some val v)), @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
  + intros.
(* Goal: @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
    inv H.
(* Goal: @derives mpred Nveric (P rho) (@tc_expr cs Delta (Econst_single f t) rho) *)
    destruct t as [| | | [|] | | | | |]; inv H1.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool true (invalid_expression (Ealignof t t0))) (tc_bool true (invalid_expression (Ealignof t t0)))) rho) *)
    exact (@prop_right mpred _ True _ I).
(* Goal: forall (v : val) (_ : @eq (option val) (@const_only_eval_expr cs (Ealignof t t0)) (@Some val v)), @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
  + intros.
(* Goal: @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ecast e t) rho) *)
    unfold tc_expr in *.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (@typecheck_expr cs Delta (Ecast e t)) rho) *)
    simpl in *.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (@typecheck_expr cs Delta e) (@isCastResultType cs (typeof e) t e)) rho) *)
    unfold option_map in H.
(* Goal: @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
    destruct (const_only_eval_expr e) eqn:HH; inv H.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (@isUnOpResultType cs u e t) (@typecheck_expr cs Delta e)) rho) *)
    specialize (IHe _ eq_refl).
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_andp (@isBinOpResultType cs b e1 e2 t) (@typecheck_expr cs Delta e1)) (@typecheck_expr cs Delta e2)) rho) *)
    unfold_lift.
(* Goal: @eq val (@liftx (LiftEnviron val) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) rho) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) *)
    rewrite denote_tc_assert_andp; simpl; apply andp_right; auto.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (@isUnOpResultType cs u e t) rho) *)
    apply const_only_isUnOpResultType_spec.
(* Goal: @eq bool (@const_only_isUnOpResultType cs u (typeof e) (@eval_expr cs e rho) t) true *)
    apply (const_only_eval_expr_eq rho) in HH.
(* Goal: @eq bool (@const_only_isUnOpResultType cs u (typeof e) (@eval_expr cs e rho) t) true *)
    rewrite HH.
(* Goal: @eq val (@liftx (LiftEnviron val) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) rho) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) *)
    destruct (const_only_isUnOpResultType u (typeof e) v0 t); inv H1; auto.
(* Goal: forall (v : val) (_ : @eq (option val) (@const_only_eval_expr cs (Ealignof t t0)) (@Some val v)), @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
  + intros.
(* Goal: @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ecast e t) rho) *)
    unfold tc_expr in *.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (@typecheck_expr cs Delta (Ecast e t)) rho) *)
    simpl in *.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (@typecheck_expr cs Delta e) (@isCastResultType cs (typeof e) t e)) rho) *)
    unfold option_map in H.
(* Goal: @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
    destruct (const_only_eval_expr e1) eqn:HH1; inv H.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_andp (@isBinOpResultType cs b e1 e2 t) (@typecheck_expr cs Delta e1)) (@typecheck_expr cs Delta e2)) rho) *)
    destruct (const_only_eval_expr e2) eqn:HH2; inv H1.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_andp (@isBinOpResultType cs b e1 e2 t) (@typecheck_expr cs Delta e1)) (@typecheck_expr cs Delta e2)) rho) *)
    specialize (IHe1 _ eq_refl).
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_andp (@isBinOpResultType cs b e1 e2 t) (@typecheck_expr cs Delta e1)) (@typecheck_expr cs Delta e2)) rho) *)
    specialize (IHe2 _ eq_refl).
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_andp (@isBinOpResultType cs b e1 e2 t) (@typecheck_expr cs Delta e1)) (@typecheck_expr cs Delta e2)) rho) *)
    unfold_lift.
(* Goal: @eq val (@liftx (LiftEnviron val) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) rho) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) *)
    rewrite !denote_tc_assert_andp; simpl; repeat apply andp_right; auto.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (@isBinOpResultType cs b e1 e2 t) rho) *)
    apply const_only_isBinOpResultType_spec.
(* Goal: @eq bool (@const_only_isBinOpResultType cs b (typeof e1) (@eval_expr cs e1 rho) (typeof e2) (@eval_expr cs e2 rho) t) true *)
    apply (const_only_eval_expr_eq rho) in HH1.
(* Goal: @eq bool (@const_only_isBinOpResultType cs b (typeof e1) (@eval_expr cs e1 rho) (typeof e2) (@eval_expr cs e2 rho) t) true *)
    apply (const_only_eval_expr_eq rho) in HH2.
(* Goal: @eq bool (@const_only_isBinOpResultType cs b (typeof e1) (@eval_expr cs e1 rho) (typeof e2) (@eval_expr cs e2 rho) t) true *)
    rewrite HH1, HH2.
(* Goal: @eq val (@liftx (LiftEnviron val) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) rho) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) *)
    destruct (const_only_isBinOpResultType b (typeof e1) v0 (typeof e2) v1 t); inv H0; auto.
(* Goal: forall (v : val) (_ : @eq (option val) (@const_only_eval_expr cs (Ealignof t t0)) (@Some val v)), @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
  + intros.
(* Goal: @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ecast e t) rho) *)
    unfold tc_expr in *.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (@typecheck_expr cs Delta (Ecast e t)) rho) *)
    simpl in *.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (@typecheck_expr cs Delta e) (@isCastResultType cs (typeof e) t e)) rho) *)
    unfold option_map in H.
(* Goal: @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
    destruct (const_only_eval_expr e) eqn:HH; inv H. (*
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (@isUnOpResultType cs u e t) (@typecheck_expr cs Delta e)) rho) *)
    specialize (IHe _ eq_refl).
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_andp (@isBinOpResultType cs b e1 e2 t) (@typecheck_expr cs Delta e1)) (@typecheck_expr cs Delta e2)) rho) *)
    unfold_lift.
(* Goal: @eq val (@liftx (LiftEnviron val) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) rho) (Vptrofs (Ptrofs.repr (@alignof (@cenv_cs cs) t))) *)
    rewrite denote_tc_assert_andp; simpl; apply andp_right; auto.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (@isUnOpResultType cs u e t) rho) *)
    apply const_only_isUnOpResultType_spec.
(* Goal: @eq bool (@const_only_isUnOpResultType cs u (typeof e) (@eval_expr cs e rho) t) true *)
    apply (const_only_eval_expr_eq rho) in HH. *)
(* Goal: forall (v : val) (_ : @eq (option val) (@const_only_eval_expr cs (Ealignof t t0)) (@Some val v)), @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
  + intros.
(* Goal: @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
    inv H.
(* Goal: @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
    unfold tc_expr.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (@typecheck_expr cs Delta (Ealignof t t0)) rho) *)
    simpl typecheck_expr.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool (complete_type (@cenv_cs cs) t) (invalid_expression (Ealignof t t0))) (tc_bool (eqb_type t0 size_t) (invalid_expression (Ealignof t t0)))) rho) *)
    simpl.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool (complete_type (@cenv_cs cs) t) (invalid_expression (Ealignof t t0))) (tc_bool (eqb_type t0 size_t) (invalid_expression (Ealignof t t0)))) rho) *)
    destruct (complete_type cenv_cs t && eqb_type t0 size_t) eqn:HH; inv H1.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool (complete_type (@cenv_cs cs) t) (invalid_expression (Ealignof t t0))) (tc_bool (eqb_type t0 size_t) (invalid_expression (Ealignof t t0)))) rho) *)
    rewrite andb_true_iff in HH.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool (complete_type (@cenv_cs cs) t) (invalid_expression (Ealignof t t0))) (tc_bool (eqb_type t0 size_t) (invalid_expression (Ealignof t t0)))) rho) *)
    unfold tuint in HH; destruct HH.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool (complete_type (@cenv_cs cs) t) (invalid_expression (Ealignof t t0))) (tc_bool (eqb_type t0 size_t) (invalid_expression (Ealignof t t0)))) rho) *)
    rewrite H, H0.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool true (invalid_expression (Ealignof t t0))) (tc_bool true (invalid_expression (Ealignof t t0)))) rho) *)
    exact (@prop_right mpred _ True _ I).
(* Goal: forall (v : val) (_ : @eq (option val) (@const_only_eval_expr cs (Ealignof t t0)) (@Some val v)), @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
  + intros.
(* Goal: @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
    inv H.
(* Goal: @derives mpred Nveric (P rho) (@tc_expr cs Delta (Ealignof t t0) rho) *)
    unfold tc_expr.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (@typecheck_expr cs Delta (Ealignof t t0)) rho) *)
    simpl typecheck_expr.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool (complete_type (@cenv_cs cs) t) (invalid_expression (Ealignof t t0))) (tc_bool (eqb_type t0 size_t) (invalid_expression (Ealignof t t0)))) rho) *)
    simpl.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool (complete_type (@cenv_cs cs) t) (invalid_expression (Ealignof t t0))) (tc_bool (eqb_type t0 size_t) (invalid_expression (Ealignof t t0)))) rho) *)
    destruct (complete_type cenv_cs t && eqb_type t0 size_t) eqn:HH; inv H1.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool (complete_type (@cenv_cs cs) t) (invalid_expression (Ealignof t t0))) (tc_bool (eqb_type t0 size_t) (invalid_expression (Ealignof t t0)))) rho) *)
    rewrite andb_true_iff in HH.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool (complete_type (@cenv_cs cs) t) (invalid_expression (Ealignof t t0))) (tc_bool (eqb_type t0 size_t) (invalid_expression (Ealignof t t0)))) rho) *)
    unfold tuint in HH; destruct HH.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool (complete_type (@cenv_cs cs) t) (invalid_expression (Ealignof t t0))) (tc_bool (eqb_type t0 size_t) (invalid_expression (Ealignof t t0)))) rho) *)
    rewrite H, H0.
(* Goal: @derives mpred Nveric (P rho) (@denote_tc_assert cs (tc_andp (tc_bool true (invalid_expression (Ealignof t t0))) (tc_bool true (invalid_expression (Ealignof t t0)))) rho) *)
    exact (@prop_right mpred _ True _ I).
Qed.
