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.sepcomp.extspec.
Require Import VST.sepcomp.step_lemmas.
Require Import VST.veric.tycontext.
Require Import VST.veric.expr2.
Require Import VST.veric.expr_lemmas.
Require Import VST.veric.juicy_extspec.
Require Import VST.veric.semax.
Require Import VST.veric.semax_lemmas.
Require Import VST.veric.Clight_lemmas.
Require Import VST.veric.own.

Local Open Scope pred.

(* This file contains two parts:
   1. Proof of semax_conseq.
   2. Deriving simpler and older version of consequence rules from semax_conseq. *)

(* Part 1: Proof of semax_conseq *)

Lemma _guard_mono: forall Espec ge Delta (P Q: assert) f k,
  (forall rho, P rho |-- Q rho) ->
  _guard Espec ge Delta Q f k |-- _guard Espec ge Delta P f k.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  intros.
(* Goal: @eq (@pred nat ag_nat) (_guard Espec ge Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) f k) (_guard Espec ge Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta rho)) (P rho))) f k) *)
  unfold _guard.
(* Goal: @derives nat ag_nat (@allp nat ag_nat temp_env (fun tx : temp_env => @allp nat ag_nat env (fun vx : env => @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta f (construct_rho (filter_genv ge) vx tx))) (Q (construct_rho (filter_genv ge) vx tx))) (funassert Delta (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx)))))) (@allp nat ag_nat temp_env (fun tx : temp_env => @allp nat ag_nat env (fun vx : env => @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta f (construct_rho (filter_genv ge) vx tx))) (P (construct_rho (filter_genv ge) vx tx))) (funassert Delta (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx)))))) *)
  apply allp_derives; intros tx.
(* Goal: @derives nat ag_nat (@allp nat ag_nat env (fun vx : env => @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta f (construct_rho (filter_genv ge) vx tx))) (Q (construct_rho (filter_genv ge) vx tx))) (funassert Delta (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx))))) (@allp nat ag_nat env (fun vx : env => @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta f (construct_rho (filter_genv ge) vx tx))) (P (construct_rho (filter_genv ge) vx tx))) (funassert Delta (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx))))) *)
  apply allp_derives; intros vx.
(* Goal: @derives nat ag_nat (@fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta f (construct_rho (filter_genv ge) vx tx))) (Q (construct_rho (filter_genv ge) vx tx))) (funassert Delta (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx)))) (@fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta f (construct_rho (filter_genv ge) vx tx))) (P (construct_rho (filter_genv ge) vx tx))) (funassert Delta (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx)))) *)
  apply fash_derives.
(* Goal: @derives nat ag_nat (@imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars c F)) (rguard Espec psi Delta' (frame_ret_assert R F) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P' rho)) (@cons cont' (Kseq c) k))) (@imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars c F)) (rguard Espec psi Delta' (frame_ret_assert R F) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) (@cons cont' (Kseq c) k))) *)
  apply imp_derives; auto.
Qed.

Lemma guard_mono: forall Espec ge Delta (P Q: assert) k,
  (forall rho, P rho |-- Q rho) ->
  guard Espec ge Delta Q k |-- guard Espec ge Delta P k.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  intros.
(* Goal: @derives nat ag_nat (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P' rho)) (@cons cont' (Kseq c) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) (@cons cont' (Kseq c) k)) *)
  unfold guard.
(* Goal: @derives nat ag_nat (_guard Espec ge Delta (proj_ret_assert Q ek vl) (current_function k) (exit_cont ek vl k)) (_guard Espec ge Delta (proj_ret_assert P ek vl) (current_function k) (exit_cont ek vl k)) *)
  apply _guard_mono; auto.
Qed.

Lemma rguard_mono: forall Espec ge Delta (P Q: ret_assert) k,
  (forall rk vl rho, proj_ret_assert P rk vl rho |-- proj_ret_assert Q rk vl rho) ->
  rguard Espec ge Delta Q k |-- rguard Espec ge Delta P k.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  intros.
(* Goal: @eq (@pred nat ag_nat) (rguard Espec ge Delta' (frame_ret_assert P F) k) (rguard Espec ge Delta' (frame_ret_assert (conj_ret_assert P (fun rho : environ => @prop rmap ag_rmap (typecheck_environ Delta rho))) F) k) *)
  unfold rguard.
(* Goal: @derives nat ag_nat (@allp nat ag_nat exitkind (fun ek : exitkind => @allp nat ag_nat (option val) (fun vl : option val => _guard Espec ge Delta (proj_ret_assert Q ek vl) (current_function k) (exit_cont ek vl k)))) (@allp nat ag_nat exitkind (fun ek : exitkind => @allp nat ag_nat (option val) (fun vl : option val => _guard Espec ge Delta (proj_ret_assert P ek vl) (current_function k) (exit_cont ek vl k)))) *)
  apply allp_derives; intros ek.
(* Goal: @derives nat ag_nat (@allp nat ag_nat (option val) (fun vl : option val => _guard Espec ge Delta (proj_ret_assert Q ek vl) (current_function k) (exit_cont ek vl k))) (@allp nat ag_nat (option val) (fun vl : option val => _guard Espec ge Delta (proj_ret_assert P ek vl) (current_function k) (exit_cont ek vl k))) *)
  apply allp_derives; intros vl.
(* Goal: @derives nat ag_nat (_guard Espec ge Delta (proj_ret_assert Q ek vl) (current_function k) (exit_cont ek vl k)) (_guard Espec ge Delta (proj_ret_assert P ek vl) (current_function k) (exit_cont ek vl k)) *)
  apply _guard_mono; auto.
Qed.

Definition bupd_ret_assert (Q: ret_assert): ret_assert :=
(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
          {| RA_normal := fun rho => bupd (RA_normal Q rho);
             RA_break := fun rho => bupd (RA_break Q rho);
             RA_continue := fun rho => bupd (RA_continue Q rho);
             RA_return := fun v rho => bupd (RA_return Q v rho) |}.

Lemma proj_bupd_ret_assert: forall Q ek vl,
  proj_ret_assert (bupd_ret_assert Q) ek vl = fun rho => bupd (proj_ret_assert Q ek vl rho).
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  intros.
  destruct ek;
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
  auto.
Qed.

(* The following four lemmas is not now used. but after deep embedded hoare logic (SL_as_Logic) is
ported, the frame does not need to be quantified in the semantic definition of semax. Then,
these two lemmas can replace the other two afterwards. *)

Lemma assert_safe_bupd':
  forall {Espec: OracleKind} gx vx tx rho (P: environ -> pred rmap) Delta f k,
    let PP1 := !! guard_environ Delta f rho in
    let PP2 := funassert Delta rho in
    PP1 && (P rho) && PP2 >=>
    assert_safe Espec gx vx tx k rho =
    PP1 && (bupd (P rho)) && PP2 >=>
    assert_safe Espec gx vx tx k rho.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  intros.
(* Goal: @eq (@pred nat ag_nat) (@fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap PP1 (P rho)) PP2) (assert_safe Espec gx vx tx k rho))) (@fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap PP1 (@orp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (@FF rmap ag_rmap)) (P rho))) PP2) (assert_safe Espec gx vx tx k rho))) *)
  apply pred_ext.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  + hnf; intros.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
    hnf; intros.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
    hnf; intros.
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap PP1 (@orp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (@FF rmap ag_rmap)) (P rho))) PP2) a' *)
    destruct H2 as [[? ?] ?].
(* Goal: @app_pred rmap ag_rmap (assert_safe Espec gx vx tx k rho) a' *)
    apply bupd_trans.
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) gx (@level rmap ag_rmap a') ora (State vx tx k) jm *)
    hnf.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
    intros.
(* Goal: @ex ghost (fun b : ghost => and (@joins ghost ghost_join b (ghost_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) c)) (@ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a')) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a')) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap (bupd (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w : rmap => forall (ora : @OK_ty Espec) (jm : juicy_mem) (_ : @app_pred rmap ag_rmap (@ext_compat (@OK_ty Espec) ora) w) (_ : @eq environ rho (construct_rho (filter_genv gx) vx tx)) (_ : @eq rmap (m_phi jm) w), @jsafeN (@OK_ty Espec) (@OK_spec Espec) gx (@level rmap ag_rmap w) ora (State vx tx k) jm) (semax.assert_safe_obligation_1 Espec gx vx tx k rho))) m')))))) *)
    specialize (H3 _ H5).
(* Goal: @ex ghost (fun b : ghost => and (@joins ghost ghost_join b (ghost_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) c)) (@ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a')) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a')) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap (bupd (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w : rmap => forall (ora : @OK_ty Espec) (jm : juicy_mem) (_ : @app_pred rmap ag_rmap (@ext_compat (@OK_ty Espec) ora) w) (_ : @eq environ rho (construct_rho (filter_genv gx) vx tx)) (_ : @eq rmap (m_phi jm) w), @jsafeN (@OK_ty Espec) (@OK_spec Espec) gx (@level rmap ag_rmap w) ora (State vx tx k) jm) (semax.assert_safe_obligation_1 Espec gx vx tx k rho))) m')))))) *)
    destruct H3 as [b [? [m' [? [? [? ?]]]]]].
(* Goal: @ex ghost (fun b : ghost => and (@joins ghost ghost_join b (ghost_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) c)) (@ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a')) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a')) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap (bupd (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w : rmap => forall (ora : @OK_ty Espec) (jm : juicy_mem) (_ : @app_pred rmap ag_rmap (@ext_compat (@OK_ty Espec) ora) w) (_ : @eq environ rho (construct_rho (filter_genv gx) vx tx)) (_ : @eq rmap (m_phi jm) w), @jsafeN (@OK_ty Espec) (@OK_spec Espec) gx (@level rmap ag_rmap w) ora (State vx tx k) jm) (semax.assert_safe_obligation_1 Espec gx vx tx k rho))) m')))))) *)
    exists b; split; auto.
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a')) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a')) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap (bupd (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w : rmap => forall (ora : @OK_ty Espec) (jm : juicy_mem) (_ : @app_pred rmap ag_rmap (@ext_compat (@OK_ty Espec) ora) w) (_ : @eq environ rho (construct_rho (filter_genv gx) vx tx)) (_ : @eq rmap (m_phi jm) w), @jsafeN (@OK_ty Espec) (@OK_spec Espec) gx (@level rmap ag_rmap w) ora (State vx tx k) jm) (semax.assert_safe_obligation_1 Espec gx vx tx k rho))) m')))) *)
    exists m'; split; [| split; [| split]]; auto.
(* Goal: @app_pred rmap ag_rmap (bupd (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w : rmap => forall (ora : @OK_ty Espec) (jm : juicy_mem) (_ : @app_pred rmap ag_rmap (@ext_compat (@OK_ty Espec) ora) w) (_ : @eq environ rho (construct_rho (filter_genv gx) vx tx)) (_ : @eq rmap (m_phi jm) w), @jsafeN (@OK_ty Espec) (@OK_spec Espec) gx (@level rmap ag_rmap w) ora (State vx tx k) jm) (semax.assert_safe_obligation_1 Espec gx vx tx k rho))) m' *)
    change (assert_safe Espec gx vx tx k rho m').
(* Goal: @app_pred rmap ag_rmap (assert_safe Espec gx vx tx k rho) m' *)
    specialize (H m' ltac: (apply necR_level in H1; omega)).
(* Goal: @app_pred rmap ag_rmap (assert_safe Espec gx vx tx k rho) m' *)
    specialize (H m' ltac: (apply necR_refl)).
(* Goal: @app_pred rmap ag_rmap (assert_safe Espec gx vx tx k rho) a' *)
    apply H.
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function (@cons cont' (Kseq c) k)) (construct_rho (filter_genv psi) ve te))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv psi) ve te)) (P' (construct_rho (filter_genv psi) ve te)))) (funassert Delta' (construct_rho (filter_genv psi) ve te))) m' *)
(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
    split; [split |]; auto.
(* Goal: @app_pred rmap ag_rmap PP2 m' *)
    subst PP2.
(* Goal: @app_pred rmap ag_rmap (funassert Delta rho) m' *)
    pose proof funassert_resource Delta rho _ _ (eq_sym H6) (eq_sym H7).
(* Goal: @app_pred rmap ag_rmap (funassert Delta rho) m' *)
    apply H10, H4.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  + hnf; intros.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
    hnf; intros.
(* Goal: @app_pred rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap PP1 (P rho)) PP2) (assert_safe Espec gx vx tx k rho)) y *)
    specialize (H y H0).
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
    hnf; intros.
(* Goal: @app_pred rmap ag_rmap (assert_safe Espec gx vx tx k rho) a' *)
    specialize (H a' H1).
(* Goal: @app_pred rmap ag_rmap (assert_safe Espec gx vx tx k rho) a' *)
    apply H.
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap PP1 (@orp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (@FF rmap ag_rmap)) (P rho))) PP2) a' *)
    destruct H2 as [[? ?] ?].
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function (@cons cont' (Kseq c) k)) (construct_rho (filter_genv psi) ve te))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv psi) ve te)) (P' (construct_rho (filter_genv psi) ve te)))) (funassert Delta' (construct_rho (filter_genv psi) ve te))) m' *)
(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
    split; [split |]; auto.
(* Goal: @app_pred rmap ag_rmap (bupd (P rho)) a' *)
    apply bupd_intro; auto.
Qed.

Lemma _guard_bupd':
  forall {Espec: OracleKind} ge Delta (P: environ -> pred rmap) f k,
    _guard Espec ge Delta P f k = _guard Espec ge Delta (fun rho => bupd (P rho)) f k.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  intros.
(* Goal: @eq (@pred nat ag_nat) (_guard Espec ge Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) f k) (_guard Espec ge Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta rho)) (P rho))) f k) *)
  unfold _guard.
