Require Import VST.veric.juicy_base.
Require Import VST.veric.juicy_mem VST.veric.juicy_mem_lemmas VST.veric.juicy_mem_ops.
Require Import VST.veric.res_predicates.
Require Import VST.veric.extend_tc.
Require Import VST.veric.Clight_seplog.
Require Import VST.veric.Clight_assert_lemmas.
Require Import VST.veric.Clight_new.
Require Import VST.veric.Clight_lemmas.
Require Import VST.sepcomp.extspec.
Require Import VST.sepcomp.step_lemmas.
Require Import VST.veric.juicy_safety.
Require Import VST.veric.juicy_extspec.
Require Import VST.veric.tycontext.
Require Import VST.veric.expr2.
Require Import VST.veric.expr_lemmas.
Require Import VST.veric.own.

Local Open Scope nat_scope.
Local Open Scope pred.

Definition closed_wrt_modvars c (F: assert) : Prop :=
    closed_wrt_vars (modifiedvars c) F.

Definition genv_symb_injective {F V} (ge: Genv.t F V) : extspec.injective_PTree block.
Proof.
(* Goal: injective_PTree block *)
exists (Genv.genv_symb ge).
(* Goal: @PTree_injective block (@Genv.genv_symb F V ge) *)
hnf; intros.
(* Goal: @eq positive id1 id2 *)
eapply Genv.genv_vars_inj; eauto.
Defined.

(* Goal: @joins ghost ghost_join (ghost_of (m_phi jm0)) (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref (@OK_ty Espec) ora) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora (State ve te ctl) jm *)
Definition jsafeN {Z} (Hspec : juicy_ext_spec Z) (ge: genv) :=
  @jsafeN_ genv _ _ genv_symb_injective (*(genv_symb := fun ge: genv => Genv.genv_symb ge)*)
               (cl_core_sem ge) Hspec ge.

(* Goal: @joins ghost ghost_join (ghost_of (m_phi jm0)) (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref (@OK_ty Espec) ora) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora (State ve te ctl) jm *)
Lemma ext_join_approx : forall {Z} (z : Z) n g,
  joins g (Some (ghost_PCM.ext_ref z, NoneP) :: nil) ->
  joins (ghost_fmap (approx n) (approx n) g) (Some (ghost_PCM.ext_ref z, NoneP) :: nil).
Proof.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
  intros.
(* Goal: @app_pred A agA (@andp A agA (@unfash A agA P) (@unfash A agA Q)) a *)
(* Goal: @derives A agA (@andp A agA (@unfash A agA P) (@unfash A agA Q)) (@unfash A agA (@andp nat ag_nat P Q)) *)
  destruct H.
  change (Some (ghost_PCM.ext_ref z, NoneP) :: nil) with
    (ghost_fmap (approx n) (approx n) (Some (ghost_PCM.ext_ref z, NoneP) :: nil)).
(* Goal: @joins ghost ghost_join (ghost_fmap (approx n) (approx n) g) (ghost_fmap (approx n) (approx n) (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref Z z) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds))))) *)
  eexists; apply ghost_fmap_join; eauto.
Qed.

(* Goal: @joins ghost ghost_join (ghost_of (m_phi jm0)) (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref (@OK_ty Espec) ora) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora (State ve te ctl) jm *)
Lemma ext_join_unapprox : forall {Z} (z : Z) n g,
  joins (ghost_fmap (approx n) (approx n) g) (Some (ghost_PCM.ext_ref z, NoneP) :: nil) ->
  joins g (Some (ghost_PCM.ext_ref z, NoneP) :: nil).
Proof.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
  intros.
(* Goal: @joins ghost ghost_join g (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref Z z) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
  destruct H as (g' & J).
(* Goal: @joins ghost ghost_join g (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref Z z) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
  destruct g; [eexists; constructor|].
(* Goal: @joins ghost ghost_join (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) o g) (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref Z z) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
  inv J.
(* Goal: @joins ghost ghost_join (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) o g) (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref Z z) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
  exists (a3 :: g); repeat constructor.
(* Goal: @join (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Join_lower (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (Join_prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) ghost_elem_join preds preds_join)) o (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref Z z) NoneP)) a3 *)
  destruct o; inv H4; constructor.
(* Goal: @join (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (Join_prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) ghost_elem_join preds preds_join) p (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref Z z) NoneP) a0 *)
  destruct p; inv H1; constructor; simpl in *; auto.
(* Goal: @join preds preds_join p NoneP (@snd (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds a0) *)
  destruct p; simpl in *.
(* Goal: @join preds preds_join (SomeP A _f) NoneP (@snd (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds a0) *)
  inv H0.
(* Goal: @join preds preds_join (SomeP A _f) NoneP (@snd (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds a0) *)
  inv H1.
(* Goal: @join preds preds_join (SomeP (ConstType unit) _f) NoneP (@snd (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds a0) *)
  inj_pair_tac.
(* Goal: @join preds preds_join (SomeP (ConstType unit) _f) NoneP (@snd (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds a0) *)
  constructor; auto.
(* Goal: @eq preds (SomeP (ConstType unit) _f) NoneP *)
  unfold NoneP; f_equal; auto.
Qed.

(* Goal: @joins ghost ghost_join (ghost_of (m_phi jm0)) (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref (@OK_ty Espec) ora) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora (State ve te ctl) jm *)
Program Definition ext_compat {Z} (ora : Z) : mpred :=
  fun w => joins (ghost_of w) (Some (ghost_PCM.ext_ref ora, NoneP) :: nil).
Next Obligation.
Proof.
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
  repeat intro.
(* Goal: @joins ghost ghost_join (ghost_of a') (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref Z ora) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
  erewrite age1_ghost_of by eauto.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) (ghost_of a)) (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref Z ora) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
  apply ext_join_approx; auto.
Qed.

Program Definition assert_safe
     (Espec : OracleKind)
     (ge: genv) ve te (ctl: cont) : assert :=
  fun rho => bupd (fun w => forall ora (jm:juicy_mem),
       ext_compat ora w ->
       rho = construct_rho (filter_genv ge) ve te ->
       m_phi jm = w ->
             jsafeN (@OK_spec Espec) ge (level w) ora (State ve te ctl) jm).
 Next Obligation.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
  intro; intros.
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora (State ve te ctl) jm *)
  subst.
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora (State ve te ctl) jm *)
   destruct (oracle_unage _ _ H) as [jm0 [? ?]].
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora (State ve te ctl) jm *)
   subst.
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora (State ve te ctl) jm *)
   specialize (H0 ora jm0); spec H0.
(* Goal: @joins ghost ghost_join (ghost_of (m_phi jm0)) (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref (@OK_ty Espec) ora) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora (State ve te ctl) jm *)
   { erewrite age1_ghost_of in H1 by eauto.
(* Goal: @joins ghost ghost_join (ghost_of (m_phi jm0)) (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref (@OK_ty Espec) ora) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
      eapply ext_join_unapprox; eauto. }
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora (State ve te ctl) jm *)
   specialize (H0 (eq_refl _) (eq_refl _)).
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora (State ve te ctl) jm *)
   forget (State ve te ctl) as c. clear H ve te ctl.
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora c jm *)
  change (level (m_phi jm)) with (level jm).
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level juicy_mem juicy_mem_ageable jm) ora c jm *)
  change (level (m_phi jm0)) with (level jm0) in H0.
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level juicy_mem juicy_mem_ageable jm) ora c jm *)
  eapply age_safe; eauto.
Qed.

(* Goal: @joins ghost ghost_join (ghost_of (m_phi jm0)) (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref (@OK_ty Espec) ora) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora (State ve te ctl) jm *)
Definition list2opt {T: Type} (vl: list T) : option T :=
 match vl with nil => None | x::_ => Some x end.

Definition match_venv (ve: venviron) (vars: list (ident * type)) :=
 forall id, match ve id with Some (b,t) => In (id,t) vars | _ => True end.

Definition guard_environ (Delta: tycontext) (f: option function) (rho: environ) : Prop :=
   typecheck_environ Delta rho /\
  match f with
  | Some f' => match_venv (ve_of rho) (fn_vars f')
                /\ ret_type Delta = fn_return f'
  | None => True
  end.

