Require Import VST.floyd.base2.
Require Import VST.floyd.functional_base.
Require Import VST.floyd.client_lemmas.
Require Import VST.floyd.go_lower.
Require Import VST.floyd.reptype_lemmas.
Require Import VST.floyd.data_at_rec_lemmas.
Require Import VST.floyd.field_at VST.floyd.nested_field_lemmas.

Local Open Scope logic.

Lemma ptrofs_of_ints_unfold: 
  forall x, Ptrofs.of_ints x = Ptrofs.repr (Int.signed x).
(* Goal: @eq Byte.int (@nth Byte.int O (@cons Byte.int Byte.zero (@nil Byte.int)) Inhabitant_byte) Byte.zero *)
(* Goal: @eq Byte.int (@nth Byte.int (S n) (@cons Byte.int Byte.zero (@nil Byte.int)) Inhabitant_byte) Byte.zero *)
Proof. reflexivity. Qed.
Hint Rewrite ptrofs_of_ints_unfold : norm.

Lemma ptrofs_of_intu_unfold: 
  forall x, Ptrofs.of_intu x = Ptrofs.repr (Int.unsigned x).
(* Goal: @eq Byte.int (@nth Byte.int O (@cons Byte.int Byte.zero (@nil Byte.int)) Inhabitant_byte) Byte.zero *)
(* Goal: @eq Byte.int (@nth Byte.int (S n) (@cons Byte.int Byte.zero (@nil Byte.int)) Inhabitant_byte) Byte.zero *)
Proof. reflexivity. Qed.
Hint Rewrite ptrofs_of_intu_unfold : norm.

Lemma isptr_force_val_sem_cast_neutral :
  forall p, isptr p -> isptr (force_val (sem_cast_pointer p)).
Proof.
(* Goal: forall i : Z, @eq Byte.int (@Znth Byte.int Inhabitant_byte i (@cons Byte.int Byte.zero (@nil Byte.int))) Byte.zero *)
intros. destruct p; try contradiction; apply I.
Qed.
Hint Resolve isptr_force_val_sem_cast_neutral : norm.

Lemma FF_local_facts: forall {A}{NA: NatDed A}, (FF:A) |-- !!False.
Proof. intros. apply FF_left. Qed.
Hint Resolve @FF_local_facts: saturate_local.

(*
(*** Omega stuff ***)

Ltac omegable' A :=
lazymatch A with
| @eq nat _ _ => idtac
| @eq Z _ _ => idtac
| Z.lt _ _ => idtac
| Z.le _ _ => idtac
| Z.gt _ _ => idtac
| Z.ge _ _ => idtac
| Peano.lt _ _ => idtac
| Peano.le _ _ => idtac
| Peano.gt _ _ => idtac
| Peano.ge _ _ => idtac
| ~ ?A => omegable' A
| ?A /\ ?B => omegable' A; omegable' B
end.

Ltac omegable := match goal with |- ?A => omegable' A end.

Ltac  add_nonredundant' F T G :=
   match G with
        | T -> _ => fail 1
        | _ -> ?G' => add_nonredundant' F T G' || fail 1
        | _ => generalize F
  end.

Ltac  add_nonredundant F :=
 match type of F with ?T =>
   match goal with |- ?G => add_nonredundant' F T G
   end
 end.

Lemma omega_aux: forall {A} (B C: A),
   B=C -> forall D, (B=C->D) -> D.
Proof. intuition. Qed.

Ltac is_const A :=
 match A with
 | Z0 => idtac
 | Zpos ?B => is_const B
 | Zneg ?B => is_const B
 | xH => idtac
 | xI ?B => is_const B
 | xO ?B => is_const B
 | O => idtac
 | S ?B => is_const B
 end.

Ltac simpl_const :=
  match goal with
   | |- context [Z.of_nat ?A] =>
     is_const A;
     let H := fresh in set (H:= Z.of_nat A); simpl in H; unfold H; clear H
   | |- context [Z.to_nat ?A] =>
     is_const A;
     let H := fresh in set (H:= Z.to_nat A); simpl in H; unfold H; clear H
  end.

Ltac Omega' L :=
repeat match goal with
 | H: @eq Z _ _ |- _ => revert H
 | H: @eq nat _ _ |- _ => revert H
 | H: @neq Z _ _ |- _ => revert H
 | H: not (@eq Z _ _) |- _ => revert H
 | H: @neq nat _ _ |- _ => revert H
 | H: not (@eq nat _ _) |- _ => revert H
 | H: _ <> _ |- _ => revert H
 | H: Z.lt _ _ |- _ => revert H
 | H: Z.le _ _ |- _ => revert H
 | H: Z.gt _ _ |- _ => revert H
 | H: Z.ge _ _ |- _ => revert H
 | H: Z.le _ _ /\ Z.le _ _ |- _ => revert H
 | H: Z.lt _ _ /\ Z.le _ _ |- _ => revert H
 | H: Z.le _ _ /\ Z.lt _ _ |- _ => revert H
 | H: lt _ _ |- _ => revert H
 | H: le _ _ |- _ => revert H
 | H: gt _ _ |- _ => revert H
 | H: ge _ _ |- _ => revert H
 | H: le _ _ /\ le _ _ |- _ => revert H
 | H: lt _ _ /\ le _ _ |- _ => revert H
 | H: le _ _ /\ lt _ _ |- _ => revert H
 | H := ?A : Z |- _ => apply (omega_aux H A (eq_refl _)); clearbody H
 | H := ?A : nat |- _ => apply (omega_aux H A (eq_refl _)); clearbody H
 | H: _ |- _ => clear H
 end;
 clear;
 abstract (
   repeat (L || simpl_const);
   intros; omega).

Ltac Omega'' L :=
  match goal with
  | |- (_ >= _)%nat => apply <- Nat2Z.inj_ge
  | |- (_ > _)%nat => apply <- Nat2Z.inj_gt
  | |- (_ <= _)%nat => apply <- Nat2Z.inj_le
  | |- (_ < _)%nat => apply <- Nat2Z.inj_lt
  | |- @eq nat _ _ => apply Nat2Z.inj
  | |- _ => idtac
  end;
 repeat first
     [ simpl_const
     | rewrite Nat2Z.id
     | rewrite Nat2Z.inj_add
     | rewrite Nat2Z.inj_mul
     | rewrite Z2Nat.id by Omega'' L
     | rewrite Nat2Z.inj_sub by Omega'' L
     | rewrite Z2Nat.inj_sub by Omega'' L
     | rewrite Z2Nat.inj_add by Omega'' L
     ];
  Omega' L.

Tactic Notation "Omega" tactic(L) := (omegable; Omega'' L).

Ltac helper1 := 
  pose_standard_const_equations;
 match goal with
   | |- context [Zlength ?A] => add_nonredundant (Zlength_correct A)
 end.

Ltac Omega0 := Omega (solve [ helper1 ]).

(*** End of Omega stuff *)
*)