(* Goal: @eq (@pred nat ag_nat) (@allp nat ag_nat temp_env (fun tx : temp_env => @allp nat ag_nat env (fun vx : env => @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx)))))) (@allp nat ag_nat temp_env (fun tx : temp_env => @allp nat ag_nat env (fun vx : env => @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta (construct_rho (filter_genv ge) vx tx))) (P (construct_rho (filter_genv ge) vx tx))))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx)))))) *)
  f_equal; extensionality tx.
(* Goal: @eq (@pred nat ag_nat) (@allp nat ag_nat env (fun vx : env => @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx))))) (@allp nat ag_nat env (fun vx : env => @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta (construct_rho (filter_genv ge) vx tx))) (P (construct_rho (filter_genv ge) vx tx))))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx))))) *)
  f_equal; extensionality vx.
(* Goal: @eq (@pred nat ag_nat) (@fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta f (construct_rho (filter_genv ge) vx tx))) (P (construct_rho (filter_genv ge) vx tx))) (funassert Delta (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx)))) (@fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta f (construct_rho (filter_genv ge) vx tx))) (bupd (P (construct_rho (filter_genv ge) vx tx)))) (funassert Delta (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx)))) *)
  apply assert_safe_bupd'.
Qed.
  
Lemma guard_bupd':
  forall {Espec: OracleKind} ge Delta (P: environ -> pred rmap) k,
    guard Espec ge Delta P k = guard Espec ge Delta (fun rho => bupd (P rho)) k.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  intros.
(* Goal: @eq (@pred nat ag_nat) (_guard Espec ge Delta (proj_ret_assert P ek vl) (current_function k) (exit_cont ek vl k)) (_guard Espec ge Delta (fun rho : environ => bupd (proj_ret_assert P ek vl rho)) (current_function k) (exit_cont ek vl k)) *)
  apply _guard_bupd'.
Qed.

Lemma rguard_bupd':
(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
  forall {Espec: OracleKind} ge Delta (P: ret_assert) k,
    rguard Espec ge Delta P k = rguard Espec ge Delta (bupd_ret_assert P) k.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  intros.
(* Goal: @eq (@pred nat ag_nat) (rguard Espec ge Delta' (frame_ret_assert P F) k) (rguard Espec ge Delta' (frame_ret_assert (conj_ret_assert P (fun rho : environ => @prop rmap ag_rmap (typecheck_environ Delta rho))) F) k) *)
  unfold rguard.
(* Goal: @eq (@pred nat ag_nat) (@allp nat ag_nat exitkind (fun ek : exitkind => @allp nat ag_nat (option val) (fun vl : option val => _guard Espec ge Delta' (proj_ret_assert (frame_ret_assert P F) ek vl) (current_function k) (exit_cont ek vl k)))) (@allp nat ag_nat exitkind (fun ek : exitkind => @allp nat ag_nat (option val) (fun vl : option val => _guard Espec ge Delta' (proj_ret_assert (frame_ret_assert (conj_ret_assert P (fun rho : environ => @prop rmap ag_rmap (typecheck_environ Delta rho))) F) ek vl) (current_function k) (exit_cont ek vl k)))) *)
  f_equal; extensionality ek.
(* Goal: @eq (@pred nat ag_nat) (@allp nat ag_nat (option val) (fun vl : option val => _guard Espec ge Delta' (proj_ret_assert (frame_ret_assert P F) ek vl) (current_function k) (exit_cont ek vl k))) (@allp nat ag_nat (option val) (fun vl : option val => _guard Espec ge Delta' (proj_ret_assert (frame_ret_assert (conj_ret_assert P (fun rho : environ => @prop rmap ag_rmap (typecheck_environ Delta rho))) F) ek vl) (current_function k) (exit_cont ek vl k))) *)
  f_equal; extensionality vl.
(* Goal: @eq (@pred nat ag_nat) (_guard Espec ge Delta (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (proj_ret_assert P ek vl rho)) (current_function k) (exit_cont ek vl k)) (_guard Espec ge Delta (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (proj_ret_assert (bupd_ret_assert P) ek vl rho)) (current_function k) (exit_cont ek vl k)) *)
  rewrite proj_bupd_ret_assert.
(* Goal: @eq (@pred nat ag_nat) (_guard Espec ge Delta (proj_ret_assert P ek vl) (current_function k) (exit_cont ek vl k)) (_guard Espec ge Delta (fun rho : environ => bupd (proj_ret_assert P ek vl rho)) (current_function k) (exit_cont ek vl k)) *)
  apply _guard_bupd'.
Qed.

Lemma assert_safe_bupd:
  forall {Espec: OracleKind} gx vx tx rho (F P: environ -> pred rmap) Delta f k,
    let PP1 := !! guard_environ Delta f rho in
    let PP2 := funassert Delta rho in
    PP1 && (F rho * P rho) && PP2 >=>
    assert_safe Espec gx vx tx k rho =
    PP1 && (F rho * bupd (P rho)) && PP2 >=>
    assert_safe Espec gx vx tx k rho.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  intros.
(* Goal: @eq (@pred nat ag_nat) (@fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap PP1 (P rho)) PP2) (assert_safe Espec gx vx tx k rho))) (@fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap PP1 (@orp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (@FF rmap ag_rmap)) (P rho))) PP2) (assert_safe Espec gx vx tx k rho))) *)
  apply pred_ext.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  + hnf; intros.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
    hnf; intros.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
    hnf; intros.
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap PP1 (@orp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (@FF rmap ag_rmap)) (P rho))) PP2) a' *)
    destruct H2 as [[? ?] ?].
(* Goal: @app_pred rmap ag_rmap (assert_safe Espec gx vx tx k rho) a' *)
    apply bupd_trans.
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) gx (@level rmap ag_rmap a') ora (State vx tx k) jm *)
    hnf.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
    intros.
(* Goal: @ex ghost (fun b : ghost => and (@joins ghost ghost_join b (ghost_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) c)) (@ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a')) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a')) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap (bupd (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w : rmap => forall (ora : @OK_ty Espec) (jm : juicy_mem) (_ : @app_pred rmap ag_rmap (@ext_compat (@OK_ty Espec) ora) w) (_ : @eq environ rho (construct_rho (filter_genv gx) vx tx)) (_ : @eq rmap (m_phi jm) w), @jsafeN (@OK_ty Espec) (@OK_spec Espec) gx (@level rmap ag_rmap w) ora (State vx tx k) jm) (semax.assert_safe_obligation_1 Espec gx vx tx k rho))) m')))))) *)
    apply bupd_frame_l in H3.
(* Goal: @ex ghost (fun b : ghost => and (@joins ghost ghost_join b (ghost_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) c)) (@ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a')) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a')) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap (bupd (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w : rmap => forall (ora : @OK_ty Espec) (jm : juicy_mem) (_ : @app_pred rmap ag_rmap (@ext_compat (@OK_ty Espec) ora) w) (_ : @eq environ rho (construct_rho (filter_genv gx) vx tx)) (_ : @eq rmap (m_phi jm) w), @jsafeN (@OK_ty Espec) (@OK_spec Espec) gx (@level rmap ag_rmap w) ora (State vx tx k) jm) (semax.assert_safe_obligation_1 Espec gx vx tx k rho))) m')))))) *)
    specialize (H3 _ H5).
(* Goal: @ex ghost (fun b : ghost => and (@joins ghost ghost_join b (ghost_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) c)) (@ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a')) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a')) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap (bupd (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w : rmap => forall (ora : @OK_ty Espec) (jm : juicy_mem) (_ : @app_pred rmap ag_rmap (@ext_compat (@OK_ty Espec) ora) w) (_ : @eq environ rho (construct_rho (filter_genv gx) vx tx)) (_ : @eq rmap (m_phi jm) w), @jsafeN (@OK_ty Espec) (@OK_spec Espec) gx (@level rmap ag_rmap w) ora (State vx tx k) jm) (semax.assert_safe_obligation_1 Espec gx vx tx k rho))) m')))))) *)
    destruct H3 as [b [? [m' [? [? [? ?]]]]]].
(* Goal: @ex ghost (fun b : ghost => and (@joins ghost ghost_join b (ghost_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) c)) (@ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a')) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a')) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap (bupd (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w : rmap => forall (ora : @OK_ty Espec) (jm : juicy_mem) (_ : @app_pred rmap ag_rmap (@ext_compat (@OK_ty Espec) ora) w) (_ : @eq environ rho (construct_rho (filter_genv gx) vx tx)) (_ : @eq rmap (m_phi jm) w), @jsafeN (@OK_ty Espec) (@OK_spec Espec) gx (@level rmap ag_rmap w) ora (State vx tx k) jm) (semax.assert_safe_obligation_1 Espec gx vx tx k rho))) m')))))) *)
    exists b; split; auto.
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a')) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a')) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap (bupd (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w : rmap => forall (ora : @OK_ty Espec) (jm : juicy_mem) (_ : @app_pred rmap ag_rmap (@ext_compat (@OK_ty Espec) ora) w) (_ : @eq environ rho (construct_rho (filter_genv gx) vx tx)) (_ : @eq rmap (m_phi jm) w), @jsafeN (@OK_ty Espec) (@OK_spec Espec) gx (@level rmap ag_rmap w) ora (State vx tx k) jm) (semax.assert_safe_obligation_1 Espec gx vx tx k rho))) m')))) *)
    exists m'; split; [| split; [| split]]; auto.
(* Goal: @app_pred rmap ag_rmap (bupd (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w : rmap => forall (ora : @OK_ty Espec) (jm : juicy_mem) (_ : @app_pred rmap ag_rmap (@ext_compat (@OK_ty Espec) ora) w) (_ : @eq environ rho (construct_rho (filter_genv gx) vx tx)) (_ : @eq rmap (m_phi jm) w), @jsafeN (@OK_ty Espec) (@OK_spec Espec) gx (@level rmap ag_rmap w) ora (State vx tx k) jm) (semax.assert_safe_obligation_1 Espec gx vx tx k rho))) m' *)
    change (assert_safe Espec gx vx tx k rho m').
(* Goal: @app_pred rmap ag_rmap (assert_safe Espec gx vx tx k rho) m' *)
    specialize (H m' ltac: (apply necR_level in H1; omega)).
(* Goal: @app_pred rmap ag_rmap (assert_safe Espec gx vx tx k rho) m' *)
    specialize (H m' ltac: (apply necR_refl)).
(* Goal: @app_pred rmap ag_rmap (assert_safe Espec gx vx tx k rho) a' *)
    apply H.
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function (@cons cont' (Kseq c) k)) (construct_rho (filter_genv psi) ve te))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv psi) ve te)) (P' (construct_rho (filter_genv psi) ve te)))) (funassert Delta' (construct_rho (filter_genv psi) ve te))) m' *)
(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
    split; [split |]; auto.
(* Goal: @app_pred rmap ag_rmap PP2 m' *)
    subst PP2.
(* Goal: @app_pred rmap ag_rmap (funassert Delta rho) m' *)
    pose proof funassert_resource Delta rho _ _ (eq_sym H6) (eq_sym H7).
(* Goal: @app_pred rmap ag_rmap (funassert Delta rho) m' *)
    apply H10, H4.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  + hnf; intros.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
    hnf; intros.
(* Goal: @app_pred rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap PP1 (P rho)) PP2) (assert_safe Espec gx vx tx k rho)) y *)
    specialize (H y H0).
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
    hnf; intros.
(* Goal: @app_pred rmap ag_rmap (assert_safe Espec gx vx tx k rho) a' *)
    specialize (H a' H1).
(* Goal: @app_pred rmap ag_rmap (assert_safe Espec gx vx tx k rho) a' *)
    apply H.
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap PP1 (@orp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (@FF rmap ag_rmap)) (P rho))) PP2) a' *)
    destruct H2 as [[? ?] ?].
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function (@cons cont' (Kseq c) k)) (construct_rho (filter_genv psi) ve te))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv psi) ve te)) (P' (construct_rho (filter_genv psi) ve te)))) (funassert Delta' (construct_rho (filter_genv psi) ve te))) m' *)
(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
    split; [split |]; auto.
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (bupd (P rho))) a' *)
    revert H3.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (f rho) (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta rho)) (@andp rmap ag_rmap (allp_fun_id Delta rho) (P rho)))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (f rho) (bupd (@orp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (@FF rmap ag_rmap)) (P' rho)))) *)
    apply sepcon_derives; auto.
(* Goal: @derives rmap ag_rmap (P rho) (bupd (P rho)) *)
    apply bupd_intro.
Qed.

Lemma _guard_bupd:
  forall {Espec: OracleKind} ge Delta (F P: environ -> pred rmap) f k,
    _guard Espec ge Delta (fun rho => F rho * P rho) f k = _guard Espec ge Delta (fun rho => F rho * bupd (P rho)) f k.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  intros.
(* Goal: @eq (@pred nat ag_nat) (_guard Espec ge Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) f k) (_guard Espec ge Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta rho)) (P rho))) f k) *)
  unfold _guard.
(* Goal: @eq (@pred nat ag_nat) (@allp nat ag_nat temp_env (fun tx : temp_env => @allp nat ag_nat env (fun vx : env => @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx)))))) (@allp nat ag_nat temp_env (fun tx : temp_env => @allp nat ag_nat env (fun vx : env => @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta (construct_rho (filter_genv ge) vx tx))) (P (construct_rho (filter_genv ge) vx tx))))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx)))))) *)
  f_equal; extensionality tx.
(* Goal: @eq (@pred nat ag_nat) (@allp nat ag_nat env (fun vx : env => @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx))))) (@allp nat ag_nat env (fun vx : env => @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta (construct_rho (filter_genv ge) vx tx))) (P (construct_rho (filter_genv ge) vx tx))))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx))))) *)
  f_equal; extensionality vx.
(* Goal: @eq (@pred nat ag_nat) (@fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) (funassert Delta (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx)))) (@fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (bupd (P (construct_rho (filter_genv ge) vx tx))))) (funassert Delta (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx)))) *)
  apply assert_safe_bupd.
