Require Import VST.floyd.proofauto.
Require Import VST.progs.union.
Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.

Import Memdata.

Lemma decode_float32_int32:
  forall (bl: list memval) (x: float32),
 size_chunk Mfloat32 = Z.of_nat (Datatypes.length bl) ->
 decode_val Mfloat32 bl = Vsingle x ->
 decode_val Mint32 bl = Vint (Float32.to_bits x).
Proof.
(* Goal: forall (bl : list memval) (_ : @eq Z (size_chunk Mfloat32) (Z.of_nat (@Datatypes.length memval bl))), iff (@eq val (decode_val Mfloat32 bl) (Vsingle (Float32.abs x))) (@eq val (decode_val Mint32 bl) (Vint (Int.and (Float32.to_bits x) (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))))))))))) *)
intros.
(* Goal: @eq val (decode_val Mint32 bl) (Vint (Float32.to_bits x)) *)
unfold decode_val,decode_int,rev_if_be in *.
(* Goal: @eq val match proj_bytes bl with | Some bl => Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int bl else bl))) | None => if Archi.ptr64 then Vundef else Val.load_result Mint32 (proj_value Q32 bl) end (Vint (Float32.to_bits x)) *)
destruct (proj_bytes bl) eqn:?H.
(* Goal: @eq val (if Archi.ptr64 then Vundef else Val.load_result Mint32 (proj_value Q32 bl)) (Vint (Float32.to_bits x)) *)
inv H0.
(* Goal: @eq val (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) (Vint (Float32.to_bits (Float32.of_bits (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))))) *)
(* Goal: @eq val (if Archi.ptr64 then Vundef else Val.load_result Mint32 (proj_value Q32 bl)) (Vint (Float32.to_bits x)) *)
rewrite Float32.to_of_bits. auto.
(* Goal: @eq val (if Archi.ptr64 then Vundef else Val.load_result Mint32 (proj_value Q32 bl)) (Vint (Float32.to_bits x)) *)
inv H0.
Qed.


Lemma NOT_decode_int32_float32:
 ~ (forall (bl: list memval) (x: float32),
     size_chunk Mfloat32 = Z.of_nat (Datatypes.length bl) ->
     decode_val Mint32 bl = Vint (Float32.to_bits x) ->
     decode_val Mfloat32 bl = Vsingle x).
