Require Import compcert.cfrontend.Ctypes.
Require Import compcert.cfrontend.Cop.
Require Import compcert.cfrontend.Clight.
Require Import VST.msl.base.
Require Import VST.veric.base.
Require Import VST.veric.mem_lessdef.

Lemma mem_lessdef_sem_cast:
  forall m1 m2, mem_lessdef m1 m2 ->
  forall v1 v1', Val.lessdef v1 v1' ->
  forall t1 t2 v, 
    classify_cast t1 t2 <> Cop.cast_case_void ->
    sem_cast v1 t1 t2 m1 = Some v ->
    sem_cast v1' t1 t2 m2 = Some v.
Proof.
(* Goal: forall (m1 m2 : Mem.mem) (_ : mem_lessdef m1 m2) (v1 v1' : val) (_ : Val.lessdef v1 v1') (t1 t2 : type) (v : val) (_ : not (@eq classify_cast_cases (classify_cast t1 t2) cast_case_void)) (_ : @eq (option val) (sem_cast v1 t1 t2 m1) (@Some val v)), @eq (option val) (sem_cast v1' t1 t2 m2) (@Some val v) *)
intros until 3. rename H1 into H9. intros.
(* Goal: @eq (option val) (sem_cast v1' t1 t2 m2) (@Some val v) *)
unfold sem_cast in *.
(* Goal: @eq (option val) match classify_cast t1 t2 with | cast_case_pointer => match v1' with | Vundef => @None val | Vint i => if Archi.ptr64 then @None val else @Some val v1' | Vlong i => if Archi.ptr64 then @Some val v1' else @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @Some val v1' end | cast_case_i2i sz2 si2 => match v1' with | Vundef => @None val | Vint i => @Some val (Vint (cast_int_int sz2 si2 i)) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | cast_case_f2f => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @Some val (Vfloat f) | Vsingle f => @None val | Vptr b i => @None val end | cast_case_s2s => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @Some val (Vsingle f) | Vptr b i => @None val end | cast_case_f2s => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @Some val (Vsingle (Float.to_single f)) | Vsingle f => @None val | Vptr b i => @None val end | cast_case_s2f => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @Some val (Vfloat (Float.of_single f)) | Vptr b i => @None val end | cast_case_i2f si1 => match v1' with | Vundef => @None val | Vint i => @Some val (Vfloat (cast_int_float si1 i)) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | cast_case_i2s si1 => match v1' with | Vundef => @None val | Vint i => @Some val (Vsingle (cast_int_single si1 i)) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | cast_case_f2i sz2 si2 => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => match cast_float_int si2 f with | Some i => @Some val (Vint (cast_int_int sz2 si2 i)) | None => @None val end | Vsingle f => @None val | Vptr b i => @None val end | cast_case_s2i sz2 si2 => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => match cast_single_int si2 f with | Some i => @Some val (Vint (cast_int_int sz2 si2 i)) | None => @None val end | Vptr b i => @None val end | cast_case_l2l => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n => @Some val (Vlong n) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | cast_case_i2l si => match v1' with | Vundef => @None val | Vint n => @Some val (Vlong (cast_int_long si n)) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | cast_case_l2i sz si => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n => @Some val (Vint (cast_int_int sz si (Int.repr (Int64.unsigned n)))) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | cast_case_l2f si1 => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @Some val (Vfloat (cast_long_float si1 i)) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | cast_case_l2s si1 => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @Some val (Vsingle (cast_long_single si1 i)) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | cast_case_f2l si2 => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => match cast_float_long si2 f with | Some i => @Some val (Vlong i) | None => @None val end | Vsingle f => @None val | Vptr b i => @None val end | cast_case_s2l si2 => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => match cast_single_long si2 f with | Some i => @Some val (Vlong i) | None => @None val end | Vptr b i => @None val end | cast_case_i2bool => match v1' with | Vundef => @None val | Vint n => @Some val (Vint (if Int.eq n Int.zero then Int.zero else Int.one)) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b ofs => if Archi.ptr64 then @None val else if Mem.weak_valid_pointer m2 b (Ptrofs.unsigned ofs) then @Some val Vone else @None val end | cast_case_l2bool => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n => @Some val (Vint (if Int64.eq n Int64.zero then Int.zero else Int.one)) | Vfloat f => @None val | Vsingle f => @None val | Vptr b ofs => if negb Archi.ptr64 then @None val else if Mem.weak_valid_pointer m2 b (Ptrofs.unsigned ofs) then @Some val Vone else @None val end | cast_case_f2bool => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @Some val (Vint (if Float.cmp Ceq f Float.zero then Int.zero else Int.one)) | Vsingle f => @None val | Vptr b i => @None val end | cast_case_s2bool => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @Some val (Vint (if Float32.cmp Ceq f Float32.zero then Int.zero else Int.one)) | Vptr b i => @None val end | cast_case_struct id1 id2 => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b ofs => if ident_eq id1 id2 then @Some val v1' else @None val end | cast_case_union id1 id2 => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b ofs => if ident_eq id1 id2 then @Some val v1' else @None val end | cast_case_void => @Some val v1' | cast_case_default => @None val end (@Some val v) *)
destruct (classify_cast t1 t2) eqn:?HH, v1; inv H1; inv H0; try reflexivity.
(* Goal: @eq (option val) (if Archi.ptr64 then @None val else if Mem.weak_valid_pointer m2 b (Ptrofs.unsigned i) then @Some val Vone else @None val) (if Archi.ptr64 then @None val else if Mem.weak_valid_pointer m1 b (Ptrofs.unsigned i) then @Some val Vone else @None val) *)
(* Goal: @eq (option val) (@Some val v1') (@Some val Vundef) *)
destruct Archi.ptr64 eqn:Hp; inv H3.
(* Goal: @eq (option val) (if Mem.weak_valid_pointer m2 b (Ptrofs.unsigned i) then @Some val Vone else @None val) (if Mem.weak_valid_pointer m1 b (Ptrofs.unsigned i) then @Some val Vone else @None val) *)
(* Goal: @eq (option val) (@Some val v1') (@Some val Vundef) *)
destruct (Mem.weak_valid_pointer m1 b (Ptrofs.unsigned i)) eqn:?; inv H1.
(* Goal: @eq (option val) (if Mem.weak_valid_pointer m2 b (Ptrofs.unsigned i) then @Some val Vone else @None val) (@Some val Vone) *)
(* Goal: @eq (option val) (@Some val v1') (@Some val Vundef) *)
rewrite (mem_lessdef_weak_valid_pointer _ _ _ _ H Heqb0). auto.
(* Goal: @eq (option val) (@Some val v1') (@Some val Vundef) *)
contradiction H9.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
auto.
Qed.

Lemma mem_lessdef_sem_binarith:
  forall m1 m2, mem_lessdef m1 m2 ->
  forall v1 v1', Val.lessdef v1 v1' ->
  forall v2 v2', Val.lessdef v2 v2' ->
  forall (sem_int: signedness -> int -> int -> option val)
    (sem_long: signedness -> int64 -> int64 -> option val)
    (sem_float: float -> float -> option val)
    (sem_single: float32 -> float32 -> option val)
    (t1: type) (t2: type) v,
   sem_binarith sem_int sem_long sem_float sem_single v1 t1 v2 t2 m1 = Some v ->
   sem_binarith sem_int sem_long sem_float sem_single v1' t1 v2' t2 m2 = Some v.
Proof.
(* Goal: forall _ : eval_lvalue ge ve te m e b i, eval_lvalue ge ve te m2 e b i *)
intros.
(* Goal: @eq (option val) (sem_binarith sem_int sem_long sem_float sem_single v1' t1 v2' t2 m2) (@Some val v) *)
unfold sem_binarith in *.
(* Goal: @eq (option val) match sem_cast v1' t1 (binarith_type (classify_binarith t1 t2)) m2 with | Some v1' => match sem_cast v2' t2 (binarith_type (classify_binarith t1 t2)) m2 with | Some v2' => match classify_binarith t1 t2 with | bin_case_i sg => match v1' with | Vundef => @None val | Vint n1 => match v2' with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end | None => @None val end | None => @None val end (@Some val v) *)
destruct (sem_cast v1 t1 (Cop.binarith_type (Cop.classify_binarith t1 t2)) m1) eqn:?H; try discriminate.
(* Goal: @eq (option val) match sem_cast v1' t1 (binarith_type (classify_binarith t1 t2)) m2 with | Some v1' => match sem_cast v2' t2 (binarith_type (classify_binarith t1 t2)) m2 with | Some v2' => match classify_binarith t1 t2 with | bin_case_i sg => match v1' with | Vundef => @None val | Vint n1 => match v2' with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end | None => @None val end | None => @None val end (@Some val v) *)
destruct (sem_cast v2 t2 (binarith_type (classify_binarith t1 t2)) m1) eqn:?H; try discriminate.
(* Goal: @eq (option val) match sem_cast v1' t1 (binarith_type (classify_binarith t1 t2)) m2 with | Some v1' => match sem_cast v2' t2 (binarith_type (classify_binarith t1 t2)) m2 with | Some v2' => match classify_binarith t1 t2 with | bin_case_i sg => match v1' with | Vundef => @None val | Vint n1 => match v2' with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end | None => @None val end | None => @None val end (@Some val v) *)
apply (mem_lessdef_sem_cast _ _ H _ _ H0) in H3.
(* Goal: @eq (option val) match sem_cast v1' t1 (binarith_type (classify_binarith t1 t2)) m2 with | Some v1' => match sem_cast v2' t2 (binarith_type (classify_binarith t1 t2)) m2 with | Some v2' => match classify_binarith t1 t2 with | bin_case_i sg => match v1' with | Vundef => @None val | Vint n1 => match v2' with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end | None => @None val end | None => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
apply (mem_lessdef_sem_cast _ _ H _ _ H1) in H4.
(* Goal: @eq (option val) match sem_cast v1' t1 (binarith_type (classify_binarith t1 t2)) m2 with | Some v1' => match sem_cast v2' t2 (binarith_type (classify_binarith t1 t2)) m2 with | Some v2' => match classify_binarith t1 t2 with | bin_case_i sg => match v1' with | Vundef => @None val | Vint n1 => match v2' with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end | None => @None val end | None => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
rewrite H3, H4.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
auto.
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
clear - H2.
destruct (classify_binarith t1 t2); inv H2; simpl;
clear; intro;
destruct t2; try destruct f; try congruence; destruct Archi.ptr64; try congruence.
destruct (classify_binarith t1 t2); inv H2; simpl;
clear; intro;
destruct t1; try destruct f; try congruence; destruct Archi.ptr64; try congruence.
Qed.

Lemma mem_lessdef_sem_shift:
  forall m1 m2, mem_lessdef m1 m2 ->
  forall v1 v1', Val.lessdef v1 v1' ->
  forall v2 v2', Val.lessdef v2 v2' ->
  forall (sem_int: signedness -> int -> int -> int)
    (sem_long: signedness -> int64 -> int64 -> int64)
    (t1: type) (t2: type) v,
   sem_shift sem_int sem_long v1 t1 v2 t2 = Some v ->
   sem_shift sem_int sem_long v1' t1 v2' t2 = Some v.
Proof.
(* Goal: forall _ : eval_lvalue ge ve te m e b i, eval_lvalue ge ve te m2 e b i *)
intros.
(* Goal: @eq (option val) (sem_shift sem_int sem_long v1' t1 v2' t2) (@Some val v) *)
unfold sem_shift in *.
destruct (classify_shift t1 t2); auto;
destruct v1; inv H2; inv H0; destruct v2; inv H4; inv H1; reflexivity.
Qed.

Lemma mem_lessdef_cmp_ptr:
  forall m1 m2, mem_lessdef m1 m2 ->
  forall v1 v1', Val.lessdef v1 v1' ->
  forall v2 v2', Val.lessdef v2 v2' ->
  forall op v,
      cmp_ptr m1 op v1 v2 = Some v ->
      cmp_ptr m2 op v1' v2' = Some v.
Proof.
(* Goal: forall _ : eval_lvalue ge ve te m e b i, eval_lvalue ge ve te m2 e b i *)
intros.
(* Goal: @eq (option val) (cmp_ptr m2 op v1' v2') (@Some val v) *)
unfold cmp_ptr in *.
(* Goal: @eq (option val) (@option_map bool val Val.of_bool (if Archi.ptr64 then Val.cmplu_bool (Mem.valid_pointer m2) op v1' v2' else Val.cmpu_bool (Mem.valid_pointer m2) op v1' v2')) (@Some val v) *)
unfold Val.cmpu_bool, Val.cmplu_bool in *.
destruct Archi.ptr64;
destruct v1; inv H2; inv H0; destruct v2; inv H4; inv H1; try reflexivity; rewrite H2;
simpl in *;
repeat match type of H2 with
 | context [eq_block ?b ?b0] => destruct (eq_block b b0); [subst b0 |]; simpl in *; try discriminate
 | context [Int64.eq ?i ?z] => destruct (Int64.eq i z); simpl in *; try discriminate 
 | context [Mem.valid_pointer m1 ?b ?z] =>
    let H9 := fresh "H" in 
    destruct (Mem.valid_pointer m1 b z) eqn:H9; 
    [ rewrite (mem_lessdef_valid_pointer _ _ _ _ H H9) |  ]
end;
rewrite ?andb_false_r in H2;
try discriminate;
rewrite ?orb_true_r;
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
auto.
Qed.

Lemma mem_lessdef_sem_cmp:
  forall m1 m2, mem_lessdef m1 m2 ->
  forall v1 v1', Val.lessdef v1 v1' ->
  forall v2 v2', Val.lessdef v2 v2' ->
  forall op (t1: type) (t2: type) v,
      sem_cmp op v1 t1 v2 t2 m1 = Some v ->
      sem_cmp op v1' t1 v2' t2 m2 = Some v.
Proof.
(* Goal: forall _ : eval_lvalue ge ve te m e b i, eval_lvalue ge ve te m2 e b i *)
intros.
(* Goal: @eq (option val) (sem_cmp op v1' t1 v2' t2 m2) (@Some val v) *)
unfold sem_cmp in *.
(* Goal: @eq (option val) match classify_cmp t1 t2 with | cmp_case_pp => cmp_ptr m2 op v1' v2' | cmp_case_pi si => match v2' with | Vundef => @None val | Vint n2 => cmp_ptr m2 op v1' (Vptrofs (ptrofs_of_int si n2)) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b ofs => if Archi.ptr64 then @None val else cmp_ptr m2 op v1' v2' end | cmp_case_ip si => match v1' with | Vundef => @None val | Vint n1 => cmp_ptr m2 op (Vptrofs (ptrofs_of_int si n1)) v2' | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b ofs => if Archi.ptr64 then @None val else cmp_ptr m2 op v1' v2' end | cmp_case_pl => match v2' with | Vundef => @None val | Vint i => @None val | Vlong n2 => cmp_ptr m2 op v1' (Vptrofs (Ptrofs.of_int64 n2)) | Vfloat f => @None val | Vsingle f => @None val | Vptr b ofs => if Archi.ptr64 then cmp_ptr m2 op v1' v2' else @None val end | cmp_case_lp => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n1 => cmp_ptr m2 op (Vptrofs (Ptrofs.of_int64 n1)) v2' | Vfloat f => @None val | Vsingle f => @None val | Vptr b ofs => if Archi.ptr64 then cmp_ptr m2 op v1' v2' else @None val end | cmp_default => sem_binarith (fun (sg : signedness) (n1 n2 : Int.int) => @Some val (Val.of_bool match sg with | Signed => Int.cmp op n1 n2 | Unsigned => Int.cmpu op n1 n2 end)) (fun (sg : signedness) (n1 n2 : Int64.int) => @Some val (Val.of_bool match sg with | Signed => Int64.cmp op n1 n2 | Unsigned => Int64.cmpu op n1 n2 end)) (fun n1 n2 : float => @Some val (Val.of_bool (Float.cmp op n1 n2))) (fun n1 n2 : float32 => @Some val (Val.of_bool (Float32.cmp op n1 n2))) v1' t1 v2' t2 m2 end (@Some val v) *)
destruct (classify_cmp t1 t2).
* (* cmp_ptr *)
(* Goal: @eq (option val) (cmp_ptr m2 op v1' v2') (@Some val v) *)
eapply mem_lessdef_cmp_ptr; eassumption.
*
(* Goal: @eq (option val) match v2' with | Vundef => @None val | Vint i => @None val | Vlong n2 => cmp_ptr m2 op v1' (Vptrofs (Ptrofs.of_int64 n2)) | Vfloat f => @None val | Vsingle f => @None val | Vptr b ofs => if Archi.ptr64 then cmp_ptr m2 op v1' v2' else @None val end (@Some val v) *)
destruct v2; try discriminate; inv H1.
(* Goal: @eq (option val) (cmp_ptr m2 op (Vptrofs (Ptrofs.of_int64 i)) v2') (@Some val v) *)
eapply mem_lessdef_cmp_ptr; try eassumption; apply Val.lessdef_refl.
all: destruct Archi.ptr64; auto;
(* Goal: @eq (option val) (cmp_ptr m2 op (Vptrofs (Ptrofs.of_int64 i)) v2') (@Some val v) *)
eapply mem_lessdef_cmp_ptr; try eassumption; apply Val.lessdef_refl.
*
(* Goal: @eq (option val) match v1' with | Vundef => @None val | Vint i => @None val | Vlong n1 => cmp_ptr m2 op (Vptrofs (Ptrofs.of_int64 n1)) v2' | Vfloat f => @None val | Vsingle f => @None val | Vptr b ofs => if Archi.ptr64 then cmp_ptr m2 op v1' v2' else @None val end (@Some val v) *)
destruct v1; try discriminate; inv H0.
(* Goal: @eq (option val) (cmp_ptr m2 op (Vptrofs (Ptrofs.of_int64 i)) v2') (@Some val v) *)
eapply mem_lessdef_cmp_ptr; try eassumption; apply Val.lessdef_refl.
all: destruct Archi.ptr64; auto;
(* Goal: @eq (option val) (cmp_ptr m2 op (Vptrofs (Ptrofs.of_int64 i)) v2') (@Some val v) *)
eapply mem_lessdef_cmp_ptr; try eassumption; apply Val.lessdef_refl.
*
(* Goal: @eq (option val) match v2' with | Vundef => @None val | Vint i => @None val | Vlong n2 => cmp_ptr m2 op v1' (Vptrofs (Ptrofs.of_int64 n2)) | Vfloat f => @None val | Vsingle f => @None val | Vptr b ofs => if Archi.ptr64 then cmp_ptr m2 op v1' v2' else @None val end (@Some val v) *)
destruct v2; try discriminate; inv H1.
(* Goal: @eq (option val) (cmp_ptr m2 op (Vptrofs (Ptrofs.of_int64 i)) v2') (@Some val v) *)
eapply mem_lessdef_cmp_ptr; try eassumption; apply Val.lessdef_refl.
all: destruct Archi.ptr64; auto;
(* Goal: @eq (option val) (cmp_ptr m2 op (Vptrofs (Ptrofs.of_int64 i)) v2') (@Some val v) *)
eapply mem_lessdef_cmp_ptr; try eassumption; apply Val.lessdef_refl.
*
(* Goal: @eq (option val) match v1' with | Vundef => @None val | Vint i => @None val | Vlong n1 => cmp_ptr m2 op (Vptrofs (Ptrofs.of_int64 n1)) v2' | Vfloat f => @None val | Vsingle f => @None val | Vptr b ofs => if Archi.ptr64 then cmp_ptr m2 op v1' v2' else @None val end (@Some val v) *)
destruct v1; try discriminate; inv H0.
(* Goal: @eq (option val) (cmp_ptr m2 op (Vptrofs (Ptrofs.of_int64 i)) v2') (@Some val v) *)
eapply mem_lessdef_cmp_ptr; try eassumption; apply Val.lessdef_refl.
all: destruct Archi.ptr64; auto;
(* Goal: @eq (option val) (cmp_ptr m2 op (Vptrofs (Ptrofs.of_int64 i)) v2') (@Some val v) *)
eapply mem_lessdef_cmp_ptr; try eassumption; apply Val.lessdef_refl.
*
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
eapply mem_lessdef_sem_binarith; eauto.
Qed.

Lemma classify_cast_void_e:
 forall t ty, classify_cast t ty = cast_case_void -> ty=Tvoid.
Proof.
(* Goal: forall _ : eval_lvalue ge ve te m e b i, eval_lvalue ge ve te m2 e b i *)
intros.
   destruct t as [ | [ | | | ] [ | ] | [ | ] | [ | ] | | | | | ];
   destruct ty as [ | [ | | | ] [ | ] | [ | ] | [ | ] | | | | | ];
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
   inv H; auto.
Qed.

Lemma mem_lessdef_eval_expr: forall ge ve te m1 m2 a v1,
   mem_lessdef m1 m2 ->
   eval_expr ge ve te m1 a v1 -> 
   exists v2, eval_expr ge ve te m2 a v2 /\ Val.lessdef v1 v2
 with mem_lessdef_eval_lvalue: forall ge ve te m1 m2 a b z,
   mem_lessdef m1 m2 ->
   eval_lvalue ge ve te m1 a b z -> 
   eval_lvalue ge ve te m2 a b z.
Proof.
*
clear mem_lessdef_eval_expr.
(* Goal: forall _ : eval_lvalue ge ve te m e b i, eval_lvalue ge ve te m2 e b i *)
intros.
induction H0;
try solve [eexists; split; [ | eapply Val.lessdef_refl ]; econstructor; eauto].
destruct IHeval_expr as [vx [? ?]].
destruct op; simpl in H1.
 +
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
   exists v. split; [ | apply Val.lessdef_refl]. econstructor; simpl; eauto.
   clear - H1 H3 H.
   unfold sem_notbool, bool_val in *.
   destruct (classify_bool (typeof a)), v1; inv H1; inv H3; try reflexivity.
   destruct Archi.ptr64 eqn:Hp; inv H2.
(* Goal: @eq (option val) (if Mem.weak_valid_pointer m2 b (Ptrofs.unsigned i) then @Some val Vone else @None val) (if Mem.weak_valid_pointer m1 b (Ptrofs.unsigned i) then @Some val Vone else @None val) *)
(* Goal: @eq (option val) (@Some val v1') (@Some val Vundef) *)
   destruct (Mem.weak_valid_pointer m1 b (Ptrofs.unsigned i)) eqn:?; inv H1.
(* Goal: @eq (option val) (if Mem.weak_valid_pointer m2 b (Ptrofs.unsigned i) then @Some val Vone else @None val) (@Some val Vone) *)
(* Goal: @eq (option val) (@Some val v1') (@Some val Vundef) *)
   rewrite (mem_lessdef_weak_valid_pointer _ _ _ _ H Heqb0). auto.
 +
   eexists; split; [ econstructor; eauto; simpl | ].
  unfold sem_notint in *.
  destruct (classify_notint (typeof a)); destruct v1; simpl in H1|-*; inv H1; inv H3; reflexivity.
  apply Val.lessdef_refl.
 +
   eexists; split; [ econstructor; eauto; simpl | ].
  unfold sem_neg in *.
  destruct (classify_neg (typeof a)); destruct v1; simpl in H1|-*; inv H1; inv H3; reflexivity.
  apply Val.lessdef_refl.
 +
   eexists; split; [ econstructor; eauto; simpl | ].
  unfold sem_absfloat in *.
  destruct (classify_neg (typeof a)); destruct v1; simpl in H1|-*; inv H1; inv H3; reflexivity.
  apply Val.lessdef_refl.
 +
   destruct IHeval_expr1 as [?v [? ?]].
   destruct IHeval_expr2 as [?v [? ?]].
   rename v0 into v1'. rename v3 into v2'.
   exists v; split; [ | apply Val.lessdef_refl].
   econstructor; try eassumption.
   clear - H0 H2 H4 H.
   destruct op; simpl in *;
   try solve [eapply mem_lessdef_sem_binarith; eauto];
   try solve [eapply mem_lessdef_sem_cmp; eauto].
   - 
     unfold sem_add in *. destruct (classify_add (typeof a1) (typeof a2)).
     destruct v1; inv H0; inv H2; destruct v2; inv H3; inv H4; reflexivity.
     destruct v1; inv H0; inv H2; destruct v2; inv H3; inv H4; reflexivity.
     destruct v1; inv H0; inv H2; destruct v2; inv H3; inv H4; reflexivity.
     destruct v1; inv H0; inv H2; destruct v2; inv H3; inv H4; reflexivity.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
     eapply mem_lessdef_sem_binarith; eauto.
  - 
     unfold sem_sub in *. destruct (classify_sub (typeof a1) (typeof a2)).
     destruct v1; inv H0; inv H2; destruct v2; inv H3; inv H4; reflexivity.
     destruct v1; inv H0; inv H2; destruct v2; inv H3; inv H4; reflexivity.
     destruct v1; inv H0; inv H2; destruct v2; inv H3; inv H4; reflexivity.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
     eapply mem_lessdef_sem_binarith; eauto.
  -
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
     eapply mem_lessdef_sem_shift; eauto.
  -
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
     eapply mem_lessdef_sem_shift; eauto.
 +   
   destruct IHeval_expr as [v1' [? ?]].
   destruct (eq_dec ty Tvoid).
   **
   subst ty. inv H1.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
   exists v1'. split. subst. econstructor; eauto. auto.
   **
   apply (mem_lessdef_sem_cast _ _ H _ _ H3) in H1.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
   exists v. split. econstructor; eauto. apply Val.lessdef_refl.
   clear - n. contradict n.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
   eapply classify_cast_void_e; eauto.
 +
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
   eapply mem_lessdef_eval_lvalue in H0; eauto.
   inv H1.
   2: eexists; split; [eapply eval_Elvalue; eauto; econstructor 2; eassumption | apply Val.lessdef_refl].
   2: eexists; split; [eapply eval_Elvalue; eauto; econstructor 3; eassumption | apply Val.lessdef_refl].
   unfold Mem.loadv in *.
   pose proof (Mem.load_valid_access _ _ _ _ _ H3).
   destruct H1 as [_ ?].
   destruct H as [? _].
   apply Mem.load_loadbytes in H3.
   destruct H3 as [bytes [? ?]]. apply H in H3.
   destruct H3 as [v' [? ?]].
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
   apply Mem.loadbytes_load in H3; auto.
   subst.
   exists (decode_val chunk v').
   split.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
   eapply eval_Elvalue; eauto.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
   econstructor 1; eauto.
   clear - H5.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
   apply mem_lessdef_decode_val; auto.
*
clear mem_lessdef_eval_lvalue.
(* Goal: forall _ : eval_lvalue ge ve te m e b i, eval_lvalue ge ve te m2 e b i *)
intros.
induction H0.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
constructor 1; auto.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
constructor 2; auto.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
eapply mem_lessdef_eval_expr in H0; eauto.
destruct H0 as [v2 [? ?]].
inv H1.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
econstructor; eauto.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
eapply mem_lessdef_eval_expr in H0; eauto.
destruct H0 as [v2 [? ?]].
inv H4.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
econstructor 4; eauto.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
eapply mem_lessdef_eval_expr in H0; eauto.
destruct H0 as [v2 [? ?]].
inv H3.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
econstructor 5; eauto.
Qed.

Lemma unaryop_mem_lessaloc {op u t m v m2}
      (V: sem_unary_operation op u t m = Some v)
      (M:mem_lessalloc m m2):
      sem_unary_operation op u t m2 = Some v.
(* Goal: @eq (option val) (sem_unary_operation op u t m2) (@Some val v) *)
Proof. destruct op; simpl; inv V; try econstructor.
(* Goal: @eq (option val) (sem_notbool u t m2) (sem_notbool u t m) *)
unfold sem_notbool.
(* Goal: @eq (option val) (@option_map bool val (fun b : bool => Val.of_bool (negb b)) (bool_val u t m2)) (@option_map bool val (fun b : bool => Val.of_bool (negb b)) (bool_val u t m)) *)
unfold bool_val.
(* Goal: @eq (option val) (@option_map bool val (fun b : bool => Val.of_bool (negb b)) match classify_bool t with | bool_case_i => match u with | Vundef => @None bool | Vint n => @Some bool (negb (Int.eq n Int.zero)) | Vlong i => @None bool | Vfloat f => @None bool | Vsingle f => @None bool | Vptr b ofs => if Archi.ptr64 then @None bool else if Mem.weak_valid_pointer m2 b (Ptrofs.unsigned ofs) then @Some bool true else @None bool end | bool_case_l => match u with | Vundef => @None bool | Vint i => @None bool | Vlong n => @Some bool (negb (Int64.eq n Int64.zero)) | Vfloat f => @None bool | Vsingle f => @None bool | Vptr b ofs => if negb Archi.ptr64 then @None bool else if Mem.weak_valid_pointer m2 b (Ptrofs.unsigned ofs) then @Some bool true else @None bool end | bool_case_f => match u with | Vundef => @None bool | Vint i => @None bool | Vlong i => @None bool | Vfloat f => @Some bool (negb (Float.cmp Ceq f Float.zero)) | Vsingle f => @None bool | Vptr b i => @None bool end | bool_case_s => match u with | Vundef => @None bool | Vint i => @None bool | Vlong i => @None bool | Vfloat f => @None bool | Vsingle f => @Some bool (negb (Float32.cmp Ceq f Float32.zero)) | Vptr b i => @None bool end | bool_default => @None bool end) (@option_map bool val (fun b : bool => Val.of_bool (negb b)) match classify_bool t with | bool_case_i => match u with | Vundef => @None bool | Vint n => @Some bool (negb (Int.eq n Int.zero)) | Vlong i => @None bool | Vfloat f => @None bool | Vsingle f => @None bool | Vptr b ofs => if Archi.ptr64 then @None bool else if Mem.weak_valid_pointer m b (Ptrofs.unsigned ofs) then @Some bool true else @None bool end | bool_case_l => match u with | Vundef => @None bool | Vint i => @None bool | Vlong n => @Some bool (negb (Int64.eq n Int64.zero)) | Vfloat f => @None bool | Vsingle f => @None bool | Vptr b ofs => if negb Archi.ptr64 then @None bool else if Mem.weak_valid_pointer m b (Ptrofs.unsigned ofs) then @Some bool true else @None bool end | bool_case_f => match u with | Vundef => @None bool | Vint i => @None bool | Vlong i => @None bool | Vfloat f => @Some bool (negb (Float.cmp Ceq f Float.zero)) | Vsingle f => @None bool | Vptr b i => @None bool end | bool_case_s => match u with | Vundef => @None bool | Vint i => @None bool | Vlong i => @None bool | Vfloat f => @None bool | Vsingle f => @Some bool (negb (Float32.cmp Ceq f Float32.zero)) | Vptr b i => @None bool end | bool_default => @None bool end) *)
remember (classify_bool t) as c.
(* Goal: @eq (option val) (@option_map bool val (fun b : bool => Val.of_bool (negb b)) match c with | bool_case_i => match u with | Vundef => @None bool | Vint n => @Some bool (negb (Int.eq n Int.zero)) | Vlong i => @None bool | Vfloat f => @None bool | Vsingle f => @None bool | Vptr b ofs => if Archi.ptr64 then @None bool else if Mem.weak_valid_pointer m2 b (Ptrofs.unsigned ofs) then @Some bool true else @None bool end | bool_case_l => match u with | Vundef => @None bool | Vint i => @None bool | Vlong n => @Some bool (negb (Int64.eq n Int64.zero)) | Vfloat f => @None bool | Vsingle f => @None bool | Vptr b ofs => if negb Archi.ptr64 then @None bool else if Mem.weak_valid_pointer m2 b (Ptrofs.unsigned ofs) then @Some bool true else @None bool end | bool_case_f => match u with | Vundef => @None bool | Vint i => @None bool | Vlong i => @None bool | Vfloat f => @Some bool (negb (Float.cmp Ceq f Float.zero)) | Vsingle f => @None bool | Vptr b i => @None bool end | bool_case_s => match u with | Vundef => @None bool | Vint i => @None bool | Vlong i => @None bool | Vfloat f => @None bool | Vsingle f => @Some bool (negb (Float32.cmp Ceq f Float32.zero)) | Vptr b i => @None bool end | bool_default => @None bool end) (@option_map bool val (fun b : bool => Val.of_bool (negb b)) match c with | bool_case_i => match u with | Vundef => @None bool | Vint n => @Some bool (negb (Int.eq n Int.zero)) | Vlong i => @None bool | Vfloat f => @None bool | Vsingle f => @None bool | Vptr b ofs => if Archi.ptr64 then @None bool else if Mem.weak_valid_pointer m b (Ptrofs.unsigned ofs) then @Some bool true else @None bool end | bool_case_l => match u with | Vundef => @None bool | Vint i => @None bool | Vlong n => @Some bool (negb (Int64.eq n Int64.zero)) | Vfloat f => @None bool | Vsingle f => @None bool | Vptr b ofs => if negb Archi.ptr64 then @None bool else if Mem.weak_valid_pointer m b (Ptrofs.unsigned ofs) then @Some bool true else @None bool end | bool_case_f => match u with | Vundef => @None bool | Vint i => @None bool | Vlong i => @None bool | Vfloat f => @Some bool (negb (Float.cmp Ceq f Float.zero)) | Vsingle f => @None bool | Vptr b i => @None bool end | bool_case_s => match u with | Vundef => @None bool | Vint i => @None bool | Vlong i => @None bool | Vfloat f => @None bool | Vsingle f => @Some bool (negb (Float32.cmp Ceq f Float32.zero)) | Vptr b i => @None bool end | bool_default => @None bool end) *)
destruct c; trivial.
(* Goal: @eq (option val) (@option_map bool val (fun b : bool => Val.of_bool (negb b)) match u with | Vundef => @None bool | Vint n => @Some bool (negb (Int.eq n Int.zero)) | Vlong i => @None bool | Vfloat f => @None bool | Vsingle f => @None bool | Vptr b ofs => if Archi.ptr64 then @None bool else if Mem.weak_valid_pointer m2 b (Ptrofs.unsigned ofs) then @Some bool true else @None bool end) (@option_map bool val (fun b : bool => Val.of_bool (negb b)) match u with | Vundef => @None bool | Vint n => @Some bool (negb (Int.eq n Int.zero)) | Vlong i => @None bool | Vfloat f => @None bool | Vsingle f => @None bool | Vptr b ofs => if Archi.ptr64 then @None bool else if Mem.weak_valid_pointer m b (Ptrofs.unsigned ofs) then @Some bool true else @None bool end) *)
destruct u; trivial.
(* Goal: @eq (option val) (if Archi.ptr64 then @None val else if Mem.weak_valid_pointer m b (Ptrofs.unsigned i) then @Some val Vone else @None val) (if Archi.ptr64 then @None val else if Mem.weak_valid_pointer m2 b (Ptrofs.unsigned i) then @Some val Vone else @None val) *)
rewrite (weak_valid_pointer_lessalloc M); trivial.
Qed.

Lemma sem_cast_mem_lessaloc {v t d m m2} (M:mem_lessalloc m m2):
      sem_cast v t d m = sem_cast v t d m2.
Proof.
(* Goal: @eq (option val) (sem_cast v t d m) (sem_cast v t d m2) *)
unfold sem_cast.
(* Goal: @eq (option val) match classify_cast t d with | cast_case_pointer => match v with | Vundef => @None val | Vint i => if Archi.ptr64 then @None val else @Some val v | Vlong i => if Archi.ptr64 then @Some val v else @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @Some val v end | cast_case_i2i sz2 si2 => match v with | Vundef => @None val | Vint i => @Some val (Vint (cast_int_int sz2 si2 i)) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | cast_case_f2f => match v with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @Some val (Vfloat f) | Vsingle f => @None val | Vptr b i => @None val end | cast_case_s2s => match v with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @Some val (Vsingle f) | Vptr b i => @None val end | cast_case_f2s => match v with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @Some val (Vsingle (Float.to_single f)) | Vsingle f => @None val | Vptr b i => @None val end | cast_case_s2f => match v with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @Some val (Vfloat (Float.of_single f)) | Vptr b i => @None val end | cast_case_i2f si1 => match v with | Vundef => @None val | Vint i => @Some val (Vfloat (cast_int_float si1 i)) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | cast_case_i2s si1 => match v with | Vundef => @None val | Vint i => @Some val (Vsingle (cast_int_single si1 i)) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | cast_case_f2i sz2 si2 => match v with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => match cast_float_int si2 f with | Some i => @Some val (Vint (cast_int_int sz2 si2 i)) | None => @None val end | Vsingle f => @None val | Vptr b i => @None val end | cast_case_s2i sz2 si2 => match v with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => match cast_single_int si2 f with | Some i => @Some val (Vint (cast_int_int sz2 si2 i)) | None => @None val end | Vptr b i => @None val end | cast_case_l2l => match v with | Vundef => @None val | Vint i => @None val | Vlong n => @Some val (Vlong n) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | cast_case_i2l si => match v with | Vundef => @None val | Vint n => @Some val (Vlong (cast_int_long si n)) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | cast_case_l2i sz si => match v with | Vundef => @None val | Vint i => @None val | Vlong n => @Some val (Vint (cast_int_int sz si (Int.repr (Int64.unsigned n)))) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | cast_case_l2f si1 => match v with | Vundef => @None val | Vint i => @None val | Vlong i => @Some val (Vfloat (cast_long_float si1 i)) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | cast_case_l2s si1 => match v with | Vundef => @None val | Vint i => @None val | Vlong i => @Some val (Vsingle (cast_long_single si1 i)) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | cast_case_f2l si2 => match v with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => match cast_float_long si2 f with | Some i => @Some val (Vlong i) | None => @None val end | Vsingle f => @None val | Vptr b i => @None val end | cast_case_s2l si2 => match v with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => match cast_single_long si2 f with | Some i => @Some val (Vlong i) | None => @None val end | Vptr b i => @None val end | cast_case_i2bool => match v with | Vundef => @None val | Vint n => @Some val (Vint (if Int.eq n Int.zero then Int.zero else Int.one)) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b ofs => if Archi.ptr64 then @None val else if Mem.weak_valid_pointer m b (Ptrofs.unsigned ofs) then @Some val Vone else @None val end | cast_case_l2bool => match v with | Vundef => @None val | Vint i => @None val | Vlong n => @Some val (Vint (if Int64.eq n Int64.zero then Int.zero else Int.one)) | Vfloat f => @None val | Vsingle f => @None val | Vptr b ofs => if negb Archi.ptr64 then @None val else if Mem.weak_valid_pointer m b (Ptrofs.unsigned ofs) then @Some val Vone else @None val end | cast_case_f2bool => match v with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @Some val (Vint (if Float.cmp Ceq f Float.zero then Int.zero else Int.one)) | Vsingle f => @None val | Vptr b i => @None val end | cast_case_s2bool => match v with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @Some val (Vint (if Float32.cmp Ceq f Float32.zero then Int.zero else Int.one)) | Vptr b i => @None val end | cast_case_struct id1 id2 => match v with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b ofs => if ident_eq id1 id2 then @Some val v else @None val end | cast_case_union id1 id2 => match v with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b ofs => if ident_eq id1 id2 then @Some val v else @None val end | cast_case_void => @Some val v | cast_case_default => @None val end match classify_cast t d with | cast_case_pointer => match v with | Vundef => @None val | Vint i => if Archi.ptr64 then @None val else @Some val v | Vlong i => if Archi.ptr64 then @Some val v else @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @Some val v end | cast_case_i2i sz2 si2 => match v with | Vundef => @None val | Vint i => @Some val (Vint (cast_int_int sz2 si2 i)) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | cast_case_f2f => match v with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @Some val (Vfloat f) | Vsingle f => @None val | Vptr b i => @None val end | cast_case_s2s => match v with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @Some val (Vsingle f) | Vptr b i => @None val end | cast_case_f2s => match v with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @Some val (Vsingle (Float.to_single f)) | Vsingle f => @None val | Vptr b i => @None val end | cast_case_s2f => match v with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @Some val (Vfloat (Float.of_single f)) | Vptr b i => @None val end | cast_case_i2f si1 => match v with | Vundef => @None val | Vint i => @Some val (Vfloat (cast_int_float si1 i)) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | cast_case_i2s si1 => match v with | Vundef => @None val | Vint i => @Some val (Vsingle (cast_int_single si1 i)) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | cast_case_f2i sz2 si2 => match v with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => match cast_float_int si2 f with | Some i => @Some val (Vint (cast_int_int sz2 si2 i)) | None => @None val end | Vsingle f => @None val | Vptr b i => @None val end | cast_case_s2i sz2 si2 => match v with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => match cast_single_int si2 f with | Some i => @Some val (Vint (cast_int_int sz2 si2 i)) | None => @None val end | Vptr b i => @None val end | cast_case_l2l => match v with | Vundef => @None val | Vint i => @None val | Vlong n => @Some val (Vlong n) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | cast_case_i2l si => match v with | Vundef => @None val | Vint n => @Some val (Vlong (cast_int_long si n)) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | cast_case_l2i sz si => match v with | Vundef => @None val | Vint i => @None val | Vlong n => @Some val (Vint (cast_int_int sz si (Int.repr (Int64.unsigned n)))) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | cast_case_l2f si1 => match v with | Vundef => @None val | Vint i => @None val | Vlong i => @Some val (Vfloat (cast_long_float si1 i)) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | cast_case_l2s si1 => match v with | Vundef => @None val | Vint i => @None val | Vlong i => @Some val (Vsingle (cast_long_single si1 i)) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | cast_case_f2l si2 => match v with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => match cast_float_long si2 f with | Some i => @Some val (Vlong i) | None => @None val end | Vsingle f => @None val | Vptr b i => @None val end | cast_case_s2l si2 => match v with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => match cast_single_long si2 f with | Some i => @Some val (Vlong i) | None => @None val end | Vptr b i => @None val end | cast_case_i2bool => match v with | Vundef => @None val | Vint n => @Some val (Vint (if Int.eq n Int.zero then Int.zero else Int.one)) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b ofs => if Archi.ptr64 then @None val else if Mem.weak_valid_pointer m2 b (Ptrofs.unsigned ofs) then @Some val Vone else @None val end | cast_case_l2bool => match v with | Vundef => @None val | Vint i => @None val | Vlong n => @Some val (Vint (if Int64.eq n Int64.zero then Int.zero else Int.one)) | Vfloat f => @None val | Vsingle f => @None val | Vptr b ofs => if negb Archi.ptr64 then @None val else if Mem.weak_valid_pointer m2 b (Ptrofs.unsigned ofs) then @Some val Vone else @None val end | cast_case_f2bool => match v with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @Some val (Vint (if Float.cmp Ceq f Float.zero then Int.zero else Int.one)) | Vsingle f => @None val | Vptr b i => @None val end | cast_case_s2bool => match v with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @Some val (Vint (if Float32.cmp Ceq f Float32.zero then Int.zero else Int.one)) | Vptr b i => @None val end | cast_case_struct id1 id2 => match v with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b ofs => if ident_eq id1 id2 then @Some val v else @None val end | cast_case_union id1 id2 => match v with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b ofs => if ident_eq id1 id2 then @Some val v else @None val end | cast_case_void => @Some val v | cast_case_default => @None val end *)
destruct (classify_cast t d); trivial.
(* Goal: @eq (option val) match v with | Vundef => @None val | Vint n => @Some val (Vint (if Int.eq n Int.zero then Int.zero else Int.one)) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b ofs => if Archi.ptr64 then @None val else if Mem.weak_valid_pointer m b (Ptrofs.unsigned ofs) then @Some val Vone else @None val end match v with | Vundef => @None val | Vint n => @Some val (Vint (if Int.eq n Int.zero then Int.zero else Int.one)) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b ofs => if Archi.ptr64 then @None val else if Mem.weak_valid_pointer m2 b (Ptrofs.unsigned ofs) then @Some val Vone else @None val end *)
destruct v; trivial.
(* Goal: @eq (option val) (if Archi.ptr64 then @None val else if Mem.weak_valid_pointer m b (Ptrofs.unsigned i) then @Some val Vone else @None val) (if Archi.ptr64 then @None val else if Mem.weak_valid_pointer m2 b (Ptrofs.unsigned i) then @Some val Vone else @None val) *)
rewrite (weak_valid_pointer_lessalloc M); trivial.
Qed.

Lemma sem_cmp_mem_lessalloc {f v1 t1 v2 t2 m m2} (M : mem_lessalloc m m2):
      sem_cmp f v1 t1 v2 t2 m2 = sem_cmp f v1 t1 v2 t2 m.
(* Goal: @eq (option val) (sem_cmp Ceq v1 t1 v2 t2 m2) (sem_cmp Ceq v1 t1 v2 t2 m) *)
Proof. unfold sem_cmp, cmp_ptr.
  destruct (classify_cmp t1 t2);
  try solve [destruct Archi.ptr64; rewrite (valid_pointer_lessalloc M); trivial].
(* Goal: @eq (option val) (sem_binarith (fun (sg : signedness) (n1 n2 : Int.int) => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end)) (fun (sg : signedness) (n1 n2 : Int64.int) => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end)) (fun n1 n2 : float => @Some val (Val.of_bool (Float.cmp Ceq n1 n2))) (fun n1 n2 : float32 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2))) v1 t1 v2 t2 m2) (sem_binarith (fun (sg : signedness) (n1 n2 : Int.int) => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end)) (fun (sg : signedness) (n1 n2 : Int64.int) => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end)) (fun n1 n2 : float => @Some val (Val.of_bool (Float.cmp Ceq n1 n2))) (fun n1 n2 : float32 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2))) v1 t1 v2 t2 m) *)
 unfold sem_binarith.
(* Goal: @eq (option val) match sem_cast v1 t1 (binarith_type (classify_binarith t1 t2)) m2 with | Some v1' => match sem_cast v2 t2 (binarith_type (classify_binarith t1 t2)) m2 with | Some v2' => match classify_binarith t1 t2 with | bin_case_i sg => match v1' with | Vundef => @None val | Vint n1 => match v2' with | Vundef => @None val | Vint n2 => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong n2 => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => @Some val (Val.of_bool (Float.cmp Ceq n1 n2)) | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2)) | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end | None => @None val end | None => @None val end match sem_cast v1 t1 (binarith_type (classify_binarith t1 t2)) m with | Some v1' => match sem_cast v2 t2 (binarith_type (classify_binarith t1 t2)) m with | Some v2' => match classify_binarith t1 t2 with | bin_case_i sg => match v1' with | Vundef => @None val | Vint n1 => match v2' with | Vundef => @None val | Vint n2 => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong n2 => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => @Some val (Val.of_bool (Float.cmp Ceq n1 n2)) | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2)) | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end | None => @None val end | None => @None val end *)
    do 2 rewrite (sem_cast_mem_lessaloc M); trivial.
Qed.

Lemma binaryop_mem_lessaloc {ge op v1 t1 v2 t2 m v m2}
      (V: sem_binary_operation ge op v1 t1 v2 t2 m = Some v)
      (M:mem_lessalloc m m2):
      sem_binary_operation ge op v1 t1 v2 t2 m2 = Some v.
Proof. destruct op; simpl; inv V; try econstructor; clear -M.
+ unfold sem_add.
(* Goal: @eq (option val) match classify_add t1 t2 with | add_case_pi ty si => sem_add_ptr_int ge ty si v1 v2 | add_case_pl ty => sem_add_ptr_long ge ty v1 v2 | add_case_ip si ty => sem_add_ptr_int ge ty si v2 v1 | add_case_lp ty => sem_add_ptr_long ge ty v2 v1 | add_default => sem_binarith (fun (_ : signedness) (n1 n2 : Int.int) => @Some val (Vint (Int.add n1 n2))) (fun (_ : signedness) (n1 n2 : Int64.int) => @Some val (Vlong (Int64.add n1 n2))) (fun n1 n2 : float => @Some val (Vfloat (Float.add n1 n2))) (fun n1 n2 : float32 => @Some val (Vsingle (Float32.add n1 n2))) v1 t1 v2 t2 m2 end match classify_add t1 t2 with | add_case_pi ty si => sem_add_ptr_int ge ty si v1 v2 | add_case_pl ty => sem_add_ptr_long ge ty v1 v2 | add_case_ip si ty => sem_add_ptr_int ge ty si v2 v1 | add_case_lp ty => sem_add_ptr_long ge ty v2 v1 | add_default => sem_binarith (fun (_ : signedness) (n1 n2 : Int.int) => @Some val (Vint (Int.add n1 n2))) (fun (_ : signedness) (n1 n2 : Int64.int) => @Some val (Vlong (Int64.add n1 n2))) (fun n1 n2 : float => @Some val (Vfloat (Float.add n1 n2))) (fun n1 n2 : float32 => @Some val (Vsingle (Float32.add n1 n2))) v1 t1 v2 t2 m end *)
  remember (classify_add t1 t2) as c.
(* Goal: @eq (option val) match c with | sub_case_pi ty si => match v1 with | Vundef => @None val | Vint n1 => match v2 with | Vundef => @None val | Vint n2 => if Archi.ptr64 then @None val else @Some val (Vint (Int.sub n1 (Int.mul (Int.repr (@sizeof ge ty)) n2))) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong n1 => match v2 with | Vundef => @None val | Vint n2 => if Archi.ptr64 then @Some val (Vlong (Int64.sub n1 (Int64.mul (Int64.repr (@sizeof ge ty)) (cast_int_long si n2)))) else @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b1 ofs1 => match v2 with | Vundef => @None val | Vint n2 => @Some val (Vptr b1 (Ptrofs.sub ofs1 (Ptrofs.mul (Ptrofs.repr (@sizeof ge ty)) (ptrofs_of_int si n2)))) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end end | sub_case_pp ty => match v1 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b1 ofs1 => match v2 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b2 ofs2 => if eq_block b1 b2 then if andb (@proj_sumbool (Z.lt Z0 (@sizeof ge ty)) (Z.ge Z0 (@sizeof ge ty)) (zlt Z0 (@sizeof ge ty))) (@proj_sumbool (Z.le (@sizeof ge ty) Ptrofs.max_signed) (Z.gt (@sizeof ge ty) Ptrofs.max_signed) (zle (@sizeof ge ty) Ptrofs.max_signed)) then @Some val (Vptrofs (Ptrofs.divs (Ptrofs.sub ofs1 ofs2) (Ptrofs.repr (@sizeof ge ty)))) else @None val else @None val end end | sub_case_pl ty => match v1 with | Vundef => @None val | Vint n1 => match v2 with | Vundef => @None val | Vint i => @None val | Vlong n2 => if Archi.ptr64 then @None val else @Some val (Vint (Int.sub n1 (Int.mul (Int.repr (@sizeof ge ty)) (Int.repr (Int64.unsigned n2))))) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong n1 => match v2 with | Vundef => @None val | Vint i => @None val | Vlong n2 => if Archi.ptr64 then @Some val (Vlong (Int64.sub n1 (Int64.mul (Int64.repr (@sizeof ge ty)) n2))) else @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b1 ofs1 => match v2 with | Vundef => @None val | Vint i => @None val | Vlong n2 => @Some val (Vptr b1 (Ptrofs.sub ofs1 (Ptrofs.mul (Ptrofs.repr (@sizeof ge ty)) (Ptrofs.of_int64 n2)))) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end end | sub_default => sem_binarith (fun (_ : signedness) (n1 n2 : Int.int) => @Some val (Vint (Int.sub n1 n2))) (fun (_ : signedness) (n1 n2 : Int64.int) => @Some val (Vlong (Int64.sub n1 n2))) (fun n1 n2 : float => @Some val (Vfloat (Float.sub n1 n2))) (fun n1 n2 : float32 => @Some val (Vsingle (Float32.sub n1 n2))) v1 t1 v2 t2 m2 end match c with | sub_case_pi ty si => match v1 with | Vundef => @None val | Vint n1 => match v2 with | Vundef => @None val | Vint n2 => if Archi.ptr64 then @None val else @Some val (Vint (Int.sub n1 (Int.mul (Int.repr (@sizeof ge ty)) n2))) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong n1 => match v2 with | Vundef => @None val | Vint n2 => if Archi.ptr64 then @Some val (Vlong (Int64.sub n1 (Int64.mul (Int64.repr (@sizeof ge ty)) (cast_int_long si n2)))) else @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b1 ofs1 => match v2 with | Vundef => @None val | Vint n2 => @Some val (Vptr b1 (Ptrofs.sub ofs1 (Ptrofs.mul (Ptrofs.repr (@sizeof ge ty)) (ptrofs_of_int si n2)))) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end end | sub_case_pp ty => match v1 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b1 ofs1 => match v2 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b2 ofs2 => if eq_block b1 b2 then if andb (@proj_sumbool (Z.lt Z0 (@sizeof ge ty)) (Z.ge Z0 (@sizeof ge ty)) (zlt Z0 (@sizeof ge ty))) (@proj_sumbool (Z.le (@sizeof ge ty) Ptrofs.max_signed) (Z.gt (@sizeof ge ty) Ptrofs.max_signed) (zle (@sizeof ge ty) Ptrofs.max_signed)) then @Some val (Vptrofs (Ptrofs.divs (Ptrofs.sub ofs1 ofs2) (Ptrofs.repr (@sizeof ge ty)))) else @None val else @None val end end | sub_case_pl ty => match v1 with | Vundef => @None val | Vint n1 => match v2 with | Vundef => @None val | Vint i => @None val | Vlong n2 => if Archi.ptr64 then @None val else @Some val (Vint (Int.sub n1 (Int.mul (Int.repr (@sizeof ge ty)) (Int.repr (Int64.unsigned n2))))) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong n1 => match v2 with | Vundef => @None val | Vint i => @None val | Vlong n2 => if Archi.ptr64 then @Some val (Vlong (Int64.sub n1 (Int64.mul (Int64.repr (@sizeof ge ty)) n2))) else @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b1 ofs1 => match v2 with | Vundef => @None val | Vint i => @None val | Vlong n2 => @Some val (Vptr b1 (Ptrofs.sub ofs1 (Ptrofs.mul (Ptrofs.repr (@sizeof ge ty)) (Ptrofs.of_int64 n2)))) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end end | sub_default => sem_binarith (fun (_ : signedness) (n1 n2 : Int.int) => @Some val (Vint (Int.sub n1 n2))) (fun (_ : signedness) (n1 n2 : Int64.int) => @Some val (Vlong (Int64.sub n1 n2))) (fun n1 n2 : float => @Some val (Vfloat (Float.sub n1 n2))) (fun n1 n2 : float32 => @Some val (Vsingle (Float32.sub n1 n2))) v1 t1 v2 t2 m end *)
  destruct c.
  - destruct v1; trivial.
  - destruct v1; trivial.
  - destruct v1; trivial.
  - destruct v1; trivial.
  - unfold sem_binarith.
(* Goal: @eq (option val) match sem_cast v1 t1 (binarith_type (classify_binarith t1 t2)) m2 with | Some v1' => match sem_cast v2 t2 (binarith_type (classify_binarith t1 t2)) m2 with | Some v2' => match classify_binarith t1 t2 with | bin_case_i sg => match v1' with | Vundef => @None val | Vint n1 => match v2' with | Vundef => @None val | Vint n2 => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong n2 => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => @Some val (Val.of_bool (Float.cmp Ceq n1 n2)) | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2)) | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end | None => @None val end | None => @None val end match sem_cast v1 t1 (binarith_type (classify_binarith t1 t2)) m with | Some v1' => match sem_cast v2 t2 (binarith_type (classify_binarith t1 t2)) m with | Some v2' => match classify_binarith t1 t2 with | bin_case_i sg => match v1' with | Vundef => @None val | Vint n1 => match v2' with | Vundef => @None val | Vint n2 => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong n2 => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => @Some val (Val.of_bool (Float.cmp Ceq n1 n2)) | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2)) | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end | None => @None val end | None => @None val end *)
    do 2 rewrite (sem_cast_mem_lessaloc M); trivial.
+ unfold sem_sub.
(* Goal: @eq (option val) match classify_sub t1 t2 with | sub_case_pi ty si => match v1 with | Vundef => @None val | Vint n1 => match v2 with | Vundef => @None val | Vint n2 => if Archi.ptr64 then @None val else @Some val (Vint (Int.sub n1 (Int.mul (Int.repr (@sizeof ge ty)) n2))) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong n1 => match v2 with | Vundef => @None val | Vint n2 => if Archi.ptr64 then @Some val (Vlong (Int64.sub n1 (Int64.mul (Int64.repr (@sizeof ge ty)) (cast_int_long si n2)))) else @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b1 ofs1 => match v2 with | Vundef => @None val | Vint n2 => @Some val (Vptr b1 (Ptrofs.sub ofs1 (Ptrofs.mul (Ptrofs.repr (@sizeof ge ty)) (ptrofs_of_int si n2)))) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end end | sub_case_pp ty => match v1 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b1 ofs1 => match v2 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b2 ofs2 => if eq_block b1 b2 then if andb (@proj_sumbool (Z.lt Z0 (@sizeof ge ty)) (Z.ge Z0 (@sizeof ge ty)) (zlt Z0 (@sizeof ge ty))) (@proj_sumbool (Z.le (@sizeof ge ty) Ptrofs.max_signed) (Z.gt (@sizeof ge ty) Ptrofs.max_signed) (zle (@sizeof ge ty) Ptrofs.max_signed)) then @Some val (Vptrofs (Ptrofs.divs (Ptrofs.sub ofs1 ofs2) (Ptrofs.repr (@sizeof ge ty)))) else @None val else @None val end end | sub_case_pl ty => match v1 with | Vundef => @None val | Vint n1 => match v2 with | Vundef => @None val | Vint i => @None val | Vlong n2 => if Archi.ptr64 then @None val else @Some val (Vint (Int.sub n1 (Int.mul (Int.repr (@sizeof ge ty)) (Int.repr (Int64.unsigned n2))))) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong n1 => match v2 with | Vundef => @None val | Vint i => @None val | Vlong n2 => if Archi.ptr64 then @Some val (Vlong (Int64.sub n1 (Int64.mul (Int64.repr (@sizeof ge ty)) n2))) else @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b1 ofs1 => match v2 with | Vundef => @None val | Vint i => @None val | Vlong n2 => @Some val (Vptr b1 (Ptrofs.sub ofs1 (Ptrofs.mul (Ptrofs.repr (@sizeof ge ty)) (Ptrofs.of_int64 n2)))) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end end | sub_default => sem_binarith (fun (_ : signedness) (n1 n2 : Int.int) => @Some val (Vint (Int.sub n1 n2))) (fun (_ : signedness) (n1 n2 : Int64.int) => @Some val (Vlong (Int64.sub n1 n2))) (fun n1 n2 : float => @Some val (Vfloat (Float.sub n1 n2))) (fun n1 n2 : float32 => @Some val (Vsingle (Float32.sub n1 n2))) v1 t1 v2 t2 m2 end match classify_sub t1 t2 with | sub_case_pi ty si => match v1 with | Vundef => @None val | Vint n1 => match v2 with | Vundef => @None val | Vint n2 => if Archi.ptr64 then @None val else @Some val (Vint (Int.sub n1 (Int.mul (Int.repr (@sizeof ge ty)) n2))) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong n1 => match v2 with | Vundef => @None val | Vint n2 => if Archi.ptr64 then @Some val (Vlong (Int64.sub n1 (Int64.mul (Int64.repr (@sizeof ge ty)) (cast_int_long si n2)))) else @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b1 ofs1 => match v2 with | Vundef => @None val | Vint n2 => @Some val (Vptr b1 (Ptrofs.sub ofs1 (Ptrofs.mul (Ptrofs.repr (@sizeof ge ty)) (ptrofs_of_int si n2)))) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end end | sub_case_pp ty => match v1 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b1 ofs1 => match v2 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b2 ofs2 => if eq_block b1 b2 then if andb (@proj_sumbool (Z.lt Z0 (@sizeof ge ty)) (Z.ge Z0 (@sizeof ge ty)) (zlt Z0 (@sizeof ge ty))) (@proj_sumbool (Z.le (@sizeof ge ty) Ptrofs.max_signed) (Z.gt (@sizeof ge ty) Ptrofs.max_signed) (zle (@sizeof ge ty) Ptrofs.max_signed)) then @Some val (Vptrofs (Ptrofs.divs (Ptrofs.sub ofs1 ofs2) (Ptrofs.repr (@sizeof ge ty)))) else @None val else @None val end end | sub_case_pl ty => match v1 with | Vundef => @None val | Vint n1 => match v2 with | Vundef => @None val | Vint i => @None val | Vlong n2 => if Archi.ptr64 then @None val else @Some val (Vint (Int.sub n1 (Int.mul (Int.repr (@sizeof ge ty)) (Int.repr (Int64.unsigned n2))))) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong n1 => match v2 with | Vundef => @None val | Vint i => @None val | Vlong n2 => if Archi.ptr64 then @Some val (Vlong (Int64.sub n1 (Int64.mul (Int64.repr (@sizeof ge ty)) n2))) else @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b1 ofs1 => match v2 with | Vundef => @None val | Vint i => @None val | Vlong n2 => @Some val (Vptr b1 (Ptrofs.sub ofs1 (Ptrofs.mul (Ptrofs.repr (@sizeof ge ty)) (Ptrofs.of_int64 n2)))) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end end | sub_default => sem_binarith (fun (_ : signedness) (n1 n2 : Int.int) => @Some val (Vint (Int.sub n1 n2))) (fun (_ : signedness) (n1 n2 : Int64.int) => @Some val (Vlong (Int64.sub n1 n2))) (fun n1 n2 : float => @Some val (Vfloat (Float.sub n1 n2))) (fun n1 n2 : float32 => @Some val (Vsingle (Float32.sub n1 n2))) v1 t1 v2 t2 m end *)
  remember (classify_sub t1 t2) as c.
(* Goal: @eq (option val) match c with | sub_case_pi ty si => match v1 with | Vundef => @None val | Vint n1 => match v2 with | Vundef => @None val | Vint n2 => if Archi.ptr64 then @None val else @Some val (Vint (Int.sub n1 (Int.mul (Int.repr (@sizeof ge ty)) n2))) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong n1 => match v2 with | Vundef => @None val | Vint n2 => if Archi.ptr64 then @Some val (Vlong (Int64.sub n1 (Int64.mul (Int64.repr (@sizeof ge ty)) (cast_int_long si n2)))) else @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b1 ofs1 => match v2 with | Vundef => @None val | Vint n2 => @Some val (Vptr b1 (Ptrofs.sub ofs1 (Ptrofs.mul (Ptrofs.repr (@sizeof ge ty)) (ptrofs_of_int si n2)))) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end end | sub_case_pp ty => match v1 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b1 ofs1 => match v2 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b2 ofs2 => if eq_block b1 b2 then if andb (@proj_sumbool (Z.lt Z0 (@sizeof ge ty)) (Z.ge Z0 (@sizeof ge ty)) (zlt Z0 (@sizeof ge ty))) (@proj_sumbool (Z.le (@sizeof ge ty) Ptrofs.max_signed) (Z.gt (@sizeof ge ty) Ptrofs.max_signed) (zle (@sizeof ge ty) Ptrofs.max_signed)) then @Some val (Vptrofs (Ptrofs.divs (Ptrofs.sub ofs1 ofs2) (Ptrofs.repr (@sizeof ge ty)))) else @None val else @None val end end | sub_case_pl ty => match v1 with | Vundef => @None val | Vint n1 => match v2 with | Vundef => @None val | Vint i => @None val | Vlong n2 => if Archi.ptr64 then @None val else @Some val (Vint (Int.sub n1 (Int.mul (Int.repr (@sizeof ge ty)) (Int.repr (Int64.unsigned n2))))) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong n1 => match v2 with | Vundef => @None val | Vint i => @None val | Vlong n2 => if Archi.ptr64 then @Some val (Vlong (Int64.sub n1 (Int64.mul (Int64.repr (@sizeof ge ty)) n2))) else @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b1 ofs1 => match v2 with | Vundef => @None val | Vint i => @None val | Vlong n2 => @Some val (Vptr b1 (Ptrofs.sub ofs1 (Ptrofs.mul (Ptrofs.repr (@sizeof ge ty)) (Ptrofs.of_int64 n2)))) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end end | sub_default => sem_binarith (fun (_ : signedness) (n1 n2 : Int.int) => @Some val (Vint (Int.sub n1 n2))) (fun (_ : signedness) (n1 n2 : Int64.int) => @Some val (Vlong (Int64.sub n1 n2))) (fun n1 n2 : float => @Some val (Vfloat (Float.sub n1 n2))) (fun n1 n2 : float32 => @Some val (Vsingle (Float32.sub n1 n2))) v1 t1 v2 t2 m2 end match c with | sub_case_pi ty si => match v1 with | Vundef => @None val | Vint n1 => match v2 with | Vundef => @None val | Vint n2 => if Archi.ptr64 then @None val else @Some val (Vint (Int.sub n1 (Int.mul (Int.repr (@sizeof ge ty)) n2))) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong n1 => match v2 with | Vundef => @None val | Vint n2 => if Archi.ptr64 then @Some val (Vlong (Int64.sub n1 (Int64.mul (Int64.repr (@sizeof ge ty)) (cast_int_long si n2)))) else @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b1 ofs1 => match v2 with | Vundef => @None val | Vint n2 => @Some val (Vptr b1 (Ptrofs.sub ofs1 (Ptrofs.mul (Ptrofs.repr (@sizeof ge ty)) (ptrofs_of_int si n2)))) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end end | sub_case_pp ty => match v1 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b1 ofs1 => match v2 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b2 ofs2 => if eq_block b1 b2 then if andb (@proj_sumbool (Z.lt Z0 (@sizeof ge ty)) (Z.ge Z0 (@sizeof ge ty)) (zlt Z0 (@sizeof ge ty))) (@proj_sumbool (Z.le (@sizeof ge ty) Ptrofs.max_signed) (Z.gt (@sizeof ge ty) Ptrofs.max_signed) (zle (@sizeof ge ty) Ptrofs.max_signed)) then @Some val (Vptrofs (Ptrofs.divs (Ptrofs.sub ofs1 ofs2) (Ptrofs.repr (@sizeof ge ty)))) else @None val else @None val end end | sub_case_pl ty => match v1 with | Vundef => @None val | Vint n1 => match v2 with | Vundef => @None val | Vint i => @None val | Vlong n2 => if Archi.ptr64 then @None val else @Some val (Vint (Int.sub n1 (Int.mul (Int.repr (@sizeof ge ty)) (Int.repr (Int64.unsigned n2))))) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong n1 => match v2 with | Vundef => @None val | Vint i => @None val | Vlong n2 => if Archi.ptr64 then @Some val (Vlong (Int64.sub n1 (Int64.mul (Int64.repr (@sizeof ge ty)) n2))) else @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b1 ofs1 => match v2 with | Vundef => @None val | Vint i => @None val | Vlong n2 => @Some val (Vptr b1 (Ptrofs.sub ofs1 (Ptrofs.mul (Ptrofs.repr (@sizeof ge ty)) (Ptrofs.of_int64 n2)))) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end end | sub_default => sem_binarith (fun (_ : signedness) (n1 n2 : Int.int) => @Some val (Vint (Int.sub n1 n2))) (fun (_ : signedness) (n1 n2 : Int64.int) => @Some val (Vlong (Int64.sub n1 n2))) (fun n1 n2 : float => @Some val (Vfloat (Float.sub n1 n2))) (fun n1 n2 : float32 => @Some val (Vsingle (Float32.sub n1 n2))) v1 t1 v2 t2 m end *)
  destruct c.
  - destruct v1; trivial.
  - destruct v1; trivial.
  - destruct v1; trivial.
  - unfold sem_binarith.
(* Goal: @eq (option val) match sem_cast v1 t1 (binarith_type (classify_binarith t1 t2)) m2 with | Some v1' => match sem_cast v2 t2 (binarith_type (classify_binarith t1 t2)) m2 with | Some v2' => match classify_binarith t1 t2 with | bin_case_i sg => match v1' with | Vundef => @None val | Vint n1 => match v2' with | Vundef => @None val | Vint n2 => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong n2 => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => @Some val (Val.of_bool (Float.cmp Ceq n1 n2)) | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2)) | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end | None => @None val end | None => @None val end match sem_cast v1 t1 (binarith_type (classify_binarith t1 t2)) m with | Some v1' => match sem_cast v2 t2 (binarith_type (classify_binarith t1 t2)) m with | Some v2' => match classify_binarith t1 t2 with | bin_case_i sg => match v1' with | Vundef => @None val | Vint n1 => match v2' with | Vundef => @None val | Vint n2 => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong n2 => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => @Some val (Val.of_bool (Float.cmp Ceq n1 n2)) | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2)) | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end | None => @None val end | None => @None val end *)
    do 2 rewrite (sem_cast_mem_lessaloc M); trivial.
+ unfold sem_mul.
(* Goal: @eq (option val) (sem_binarith (fun (sg : signedness) (n1 n2 : Int.int) => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end)) (fun (sg : signedness) (n1 n2 : Int64.int) => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end)) (fun n1 n2 : float => @Some val (Val.of_bool (Float.cmp Ceq n1 n2))) (fun n1 n2 : float32 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2))) v1 t1 v2 t2 m2) (sem_binarith (fun (sg : signedness) (n1 n2 : Int.int) => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end)) (fun (sg : signedness) (n1 n2 : Int64.int) => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end)) (fun n1 n2 : float => @Some val (Val.of_bool (Float.cmp Ceq n1 n2))) (fun n1 n2 : float32 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2))) v1 t1 v2 t2 m) *)
  unfold sem_binarith.
(* Goal: @eq (option val) match sem_cast v1 t1 (binarith_type (classify_binarith t1 t2)) m2 with | Some v1' => match sem_cast v2 t2 (binarith_type (classify_binarith t1 t2)) m2 with | Some v2' => match classify_binarith t1 t2 with | bin_case_i sg => match v1' with | Vundef => @None val | Vint n1 => match v2' with | Vundef => @None val | Vint n2 => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong n2 => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => @Some val (Val.of_bool (Float.cmp Ceq n1 n2)) | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2)) | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end | None => @None val end | None => @None val end match sem_cast v1 t1 (binarith_type (classify_binarith t1 t2)) m with | Some v1' => match sem_cast v2 t2 (binarith_type (classify_binarith t1 t2)) m with | Some v2' => match classify_binarith t1 t2 with | bin_case_i sg => match v1' with | Vundef => @None val | Vint n1 => match v2' with | Vundef => @None val | Vint n2 => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong n2 => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => @Some val (Val.of_bool (Float.cmp Ceq n1 n2)) | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2)) | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end | None => @None val end | None => @None val end *)
  do 2 rewrite (sem_cast_mem_lessaloc M); trivial.
+ unfold sem_div.
(* Goal: @eq (option val) (sem_binarith (fun (sg : signedness) (n1 n2 : Int.int) => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end)) (fun (sg : signedness) (n1 n2 : Int64.int) => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end)) (fun n1 n2 : float => @Some val (Val.of_bool (Float.cmp Ceq n1 n2))) (fun n1 n2 : float32 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2))) v1 t1 v2 t2 m2) (sem_binarith (fun (sg : signedness) (n1 n2 : Int.int) => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end)) (fun (sg : signedness) (n1 n2 : Int64.int) => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end)) (fun n1 n2 : float => @Some val (Val.of_bool (Float.cmp Ceq n1 n2))) (fun n1 n2 : float32 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2))) v1 t1 v2 t2 m) *)
  unfold sem_binarith.