Lemma guard_environ_e1:
   forall Delta f rho, guard_environ Delta f rho ->
     typecheck_environ Delta rho.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
Proof. intros. destruct H; auto. Qed.

Definition _guard (Espec : OracleKind)
    (gx: genv) (Delta: tycontext) (P : assert) (f: option function) (ctl: cont) : pred nat :=
     ALL tx : Clight.temp_env, ALL vx : env,
          let rho := construct_rho (filter_genv gx) vx tx in
          !! guard_environ Delta f rho
                  && P rho && funassert Delta rho
             >=> assert_safe Espec gx vx tx ctl rho.

Definition guard (Espec : OracleKind)
    (gx: genv) (Delta: tycontext) (P : assert)  (ctl: cont) : pred nat :=
  _guard Espec gx Delta P (current_function ctl) ctl.

Definition zap_fn_return (f: function) : function :=
 mkfunction Tvoid f.(fn_callconv) f.(fn_params) f.(fn_vars) f.(fn_temps) f.(fn_body).

Definition exit_cont (ek: exitkind) (vl: option val) (k: cont) : cont :=
  match ek with
  | EK_normal => k
  | EK_break => break_cont k
  | EK_continue => continue_cont k
  | EK_return =>
         match vl, call_cont k with
         | Some v, Kcall (Some x) f ve te :: k' =>
                    Kseq (Sreturn None) :: Kcall None (zap_fn_return f) ve (PTree.set x v te) :: k'
         | _,_ => Kseq (Sreturn None) :: call_cont k
         end
   end.

Definition rguard (Espec : OracleKind)
    (gx: genv) (Delta: tycontext)  (R : ret_assert) (ctl: cont) : pred nat :=
  ALL ek: exitkind, ALL vl: option val,
    _guard Espec gx Delta (proj_ret_assert R ek vl) (current_function ctl) (exit_cont ek vl ctl).

(* Goal: @joins ghost ghost_join (ghost_of (m_phi jm0)) (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref (@OK_ty Espec) ora) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora (State ve te ctl) jm *)
Record semaxArg :Type := SemaxArg {
 sa_Delta: tycontext;
 sa_P: assert;
 sa_c: statement;
 sa_R: ret_assert
}.