Proof.
+
(* Goal: forall _ : @eq nat (@Datatypes.length memval bl) (size_chunk_nat Mfloat32), @eq Prop (and (@eq val (decode_val Mfloat32 bl) v1) (Z.divide (Zpos (xO (xO xH))) (Ptrofs.unsigned i))) (and (@eq val (decode_val Mint32 bl) v2) (Z.divide (Zpos (xO (xO xH))) (Ptrofs.unsigned i))) *)
intro.
(* Goal: False *)
set (x := Float32.zero). (* nothing special about zero, any value would do *)
(* Goal: False *)
set (i := Float32.to_bits x).
(* Goal: False *)
set (bl := [Fragment (Vint i) Q32 3; Fragment (Vint i) Q32 2; Fragment (Vint i) Q32 1; Fragment (Vint i) Q32 0]).
(* Goal: False *)
specialize (H bl x).
(* Goal: False *)
specialize (H (eq_refl _)).
(* Goal: False *)
assert (decode_val Mint32 bl = Vint (Float32.to_bits x)).
(* Goal: @eq val (decode_val Mint32 bl) (Vint (Float32.to_bits x)) *)
(* Goal: False *)
unfold decode_val, bl.
(* Goal: @derives mpred Nveric (@field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _f) (@nil gfield)) (Vsingle (Float32.abs x)) v_u) match @default_val CompSpecs (@nested_field_type CompSpecs (Tunion __135 noattr) (@nil gfield)) with | inl v => @field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _f) (@nil gfield)) v v_u | inr v => @field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _i) (@nil gfield)) v v_u end *)
simpl.
(* Goal: @eq val match (if andb (andb (andb (@proj_sumbool (@eq val (Vint i) (Vint i)) (not (@eq val (Vint i) (Vint i))) (Val.eq (Vint i) (Vint i))) (@proj_sumbool (@eq quantity Q32 Q32) (not (@eq quantity Q32 Q32)) (quantity_eq Q32 Q32))) true) (andb (andb (andb (@proj_sumbool (@eq val (Vint i) (Vint i)) (not (@eq val (Vint i) (Vint i))) (Val.eq (Vint i) (Vint i))) (@proj_sumbool (@eq quantity Q32 Q32) (not (@eq quantity Q32 Q32)) (quantity_eq Q32 Q32))) true) (andb (andb (andb (@proj_sumbool (@eq val (Vint i) (Vint i)) (not (@eq val (Vint i) (Vint i))) (Val.eq (Vint i) (Vint i))) (@proj_sumbool (@eq quantity Q32 Q32) (not (@eq quantity Q32 Q32)) (quantity_eq Q32 Q32))) true) (andb (andb (andb (@proj_sumbool (@eq val (Vint i) (Vint i)) (not (@eq val (Vint i) (Vint i))) (Val.eq (Vint i) (Vint i))) (@proj_sumbool (@eq quantity Q32 Q32) (not (@eq quantity Q32 Q32)) (quantity_eq Q32 Q32))) true) true))) then Vint i else Vundef) with | Vundef => Vundef | Vint n => Vint n | Vlong i => Vundef | Vfloat f => Vundef | Vsingle f => Vundef | Vptr b ofs => Vptr b ofs end (Vint (Float32.to_bits x)) *)
(* Goal: False *)
destruct (Val.eq (Vint i) (Vint i)); [ | congruence].
(* Goal: @eq val match (if andb (andb (andb (@proj_sumbool (@eq val (Vint i) (Vint i)) (not (@eq val (Vint i) (Vint i))) (@left (@eq val (Vint i) (Vint i)) (not (@eq val (Vint i) (Vint i))) e)) (@proj_sumbool (@eq quantity Q32 Q32) (not (@eq quantity Q32 Q32)) (quantity_eq Q32 Q32))) true) (andb (andb (andb (@proj_sumbool (@eq val (Vint i) (Vint i)) (not (@eq val (Vint i) (Vint i))) (@left (@eq val (Vint i) (Vint i)) (not (@eq val (Vint i) (Vint i))) e)) (@proj_sumbool (@eq quantity Q32 Q32) (not (@eq quantity Q32 Q32)) (quantity_eq Q32 Q32))) true) (andb (andb (andb (@proj_sumbool (@eq val (Vint i) (Vint i)) (not (@eq val (Vint i) (Vint i))) (@left (@eq val (Vint i) (Vint i)) (not (@eq val (Vint i) (Vint i))) e)) (@proj_sumbool (@eq quantity Q32 Q32) (not (@eq quantity Q32 Q32)) (quantity_eq Q32 Q32))) true) (andb (andb (andb (@proj_sumbool (@eq val (Vint i) (Vint i)) (not (@eq val (Vint i) (Vint i))) (@left (@eq val (Vint i) (Vint i)) (not (@eq val (Vint i) (Vint i))) e)) (@proj_sumbool (@eq quantity Q32 Q32) (not (@eq quantity Q32 Q32)) (quantity_eq Q32 Q32))) true) true))) then Vint i else Vundef) with | Vundef => Vundef | Vint n => Vint n | Vlong i => Vundef | Vfloat f => Vundef | Vsingle f => Vundef | Vptr b ofs => Vptr b ofs end (Vint (Float32.to_bits x)) *)
(* Goal: False *)
destruct (quantity_eq Q32 Q32); [ | congruence].
(* Goal: @derives mpred Nveric (@field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _f) (@nil gfield)) (Vsingle (Float32.abs x)) v_u) match @default_val CompSpecs (@nested_field_type CompSpecs (Tunion __135 noattr) (@nil gfield)) with | inl v => @field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _f) (@nil gfield)) v v_u | inr v => @field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _i) (@nil gfield)) v v_u end *)
simpl.
(* Goal: @eq Z (size_chunk Mfloat32) (Z.of_nat (size_chunk_nat Mfloat32)) *)
reflexivity.
(* Goal: False *)
specialize (H H0).
(* Goal: False *)
clear - H. subst bl i.
(* Goal: False *)
unfold decode_val in H.
(* Goal: False *)
simpl in H. inversion H.
Qed.


Lemma decode_float32_iff_int32:
  forall (bl: list Memdata.memval) (x: float32),
 Memdata.size_chunk Mfloat32 = Z.of_nat (Datatypes.length bl) ->
 (Memdata.decode_val Mfloat32 bl = Vsingle x <->
   Memdata.decode_val Mint32 bl = Vint (Float32.to_bits x)).
Proof.
Admitted.  (* not provable at present; see https://github.com/AbsInt/CompCert/issues/207
    for a description of how to solve this problem. *)

Definition samerep (ch1 ch2: memory_chunk) (v1 v2: val) :=
  Memdata.size_chunk ch1 = Memdata.size_chunk ch2 /\
  forall bl: list Memdata.memval,
   Memdata.size_chunk ch1 = Z.of_nat (length bl) ->
   (Memdata.decode_val ch1 bl = v1 <-> Memdata.decode_val ch2 bl = v2).

Lemma mapsto_single_int: forall sh v1 v2 p,
  is_single v1 -> is_int I32 Unsigned v2 ->
  samerep Mfloat32 Mint32 v1 v2 ->
  mapsto sh (Tfloat F32 noattr) p v1 = mapsto sh (Tint I32 Unsigned noattr) p v2.
Proof.
(* Goal: forall (bl : list memval) (_ : @eq Z (size_chunk Mfloat32) (Z.of_nat (@Datatypes.length memval bl))), iff (@eq val (decode_val Mfloat32 bl) (Vsingle (Float32.abs x))) (@eq val (decode_val Mint32 bl) (Vint (Int.and (Float32.to_bits x) (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))))))))))) *)
  intros.
(* Goal: @eq mpred (mapsto sh (Tfloat F32 noattr) p v1) (mapsto sh (Tint I32 Unsigned noattr) p v2) *)
  subst.