Ltac simpl_compare :=
 match goal with
 | H: Vint _ = _ |- _ =>
         revert H; simpl_compare; intro H;
         try (simpl in H; apply Vint_inj in H;
               match type of H with ?a = ?b =>
                  first [safe_subst a | safe_subst b | idtac]
               end)
 | H: typed_true _ _ |- _ =>
         simpl in H; revert H; simpl_compare; intro H;
         first [apply typed_true_ptr in H
                 | apply typed_true_of_bool in H;
                   first [apply (int_cmp_repr Clt) in H;
                            [ | rep_omega ..]; simpl in H
                          | apply (int_cmp_repr Ceq) in H;
                             [ | rep_omega ..]; simpl in H
                          | idtac ]
                 | discriminate H
                 | idtac ]
 | H: typed_false _ _ |- _ =>
         simpl in H; revert H; simpl_compare; intro H;
         first [ apply typed_false_ptr in H
                | apply typed_false_of_bool in H;
                   first [apply (int_cmp_repr' Clt) in H;
                            [ | rep_omega ..]; simpl in H
                          | apply (int_cmp_repr' Ceq) in H;
                            [ | rep_omega ..]; simpl in H
                          | idtac]
                 | discriminate H
                 | idtac ]
 | H : Int.lt _ _ = false |- _ =>
         revert H; simpl_compare; intro H;
         try (apply (int_cmp_repr' Clt) in H ;
                    [ | rep_omega ..]; simpl in H)
 | H : Int.lt _ _ = true |- _ =>
         revert H; simpl_compare;  intro H;
         try (apply (int_cmp_repr Clt) in H ;
                    [ | rep_omega ..]; simpl in H)
 | H : Int.eq _ _ = false |- _ =>
         revert H; simpl_compare;  intro H;
         try (apply (int_cmp_repr' Ceq) in H ;
                    [ | rep_omega ..]; simpl in H)
 | H : Int.eq _ _ = true |- _ =>
         revert H; simpl_compare;  intro H;
         try (apply (int_cmp_repr Ceq) in H ;
                    [ | rep_omega ..]; simpl in H)
 | |- _ => idtac
end.

Lemma prop_and_same_derives {A}{NA: NatDed A}:
  forall P Q, Q |-- !! P   ->   Q |-- !!P && Q.
Proof.
(* Goal: forall i : Z, @eq Byte.int (@Znth Byte.int Inhabitant_byte i (@cons Byte.int Byte.zero (@nil Byte.int))) Byte.zero *)
intros. apply andp_right; auto.
Qed.

Arguments denote_tc_isptr v / .
Arguments denote_tc_iszero !v .
Arguments denote_tc_nonzero !v .
Arguments denote_tc_igt i !v .
Arguments denote_tc_Zge z !v .
Arguments denote_tc_Zle z !v .
Arguments denote_tc_samebase !v1 !v2 .
Arguments denote_tc_nodivover !v1 !v2 .
Arguments denote_tc_initialized id ty rho / .
Arguments denote_tc_nosignedover op v1 v2 / .
Ltac simpl_denote_tc :=
 simpl denote_tc_isptr;
 simpl denote_tc_iszero;
 simpl denote_tc_nonzero;
 simpl denote_tc_igt;
 simpl denote_tc_Zge;
 simpl denote_tc_Zle;
 simpl denote_tc_samebase;
 simpl denote_tc_nodivover;
 simpl denote_tc_initialized;
 simpl denote_tc_nosignedover.

Lemma denote_tc_test_eq_split:
  forall P x y,
    P |-- valid_pointer x ->
    P |-- valid_pointer y ->
    P |-- denote_tc_test_eq x y.
Proof.
(* Goal: forall i : Z, @eq Byte.int (@Znth Byte.int Inhabitant_byte i (@cons Byte.int Byte.zero (@nil Byte.int))) Byte.zero *)
 intros.
(* Goal: @derives mpred Nveric P (denote_tc_test_eq x y) *)
 eapply derives_trans with (valid_pointer x && valid_pointer y).
(* Goal: @derives A NA Q (@andp A NA (@prop A NA P) Q) *)
 apply andp_right; auto.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (valid_pointer x) (valid_pointer y)) (denote_tc_test_eq x y) *)
 clear H H0.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (valid_pointer x) (valid_pointer y)) (denote_tc_test_eq x y) *)
 unfold denote_tc_test_eq, weak_valid_pointer.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (valid_pointer x) (valid_pointer y)) match x with | Vundef => @FF mpred Nveric | Vint i => match y with | Vundef => @FF mpred Nveric | Vint j => if Archi.ptr64 then @FF mpred Nveric else @andp mpred Nveric (@prop mpred Nveric (@eq Int.int i Int.zero)) (@prop mpred Nveric (@eq Int.int j Int.zero)) | Vlong i0 => @FF mpred Nveric | Vfloat f => @FF mpred Nveric | Vsingle f => @FF mpred Nveric | Vptr b i0 => if Archi.ptr64 then @FF mpred Nveric else @andp mpred Nveric (@prop mpred Nveric (@eq Int.int i Int.zero)) (@predicates_hered.orp compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (valid_pointer' y Z0) (valid_pointer' y (Zneg xH))) end | Vlong i => match y with | Vundef => @FF mpred Nveric | Vint i0 => @FF mpred Nveric | Vlong j => if Archi.ptr64 then @andp mpred Nveric (@prop mpred Nveric (@eq Int64.int i Int64.zero)) (@prop mpred Nveric (@eq Int64.int j Int64.zero)) else @FF mpred Nveric | Vfloat f => @FF mpred Nveric | Vsingle f => @FF mpred Nveric | Vptr b i0 => if Archi.ptr64 then @andp mpred Nveric (@prop mpred Nveric (@eq Int64.int i Int64.zero)) (@predicates_hered.orp compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (valid_pointer' y Z0) (valid_pointer' y (Zneg xH))) else @FF mpred Nveric end | Vfloat f => @FF mpred Nveric | Vsingle f => @FF mpred Nveric | Vptr b i0 => match y with | Vundef => @FF mpred Nveric | Vint i => if Archi.ptr64 then @FF mpred Nveric else @andp mpred Nveric (@prop mpred Nveric (@eq Int.int i Int.zero)) (@predicates_hered.orp compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (valid_pointer' x Z0) (valid_pointer' x (Zneg xH))) | Vlong i => if Archi.ptr64 then @andp mpred Nveric (@prop mpred Nveric (@eq Int64.int i Int64.zero)) (@predicates_hered.orp compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (valid_pointer' x Z0) (valid_pointer' x (Zneg xH))) else @FF mpred Nveric | Vfloat f => @FF mpred Nveric | Vsingle f => @FF mpred Nveric | Vptr b0 i => test_eq_ptrs x y end end *)
change predicates_hered.orp with orp.
 destruct x; try (apply andp_left1; apply @FF_left); try apply @TT_right;
 destruct y; try (apply andp_left2; apply @FF_left); try apply @TT_right.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (valid_pointer (Vint i0)) (valid_pointer (Vptr b i))) (if Archi.ptr64 then @FF mpred Nveric else @andp mpred Nveric (@prop mpred Nveric (@eq Int.int i0 Int.zero)) (@orp mpred Nveric (valid_pointer' (Vptr b i) Z0) (valid_pointer' (Vptr b i) (Zneg xH)))) *)
(* Goal: @derives mpred Nveric (@andp mpred Nveric (valid_pointer (Vptr b i)) (valid_pointer (Vptr b0 i0))) (test_eq_ptrs (Vptr b i) (Vptr b0 i0)) *)
 apply andp_derives; try apply derives_refl.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (valid_pointer (Vint i0)) (valid_pointer (Vptr b i))) (if Archi.ptr64 then @FF mpred Nveric else @andp mpred Nveric (@prop mpred Nveric (@eq Int.int i0 Int.zero)) (@orp mpred Nveric (valid_pointer' (Vptr b i) Z0) (valid_pointer' (Vptr b i) (Zneg xH)))) *)
(* Goal: @derives mpred Nveric (@andp mpred Nveric (valid_pointer (Vptr b i)) (valid_pointer (Vptr b0 i0))) (test_eq_ptrs (Vptr b i) (Vptr b0 i0)) *)
 apply andp_derives; try apply derives_refl.