(* Goal: @eq (option val) match sem_cast v1 t1 (binarith_type (classify_binarith t1 t2)) m2 with | Some v1' => match sem_cast v2 t2 (binarith_type (classify_binarith t1 t2)) m2 with | Some v2' => match classify_binarith t1 t2 with | bin_case_i sg => match v1' with | Vundef => @None val | Vint n1 => match v2' with | Vundef => @None val | Vint n2 => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong n2 => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => @Some val (Val.of_bool (Float.cmp Ceq n1 n2)) | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2)) | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end | None => @None val end | None => @None val end match sem_cast v1 t1 (binarith_type (classify_binarith t1 t2)) m with | Some v1' => match sem_cast v2 t2 (binarith_type (classify_binarith t1 t2)) m with | Some v2' => match classify_binarith t1 t2 with | bin_case_i sg => match v1' with | Vundef => @None val | Vint n1 => match v2' with | Vundef => @None val | Vint n2 => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong n2 => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => @Some val (Val.of_bool (Float.cmp Ceq n1 n2)) | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2)) | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end | None => @None val end | None => @None val end *)
  do 2 rewrite (sem_cast_mem_lessaloc M); trivial.
+ unfold sem_mod.
(* Goal: @eq (option val) (sem_binarith (fun (sg : signedness) (n1 n2 : Int.int) => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end)) (fun (sg : signedness) (n1 n2 : Int64.int) => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end)) (fun n1 n2 : float => @Some val (Val.of_bool (Float.cmp Ceq n1 n2))) (fun n1 n2 : float32 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2))) v1 t1 v2 t2 m2) (sem_binarith (fun (sg : signedness) (n1 n2 : Int.int) => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end)) (fun (sg : signedness) (n1 n2 : Int64.int) => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end)) (fun n1 n2 : float => @Some val (Val.of_bool (Float.cmp Ceq n1 n2))) (fun n1 n2 : float32 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2))) v1 t1 v2 t2 m) *)
  unfold sem_binarith.