(* Goal: @eq mpred (mapsto sh (Tfloat F32 noattr) p v1) (mapsto sh (Tint I32 Unsigned noattr) p v2) *)
  unfold mapsto.
(* Goal: @eq val (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) *)
(* Goal: @eq val (if Archi.ptr64 then Vundef else Val.load_result Mint32 (proj_value Q32 bl)) (Vint (Float32.to_bits x)) *)
  simpl. destruct p; auto.
(* Goal: @eq mpred (if readable_share_dec sh then @orp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (is_single v1)) (res_predicates.address_mapsto Mfloat32 v1 sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@eq val v1 Vundef)) (@exp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric val (fun v2' : val => res_predicates.address_mapsto Mfloat32 v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (and (tc_val' (Tfloat F32 noattr) v1) (Z.divide (Zpos (xO (xO xH))) (Ptrofs.unsigned i)))) (res_predicates.nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (Zpos (xO (xO xH))))) (if readable_share_dec sh then @orp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (is_int I32 Unsigned v2)) (res_predicates.address_mapsto Mint32 v2 sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@eq val v2 Vundef)) (@exp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric val (fun v2' : val => res_predicates.address_mapsto Mint32 v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (and (tc_val' (Tint I32 Unsigned noattr) v2) (Z.divide (Zpos (xO (xO xH))) (Ptrofs.unsigned i)))) (res_predicates.nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (Zpos (xO (xO xH))))) *)
  if_tac.
*
(* Goal: @eq mpred (@orp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (is_single v1)) (res_predicates.address_mapsto Mfloat32 v1 sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@eq val v1 Vundef)) (@exp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric val (fun v2' : val => res_predicates.address_mapsto Mfloat32 v2' sh (@pair block Z b (Ptrofs.unsigned i)))))) (@orp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (is_int I32 Unsigned v2)) (res_predicates.address_mapsto Mint32 v2 sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@eq val v2 Vundef)) (@exp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric val (fun v2' : val => res_predicates.address_mapsto Mint32 v2' sh (@pair block Z b (Ptrofs.unsigned i)))))) *)
    rewrite (prop_true_andp _ _ H).
(* Goal: @eq mpred (@orp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (res_predicates.address_mapsto Mfloat32 v1 sh (@pair block Z b (Ptrofs.unsigned i))) (@andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@eq val v1 Vundef)) (@exp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric val (fun v2' : val => res_predicates.address_mapsto Mfloat32 v2' sh (@pair block Z b (Ptrofs.unsigned i)))))) (@orp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (is_int I32 Unsigned v2)) (res_predicates.address_mapsto Mint32 v2 sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@eq val v2 Vundef)) (@exp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric val (fun v2' : val => res_predicates.address_mapsto Mint32 v2' sh (@pair block Z b (Ptrofs.unsigned i)))))) *)
    rewrite (prop_true_andp _ _ H0).
(* Goal: @eq Prop (and (tc_val' (Tfloat F32 noattr) v1) (Z.divide (Zpos (xO (xO xH))) (Ptrofs.unsigned i))) (and (tc_val' (Tint I32 Unsigned noattr) v2) (Z.divide (Zpos (xO (xO xH))) (Ptrofs.unsigned i))) *)
    f_equal.
 +
(* Goal: @eq (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) (res_predicates.address_mapsto Mfloat32 v1 sh (@pair block Z b (Ptrofs.unsigned i))) (res_predicates.address_mapsto Mint32 v2 sh (@pair block Z b (Ptrofs.unsigned i))) *)
    unfold res_predicates.address_mapsto.
(* Goal: @eq (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) (@predicates_hered.exp compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (list memval) (fun bl : list memval => @predicates_hered.andp compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (@predicates_hered.andp compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (@predicates_hered.prop compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (and (@eq nat (@Datatypes.length memval bl) (size_chunk_nat Mfloat32)) (and (@eq val (decode_val Mfloat32 bl) v1) (Z.divide (align_chunk Mfloat32) (@snd block Z (@pair block Z b (Ptrofs.unsigned i))))))) (@predicates_hered.allp compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap address (@res_predicates.jam compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.Join_rmap compcert_rmaps.RML.R.Perm_rmap compcert_rmaps.RML.R.ag_rmap compcert_rmaps.RML.R.Age_rmap address (adr_range (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mfloat32)) (adr_range_dec (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mfloat32)) (fun loc : address => res_predicates.yesat compcert_rmaps.RML.R.NoneP (compcert_rmaps.VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z (@pair block Z b (Ptrofs.unsigned i))))) bl Undef)) sh loc) res_predicates.noat))) res_predicates.noghost)) (@predicates_hered.exp compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (list memval) (fun bl : list memval => @predicates_hered.andp compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (@predicates_hered.andp compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (@predicates_hered.prop compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (and (@eq nat (@Datatypes.length memval bl) (size_chunk_nat Mint32)) (and (@eq val (decode_val Mint32 bl) v2) (Z.divide (align_chunk Mint32) (@snd block Z (@pair block Z b (Ptrofs.unsigned i))))))) (@predicates_hered.allp compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap address (@res_predicates.jam compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.Join_rmap compcert_rmaps.RML.R.Perm_rmap compcert_rmaps.RML.R.ag_rmap compcert_rmaps.RML.R.Age_rmap address (adr_range (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mint32)) (adr_range_dec (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mint32)) (fun loc : address => res_predicates.yesat compcert_rmaps.RML.R.NoneP (compcert_rmaps.VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z (@pair block Z b (Ptrofs.unsigned i))))) bl Undef)) sh loc) res_predicates.noat))) res_predicates.noghost)) *)
    apply predicates_hered.pred_ext'. extensionality phi.
