Require Import compcert.common.Memory.
Require Import VST.msl.Coqlib2.
Require Import VST.msl.eq_dec.
Require Import VST.msl.ageable.
Require Import VST.msl.age_to.
Require Import VST.veric.coqlib4.
Require Import VST.veric.juicy_mem.
Require Import VST.veric.compcert_rmaps. 
Require Import VST.veric.seplog.
Require Import VST.veric.juicy_extspec.
Require Import VST.veric.mem_lessdef.
Require Import VST.veric.age_to_resource_at.

Set Bullet Behavior "Strict Subproofs".

Ltac hered :=
  match goal with
    H : ?P ?x |- ?P ?y => revert H
  end;
  match goal with
    |- ?P ?x -> ?P ?y =>
    cut (hereditary age P);
    [ let h := fresh "h" in intros h; apply h; auto | ]
  end.

Ltac agejoinhyp :=
  match goal with
    H : sepalg.join _ _ ?m, A : age ?m _ |- _ =>
    pose proof age1_join2 _ H A; clear H
  end.

Ltac agehyps :=
  match goal with
    H : age ?x ?y, HH : ?P ?x |- _ =>
    cut (P y);
    [ clear HH; intros HH
    | hered;
      try apply pred_hered;
      try apply predicates_hered.exactly_obligation_1]
  end.

(** * Aging and predicates *)