(* Goal: @eq (option val) match sem_cast v1 t1 (binarith_type (classify_binarith t1 t2)) m2 with | Some v1' => match sem_cast v2 t2 (binarith_type (classify_binarith t1 t2)) m2 with | Some v2' => match classify_binarith t1 t2 with | bin_case_i sg => match v1' with | Vundef => @None val | Vint n1 => match v2' with | Vundef => @None val | Vint n2 => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong n2 => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => @Some val (Val.of_bool (Float.cmp Ceq n1 n2)) | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2)) | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end | None => @None val end | None => @None val end match sem_cast v1 t1 (binarith_type (classify_binarith t1 t2)) m with | Some v1' => match sem_cast v2 t2 (binarith_type (classify_binarith t1 t2)) m with | Some v2' => match classify_binarith t1 t2 with | bin_case_i sg => match v1' with | Vundef => @None val | Vint n1 => match v2' with | Vundef => @None val | Vint n2 => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong n2 => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => @Some val (Val.of_bool (Float.cmp Ceq n1 n2)) | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2)) | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end | None => @None val end | None => @None val end *)
  do 2 rewrite (sem_cast_mem_lessaloc M); trivial.
+ unfold sem_and.
(* Goal: @eq (option val) (sem_binarith (fun (sg : signedness) (n1 n2 : Int.int) => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end)) (fun (sg : signedness) (n1 n2 : Int64.int) => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end)) (fun n1 n2 : float => @Some val (Val.of_bool (Float.cmp Ceq n1 n2))) (fun n1 n2 : float32 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2))) v1 t1 v2 t2 m2) (sem_binarith (fun (sg : signedness) (n1 n2 : Int.int) => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end)) (fun (sg : signedness) (n1 n2 : Int64.int) => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end)) (fun n1 n2 : float => @Some val (Val.of_bool (Float.cmp Ceq n1 n2))) (fun n1 n2 : float32 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2))) v1 t1 v2 t2 m) *)
  unfold sem_binarith.