(* Goal: @derives mpred Nveric (@field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _f) (@nil gfield)) (Vsingle (Float32.abs x)) v_u) match @default_val CompSpecs (@nested_field_type CompSpecs (Tunion __135 noattr) (@nil gfield)) with | inl v => @field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _f) (@nil gfield)) v v_u | inr v => @field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _i) (@nil gfield)) v v_u end *)
    simpl. apply exists_ext; intro bl.
(* Goal: @eq Prop (and (tc_val' (Tfloat F32 noattr) v1) (Z.divide (Zpos (xO (xO xH))) (Ptrofs.unsigned i))) (and (tc_val' (Tint I32 Unsigned noattr) v2) (Z.divide (Zpos (xO (xO xH))) (Ptrofs.unsigned i))) *)
    f_equal; f_equal.
(* Goal: @eq val (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) *)
(* Goal: @eq val (if Archi.ptr64 then Vundef else Val.load_result Mint32 (proj_value Q32 bl)) (Vint (Float32.to_bits x)) *)
    apply and_ext'; auto. intro.
(* Goal: @eq Prop (and (@eq val (decode_val Mfloat32 bl) v1) (Z.divide (Zpos (xO (xO xH))) (Ptrofs.unsigned i))) (and (@eq val (decode_val Mint32 bl) v2) (Z.divide (Zpos (xO (xO xH))) (Ptrofs.unsigned i))) *)
    destruct H1 as [H1' H1].
(* Goal: @eq Prop (and (@eq val (decode_val Mfloat32 bl) v1) (Z.divide (Zpos (xO (xO xH))) (Ptrofs.unsigned i))) (and (@eq val (decode_val Mint32 bl) v2) (Z.divide (Zpos (xO (xO xH))) (Ptrofs.unsigned i))) *)
    specialize (H1 bl).
(* Goal: @eq Prop (and (tc_val' (Tfloat F32 noattr) v1) (Z.divide (Zpos (xO (xO xH))) (Ptrofs.unsigned i))) (and (tc_val' (Tint I32 Unsigned noattr) v2) (Z.divide (Zpos (xO (xO xH))) (Ptrofs.unsigned i))) *)
    f_equal.
(* Goal: @eq Prop (forall _ : not (@eq val v1 Vundef), tc_val (Tfloat F32 noattr) v1) (forall _ : not (@eq val v2 Vundef), tc_val (Tint I32 Unsigned noattr) v2) *)
    apply prop_ext.
(* Goal: @eq Z (size_chunk Mfloat32) (Z.of_nat (size_chunk_nat Mfloat32)) *)
    apply H1. rewrite H3. reflexivity.
 +
(* Goal: @derives (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@eq val v2 Vundef)) (res_predicates.address_mapsto Mint32 bl sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@eq val v1 Vundef)) (res_predicates.address_mapsto Mfloat32 bl sh (@pair block Z b (Ptrofs.unsigned i)))) *)
    normalize.
(* Goal: @derives (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@eq val v2 Vundef)) (res_predicates.address_mapsto Mint32 bl sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@eq val v1 Vundef)) (res_predicates.address_mapsto Mfloat32 bl sh (@pair block Z b (Ptrofs.unsigned i)))) *)
    apply pred_ext. normalize. apply exp_left; intro bl. apply exp_right with bl.
(* Goal: @derives (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@eq val v2 Vundef)) (res_predicates.address_mapsto Mint32 bl sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@eq val v1 Vundef)) (res_predicates.address_mapsto Mfloat32 bl sh (@pair block Z b (Ptrofs.unsigned i)))) *)
    normalize.
*
(* Goal: @eq Prop (and (tc_val' (Tfloat F32 noattr) v1) (Z.divide (Zpos (xO (xO xH))) (Ptrofs.unsigned i))) (and (tc_val' (Tint I32 Unsigned noattr) v2) (Z.divide (Zpos (xO (xO xH))) (Ptrofs.unsigned i))) *)
    f_equal. f_equal. f_equal.
(* Goal: @eq Prop (forall _ : not (@eq val v1 Vundef), tc_val (Tfloat F32 noattr) v1) (forall _ : not (@eq val v2 Vundef), tc_val (Tint I32 Unsigned noattr) v2) *)
    unfold tc_val'. apply prop_ext. intuition.
Qed.