Qed.
  
Lemma guard_bupd:
  forall {Espec: OracleKind} ge Delta (F P: environ -> pred rmap) k,
    guard Espec ge Delta (fun rho => F rho * P rho) k = guard Espec ge Delta (fun rho => F rho * bupd (P rho)) k.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  intros.
(* Goal: @eq (@pred nat ag_nat) (_guard Espec ge Delta (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (proj_ret_assert P ek vl rho)) (current_function k) (exit_cont ek vl k)) (_guard Espec ge Delta (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (bupd (proj_ret_assert P ek vl rho))) (current_function k) (exit_cont ek vl k)) *)
  apply _guard_bupd.
Qed.

Lemma rguard_bupd:
(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
  forall {Espec: OracleKind} ge Delta F (P: ret_assert) k,
    rguard Espec ge Delta (frame_ret_assert P F) k = rguard Espec ge Delta (frame_ret_assert (bupd_ret_assert P) F) k.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  intros.
(* Goal: @eq (@pred nat ag_nat) (rguard Espec ge Delta' (frame_ret_assert P F) k) (rguard Espec ge Delta' (frame_ret_assert (conj_ret_assert P (fun rho : environ => @prop rmap ag_rmap (typecheck_environ Delta rho))) F) k) *)
  unfold rguard.
(* Goal: @eq (@pred nat ag_nat) (@allp nat ag_nat exitkind (fun ek : exitkind => @allp nat ag_nat (option val) (fun vl : option val => _guard Espec ge Delta' (proj_ret_assert (frame_ret_assert P F) ek vl) (current_function k) (exit_cont ek vl k)))) (@allp nat ag_nat exitkind (fun ek : exitkind => @allp nat ag_nat (option val) (fun vl : option val => _guard Espec ge Delta' (proj_ret_assert (frame_ret_assert (conj_ret_assert P (fun rho : environ => @prop rmap ag_rmap (typecheck_environ Delta rho))) F) ek vl) (current_function k) (exit_cont ek vl k)))) *)
  f_equal; extensionality ek.
(* Goal: @eq (@pred nat ag_nat) (@allp nat ag_nat (option val) (fun vl : option val => _guard Espec ge Delta' (proj_ret_assert (frame_ret_assert P F) ek vl) (current_function k) (exit_cont ek vl k))) (@allp nat ag_nat (option val) (fun vl : option val => _guard Espec ge Delta' (proj_ret_assert (frame_ret_assert (conj_ret_assert P (fun rho : environ => @prop rmap ag_rmap (typecheck_environ Delta rho))) F) ek vl) (current_function k) (exit_cont ek vl k))) *)
  f_equal; extensionality vl.
(* Goal: @eq (@pred nat ag_nat) (_guard Espec ge Delta' (proj_ret_assert (frame_ret_assert P F) ek vl) (current_function k) (exit_cont ek vl k)) (_guard Espec ge Delta' (proj_ret_assert (frame_ret_assert (conj_ret_assert P (fun rho : environ => @prop rmap ag_rmap (typecheck_environ Delta rho))) F) ek vl) (current_function k) (exit_cont ek vl k)) *)
  rewrite !proj_frame.
(* Goal: @eq (@pred nat ag_nat) (_guard Espec ge Delta (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (proj_ret_assert P ek vl rho)) (current_function k) (exit_cont ek vl k)) (_guard Espec ge Delta (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (proj_ret_assert (bupd_ret_assert P) ek vl rho)) (current_function k) (exit_cont ek vl k)) *)
  rewrite proj_bupd_ret_assert.
(* Goal: @eq (@pred nat ag_nat) (_guard Espec ge Delta (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (proj_ret_assert P ek vl rho)) (current_function k) (exit_cont ek vl k)) (_guard Espec ge Delta (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (bupd (proj_ret_assert P ek vl rho))) (current_function k) (exit_cont ek vl k)) *)
  apply _guard_bupd.
Qed.

Definition except_0_ret_assert (Q: ret_assert): ret_assert :=
(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
          {| RA_normal := fun rho => (|> FF || RA_normal Q rho);
             RA_break := fun rho => (|> FF || RA_break Q rho);
             RA_continue := fun rho => (|> FF || RA_continue Q rho);
             RA_return := fun v rho => (|> FF || RA_return Q v rho) |}.

Lemma proj_except_0_ret_assert: forall Q ek vl,
  proj_ret_assert (except_0_ret_assert Q) ek vl = fun rho => |> FF || proj_ret_assert Q ek vl rho.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  intros.
  destruct ek;
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
  auto.
Qed.

(* The following two lemmas is not now used. but after deep embedded hoare logic (SL_as_Logic) is
ported, the frame does not need to be quantified in the semantic definition of semax. Then,
these two lemmas can replace the other two afterwards. *)

Lemma assert_safe_except_0':
  forall {Espec: OracleKind} gx vx tx PP1 PP2 rho (P: environ -> pred rmap) k,
    PP1 && (P rho) && PP2 >=>
    assert_safe Espec gx vx tx k rho =
    PP1 && ((|> FF || P rho)) && PP2 >=>
    assert_safe Espec gx vx tx k rho.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  intros.
(* Goal: @eq (@pred nat ag_nat) (@fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap PP1 (P rho)) PP2) (assert_safe Espec gx vx tx k rho))) (@fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap PP1 (@orp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (@FF rmap ag_rmap)) (P rho))) PP2) (assert_safe Espec gx vx tx k rho))) *)
  apply pred_ext.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  + hnf; intros.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
    hnf; intros.
(* Goal: @app_pred rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap PP1 (P rho)) PP2) (assert_safe Espec gx vx tx k rho)) y *)
    specialize (H y H0).
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
    hnf; intros.
(* Goal: @app_pred rmap ag_rmap (assert_safe Espec gx vx tx k rho) a' *)
    specialize (H a' H1).
(* Goal: @app_pred rmap ag_rmap (assert_safe Espec gx vx tx k rho) a' *)
    clear - H H2.
(* Goal: @app_pred rmap ag_rmap (assert_safe Espec gx vx tx k rho) a' *)
    destruct (level a') eqn:?H in |- *.
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) gx (@level rmap ag_rmap a') ora (State vx tx k) jm *)
    - hnf.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
      intros.
(* Goal: @ex ghost (fun b : ghost => and (@joins ghost ghost_join b (ghost_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) c)) (@ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a')) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a')) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w : rmap => forall (ora : @OK_ty Espec) (jm : juicy_mem) (_ : @app_pred rmap ag_rmap (@ext_compat (@OK_ty Espec) ora) w) (_ : @eq environ rho (construct_rho (filter_genv gx) vx tx)) (_ : @eq rmap (m_phi jm) w), @jsafeN (@OK_ty Espec) (@OK_spec Espec) gx (@level rmap ag_rmap w) ora (State vx tx k) jm) (semax.assert_safe_obligation_1 Espec gx vx tx k rho)) m')))))) *)
      eexists; split; [exact H1 |].
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a')) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a')) (and (@eq ghost (ghost_of m') (ghost_of a')) (@app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w : rmap => forall (ora : @OK_ty Espec) (jm : juicy_mem) (_ : @app_pred rmap ag_rmap (@ext_compat (@OK_ty Espec) ora) w) (_ : @eq environ rho (construct_rho (filter_genv gx) vx tx)) (_ : @eq rmap (m_phi jm) w), @jsafeN (@OK_ty Espec) (@OK_spec Espec) gx (@level rmap ag_rmap w) ora (State vx tx k) jm) (semax.assert_safe_obligation_1 Espec gx vx tx k rho)) m')))) *)
      eexists; split; [reflexivity |].
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta rho)) (P rho)) a *)
      split; auto.
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta rho)) (P rho)) a *)
      split; auto.
(* Goal: @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
      simpl.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
      intros.
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) gx (@level rmap ag_rmap a') ora (State vx tx k) jm *)
      hnf.
(* Goal: @jsafeN_ genv corestate (@OK_ty Espec) (fun ge : genv => @genv_symb_injective fundef type (genv_genv ge)) (cl_core_sem gx) (@OK_spec Espec) gx (@level rmap ag_rmap a') ora (State vx tx k) jm *)
      rewrite H0; constructor.
(* Goal: @app_pred rmap ag_rmap (assert_safe Espec gx vx tx k rho) a' *)
    - apply H.
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap PP1 (@orp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (@FF rmap ag_rmap)) (P rho))) PP2) a' *)
      destruct H2 as [[? ?] ?].
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function (@cons cont' (Kseq c) k)) (construct_rho (filter_genv psi) ve te))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv psi) ve te)) (P' (construct_rho (filter_genv psi) ve te)))) (funassert Delta' (construct_rho (filter_genv psi) ve te))) m' *)
(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
      split; [split |]; auto.
(* Goal: @app_pred rmap ag_rmap (P rho) a' *)
      destruct H2; auto.
(* Goal: @app_pred rmap ag_rmap (P rho) a' *)
      hnf in H2.
(* Goal: @app_pred rmap ag_rmap (P rho) a' *)
      unfold laterM in H2; simpl in H2.
(* Goal: @app_pred rmap ag_rmap (P rho) a' *)
      pose proof levelS_age a' n (eq_sym H0) as [? [? ?]].
(* Goal: @app_pred rmap ag_rmap (P rho) a' *)
      exfalso; apply (H2 x).
(* Goal: @laterR rmap ag_rmap a' x *)
      apply age_laterR.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
      auto.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  + hnf; intros.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
    hnf; intros.
(* Goal: @app_pred rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap PP1 (P rho)) PP2) (assert_safe Espec gx vx tx k rho)) y *)
    specialize (H y H0).
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
    hnf; intros.
(* Goal: @app_pred rmap ag_rmap (assert_safe Espec gx vx tx k rho) a' *)
    specialize (H a' H1).
(* Goal: @app_pred rmap ag_rmap (assert_safe Espec gx vx tx k rho) a' *)
    apply H.
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap PP1 (@orp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (@FF rmap ag_rmap)) (P rho))) PP2) a' *)
    destruct H2 as [[? ?] ?].
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function (@cons cont' (Kseq c) k)) (construct_rho (filter_genv psi) ve te))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv psi) ve te)) (P' (construct_rho (filter_genv psi) ve te)))) (funassert Delta' (construct_rho (filter_genv psi) ve te))) m' *)
(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
    split; [split |]; auto.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
    right; auto.
Qed.

Lemma _guard_except_0':
  forall {Espec: OracleKind} ge Delta (P: environ -> pred rmap) f k,
    _guard Espec ge Delta P f k = _guard Espec ge Delta (fun rho => |> FF || P rho) f k.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  intros.
(* Goal: @eq (@pred nat ag_nat) (_guard Espec ge Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) f k) (_guard Espec ge Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta rho)) (P rho))) f k) *)
  unfold _guard.
(* Goal: @eq (@pred nat ag_nat) (@allp nat ag_nat temp_env (fun tx : temp_env => @allp nat ag_nat env (fun vx : env => @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx)))))) (@allp nat ag_nat temp_env (fun tx : temp_env => @allp nat ag_nat env (fun vx : env => @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta (construct_rho (filter_genv ge) vx tx))) (P (construct_rho (filter_genv ge) vx tx))))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx)))))) *)
  f_equal; extensionality tx.
(* Goal: @eq (@pred nat ag_nat) (@allp nat ag_nat env (fun vx : env => @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx))))) (@allp nat ag_nat env (fun vx : env => @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta (construct_rho (filter_genv ge) vx tx))) (P (construct_rho (filter_genv ge) vx tx))))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx))))) *)
  f_equal; extensionality vx.
(* Goal: @eq (@pred nat ag_nat) (@fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta f (construct_rho (filter_genv ge) vx tx))) (P (construct_rho (filter_genv ge) vx tx))) (funassert Delta (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx)))) (@fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta f (construct_rho (filter_genv ge) vx tx))) (@orp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (@FF rmap ag_rmap)) (P (construct_rho (filter_genv ge) vx tx)))) (funassert Delta (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx)))) *)
  apply assert_safe_except_0'.
Qed.
  
Lemma guard_except_0':
  forall {Espec: OracleKind} ge Delta (P: environ -> pred rmap) k,
    guard Espec ge Delta P k = guard Espec ge Delta (fun rho => |> FF || P rho) k.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  intros.
(* Goal: @eq (@pred nat ag_nat) (_guard Espec ge Delta (proj_ret_assert P ek vl) (current_function k) (exit_cont ek vl k)) (_guard Espec ge Delta (fun rho : environ => @orp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (@FF rmap ag_rmap)) (proj_ret_assert P ek vl rho)) (current_function k) (exit_cont ek vl k)) *)
  apply _guard_except_0'.
Qed.