(* Goal: @eq (option val) match sem_cast v1 t1 (binarith_type (classify_binarith t1 t2)) m2 with | Some v1' => match sem_cast v2 t2 (binarith_type (classify_binarith t1 t2)) m2 with | Some v2' => match classify_binarith t1 t2 with | bin_case_i sg => match v1' with | Vundef => @None val | Vint n1 => match v2' with | Vundef => @None val | Vint n2 => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong n2 => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => @Some val (Val.of_bool (Float.cmp Ceq n1 n2)) | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2)) | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end | None => @None val end | None => @None val end match sem_cast v1 t1 (binarith_type (classify_binarith t1 t2)) m with | Some v1' => match sem_cast v2 t2 (binarith_type (classify_binarith t1 t2)) m with | Some v2' => match classify_binarith t1 t2 with | bin_case_i sg => match v1' with | Vundef => @None val | Vint n1 => match v2' with | Vundef => @None val | Vint n2 => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong n2 => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => @Some val (Val.of_bool (Float.cmp Ceq n1 n2)) | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2)) | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end | None => @None val end | None => @None val end *)
  do 2 rewrite (sem_cast_mem_lessaloc M); trivial.
+ unfold sem_or.
(* Goal: @eq (option val) (sem_binarith (fun (sg : signedness) (n1 n2 : Int.int) => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end)) (fun (sg : signedness) (n1 n2 : Int64.int) => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end)) (fun n1 n2 : float => @Some val (Val.of_bool (Float.cmp Ceq n1 n2))) (fun n1 n2 : float32 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2))) v1 t1 v2 t2 m2) (sem_binarith (fun (sg : signedness) (n1 n2 : Int.int) => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end)) (fun (sg : signedness) (n1 n2 : Int64.int) => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end)) (fun n1 n2 : float => @Some val (Val.of_bool (Float.cmp Ceq n1 n2))) (fun n1 n2 : float32 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2))) v1 t1 v2 t2 m) *)
  unfold sem_binarith.