(* Goal: @derives mpred Nveric (valid_pointer (Vptr b i)) (@orp mpred Nveric (valid_pointer' (Vptr b i) Z0) (valid_pointer' (Vptr b i) (Zneg xH))) *)
(* Goal: @derives mpred Nveric (@andp mpred Nveric (valid_pointer (Vptr b i)) (valid_pointer (Vptr b0 i0))) (test_eq_ptrs (Vptr b i) (Vptr b0 i0)) *)
 apply orp_right1. apply derives_refl.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (valid_pointer (Vptr b i)) (valid_pointer (Vint i0))) (if Archi.ptr64 then @FF mpred Nveric else @andp mpred Nveric (@prop mpred Nveric (@eq Int.int i0 Int.zero)) (@orp mpred Nveric (valid_pointer' (Vptr b i) Z0) (valid_pointer' (Vptr b i) (Zneg xH)))) *)
(* Goal: @derives mpred Nveric (@andp mpred Nveric (valid_pointer (Vptr b i)) (valid_pointer (Vptr b0 i0))) (test_eq_ptrs (Vptr b i) (Vptr b0 i0)) *)
 rewrite andp_comm.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (valid_pointer (Vint i0)) (valid_pointer (Vptr b i))) (if Archi.ptr64 then @FF mpred Nveric else @andp mpred Nveric (@prop mpred Nveric (@eq Int.int i0 Int.zero)) (@orp mpred Nveric (valid_pointer' (Vptr b i) Z0) (valid_pointer' (Vptr b i) (Zneg xH)))) *)
(* Goal: @derives mpred Nveric (@andp mpred Nveric (valid_pointer (Vptr b i)) (valid_pointer (Vptr b0 i0))) (test_eq_ptrs (Vptr b i) (Vptr b0 i0)) *)
 apply andp_derives; try apply derives_refl.
(* Goal: @derives mpred Nveric (valid_pointer (Vptr b i)) (@orp mpred Nveric (valid_pointer' (Vptr b i) Z0) (valid_pointer' (Vptr b i) (Zneg xH))) *)
(* Goal: @derives mpred Nveric (@andp mpred Nveric (valid_pointer (Vptr b i)) (valid_pointer (Vptr b0 i0))) (test_eq_ptrs (Vptr b i) (Vptr b0 i0)) *)
 apply orp_right1. apply derives_refl.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (valid_pointer (Vptr b i)) (valid_pointer (Vptr b0 i0))) (test_eq_ptrs (Vptr b i) (Vptr b0 i0)) *)
 unfold test_eq_ptrs.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (valid_pointer (Vptr b i)) (valid_pointer (Vptr b0 i0))) (if sameblock (Vptr b i) (Vptr b0 i0) then @andp mpred Nveric (weak_valid_pointer (Vptr b i)) (weak_valid_pointer (Vptr b0 i0)) else @andp mpred Nveric (valid_pointer (Vptr b i)) (valid_pointer (Vptr b0 i0))) *)
 destruct (sameblock _ _); auto.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (valid_pointer (Vptr b i)) (valid_pointer (Vptr b0 i0))) (@andp mpred Nveric (weak_valid_pointer (Vptr b i)) (weak_valid_pointer (Vptr b0 i0))) *)
 apply andp_derives; apply valid_pointer_weak.
Qed.

Lemma valid_pointer_null:
  forall P, P |-- valid_pointer nullval.
Proof.
(* Goal: forall i : Z, @eq Byte.int (@Znth Byte.int Inhabitant_byte i (@cons Byte.int Byte.zero (@nil Byte.int))) Byte.zero *)
  intros. unfold nullval, valid_pointer, valid_pointer'. 
  destruct Archi.ptr64 eqn:Hp; simpl;
 change predicates_hered.prop with prop; (* delete me *)
 normalize.
Qed.


Lemma extend_valid_pointer:
  forall p Q, valid_pointer p * Q |-- valid_pointer p.
Proof.
(* Goal: forall i : Z, @eq Byte.int (@Znth Byte.int Inhabitant_byte i (@cons Byte.int Byte.zero (@nil Byte.int))) Byte.zero *)
intros.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (valid_pointer p) Q) (valid_pointer p) *)
 unfold valid_pointer.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@predicates_hered.orp compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (valid_pointer' p Z0) (valid_pointer' p (Zneg xH))) Q) (@predicates_hered.orp compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (valid_pointer' p Z0) (valid_pointer' p (Zneg xH))) *)
 pose proof (extend_tc.extend_valid_pointer' p 0).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@predicates_hered.orp compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (valid_pointer' p Z0) (valid_pointer' p (Zneg xH))) Q) (@predicates_hered.orp compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (valid_pointer' p Z0) (valid_pointer' p (Zneg xH))) *)
 pose proof (predicates_hered.boxy_e _ _ H).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (valid_pointer' p Z0) Q) (valid_pointer' p Z0) *)
 change (_ |-- _) with (predicates_hered.derives (valid_pointer' p 0 * Q) (valid_pointer' p 0)).
(* Goal: @predicates_hered.derives compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (@sepcon (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric Sveric (@predicates_hered.orp compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (valid_pointer' p Z0) (valid_pointer' p (Zneg xH))) Q) (@predicates_hered.orp compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (valid_pointer' p Z0) (valid_pointer' p (Zneg xH))) *)
 intros ? (w1 & w2 & Hj & Hp & ?).
(* Goal: @predicates_hered.app_pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (valid_pointer' p Z0) a *)
 apply (H0 w1); auto.
(* Goal: @predicates_hered.app_mode compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (@predicates_sl.extendM 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) w1 a *)
 hnf; eauto.
Qed.

Lemma extend_weak_valid_pointer:
  forall p Q, weak_valid_pointer p * Q |-- weak_valid_pointer p.
Proof.
(* Goal: forall i : Z, @eq Byte.int (@Znth Byte.int Inhabitant_byte i (@cons Byte.int Byte.zero (@nil Byte.int))) Byte.zero *)
  intros. unfold weak_valid_pointer.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@predicates_hered.orp compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (valid_pointer' p Z0) (valid_pointer' p (Zneg xH))) Q) (@predicates_hered.orp compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (valid_pointer' p Z0) (valid_pointer' p (Zneg xH))) *)
  pose proof (extend_tc.extend_valid_pointer' p 0).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@predicates_hered.orp compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (valid_pointer' p Z0) (valid_pointer' p (Zneg xH))) Q) (@predicates_hered.orp compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (valid_pointer' p Z0) (valid_pointer' p (Zneg xH))) *)
  pose proof (predicates_hered.boxy_e _ _ H). 
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@predicates_hered.orp compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (valid_pointer' p Z0) (valid_pointer' p (Zneg xH))) Q) (@predicates_hered.orp compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (valid_pointer' p Z0) (valid_pointer' p (Zneg xH))) *)
  pose proof (extend_tc.extend_valid_pointer' p (-1)).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@predicates_hered.orp compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (valid_pointer' p Z0) (valid_pointer' p (Zneg xH))) Q) (@predicates_hered.orp compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (valid_pointer' p Z0) (valid_pointer' p (Zneg xH))) *)
  pose proof (predicates_hered.boxy_e _ _ H1).
  change (_ |-- _) with
      (predicates_hered.derives
         (predicates_hered.orp (valid_pointer' p 0) (valid_pointer' p (-1)) * Q)
         (predicates_hered.orp (valid_pointer' p 0) (valid_pointer' p (-1)))).
(* Goal: @predicates_hered.derives compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (@sepcon (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric Sveric (@predicates_hered.orp compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (valid_pointer' p Z0) (valid_pointer' p (Zneg xH))) Q) (@predicates_hered.orp compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (valid_pointer' p Z0) (valid_pointer' p (Zneg xH))) *)
  intros ? (w1 & w2 & Hj & Hp & ?). simpl in Hp |- * .
(* Goal: @predicates_hered.app_mode compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap (@predicates_sl.extendM 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) w1 a *)
  destruct Hp; [left; apply (H0 w1) | right; apply (H2 w1)]; auto; hnf; eauto.
Qed.

Lemma sepcon_valid_pointer1:
     forall (P Q: mpred) p,
        P |-- valid_pointer p ->
        P * Q |-- valid_pointer p.
Proof.
(* Goal: forall i : Z, @eq Byte.int (@Znth Byte.int Inhabitant_byte i (@cons Byte.int Byte.zero (@nil Byte.int))) Byte.zero *)
intros.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric P Q) (valid_pointer p) *)
 eapply derives_trans; [apply sepcon_derives; [eassumption | apply TT_right] |].
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (valid_pointer p) (@TT mpred Nveric)) (valid_pointer p) *)
 clear H.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (valid_pointer p) (@TT mpred Nveric)) (valid_pointer p) *)
 apply extend_valid_pointer.