Lemma rguard_except_0':
(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
  forall {Espec: OracleKind} ge Delta (P: ret_assert) k,
    rguard Espec ge Delta P k = rguard Espec ge Delta (except_0_ret_assert P) k.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  intros.
(* Goal: @eq (@pred nat ag_nat) (rguard Espec ge Delta' (frame_ret_assert P F) k) (rguard Espec ge Delta' (frame_ret_assert (conj_ret_assert P (fun rho : environ => @prop rmap ag_rmap (typecheck_environ Delta rho))) F) k) *)
  unfold rguard.
(* Goal: @eq (@pred nat ag_nat) (@allp nat ag_nat exitkind (fun ek : exitkind => @allp nat ag_nat (option val) (fun vl : option val => _guard Espec ge Delta' (proj_ret_assert (frame_ret_assert P F) ek vl) (current_function k) (exit_cont ek vl k)))) (@allp nat ag_nat exitkind (fun ek : exitkind => @allp nat ag_nat (option val) (fun vl : option val => _guard Espec ge Delta' (proj_ret_assert (frame_ret_assert (conj_ret_assert P (fun rho : environ => @prop rmap ag_rmap (typecheck_environ Delta rho))) F) ek vl) (current_function k) (exit_cont ek vl k)))) *)
  f_equal; extensionality ek.
(* Goal: @eq (@pred nat ag_nat) (@allp nat ag_nat (option val) (fun vl : option val => _guard Espec ge Delta' (proj_ret_assert (frame_ret_assert P F) ek vl) (current_function k) (exit_cont ek vl k))) (@allp nat ag_nat (option val) (fun vl : option val => _guard Espec ge Delta' (proj_ret_assert (frame_ret_assert (conj_ret_assert P (fun rho : environ => @prop rmap ag_rmap (typecheck_environ Delta rho))) F) ek vl) (current_function k) (exit_cont ek vl k))) *)
  f_equal; extensionality vl.
(* Goal: @eq (@pred nat ag_nat) (_guard Espec ge Delta (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (proj_ret_assert Q ek vl rho)) (current_function k) (exit_cont ek vl k)) (_guard Espec ge Delta (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (proj_ret_assert (except_0_ret_assert Q) ek vl rho)) (current_function k) (exit_cont ek vl k)) *)
  rewrite proj_except_0_ret_assert.
(* Goal: @eq (@pred nat ag_nat) (_guard Espec ge Delta (proj_ret_assert P ek vl) (current_function k) (exit_cont ek vl k)) (_guard Espec ge Delta (fun rho : environ => @orp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (@FF rmap ag_rmap)) (proj_ret_assert P ek vl rho)) (current_function k) (exit_cont ek vl k)) *)
  apply _guard_except_0'.
Qed.

Lemma assert_safe_except_0:
  forall {Espec: OracleKind} gx vx tx PP1 PP2 rho (F P: environ -> pred rmap) k,
    PP1 && (F rho * P rho) && PP2 >=>
    assert_safe Espec gx vx tx k rho =
    PP1 && (F rho * (|> FF || P rho)) && PP2 >=>
    assert_safe Espec gx vx tx k rho.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  intros.
(* Goal: @eq (@pred nat ag_nat) (@fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap PP1 (P rho)) PP2) (assert_safe Espec gx vx tx k rho))) (@fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap PP1 (@orp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (@FF rmap ag_rmap)) (P rho))) PP2) (assert_safe Espec gx vx tx k rho))) *)
  apply pred_ext.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  + hnf; intros.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
    hnf; intros.
(* Goal: @app_pred rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap PP1 (P rho)) PP2) (assert_safe Espec gx vx tx k rho)) y *)
    specialize (H y H0).
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
    hnf; intros.
(* Goal: @app_pred rmap ag_rmap (assert_safe Espec gx vx tx k rho) a' *)
    specialize (H a' H1).
(* Goal: @app_pred rmap ag_rmap (assert_safe Espec gx vx tx k rho) a' *)
    clear - H H2.
(* Goal: @app_pred rmap ag_rmap (assert_safe Espec gx vx tx k rho) a' *)
    destruct (level a') eqn:?H in |- *.
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) gx (@level rmap ag_rmap a') ora (State vx tx k) jm *)
    - hnf.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
      intros.
(* Goal: @ex ghost (fun b : ghost => and (@joins ghost ghost_join b (ghost_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) c)) (@ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a')) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a')) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w : rmap => forall (ora : @OK_ty Espec) (jm : juicy_mem) (_ : @app_pred rmap ag_rmap (@ext_compat (@OK_ty Espec) ora) w) (_ : @eq environ rho (construct_rho (filter_genv gx) vx tx)) (_ : @eq rmap (m_phi jm) w), @jsafeN (@OK_ty Espec) (@OK_spec Espec) gx (@level rmap ag_rmap w) ora (State vx tx k) jm) (semax.assert_safe_obligation_1 Espec gx vx tx k rho)) m')))))) *)
      eexists; split; [exact H1 |].
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a')) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a')) (and (@eq ghost (ghost_of m') (ghost_of a')) (@app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w : rmap => forall (ora : @OK_ty Espec) (jm : juicy_mem) (_ : @app_pred rmap ag_rmap (@ext_compat (@OK_ty Espec) ora) w) (_ : @eq environ rho (construct_rho (filter_genv gx) vx tx)) (_ : @eq rmap (m_phi jm) w), @jsafeN (@OK_ty Espec) (@OK_spec Espec) gx (@level rmap ag_rmap w) ora (State vx tx k) jm) (semax.assert_safe_obligation_1 Espec gx vx tx k rho)) m')))) *)
      eexists; split; [reflexivity |].
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta rho)) (P rho)) a *)
      split; auto.
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta rho)) (P rho)) a *)
      split; auto.
(* Goal: @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
      simpl.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
      intros.
(* Goal: @jsafeN (@OK_ty Espec) (@OK_spec Espec) gx (@level rmap ag_rmap a') ora (State vx tx k) jm *)
      hnf.
(* Goal: @jsafeN_ genv corestate (@OK_ty Espec) (fun ge : genv => @genv_symb_injective fundef type (genv_genv ge)) (cl_core_sem gx) (@OK_spec Espec) gx (@level rmap ag_rmap a') ora (State vx tx k) jm *)
      rewrite H0; constructor.
(* Goal: @app_pred rmap ag_rmap (assert_safe Espec gx vx tx k rho) a' *)
    - apply H.
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap PP1 (@orp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (@FF rmap ag_rmap)) (P rho))) PP2) a' *)
      destruct H2 as [[? ?] ?].
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function (@cons cont' (Kseq c) k)) (construct_rho (filter_genv psi) ve te))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv psi) ve te)) (P' (construct_rho (filter_genv psi) ve te)))) (funassert Delta' (construct_rho (filter_genv psi) ve te))) m' *)
(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
      split; [split |]; auto.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
      destruct H2 as [? [? [? [? ?]]]]; auto.
      pose proof join_level _ _ _ H2 as [_ ?].
      rewrite <- H6 in H0; clear H6.
      hnf; eexists; eexists.
      split; [| split]; [exact H2 | exact H4 |].
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
      destruct H5; auto.
      hnf in H5.
      unfold laterM in H5; simpl in H5.
      pose proof levelS_age x0 n (eq_sym H0) as [? [? ?]].
      exfalso; apply (H5 x1).
(* Goal: @laterR rmap ag_rmap a' x *)
      apply age_laterR.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
      auto.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  + hnf; intros.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
    hnf; intros.
(* Goal: @app_pred rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap PP1 (P rho)) PP2) (assert_safe Espec gx vx tx k rho)) y *)
    specialize (H y H0).
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
    hnf; intros.
(* Goal: @app_pred rmap ag_rmap (assert_safe Espec gx vx tx k rho) a' *)
    specialize (H a' H1).
(* Goal: @app_pred rmap ag_rmap (assert_safe Espec gx vx tx k rho) a' *)
    apply H.
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap PP1 (@orp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (@FF rmap ag_rmap)) (P rho))) PP2) a' *)
    destruct H2 as [[? ?] ?].
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function (@cons cont' (Kseq c) k)) (construct_rho (filter_genv psi) ve te))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv psi) ve te)) (P' (construct_rho (filter_genv psi) ve te)))) (funassert Delta' (construct_rho (filter_genv psi) ve te))) m' *)
(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
    split; [split |]; auto.
    destruct H3 as [? [? [? [? ?]]]].
    hnf; eexists; eexists.
    split; [| split]; [exact H3 | exact H5 |].
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
    right; auto.
Qed.

Lemma _guard_except_0:
  forall {Espec: OracleKind} ge Delta (F P: environ -> pred rmap) f k,
    _guard Espec ge Delta (fun rho => F rho * P rho) f k = _guard Espec ge Delta (fun rho => F rho * (|> FF || P rho)) f k.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  intros.
(* Goal: @eq (@pred nat ag_nat) (_guard Espec ge Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) f k) (_guard Espec ge Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta rho)) (P rho))) f k) *)
  unfold _guard.
(* Goal: @eq (@pred nat ag_nat) (@allp nat ag_nat temp_env (fun tx : temp_env => @allp nat ag_nat env (fun vx : env => @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx)))))) (@allp nat ag_nat temp_env (fun tx : temp_env => @allp nat ag_nat env (fun vx : env => @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta (construct_rho (filter_genv ge) vx tx))) (P (construct_rho (filter_genv ge) vx tx))))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx)))))) *)
  f_equal; extensionality tx.
(* Goal: @eq (@pred nat ag_nat) (@allp nat ag_nat env (fun vx : env => @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx))))) (@allp nat ag_nat env (fun vx : env => @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta (construct_rho (filter_genv ge) vx tx))) (P (construct_rho (filter_genv ge) vx tx))))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx))))) *)
  f_equal; extensionality vx.
(* Goal: @eq (@pred nat ag_nat) (@fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) (funassert Delta (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx)))) (@fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (@orp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (@FF rmap ag_rmap)) (P (construct_rho (filter_genv ge) vx tx))))) (funassert Delta (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx)))) *)
  apply assert_safe_except_0.
Qed.

Lemma guard_except_0: 
  forall {Espec: OracleKind} ge Delta (F P: environ -> pred rmap) k,
    guard Espec ge Delta (fun rho => F rho * P rho) k =
    guard Espec ge Delta (fun rho => F rho * (|> FF || P rho)) k.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  intros.
(* Goal: @eq (@pred nat ag_nat) (_guard Espec ge Delta (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (proj_ret_assert Q ek vl rho)) (current_function k) (exit_cont ek vl k)) (_guard Espec ge Delta (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (@orp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (@FF rmap ag_rmap)) (proj_ret_assert Q ek vl rho))) (current_function k) (exit_cont ek vl k)) *)
  apply _guard_except_0.
Qed.

Lemma rguard_except_0:
  forall {Espec: OracleKind} ge Delta (F: environ -> pred rmap) Q k,
    rguard Espec ge Delta (frame_ret_assert Q F) k =
    rguard Espec ge Delta (frame_ret_assert (except_0_ret_assert Q) F) k.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  intros.
(* Goal: @eq (@pred nat ag_nat) (rguard Espec ge Delta' (frame_ret_assert P F) k) (rguard Espec ge Delta' (frame_ret_assert (conj_ret_assert P (fun rho : environ => @prop rmap ag_rmap (typecheck_environ Delta rho))) F) k) *)
  unfold rguard.
(* Goal: @eq (@pred nat ag_nat) (@allp nat ag_nat exitkind (fun ek : exitkind => @allp nat ag_nat (option val) (fun vl : option val => _guard Espec ge Delta' (proj_ret_assert (frame_ret_assert P F) ek vl) (current_function k) (exit_cont ek vl k)))) (@allp nat ag_nat exitkind (fun ek : exitkind => @allp nat ag_nat (option val) (fun vl : option val => _guard Espec ge Delta' (proj_ret_assert (frame_ret_assert (conj_ret_assert P (fun rho : environ => @prop rmap ag_rmap (typecheck_environ Delta rho))) F) ek vl) (current_function k) (exit_cont ek vl k)))) *)
  f_equal; extensionality ek.
(* Goal: @eq (@pred nat ag_nat) (@allp nat ag_nat (option val) (fun vl : option val => _guard Espec ge Delta' (proj_ret_assert (frame_ret_assert P F) ek vl) (current_function k) (exit_cont ek vl k))) (@allp nat ag_nat (option val) (fun vl : option val => _guard Espec ge Delta' (proj_ret_assert (frame_ret_assert (conj_ret_assert P (fun rho : environ => @prop rmap ag_rmap (typecheck_environ Delta rho))) F) ek vl) (current_function k) (exit_cont ek vl k))) *)
  f_equal; extensionality vl.
(* Goal: @eq (@pred nat ag_nat) (_guard Espec ge Delta' (proj_ret_assert (frame_ret_assert P F) ek vl) (current_function k) (exit_cont ek vl k)) (_guard Espec ge Delta' (proj_ret_assert (frame_ret_assert (conj_ret_assert P (fun rho : environ => @prop rmap ag_rmap (typecheck_environ Delta rho))) F) ek vl) (current_function k) (exit_cont ek vl k)) *)
  rewrite !proj_frame.
(* Goal: @eq (@pred nat ag_nat) (_guard Espec ge Delta (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (proj_ret_assert Q ek vl rho)) (current_function k) (exit_cont ek vl k)) (_guard Espec ge Delta (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (proj_ret_assert (except_0_ret_assert Q) ek vl rho)) (current_function k) (exit_cont ek vl k)) *)
  rewrite proj_except_0_ret_assert.
(* Goal: @eq (@pred nat ag_nat) (_guard Espec ge Delta (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (proj_ret_assert Q ek vl rho)) (current_function k) (exit_cont ek vl k)) (_guard Espec ge Delta (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (@orp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (@FF rmap ag_rmap)) (proj_ret_assert Q ek vl rho))) (current_function k) (exit_cont ek vl k)) *)
  apply _guard_except_0.
Qed.

Lemma _guard_allp_fun_id:
  forall {Espec: OracleKind} ge Delta' Delta (F P: environ -> pred rmap) f k,
    tycontext_sub Delta Delta' ->
    _guard Espec ge Delta' (fun rho => F rho * P rho) f k = _guard Espec ge Delta' (fun rho => F rho * (allp_fun_id Delta rho && P rho)) f k.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  intros.
(* Goal: @eq (@pred nat ag_nat) (_guard Espec ge Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) f k) (_guard Espec ge Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta rho)) (P rho))) f k) *)
  unfold _guard.
(* Goal: @eq (@pred nat ag_nat) (@allp nat ag_nat temp_env (fun tx : temp_env => @allp nat ag_nat env (fun vx : env => @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx)))))) (@allp nat ag_nat temp_env (fun tx : temp_env => @allp nat ag_nat env (fun vx : env => @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta (construct_rho (filter_genv ge) vx tx))) (P (construct_rho (filter_genv ge) vx tx))))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx)))))) *)
  f_equal; extensionality tx.