(* Goal: @eq (option val) match sem_cast v1 t1 (binarith_type (classify_binarith t1 t2)) m2 with | Some v1' => match sem_cast v2 t2 (binarith_type (classify_binarith t1 t2)) m2 with | Some v2' => match classify_binarith t1 t2 with | bin_case_i sg => match v1' with | Vundef => @None val | Vint n1 => match v2' with | Vundef => @None val | Vint n2 => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong n2 => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => @Some val (Val.of_bool (Float.cmp Ceq n1 n2)) | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2)) | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end | None => @None val end | None => @None val end match sem_cast v1 t1 (binarith_type (classify_binarith t1 t2)) m with | Some v1' => match sem_cast v2 t2 (binarith_type (classify_binarith t1 t2)) m with | Some v2' => match classify_binarith t1 t2 with | bin_case_i sg => match v1' with | Vundef => @None val | Vint n1 => match v2' with | Vundef => @None val | Vint n2 => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong n2 => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => @Some val (Val.of_bool (Float.cmp Ceq n1 n2)) | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2)) | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end | None => @None val end | None => @None val end *)
  do 2 rewrite (sem_cast_mem_lessaloc M); trivial.
+ unfold sem_xor.
(* Goal: @eq (option val) (sem_binarith (fun (sg : signedness) (n1 n2 : Int.int) => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end)) (fun (sg : signedness) (n1 n2 : Int64.int) => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end)) (fun n1 n2 : float => @Some val (Val.of_bool (Float.cmp Ceq n1 n2))) (fun n1 n2 : float32 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2))) v1 t1 v2 t2 m2) (sem_binarith (fun (sg : signedness) (n1 n2 : Int.int) => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end)) (fun (sg : signedness) (n1 n2 : Int64.int) => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end)) (fun n1 n2 : float => @Some val (Val.of_bool (Float.cmp Ceq n1 n2))) (fun n1 n2 : float32 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2))) v1 t1 v2 t2 m) *)
  unfold sem_binarith.