Qed.

 Lemma sepcon_valid_pointer2:
     forall (P Q: mpred) p,
        P |-- valid_pointer p ->
        Q * P |-- valid_pointer p.
Proof.
(* Goal: forall i : Z, @eq Byte.int (@Znth Byte.int Inhabitant_byte i (@cons Byte.int Byte.zero (@nil Byte.int))) Byte.zero *)
 intros. rewrite sepcon_comm; apply sepcon_valid_pointer1.
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q) (_ : P), Q *)
 auto.
Qed.

Lemma sepcon_weak_valid_pointer1: 
 forall (P Q : mpred) (p : val),
   P |-- weak_valid_pointer p -> P * Q |-- weak_valid_pointer p.
Proof.
(* Goal: forall i : Z, @eq Byte.int (@Znth Byte.int Inhabitant_byte i (@cons Byte.int Byte.zero (@nil Byte.int))) Byte.zero *)
  intros.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric P Q) (weak_valid_pointer p) *)
  eapply derives_trans; [ | apply (extend_weak_valid_pointer p Q)].
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q) (_ : P), Q *)
  apply sepcon_derives; auto.
Qed.

Lemma sepcon_weak_valid_pointer2:
  forall (P Q : mpred) (p : val),
    P |-- weak_valid_pointer p -> Q * P |-- weak_valid_pointer p.
Proof.
(* Goal: forall i : Z, @eq Byte.int (@Znth Byte.int Inhabitant_byte i (@cons Byte.int Byte.zero (@nil Byte.int))) Byte.zero *)
  intros. rewrite sepcon_comm.
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q) (_ : P), Q *)
  apply sepcon_weak_valid_pointer1; auto.
Qed.

 Lemma andp_valid_pointer1:
     forall (P Q: mpred) p,
        P |-- valid_pointer p ->
        P && Q |-- valid_pointer p.
Proof.
(* Goal: forall i : Z, @eq Byte.int (@Znth Byte.int Inhabitant_byte i (@cons Byte.int Byte.zero (@nil Byte.int))) Byte.zero *)
intros.
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q) (_ : P), Q *)
 apply andp_left1; auto.
Qed.

 Lemma andp_valid_pointer2:
     forall (P Q: mpred) p,
        P |-- valid_pointer p ->
        Q && P |-- valid_pointer p.
Proof.
(* Goal: forall i : Z, @eq Byte.int (@Znth Byte.int Inhabitant_byte i (@cons Byte.int Byte.zero (@nil Byte.int))) Byte.zero *)
intros.
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q) (_ : P), Q *)
 apply andp_left2; auto.
Qed.

Lemma valid_pointer_zero32:
  forall P, Archi.ptr64=false -> P |-- valid_pointer (Vint (Int.repr 0)).
Proof.
(* Goal: forall i : Z, @eq Byte.int (@Znth Byte.int Inhabitant_byte i (@cons Byte.int Byte.zero (@nil Byte.int))) Byte.zero *)
 intros.
(* Goal: @derives mpred Nveric P (valid_pointer (Vlong (Int64.repr Z0))) *)
 unfold valid_pointer, valid_pointer'. rewrite H.
 change predicates_hered.prop with prop; (* delete me *)
 normalize.
Qed.

Lemma valid_pointer_zero64:
  forall P, Archi.ptr64=true -> P |-- valid_pointer (Vlong (Int64.repr 0)).
Proof.
(* Goal: forall i : Z, @eq Byte.int (@Znth Byte.int Inhabitant_byte i (@cons Byte.int Byte.zero (@nil Byte.int))) Byte.zero *)
 intros.
(* Goal: @derives mpred Nveric P (valid_pointer (Vlong (Int64.repr Z0))) *)
 unfold valid_pointer, valid_pointer'. rewrite H.
 change predicates_hered.prop with prop; (* delete me *)
 normalize.
Qed.


Hint Resolve sepcon_valid_pointer1 sepcon_valid_pointer2 : valid_pointer.
Hint Resolve andp_valid_pointer1 andp_valid_pointer2 : valid_pointer.
Hint Resolve valid_pointer_null : valid_pointer.
Hint Resolve valid_pointer_zero32 : valid_pointer.
Hint Resolve valid_pointer_zero64 : valid_pointer.
Hint Resolve sepcon_weak_valid_pointer1: valid_pointer. 
Hint Resolve sepcon_weak_valid_pointer2: valid_pointer. 


(* TODO: test_order need to be added *)
Ltac solve_valid_pointer :=
match goal with
| |- _ |-- denote_tc_test_eq _ _ && _ =>
           apply andp_right;
               [apply denote_tc_test_eq_split;
                solve [auto 50 with valid_pointer] | ]
| |- _ |-- valid_pointer _ && _ =>
           apply andp_right; [ solve [auto 50 with valid_pointer] | ]
| |- _ |-- weak_valid_pointer _ && _ =>
           apply andp_right; [ solve [auto 50 with valid_pointer] | ]
| |- _ |-- denote_tc_test_eq _ _ =>
              auto 50 with valid_pointer
| |- _ |-- valid_pointer _ =>
              auto 50 with valid_pointer
| |- _ |-- weak_valid_pointer _ =>
              auto 50 with valid_pointer
end.

Hint Rewrite (@TT_andp mpred _) : gather_prop.
Hint Rewrite (@andp_TT mpred _) : gather_prop.