Lemma hereditary_func_at' loc fs :
  hereditary age (func_at' fs loc).
Proof.
(* Goal: @hereditary rmap (@age rmap ag_rmap) (@app_pred rmap ag_rmap (func_at' fs loc)) *)
  apply pred_hered.
Qed.

Lemma anti_hereditary_func_at' loc fs :
  hereditary (fun x y => age y x) (func_at' fs loc).
Proof.
(* Goal: @hereditary rmap (fun x y : rmap => @age rmap ag_rmap y x) (@app_pred rmap ag_rmap (func_at' fs loc)) *)
  intros x y a; destruct fs as [f cc A P Q]; simpl.
(* Goal: forall _ : @ex preds (fun b : preds => @eq resource (resource_at x loc) (PURE (FUN f cc) (preds_fmap (approx (@level rmap ag_rmap x)) (approx (@level rmap ag_rmap x)) b))), @ex preds (fun b : preds => @eq resource (resource_at y loc) (PURE (FUN f cc) (preds_fmap (approx (@level rmap ag_rmap y)) (approx (@level rmap ag_rmap y)) b))) *)
  intros [pp E].
(* Goal: @ex preds (fun b : preds => @eq resource (resource_at y loc) (PURE (FUN f cc) (preds_fmap (approx (@level rmap ag_rmap y)) (approx (@level rmap ag_rmap y)) b))) *)
  destruct (proj2 (age1_PURE _ _ loc (FUN f cc) a)) as [pp' Ey]; eauto.
(* Goal: @ex preds (fun b : preds => @eq resource (resource_at y loc) (PURE (FUN f cc) (preds_fmap (approx (@level rmap ag_rmap y)) (approx (@level rmap ag_rmap y)) b))) *)
  pose proof resource_at_approx y loc as H.
(* Goal: @ex preds (fun b : preds => @eq resource (resource_at y loc) (PURE (FUN f cc) (preds_fmap (approx (@level rmap ag_rmap y)) (approx (@level rmap ag_rmap y)) b))) *)
  rewrite Ey in H at 1; simpl in H.
(* Goal: @ex preds (fun b : preds => @eq resource (resource_at y loc) (PURE (FUN f cc) (preds_fmap (approx (@level rmap ag_rmap y)) (approx (@level rmap ag_rmap y)) b))) *)
  rewrite <-H.
(* Goal: @ex preds (fun b : preds => @eq resource (PURE (FUN f cc) (preds_fmap (approx (@level rmap ag_rmap y)) (approx (@level rmap ag_rmap y)) pp')) (PURE (FUN f cc) (preds_fmap (approx (@level rmap ag_rmap y)) (approx (@level rmap ag_rmap y)) b))) *)
  exists pp'.
(* Goal: @eq rmap (m_phi (@age_by O juicy_mem juicy_mem_ageable jm)) (@age_by O rmap ag_rmap (m_phi jm)) *)
(* Goal: @eq rmap (m_phi (@age_by (S n) juicy_mem juicy_mem_ageable jm)) (@age_by (S n) rmap ag_rmap (m_phi jm)) *)
  reflexivity.
Qed.

Lemma pures_eq_unage {phi1 phi1' phi2}:
  ge (level phi1') (level phi2) ->
  age phi1 phi1' ->
  juicy_safety.pures_eq phi1' phi2 ->
  juicy_safety.pures_eq phi1 phi2.
Proof.
(* Goal: forall (_ : ge (@level rmap ag_rmap phi1') (@level rmap ag_rmap phi2)) (_ : @age rmap ag_rmap phi1 phi1') (_ : juicy_safety.pures_eq phi1' phi2), juicy_safety.pures_eq phi1 phi2 *)
  intros L A [S P]; split; intros loc; [clear P; autospec S | clear S; autospec P ].
  - rewrite (age_resource_at A) in S.
(* Goal: match resource_at phi1 loc with | NO sh n => True | YES sh r k p => True | PURE k pp => @eq resource (resource_at phi2 loc) (PURE k (preds_fmap (approx (@level rmap ag_rmap phi2)) (approx (@level rmap ag_rmap phi2)) pp)) end *)
    destruct (phi1 @ loc) eqn:E; auto.
(* Goal: @eq resource (resource_at phi2 loc) (PURE k (preds_fmap (approx (@level rmap ag_rmap phi2)) (approx (@level rmap ag_rmap phi2)) p)) *)
    simpl in S.
(* Goal: @eq resource (resource_at phi2 loc) (PURE k (preds_fmap (approx (@level rmap ag_rmap phi2)) (approx (@level rmap ag_rmap phi2)) p)) *)
    rewrite S.
(* Goal: @eq resource (PURE k (preds_fmap (approx (@level rmap ag_rmap phi2)) (approx (@level rmap ag_rmap phi2)) (preds_fmap (approx (@level rmap ag_rmap phi1')) (approx (@level rmap ag_rmap phi1')) p))) (PURE k (preds_fmap (approx (@level rmap ag_rmap phi2)) (approx (@level rmap ag_rmap phi2)) p)) *)
    rewrite preds_fmap_fmap.
(* Goal: @eq resource (PURE k (preds_fmap (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx (@level rmap ag_rmap phi2)) (approx (@level rmap ag_rmap phi1'))) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx (@level rmap ag_rmap phi1')) (approx (@level rmap ag_rmap phi2))) p)) (PURE k (preds_fmap (approx (@level rmap ag_rmap phi2)) (approx (@level rmap ag_rmap phi2)) p)) *)
    rewrite approx_oo_approx'; auto.
(* Goal: @eq resource (PURE k (preds_fmap (approx (@level rmap ag_rmap phi2)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx (@level rmap ag_rmap phi1')) (approx (@level rmap ag_rmap phi2))) p)) (PURE k (preds_fmap (approx (@level rmap ag_rmap phi2)) (approx (@level rmap ag_rmap phi2)) p)) *)
    rewrite approx'_oo_approx; auto.
  - destruct (phi2 @ loc) eqn:E; auto.
(* Goal: @ex preds (fun pp : preds => @eq resource (resource_at phi1 loc) (PURE k pp)) *)
    revert P.
(* Goal: forall _ : @ex preds (fun pp : preds => @eq resource (resource_at phi1' loc) (PURE k pp)), @ex preds (fun pp : preds => @eq resource (resource_at phi1 loc) (PURE k pp)) *)
    eapply age1_PURE. auto.
Qed.

(** * Aging and operational steps *)

Lemma jstep_age_sim {C} {csem : @semantics.CoreSemantics C mem} {c c' jm1 jm2 jm1'} :
  age jm1 jm2 ->
  jstep csem c jm1 c' jm1' ->
  level jm2 <> O ->
  exists jm2',
    age jm1' jm2' /\
    jstep csem c jm2 c' jm2'.
Proof.
(* Goal: forall (_ : @age juicy_mem juicy_mem_ageable jm1 jm2) (_ : @jstep C csem c jm1 c' jm1') (_ : not (@eq nat (@level juicy_mem juicy_mem_ageable jm2) O)), @ex juicy_mem (fun jm2' : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm1' jm2') (@jstep C csem c jm2 c' jm2')) *)
  intros A [step [rd [lev Hg]]] nz.
(* Goal: @ex juicy_mem (fun jm2' : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm1' jm2') (@jstep C csem c jm2 c' jm2')) *)
  destruct (age1 jm1') as [jm2'|] eqn:E.
  - exists jm2'. split; auto.
(* Goal: @eq nat (@level rmap ag_rmap (m_phi jm1)) (S (@level rmap ag_rmap (m_phi jm1'))) *)
    split; [|split; [|split]]; auto.
    + exact_eq step.
(* Goal: @eq nat (@level rmap ag_rmap (m_phi jm1)) (S (@level rmap ag_rmap (m_phi jm1'))) *)
      f_equal; apply age_jm_dry; auto.
    + eapply (age_resource_decay _ (m_phi jm1) (m_phi jm1')).
      * exact_eq rd.
(* Goal: @eq nat (@level rmap ag_rmap (m_phi jm1)) (S (@level rmap ag_rmap (m_phi jm1'))) *)
        f_equal. f_equal. apply age_jm_dry; auto.
(* Goal: @eq nat (@level rmap ag_rmap (m_phi jm1)) (S (@level rmap ag_rmap (m_phi jm1'))) *)
      * apply age_jm_phi; auto.
(* Goal: @eq nat (@level rmap ag_rmap (m_phi jm1)) (S (@level rmap ag_rmap (m_phi jm1'))) *)
      * apply age_jm_phi; auto.
(* Goal: @eq nat (@level rmap ag_rmap (m_phi jm1)) (S (@level rmap ag_rmap (m_phi jm1'))) *)
      * rewrite level_juice_level_phi in *. auto.
    + apply age_level in E.
(* Goal: @ex juicy_mem (fun jm2' : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm1' jm2') (@jstep C csem c jm2 c' jm2')) *)
      apply age_level in A.
(* Goal: le n (@level juicy_mem juicy_mem_ageable y) *)
      omega.
    + rewrite (age1_ghost_of _ _ (age_jm_phi A)), (age1_ghost_of _ _ (age_jm_phi E)), Hg.
(* Goal: @eq ghost (ghost_fmap (approx (@level rmap ag_rmap (m_phi jm2'))) (approx (@level rmap ag_rmap (m_phi jm2'))) (ghost_fmap (approx (@level juicy_mem juicy_mem_ageable jm1')) (approx (@level juicy_mem juicy_mem_ageable jm1')) (ghost_of (m_phi jm1)))) (ghost_fmap (approx (@level juicy_mem juicy_mem_ageable jm2')) (approx (@level juicy_mem juicy_mem_ageable jm2')) (ghost_fmap (approx (@level rmap ag_rmap (m_phi jm2))) (approx (@level rmap ag_rmap (m_phi jm2))) (ghost_of (m_phi jm1)))) *)
      apply age_level in A; rewrite A in lev; inv lev.
(* Goal: @eq ghost (ghost_fmap (approx (@level rmap ag_rmap (m_phi jm2'))) (approx (@level rmap ag_rmap (m_phi jm2'))) (ghost_fmap (approx (@level juicy_mem juicy_mem_ageable jm1')) (approx (@level juicy_mem juicy_mem_ageable jm1')) (ghost_of (m_phi jm1)))) (ghost_fmap (approx (@level juicy_mem juicy_mem_ageable jm2')) (approx (@level juicy_mem juicy_mem_ageable jm2')) (ghost_fmap (approx (@level rmap ag_rmap (m_phi jm2))) (approx (@level rmap ag_rmap (m_phi jm2))) (ghost_of (m_phi jm1)))) *)
      rewrite !level_juice_level_phi; congruence.
  - apply age1_level0 in E.
(* Goal: @ex juicy_mem (fun jm2' : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm1' jm2') (@jstep C csem c jm2 c' jm2')) *)
    apply age_level in A.
(* Goal: le n (@level juicy_mem juicy_mem_ageable y) *)
    omega.
Qed.

Lemma jsafeN__age {G C Z HH Sem Jspec ge ora q n} jm jmaged :
  ext_spec_stable age (JE_spec _ Jspec) ->
  age jm jmaged ->
  le n (level jmaged) ->
  @jsafeN_ G Z C HH Sem Jspec ge n ora q jm ->
  @jsafeN_ G Z C HH Sem Jspec ge n ora q jmaged.
Proof.
  revert q jm jmaged; induction n.
  - constructor 1.
  - intros ??? heredspec A L Safe.
    inv Safe.
    + destruct (jstep_age_sim A H0 ltac:(omega)) as [jmaged' [A' step']].
(* Goal: @eq nat (@level rmap ag_rmap (m_phi jm1)) (S (@level rmap ag_rmap (m_phi jm1'))) *)
      econstructor 2; eauto.
      intros gh Hg J.
      rewrite (age1_ghost_of _ _ (age_jm_phi A')) in J.
      destruct (own.ghost_joins_approx _ _ _ J) as (J' & Hd').
      rewrite <- level_juice_level_phi in *.
      rewrite <- (age_level _ _ A') in *.
      rewrite level_juice_level_phi, ghost_of_approx in J'.
(* Goal: @eq nat (@level rmap ag_rmap (m_phi jm1)) (S (@level rmap ag_rmap (m_phi jm1'))) *)
      destruct (H1 (own.make_join (ghost_of (m_phi m')) gh)) as (b & ? & Hupd & Hsafe); auto.
(* Goal: @eq nat (@level rmap ag_rmap (m_phi jm1)) (S (@level rmap ag_rmap (m_phi jm1'))) *)
      { eapply make_join_ext; eauto. }
      destruct (jm_update_age _ _ _ Hupd A') as (b' & Hupd' & Hage').
(* Goal: @eq nat (@level rmap ag_rmap (m_phi jm1)) (S (@level rmap ag_rmap (m_phi jm1'))) *)
      eapply IHn in Hsafe; eauto.
      eexists; split; [|eauto].
      rewrite (age1_ghost_of _ _ (age_jm_phi Hage')).
      rewrite <- level_juice_level_phi.
      destruct Hupd' as (_ & -> & _); auto.
      { destruct Hupd' as (_ & -> & _).
        apply age_level in A'.
        destruct H0 as (? & ? & ? & ?).
(* Goal: @ex juicy_mem (fun jm2' : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm1' jm2') (@jstep C csem c jm2 c' jm2')) *)
        apply age_level in A.
(* Goal: le n (@level juicy_mem juicy_mem_ageable y) *)
        omega. }
    + econstructor 3.
      * unfold j_at_external in *; rewrite <- (age_jm_dry A); eassumption. 
(* Goal: @eq nat (@level rmap ag_rmap (m_phi jm1)) (S (@level rmap ag_rmap (m_phi jm1'))) *)
      * eapply (proj1 heredspec); eauto.
      * intros ret jm' z' n' Hargsty Hretty H rel post.
(* Goal: @eq nat (@level rmap ag_rmap (m_phi jm1)) (S (@level rmap ag_rmap (m_phi jm1'))) *)
        destruct (H2 ret jm' z' n' Hargsty Hretty H) as (c' & atex' & safe'); eauto.
        unfold Hrel in *.
        split;[|split]; try apply rel.
        -- apply age_level in A; omega.
        -- apply age_jm_phi in A.
           unshelve eapply (pures_eq_unage _ A), rel.
           do 2 rewrite <-level_juice_level_phi.
(* Goal: le n (@level juicy_mem juicy_mem_ageable y) *)
           omega.
(* Goal: @eq nat (@level rmap ag_rmap (m_phi jm1)) (S (@level rmap ag_rmap (m_phi jm1'))) *)
    + econstructor 4. eauto.
(* Goal: @eq nat (@level rmap ag_rmap (m_phi jm1)) (S (@level rmap ag_rmap (m_phi jm1'))) *)
      eapply (proj2 heredspec); eauto.
Qed.

Lemma jsafeN__age_to {G C Z HH Sem Jspec ge ora q n} l jm :
  ext_spec_stable age (JE_spec _ Jspec) ->
  le n l ->
  @jsafeN_ G Z C HH Sem Jspec ge n ora q jm ->
  @jsafeN_ G Z C HH Sem Jspec ge n ora q (age_to l jm).
Proof.
(* Goal: forall (_ : @ext_spec_stable juicy_mem external_function C (@age juicy_mem juicy_mem_ageable) (JE_spec C Jspec)) (_ : le n l) (_ : @jsafeN_ G Z C HH Sem Jspec ge n ora q jm), @jsafeN_ G Z C HH Sem Jspec ge n ora q (@age_to l juicy_mem juicy_mem_ageable jm) *)
  intros Stable nl.
(* Goal: forall _ : @jsafeN_ G Z C HH Sem Jspec ge n ora q jm, @jsafeN_ G Z C HH Sem Jspec ge n ora q (@age_to l juicy_mem juicy_mem_ageable jm) *)
  apply age_to_ind_refined.
(* Goal: forall (x y : juicy_mem) (_ : @age juicy_mem juicy_mem_ageable x y) (_ : le l (@level juicy_mem juicy_mem_ageable y)) (_ : @jsafeN_ G Z C HH Sem Jspec ge n ora q x), @jsafeN_ G Z C HH Sem Jspec ge n ora q y *)
  intros x y H L.
(* Goal: @eq nat (@level rmap ag_rmap (m_phi jm1)) (S (@level rmap ag_rmap (m_phi jm1'))) *)
  apply jsafeN__age; auto.
(* Goal: le n (@level juicy_mem juicy_mem_ageable y) *)
  omega.
Qed.

Lemma m_dry_age_to n jm : m_dry (age_to n jm) = m_dry jm.
Proof.
(* Goal: @eq Mem.mem (m_dry (@age_to n juicy_mem juicy_mem_ageable jm)) (m_dry jm) *)
  remember (m_dry jm) as m eqn:E; symmetry; revert E.
(* Goal: @eq nat (@level rmap ag_rmap (m_phi jm1)) (S (@level rmap ag_rmap (m_phi jm1'))) *)
  apply age_to_ind; auto.
  intros x y H E ->. rewrite E; auto. clear E.
(* Goal: @eq nat (@level rmap ag_rmap (m_phi jm1)) (S (@level rmap ag_rmap (m_phi jm1'))) *)
  apply age_jm_dry; auto.
Qed.

Lemma m_phi_age_to n jm : m_phi (age_to n jm) = age_to n (m_phi jm).
Proof.
(* Goal: @eq rmap (m_phi (@age_to n juicy_mem juicy_mem_ageable jm)) (@age_to n rmap ag_rmap (m_phi jm)) *)
  unfold age_to.
(* Goal: @eq rmap (m_phi (@age_by (Init.Nat.sub (@level juicy_mem juicy_mem_ageable jm) n) juicy_mem juicy_mem_ageable jm)) (@age_by (Init.Nat.sub (@level rmap ag_rmap (m_phi jm)) n) rmap ag_rmap (m_phi jm)) *)
  rewrite level_juice_level_phi.
  generalize (level (m_phi jm) - n)%nat; clear n.
(* Goal: @eq rmap (m_phi (@age_by O juicy_mem juicy_mem_ageable jm)) (@age_by O rmap ag_rmap (m_phi jm)) *)
(* Goal: @eq rmap (m_phi (@age_by (S n) juicy_mem juicy_mem_ageable jm)) (@age_by (S n) rmap ag_rmap (m_phi jm)) *)
  intros n; induction n. reflexivity.
  simpl. rewrite <- IHn.
(* Goal: @eq rmap (m_phi (@age1' juicy_mem juicy_mem_ageable (@age_by n juicy_mem juicy_mem_ageable jm))) (@age1' rmap ag_rmap (m_phi (@age_by n juicy_mem juicy_mem_ageable jm))) *)
  clear IHn. generalize (age_by n jm); clear jm; intros jm.
(* Goal: @eq rmap (m_phi (@age1' juicy_mem juicy_mem_ageable jm)) (@age1' rmap ag_rmap (m_phi jm)) *)
  unfold age1'.
(* Goal: @eq rmap (m_phi match @age1 juicy_mem juicy_mem_ageable jm with | Some y => y | None => jm end) match @age1 rmap ag_rmap (m_phi jm) with | Some y => y | None => m_phi jm end *)
  destruct (age1 jm) as [jm'|] eqn:e.
  - rewrite (age1_juicy_mem_Some _ _ e). easy.
  - rewrite (age1_juicy_mem_None1 _ e). easy.
Qed.