(* Goal: @eq (option val) match sem_cast v1 t1 (binarith_type (classify_binarith t1 t2)) m2 with | Some v1' => match sem_cast v2 t2 (binarith_type (classify_binarith t1 t2)) m2 with | Some v2' => match classify_binarith t1 t2 with | bin_case_i sg => match v1' with | Vundef => @None val | Vint n1 => match v2' with | Vundef => @None val | Vint n2 => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong n2 => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => @Some val (Val.of_bool (Float.cmp Ceq n1 n2)) | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2)) | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end | None => @None val end | None => @None val end match sem_cast v1 t1 (binarith_type (classify_binarith t1 t2)) m with | Some v1' => match sem_cast v2 t2 (binarith_type (classify_binarith t1 t2)) m with | Some v2' => match classify_binarith t1 t2 with | bin_case_i sg => match v1' with | Vundef => @None val | Vint n1 => match v2' with | Vundef => @None val | Vint n2 => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong n2 => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => @Some val (Val.of_bool (Float.cmp Ceq n1 n2)) | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2)) | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end | None => @None val end | None => @None val end *)
  do 2 rewrite (sem_cast_mem_lessaloc M); trivial.
+ unfold sem_cmp, cmp_ptr.
  destruct (classify_cmp t1 t2);
  try solve [destruct Archi.ptr64; rewrite (valid_pointer_lessalloc M); trivial].