(* Goal: @eq (@pred nat ag_nat) (@allp nat ag_nat env (fun vx : env => @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx))))) (@allp nat ag_nat env (fun vx : env => @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta (construct_rho (filter_genv ge) vx tx))) (P (construct_rho (filter_genv ge) vx tx))))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx))))) *)
  f_equal; extensionality vx.
(* Goal: @eq (@pred rmap ag_rmap) (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@prop rmap ag_rmap (typecheck_environ Delta (construct_rho (filter_genv ge) vx tx)))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) *)
  f_equal.
(* Goal: @eq (@pred rmap ag_rmap) (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@prop rmap ag_rmap (typecheck_environ Delta (construct_rho (filter_genv ge) vx tx)))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) *)
  f_equal.
(* Goal: @eq (@pred rmap ag_rmap) (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (@andp rmap ag_rmap (allp_fun_id Delta (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx))))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) *)
  rewrite !andp_assoc.
(* Goal: @eq (@pred rmap ag_rmap) (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@prop rmap ag_rmap (typecheck_environ Delta (construct_rho (filter_genv ge) vx tx)))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) *)
  f_equal.
(* Goal: @eq (@pred rmap ag_rmap) (@andp rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) (@andp rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (@andp rmap ag_rmap (allp_fun_id Delta (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) *)
  rewrite corable_sepcon_andp1 by apply corable_allp_fun_id.
(* Goal: @eq (@pred rmap ag_rmap) (@andp rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) (@andp rmap ag_rmap (@andp rmap ag_rmap (allp_fun_id Delta (construct_rho (filter_genv ge) vx tx)) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) *)
  rewrite (andp_comm (allp_fun_id _ _ )), andp_assoc.
(* Goal: @eq (@pred rmap ag_rmap) (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@prop rmap ag_rmap (typecheck_environ Delta (construct_rho (filter_genv ge) vx tx)))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) *)
  f_equal.
(* Goal: @eq mpred (funassert Delta' (construct_rho (filter_genv ge) vx tx)) (@andp rmap ag_rmap (allp_fun_id Delta (construct_rho (filter_genv ge) vx tx)) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) *)
  apply pred_ext; [apply andp_right; auto | apply andp_left2; auto].
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
  apply funassert_allp_fun_id_sub; auto.
Qed.

Lemma guard_allp_fun_id: forall {Espec: OracleKind} ge Delta' Delta (F P: environ -> pred rmap) k,
  tycontext_sub Delta Delta' ->
  guard Espec ge Delta' (fun rho => F rho * P rho) k = guard Espec ge Delta' (fun rho => F rho * (allp_fun_id Delta rho && P rho)) k.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  intros.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
  apply _guard_allp_fun_id; auto.
Qed.

Lemma rguard_allp_fun_id: forall {Espec: OracleKind} ge Delta' Delta (F: environ -> pred rmap) P k,
  tycontext_sub Delta Delta' ->
  rguard Espec ge Delta' (frame_ret_assert P F) k = rguard Espec ge Delta' (frame_ret_assert (conj_ret_assert P (allp_fun_id Delta)) F) k.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  intros.
(* Goal: @eq (@pred nat ag_nat) (rguard Espec ge Delta' (frame_ret_assert P F) k) (rguard Espec ge Delta' (frame_ret_assert (conj_ret_assert P (fun rho : environ => @prop rmap ag_rmap (typecheck_environ Delta rho))) F) k) *)
  unfold rguard.
(* Goal: @eq (@pred nat ag_nat) (@allp nat ag_nat exitkind (fun ek : exitkind => @allp nat ag_nat (option val) (fun vl : option val => _guard Espec ge Delta' (proj_ret_assert (frame_ret_assert P F) ek vl) (current_function k) (exit_cont ek vl k)))) (@allp nat ag_nat exitkind (fun ek : exitkind => @allp nat ag_nat (option val) (fun vl : option val => _guard Espec ge Delta' (proj_ret_assert (frame_ret_assert (conj_ret_assert P (fun rho : environ => @prop rmap ag_rmap (typecheck_environ Delta rho))) F) ek vl) (current_function k) (exit_cont ek vl k)))) *)
  f_equal; extensionality ek.
(* Goal: @eq (@pred nat ag_nat) (@allp nat ag_nat (option val) (fun vl : option val => _guard Espec ge Delta' (proj_ret_assert (frame_ret_assert P F) ek vl) (current_function k) (exit_cont ek vl k))) (@allp nat ag_nat (option val) (fun vl : option val => _guard Espec ge Delta' (proj_ret_assert (frame_ret_assert (conj_ret_assert P (fun rho : environ => @prop rmap ag_rmap (typecheck_environ Delta rho))) F) ek vl) (current_function k) (exit_cont ek vl k))) *)
  f_equal; extensionality vl.
(* Goal: @eq (@pred nat ag_nat) (_guard Espec ge Delta' (proj_ret_assert (frame_ret_assert P F) ek vl) (current_function k) (exit_cont ek vl k)) (_guard Espec ge Delta' (proj_ret_assert (frame_ret_assert (conj_ret_assert P (fun rho : environ => @prop rmap ag_rmap (typecheck_environ Delta rho))) F) ek vl) (current_function k) (exit_cont ek vl k)) *)
  rewrite !proj_frame.
(* Goal: @eq (@pred nat ag_nat) (_guard Espec ge Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (proj_ret_assert P ek vl rho)) (current_function k) (exit_cont ek vl k)) (_guard Espec ge Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (proj_ret_assert (conj_ret_assert P (fun rho0 : environ => @prop rmap ag_rmap (typecheck_environ Delta rho0))) ek vl rho)) (current_function k) (exit_cont ek vl k)) *)
  rewrite proj_conj.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
  apply _guard_allp_fun_id; auto.
Qed.

Lemma _guard_tc_environ:
  forall {Espec: OracleKind} ge Delta' Delta (F P: environ -> pred rmap) f k,
    tycontext_sub Delta Delta' ->
    _guard Espec ge Delta' (fun rho => F rho * P rho) f k = _guard Espec ge Delta' (fun rho => F rho * (!! typecheck_environ Delta rho && P rho)) f k.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  intros.
(* Goal: @eq (@pred nat ag_nat) (_guard Espec ge Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) f k) (_guard Espec ge Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta rho)) (P rho))) f k) *)
  unfold _guard.
(* Goal: @eq (@pred nat ag_nat) (@allp nat ag_nat temp_env (fun tx : temp_env => @allp nat ag_nat env (fun vx : env => @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx)))))) (@allp nat ag_nat temp_env (fun tx : temp_env => @allp nat ag_nat env (fun vx : env => @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta (construct_rho (filter_genv ge) vx tx))) (P (construct_rho (filter_genv ge) vx tx))))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx)))))) *)
  f_equal; extensionality tx.
(* Goal: @eq (@pred nat ag_nat) (@allp nat ag_nat env (fun vx : env => @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx))))) (@allp nat ag_nat env (fun vx : env => @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta (construct_rho (filter_genv ge) vx tx))) (P (construct_rho (filter_genv ge) vx tx))))) (funassert Delta' (construct_rho (filter_genv ge) vx tx))) (assert_safe Espec ge vx tx k (construct_rho (filter_genv ge) vx tx))))) *)
  f_equal; extensionality vx.
(* Goal: @eq (@pred rmap ag_rmap) (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@prop rmap ag_rmap (typecheck_environ Delta (construct_rho (filter_genv ge) vx tx)))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) *)
  f_equal.
(* Goal: @eq (@pred rmap ag_rmap) (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@prop rmap ag_rmap (typecheck_environ Delta (construct_rho (filter_genv ge) vx tx)))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) *)
  f_equal.
(* Goal: @eq (@pred rmap ag_rmap) (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@prop rmap ag_rmap (typecheck_environ Delta (construct_rho (filter_genv ge) vx tx)))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) *)
  f_equal.
(* Goal: @eq (@pred rmap ag_rmap) (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta (construct_rho (filter_genv ge) vx tx))) (P (construct_rho (filter_genv ge) vx tx))))) *)
  rewrite corable_sepcon_andp1 by apply corable_prop.
  rewrite <- andp_assoc.
(* Goal: @eq (@pred rmap ag_rmap) (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@prop rmap ag_rmap (typecheck_environ Delta (construct_rho (filter_genv ge) vx tx)))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F (construct_rho (filter_genv ge) vx tx)) (P (construct_rho (filter_genv ge) vx tx)))) *)
  f_equal.
(* Goal: @eq (@pred rmap ag_rmap) (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@prop rmap ag_rmap (typecheck_environ Delta (construct_rho (filter_genv ge) vx tx)))) *)
  apply pred_ext; [apply andp_right; auto | apply andp_left1; auto].
(* Goal: @derives rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' f (construct_rho (filter_genv ge) vx tx))) (@prop rmap ag_rmap (typecheck_environ Delta (construct_rho (filter_genv ge) vx tx))) *)
  intros ? ?; simpl in *.
(* Goal: typecheck_environ Delta (construct_rho (filter_genv ge) vx tx) *)
  destruct H0 as [? _].
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
  eapply typecheck_environ_sub; eauto.
Qed.

Lemma guard_tc_environ: forall {Espec: OracleKind} ge Delta' Delta (F P: environ -> pred rmap) k,
  tycontext_sub Delta Delta' ->
  guard Espec ge Delta' (fun rho => F rho * P rho) k = guard Espec ge Delta' (fun rho => F rho * (!! typecheck_environ Delta rho && P rho)) k.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  intros.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
  apply _guard_tc_environ; auto.
Qed.

Lemma rguard_tc_environ: forall {Espec: OracleKind} ge Delta' Delta (F: environ -> pred rmap) P k,
  tycontext_sub Delta Delta' ->
  rguard Espec ge Delta' (frame_ret_assert P F) k = rguard Espec ge Delta' (frame_ret_assert (conj_ret_assert P (fun rho => !! typecheck_environ Delta rho)) F) k.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  intros.
(* Goal: @eq (@pred nat ag_nat) (rguard Espec ge Delta' (frame_ret_assert P F) k) (rguard Espec ge Delta' (frame_ret_assert (conj_ret_assert P (fun rho : environ => @prop rmap ag_rmap (typecheck_environ Delta rho))) F) k) *)
  unfold rguard.
(* Goal: @eq (@pred nat ag_nat) (@allp nat ag_nat exitkind (fun ek : exitkind => @allp nat ag_nat (option val) (fun vl : option val => _guard Espec ge Delta' (proj_ret_assert (frame_ret_assert P F) ek vl) (current_function k) (exit_cont ek vl k)))) (@allp nat ag_nat exitkind (fun ek : exitkind => @allp nat ag_nat (option val) (fun vl : option val => _guard Espec ge Delta' (proj_ret_assert (frame_ret_assert (conj_ret_assert P (fun rho : environ => @prop rmap ag_rmap (typecheck_environ Delta rho))) F) ek vl) (current_function k) (exit_cont ek vl k)))) *)
  f_equal; extensionality ek.
(* Goal: @eq (@pred nat ag_nat) (@allp nat ag_nat (option val) (fun vl : option val => _guard Espec ge Delta' (proj_ret_assert (frame_ret_assert P F) ek vl) (current_function k) (exit_cont ek vl k))) (@allp nat ag_nat (option val) (fun vl : option val => _guard Espec ge Delta' (proj_ret_assert (frame_ret_assert (conj_ret_assert P (fun rho : environ => @prop rmap ag_rmap (typecheck_environ Delta rho))) F) ek vl) (current_function k) (exit_cont ek vl k))) *)
  f_equal; extensionality vl.
(* Goal: @eq (@pred nat ag_nat) (_guard Espec ge Delta' (proj_ret_assert (frame_ret_assert P F) ek vl) (current_function k) (exit_cont ek vl k)) (_guard Espec ge Delta' (proj_ret_assert (frame_ret_assert (conj_ret_assert P (fun rho : environ => @prop rmap ag_rmap (typecheck_environ Delta rho))) F) ek vl) (current_function k) (exit_cont ek vl k)) *)
  rewrite !proj_frame.
(* Goal: @eq (@pred nat ag_nat) (_guard Espec ge Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (proj_ret_assert P ek vl rho)) (current_function k) (exit_cont ek vl k)) (_guard Espec ge Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (proj_ret_assert (conj_ret_assert P (fun rho0 : environ => @prop rmap ag_rmap (typecheck_environ Delta rho0))) ek vl rho)) (current_function k) (exit_cont ek vl k)) *)
  rewrite proj_conj.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
  apply _guard_tc_environ; auto.
Qed.

(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
Lemma semax_conseq {CS: compspecs} {Espec: OracleKind}:
 forall Delta P' (R': ret_assert) P c (R: ret_assert) ,
   (forall rho,  !!(typecheck_environ Delta rho) && (allp_fun_id Delta rho && P rho)
                   |-- bupd (|> FF || P' rho) )%pred ->
   (forall rho,  !!(typecheck_environ Delta rho) && (allp_fun_id Delta rho && RA_normal R' rho)
                   |-- bupd (|> FF || RA_normal R rho)) ->
   (forall rho, !! (typecheck_environ Delta rho) && (allp_fun_id Delta rho && RA_break R' rho)
                   |-- bupd (|> FF || RA_break R rho)) ->
   (forall rho, !! (typecheck_environ Delta rho) && (allp_fun_id Delta rho && RA_continue R' rho)
                   |-- bupd (|> FF || RA_continue R rho)) ->
   (forall vl rho, !! (typecheck_environ Delta rho) && (allp_fun_id Delta rho && RA_return R' vl rho)
                   |-- bupd (|> FF || RA_return R vl rho)) ->
   semax Espec Delta P' c R' ->  semax Espec Delta P c R.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
  intros.
  assert (semax' Espec Delta P' c R' |-- semax' Espec Delta P c R);
    [clear H4 | exact (fun n => H5 n (H4 n))].
(* Goal: @derives nat ag_nat (@semax' CS Espec Delta P c R') (@semax' CS Espec Delta P c R) *)
  rewrite semax_fold_unfold.
(* Goal: @derives 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 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))))))))) (@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))))))))) *)
  apply allp_derives; intros gx.