Lemma data_at_single_int: forall sh v1 v2 p1 p2,
  is_single v1 -> is_int I32 Unsigned v2 ->
  samerep Mfloat32 Mint32 v1 v2 ->
  readable_share sh ->
  p1 = p2 ->
  data_at sh (Tfloat F32 noattr) v1 p1 = data_at sh (Tint I32 Unsigned noattr) v2 p2.
Proof.
(* Goal: forall (bl : list memval) (_ : @eq Z (size_chunk Mfloat32) (Z.of_nat (@Datatypes.length memval bl))), iff (@eq val (decode_val Mfloat32 bl) (Vsingle (Float32.abs x))) (@eq val (decode_val Mint32 bl) (Vint (Int.and (Float32.to_bits x) (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))))))))))) *)
  intros.
(* Goal: @eq mpred (mapsto sh (Tfloat F32 noattr) p v1) (mapsto sh (Tint I32 Unsigned noattr) p v2) *)
  subst.
(* Goal: @eq (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) (@exp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric val (fun x : val => @andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@eq val v1 Vundef)) (res_predicates.address_mapsto Mfloat32 x sh (@pair block Z b (Ptrofs.unsigned i))))) (@exp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric val (fun x : val => @andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@eq val v2 Vundef)) (res_predicates.address_mapsto Mint32 x sh (@pair block Z b (Ptrofs.unsigned i))))) *)
  apply pred_ext.
  + entailer!.
(* Goal: @eq val (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) *)
(* Goal: @eq val (if Archi.ptr64 then Vundef else Val.load_result Mint32 (proj_value Q32 bl)) (Vint (Float32.to_bits x)) *)
    erewrite <- mapsto_data_at'; auto.
(* Goal: @eq val (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) *)
(* Goal: @eq val (if Archi.ptr64 then Vundef else Val.load_result Mint32 (proj_value Q32 bl)) (Vint (Float32.to_bits x)) *)
    erewrite <- mapsto_data_at'; auto.
(* Goal: @eq val (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) *)
(* Goal: @eq val (if Archi.ptr64 then Vundef else Val.load_result Mint32 (proj_value Q32 bl)) (Vint (Float32.to_bits x)) *)
    - erewrite mapsto_single_int; try apply derives_refl; auto.
    - destruct H3 as [? [? [? [? ?]]]].
(* Goal: @eq val (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) *)
(* Goal: @eq val (if Archi.ptr64 then Vundef else Val.load_result Mint32 (proj_value Q32 bl)) (Vint (Float32.to_bits x)) *)
      split; [| split; [| split; [| split]]]; auto.
(* Goal: @eq val (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) *)
(* Goal: @eq val (if Archi.ptr64 then Vundef else Val.load_result Mint32 (proj_value Q32 bl)) (Vint (Float32.to_bits x)) *)
      destruct p2; auto.
      inv H7. econstructor.
(* Goal: @eq Z (size_chunk Mfloat32) (Z.of_nat (size_chunk_nat Mfloat32)) *)
      * reflexivity.
      * inv H9.
        exact H10.
  + entailer!.
(* Goal: @eq val (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) *)
(* Goal: @eq val (if Archi.ptr64 then Vundef else Val.load_result Mint32 (proj_value Q32 bl)) (Vint (Float32.to_bits x)) *)
    erewrite <- mapsto_data_at'; auto.
(* Goal: @eq val (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) *)
(* Goal: @eq val (if Archi.ptr64 then Vundef else Val.load_result Mint32 (proj_value Q32 bl)) (Vint (Float32.to_bits x)) *)
    erewrite <- mapsto_data_at'; auto.
(* Goal: @eq val (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) *)
(* Goal: @eq val (if Archi.ptr64 then Vundef else Val.load_result Mint32 (proj_value Q32 bl)) (Vint (Float32.to_bits x)) *)
    - erewrite mapsto_single_int; try apply derives_refl; auto.
    - destruct H3 as [? [? [? [? ?]]]].
(* Goal: @eq val (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) *)
(* Goal: @eq val (if Archi.ptr64 then Vundef else Val.load_result Mint32 (proj_value Q32 bl)) (Vint (Float32.to_bits x)) *)
      split; [| split; [| split; [| split]]]; auto.
(* Goal: @eq val (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) *)
(* Goal: @eq val (if Archi.ptr64 then Vundef else Val.load_result Mint32 (proj_value Q32 bl)) (Vint (Float32.to_bits x)) *)
      destruct p2; auto.
      inv H7. econstructor.
(* Goal: @eq Z (size_chunk Mfloat32) (Z.of_nat (size_chunk_nat Mfloat32)) *)
      * reflexivity.
      * inv H9.
        exact H10.
Qed.

Lemma float32_to_bits_abs':
 forall x,
  Fappli_IEEE_bits.bits_of_b32 (Fappli_IEEE.Babs 24 128 (fun _ pl => (false,pl)) x) =
   Z.land (Fappli_IEEE_bits.bits_of_b32 x) (2 ^ 31 - 1).