(* Goal: @eq (option val) (sem_binarith (fun (sg : signedness) (n1 n2 : Int.int) => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end)) (fun (sg : signedness) (n1 n2 : Int64.int) => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end)) (fun n1 n2 : float => @Some val (Val.of_bool (Float.cmp Ceq n1 n2))) (fun n1 n2 : float32 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2))) v1 t1 v2 t2 m2) (sem_binarith (fun (sg : signedness) (n1 n2 : Int.int) => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end)) (fun (sg : signedness) (n1 n2 : Int64.int) => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end)) (fun n1 n2 : float => @Some val (Val.of_bool (Float.cmp Ceq n1 n2))) (fun n1 n2 : float32 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2))) v1 t1 v2 t2 m) *)
 unfold sem_binarith.
(* Goal: @eq (option val) match sem_cast v1 t1 (binarith_type (classify_binarith t1 t2)) m2 with | Some v1' => match sem_cast v2 t2 (binarith_type (classify_binarith t1 t2)) m2 with | Some v2' => match classify_binarith t1 t2 with | bin_case_i sg => match v1' with | Vundef => @None val | Vint n1 => match v2' with | Vundef => @None val | Vint n2 => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong n2 => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => @Some val (Val.of_bool (Float.cmp Ceq n1 n2)) | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2)) | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end | None => @None val end | None => @None val end match sem_cast v1 t1 (binarith_type (classify_binarith t1 t2)) m with | Some v1' => match sem_cast v2 t2 (binarith_type (classify_binarith t1 t2)) m with | Some v2' => match classify_binarith t1 t2 with | bin_case_i sg => match v1' with | Vundef => @None val | Vint n1 => match v2' with | Vundef => @None val | Vint n2 => @Some val (Val.of_bool match sg with | Signed => Int.cmp Ceq n1 n2 | Unsigned => Int.cmpu Ceq n1 n2 end) | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v1' with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong n2 => @Some val (Val.of_bool match sg with | Signed => Int64.cmp Ceq n1 n2 | Unsigned => Int64.cmpu Ceq n1 n2 end) | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => @Some val (Val.of_bool (Float.cmp Ceq n1 n2)) | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v1' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v2' with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => @Some val (Val.of_bool (Float32.cmp Ceq n1 n2)) | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end | None => @None val end | None => @None val end *)
    do 2 rewrite (sem_cast_mem_lessaloc M); trivial.