Ltac pull_out_props :=
    repeat (( simple apply derives_extract_prop
                || simple apply derives_extract_prop');
                fancy_intros true);
    autorewrite with gather_prop;
    repeat (( simple apply derives_extract_prop
                || simple apply derives_extract_prop');
                fancy_intros true).

Ltac simplify_float2int :=
match goal with
| |- context [Zofsingle (Float32.of_bits (Int.repr ?A))] =>
   putable A; 
   let x := fresh "x" in (evar (x: Z));
   replace (Zofsingle (Float32.of_bits (Int.repr A))) with (Some x) by (subst x; reflexivity);
   compute in x; subst x
| |- context [Zoffloat (Float.of_bits (Int.repr ?A))] =>
   putable A; 
   let x := fresh "x" in (evar (x: Z));
   replace (Zoffloat (Float.of_bits (Int.repr A))) with (Some x) by (subst x; reflexivity);
   compute in x; subst x
end.

Ltac ent_iter :=
    repeat simplify_float2int;
    autorewrite with gather_prop;
    repeat (( simple apply derives_extract_prop
                || simple apply derives_extract_prop');
                fancy_intros true);
(*   saturate_local; *)
   repeat erewrite unfold_reptype_elim in * by (apply JMeq_refl; reflexivity);
   simpl_compare;
   simpl_denote_tc;
   safe_subst_any;
   try autorewrite with entailer_rewrite in *;
   try solve_valid_pointer;
   repeat data_at_conflict_neq.

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

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

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

Lemma False_and: forall x, (False /\ x) = False.
Proof.
(* Goal: forall x : Prop, @eq Prop (and False x) False *)
intros; apply prop_ext; intuition.
Qed.
Ltac splittable :=
 match goal with
 | |- _ <= _ < _ => fail 1
 | |- _ < _ <= _ => fail 1
 | |- _ <= _ <= _ => fail 1
 | |- _ < _ < _ => fail 1
 | |- _ <-> _ => fail 1
 | |- _ /\ _ => idtac
 end.

Ltac prove_signed_range :=
  match goal with
  | |- Int.min_signed <= _ <= Int.max_signed => 
           normalize; rep_omega
  | |- Int64.min_signed <= _ <= Int64.max_signed => 
           normalize; rep_omega
  end.

Lemma ptr_eq_refl: forall x, isptr x -> ptr_eq x x.
Proof.
(* Goal: forall (x : val) (_ : isptr x), ptr_eq x x *)
destruct x; simpl; intros; try contradiction.
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q) (_ : P), Q *)
split; auto. apply Ptrofs.eq_true.
Qed.
Hint Resolve ptr_eq_refl : prove_it_now.

Lemma ptr_eq_nullval: ptr_eq nullval nullval.
Proof.
Transparent Archi.ptr64.
unfold ptr_eq, nullval; simpl.
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q) (_ : P), Q *)
split3; auto.
Opaque Archi.ptr64.
Qed.

Hint Resolve ptr_eq_nullval : prove_it_now.

Hint Extern 4 (value_fits _ _ _) =>
   (rewrite ?proj_sumbool_is_true by auto;
    rewrite ?proj_sumbool_is_false by auto;
    repeat simplify_value_fits; auto) : prove_it_now.

Lemma intsigned_intrepr_bytesigned: forall i,
   Int.signed (Int.repr (Byte.signed i)) = Byte.signed i.
Proof.
(* Goal: forall i : Z, @eq Byte.int (@Znth Byte.int Inhabitant_byte i (@cons Byte.int Byte.zero (@nil Byte.int))) Byte.zero *)
 intros. rewrite Int.signed_repr; auto.
(* Goal: and (Z.le Int.min_signed (Byte.signed i)) (Z.le (Byte.signed i) Int.max_signed) *)
  destruct (Byte.signed_range i).
(* Goal: and (Z.le Int.min_signed (Byte.signed i)) (Z.le (Byte.signed i) Int.max_signed) *)
  split.
(* Goal: Z.le Int.min_signed (Byte.signed i) *)
(* Goal: Z.le (Byte.signed i) Int.max_signed *)
  eapply Z.le_trans; [ | eassumption]. compute; intros Hx; inv Hx.
(* Goal: Z.le Byte.max_signed Int.max_signed *)
  eapply Z.le_trans; [eassumption | ]. compute; intros Hx; inv Hx.
Qed.

Hint Rewrite intsigned_intrepr_bytesigned : rep_omega.

Ltac prove_it_now :=
 first [ splittable; fail 1
        | computable
        | apply Coq.Init.Logic.I
        | reflexivity
        | rewrite ?intsigned_intrepr_bytesigned; rep_omega (* Omega0 *)
        | prove_signed_range
        | repeat match goal with H: ?A |- _ => has_evar A; clear H end;
          auto with prove_it_now field_compatible;
          autorewrite with norm entailer_rewrite; normalize;
          first [eapply field_compatible_nullval; eassumption
                 | eapply field_compatible_nullval1; eassumption
                 | eapply field_compatible_nullval2; eassumption
                 ]
         ].

Ltac try_prove_it_now :=
 first [match goal with H := _ |- _ => instantiate (1:=True) in H; prove_it_now end
       | eassumption].

(* try_conjuncts.  The purpose of this is to avoid splitting any
  goal into two subgoals, for the reason that perhaps the
  user wants to simplify things above the line before splitting.
   On the other hand, if the current goal is  A/\B/\C/\D
  where B and D are easily provable, one wants to leave the
  goal A/\C.
*)
Lemma try_conjuncts_lem2: forall A B : Prop,
   B -> A -> (A /\ B).
Proof. intuition. Qed.

Lemma try_conjuncts_lem: forall A B A' B' : Prop,
   (A -> A') -> (B -> B') -> (A /\ B -> A' /\ B').
Proof. intuition. Qed.

Lemma try_conjuncts_start: forall A B: Prop,
   (A -> B) -> (A -> B).
 Proof. intuition. Qed.

Ltac try_conjuncts_solver :=
    lazymatch goal with H:_ |- ?A =>
         no_evars A;
         clear H; try immediate; auto; prove_it_now; fail
    end.

Ltac try_conjuncts :=
 first [ simple eapply conj;
                [try_conjuncts_solver | try_conjuncts ]
        | simple eapply try_conjuncts_lem2;
                [try_conjuncts_solver | match goal with H:_ |- _ => apply H end ]
        | simple eapply try_conjuncts_lem;
            [intro; try_conjuncts | intro; try_conjuncts
            |match goal with H:_ |- _ => apply H end ]
        | match goal with H:_ |- _ => instantiate (1:=True) in H;
                try_conjuncts_solver
          end
        | match goal with H:_ |- _ => apply H end
        ].

Lemma try_conjuncts_prop_and:
  forall {A}{NA: NatDed A} (S: A) (P P': Prop) Q,
      (P' -> P) ->
      S |-- !! P' && Q ->
      S |-- !! P && Q.
(* Goal: forall i : Z, @eq Byte.int (@Znth Byte.int Inhabitant_byte i (@cons Byte.int Byte.zero (@nil Byte.int))) Byte.zero *)
Proof. intros.
(* Goal: @derives A NA S (@prop A NA P) *)
 eapply derives_trans; [apply H0 |].
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q) (_ : P), Q *)
 apply andp_derives; auto.
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q) (_ : P), Q *)
 apply prop_derives; auto.
Qed.


Lemma try_conjuncts_prop:
  forall {A}{NA: NatDed A} (S: A) (P P': Prop),
      (P' -> P) ->
      S |-- !! P' ->
      S |-- !! P .
(* Goal: forall i : Z, @eq Byte.int (@Znth Byte.int Inhabitant_byte i (@cons Byte.int Byte.zero (@nil Byte.int))) Byte.zero *)
Proof. intros.
(* Goal: @derives A NA S (@prop A NA P) *)
 eapply derives_trans; [apply H0 |].
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q) (_ : P), Q *)
 apply prop_derives; auto.
Qed.

Ltac prop_right_cautious :=
 try solve [simple apply prop_right; auto; prove_it_now].

Ltac prune_conjuncts :=
 repeat rewrite and_assoc';
 first [simple eapply try_conjuncts_prop;
              [intro; try_conjuncts
              | cbv beta; repeat rewrite and_True; prop_right_cautious ]
         | simple eapply try_conjuncts_prop_and;
              [intro; try_conjuncts
              | cbv beta; repeat rewrite and_True; try simple apply go_lower_lem1]
         | idtac].