Definition ext_spec_pre' (Espec: OracleKind) (ef: external_function)
   (x': ext_spec_type OK_spec ef) (ge_s: injective_PTree block)
   (ts: list typ) (args: list val) (z: OK_ty) : pred juicy_mem :=
  exist (hereditary age)
     (ext_spec_pre OK_spec ef x' ge_s ts args z)
     (JE_pre_hered _ _ _ _ _ _ _ _).

Program Definition ext_spec_post' (Espec: OracleKind)
   (ef: external_function) (x': ext_spec_type OK_spec ef) (ge_s: injective_PTree block)
   (tret: option typ) (ret: option val) (z: OK_ty) : pred juicy_mem :=
  exist (hereditary age)
   (ext_spec_post OK_spec ef x' ge_s tret ret z)
     (JE_post_hered _ _ _ _ _ _ _ _).

Definition juicy_mem_pred (P : pred rmap) (jm: juicy_mem): pred nat :=
     # diamond fashionM (exactly (m_phi jm) && P).

Fixpoint make_ext_args (gx: genviron) (ids: list ident) (vl: list val)  :=
  match ids, vl with
  | id::ids', v::vl' => env_set (make_ext_args gx ids' vl') id v
  | _, v::vl' => env_set (make_ext_args gx ids vl') 1%positive v
  | _, _ => mkEnviron gx (Map.empty _) (Map.empty _)
 end.

Definition make_ext_rval  (gx: genviron) (v: option val):=
  match v with
  | Some v' =>  mkEnviron gx (Map.empty _)
                              (Map.set 1%positive v' (Map.empty _))
  | None => mkEnviron gx (Map.empty _) (Map.empty _)
  end.

Definition semax_external
  (Hspec: OracleKind) (ids: list ident) ef
  (A: TypeTree)
  (P Q: forall ts, dependent_type_functor_rec ts (AssertTT A) (pred rmap)):
        pred nat :=
 ALL gx: genv, ALL Ts: list Type,
 ALL x: (dependent_type_functor_rec Ts A (pred rmap)),
   |>  ALL F: pred rmap, ALL ts: list typ,
   ALL args: list val,
   !!Val.has_type_list args (sig_args (ef_sig ef)) &&
   juicy_mem_op (P Ts x (make_ext_args (filter_genv gx) ids args) * F) >=>
   EX x': ext_spec_type OK_spec ef,
    (ALL z:_, juicy_mem_op (ext_compat z) -->
     ext_spec_pre' Hspec ef x' (genv_symb_injective gx) ts args z) &&
     ! ALL tret: option typ, ALL ret: option val, ALL z': OK_ty,
      ext_spec_post' Hspec ef x' (genv_symb_injective gx) tret ret z' >=>
          juicy_mem_op (Q Ts x (make_ext_rval (filter_genv gx) ret) * F).

Definition tc_option_val (sig: type) (ret: option val) :=
  match sig, ret with
    | Tvoid, None => True
    | Tvoid, Some _ => False
    | ty, Some v => tc_val ty v
    | _, _ => False
  end.

(* Goal: @joins ghost ghost_join (ghost_of (m_phi jm0)) (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref (@OK_ty Espec) ora) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora (State ve te ctl) jm *)
Fixpoint zip_with_tl {A : Type} (l1 : list A) (l2 : typelist) : list (A*type) :=
  match l1, l2 with
    | a::l1', Tcons b l2' => (a,b)::zip_with_tl l1' l2'
    | _, _ => nil
  end.

Definition believe_external (Hspec: OracleKind) (gx: genv) (v: val) (fsig: funsig) cc
  (A: TypeTree)
  (P Q: forall ts, dependent_type_functor_rec ts (AssertTT A) (pred rmap)):
  pred nat :=
  match Genv.find_funct gx v with
  | Some (External ef sigargs sigret cc') =>
      let ids := fst (split (fst fsig)) in
        !! (fsig = (zip_with_tl ids sigargs, sigret) /\ cc'=cc
           /\ ef_sig ef = mksignature
                           (typlist_of_typelist (type_of_params (fst fsig)))
                           (opttyp_of_type (snd fsig)) cc
           /\ length (typelist2list sigargs)=length ids)
        && semax_external Hspec ids ef A P Q
        && ! (ALL ts: list Type,
              ALL x: dependent_type_functor_rec ts A (pred rmap),
              ALL ret:option val,
                Q ts x (make_ext_rval (filter_genv gx) ret)
                  && !!has_opttyp ret (opttyp_of_type (snd fsig))
                  >=> !! tc_option_val sigret ret)
  | _ => FF
  end.

Definition fn_funsig (f: function) : funsig := (fn_params f, fn_return f).

Definition var_sizes_ok (cenv: composite_env) (vars: list (ident*type)) :=
   Forall (fun var : ident * type => @sizeof cenv (snd var) <= Ptrofs.max_unsigned)%Z vars.

Definition var_block' (sh: Share.t) (cenv: composite_env) (idt: ident * type) (rho: environ): mpred :=
  !! (sizeof (snd idt) <= Ptrofs.max_unsigned)%Z &&
  (memory_block sh (sizeof (snd idt))) (eval_lvar (fst idt) (snd idt) rho).

Definition stackframe_of' (cenv: composite_env) (f: Clight.function) : assert :=
  fold_right (fun P Q rho => P rho * Q rho) (fun rho => emp)
     (map (fun idt => var_block' Share.top cenv idt) (Clight.fn_vars f)).


Definition believe_internal_
  (semax:semaxArg -> pred nat)
  (gx: genv) (Delta: tycontext) v (fsig: funsig) cc (A: TypeTree)
  (P Q: forall ts, dependent_type_functor_rec ts (AssertTT A) (pred rmap)) : pred nat :=
  (EX b: block, EX f: function,
   prop (v = Vptr b Ptrofs.zero /\ Genv.find_funct_ptr gx b = Some (Internal f)
                 /\ Forall (fun it => complete_type (genv_cenv gx) (snd it) = true) (fn_vars f)
                 /\ list_norepet (map (@fst _ _) f.(fn_params) ++ map (@fst _ _) f.(fn_temps))
                 /\ list_norepet (map (@fst _ _) f.(fn_vars)) /\ var_sizes_ok (genv_cenv gx) (f.(fn_vars))
                 /\ fsig = fn_funsig f /\ f.(fn_callconv) = cc)
  && ALL ts: list Type,
     ALL x : dependent_type_functor_rec ts A (pred rmap),
           |> semax (SemaxArg  (func_tycontext' f Delta)
                                (fun rho => (bind_args f.(fn_params) f.(fn_vars) (P ts x) rho * stackframe_of' (genv_cenv gx) f rho)
                                             && funassert (func_tycontext' f Delta) rho)
                              (Ssequence f.(fn_body) (Sreturn None))
           (frame_ret_assert (function_body_ret_assert (fn_return f) (Q ts x)) (stackframe_of' (genv_cenv gx) f)))).

Definition empty_environ (ge: genv) := mkEnviron (filter_genv ge) (Map.empty _) (Map.empty _).

Definition claims (ge: genv) (Delta: tycontext) v fsig cc A P Q : Prop :=
  exists id HP HQ, (glob_specs Delta)!id = Some (mk_funspec fsig cc A P Q HP HQ) /\
    exists b, Genv.find_symbol ge id = Some b /\ v = Vptr b Ptrofs.zero.

Definition believepred (Espec: OracleKind) (semax: semaxArg -> pred nat)
              (Delta: tycontext) (gx: genv)  (Delta': tycontext) : pred nat :=
  ALL v:val, ALL fsig: funsig, ALL cc: calling_convention,
  ALL A: TypeTree,
  ALL P: forall ts, dependent_type_functor_rec ts (AssertTT A) mpred,
  ALL Q: forall ts, dependent_type_functor_rec ts (AssertTT A) mpred,
       !! claims gx Delta' v fsig cc A P Q  -->
      (believe_external Espec gx v fsig cc A P Q
        || believe_internal_ semax gx Delta v fsig cc A P Q).

(* Goal: @joins ghost ghost_join (ghost_of (m_phi jm0)) (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref (@OK_ty Espec) ora) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora (State ve te ctl) jm *)
Definition semax_  {CS: compspecs}  (Espec: OracleKind)
       (semax: semaxArg -> pred nat) (a: semaxArg) : pred nat :=
 match a with SemaxArg Delta P c R =>
  ALL gx: genv, ALL Delta': tycontext,
       !! (tycontext_sub Delta Delta' /\ genv_cenv gx = cenv_cs)-->
      (believepred Espec semax Delta' gx Delta') -->
     ALL k: cont, ALL F: assert,
       (!! (closed_wrt_modvars c F) &&
              rguard Espec gx Delta' (frame_ret_assert R F) k) -->
        guard Espec gx Delta' (fun rho => F rho * P rho) (Kseq c :: k)
  end.

(* Goal: @joins ghost ghost_join (ghost_of (m_phi jm0)) (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref (@OK_ty Espec) ora) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora (State ve te ctl) jm *)
Definition semax'  {CS: compspecs} (Espec: OracleKind) Delta P c R : pred nat :=
     HORec (semax_  Espec) (SemaxArg Delta P c R).

(* Goal: @joins ghost ghost_join (ghost_of (m_phi jm0)) (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref (@OK_ty Espec) ora) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora (State ve te ctl) jm *)
Definition believe_internal {CS: compspecs} (Espec:  OracleKind)
  (gx: genv) (Delta: tycontext) v (fsig: funsig) cc (A: TypeTree)
  (P Q: forall ts, dependent_type_functor_rec ts (AssertTT A) (pred rmap)) : pred nat :=
  (EX b: block, EX f: function,
   prop (v = Vptr b Ptrofs.zero /\ Genv.find_funct_ptr gx b = Some (Internal f)
                 /\ Forall (fun it => complete_type (genv_cenv gx) (snd it) = true) (fn_vars f)
                 /\ list_norepet (map (@fst _ _) f.(fn_params) ++ map (@fst _ _) f.(fn_temps))
                 /\ list_norepet (map (@fst _ _) f.(fn_vars)) /\ var_sizes_ok (genv_cenv gx) (f.(fn_vars))
                 /\ fsig = fn_funsig f /\ f.(fn_callconv) = cc)
  && ALL ts: list Type,
     ALL x : dependent_type_functor_rec ts A (pred rmap),
        |> semax' Espec (func_tycontext' f Delta)
                                (fun rho => (bind_args f.(fn_params) f.(fn_vars) (P ts x) rho * stackframe_of' (genv_cenv gx)  f rho)
                                             && funassert (func_tycontext' f Delta) rho)
                               (Ssequence f.(fn_body) (Sreturn None))
           (frame_ret_assert (function_body_ret_assert (fn_return f) (Q ts x)) (stackframe_of' (genv_cenv gx) f))).

(* Goal: @joins ghost ghost_join (ghost_of (m_phi jm0)) (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref (@OK_ty Espec) ora) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora (State ve te ctl) jm *)
Definition believe {CS: compspecs} (Espec:OracleKind)
              (Delta: tycontext) (gx: genv) (Delta': tycontext): pred nat :=
  ALL v:val, ALL fsig: funsig, ALL cc: calling_convention,
  ALL A: TypeTree,
  ALL P: (forall ts, dependent_type_functor_rec ts (AssertTT A) (pred rmap)),
  ALL Q: (forall ts, dependent_type_functor_rec ts (AssertTT A) (pred rmap)),
       !! claims gx Delta' v fsig cc A P Q  -->
      (believe_external Espec gx v fsig cc A P Q
        || believe_internal Espec gx Delta v fsig cc A P Q).

(* Goal: @joins ghost ghost_join (ghost_of (m_phi jm0)) (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref (@OK_ty Espec) ora) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora (State ve te ctl) jm *)
Lemma semax_fold_unfold : forall {CS: compspecs} (Espec : OracleKind),
  semax' Espec = fun Delta P c R =>
  ALL gx: genv, ALL Delta': tycontext,
       !! (tycontext_sub Delta Delta' /\ genv_cenv gx = cenv_cs) -->
       believe Espec Delta' gx Delta' -->
     ALL k: cont, ALL F: assert,
        (!! (closed_wrt_modvars c F) && rguard Espec gx Delta' (frame_ret_assert R F) k) -->
        guard Espec gx Delta' (fun rho => F rho * P rho) (Kseq c :: k).
Proof.
(* Goal: @derives A agA (@unfash A agA (@andp nat ag_nat P Q)) (@andp A agA (@unfash A agA P) (@unfash A agA Q)) *)
(* Goal: @derives A agA (@andp A agA (@unfash A agA P) (@unfash A agA Q)) (@unfash A agA (@andp nat ag_nat P Q)) *)
intros ? ?.
(* Goal: @eq (forall (_ : tycontext) (_ : assert) (_ : statement) (_ : ret_assert), @pred nat ag_nat) (@semax' CS Espec) (fun (Delta : tycontext) (P : assert) (c : statement) (R : ret_assert) => @allp nat ag_nat genv (fun gx : genv => @allp nat ag_nat tycontext (fun Delta' : tycontext => @imp nat ag_nat (@prop nat ag_nat (and (tycontext_sub Delta Delta') (@eq composite_env (genv_cenv gx) (@cenv_cs CS)))) (@imp nat ag_nat (@believe CS Espec Delta' gx Delta') (@allp nat ag_nat cont (fun k : cont => @allp nat ag_nat assert (fun F : assert => @imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars c F)) (rguard Espec gx Delta' (frame_ret_assert R F) k)) (guard Espec gx Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) (@cons cont' (Kseq c) k))))))))) *)
extensionality G P. extensionality c R.
(* Goal: @eq (@pred nat ag_nat) (@semax' CS Espec G P c R) (@allp nat ag_nat genv (fun gx : genv => @allp nat ag_nat tycontext (fun Delta' : tycontext => @imp nat ag_nat (@prop nat ag_nat (and (tycontext_sub G Delta') (@eq composite_env (genv_cenv gx) (@cenv_cs CS)))) (@imp nat ag_nat (@believe CS Espec Delta' gx Delta') (@allp nat ag_nat cont (fun k : cont => @allp nat ag_nat assert (fun F : assert => @imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars c F)) (rguard Espec gx Delta' (frame_ret_assert R F) k)) (guard Espec gx Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) (@cons cont' (Kseq c) k))))))))) *)
unfold semax'.
(* Goal: @eq (@pred nat ag_nat) (@HORec nat ag_nat semaxArg (@semax_ CS Espec) (SemaxArg G P c R)) (@allp nat ag_nat genv (fun gx : genv => @allp nat ag_nat tycontext (fun Delta' : tycontext => @imp nat ag_nat (@prop nat ag_nat (and (tycontext_sub G Delta') (@eq composite_env (genv_cenv gx) (@cenv_cs CS)))) (@imp nat ag_nat (@believe CS Espec Delta' gx Delta') (@allp nat ag_nat cont (fun k : cont => @allp nat ag_nat assert (fun F : assert => @imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars c F)) (rguard Espec gx Delta' (frame_ret_assert R F) k)) (guard Espec gx Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) (@cons cont' (Kseq c) k))))))))) *)
pattern (HORec (semax_ Espec)) at 1; rewrite HORec_fold_unfold.
(* Goal: @eq (@pred nat ag_nat) (@semax_ CS Espec (@HORec nat ag_nat semaxArg (@semax_ CS Espec)) (SemaxArg G P c R)) (@allp nat ag_nat genv (fun gx : genv => @allp nat ag_nat tycontext (fun Delta' : tycontext => @imp nat ag_nat (@prop nat ag_nat (and (tycontext_sub G Delta') (@eq composite_env (genv_cenv gx) (@cenv_cs CS)))) (@imp nat ag_nat (@believe CS Espec Delta' gx Delta') (@allp nat ag_nat cont (fun k : cont => @allp nat ag_nat assert (fun F : assert => @imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars c F)) (rguard Espec gx Delta' (frame_ret_assert R F) k)) (guard Espec gx Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) (@cons cont' (Kseq c) k))))))))) *)
(* Goal: @HOcontractive nat ag_nat semaxArg (@semax_ CS Espec) *)
reflexivity.
(* Goal: @HOcontractive nat ag_nat semaxArg (@semax_ CS Espec) *)
apply prove_HOcontractive.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
intros.
(* Goal: @derives nat ag_nat (@allp nat ag_nat semaxArg (fun x : semaxArg => @fash nat ag_nat (@andp nat ag_nat (@imp nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (P0 x)) (@box nat ag_nat (@laterM nat ag_nat) (Q x))) (@imp nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (Q x)) (@box nat ag_nat (@laterM nat ag_nat) (P0 x)))))) (@fash nat ag_nat (@imp nat ag_nat (@semax_ CS Espec P0 x) (@semax_ CS Espec Q x))) *)
unfold semax_.
(* Goal: @derives nat ag_nat (@allp nat ag_nat semaxArg (fun x : semaxArg => @fash nat ag_nat (@andp nat ag_nat (@imp nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (P0 x)) (@box nat ag_nat (@laterM nat ag_nat) (Q x))) (@imp nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (Q x)) (@box nat ag_nat (@laterM nat ag_nat) (P0 x)))))) (@fash nat ag_nat (@imp nat ag_nat match x with | {| sa_Delta := Delta; sa_P := P; sa_c := c; sa_R := R |} => @allp nat ag_nat genv (fun gx : genv => @allp nat ag_nat tycontext (fun Delta' : tycontext => @imp nat ag_nat (@prop nat ag_nat (and (tycontext_sub Delta Delta') (@eq composite_env (genv_cenv gx) (@cenv_cs CS)))) (@imp nat ag_nat (believepred Espec P0 Delta' gx Delta') (@allp nat ag_nat cont (fun k : cont => @allp nat ag_nat assert (fun F : assert => @imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars c F)) (rguard Espec gx Delta' (frame_ret_assert R F) k)) (guard Espec gx Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) (@cons cont' (Kseq c) k)))))))) end match x with | {| sa_Delta := Delta; sa_P := P; sa_c := c; sa_R := R |} => @allp nat ag_nat genv (fun gx : genv => @allp nat ag_nat tycontext (fun Delta' : tycontext => @imp nat ag_nat (@prop nat ag_nat (and (tycontext_sub Delta Delta') (@eq composite_env (genv_cenv gx) (@cenv_cs CS)))) (@imp nat ag_nat (believepred Espec Q Delta' gx Delta') (@allp nat ag_nat cont (fun k : cont => @allp nat ag_nat assert (fun F : assert => @imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars c F)) (rguard Espec gx Delta' (frame_ret_assert R F) k)) (guard Espec gx Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) (@cons cont' (Kseq c) k)))))))) end)) *)
clear.
(* Goal: @derives nat ag_nat (@allp nat ag_nat semaxArg (fun x : semaxArg => @fash nat ag_nat (@andp nat ag_nat (@imp nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (P0 x)) (@box nat ag_nat (@laterM nat ag_nat) (Q x))) (@imp nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (Q x)) (@box nat ag_nat (@laterM nat ag_nat) (P0 x)))))) (@fash nat ag_nat (@imp nat ag_nat match x with | {| sa_Delta := Delta; sa_P := P; sa_c := c; sa_R := R |} => @allp nat ag_nat genv (fun gx : genv => @allp nat ag_nat tycontext (fun Delta' : tycontext => @imp nat ag_nat (@prop nat ag_nat (and (tycontext_sub Delta Delta') (@eq composite_env (genv_cenv gx) (@cenv_cs CS)))) (@imp nat ag_nat (believepred Espec P0 Delta' gx Delta') (@allp nat ag_nat cont (fun k : cont => @allp nat ag_nat assert (fun F : assert => @imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars c F)) (rguard Espec gx Delta' (frame_ret_assert R F) k)) (guard Espec gx Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) (@cons cont' (Kseq c) k)))))))) end match x with | {| sa_Delta := Delta; sa_P := P; sa_c := c; sa_R := R |} => @allp nat ag_nat genv (fun gx : genv => @allp nat ag_nat tycontext (fun Delta' : tycontext => @imp nat ag_nat (@prop nat ag_nat (and (tycontext_sub Delta Delta') (@eq composite_env (genv_cenv gx) (@cenv_cs CS)))) (@imp nat ag_nat (believepred Espec Q Delta' gx Delta') (@allp nat ag_nat cont (fun k : cont => @allp nat ag_nat assert (fun F : assert => @imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars c F)) (rguard Espec gx Delta' (frame_ret_assert R F) k)) (guard Espec gx Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) (@cons cont' (Kseq c) k)))))))) end)) *)
sub_unfold.
(* Goal: @derives nat ag_nat (@allp nat ag_nat semaxArg (fun x : semaxArg => @fash nat ag_nat (@andp nat ag_nat (@imp nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (P0 x)) (@box nat ag_nat (@laterM nat ag_nat) (Q x))) (@imp nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (Q x)) (@box nat ag_nat (@laterM nat ag_nat) (P0 x)))))) (@fash nat ag_nat (@imp nat ag_nat (@allp nat ag_nat genv (fun gx : genv => @allp nat ag_nat tycontext (fun Delta' : tycontext => @imp nat ag_nat (@prop nat ag_nat (and (tycontext_sub sa_Delta0 Delta') (@eq composite_env (genv_cenv gx) (@cenv_cs CS)))) (@imp nat ag_nat (believepred Espec P0 Delta' gx Delta') (@allp nat ag_nat cont (fun k : cont => @allp nat ag_nat assert (fun F : assert => @imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars sa_c0 F)) (rguard Espec gx Delta' (frame_ret_assert sa_R0 F) k)) (guard Espec gx Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (sa_P0 rho)) (@cons cont' (Kseq sa_c0) k))))))))) (@allp nat ag_nat genv (fun gx : genv => @allp nat ag_nat tycontext (fun Delta' : tycontext => @imp nat ag_nat (@prop nat ag_nat (and (tycontext_sub sa_Delta0 Delta') (@eq composite_env (genv_cenv gx) (@cenv_cs CS)))) (@imp nat ag_nat (believepred Espec Q Delta' gx Delta') (@allp nat ag_nat cont (fun k : cont => @allp nat ag_nat assert (fun F : assert => @imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars sa_c0 F)) (rguard Espec gx Delta' (frame_ret_assert sa_R0 F) k)) (guard Espec gx Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (sa_P0 rho)) (@cons cont' (Kseq sa_c0) k))))))))))) *)
do 2 (apply subp_allp; intros).
(* Goal: @derives nat ag_nat (@allp nat ag_nat semaxArg (fun x : semaxArg => @fash nat ag_nat (@andp nat ag_nat (@imp nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (P0 x)) (@box nat ag_nat (@laterM nat ag_nat) (Q x))) (@imp nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (Q x)) (@box nat ag_nat (@laterM nat ag_nat) (P0 x)))))) (@fash nat ag_nat (@imp nat ag_nat (@imp nat ag_nat (@prop nat ag_nat (and (tycontext_sub sa_Delta0 x0) (@eq composite_env (genv_cenv x) (@cenv_cs CS)))) (@imp nat ag_nat (believepred Espec P0 x0 x x0) (@allp nat ag_nat cont (fun k : cont => @allp nat ag_nat assert (fun F : assert => @imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars sa_c0 F)) (rguard Espec x x0 (frame_ret_assert sa_R0 F) k)) (guard Espec x x0 (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (sa_P0 rho)) (@cons cont' (Kseq sa_c0) k))))))) (@imp nat ag_nat (@prop nat ag_nat (and (tycontext_sub sa_Delta0 x0) (@eq composite_env (genv_cenv x) (@cenv_cs CS)))) (@imp nat ag_nat (believepred Espec Q x0 x x0) (@allp nat ag_nat cont (fun k : cont => @allp nat ag_nat assert (fun F : assert => @imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars sa_c0 F)) (rguard Espec x x0 (frame_ret_assert sa_R0 F) k)) (guard Espec x x0 (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (sa_P0 rho)) (@cons cont' (Kseq sa_c0) k))))))))) *)
apply subp_imp; [auto with contractive | ].
(* Goal: @derives nat ag_nat (@allp nat ag_nat semaxArg (fun x : semaxArg => @fash nat ag_nat (@andp nat ag_nat (@imp nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (P0 x)) (@box nat ag_nat (@laterM nat ag_nat) (Q x))) (@imp nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (Q x)) (@box nat ag_nat (@laterM nat ag_nat) (P0 x)))))) (@fash nat ag_nat (@imp nat ag_nat (@imp nat ag_nat (believepred Espec P0 x0 x x0) (@allp nat ag_nat cont (fun k : cont => @allp nat ag_nat assert (fun F : assert => @imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars sa_c0 F)) (rguard Espec x x0 (frame_ret_assert sa_R0 F) k)) (guard Espec x x0 (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (sa_P0 rho)) (@cons cont' (Kseq sa_c0) k)))))) (@imp nat ag_nat (believepred Espec Q x0 x x0) (@allp nat ag_nat cont (fun k : cont => @allp nat ag_nat assert (fun F : assert => @imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars sa_c0 F)) (rguard Espec x x0 (frame_ret_assert sa_R0 F) k)) (guard Espec x x0 (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (sa_P0 rho)) (@cons cont' (Kseq sa_c0) k)))))))) *)
apply subp_imp; [ | auto 50 with contractive].
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
apply subp_allp; intros.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
apply subp_allp; intros.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
apply subp_allp; intros.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
apply subp_allp; intros.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
apply subp_allp; intros.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
apply subp_allp; intros.
(* Goal: @derives nat ag_nat (@allp nat ag_nat semaxArg (fun x : semaxArg => @fash nat ag_nat (@andp nat ag_nat (@imp nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (P0 x)) (@box nat ag_nat (@laterM nat ag_nat) (Q x))) (@imp nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (Q x)) (@box nat ag_nat (@laterM nat ag_nat) (P0 x)))))) (@fash nat ag_nat (@imp nat ag_nat (@imp nat ag_nat (@prop nat ag_nat (claims x x0 x1 x2 x3 x4 x5 x6)) (@orp nat ag_nat (believe_external Espec x x1 x2 x3 x4 x5 x6) (believe_internal_ Q x x0 x1 x2 x3 x4 x5 x6))) (@imp nat ag_nat (@prop nat ag_nat (claims x x0 x1 x2 x3 x4 x5 x6)) (@orp nat ag_nat (believe_external Espec x x1 x2 x3 x4 x5 x6) (believe_internal_ P0 x x0 x1 x2 x3 x4 x5 x6))))) *)
apply subp_imp; intros; [ auto 50 with contractive | ].
(* Goal: @derives nat ag_nat (@allp nat ag_nat semaxArg (fun x : semaxArg => @fash nat ag_nat (@andp nat ag_nat (@imp nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (P0 x)) (@box nat ag_nat (@laterM nat ag_nat) (Q x))) (@imp nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (Q x)) (@box nat ag_nat (@laterM nat ag_nat) (P0 x)))))) (@fash nat ag_nat (@imp nat ag_nat (@orp nat ag_nat (believe_external Espec x x1 x2 x3 x4 x5 x6) (believe_internal_ Q x x0 x1 x2 x3 x4 x5 x6)) (@orp nat ag_nat (believe_external Espec x x1 x2 x3 x4 x5 x6) (believe_internal_ P0 x x0 x1 x2 x3 x4 x5 x6)))) *)
apply subp_orp; [ auto 50 with contractive | ].
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
apply subp_exp; intros.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
apply subp_exp; intros.
(* Goal: @derives nat ag_nat (@allp nat ag_nat semaxArg (fun x : semaxArg => @fash nat ag_nat (@andp nat ag_nat (@imp nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (P0 x)) (@box nat ag_nat (@laterM nat ag_nat) (Q x))) (@imp nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (Q x)) (@box nat ag_nat (@laterM nat ag_nat) (P0 x)))))) (@fash nat ag_nat (@imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (and (@eq val x1 (Vptr x7 Ptrofs.zero)) (and (@eq (option fundef) (@Genv.find_funct_ptr fundef type (genv_genv x) x7) (@Some (Ctypes.fundef function) (@Internal function x8))) (and (@Forall (prod ident type) (fun it : prod ident type => @eq bool (complete_type (genv_cenv x) (@snd ident type it)) true) (fn_vars x8)) (and (@list_norepet ident (@app ident (@map (prod ident type) ident (@fst ident type) (fn_params x8)) (@map (prod ident type) ident (@fst ident type) (fn_temps x8)))) (and (@list_norepet ident (@map (prod ident type) ident (@fst ident type) (fn_vars x8))) (and (var_sizes_ok (genv_cenv x) (fn_vars x8)) (and (@eq funsig x2 (fn_funsig x8)) (@eq calling_convention (fn_callconv x8) x3))))))))) (@allp nat ag_nat (list Type) (fun ts : list Type => @allp nat ag_nat (_functor (dependent_type_functor_rec ts x4) (@pred rmap ag_rmap)) (fun x1 : _functor (dependent_type_functor_rec ts x4) (@pred rmap ag_rmap) => @box nat ag_nat (@laterM nat ag_nat) (Q (SemaxArg (func_tycontext' x8 x0) (fun rho : environ => @andp rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (bind_args (fn_params x8) (fn_vars x8) (x5 ts x1) rho) (stackframe_of' (genv_cenv x) x8 rho)) (funassert (func_tycontext' x8 x0) rho)) (Ssequence (fn_body x8) (Sreturn (@None expr))) (frame_ret_assert (function_body_ret_assert (fn_return x8) (x6 ts x1)) (stackframe_of' (genv_cenv x) x8)))))))) (@andp nat ag_nat (@prop nat ag_nat (and (@eq val x1 (Vptr x7 Ptrofs.zero)) (and (@eq (option fundef) (@Genv.find_funct_ptr fundef type (genv_genv x) x7) (@Some (Ctypes.fundef function) (@Internal function x8))) (and (@Forall (prod ident type) (fun it : prod ident type => @eq bool (complete_type (genv_cenv x) (@snd ident type it)) true) (fn_vars x8)) (and (@list_norepet ident (@app ident (@map (prod ident type) ident (@fst ident type) (fn_params x8)) (@map (prod ident type) ident (@fst ident type) (fn_temps x8)))) (and (@list_norepet ident (@map (prod ident type) ident (@fst ident type) (fn_vars x8))) (and (var_sizes_ok (genv_cenv x) (fn_vars x8)) (and (@eq funsig x2 (fn_funsig x8)) (@eq calling_convention (fn_callconv x8) x3))))))))) (@allp nat ag_nat (list Type) (fun ts : list Type => @allp nat ag_nat (_functor (dependent_type_functor_rec ts x4) (@pred rmap ag_rmap)) (fun x1 : _functor (dependent_type_functor_rec ts x4) (@pred rmap ag_rmap) => @box nat ag_nat (@laterM nat ag_nat) (P0 (SemaxArg (func_tycontext' x8 x0) (fun rho : environ => @andp rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (bind_args (fn_params x8) (fn_vars x8) (x5 ts x1) rho) (stackframe_of' (genv_cenv x) x8 rho)) (funassert (func_tycontext' x8 x0) rho)) (Ssequence (fn_body x8) (Sreturn (@None expr))) (frame_ret_assert (function_body_ret_assert (fn_return x8) (x6 ts x1)) (stackframe_of' (genv_cenv x) x8)))))))))) *)
auto 50 with contractive.
Qed.