Proof.
(* Goal: forall (bl : list memval) (_ : @eq Z (size_chunk Mfloat32) (Z.of_nat (@Datatypes.length memval bl))), iff (@eq val (decode_val Mfloat32 bl) (Vsingle (Float32.abs x))) (@eq val (decode_val Mint32 bl) (Vint (Int.and (Float32.to_bits x) (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))))))))))) *)
intros.
(* Goal: @eq Z (size_chunk Mfloat32) (Z.of_nat (size_chunk_nat Mfloat32)) *)
destruct x,b; try reflexivity.
* (* nan sign=true *)
(* Goal: @derives mpred Nveric (@field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _f) (@nil gfield)) (Vsingle (Float32.abs x)) v_u) match @default_val CompSpecs (@nested_field_type CompSpecs (Tunion __135 noattr) (@nil gfield)) with | inl v => @field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _f) (@nil gfield)) v v_u | inr v => @field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _i) (@nil gfield)) v v_u end *)
simpl.
destruct n.
unfold Fappli_IEEE_bits.join_bits.
change (0+255) with 255.
admit.
* (* nan sign=false*)
admit.
* (* finite sign=true *)
unfold Fappli_IEEE_bits.bits_of_b32, Fappli_IEEE.Babs, Fappli_IEEE_bits.bits_of_binary_float.
Admitted.

Lemma float32_to_bits_abs: 
  forall x, Float32.to_bits (Float32.abs x) = Int.and (Float32.to_bits x) (Int.repr (2 ^ 31 - 1)).
Proof.
(* Goal: forall (bl : list memval) (_ : @eq Z (size_chunk Mfloat32) (Z.of_nat (@Datatypes.length memval bl))), iff (@eq val (decode_val Mfloat32 bl) (Vsingle (Float32.abs x))) (@eq val (decode_val Mint32 bl) (Vint (Int.and (Float32.to_bits x) (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))))))))))) *)
intros.
Transparent Float32.to_bits.
unfold Float32.to_bits.
Opaque Float32.to_bits.
rewrite and_repr.
(* Goal: @eq Prop (and (tc_val' (Tfloat F32 noattr) v1) (Z.divide (Zpos (xO (xO xH))) (Ptrofs.unsigned i))) (and (tc_val' (Tint I32 Unsigned noattr) v2) (Z.divide (Zpos (xO (xO xH))) (Ptrofs.unsigned i))) *)
f_equal.
Transparent Float32.abs.
unfold Float32.abs.
Opaque Float32.abs.
unfold Float32.abs_pl.
apply float32_to_bits_abs'.
Qed.

Lemma fabs_float32_lemma:
  forall x: float32,
  exists y: int,
  samerep Mfloat32 Mint32 (Vsingle x) (Vint y) /\
  samerep Mfloat32 Mint32 (Vsingle (Float32.abs x)) (Vint (Int.and y (Int.repr 2147483647))).
Proof.
(* Goal: forall (bl : list memval) (_ : @eq Z (size_chunk Mfloat32) (Z.of_nat (@Datatypes.length memval bl))), iff (@eq val (decode_val Mfloat32 bl) (Vsingle (Float32.abs x))) (@eq val (decode_val Mint32 bl) (Vint (Int.and (Float32.to_bits x) (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))))))))))) *)
intros.
(* Goal: @ex Int.int (fun y : Int.int => and (samerep Mfloat32 Mint32 (Vsingle x) (Vint y)) (samerep Mfloat32 Mint32 (Vsingle (Float32.abs x)) (Vint (Int.and y (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))))))))))) *)
exists (Float32.to_bits x).
(* Goal: and (samerep Mfloat32 Mint32 (Vsingle x) (Vint (Float32.to_bits x))) (samerep Mfloat32 Mint32 (Vsingle (Float32.abs x)) (Vint (Int.and (Float32.to_bits x) (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))))))))))) *)
split.
*
(* Goal: samerep Mfloat32 Mint32 (Vsingle (Float32.abs x)) (Vint (Int.and (Float32.to_bits x) (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))))))))) *)
split; [ reflexivity | ].
(* Goal: forall (bl : list memval) (_ : @eq Z (size_chunk Mfloat32) (Z.of_nat (@Datatypes.length memval bl))), iff (@eq val (decode_val Mfloat32 bl) (Vsingle (Float32.abs x))) (@eq val (decode_val Mint32 bl) (Vint (Int.and (Float32.to_bits x) (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))))))))))) *)
intros.
(* Goal: @eq val (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) *)
(* Goal: @eq val (if Archi.ptr64 then Vundef else Val.load_result Mint32 (proj_value Q32 bl)) (Vint (Float32.to_bits x)) *)
apply decode_float32_iff_int32; auto.
*
(* Goal: samerep Mfloat32 Mint32 (Vsingle (Float32.abs x)) (Vint (Int.and (Float32.to_bits x) (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))))))))) *)
split; [ reflexivity | ].
(* Goal: forall (bl : list memval) (_ : @eq Z (size_chunk Mfloat32) (Z.of_nat (@Datatypes.length memval bl))), iff (@eq val (decode_val Mfloat32 bl) (Vsingle (Float32.abs x))) (@eq val (decode_val Mint32 bl) (Vint (Int.and (Float32.to_bits x) (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))))))))))) *)
intros.
rewrite <- float32_to_bits_abs.
(* Goal: @eq val (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) *)
(* Goal: @eq val (if Archi.ptr64 then Vundef else Val.load_result Mint32 (proj_value Q32 bl)) (Vint (Float32.to_bits x)) *)
apply decode_float32_iff_int32; auto.
Qed.