Ltac entailer' :=
 repeat (progress (ent_iter; normalize));
 try simple apply prop_and_same_derives;
 prune_conjuncts;
 try rewrite (prop_true_andp True) by apply Coq.Init.Logic.I;
 try solve_valid_pointer;
 try first [apply derives_refl
              | simple apply FF_left
              | simple apply TT_right].

Lemma empTrue:
 @derives mpred Nveric (@emp mpred Nveric Sveric) (@prop mpred Nveric True).
Proof.
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q) (_ : P), Q *)
apply prop_right; auto.
Qed.

Ltac entailer :=
 try match goal with POSTCONDITION := @abbreviate ret_assert _ |- _ =>
        clear POSTCONDITION
      end;
 try match goal with MORE_COMMANDS := @abbreviate statement _ |- _ =>
        clear MORE_COMMANDS
      end;
 match goal with
 | |- ?P |-- _ =>
    match type of P with
    | ?T => unify T (environ->mpred); go_lower
    | _ => clear_Delta; pull_out_props
    end
 | |- _ => fail "The entailer tactic works only on entailments   _ |-- _ "
 end;
 saturate_local;
 entailer';
 rewrite <- ?sepcon_assoc.

Lemma my_auto_lem:
 forall (P Q: Prop), (P -> Q) -> (P -> Q).
Proof. auto. Qed.

Ltac my_auto_iter H :=
 first [instantiate (1:=True) in H;  prove_it_now
       | splittable;
         eapply try_conjuncts_lem;
            [let H1 := fresh in intro H1; my_auto_iter H1
            |let H1 := fresh in intro H1; my_auto_iter H1
            | apply H ]
       | apply H
       ].

Ltac all_True :=  solve [repeat simple apply conj; simple apply Coq.Init.Logic.I].

Ltac my_auto_reiter :=
 first [simple apply conj; [all_True | ]; my_auto_reiter
        |simple apply conj; [ | all_True]; my_auto_reiter
        |splittable; eapply try_conjuncts_lem;
                [intro; my_auto_reiter
                |intro; my_auto_reiter
                |eassumption]
        |eassumption].

Ltac my_auto :=
 rewrite ?isptr_force_ptr by auto;
 let H := fresh in eapply my_auto_lem; [intro H; my_auto_iter H | ];
 try all_True;
 (eapply my_auto_lem; [intro; my_auto_reiter | ]);
 normalize.

Lemma prop_and_same_derives' {A}{NA: NatDed A}:
  forall (P: Prop) Q,   P   ->   Q |-- !!P && Q.
Proof.
(* Goal: forall i : Z, @eq Byte.int (@Znth Byte.int Inhabitant_byte i (@cons Byte.int Byte.zero (@nil Byte.int))) Byte.zero *)
intros. apply andp_right; auto. apply prop_right; auto.
Qed.