(* Goal: @joins ghost ghost_join (ghost_of (m_phi jm0)) (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref (@OK_ty Espec) ora) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora (State ve te ctl) jm *)
Definition weakest_pre {CS: compspecs} (Espec: OracleKind) (Delta: tycontext) c Q: assert :=
  fun rho: environ =>
  ALL gx: genv, ALL Delta': tycontext,
       !! (tycontext_sub Delta Delta' /\ genv_cenv gx = cenv_cs) -->
       unfash (believe Espec Delta' gx Delta') -->
     ALL k: cont, ALL F: assert,
        unfash (!! (closed_wrt_modvars c F) && rguard Espec gx Delta' (frame_ret_assert Q F) k) -->
        (* guard Espec gx Delta' (fun rho => F rho * P rho) (Kseq c :: k) *)
        ALL tx : Clight.temp_env, ALL vx : env,
          (!! (rho = construct_rho (filter_genv gx) vx tx)) -->
          ((!! guard_environ Delta' (current_function (Kseq c :: k)) rho && funassert Delta' rho) -->
             (F rho -* assert_safe Espec gx vx tx (Kseq c :: k) rho)).

Opaque semax'.

(* Goal: @joins ghost ghost_join (ghost_of (m_phi jm0)) (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref (@OK_ty Espec) ora) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora (State ve te ctl) jm *)
Definition semax {CS: compspecs} (Espec: OracleKind) (Delta: tycontext) P c Q :=
  forall n, semax' Espec Delta P c Q n.

Lemma any_level_pred_nat: forall P: pred nat, (forall n, P n) <-> TT |-- P.
Proof.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
  intros.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
  split; intros.
  + hnf; intros; auto.
  + hnf in H; auto.
Qed.

(* Goal: @joins ghost ghost_join (ghost_of (m_phi jm0)) (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref (@OK_ty Espec) ora) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora (State ve te ctl) jm *)
Lemma semax_weakest_pre_aux: forall {A: Type} (P: pred nat) (Q R: A -> pred rmap),
  P = fash (ALL x: A, Q x --> R x) ->
  (TT |-- P <-> forall x, Q x |-- R x).
Proof.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
  intros.
(* Goal: iff (@derives nat ag_nat (@TT nat ag_nat) P) (forall x : A, @derives rmap ag_rmap (Q x) (R x)) *)
  assert (TT |-- ALL x: A, Q x --> R x <-> (forall x : A, Q x |-- R x)).
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
  + split; intros.
    - rewrite <- (TT_and (Q x)).
(* Goal: @derives A agA (@andp A agA (@allp A agA B (fun x : B => @imp A agA P (Q x))) P) (Q x) *)
      rewrite imp_andp_adjoint.
(* Goal: @derives rmap ag_rmap (@TT rmap ag_rmap) (@imp rmap ag_rmap (Q x) (R x)) *)
      eapply derives_trans; [exact H0 |].
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
      apply (allp_left _ x); intros.
(* Goal: @eq Prop (@app_pred nat ag_nat P (@level A agA w)) (@app_pred nat ag_nat P (@level A agA w)) *)
      auto.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
    - apply allp_right; intros.
      rewrite <- imp_andp_adjoint.
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap (@TT rmap ag_rmap) (Q v)) (R v) *)
      rewrite (TT_and (Q v)).
(* Goal: @eq Prop (@app_pred nat ag_nat P (@level A agA w)) (@app_pred nat ag_nat P (@level A agA w)) *)
      auto.
  + rewrite <- H0, H.
(* Goal: @derives nat ag_nat (@allp nat ag_nat semaxArg (fun x : semaxArg => @fash nat ag_nat (@andp nat ag_nat (@imp nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (P0 x)) (@box nat ag_nat (@laterM nat ag_nat) (Q x))) (@imp nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (Q x)) (@box nat ag_nat (@laterM nat ag_nat) (P0 x)))))) (@fash nat ag_nat (@imp nat ag_nat match x with | {| sa_Delta := Delta; sa_P := P; sa_c := c; sa_R := R |} => @allp nat ag_nat genv (fun gx : genv => @allp nat ag_nat tycontext (fun Delta' : tycontext => @imp nat ag_nat (@prop nat ag_nat (and (tycontext_sub Delta Delta') (@eq composite_env (genv_cenv gx) (@cenv_cs CS)))) (@imp nat ag_nat (believepred Espec P0 Delta' gx Delta') (@allp nat ag_nat cont (fun k : cont => @allp nat ag_nat assert (fun F : assert => @imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars c F)) (rguard Espec gx Delta' (frame_ret_assert R F) k)) (guard Espec gx Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) (@cons cont' (Kseq c) k)))))))) end match x with | {| sa_Delta := Delta; sa_P := P; sa_c := c; sa_R := R |} => @allp nat ag_nat genv (fun gx : genv => @allp nat ag_nat tycontext (fun Delta' : tycontext => @imp nat ag_nat (@prop nat ag_nat (and (tycontext_sub Delta Delta') (@eq composite_env (genv_cenv gx) (@cenv_cs CS)))) (@imp nat ag_nat (believepred Espec Q Delta' gx Delta') (@allp nat ag_nat cont (fun k : cont => @allp nat ag_nat assert (fun F : assert => @imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars c F)) (rguard Espec gx Delta' (frame_ret_assert R F) k)) (guard Espec gx Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) (@cons cont' (Kseq c) k)))))))) end)) *)
    clear; forget (ALL x : A , Q x --> R x) as P; clear.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
    split; intros.
    - unfold fash in H.
      hnf in H |- *.