Module Single.

Definition fabs_single_spec :=
 DECLARE _fabs_single
 WITH x: float32
 PRE [ _x OF Tfloat F32 noattr]
   PROP() LOCAL(temp _x (Vsingle x)) SEP()
 POST [ Tfloat F32 noattr ]
   PROP() LOCAL (temp ret_temp (Vsingle (Float32.abs x))) SEP().

Definition Gprog : funspecs :=
    ltac:(with_library prog [ fabs_single_spec ]).

Lemma union_field_address: forall id,
  composites = (Composite id Union ((_f, tfloat) :: (_i, tuint) :: nil) noattr :: nil) ->
 forall p,
  field_address (Tunion id noattr) [UnionField _f] p = field_address (Tunion id noattr) [UnionField _i] p.
Proof.
(* Goal: forall (bl : list memval) (_ : @eq Z (size_chunk Mfloat32) (Z.of_nat (@Datatypes.length memval bl))), iff (@eq val (decode_val Mfloat32 bl) (Vsingle (Float32.abs x))) (@eq val (decode_val Mint32 bl) (Vint (Int.and (Float32.to_bits x) (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))))))))))) *)
  intros.
(* Goal: False *)
  inversion H.
  assert (field_compatible (Tunion id noattr) [UnionField _f] p 
               <-> field_compatible (Tunion id noattr) [UnionField _i] p).
(* Goal: @eq val (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) *)
(* Goal: @eq val (if Archi.ptr64 then Vundef else Val.load_result Mint32 (proj_value Q32 bl)) (Vint (Float32.to_bits x)) *)
2: subst id;  unfold field_address; if_tac; if_tac; auto; tauto.
subst id.
(* Goal: @derives mpred Nveric (@field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _f) (@nil gfield)) (Vsingle (Float32.abs x)) v_u) match @default_val CompSpecs (@nested_field_type CompSpecs (Tunion __135 noattr) (@nil gfield)) with | inl v => @field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _f) (@nil gfield)) v v_u | inr v => @field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _i) (@nil gfield)) v v_u end *)
  rewrite !field_compatible_cons; simpl.
(* Goal: @derives mpred Nveric (@field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _f) (@nil gfield)) (Vsingle (Float32.abs x)) v_u) match @default_val CompSpecs (@nested_field_type CompSpecs (Tunion __135 noattr) (@nil gfield)) with | inl v => @field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _f) (@nil gfield)) v v_u | inr v => @field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _i) (@nil gfield)) v v_u end *)
  unfold in_members; simpl.
(* Goal: @eq val (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) (Vint (Int.repr (int_of_bytes (if Archi.big_endian then @rev Byte.int l else l)))) *)
(* Goal: @eq val (if Archi.ptr64 then Vundef else Val.load_result Mint32 (proj_value Q32 bl)) (Vint (Float32.to_bits x)) *)
  tauto.
Qed.