Ltac entbang :=
 intros;
 try match goal with POSTCONDITION := @abbreviate ret_assert _ |- _ =>
        clear POSTCONDITION
      end;
 try match goal with MORE_COMMANDS := @abbreviate statement _ |- _ =>
        clear MORE_COMMANDS
      end;
 match goal with
 | |- local _ && ?P |-- _ => go_lower; (*simpl;*) try (*simple*) apply empTrue
 | |- ?P |-- _ =>
    match type of P with
    | ?T => unify T mpred; pull_out_props
    end
 | |- _ => fail "The entailer tactic works only on entailments  _ |-- _ "
 end;
 (* The following lines are only a temporary solution. Many current proofs
 depend on one original feature of "entailer!": sem_cast expressions and
 sem_binary_operation' expressions will be simplified. This step was done
 in go_lower. But that is not a reasonable design. Current version of
 go_lower does not "simpl" user's expressions any longer---go_lower should
 be safe. Thus we add the following lines here. *)
 repeat match goal with
        | |- context [force_val (sem_binary_operation' ?op ?t1 ?t2 ?v1 ?v2)] =>
          progress simpl (force_val (sem_binary_operation' op t1 t2 v1 v2))
        end;
 simpl sem_cast;
 (* end of temporary solution *)
 saturate_local;
 ent_iter;
 repeat change (mapsto_memory_block.spacer _ _ _ _) with emp;
 first [ contradiction
        | simple apply prop_right; my_auto
        | match goal with |- ?Q |-- !! _ && ?Q' => constr_eq  Q Q';
                      simple apply prop_and_same_derives'; my_auto
          end
        | simple apply andp_right;
            [apply prop_right; my_auto 
            | cancel; rewrite <- ?sepcon_assoc; autorewrite with norm ]
        | normalize; cancel; rewrite <- ?sepcon_assoc
        ].

Tactic Notation "entailer" "!" := entbang.

Ltac elim_hyps :=  (* not in use anywhere? *)
 repeat match goal with
 | H: isptr ?x |- _ =>
     let x1 := fresh x "_b" in let x2 := fresh x "_ofs" in
     destruct x as [ | | | | | x1 x2]; inv H
 | H: ptr_eq _ _ |- _ => apply ptr_eq_e in H; safe_subst_any
 end.

Ltac aggressive :=
  repeat split; auto; elim_hyps; simpl; (computable || auto).

(**** try this out here, for now ****)

Hint Rewrite Int.signed_repr using rep_omega : norm.
Hint Rewrite Int.unsigned_repr using rep_omega : norm.
Hint Rewrite Int64.signed_repr using rep_omega : norm.
Hint Rewrite Int64.unsigned_repr using rep_omega : norm.

(************** TACTICS FOR GENERATING AND EXECUTING TEST CASES *******)

Definition EVAR (x: Prop) := x.
Lemma EVAR_e: forall x, EVAR x -> x.
Proof. intros. apply H. Qed.

Ltac gather_entail :=
repeat match goal with
 | A := _ |- _ =>  clear A || (revert A; match goal with |- ?B => no_evars B end)
 | H : ?P |- _ =>
  match type of P with
  | Prop => match P with name _ => fail 2 | _ => revert H; match goal with |- ?B => no_evars B end end
  | _ => clear H || (revert H; match goal with |- ?B => no_evars B end)
  end
end;
repeat match goal with
 | x := ?X |- _ => is_evar X; clearbody x; revert x; apply EVAR_e
end;
repeat match goal with
  | H : name _ |- _ => revert H
 end.

Lemma EVAR_i: forall P: Prop, P -> EVAR P.
Proof. intros. apply H. Qed.

Ltac ungather_entail :=
match goal with
  | |- EVAR (forall x : ?t, _) =>
       let x' := fresh x in evar (x' : t);
       let x'' := fresh x in apply EVAR_i; intro x'';
       replace x'' with x'; [ungather_entail; clear x'' | admit ]
  | |- _ => intros
 end.

Lemma offset_val_sizeof_hack:
 forall cenv t i p,
   isptr p ->
   i=0 ->
   (offset_val (@sizeof cenv t * i) p = p) = True.
Proof.
(* Goal: forall i : Z, @eq Byte.int (@Znth Byte.int Inhabitant_byte i (@cons Byte.int Byte.zero (@nil Byte.int))) Byte.zero *)
intros.
(* Goal: @eq Prop (@eq val (offset_val (Z.mul (@sizeof cenv t) i) p) (offset_val (@sizeof cenv t) p)) True *)
subst.
(* Goal: and (Z.le (Z.add (@Zlength Byte.int s) (Zpos xH)) n) (Z.le n Ptrofs.max_unsigned) *)
destruct p; try contradiction.
(* Goal: @eq Prop (@eq val (offset_val (Z.mul (@sizeof cenv t) Z0) (Vptr b i)) (Vptr b i)) True *)
simpl. rewrite Z.mul_0_r.
(* Goal: @eq Prop (@eq val (Vptr b (Ptrofs.add i (Ptrofs.repr Z0))) (Vptr b i)) True *)
rewrite Ptrofs.add_zero.
(* Goal: forall (A B : Prop) (_ : forall _ : A, B) (_ : A), B *)
apply prop_ext; intuition.
Qed.
Hint Rewrite offset_val_sizeof_hack : norm.

Lemma offset_val_sizeof_hack2:
 forall cenv t i j p,
   isptr p ->
   i=j ->
   (offset_val (@sizeof cenv t * i) p = offset_val (@sizeof cenv t * j) p) = True.
Proof.
(* Goal: forall i : Z, @eq Byte.int (@Znth Byte.int Inhabitant_byte i (@cons Byte.int Byte.zero (@nil Byte.int))) Byte.zero *)
intros.
(* Goal: @eq Prop (@eq val (offset_val (Z.mul (@sizeof cenv t) i) p) (offset_val (@sizeof cenv t) p)) True *)
subst.
(* Goal: forall (A B : Prop) (_ : forall _ : A, B) (_ : A), B *)
apply prop_ext; intuition.
Qed.
Hint Rewrite offset_val_sizeof_hack2 : norm.

Lemma offset_val_sizeof_hack3:
 forall cenv t i p,
   isptr p ->
   i=1 ->
   (offset_val (@sizeof cenv t * i) p = offset_val (@sizeof cenv t) p) = True.
Proof.
(* Goal: forall i : Z, @eq Byte.int (@Znth Byte.int Inhabitant_byte i (@cons Byte.int Byte.zero (@nil Byte.int))) Byte.zero *)
intros.
(* Goal: @eq Prop (@eq val (offset_val (Z.mul (@sizeof cenv t) i) p) (offset_val (@sizeof cenv t) p)) True *)
subst.
(* Goal: @eq Prop (@eq val (offset_val (Z.mul (@sizeof cenv t) (Zpos xH)) p) (offset_val (@sizeof cenv t) p)) True *)
rewrite Z.mul_1_r.
(* Goal: forall (A B : Prop) (_ : forall _ : A, B) (_ : A), B *)
apply prop_ext; intuition.
Qed.
Hint Rewrite offset_val_sizeof_hack3 : norm.

Ltac make_Vptr c :=
  let H := fresh in assert (isptr c) by auto;
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (valid_pointer p) (@TT mpred Nveric)) (valid_pointer p) *)
  destruct c; try (contradiction H); clear H.

Lemma Zmax0r: forall n, 0 <= n -> Z.max 0 n = n.
Proof.
(* Goal: forall i : Z, @eq Byte.int (@Znth Byte.int Inhabitant_byte i (@cons Byte.int Byte.zero (@nil Byte.int))) Byte.zero *)
intros. apply Z.max_r; auto.
Qed.
Hint Rewrite Zmax0r using (try computable; rep_omega (*Omega0*)) : norm.

Import ListNotations.

Definition cstring {CS : compspecs} sh (s: list byte) p := 
  !!(~In Byte.zero s) &&
  data_at sh (tarray tschar (Zlength s + 1)) (map Vbyte (s ++ [Byte.zero])) p.

Lemma cstring_local_facts: forall {CS : compspecs} sh s p, 
  cstring sh s p |-- !! (isptr p /\ Zlength s + 1 < Ptrofs.modulus).
Proof.
(* Goal: forall (CS : compspecs) (sh : Share.t) (s : list Byte.int) (p : val), @derives mpred Nveric (@cstring CS sh s p) (@prop mpred Nveric (and (isptr p) (Z.lt (Z.add (@Zlength Byte.int s) (Zpos xH)) Ptrofs.modulus))) *)
  intros; unfold cstring; entailer!.
(* Goal: and (Z.le (Z.add (@Zlength Byte.int s) (Zpos xH)) n) (Z.le n Ptrofs.max_unsigned) *)
  destruct H0 as [? [_ [? _]]].
(* Goal: and (Z.le (Z.add (@Zlength Byte.int s) (Zpos xH)) n) (Z.le n Ptrofs.max_unsigned) *)
  destruct p; try contradiction.
(* Goal: Z.lt (Z.add (@Zlength Byte.int s) (Zpos xH)) Ptrofs.modulus *)
  red in H3.
(* Goal: Z.lt (Z.add (@Zlength Byte.int s) (Zpos xH)) Ptrofs.modulus *)
  unfold sizeof in H3; clear H1.
(* Goal: Z.lt (Z.add (@Zlength Byte.int s) (Zpos xH)) Ptrofs.modulus *)
  rewrite Z.max_r in H3 by list_solve.
(* Goal: Z.lt (Z.add (@Zlength Byte.int s) (Zpos xH)) Ptrofs.modulus *)
  fold sizeof in H3.
(* Goal: Z.lt (Z.add (@Zlength Byte.int s) (Zpos xH)) Ptrofs.modulus *)
  change (sizeof tschar) with 1 in H3.
(* Goal: Z.le n Ptrofs.max_unsigned *)
  pose proof (Ptrofs.unsigned_range i).
(* Goal: Z.lt (Z.add (@Zlength Byte.int s) (Zpos xH)) Ptrofs.modulus *)
  omega. 
Qed.

Hint Resolve cstring_local_facts : saturate_local.

Lemma cstring_valid_pointer: forall {CS : compspecs} sh s p, 
   nonempty_share sh -> 
   cstring sh s p |-- valid_pointer p.
Proof.
(* Goal: forall (CS : compspecs) (sh : share) (s : list Byte.int) (p : val) (_ : nonempty_share sh), @derives mpred Nveric (@cstring CS sh s p) (valid_pointer p) *)
  intros; unfold cstring; Intros.
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q) (_ : P), Q *)
  apply data_at_valid_ptr; auto.
(* Goal: Z.gt (@sizeof (@cenv_cs CS) (tarray tschar (Z.add (@Zlength Byte.int s) (Zpos xH)))) Z0 *)
  unfold tarray, tschar, sizeof.
(* Goal: Z.gt (Z.mul (Zpos xH) (Z.max Z0 n)) Z0 *)
  pose proof (Zlength_nonneg s).
(* Goal: Z.lt (Z.add (@Zlength Byte.int s) (Zpos xH)) Ptrofs.modulus *)
  rewrite Z.max_r; omega.
Qed.

Hint Resolve cstring_valid_pointer : valid_pointer.
Definition cstringn {CS : compspecs} sh (s: list byte) n p :=
  !!(~In Byte.zero s) &&
  data_at sh (tarray tschar n) (map Vbyte (s ++ [Byte.zero]) ++
    list_repeat (Z.to_nat (n - (Zlength s + 1))) Vundef) p.

Lemma cstringn_equiv : forall {CS : compspecs} sh s p, cstring sh s p = cstringn sh s (Zlength s + 1) p.
Proof.
(* Goal: forall (CS : compspecs) (sh : Share.t) (s : list Byte.int) (p : val), @eq mpred (@cstring CS sh s p) (@cstringn CS sh s (Z.add (@Zlength Byte.int s) (Zpos xH)) p) *)
  intros; unfold cstring, cstringn.
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q) (_ : P), Q *)
  rewrite Zminus_diag, app_nil_r; auto.
Qed.

Lemma cstringn_local_facts: forall {CS : compspecs} sh s n p, 
   cstringn sh s n p |-- !! (isptr p /\ Zlength s + 1 <= n <= Ptrofs.max_unsigned).