(* Goal: forall (a : rmap) (_ : @app_pred rmap ag_rmap (@TT rmap ag_rmap) a), @app_pred rmap ag_rmap P a *)
      intros; simpl in H.
(* Goal: @eq Prop (@app_pred nat ag_nat P (@level A agA w)) (@app_pred nat ag_nat P (@level A agA w)) *)
      eapply H; auto.
    - unfold fash.
      hnf in H |- *.
(* Goal: forall (a : nat) (_ : @app_pred nat ag_nat (@TT nat ag_nat) a), @app_pred nat ag_nat (@exist (forall _ : nat, Prop) (fun p : forall _ : nat, Prop => @hereditary nat (@age nat ag_nat) p) (fun n : nat => forall (y : rmap) (_ : ge n (@level rmap ag_rmap y)), @app_pred rmap ag_rmap P y) (subtypes.fash_obligation_1 rmap ag_rmap P)) a *)
      intros; simpl.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
      intros.
(* Goal: @app_pred nat ag_nat Q (@level A agA a) *)
      apply H.
(* Goal: @eq Prop (@app_pred nat ag_nat P (@level A agA w)) (@app_pred nat ag_nat P (@level A agA w)) *)
      auto.
Qed.

(* Copied from semax_switch. *)

(* Goal: @joins ghost ghost_join (ghost_of (m_phi jm0)) (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref (@OK_ty Espec) ora) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora (State ve te ctl) jm *)
Lemma unfash_allp:  forall {A} {agA: ageable A} {B} (f: B -> pred nat),
  @unfash _ agA (allp f) = allp (fun x:B => unfash (f x)).