+ apply (sem_cmp_mem_lessalloc M).
+ apply (sem_cmp_mem_lessalloc M).
+ apply (sem_cmp_mem_lessalloc M).
+ apply (sem_cmp_mem_lessalloc M).
+ apply (sem_cmp_mem_lessalloc M).
Qed.

Lemma eval_expr_eval_lvalue_mem_lessalloc ge ve te m:
     (forall (e : expr) (v : val),
        eval_expr ge ve te m e v ->
        forall m2 : mem, mem_lessalloc m m2 -> eval_expr ge ve te m2 e v) /\
     (forall (e : expr) (b : block) (i : ptrofs),
        eval_lvalue ge ve te m e b i ->
        forall m2 : mem, mem_lessalloc m m2 -> eval_lvalue ge ve te m2 e b i).
(* Goal: and (forall (e : expr) (v : val) (_ : eval_expr ge ve te m e v) (m2 : Mem.mem) (_ : mem_lessalloc m m2), eval_expr ge ve te m2 e v) (forall (e : expr) (b : block) (i : Ptrofs.int) (_ : eval_lvalue ge ve te m e b i) (m2 : Mem.mem) (_ : mem_lessalloc m m2), eval_lvalue ge ve te m2 e b i) *)
Proof. apply eval_expr_lvalue_ind; intros; try solve [econstructor; eauto].
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
+ econstructor; eauto. eapply unaryop_mem_lessaloc; eauto.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
+ econstructor; eauto. eapply binaryop_mem_lessaloc; eauto.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
+ econstructor; eauto. rewrite <- H1. symmetry. apply sem_cast_mem_lessaloc; trivial.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
+ econstructor; eauto.
(* Goal: deref_loc (typeof a) m2 loc ofs v *)
  destruct H2 as [M1 [M2 M3]].
  inv H1; simpl in *.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
  - eapply deref_loc_value; eauto.
    simpl. destruct (Mem.load_loadbytes _ _ _ _ _ H3) as [vals [X Y]]; subst.
(* Goal: @eq (option val) (Mem.load chunk m2 loc (Ptrofs.unsigned ofs)) (@Some val (decode_val chunk vals)) *)
    rewrite M1 in X. apply Mem.load_valid_access in H3. destruct H3.
(* Goal: @eq (option val) (Mem.load chunk m2 loc (Ptrofs.unsigned ofs)) (@Some val (decode_val chunk vals)) *)
    eapply Mem.loadbytes_load; trivial.
  - apply deref_loc_reference; trivial.
  - apply deref_loc_copy; trivial.
Qed.

Lemma eval_expr_mem_lessalloc {ge ve te m m2 e v} (M:mem_lessalloc m m2):
      eval_expr ge ve te m e v -> eval_expr ge ve te m2 e v.
(* Goal: forall _ : eval_lvalue ge ve te m e b i, eval_lvalue ge ve te m2 e b i *)
Proof. intros. eapply eval_expr_eval_lvalue_mem_lessalloc; eauto. Qed.

Lemma eval_exprlist_mem_lessalloc {ge ve te}:
      forall al tyargs vargs m m2 (M:mem_lessalloc m m2)
             (E:eval_exprlist ge ve te m al tyargs vargs),
      eval_exprlist ge ve te m2 al tyargs vargs.
Proof.
(* Goal: forall (al : list expr) (tyargs : typelist) (vargs : list val) (m m2 : Mem.mem) (_ : mem_lessalloc m m2) (_ : eval_exprlist ge ve te m al tyargs vargs), eval_exprlist ge ve te m2 al tyargs vargs *)
  induction al; simpl; intros; inv E.
(* Goal: eval_exprlist ge ve te m2 (@nil expr) Tnil (@nil val) *)
(* Goal: eval_exprlist ge ve te m2 (@cons expr a al) (Tcons ty tyl) (@cons val v2 vl) *)
   econstructor.
(* Goal: eval_exprlist ge ve te m2 (@cons expr a al) (Tcons ty tyl) (@cons val v2 vl) *)
   apply (eval_expr_mem_lessalloc M) in H1.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
   rewrite (sem_cast_mem_lessaloc M) in H2. econstructor; eauto.
Qed.

Lemma eval_lvalue_mem_lessalloc {ge ve te m m2 e b i} (M:mem_lessalloc m m2):
      eval_lvalue ge ve te m e b i -> eval_lvalue ge ve te m2 e b i.
(* Goal: forall _ : eval_lvalue ge ve te m e b i, eval_lvalue ge ve te m2 e b i *)
Proof. intros. eapply eval_expr_eval_lvalue_mem_lessalloc; eauto. Qed.

(* Currently fails because jsafeN__ind is too weak.

Lemma jsafeN_mem_equiv {Z Jspec ge n z c jm1 jm2} :
  juicy_mem_equiv jm1 jm2 ->
  ext_spec_stable juicy_mem_equiv (JE_spec _ Jspec) ->
  @jsafeN Z Jspec ge n z c jm1 ->
  @jsafeN Z Jspec ge n z c jm2.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
Proof. intros; eapply jsafeN__mem_equiv; eauto. Qed. should do it;
explicit proof attempt:
  unfold jsafeN in *.
  intros E [Spre Sexit] S1.
  revert jm2 E. unfold jsafeN in *.
  induction S1 as
      [ z c jm1
      | n z c jm1 c' jm1' step safe IH
      | n z c jm1 ef args x atex Pre Post
      | n z c jm1 v Halt Exit ]; intros jm2 E.

  - constructor 1.

  - destruct (juicy_step_mem_equiv_sim E step) as (jm2' & E' & step').
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
    econstructor 2; eauto.
    apply IH, E'.

(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
  - econstructor 3 with (x := x); eauto.
    intros ret jm2' z' n' Hargsty Hretty Hn [-> [lev pure]] post.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
    destruct (Post ret jm2' z' _ Hargsty Hretty Hn) as (c' & atex' & safe'); auto.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
    + split; auto.
      destruct E as [Ed Ew].
      unfold juicy_safety.pures_eq in *.
      unfold juicy_safety.pures_sub in *.
      split.
      * repeat rewrite level_juice_level_phi in *.
        congruence.
      * revert pure.
        rewrite Ew.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
        auto.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
    + exists c'; split; auto.

(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
  - econstructor 4; eauto.
Qed.

Lemma jsafeN_mem_lessdef {Z Jspec ge n z c jm1 jm2} :
  juicy_mem_lessdef jm1 jm2 ->
  ext_spec_stable juicy_mem_lessdef (JE_spec _ Jspec) ->
  @jsafeN Z Jspec ge n z c jm1 ->
  @jsafeN Z Jspec ge n z c jm2.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
Proof. intros; eapply jsafeN__mem_lessdef; eauto. Qed. should do it;
explicit proof attempt:
  intros L [Spre Sexit] S1.
  revert jm2 L.
  induction S1 as
      [ z c jm1
      | n z c jm1 c' jm1' step safe IH
      | n z c jm1 ef args x atex Pre Post
      | n z c jm1 v Halt Exit ]; intros jm2 L.

  - constructor 1.

  - destruct (juicy_step_mem_lessdef_sim L step) as (jm2' & E' & step').
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
    econstructor 2; eauto.
    apply IH, E'.

(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
  - econstructor 3 with (x := x); eauto.
    intros ret jm2' z' n' Hargsty Hretty Hn [-> [lev pure]] post.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
    destruct (Post ret jm2' z' _ Hargsty Hretty Hn) as (c' & atex' & safe'); auto.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
    + split; auto.
      destruct L as [Ed Ew].
      unfold juicy_safety.pures_eq in *.
      unfold juicy_safety.pures_sub in *.
      split.
      * repeat rewrite level_juice_level_phi in *.
        congruence.
      * revert pure.
        rewrite Ew.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
        auto.
(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
    + exists c'; split; auto.

(* Goal: @eq (option val) match classify_binarith t1 t2 with | bin_case_i sg => match v0 with | Vundef => @None val | Vint n1 => match v3 with | Vundef => @None val | Vint n2 => sem_int sg n1 n2 | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vlong i => @None val | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_l sg => match v0 with | Vundef => @None val | Vint i => @None val | Vlong n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong n2 => sem_long sg n1 n2 | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | Vfloat f => @None val | Vsingle f => @None val | Vptr b i => @None val end | bin_case_f => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat n2 => sem_float n1 n2 | Vsingle f => @None val | Vptr b i => @None val end | Vsingle f => @None val | Vptr b i => @None val end | bin_case_s => match v0 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n1 => match v3 with | Vundef => @None val | Vint i => @None val | Vlong i => @None val | Vfloat f => @None val | Vsingle n2 => sem_single n1 n2 | Vptr b i => @None val end | Vptr b i => @None val end | bin_default => @None val end (@Some val v) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t2 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
(* Goal: not (@eq classify_cast_cases (classify_cast t1 (binarith_type (classify_binarith t1 t2))) cast_case_void) *)
  - econstructor 4; eauto.
Qed.*)