Proof.
(* Goal: forall (CS : compspecs) (sh : Share.t) (s : list Byte.int) (n : Z) (p : val), @derives mpred Nveric (@cstringn CS sh s n p) (@prop mpred Nveric (and (isptr p) (and (Z.le (Z.add (@Zlength Byte.int s) (Zpos xH)) n) (Z.le n Ptrofs.max_unsigned)))) *)
  intros; unfold cstringn; entailer!.
(* Goal: and (Z.le (Z.add (@Zlength Byte.int s) (Zpos xH)) n) (Z.le n Ptrofs.max_unsigned) *)
  autorewrite with sublist in H1.
(* Goal: Z.gt (Z.mul (Zpos xH) (Z.max Z0 n)) Z0 *)
  pose proof (Zlength_nonneg s).
(* Goal: and (Z.le (Z.add (@Zlength Byte.int s) (Zpos xH)) n) (Z.le n Ptrofs.max_unsigned) *)
  pose proof (Zlength_nonneg (list_repeat (Z.to_nat (n - (Zlength s + 1))) Vundef)).
(* Goal: and (Z.le (Z.add (@Zlength Byte.int s) (Zpos xH)) n) (Z.le n Ptrofs.max_unsigned) *)
  destruct H0 as [? [_ [? _]]].
(* Goal: and (Z.le (Z.add (@Zlength Byte.int s) (Zpos xH)) n) (Z.le n Ptrofs.max_unsigned) *)
  destruct p; try contradiction.
(* Goal: and (Z.le (Z.add (@Zlength Byte.int s) (Zpos xH)) n) (Z.le n Ptrofs.max_unsigned) *)
  red in H5.
(* Goal: and (Z.le (Z.add (@Zlength Byte.int s) (Zpos xH)) n) (Z.le n Ptrofs.max_unsigned) *)
  clear H2.
(* Goal: Z.lt (Z.add (@Zlength Byte.int s) (Zpos xH)) Ptrofs.modulus *)
  destruct (Z.max_spec 0 n) as [[? Hn] | [? Hn]]; rewrite Hn in *; split; try omega.
(* Goal: Z.le n Ptrofs.max_unsigned *)
  unfold sizeof in H5. rewrite Hn in H5. fold sizeof in H5.
(* Goal: Z.le n Ptrofs.max_unsigned *)
  change (sizeof tschar) with 1 in H5. 
(* Goal: Z.le n Ptrofs.max_unsigned *)
  pose proof (Ptrofs.unsigned_range i).
(* Goal: Z.lt (Z.add (@Zlength Byte.int s) (Zpos xH)) Ptrofs.modulus *)
  rep_omega.
Qed.

Hint Resolve cstringn_local_facts : saturate_local.

Lemma cstringn_valid_pointer: forall {CS : compspecs} sh s n p, 
     nonempty_share sh -> 
     cstringn sh s n p |-- valid_pointer p.
Proof.
(* Goal: forall i : Z, @eq Byte.int (@Znth Byte.int Inhabitant_byte i (@cons Byte.int Byte.zero (@nil Byte.int))) Byte.zero *)
  intros.
(* Goal: @derives mpred Nveric (@cstringn CS sh s n p) (valid_pointer p) *)
  entailer!. 
(* Goal: @derives mpred Nveric (@cstringn CS sh s n p) (valid_pointer p) *)
  unfold cstringn; Intros.
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q) (_ : P), Q *)
  apply data_at_valid_ptr; auto.
(* Goal: Z.gt (@sizeof (@cenv_cs CS) (tarray tschar n)) Z0 *)
  unfold tarray, tschar, sizeof; cbv beta iota zeta.
(* Goal: Z.gt (Z.mul (Zpos xH) (Z.max Z0 n)) Z0 *)
  pose proof (Zlength_nonneg s).
(* Goal: Z.lt (Z.add (@Zlength Byte.int s) (Zpos xH)) Ptrofs.modulus *)
  rewrite Z.max_r; omega.
Qed.

Hint Resolve cstringn_valid_pointer : valid_pointer.


Lemma Znth_zero_zero:
  forall i, Znth i [Byte.zero] = Byte.zero.
Proof.
(* Goal: forall i : Z, @eq Byte.int (@Znth Byte.int Inhabitant_byte i (@cons Byte.int Byte.zero (@nil Byte.int))) Byte.zero *)
intros.
(* Goal: @eq Byte.int (@Znth Byte.int Inhabitant_byte i (@cons Byte.int Byte.zero (@nil Byte.int))) Byte.zero *)
unfold Znth.
(* Goal: @eq Byte.int (@nth Byte.int O (@cons Byte.int Byte.zero (@nil Byte.int)) Inhabitant_byte) Byte.zero *)
(* Goal: @eq Byte.int (@nth Byte.int (S n) (@cons Byte.int Byte.zero (@nil Byte.int)) Inhabitant_byte) Byte.zero *)
if_tac; auto. destruct (Z.to_nat i). reflexivity. destruct n; reflexivity.
Qed.


(* THIS TACTIC solves goals of the form,
    ~In 0 ls,  Znth i (ls++[0]) = 0 |-  (any omega consequence of)  i < Zlength ls
    ~In 0 ls,  Znth i (ls++[0]) <> 0 |-  (any omega consequence of)  i >= Zlength ls
*)
Ltac cstring :=
  lazymatch goal with
  | H: ~In Byte.zero _ |- _ => idtac
  | |- _ => fail "The cstring tactic expects to see a hypothesis above the line of the form, ~ In Byte.zero _"
  end;
 lazymatch goal with
 | H1: Znth _ (_++[Byte.zero]) = Byte.zero |- _ => idtac 
 | H1: Znth _ (_++[Byte.zero]) <> Byte.zero |- _ => idtac 
 | |- _ => fail "The cstring tactic expects to see one of the following hypotheses above the line:
Znth _ (_++[Byte.zero]) = Byte.zero
Znth _ (_++[Byte.zero]) <> Byte.zero"
 end;
 (pose_Zlength_nonneg;
  apply Classical_Prop.NNPP; intro;
  match goal with
  | H: ~In Byte.zero ?ls, H1: Znth ?i (?ls' ++ [Byte.zero]) = Byte.zero |- _ =>
     constr_eq ls ls'; apply H; rewrite <- H1;  
    rewrite app_Znth1 by omega; apply Znth_In; omega
  | H: ~In Byte.zero ?ls, H1: Znth ?i (?ls' ++ [Byte.zero]) <> Byte.zero |- _ =>
     constr_eq ls ls'; apply H1;
     rewrite app_Znth2 by omega; apply Znth_zero_zero
  end) || 
  match goal with |- @eq ?t (?f1 _) (?f2 _) =>
       (unify t Z || unify t nat) ||
       (constr_eq f1 f2;
        fail "The cstring tactic solves omega-style goals.
Your goal is an equality at type" t ", not type Z.
Try the [f_equal] tactic first.")
 end.

Ltac progress_entailer :=
 lazymatch goal with
 | |- @derives mpred _ ?A ?B => 
     entailer!; try match goal with |- @derives mpred _ A B => fail 2 end
 | |- _ => progress entailer!
 end.

Ltac cstring' := 
lazymatch goal with
| |- @eq Z _ _ => cstring
| |- ?A _ = ?B _ => constr_eq A B; f_equal; cstring'
| |- _ => cstring
end.

Ltac cstring1 :=
match goal with 
| H: 0 <= ?x < Zlength ?s + 1,
  H1: Znth ?x (?s ++ [Byte.zero]) = Byte.zero |- _ =>
  is_var x; assert  (x = Zlength s) by cstring; subst x
end.