Proof.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
intros.
(* Goal: @eq (@pred rmap ag_rmap) (@imp rmap ag_rmap (@prop rmap ag_rmap P) Q) Q *)
apply pred_ext.
(* Goal: @derives A agA (@unfash A agA (@allp nat ag_nat B f)) (@allp A agA B (fun x : B => @unfash A agA (f x))) *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
intros ? ? ?.
(* Goal: @eq Prop (@app_pred nat ag_nat P (@level A agA w)) (@app_pred nat ag_nat P (@level A agA w)) *)
specialize (H b). auto.
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
repeat intro. apply (H b).
Qed.

(* Goal: @joins ghost ghost_join (ghost_of (m_phi jm0)) (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref (@OK_ty Espec) ora) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora (State ve te ctl) jm *)
Lemma fash_TT: forall {A} {agA: ageable A}, @unfash A agA TT = TT.
Proof.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
intros.
(* Goal: @eq (@pred A agA) (@unfash A agA (@TT nat ag_nat)) (@TT A agA) *)
apply pred_ext; intros ? ?; apply I.
Qed.

Lemma allp_andp: 
(* Goal: @joins ghost ghost_join (ghost_of (m_phi jm0)) (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref (@OK_ty Espec) ora) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora (State ve te ctl) jm *)
  forall {A} {NA: ageable A} {B: Type} (b0: B) (P: B -> pred A) (Q: pred A),
   (allp P && Q = allp (fun x => P x && Q))%pred.
Proof.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
intros.
(* Goal: @eq (@pred rmap ag_rmap) (@imp rmap ag_rmap (@prop rmap ag_rmap P) Q) Q *)
apply pred_ext.
(* Goal: @eq Prop (@app_pred nat ag_nat P (@level A agA w)) (@app_pred nat ag_nat P (@level A agA w)) *)
intros ? [? ?] b. split; auto.
(* Goal: @derives A agA (@unfash A agA (@andp nat ag_nat P Q)) (@andp A agA (@unfash A agA P) (@unfash A agA Q)) *)
(* Goal: @derives A agA (@andp A agA (@unfash A agA P) (@unfash A agA Q)) (@unfash A agA (@andp nat ag_nat P Q)) *)
intros ? ?.
(* Goal: @app_pred A NA (@andp A NA (@allp A NA B P) Q) a *)
split.
(* Goal: @app_pred A NA (P b) a *)
(* Goal: @app_pred A NA Q a *)
intro b. apply (H b).
(* Goal: @app_pred A NA Q a *)
apply (H b0).
Qed.

Lemma unfash_prop_imp:
(* Goal: @joins ghost ghost_join (ghost_of (m_phi jm0)) (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref (@OK_ty Espec) ora) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora (State ve te ctl) jm *)
  forall {A} {agA: ageable A} (P: Prop) (Q: pred nat),
  (@unfash _ agA (prop P --> Q) = prop P --> @unfash _ agA Q)%pred.
Proof.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
intros.
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
apply pred_ext; repeat intro.
(* Goal: @eq Prop (@app_pred nat ag_nat P (@level A agA w)) (@app_pred nat ag_nat P (@level A agA w)) *)
apply H; auto. apply necR_level'; auto.
(* Goal: @app_pred nat ag_nat Q a' *)
hnf in H.
(* Goal: @app_pred nat ag_nat Q a' *)
specialize (H a (necR_refl _) H1).
(* Goal: @app_pred nat ag_nat Q a' *)
eapply pred_nec_hereditary; try apply H0.
(* Goal: @app_pred nat ag_nat Q (@level A agA a) *)
apply H.
Qed.

Import age_to.

Lemma unfash_imp:
(* Goal: @joins ghost ghost_join (ghost_of (m_phi jm0)) (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref (@OK_ty Espec) ora) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora (State ve te ctl) jm *)
  forall {A} {NA: ageable A} (P Q: pred nat),
  (@unfash A _ (P --> Q) = (@unfash A _ P) --> @unfash A _ Q)%pred.
Proof.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
intros.
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
apply pred_ext; repeat intro.
(* Goal: @eq Prop (@app_pred nat ag_nat P (@level A agA w)) (@app_pred nat ag_nat P (@level A agA w)) *)
apply H; auto. apply necR_level'; auto.
(* Goal: @app_pred nat ag_nat Q a' *)
specialize (H (age_to a' a)).
(* Goal: @app_pred nat ag_nat Q a' *)
spec H.
(* Goal: @necR A NA a (@age_to a' A NA a) *)
(* Goal: @app_pred nat ag_nat Q a' *)
apply age_to_necR.
(* Goal: @app_pred nat ag_nat Q a' *)
spec H.
(* Goal: @app_pred A NA (@unfash A NA P) (@age_to a' A NA a) *)
(* Goal: @app_pred nat ag_nat Q a' *)
do 3 red. 
(* Goal: @eq Prop (@app_pred nat ag_nat P (@level A agA w)) (@app_pred nat ag_nat P (@level A agA w)) *)
rewrite level_age_to; auto.
(* Goal: le a' (@level A NA a) *)
apply necR_level in H0. apply H0.
(* Goal: @app_pred nat ag_nat Q a' *)
do 3 red in H.
(* Goal: @eq Prop (@app_pred nat ag_nat P (@level A agA w)) (@app_pred nat ag_nat P (@level A agA w)) *)
rewrite level_age_to in H; auto.
(* Goal: le a' (@level A NA a) *)
apply necR_level in H0.
(* Goal: le a' (@level A NA a) *)
apply H0.
Qed.

(* Goal: @joins ghost ghost_join (ghost_of (m_phi jm0)) (@cons (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)) (@Some (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds) (@pair (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds (@ghost_PCM.ext_ref (@OK_ty Espec) ora) NoneP)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) *)
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) ge (@level rmap ag_rmap (m_phi jm)) ora (State ve te ctl) jm *)
Lemma unfash_andp:  forall {A} {agA: ageable A} (P Q: pred nat),
  (@unfash A agA (andp P Q) = andp (@unfash A agA P) (@unfash A agA Q)).
Proof.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
intros.
(* Goal: @eq (@pred rmap ag_rmap) (@imp rmap ag_rmap (@prop rmap ag_rmap P) Q) Q *)
apply pred_ext.
(* Goal: @derives A agA (@unfash A agA (@andp nat ag_nat P Q)) (@andp A agA (@unfash A agA P) (@unfash A agA Q)) *)
(* Goal: @derives A agA (@andp A agA (@unfash A agA P) (@unfash A agA Q)) (@unfash A agA (@andp nat ag_nat P Q)) *)
intros ? ?.
(* Goal: @app_pred A agA (@andp A agA (@unfash A agA P) (@unfash A agA Q)) a *)
(* Goal: @derives A agA (@andp A agA (@unfash A agA P) (@unfash A agA Q)) (@unfash A agA (@andp nat ag_nat P Q)) *)
destruct H.
(* Goal: @eq Prop (@app_pred nat ag_nat P (@level A agA w)) (@app_pred nat ag_nat P (@level A agA w)) *)
split; auto.
(* Goal: @derives A agA (@andp A agA P (@imp A agA P Q)) Q *)
intros ? [? ?].
(* Goal: @eq Prop (@app_pred nat ag_nat P (@level A agA w)) (@app_pred nat ag_nat P (@level A agA w)) *)
split; auto.
Qed.

Lemma andp_imp_e':
  forall (A : Type) (agA : ageable A) (P Q : pred A),
   P && (P --> Q) |-- P && Q.
Proof.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
intros.
(* Goal: @derives A agA (@andp A agA P (@imp A agA P Q)) (@andp A agA P Q) *)
apply andp_right.
(* Goal: @eq Prop (@app_pred nat ag_nat P (@level A agA w)) (@app_pred nat ag_nat P (@level A agA w)) *)
apply andp_left1; auto.
(* Goal: @derives A agA (@andp A agA P (@imp A agA P Q)) Q *)
intros ? [? ?].
(* Goal: @eq Prop (@app_pred nat ag_nat P (@level A agA w)) (@app_pred nat ag_nat P (@level A agA w)) *)
eapply H0; auto.
Qed.

(* End copied from semax_switch. *)

Lemma unfash_fash:
  forall (A : Type) (agA : ageable A) (P : pred A),
   unfash (fash P) |-- P.
Proof.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
  intros.
(* Goal: @eq (@pred nat ag_nat) (@fash rmap ag_rmap (@unfash rmap ag_rmap P : @pred rmap ag_rmap)) P *)
  unfold fash, unfash.
(* Goal: @derives A agA (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A agA) p) (fun x : A => @app_pred nat ag_nat (@exist (forall _ : nat, Prop) (fun p : forall _ : nat, Prop => @hereditary nat (@age nat ag_nat) p) (fun n : nat => forall (y : A) (_ : ge n (@level A agA y)), @app_pred A agA P y) (subtypes.fash_obligation_1 A agA P)) (@level A agA x)) (subtypes.unfash_obligation_1 A agA (@exist (forall _ : nat, Prop) (fun p : forall _ : nat, Prop => @hereditary nat (@age nat ag_nat) p) (fun n : nat => forall (y : A) (_ : ge n (@level A agA y)), @app_pred A agA P y) (subtypes.fash_obligation_1 A agA P)))) P *)
  simpl.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
  hnf; simpl; intros.
(* Goal: @app_pred A agA P a *)
  apply (H a).
(* Goal: ge a (@level rmap ag_rmap r) *)
  omega.
Qed.

Lemma imp_imp:
  forall (A : Type) (agA : ageable A) (P Q R: pred A),
    P --> (Q --> R) = P && Q --> R.
Proof.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (@imp rmap ag_rmap (@prop rmap ag_rmap P) Q) Q *)
  apply pred_ext.
  + apply imp_andp_adjoint.
    rewrite <- andp_assoc.
(* Goal: @derives rmap ag_rmap Q (@imp rmap ag_rmap (@prop rmap ag_rmap P) Q) *)
    apply imp_andp_adjoint.
(* Goal: @derives A agA (@andp A agA (@imp A agA P (@imp A agA Q R)) P) (@imp A agA Q R) *)
    rewrite andp_comm.
(* Goal: @derives A agA (@andp A agA P (@imp A agA P (@imp A agA Q R))) (@imp A agA Q R) *)
    eapply derives_trans; [apply andp_imp_e' | apply andp_left2].
(* Goal: @eq Prop (@app_pred nat ag_nat P (@level A agA w)) (@app_pred nat ag_nat P (@level A agA w)) *)
    auto.
  + rewrite <- !imp_andp_adjoint.
(* Goal: @derives A agA (@andp A agA (@andp A agA (@imp A agA (@andp A agA P Q) R) P) Q) R *)
    rewrite andp_assoc.
(* Goal: @derives A agA (@andp A agA (@allp A agA B (fun x : B => @imp A agA P (Q x))) P) (Q x) *)
    rewrite imp_andp_adjoint.
(* Goal: @eq Prop (@app_pred nat ag_nat P (@level A agA w)) (@app_pred nat ag_nat P (@level A agA w)) *)
    auto.
Qed.

Lemma imp_allp:
  forall B (A : Type) (agA : ageable A) (P: pred A) (Q: B -> pred A),
    P --> allp Q  = ALL x: B, P --> Q x.
Proof.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (@imp rmap ag_rmap (@prop rmap ag_rmap P) Q) Q *)
  apply pred_ext.
  + apply allp_right; intros x.
    rewrite <- imp_andp_adjoint, andp_comm.
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap P) (@imp rmap ag_rmap (@prop rmap ag_rmap P) Q)) Q *)
    eapply derives_trans; [apply andp_imp_e' |].
(* Goal: @derives A agA (@andp A agA P (@allp A agA B Q)) (Q x) *)
    apply andp_left2.
(* Goal: @derives A agA (@allp A agA B (fun x : B => @imp A agA P (Q x))) (@imp A agA P (Q x)) *)
    apply (allp_left _ x).
(* Goal: @eq Prop (@app_pred nat ag_nat P (@level A agA w)) (@app_pred nat ag_nat P (@level A agA w)) *)
    auto.
  + rewrite <- imp_andp_adjoint.
(* Goal: @derives A agA (@andp A agA (@allp A agA B (fun x : B => @imp A agA P (Q x))) P) (@allp A agA B Q) *)
    apply allp_right; intros x.
(* Goal: @derives A agA (@andp A agA (@allp A agA B (fun x : B => @imp A agA P (Q x))) P) (Q x) *)
    rewrite imp_andp_adjoint.
(* Goal: @derives A agA (@allp A agA B (fun x : B => @imp A agA P (Q x))) (@imp A agA P (Q x)) *)
    apply (allp_left _ x).
(* Goal: @eq Prop (@app_pred nat ag_nat P (@level A agA w)) (@app_pred nat ag_nat P (@level A agA w)) *)
    auto.
Qed.

Lemma fash_prop: forall P: Prop,
  fash (!! P: pred rmap) = !! P.
Proof.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
  intros.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
  apply pred_ext; unfold fash; hnf; simpl; intros.
  + destruct (ex_level a) as [r ?].
(* Goal: P *)
    apply (H r).
(* Goal: ge a (@level rmap ag_rmap r) *)
    omega.
  + auto.
Qed.

Lemma fash_unfash:
  forall (P : pred nat),
   fash (unfash P: pred rmap) = P.
Proof.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
  intros.
(* Goal: @eq (@pred nat ag_nat) (@fash rmap ag_rmap (@unfash rmap ag_rmap P : @pred rmap ag_rmap)) P *)
  unfold fash, unfash.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
  apply pred_ext; hnf; simpl; intros.
  + destruct (ex_level a) as [r ?].
(* Goal: @app_pred nat ag_nat P a *)
    specialize (H r).
(* Goal: @app_pred nat ag_nat P a *)
    rewrite H0 in H.
(* Goal: ge a (@level rmap ag_rmap r) *)
    apply H; omega.
  + eapply pred_nec_hereditary; [| eassumption].
(* Goal: ge a (@level rmap ag_rmap r) *)
    rewrite nec_nat; omega.
Qed.

Lemma prop_true_imp:
  forall (P: Prop) (Q: pred rmap),
    P -> !! P --> Q = Q.
Proof.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (@imp rmap ag_rmap (@prop rmap ag_rmap P) Q) Q *)
  apply pred_ext.
  + rewrite <- (True_andp_eq P (!! P --> Q)) by auto.
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap P) (@imp rmap ag_rmap (@prop rmap ag_rmap P) Q)) Q *)
    eapply derives_trans; [apply andp_imp_e' |].
(* Goal: @eq Prop (@app_pred nat ag_nat P (@level A agA w)) (@app_pred nat ag_nat P (@level A agA w)) *)
    apply andp_left2; auto.
  + apply imp_andp_adjoint.
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap Q (@prop rmap ag_rmap P)) Q *)
    apply andp_left1.
(* Goal: @eq Prop (@app_pred nat ag_nat P (@level A agA w)) (@app_pred nat ag_nat P (@level A agA w)) *)
    auto.
Qed.

Lemma corable_unfash:
  forall (A : Type) (JA : Join A) (PA : Perm_alg A) (SA : Sep_alg A) (agA : ageable A) 
    (AgeA : Age_alg A) (P : pred nat), corable (! P).
Proof.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
  intros.
(* Goal: @derives A agA (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A agA) p) (fun x : A => @app_pred nat ag_nat (@exist (forall _ : nat, Prop) (fun p : forall _ : nat, Prop => @hereditary nat (@age nat ag_nat) p) (fun n : nat => forall (y : A) (_ : ge n (@level A agA y)), @app_pred A agA P y) (subtypes.fash_obligation_1 A agA P)) (@level A agA x)) (subtypes.unfash_obligation_1 A agA (@exist (forall _ : nat, Prop) (fun p : forall _ : nat, Prop => @hereditary nat (@age nat ag_nat) p) (fun n : nat => forall (y : A) (_ : ge n (@level A agA y)), @app_pred A agA P y) (subtypes.fash_obligation_1 A agA P)))) P *)
  unfold unfash; simpl.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred nat ag_nat), @corable A JA PA SA agA AgeA (@unfash A agA P) *)
  hnf; simpl; intros.
(* Goal: @eq Prop (@app_pred nat ag_nat P (@level A agA w)) (@app_pred nat ag_nat P (@level A agA (@core A JA SA w))) *)
  rewrite level_core.
(* Goal: @eq Prop (@app_pred nat ag_nat P (@level A agA w)) (@app_pred nat ag_nat P (@level A agA w)) *)
  auto.
Qed.