Lemma body_fabs_single: semax_body Vprog Gprog f_fabs_single fabs_single_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_fabs_single fabs_single_spec *)
start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vsingle (Float32.abs x))) (@cons localdef (temp _t'2 (Vint y)) (@cons localdef (lvar _u (Tunion __135 noattr) v_u) (@cons localdef (temp _x (Vsingle x)) (@nil localdef))))) (SEPx (@cons mpred (@field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _f) (@nil gfield)) (Vsingle (Float32.abs x)) v_u) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _t'1 tfloat))) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (lvar _u (Tunion __135 noattr) v_u) (@cons localdef (temp _x (Vsingle x)) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (Tunion __135 noattr) (@inl val val (Vsingle x)) v_u) (@nil mpred))))) (Ssequence (Ssequence (Sset _t'2 (Efield (Evar _u (Tunion __135 noattr)) _i tuint)) (Sassign (Efield (Evar _u (Tunion __135 noattr)) _i tuint) (Ebinop Oand (Etempvar _t'2 tuint) (Econst_int (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))))))) tint) tuint))) MORE_COMMANDS) POSTCONDITION *)
destruct (fabs_float32_lemma x) as [y [H3 H4]].
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (lvar _u (Tunion __135 noattr) v_u) (@cons localdef (temp _x (Vsingle x)) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (Tunion __135 noattr) (@inl val val (Vsingle x)) v_u) (@nil mpred))))) (Ssequence (Ssequence (Sset _t'2 (Efield (Evar _u (Tunion __135 noattr)) _i tuint)) (Sassign (Efield (Evar _u (Tunion __135 noattr)) _i tuint) (Ebinop Oand (Etempvar _t'2 tuint) (Econst_int (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))))))) tint) tuint))) MORE_COMMANDS) POSTCONDITION *)
unfold_data_at (data_at _ _ _ _).
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (Vint y)) (@cons localdef (lvar _u (Tunion __135 noattr) v_u) (@cons localdef (temp _x (Vsingle x)) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _i) (@nil gfield)) (Vint (Int.and y (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))))))))) v_u) (@nil mpred))))) (Ssequence (Sset _t'1 (Efield (Evar _u (Tunion __135 noattr)) _f tfloat)) MORE_COMMANDS) POSTCONDITION *)
rewrite field_at_data_at.
erewrite data_at_single_int with (v2:= Vint y);
 [ | apply I | apply I | exact H3 | auto | apply (union_field_address _ (eq_refl _))].
match goal with |- context [Tunion ?structid] =>
 change (Tint I32 Unsigned noattr) with (nested_field_type (Tunion structid noattr) [UnionField _i])
end.
rewrite <- field_at_data_at.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vsingle (Float32.abs x))) (@cons localdef (temp _t'2 (Vint y)) (@cons localdef (lvar _u (Tunion __135 noattr) v_u) (@cons localdef (temp _x (Vsingle x)) (@nil localdef))))) (SEPx (@cons mpred (@field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _f) (@nil gfield)) (Vsingle (Float32.abs x)) v_u) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _t'1 tfloat))) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vsingle (Float32.abs x))) (@cons localdef (temp _t'2 (Vint y)) (@cons localdef (lvar _u (Tunion __135 noattr) v_u) (@cons localdef (temp _x (Vsingle x)) (@nil localdef))))) (SEPx (@cons mpred (@field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _f) (@nil gfield)) (Vsingle (Float32.abs x)) v_u) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _t'1 tfloat))) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (Vint y)) (@cons localdef (lvar _u (Tunion __135 noattr) v_u) (@cons localdef (temp _x (Vsingle x)) (@nil localdef)))) (SEPx (@cons mpred (@field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _i) (@nil gfield)) (Vint (Int.and y (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))))))))) v_u) (@nil mpred))))) (Ssequence (Sset _t'1 (Efield (Evar _u (Tunion __135 noattr)) _f tfloat)) MORE_COMMANDS) POSTCONDITION *)
rewrite field_at_data_at.
erewrite <- data_at_single_int with (v1:= Vsingle (Float32.abs x));
    [| apply I | apply I | exact H4 | auto | apply (union_field_address _ (eq_refl _))].
match goal with |- context [Tunion ?structid] =>
  change (Tfloat F32 noattr) with (nested_field_type (Tunion structid noattr) [UnionField _f])
end.
rewrite <- field_at_data_at.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vsingle (Float32.abs x))) (@cons localdef (temp _t'2 (Vint y)) (@cons localdef (lvar _u (Tunion __135 noattr) v_u) (@cons localdef (temp _x (Vsingle x)) (@nil localdef))))) (SEPx (@cons mpred (@field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _f) (@nil gfield)) (Vsingle (Float32.abs x)) v_u) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _t'1 tfloat))) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vsingle (Float32.abs x))) (@cons localdef (temp _t'2 (Vint y)) (@cons localdef (lvar _u (Tunion __135 noattr) v_u) (@cons localdef (temp _x (Vsingle x)) (@nil localdef))))) (SEPx (@cons mpred (@field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _f) (@nil gfield)) (Vsingle (Float32.abs x)) v_u) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _t'1 tfloat))) POSTCONDITION *)
forward.
(* Goal: @derives mpred Nveric (@field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _f) (@nil gfield)) (Vsingle (Float32.abs x)) v_u) (@data_at_ CompSpecs Tsh (Tunion __135 noattr) v_u) *)
unfold_data_at (data_at_ _ _ _).
(* Goal: @derives mpred Nveric (@field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _f) (@nil gfield)) (Vsingle (Float32.abs x)) v_u) match @default_val CompSpecs (@nested_field_type CompSpecs (Tunion __135 noattr) (@nil gfield)) with | inl v => @field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _f) (@nil gfield)) v v_u | inr v => @field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _i) (@nil gfield)) v v_u end *)
simpl.
(* Goal: @derives mpred Nveric (@field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _f) (@nil gfield)) (Vsingle (Float32.abs x)) v_u) (@field_at CompSpecs Tsh (Tunion __135 noattr) (@cons gfield (UnionField _f) (@nil gfield)) Vundef v_u) *)
entailer!.
Qed.

End Single.

Module Float.

 (* This experiment shows what kind of error message you get
   if you put the wrong LOCAL precondition.
   In fact, Vfloat x is wrong, leading to an unsatisfying precondition,
   it must be Vsingle. *)

Definition fabs_single_spec :=
 DECLARE _fabs_single
 WITH x: float
 PRE [ _x OF Tfloat F32 noattr]
   PROP() LOCAL(temp _x (Vfloat x)) SEP()
 POST [ Tfloat F32 noattr ]
   PROP() LOCAL (temp ret_temp (Vfloat (Float.abs x))) SEP().

Definition Gprog : funspecs :=
    ltac:(with_library prog [ fabs_single_spec ]).

Lemma body_fabs_single: semax_body Vprog Gprog f_fabs_single fabs_single_spec.
Proof.
try (start_function; fail 99).
Abort.

End Float.