(* Goal: @derives nat ag_nat (@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)))))))) (@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)))))))) *)
  apply allp_derives; intros Delta'.
(* Goal: @derives nat ag_nat (@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))))))) (@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))))))) *)
  apply prop_imp_derives; intros [? _].
(* Goal: @derives nat ag_nat (@imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars c F)) (rguard Espec psi Delta' (frame_ret_assert R F) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P' rho)) (@cons cont' (Kseq c) k))) (@imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars c F)) (rguard Espec psi Delta' (frame_ret_assert R F) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) (@cons cont' (Kseq c) k))) *)
  apply imp_derives; auto.
(* Goal: @derives nat ag_nat (@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))))) (@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))))) *)
  apply allp_derives; intros k.
(* Goal: @derives nat ag_nat (@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)))) (@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)))) *)
  apply allp_derives; intros f.
(* Goal: @derives nat ag_nat (@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))) (@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))) *)
  apply imp_derives; [apply andp_derives; auto |].
  + erewrite (rguard_allp_fun_id _ _ _ _ R') by eauto.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
    erewrite (rguard_tc_environ _ _ _ _ (conj_ret_assert _ _)) by eauto.
(* Goal: @derives nat ag_nat (rguard Espec gx Delta' (frame_ret_assert R f) k) (rguard Espec gx Delta' (frame_ret_assert (conj_ret_assert (conj_ret_assert R' (allp_fun_id Delta)) (fun rho : environ => @prop rmap ag_rmap (typecheck_environ Delta rho))) f) k) *)
    rewrite (rguard_except_0 _ _ _ R).
(* Goal: @derives nat ag_nat (rguard Espec gx Delta' (frame_ret_assert (except_0_ret_assert R) f) k) (rguard Espec gx Delta' (frame_ret_assert (conj_ret_assert (conj_ret_assert R' (allp_fun_id Delta)) (fun rho : environ => @prop rmap ag_rmap (typecheck_environ Delta rho))) f) k) *)
    rewrite (rguard_bupd _ _ _ (except_0_ret_assert _)).
(* Goal: @derives nat ag_nat (rguard Espec gx Delta' (frame_ret_assert (bupd_ret_assert (except_0_ret_assert R)) f) k) (rguard Espec gx Delta' (frame_ret_assert (conj_ret_assert (conj_ret_assert R' (allp_fun_id Delta)) (fun rho : environ => @prop rmap ag_rmap (typecheck_environ Delta rho))) f) k) *)
    apply rguard_mono.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
    intros.
(* Goal: @derives rmap ag_rmap (proj_ret_assert (frame_ret_assert (conj_ret_assert (conj_ret_assert R' (allp_fun_id Delta)) (fun rho : environ => @prop rmap ag_rmap (typecheck_environ Delta rho))) f) rk vl rho) (proj_ret_assert (frame_ret_assert (bupd_ret_assert (except_0_ret_assert R)) f) rk vl rho) *)
    rewrite proj_frame, proj_conj, proj_conj.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (f rho) (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta rho)) (@andp rmap ag_rmap (allp_fun_id Delta rho) (proj_ret_assert R' rk vl rho)))) (proj_ret_assert (frame_ret_assert (bupd_ret_assert (except_0_ret_assert R)) f) rk vl rho) *)
    rewrite proj_frame, proj_bupd_ret_assert, proj_except_0_ret_assert.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (f rho) (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta rho)) (@andp rmap ag_rmap (allp_fun_id Delta rho) (P rho)))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (f rho) (bupd (@orp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (@FF rmap ag_rmap)) (P' rho)))) *)
    apply sepcon_derives; auto.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
    destruct rk; unfold proj_ret_assert; auto.
  + erewrite (guard_allp_fun_id _ _ _ _ P) by eauto.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
    erewrite (guard_tc_environ _ _ _ _ (fun rho => allp_fun_id Delta rho && P rho)) by eauto.
(* Goal: @derives nat ag_nat (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)) (guard Espec gx Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (f rho) (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta rho)) (@andp rmap ag_rmap (allp_fun_id Delta rho) (P rho)))) (@cons cont' (Kseq c) k)) *)
    rewrite (guard_except_0 _ _ _ P').
(* Goal: @derives nat ag_nat (guard Espec gx Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (f rho) (@orp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (@FF rmap ag_rmap)) (P' rho))) (@cons cont' (Kseq c) k)) (guard Espec gx Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (f rho) (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta rho)) (@andp rmap ag_rmap (allp_fun_id Delta rho) (P rho)))) (@cons cont' (Kseq c) k)) *)
    rewrite (guard_bupd _ _ _ (fun rho => |> FF || P' rho)).
(* Goal: @derives nat ag_nat (guard Espec gx Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (f rho) (bupd (@orp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (@FF rmap ag_rmap)) (P' rho)))) (@cons cont' (Kseq c) k)) (guard Espec gx Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (f rho) (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta rho)) (@andp rmap ag_rmap (allp_fun_id Delta rho) (P rho)))) (@cons cont' (Kseq c) k)) *)
    apply guard_mono.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
    intros.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (f rho) (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta rho)) (@andp rmap ag_rmap (allp_fun_id Delta rho) (P rho)))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (f rho) (bupd (@orp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (@FF rmap ag_rmap)) (P' rho)))) *)
    apply sepcon_derives; auto.
Qed.

(* Part 2: Deriving simpler and older version of consequence rules from semax_conseq. *)
Lemma semax'_post_bupd:
(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
 forall {CS: compspecs} {Espec: OracleKind} (R': ret_assert) Delta (R: ret_assert) P c,
   (forall ek vl rho,  !!(typecheck_environ Delta rho ) && 
                proj_ret_assert R' ek vl rho 
         |-- bupd (proj_ret_assert R ek vl rho)) ->
   semax' Espec Delta P c R' |-- semax' Espec Delta P c R.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
intros.
(* Goal: @derives nat ag_nat (@semax' CS Espec Delta P c R') (@semax' CS Espec Delta P c R) *)
rewrite semax_fold_unfold.
(* Goal: @derives 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 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))))))))) (@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))))))))) *)
apply allp_derives; intro psi.
(* Goal: @derives nat ag_nat (@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 psi) (@cenv_cs CS)))) (@imp nat ag_nat (@believe CS Espec Delta' psi 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 psi Delta' (frame_ret_assert R F) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P' rho)) (@cons cont' (Kseq c) k)))))))) (@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 psi) (@cenv_cs CS)))) (@imp nat ag_nat (@believe CS Espec Delta' psi 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 psi Delta' (frame_ret_assert R F) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) (@cons cont' (Kseq c) k)))))))) *)
apply allp_derives; intro Delta'.
(* Goal: @derives nat ag_nat (@imp nat ag_nat (@prop nat ag_nat (and (tycontext_sub Delta Delta') (@eq composite_env (genv_cenv psi) (@cenv_cs CS)))) (@imp nat ag_nat (@believe CS Espec Delta' psi 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 psi Delta' (frame_ret_assert R F) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P' rho)) (@cons cont' (Kseq c) k))))))) (@imp nat ag_nat (@prop nat ag_nat (and (tycontext_sub Delta Delta') (@eq composite_env (genv_cenv psi) (@cenv_cs CS)))) (@imp nat ag_nat (@believe CS Espec Delta' psi 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 psi Delta' (frame_ret_assert R F) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) (@cons cont' (Kseq c) k))))))) *)
apply prop_imp_derives; intros [TS HGG].
(* Goal: @derives nat ag_nat (@imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars c F)) (rguard Espec psi Delta' (frame_ret_assert R F) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P' rho)) (@cons cont' (Kseq c) k))) (@imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars c F)) (rguard Espec psi Delta' (frame_ret_assert R F) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) (@cons cont' (Kseq c) k))) *)
apply imp_derives; auto.
(* Goal: @derives nat ag_nat (@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 psi Delta' (frame_ret_assert R F) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P' rho)) (@cons cont' (Kseq c) k))))) (@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 psi Delta' (frame_ret_assert R F) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) (@cons cont' (Kseq c) k))))) *)
apply allp_derives; intro k.
(* Goal: @derives nat ag_nat (@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 psi Delta' (frame_ret_assert R F) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P' rho)) (@cons cont' (Kseq c) k)))) (@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 psi Delta' (frame_ret_assert R F) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) (@cons cont' (Kseq c) k)))) *)
apply allp_derives; intro F.
(* Goal: @derives nat ag_nat (@imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars c F)) (rguard Espec psi Delta' (frame_ret_assert R F) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P' rho)) (@cons cont' (Kseq c) k))) (@imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars c F)) (rguard Espec psi Delta' (frame_ret_assert R F) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) (@cons cont' (Kseq c) k))) *)
apply imp_derives; auto.
(* Goal: @derives nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars c F)) (rguard Espec psi Delta' (frame_ret_assert R F) k)) (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars c F)) (rguard Espec psi Delta' (frame_ret_assert R' F) k)) *)
unfold rguard, guard.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
apply andp_derives; auto.
(* Goal: @derives nat ag_nat (@allp nat ag_nat exitkind (fun ek : exitkind => @allp nat ag_nat (option val) (fun vl : option val => _guard Espec psi Delta' (proj_ret_assert (frame_ret_assert R F) ek vl) (current_function k) (exit_cont ek vl k)))) (@allp nat ag_nat exitkind (fun ek : exitkind => @allp nat ag_nat (option val) (fun vl : option val => _guard Espec psi Delta' (proj_ret_assert (frame_ret_assert R' F) ek vl) (current_function k) (exit_cont ek vl k)))) *)
apply allp_derives; intro ek.
(* Goal: @derives nat ag_nat (@allp nat ag_nat (option val) (fun vl : option val => _guard Espec psi Delta' (proj_ret_assert (frame_ret_assert R F) ek vl) (current_function k) (exit_cont ek vl k))) (@allp nat ag_nat (option val) (fun vl : option val => _guard Espec psi Delta' (proj_ret_assert (frame_ret_assert R' F) ek vl) (current_function k) (exit_cont ek vl k))) *)
apply allp_derives; intro vl.
(* Goal: @derives nat ag_nat (_guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P' rho)) (current_function (@cons cont' (Kseq c) k)) (@cons cont' (Kseq c) k)) (_guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) (current_function (@cons cont' (Kseq c) k)) (@cons cont' (Kseq c) k)) *)
apply allp_derives; intro te.
(* Goal: @derives nat ag_nat (@allp nat ag_nat env (fun vx : env => let rho := construct_rho (filter_genv psi) vx te in @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function (@cons cont' (Kseq c) k)) rho)) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P' rho))) (funassert Delta' rho)) (assert_safe Espec psi vx te (@cons cont' (Kseq c) k) rho)))) (@allp nat ag_nat env (fun vx : env => let rho := construct_rho (filter_genv psi) vx te in @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function (@cons cont' (Kseq c) k)) rho)) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho))) (funassert Delta' rho)) (assert_safe Espec psi vx te (@cons cont' (Kseq c) k) rho)))) *)
apply allp_derives; intro ve.
(* Goal: @derives nat ag_nat (let rho := construct_rho (filter_genv psi) ve te in @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function (@cons cont' (Kseq c) k)) rho)) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P' rho))) (funassert Delta' rho)) (assert_safe Espec psi ve te (@cons cont' (Kseq c) k) rho))) (let rho := construct_rho (filter_genv psi) ve te in @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function (@cons cont' (Kseq c) k)) rho)) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho))) (funassert Delta' rho)) (assert_safe Espec psi ve te (@cons cont' (Kseq c) k) rho))) *)
intros ? ?.
(* Goal: @app_pred nat ag_nat (let rho := construct_rho (filter_genv psi) ve te in @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function (@cons cont' (Kseq c) k)) rho)) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho))) (funassert Delta' rho)) (assert_safe Espec psi ve te (@cons cont' (Kseq c) k) rho))) a *)
intros ? ? ? ? ?.
(* Goal: @app_pred rmap ag_rmap (assert_safe Espec psi ve te (@cons cont' (Kseq c) k) (construct_rho (filter_genv psi) ve te)) a' *)
destruct H3 as [[? HFP] ?].
assert (bupd (proj_ret_assert (frame_ret_assert R F) ek vl
  (construct_rho (filter_genv psi) ve te)) a') as HFP'.
(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
{ specialize (H ek vl (construct_rho (filter_genv psi) ve te)).
(* Goal: @app_pred rmap ag_rmap (bupd (proj_ret_assert (frame_ret_assert R F) ek vl (construct_rho (filter_genv psi) ve te))) a' *)
  rewrite prop_true_andp in H.
  destruct ek; simpl in * |-.
  * destruct R'.
(* Goal: @app_pred rmap ag_rmap (bupd (proj_ret_assert (frame_ret_assert R F) EK_return vl (construct_rho (filter_genv psi) ve te))) a' *)
    eapply sepcon_derives in HFP; [| apply H | apply derives_refl].
(* Goal: @app_pred rmap ag_rmap (bupd (proj_ret_assert (frame_ret_assert R F) EK_return vl (construct_rho (filter_genv psi) ve te))) a' *)
    apply bupd_frame_r in HFP.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
    destruct R; auto.
  * destruct R'.
(* Goal: @app_pred rmap ag_rmap (bupd (proj_ret_assert (frame_ret_assert R F) EK_return vl (construct_rho (filter_genv psi) ve te))) a' *)
    eapply sepcon_derives in HFP; [| apply H | apply derives_refl].
(* Goal: @app_pred rmap ag_rmap (bupd (proj_ret_assert (frame_ret_assert R F) EK_return vl (construct_rho (filter_genv psi) ve te))) a' *)
    apply bupd_frame_r in HFP.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
    destruct R; auto.
  * destruct R'.
(* Goal: @app_pred rmap ag_rmap (bupd (proj_ret_assert (frame_ret_assert R F) EK_return vl (construct_rho (filter_genv psi) ve te))) a' *)
    eapply sepcon_derives in HFP; [| apply H | apply derives_refl].
(* Goal: @app_pred rmap ag_rmap (bupd (proj_ret_assert (frame_ret_assert R F) EK_return vl (construct_rho (filter_genv psi) ve te))) a' *)
    apply bupd_frame_r in HFP.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
    destruct R; auto.
  * destruct R'.
(* Goal: @app_pred rmap ag_rmap (bupd (proj_ret_assert (frame_ret_assert R F) EK_return vl (construct_rho (filter_genv psi) ve te))) a' *)
    eapply sepcon_derives in HFP; [| apply H | apply derives_refl].
(* Goal: @app_pred rmap ag_rmap (bupd (proj_ret_assert (frame_ret_assert R F) EK_return vl (construct_rho (filter_genv psi) ve te))) a' *)
    apply bupd_frame_r in HFP.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
    destruct R; auto.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
  * destruct H3; eapply typecheck_environ_sub; eauto. }
assert ((bupd (assert_safe Espec psi ve te (exit_cont ek vl k)
  (construct_rho (filter_genv psi) ve te))) a') as Hsafe.
(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
{ intros ? J.
(* Goal: @ex ghost (fun b : ghost => and (@joins ghost ghost_join b (ghost_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) c0)) (@ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a')) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a')) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap (assert_safe Espec psi ve te (exit_cont ek vl k) (construct_rho (filter_genv psi) ve te)) m')))))) *)
  destruct (HFP' _ J) as (b & ? & m' & ? & ? & ? & ?).
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta rho)) (P rho)) a *)
  exists b; split; auto; exists m'; repeat split; auto.
(* Goal: @app_pred rmap ag_rmap (bupd (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w : rmap => forall (ora : @OK_ty Espec) (jm : juicy_mem) (_ : @app_pred rmap ag_rmap (@ext_compat (@OK_ty Espec) ora) w) (_ : @eq environ (construct_rho (filter_genv psi) ve te) (construct_rho (filter_genv psi) ve te)) (_ : @eq rmap (m_phi jm) w), @jsafeN (@OK_ty Espec) (@OK_spec Espec) psi (@level rmap ag_rmap w) ora (State ve te (@cons cont' (Kseq c) k)) jm) (semax.assert_safe_obligation_1 Espec psi ve te (@cons cont' (Kseq c) k) (construct_rho (filter_genv psi) ve te)))) m' *)
(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
  pose proof (necR_level _ _ H2).
(* Goal: @app_pred rmap ag_rmap (bupd (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w : rmap => forall (ora : @OK_ty Espec) (jm : juicy_mem) (_ : @app_pred rmap ag_rmap (@ext_compat (@OK_ty Espec) ora) w) (_ : @eq environ (construct_rho (filter_genv psi) ve te) (construct_rho (filter_genv psi) ve te)) (_ : @eq rmap (m_phi jm) w), @jsafeN (@OK_ty Espec) (@OK_spec Espec) psi (@level rmap ag_rmap w) ora (State ve te (@cons cont' (Kseq c) k)) jm) (semax.assert_safe_obligation_1 Espec psi ve te (@cons cont' (Kseq c) k) (construct_rho (filter_genv psi) ve te)))) m' *)
(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
  lapply (H0 m'); [|omega].
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
  intro X; apply X; auto.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
  split; [split|]; auto.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
  apply funassert_resource with (a := a'); auto. }
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
eapply bupd_trans; eauto.
Qed.

Lemma semax'_post:
(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
 forall {CS: compspecs} {Espec: OracleKind} (R': ret_assert) Delta (R: ret_assert) P c,
   (forall ek vl rho,  !!(typecheck_environ Delta rho) && 
                proj_ret_assert R' ek vl rho 
         |-- proj_ret_assert R ek vl rho) ->
   semax' Espec Delta P c R' |-- semax' Espec Delta P c R.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
intros.
(* Goal: forall (n : nat) (_ : @app_pred nat ag_nat (@semax' CS Espec Delta P c R') n), @app_pred nat ag_nat (@semax' CS Espec Delta P c R) n *)
apply semax'_post_bupd.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
intros; eapply derives_trans, bupd_intro; auto.
Qed.

Lemma semax'_pre_bupd:
(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
 forall {CS: compspecs} {Espec: OracleKind} P' Delta R P c,
  (forall rho, typecheck_environ Delta rho ->   P rho |-- bupd (P' rho))
   ->   semax' Espec Delta P' c R |-- semax' Espec Delta P c R.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
intros.
(* Goal: @derives nat ag_nat (@semax' CS Espec Delta P c R') (@semax' CS Espec Delta P c R) *)
repeat rewrite semax_fold_unfold.
(* Goal: @derives 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 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))))))))) (@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))))))))) *)
apply allp_derives; intro psi.
(* Goal: @derives nat ag_nat (@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 psi) (@cenv_cs CS)))) (@imp nat ag_nat (@believe CS Espec Delta' psi 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 psi Delta' (frame_ret_assert R F) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P' rho)) (@cons cont' (Kseq c) k)))))))) (@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 psi) (@cenv_cs CS)))) (@imp nat ag_nat (@believe CS Espec Delta' psi 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 psi Delta' (frame_ret_assert R F) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) (@cons cont' (Kseq c) k)))))))) *)
apply allp_derives; intro Delta'.
(* Goal: @derives nat ag_nat (@imp nat ag_nat (@prop nat ag_nat (and (tycontext_sub Delta Delta') (@eq composite_env (genv_cenv psi) (@cenv_cs CS)))) (@imp nat ag_nat (@believe CS Espec Delta' psi 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 psi Delta' (frame_ret_assert R F) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P' rho)) (@cons cont' (Kseq c) k))))))) (@imp nat ag_nat (@prop nat ag_nat (and (tycontext_sub Delta Delta') (@eq composite_env (genv_cenv psi) (@cenv_cs CS)))) (@imp nat ag_nat (@believe CS Espec Delta' psi 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 psi Delta' (frame_ret_assert R F) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) (@cons cont' (Kseq c) k))))))) *)
apply prop_imp_derives; intros [TS HGG].
(* Goal: @derives nat ag_nat (@imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars c F)) (rguard Espec psi Delta' (frame_ret_assert R F) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P' rho)) (@cons cont' (Kseq c) k))) (@imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars c F)) (rguard Espec psi Delta' (frame_ret_assert R F) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) (@cons cont' (Kseq c) k))) *)
apply imp_derives; auto.
(* Goal: @derives nat ag_nat (@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 psi Delta' (frame_ret_assert R F) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P' rho)) (@cons cont' (Kseq c) k))))) (@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 psi Delta' (frame_ret_assert R F) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) (@cons cont' (Kseq c) k))))) *)
apply allp_derives; intro k.
(* Goal: @derives nat ag_nat (@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 psi Delta' (frame_ret_assert R F) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P' rho)) (@cons cont' (Kseq c) k)))) (@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 psi Delta' (frame_ret_assert R F) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) (@cons cont' (Kseq c) k)))) *)
apply allp_derives; intro F.
(* Goal: @derives nat ag_nat (@imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars c F)) (rguard Espec psi Delta' (frame_ret_assert R F) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P' rho)) (@cons cont' (Kseq c) k))) (@imp nat ag_nat (@andp nat ag_nat (@prop nat ag_nat (closed_wrt_modvars c F)) (rguard Espec psi Delta' (frame_ret_assert R F) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) (@cons cont' (Kseq c) k))) *)
apply imp_derives; auto.
(* Goal: @derives nat ag_nat (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P' rho)) (@cons cont' (Kseq c) k)) (guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) (@cons cont' (Kseq c) k)) *)
unfold guard.
(* Goal: @derives nat ag_nat (_guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P' rho)) (current_function (@cons cont' (Kseq c) k)) (@cons cont' (Kseq c) k)) (_guard Espec psi Delta' (fun rho : environ => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho)) (current_function (@cons cont' (Kseq c) k)) (@cons cont' (Kseq c) k)) *)
apply allp_derives; intro te.
(* Goal: @derives nat ag_nat (@allp nat ag_nat env (fun vx : env => let rho := construct_rho (filter_genv psi) vx te in @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function (@cons cont' (Kseq c) k)) rho)) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P' rho))) (funassert Delta' rho)) (assert_safe Espec psi vx te (@cons cont' (Kseq c) k) rho)))) (@allp nat ag_nat env (fun vx : env => let rho := construct_rho (filter_genv psi) vx te in @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function (@cons cont' (Kseq c) k)) rho)) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho))) (funassert Delta' rho)) (assert_safe Espec psi vx te (@cons cont' (Kseq c) k) rho)))) *)
apply allp_derives; intro ve.
(* Goal: @derives nat ag_nat (let rho := construct_rho (filter_genv psi) ve te in @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function (@cons cont' (Kseq c) k)) rho)) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P' rho))) (funassert Delta' rho)) (assert_safe Espec psi ve te (@cons cont' (Kseq c) k) rho))) (let rho := construct_rho (filter_genv psi) ve te in @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function (@cons cont' (Kseq c) k)) rho)) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho))) (funassert Delta' rho)) (assert_safe Espec psi ve te (@cons cont' (Kseq c) k) rho))) *)
intros ? ?.
(* Goal: @app_pred nat ag_nat (let rho := construct_rho (filter_genv psi) ve te in @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function (@cons cont' (Kseq c) k)) rho)) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (F rho) (P rho))) (funassert Delta' rho)) (assert_safe Espec psi ve te (@cons cont' (Kseq c) k) rho))) a *)
intros ? ? ? ? ?.
(* Goal: @app_pred rmap ag_rmap (assert_safe Espec psi ve te (@cons cont' (Kseq c) k) (construct_rho (filter_genv psi) ve te)) a' *)
destruct H3 as [[? HFP] ?].
(* Goal: @app_pred rmap ag_rmap (assert_safe Espec psi ve te (@cons cont' (Kseq c) k) (construct_rho (filter_genv psi) ve te)) a' *)
eapply sepcon_derives in HFP; [| apply derives_refl | apply H].
(* Goal: @app_pred rmap ag_rmap (assert_safe Espec psi ve te (@cons cont' (Kseq c) k) (construct_rho (filter_genv psi) ve te)) a' *)
(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
apply bupd_frame_l in HFP.
(* Goal: @app_pred rmap ag_rmap (bupd (assert_safe Espec psi ve te (exit_cont ek vl k) (construct_rho (filter_genv psi) ve te))) a' *)
apply bupd_trans; intros ? J.
(* Goal: @ex ghost (fun b : ghost => and (@joins ghost ghost_join b (ghost_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) c0)) (@ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a')) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a')) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap (bupd (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w : rmap => forall (ora : @OK_ty Espec) (jm : juicy_mem) (_ : @app_pred rmap ag_rmap (@ext_compat (@OK_ty Espec) ora) w) (_ : @eq environ (construct_rho (filter_genv psi) ve te) (construct_rho (filter_genv psi) ve te)) (_ : @eq rmap (m_phi jm) w), @jsafeN (@OK_ty Espec) (@OK_spec Espec) psi (@level rmap ag_rmap w) ora (State ve te (@cons cont' (Kseq c) k)) jm) (semax.assert_safe_obligation_1 Espec psi ve te (@cons cont' (Kseq c) k) (construct_rho (filter_genv psi) ve te)))) m')))))) *)
(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
destruct (HFP _ J) as (b & ? & m' & ? & ? & ? & HFP').
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta rho)) (P rho)) a *)
exists b; split; auto; exists m'; repeat split; auto.
(* Goal: @app_pred rmap ag_rmap (bupd (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w : rmap => forall (ora : @OK_ty Espec) (jm : juicy_mem) (_ : @app_pred rmap ag_rmap (@ext_compat (@OK_ty Espec) ora) w) (_ : @eq environ (construct_rho (filter_genv psi) ve te) (construct_rho (filter_genv psi) ve te)) (_ : @eq rmap (m_phi jm) w), @jsafeN (@OK_ty Espec) (@OK_spec Espec) psi (@level rmap ag_rmap w) ora (State ve te (@cons cont' (Kseq c) k)) jm) (semax.assert_safe_obligation_1 Espec psi ve te (@cons cont' (Kseq c) k) (construct_rho (filter_genv psi) ve te)))) m' *)
(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
pose proof (necR_level _ _ H2).
(* Goal: @app_pred rmap ag_rmap (bupd (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w : rmap => forall (ora : @OK_ty Espec) (jm : juicy_mem) (_ : @app_pred rmap ag_rmap (@ext_compat (@OK_ty Espec) ora) w) (_ : @eq environ (construct_rho (filter_genv psi) ve te) (construct_rho (filter_genv psi) ve te)) (_ : @eq rmap (m_phi jm) w), @jsafeN (@OK_ty Espec) (@OK_spec Espec) psi (@level rmap ag_rmap w) ora (State ve te (@cons cont' (Kseq c) k)) jm) (semax.assert_safe_obligation_1 Espec psi ve te (@cons cont' (Kseq c) k) (construct_rho (filter_genv psi) ve te)))) m' *)
(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
lapply (H0 m'); [|omega].
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
intro X; apply X; auto.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
split; [split|]; auto.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
apply funassert_resource with (a := a'); auto.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
{ destruct H3; eapply typecheck_environ_sub; eauto. }
Qed.

Lemma semax'_pre:
(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
 forall {CS: compspecs} {Espec: OracleKind} P' Delta R P c,
  (forall rho, typecheck_environ Delta rho ->   P rho |-- P' rho)
   ->   semax' Espec Delta P' c R |-- semax' Espec Delta P c R.
Proof.
(* Goal: forall (CS : compspecs) (Espec : OracleKind) (P' : forall _ : environ, @pred rmap ag_rmap) (Delta : tycontext) (R : ret_assert) (P : forall _ : environ, @pred rmap ag_rmap) (c : statement) (_ : forall (rho : environ) (_ : typecheck_environ Delta rho), @derives rmap ag_rmap (P rho) (P' rho)), @derives nat ag_nat (@semax' CS Espec Delta P' c R) (@semax' CS Espec Delta P c R) *)
intros; apply semax'_pre_bupd.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
intros; eapply derives_trans, bupd_intro; auto.
Qed.

Lemma semax'_pre_post_bupd:
 forall
(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
      {CS: compspecs} {Espec: OracleKind} P' (R': ret_assert) Delta (R: ret_assert) P c,
   (forall rho, typecheck_environ Delta rho ->   P rho |-- bupd (P' rho)) ->
   (forall ek vl rho, !!(typecheck_environ Delta rho) 
                       &&  proj_ret_assert R ek vl rho 
                    |-- bupd (proj_ret_assert R' ek vl rho)) ->
   semax' Espec Delta P' c R |-- semax' Espec Delta P c R'.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
intros.
eapply derives_trans.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
apply semax'_pre_bupd; eauto.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
apply semax'_post_bupd; auto.
Qed.

Lemma semax'_pre_post:
 forall
(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
      {CS: compspecs} {Espec: OracleKind} P' (R': ret_assert) Delta (R: ret_assert) P c,
   (forall rho, typecheck_environ Delta rho ->   P rho |-- P' rho) ->
   (forall ek vl rho, !!(typecheck_environ Delta rho) 
                       &&  proj_ret_assert R ek vl rho 
                    |-- proj_ret_assert R' ek vl rho) ->
   semax' Espec Delta P' c R |-- semax' Espec Delta P c R'.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
intros.
eapply derives_trans.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
apply semax'_pre; eauto.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
apply semax'_post; auto.
Qed.

(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
Lemma semax_post'_bupd {CS: compspecs} {Espec: OracleKind}:
 forall (R': ret_assert) Delta (R: ret_assert) P c,
   (forall ek vl rho,  !!(typecheck_environ Delta rho) 
                      &&  proj_ret_assert R' ek vl rho
                        |-- bupd (proj_ret_assert R ek vl rho)) ->
   semax Espec Delta P c R' ->  semax Espec Delta P c R.
Proof.
(* Goal: forall (P' : forall _ : environ, @pred rmap ag_rmap) (Delta : tycontext) (P : forall _ : environ, @pred rmap ag_rmap) (c : statement) (R : ret_assert) (_ : forall rho : environ, @derives rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta rho)) (P rho)) (P' rho)) (_ : @semax CS Espec Delta P' c R), @semax CS Espec Delta P c R *)
unfold semax.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
intros.
(* Goal: @app_pred nat ag_nat (@semax' CS Espec Delta P c R) n *)
specialize (H0 n). revert n H0.
(* Goal: forall (n : nat) (_ : @app_pred nat ag_nat (@semax' CS Espec Delta P c R') n), @app_pred nat ag_nat (@semax' CS Espec Delta P c R) n *)
apply semax'_post_bupd.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
auto.
Qed.

(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
Lemma semax_post_bupd {CS: compspecs} {Espec: OracleKind}:
 forall (R': ret_assert) Delta (R: ret_assert) P c,
   (forall rho,  !!(typecheck_environ Delta rho) 
                      &&  RA_normal R' rho |-- bupd (RA_normal R rho)) ->
   (forall rho, !! (typecheck_environ Delta rho) 
                      && RA_break R' rho |-- bupd (RA_break R rho)) ->
   (forall rho, !! (typecheck_environ Delta rho) 
                      && RA_continue R' rho |-- bupd (RA_continue R rho)) ->
   (forall vl rho, !! (typecheck_environ Delta rho) 
                      && RA_return R' vl rho |-- bupd (RA_return R vl rho)) ->
   semax Espec Delta P c R' ->  semax Espec Delta P c R.
Proof.
(* Goal: forall (P' : forall _ : environ, @pred rmap ag_rmap) (Delta : tycontext) (P : forall _ : environ, @pred rmap ag_rmap) (c : statement) (R : ret_assert) (_ : forall rho : environ, @derives rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta rho)) (P rho)) (P' rho)) (_ : @semax CS Espec Delta P' c R), @semax CS Espec Delta P c R *)
unfold semax.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
intros.
(* Goal: @app_pred nat ag_nat (@semax' CS Espec Delta P c R) n *)
specialize (H3 n). revert n H3.
(* Goal: forall (n : nat) (_ : @app_pred nat ag_nat (@semax' CS Espec Delta P c R') n), @app_pred nat ag_nat (@semax' CS Espec Delta P c R) n *)
apply semax'_post_bupd.
intros; destruct ek; simpl;
repeat (apply normalize.derives_extract_prop; intro); rewrite ?prop_true_andp by auto;
specialize (H rho); specialize (H0 rho); specialize (H1 rho); specialize (H2 vl rho);
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
rewrite prop_true_andp in * by auto; auto.
Qed.

(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
Lemma semax_post' {CS: compspecs} {Espec: OracleKind}:
 forall (R': ret_assert) Delta (R: ret_assert) P c,
   (forall ek vl rho,  !!(typecheck_environ Delta rho) 
                      &&  proj_ret_assert R' ek vl rho
                        |-- proj_ret_assert R ek vl rho) ->
   semax Espec Delta P c R' ->  semax Espec Delta P c R.
Proof.
(* Goal: forall (P' : forall _ : environ, @pred rmap ag_rmap) (Delta : tycontext) (P : forall _ : environ, @pred rmap ag_rmap) (c : statement) (R : ret_assert) (_ : forall rho : environ, @derives rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta rho)) (P rho)) (P' rho)) (_ : @semax CS Espec Delta P' c R), @semax CS Espec Delta P c R *)
unfold semax.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
intros.
(* Goal: @app_pred nat ag_nat (@semax' CS Espec Delta P c R) n *)
specialize (H0 n). revert n H0.
(* Goal: forall (n : nat) (_ : @app_pred nat ag_nat (@semax' CS Espec Delta P c R') n), @app_pred nat ag_nat (@semax' CS Espec Delta P c R) n *)
apply semax'_post.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
auto.
Qed.

(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
Lemma semax_post {CS: compspecs} {Espec: OracleKind}:
 forall (R': ret_assert) Delta (R: ret_assert) P c,
   (forall rho,  !!(typecheck_environ Delta rho) 
                      &&  RA_normal R' rho |-- RA_normal R rho) ->
   (forall rho, !! (typecheck_environ Delta rho) 
                      && RA_break R' rho |-- RA_break R rho) ->
   (forall rho, !! (typecheck_environ Delta rho) 
                      && RA_continue R' rho |-- RA_continue R rho) ->
   (forall vl rho, !! (typecheck_environ Delta rho) 
                      && RA_return R' vl rho |-- RA_return R vl rho) ->
   semax Espec Delta P c R' ->  semax Espec Delta P c R.
Proof.
(* Goal: forall (P' : forall _ : environ, @pred rmap ag_rmap) (Delta : tycontext) (P : forall _ : environ, @pred rmap ag_rmap) (c : statement) (R : ret_assert) (_ : forall rho : environ, @derives rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta rho)) (P rho)) (P' rho)) (_ : @semax CS Espec Delta P' c R), @semax CS Espec Delta P c R *)
unfold semax.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
intros.
(* Goal: @app_pred nat ag_nat (@semax' CS Espec Delta P c R) n *)
specialize (H3 n). revert n H3.
(* Goal: forall (n : nat) (_ : @app_pred nat ag_nat (@semax' CS Espec Delta P c R') n), @app_pred nat ag_nat (@semax' CS Espec Delta P c R) n *)
apply semax'_post.
intros; destruct ek; simpl;
repeat (apply normalize.derives_extract_prop; intro); rewrite ?prop_true_andp by auto;
specialize (H rho); specialize (H0 rho); specialize (H1 rho); specialize (H2 vl rho);
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
rewrite prop_true_andp in * by auto; auto.
Qed.

(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
Lemma semax_pre_bupd {CS: compspecs} {Espec: OracleKind} :
 forall P' Delta P c R,
   (forall rho,  !!(typecheck_environ Delta rho) &&  P rho |-- bupd (P' rho) )%pred ->
     semax Espec Delta P' c R  -> semax Espec Delta P c R.
Proof.
(* Goal: forall (P' : forall _ : environ, @pred rmap ag_rmap) (Delta : tycontext) (P : forall _ : environ, @pred rmap ag_rmap) (c : statement) (R : ret_assert) (_ : forall rho : environ, @derives rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta rho)) (P rho)) (P' rho)) (_ : @semax CS Espec Delta P' c R), @semax CS Espec Delta P c R *)
unfold semax.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
intros.
(* Goal: @app_pred nat ag_nat (@semax' CS Espec Delta P c R) n *)
specialize (H0 n).
(* Goal: @app_pred nat ag_nat (@semax' CS Espec Delta P c R) n *)
revert n H0.
(* Goal: forall (n : nat) (_ : @app_pred nat ag_nat (@semax' CS Espec Delta P' c R) n), @app_pred nat ag_nat (@semax' CS Espec Delta P c R) n *)
apply semax'_pre_bupd.
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta rho)) (P rho)) a *)
repeat intro. apply (H rho a); auto. split; auto.
Qed.

(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
Lemma semax_pre {CS: compspecs} {Espec: OracleKind} :
 forall P' Delta P c R,
   (forall rho,  !!(typecheck_environ Delta rho) &&  P rho |-- P' rho )%pred ->
     semax Espec Delta P' c R  -> semax Espec Delta P c R.
Proof.
(* Goal: forall (P' : forall _ : environ, @pred rmap ag_rmap) (Delta : tycontext) (P : forall _ : environ, @pred rmap ag_rmap) (c : statement) (R : ret_assert) (_ : forall rho : environ, @derives rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta rho)) (P rho)) (P' rho)) (_ : @semax CS Espec Delta P' c R), @semax CS Espec Delta P c R *)
unfold semax.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
intros.
(* Goal: @app_pred nat ag_nat (@semax' CS Espec Delta P c R) n *)
specialize (H0 n).
(* Goal: @app_pred nat ag_nat (@semax' CS Espec Delta P c R) n *)
revert n H0.
(* Goal: forall (n : nat) (_ : @app_pred nat ag_nat (@semax' CS Espec Delta P' c R) n), @app_pred nat ag_nat (@semax' CS Espec Delta P c R) n *)
apply semax'_pre.
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (typecheck_environ Delta rho)) (P rho)) a *)
repeat intro. apply (H rho a). split; auto.
Qed.

(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
Lemma semax_pre_post_bupd {CS: compspecs} {Espec: OracleKind}:
 forall P' (R': ret_assert) Delta P c (R: ret_assert) ,
   (forall rho,  !!(typecheck_environ Delta rho) &&  P rho |-- bupd (P' rho) )%pred ->
   (forall rho,  !!(typecheck_environ Delta rho) 
                      &&  RA_normal R' rho |-- bupd (RA_normal R rho)) ->
   (forall rho, !! (typecheck_environ Delta rho) 
                      && RA_break R' rho |-- bupd (RA_break R rho)) ->
   (forall rho, !! (typecheck_environ Delta rho) 
                      && RA_continue R' rho |-- bupd (RA_continue R rho)) ->
   (forall vl rho, !! (typecheck_environ Delta rho) 
                      && RA_return R' vl rho |-- bupd (RA_return R vl rho)) ->
   semax Espec Delta P' c R' ->  semax Espec Delta P c R.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
intros.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
eapply semax_pre_bupd; eauto.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
eapply semax_post_bupd; eauto.
Qed.

(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
Lemma semax_pre_post {CS: compspecs} {Espec: OracleKind}:
 forall P' (R': ret_assert) Delta P c (R: ret_assert) ,
   (forall rho,  !!(typecheck_environ Delta rho) &&  P rho |-- P' rho )%pred ->
   (forall rho,  !!(typecheck_environ Delta rho) 
                      &&  RA_normal R' rho |-- RA_normal R rho) ->
   (forall rho, !! (typecheck_environ Delta rho) 
                      && RA_break R' rho |-- RA_break R rho) ->
   (forall rho, !! (typecheck_environ Delta rho) 
                      && RA_continue R' rho |-- RA_continue R rho) ->
   (forall vl rho, !! (typecheck_environ Delta rho) 
                      && RA_return R' vl rho |-- RA_return R vl rho) ->
   semax Espec Delta P' c R' ->  semax Espec Delta P c R.
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
intros.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
eapply semax_pre; eauto.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
eapply semax_post; eauto.
Qed.

(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
Lemma semax_bupd_elim {CS: compspecs} {Espec: OracleKind}:
 forall Delta P c R,
  semax Espec Delta P c R -> semax Espec Delta (fun rho => bupd (P rho)) c R.
Proof.
(* Goal: forall (Delta : tycontext) (P : assert) (c : statement) (R : ret_assert) (_ : @semax CS Espec Delta P c R), @semax CS Espec Delta (fun rho : environ => bupd (P rho)) c R *)
intros ????; apply semax_pre_bupd.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
intro; apply prop_andp_left; auto.
Qed.

(* Goal: typecheck_environ Delta (construct_rho (filter_genv psi) ve te) *)
Lemma semax_skip {CS: compspecs} {Espec: OracleKind}:
   forall Delta P, semax Espec Delta P Sskip (normal_ret_assert P).
Proof.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
intros.
(* Goal: @semax CS Espec Delta P Sskip (normal_ret_assert P) *)
apply derives_skip.
(* Goal: forall rho : environ, @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
intros.
(* Goal: @derives rmap ag_rmap (P rho) (proj_ret_assert (normal_ret_assert P) EK_normal (@None val) rho) *)
simpl.
(* Goal: @derives rmap ag_rmap (P rho) (P rho) *)
auto.
Qed.

