Require Import VST.msl.msl_standard.
Require Import VST.msl.seplog.
Require Import VST.veric.Clight_base.
Require Import VST.veric.compcert_rmaps.
Require Import VST.veric.juicy_mem.
Require Import VST.veric.juicy_mem_lemmas.
Require Import VST.veric.juicy_mem_ops.
Require Import VST.veric.juicy_extspec.
Require Import VST.veric.tycontext.
Require Import VST.veric.expr2.
Require Import VST.veric.semax.
Require Import VST.veric.semax_call.
Require Import VST.veric.semax_ext.
Require Import VST.veric.juicy_safety.
Require Import VST.veric.Clight_new.
Require Import VST.veric.res_predicates.
Require Import VST.veric.SeparationLogic.
Require Import VST.sepcomp.semantics.
Require Import VST.sepcomp.extspec.
Require Import VST.floyd.reptype_lemmas.
Require Import VST.floyd.field_at.
Require Import VST.floyd.nested_field_lemmas.
Require Import VST.floyd.client_lemmas.
Require Import VST.floyd.jmeq_lemmas.
Require Import VST.concurrency.lksize.
Require Import VST.concurrency.semax_conc_pred.
Import String.

Set Bullet Behavior "Strict Subproofs".

(* Variables to be instantiated once the program is known. *)
Definition _f := 1%positive.      (* alpha-convertible *)
Definition _args := 2%positive.   (* alpha-convertible *)
Definition _lock := 1%positive.   (* alpha-convertible *)
Definition _cond := 2%positive.   (* alpha-convertible *)
(*Definition _lock_t := 2%positive. (* 2 (* or sometimes 3 -WM *) is the number given by
clightgen when threads.h is included first *)*)

Definition voidstar_funtype := Tfunction (Tcons (tptr tvoid) Tnil) (tptr tvoid) cc_default.
(* Definition tlock := Tstruct _lock_t noattr. *)
Definition tlock := (Tarray (Tpointer Tvoid noattr) 2 noattr).
(* Notation tlock := tuint (only parsing). *)

Goal forall (cenv: composite_env), @sizeof cenv tlock = LKSIZE.
(* Goal: @eq mpred (res_invariants_fun Q sh1 p1 sh2 p2 (res_invariants Q sh1 p1 sh2 p2) false) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric Q (lock_inv sh1 p1 (@later mpred Nveric Iveric (res_invariant Q sh1 p1 sh2 p2)))) (lock_inv sh2 p2 (@later mpred Nveric Iveric (join_res_invariant Q sh1 p1 sh2 p2)))) *)
Proof. reflexivity. Qed.

Definition selflock_fun Q sh p : (unit -> mpred) -> (unit -> mpred) :=
  fun R _ => (Q * |>lock_inv sh p (R tt))%logic.

Definition selflock' Q sh p : unit -> mpred := HORec (selflock_fun Q sh p).
Definition selflock Q sh p : mpred := selflock' Q sh p tt.

Lemma nonexpansive_entail (F: pred rmap -> pred rmap) : nonexpansive F -> forall P Q, (P <=> Q |-- F P <=> F Q)%logic.
Proof.
(* Goal: forall (_ : @nonexpansive rmap ag_rmap F) (P Q : @pred rmap ag_rmap), @derives Triv TrivNatDed (@fash (@pred rmap ag_rmap) Nveric Iveric Rveric (@andp (@pred rmap ag_rmap) Nveric (@imp (@pred rmap ag_rmap) Nveric P Q) (@imp (@pred rmap ag_rmap) Nveric Q P))) (@fash (@pred rmap ag_rmap) Nveric Iveric Rveric (@andp (@pred rmap ag_rmap) Nveric (@imp (@pred rmap ag_rmap) Nveric (F P) (F Q)) (@imp (@pred rmap ag_rmap) Nveric (F Q) (F P)))) *)
  intros N P Q.
(* Goal: @derives Triv TrivNatDed (@fash (@pred rmap ag_rmap) Nveric Iveric Rveric (@andp (@pred rmap ag_rmap) Nveric (@imp (@pred rmap ag_rmap) Nveric P Q) (@imp (@pred rmap ag_rmap) Nveric Q P))) (@fash (@pred rmap ag_rmap) Nveric Iveric Rveric (@andp (@pred rmap ag_rmap) Nveric (@imp (@pred rmap ag_rmap) Nveric (F P) (F Q)) (@imp (@pred rmap ag_rmap) Nveric (F Q) (F P)))) *)
  specialize (N P Q).
  eapply derives_trans; [ eapply derives_trans | ]; [ | apply N | ];
  apply derives_refl.
Qed.

Lemma HOnonexpansive_nonexpansive: forall F: mpred -> mpred, nonexpansive F <-> HOnonexpansive (fun P (_ : unit) => F (P tt)).
Proof.
(* Goal: forall (n : nat) (P : @pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap), @eq (@pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap) (compcert_rmaps.R.approx n (compcert_rmaps.R.approx n P)) (compcert_rmaps.R.approx n P) *)
  intros.
(* Goal: iff (@nonexpansive rmap ag_rmap F) (@HOnonexpansive mpred Nveric Iveric Rveric unit (fun (P : forall _ : unit, mpred) (_ : unit) => F (P tt))) *)
  split; intros; hnf in H |- *.
  + intros P Q.
(* Goal: @derives Triv TrivNatDed (@allp Triv TrivNatDed unit (fun x : unit => @fash mpred Nveric Iveric Rveric (@andp mpred Nveric (@imp mpred Nveric (P x) (Q x)) (@imp mpred Nveric (Q x) (P x))))) (@allp Triv TrivNatDed unit (fun _ : unit => @fash mpred Nveric Iveric Rveric (@andp mpred Nveric (@imp mpred Nveric (F (P tt)) (F (Q tt))) (@imp mpred Nveric (F (Q tt)) (F (P tt)))))) *)
    specialize (H (P tt) (Q tt)).
(* Goal: @derives Triv TrivNatDed (@allp Triv TrivNatDed unit (fun x : unit => @fash mpred Nveric Iveric Rveric (@andp mpred Nveric (@imp mpred Nveric (P x) (Q x)) (@imp mpred Nveric (Q x) (P x))))) (@allp Triv TrivNatDed unit (fun _ : unit => @fash mpred Nveric Iveric Rveric (@andp mpred Nveric (@imp mpred Nveric (F (P tt)) (F (Q tt))) (@imp mpred Nveric (F (Q tt)) (F (P tt)))))) *)
    rewrite !allp_unit.
(* Goal: @eq (@pred rmap ag_rmap) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) *)
    auto.
  + intros P Q.
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P Q) (@predicates_hered.imp rmap ag_rmap Q P))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (F P) (F Q)) (@predicates_hered.imp rmap ag_rmap (F Q) (F P)))) *)
    specialize (H (fun x => P) (fun x => Q)).
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P Q) (@predicates_hered.imp rmap ag_rmap Q P))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (F P) (F Q)) (@predicates_hered.imp rmap ag_rmap (F Q) (F P)))) *)
    rewrite !allp_unit in H.
(* Goal: @eq (@pred rmap ag_rmap) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) *)
    auto.
Qed.

Lemma selflock'_eq Q sh p : selflock' Q sh p =
  selflock_fun Q sh p (selflock' Q sh p).
Proof.
(* Goal: @eq (forall _ : unit, mpred) (selflock' Q sh p) (selflock_fun Q sh p (selflock' Q sh p)) *)
  apply HORec_fold_unfold, prove_HOcontractive.
(* Goal: forall (P Q0 : forall _ : unit, mpred) (x : unit), @derives Triv TrivNatDed (@allp Triv TrivNatDed unit (fun x0 : unit => @fash mpred Nveric Iveric Rveric (@andp mpred Nveric (@imp mpred Nveric (@later mpred Nveric Iveric (P x0)) (@later mpred Nveric Iveric (Q0 x0))) (@imp mpred Nveric (@later mpred Nveric Iveric (Q0 x0)) (@later mpred Nveric Iveric (P x0)))))) (@fash mpred Nveric Iveric Rveric (@imp mpred Nveric (selflock_fun Q sh p P x) (selflock_fun Q sh p Q0 x))) *)
  intros P1 P2 u.
(* Goal: @derives Triv TrivNatDed (@allp Triv TrivNatDed unit (fun x : unit => @fash mpred Nveric Iveric Rveric (@andp mpred Nveric (@imp mpred Nveric (@later mpred Nveric Iveric (P1 x)) (@later mpred Nveric Iveric (P2 x))) (@imp mpred Nveric (@later mpred Nveric Iveric (P2 x)) (@later mpred Nveric Iveric (P1 x)))))) (@fash mpred Nveric Iveric Rveric (@imp mpred Nveric (selflock_fun Q sh p P1 u) (selflock_fun Q sh p P2 u))) *)
  apply subp_sepcon; [ apply subp_refl | ].
(* Goal: @derives Triv TrivNatDed (@allp Triv TrivNatDed unit (fun x : unit => @fash mpred Nveric Iveric Rveric (@andp mpred Nveric (@imp mpred Nveric (@later mpred Nveric Iveric (P1 x)) (@later mpred Nveric Iveric (P2 x))) (@imp mpred Nveric (@later mpred Nveric Iveric (P2 x)) (@later mpred Nveric Iveric (P1 x)))))) (@fash mpred Nveric Iveric Rveric (@imp mpred Nveric (@later mpred Nveric Iveric (lock_inv sh p (P1 tt))) (@later mpred Nveric Iveric (lock_inv sh p (P2 tt))))) *)
  rewrite <- subp_later.
(* Goal: @super_non_expansive spawn_arg_type spawn_pre *)
  repeat intro.
(* Goal: @app_pred nat ag_nat (@fash mpred Nveric Iveric Rveric (@imp mpred Nveric (lock_inv sh p (P1 tt)) (lock_inv sh p (P2 tt)))) a' *)
  match goal with |- app_pred (?P >=> ?Q)%logic ?a => change (subtypes.fash (P --> Q) a) end.
(* Goal: @super_non_expansive spawn_arg_type spawn_pre *)
  unfold lock_inv; repeat intro.
(* Goal: @eq (@pred rmap ag_rmap) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) *)
  destruct H3 as (b & ofs & ? & Hl & ?); exists b, ofs; split; auto; split; auto.
(* Goal: @app_pred rmap ag_rmap (@predicates_hered.allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range (@pair block Z b (Ptrofs.unsigned ofs)) LKSIZE) (adr_range_dec (@pair block Z b (Ptrofs.unsigned ofs)) LKSIZE) (fun l' : address => yesat (SomeP rmaps.Mpred (fun _ : list Type => P2 tt)) (LK LKSIZE (Z.sub (@snd block Z l') (@snd block Z (@pair block Z b (Ptrofs.unsigned ofs))))) sh l') noat)) a'0 *)
  intro l; specialize (Hl l); simpl in *.
(* Goal: @eq (@pred rmap ag_rmap) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) *)
  if_tac; auto.
(* Goal: @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at a'0 l) (YES sh rsh (LK LKSIZE (Z.sub (@snd block Z l) (Ptrofs.unsigned ofs))) (SomeP rmaps.Mpred (fun _ : list Type => approx (@level rmap ag_rmap a'0) (P2 tt))))) *)
  destruct Hl as [rsh Hl]; exists rsh; rewrite Hl; repeat f_equal.
(* Goal: @eq (forall _ : list Type, @pred rmap ag_rmap) (fun _ : list Type => approx (@level rmap ag_rmap a'0) (P1 tt)) (fun _ : list Type => approx (@level rmap ag_rmap a'0) (P2 tt)) *)
  extensionality.
(* Goal: @eq (@pred rmap ag_rmap) (approx (@level rmap ag_rmap a'0) (P1 tt)) (approx (@level rmap ag_rmap a'0) (P2 tt)) *)
  specialize (H tt); rewrite <- eqp_later in H.
(* Goal: @eq (@pred rmap ag_rmap) (approx (@level rmap ag_rmap a'0) (P1 tt)) (approx (@level rmap ag_rmap a'0) (P2 tt)) *)
  specialize (H _ H0).
(* Goal: @eq (@pred rmap ag_rmap) (approx (@level rmap ag_rmap a'0) (P1 tt)) (approx (@level rmap ag_rmap a'0) (P2 tt)) *)
  apply necR_level in H2.
(* Goal: @eq (@pred rmap ag_rmap) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) *)
  apply predicates_hered.pred_ext; intros ? []; split; auto.
  - destruct (H a0) as [X _]; [omega|].
(* Goal: @eq (@pred rmap ag_rmap) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) *)
    specialize (X _ (necR_refl _)); auto.
  - destruct (H a0) as [_ X]; [omega|].
(* Goal: @eq (@pred rmap ag_rmap) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) *)
    specialize (X _ (necR_refl _)); auto.
Qed.

Lemma selflock_eq Q sh p : selflock Q sh p = (Q * |>lock_inv sh p (selflock Q sh p))%logic.
Proof.
(* Goal: @eq mpred (selflock Q sh p) (@sepcon mpred Nveric Sveric Q (@later mpred Nveric Iveric (lock_inv sh p (selflock Q sh p)))) *)
  unfold selflock at 1.
(* Goal: @eq mpred (selflock' Q sh p tt) (@sepcon mpred Nveric Sveric Q (@later mpred Nveric Iveric (lock_inv sh p (selflock Q sh p)))) *)
  rewrite selflock'_eq.
(* Goal: @eq mpred (res_invariants_fun Q sh1 p1 sh2 p2 (res_invariants Q sh1 p1 sh2 p2) false) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric Q (lock_inv sh1 p1 (@later mpred Nveric Iveric (res_invariant Q sh1 p1 sh2 p2)))) (lock_inv sh2 p2 (@later mpred Nveric Iveric (join_res_invariant Q sh1 p1 sh2 p2)))) *)
  reflexivity.
Qed.

(* In fact we need locks to two resources:
   1) the resource invariant, for passing the resources
   2) the join resource invariant, for returning all resources, including itself
   for this we need to define them in a mutually recursive fashion: *)

Definition res_invariants_fun Q sh1 p1 sh2 p2 : (bool -> mpred) -> (bool -> mpred) :=
  fun R b =>
    if b then
      (Q * lock_inv sh2 p2 (|> R false))%logic
    else
      (Q * lock_inv sh1 p1 (|> R true) * lock_inv sh2 p2 (|> R false))%logic.

Definition res_invariants Q sh1 p1 sh2 p2 : bool -> mpred := HORec (res_invariants_fun Q sh1 p1 sh2 p2).
Definition res_invariant Q sh1 p1 sh2 p2 : mpred := res_invariants Q sh1 p1 sh2 p2 true.
Definition join_res_invariant Q sh1 p1 sh2 p2 : mpred := res_invariants Q sh1 p1 sh2 p2 false.

Lemma res_invariants_eq Q sh1 p1 sh2 p2 : res_invariants Q sh1 p1 sh2 p2 =
  res_invariants_fun Q sh1 p1 sh2 p2 (res_invariants Q sh1 p1 sh2 p2).
Proof.
(* Goal: @eq (forall _ : unit, mpred) (selflock' Q sh p) (selflock_fun Q sh p (selflock' Q sh p)) *)
  apply HORec_fold_unfold, prove_HOcontractive.
  intros P1 P2 b.
  destruct b.
    (* resource invariant *)
    apply subp_sepcon; try apply subp_refl.
    apply allp_left with false.
    eapply derives_trans.
      apply nonexpansive_entail, nonexpansive_lock_inv.
      apply fash_derives, andp_left1, derives_refl.

    (* join resource invariant *)
    repeat apply subp_sepcon; try apply subp_refl.
      apply allp_left with true.
      eapply derives_trans.
        apply nonexpansive_entail, nonexpansive_lock_inv.
        apply fash_derives, andp_left1, derives_refl.

      apply allp_left with false.
      eapply derives_trans.
        apply nonexpansive_entail, nonexpansive_lock_inv.
        apply fash_derives, andp_left1, derives_refl.
Qed.

Lemma res_invariant_eq Q sh1 p1 sh2 p2 :
  res_invariant Q sh1 p1 sh2 p2 =
  (Q *
  lock_inv sh2 p2 (|> join_res_invariant Q sh1 p1 sh2 p2))%logic.
Proof.
(* Goal: @eq mpred (res_invariant Q sh1 p1 sh2 p2) (@sepcon mpred Nveric Sveric Q (lock_inv sh2 p2 (@later mpred Nveric Iveric (join_res_invariant Q sh1 p1 sh2 p2)))) *)
  unfold res_invariant at 1.
(* Goal: @eq mpred (res_invariants Q sh1 p1 sh2 p2 false) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric Q (lock_inv sh1 p1 (@later mpred Nveric Iveric (res_invariant Q sh1 p1 sh2 p2)))) (lock_inv sh2 p2 (@later mpred Nveric Iveric (join_res_invariant Q sh1 p1 sh2 p2)))) *)
  rewrite res_invariants_eq.
(* Goal: @eq mpred (res_invariants_fun Q sh1 p1 sh2 p2 (res_invariants Q sh1 p1 sh2 p2) false) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric Q (lock_inv sh1 p1 (@later mpred Nveric Iveric (res_invariant Q sh1 p1 sh2 p2)))) (lock_inv sh2 p2 (@later mpred Nveric Iveric (join_res_invariant Q sh1 p1 sh2 p2)))) *)
  reflexivity.
Qed.

Lemma join_res_invariant_eq Q sh1 p1 sh2 p2 :
  join_res_invariant Q sh1 p1 sh2 p2 =
  (Q *
  lock_inv sh1 p1 (|> res_invariant Q sh1 p1 sh2 p2) *
  lock_inv sh2 p2 (|> join_res_invariant Q sh1 p1 sh2 p2))%logic.
Proof.
(* Goal: @eq mpred (join_res_invariant Q sh1 p1 sh2 p2) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric Q (lock_inv sh1 p1 (@later mpred Nveric Iveric (res_invariant Q sh1 p1 sh2 p2)))) (lock_inv sh2 p2 (@later mpred Nveric Iveric (join_res_invariant Q sh1 p1 sh2 p2)))) *)
  unfold join_res_invariant at 1.
(* Goal: @eq mpred (res_invariants Q sh1 p1 sh2 p2 false) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric Q (lock_inv sh1 p1 (@later mpred Nveric Iveric (res_invariant Q sh1 p1 sh2 p2)))) (lock_inv sh2 p2 (@later mpred Nveric Iveric (join_res_invariant Q sh1 p1 sh2 p2)))) *)
  rewrite res_invariants_eq.
(* Goal: @eq mpred (res_invariants_fun Q sh1 p1 sh2 p2 (res_invariants Q sh1 p1 sh2 p2) false) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric Q (lock_inv sh1 p1 (@later mpred Nveric Iveric (res_invariant Q sh1 p1 sh2 p2)))) (lock_inv sh2 p2 (@later mpred Nveric Iveric (join_res_invariant Q sh1 p1 sh2 p2)))) *)
  reflexivity.
Qed.

(* Condition variables *)
(*Definition _cond_t := 4%positive.*)
Definition tcond := tint.

(* Does this need to be anything special? *)
Definition cond_var {cs} sh v := @data_at_ cs sh tcond v.

(*+ Specification of each concurrent primitive *)

Lemma approx_eq_i':
  forall (P Q : pred rmap) n,
  (|> (P <=> Q))%pred n -> approx n P = approx n Q.
Proof.
(* Goal: forall (n : nat) (P : @pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap), @eq (@pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap) (compcert_rmaps.R.approx n (compcert_rmaps.R.approx n P)) (compcert_rmaps.R.approx n P) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (approx n P) (approx n Q) *)
apply pred_ext'; extensionality m'.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (approx n P) m') (@app_pred rmap ag_rmap (approx n Q) m') *)
unfold approx.
(* Goal: forall (n : nat) (P : @pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap), @eq (@pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap) (compcert_rmaps.R.approx n (compcert_rmaps.R.approx n P)) (compcert_rmaps.R.approx n P) *)
apply and_ext'; auto; intros.
(* Goal: @eq Prop (@app_pred rmap ag_rmap P m') (@app_pred rmap ag_rmap Q m') *)
specialize (H (level m')); spec H; [simpl; apply later_nat; auto |].
(* Goal: @eq Prop (@app_pred rmap ag_rmap P m') (@app_pred rmap ag_rmap Q m') *)
specialize (H m').
(* Goal: @eq Prop (@app_pred rmap ag_rmap P m') (@app_pred rmap ag_rmap Q m') *)
spec H; [omega |].
(* Goal: @eq Prop (@app_pred rmap ag_rmap P m') (@app_pred rmap ag_rmap Q m') *)
destruct H.
(* Goal: @eq Prop (@app_pred rmap ag_rmap P m') (@app_pred rmap ag_rmap Q m') *)
specialize (H m').
(* Goal: @eq Prop (@app_pred rmap ag_rmap P m') (@app_pred rmap ag_rmap Q m') *)
specialize (H1 m').
(* Goal: @eq (@pred rmap ag_rmap) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) *)
apply prop_ext; split; auto.
Qed.

Lemma fash_equiv_approx: forall n (R: pred rmap),
  (|> (R <=> approx n R))%pred n.
Proof.
(* Goal: forall (n : nat) (P : @pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap), @eq (@pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap) (compcert_rmaps.R.approx n (compcert_rmaps.R.approx n P)) (compcert_rmaps.R.approx n P) *)
  intros.
(* Goal: @app_pred nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (approx n R)) (@predicates_hered.imp rmap ag_rmap (approx n R) R)))) n *)
  intros m ? x ?; split; intros y ? ?.
  + apply approx_lt; auto.
(* Goal: lt (@level rmap ag_rmap y) n *)
    apply necR_level in H1.
(* Goal: lt (@level rmap ag_rmap y) n *)
    apply later_nat in H; omega.
  + eapply approx_p; eauto.
Qed.

Lemma nonexpansive_super_non_expansive: forall (F: mpred -> mpred),
  nonexpansive F ->
  forall R n,
  approx n (F R) = approx n (F (approx n R)).
Proof.
(* Goal: forall (n : nat) (P : @pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap), @eq (@pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap) (compcert_rmaps.R.approx n (compcert_rmaps.R.approx n P)) (compcert_rmaps.R.approx n P) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (approx n (F P Q)) (approx n (F (approx n P) (approx n Q))) *)
  apply approx_eq_i'.
(* Goal: @app_pred nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (F P Q) (F (approx n P) (approx n Q))) (@predicates_hered.imp rmap ag_rmap (F (approx n P) (approx n Q)) (F P Q))))) n *)
  intros m ?.
(* Goal: @app_pred nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (F R) (F (approx n R))) (@predicates_hered.imp rmap ag_rmap (F (approx n R)) (F R)))) m *)
  pose proof nonexpansive_entail _ H R (approx n R) m.
(* Goal: @app_pred nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (F R) (F (approx n R))) (@predicates_hered.imp rmap ag_rmap (F (approx n R)) (F R)))) m *)
  apply H1.
  clear - H0.
(* Goal: @eq (@pred rmap ag_rmap) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) *)
  apply (fash_equiv_approx n R m); auto.
Qed.

Lemma nonexpansive2_super_non_expansive: forall (F: mpred -> mpred -> mpred),
  (forall P, nonexpansive (fun Q => F P Q)) ->
  (forall Q, nonexpansive (fun P => F P Q)) ->
  forall P Q n,
  approx n (F P Q) = approx n (F (approx n P) (approx n Q)).
Proof.
(* Goal: forall (n : nat) (P : @pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap), @eq (@pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap) (compcert_rmaps.R.approx n (compcert_rmaps.R.approx n P)) (compcert_rmaps.R.approx n P) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (approx n (F P Q)) (approx n (F (approx n P) (approx n Q))) *)
  apply approx_eq_i'.
(* Goal: @app_pred nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (F P Q) (F (approx n P) (approx n Q))) (@predicates_hered.imp rmap ag_rmap (F (approx n P) (approx n Q)) (F P Q))))) n *)
  intros m ?.
(* Goal: @app_pred nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (F P Q) (F (approx n P) (approx n Q))) (@predicates_hered.imp rmap ag_rmap (F (approx n P) (approx n Q)) (F P Q)))) m *)
  pose proof nonexpansive_entail _ (H P) Q (approx n Q) m; cbv beta in H2.
(* Goal: @app_pred nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (F P Q) (F (approx n P) (approx n Q))) (@predicates_hered.imp rmap ag_rmap (F (approx n P) (approx n Q)) (F P Q)))) m *)
  spec H2; [apply (fash_equiv_approx n Q m); auto |].
(* Goal: @app_pred nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (F P Q) (F (approx n P) (approx n Q))) (@predicates_hered.imp rmap ag_rmap (F (approx n P) (approx n Q)) (F P Q)))) m *)
  pose proof nonexpansive_entail _ (H0 (approx n Q)) P (approx n P) m; cbv beta in H3.
(* Goal: @app_pred nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (F P Q) (F (approx n P) (approx n Q))) (@predicates_hered.imp rmap ag_rmap (F (approx n P) (approx n Q)) (F P Q)))) m *)
  spec H3; [apply (fash_equiv_approx n P m); auto |].
(* Goal: @app_pred nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (F P Q) (F (approx n P) (approx n Q))) (@predicates_hered.imp rmap ag_rmap (F (approx n P) (approx n Q)) (F P Q)))) m *)
  remember (F P Q) as X1.
(* Goal: @app_pred nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap X1 (F (approx n P) (approx n Q))) (@predicates_hered.imp rmap ag_rmap (F (approx n P) (approx n Q)) X1))) m *)
  remember (F P (approx n Q)) as X2.
(* Goal: @app_pred nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap X1 (F (approx n P) (approx n Q))) (@predicates_hered.imp rmap ag_rmap (F (approx n P) (approx n Q)) X1))) m *)
  remember (F (approx n P) (approx n Q)) as X3.
  clear - H2 H3.
(* Goal: @app_pred nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap X1 X3) (@predicates_hered.imp rmap ag_rmap X3 X1))) m *)
  change ((X1 <=> X2)%pred m) in H2.
(* Goal: @app_pred nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap X1 X3) (@predicates_hered.imp rmap ag_rmap X3 X1))) m *)
  change ((X2 <=> X3)%pred m) in H3.
(* Goal: @app_pred nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap X1 X3) (@predicates_hered.imp rmap ag_rmap X3 X1))) m *)
  intros y H; specialize (H2 y H); specialize (H3 y H).
(* Goal: @app_pred rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap X1 X3) (@predicates_hered.imp rmap ag_rmap X3 X1)) y *)
  destruct H2 as [H2A H2B], H3 as [H3A H3B].
(* Goal: @app_pred rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap X1 X3) (@predicates_hered.imp rmap ag_rmap X3 X1)) y *)
  split; intros z H0.
  + specialize (H2A z H0); specialize (H3A z H0); auto.
  + specialize (H2B z H0); specialize (H3B z H0); auto.
Qed.

(*
Lemma nonexpansive_2super_non_expansive: forall {A B: Type} (F: (A -> B -> mpred) -> mpred),
  (forall a b, nonexpansive (fun Q => F P Q)) ->
  (forall Q, nonexpansive (fun P => F P Q)) ->
  forall P Q n,
  approx n (F P Q) = approx n (F (approx n P) (approx n Q)).
*)
Definition acquire_arg_type: rmaps.TypeTree := rmaps.ProdType (rmaps.ConstType (val * share)) rmaps.Mpred.

Definition acquire_pre: val * share * mpred -> environ -> mpred :=
  fun args =>
  match args with
  | (v, sh, R) =>
     PROP (readable_share sh)
     LOCAL (temp _lock v)
     SEP (lock_inv sh v R)
  end.

Notation acquire_post :=
  (fun args =>
  match args with
  | (v, sh, R) =>
     PROP ()
     LOCAL ()
     SEP (lock_inv sh v R; R)
  end).

Lemma NP_acquire_pre: @super_non_expansive acquire_arg_type (fun _ => acquire_pre).
Proof.
(* Goal: @super_non_expansive release_arg_type (fun (ts : list Type) (args : _functor ((fix dtfr (T : rmaps.TypeTree) : functor := match T with | rmaps.ConstType A => fconst A | rmaps.Mpred => fidentity | rmaps.DependentType n => fconst (@nth Type n ts unit) | rmaps.ProdType T1 T2 => fpair (dtfr T1) (dtfr T2) | rmaps.ArrowType T1 T2 => ffunc (dtfr T1) (dtfr T2) | rmaps.PiType I0 f => @fpi I0 (fun i : I0 => dtfr (f i)) | rmaps.ListType T0 => flist (dtfr T0) end) release_arg_type) mpred) => let (_f, R) := args in let (v, sh) := _f in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (lock_inv sh v R) (@nil mpred))))) *)
  hnf.
(* Goal: forall (n : nat) (P : @pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap), @eq (@pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap) (compcert_rmaps.R.approx n (compcert_rmaps.R.approx n P)) (compcert_rmaps.R.approx n P) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (approx n ((let program_branch_0 := fun (v : val) (sh : share) (R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) (@pair val share v sh) R) x) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@data_at_ cs sh tlock v) (@cons mpred R (@nil mpred))))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) x' x, _functor (ffunc (fconst environ) fidentity) mpred) := x in let (v, sh) as _f0 return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) _f0 R) x, _functor (ffunc (fconst environ) fidentity) mpred) := _f in program_branch_0 v sh R) (@eq_refl (_functor (fpair (fconst (prod val share)) fidentity) mpred) x)) rho)) (approx n ((let program_branch_0 := fun (v : val) (sh : share) (R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) (@pair val share v sh) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x)) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@data_at_ cs sh tlock v) (@cons mpred R (@nil mpred))))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) x' (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := @fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x in let (v, sh) as _f0 return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) _f0 R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := _f in program_branch_0 v sh R) (@eq_refl (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x))) rho)) *)
  destruct x as [[v sh] R]; simpl in *.
  apply (nonexpansive_super_non_expansive
   (fun R => (PROP (readable_share sh)  LOCAL (temp _lock v)  SEP (lock_inv sh v R)) rho)).
  apply (PROP_LOCAL_SEP_nonexpansive
          ((fun _ => readable_share sh) :: nil)
          ((temp _lock v) :: nil)
          ((fun R => lock_inv sh v R) :: nil));
  repeat apply Forall_cons; try apply Forall_nil.
  + unfold compose. apply const_nonexpansive.
  + apply nonexpansive_lock_inv.
Qed.

Lemma NP_acquire_post: @super_non_expansive acquire_arg_type (fun _ => acquire_post).
Proof.
(* Goal: @super_non_expansive release_arg_type (fun (ts : list Type) (args : _functor ((fix dtfr (T : rmaps.TypeTree) : functor := match T with | rmaps.ConstType A => fconst A | rmaps.Mpred => fidentity | rmaps.DependentType n => fconst (@nth Type n ts unit) | rmaps.ProdType T1 T2 => fpair (dtfr T1) (dtfr T2) | rmaps.ArrowType T1 T2 => ffunc (dtfr T1) (dtfr T2) | rmaps.PiType I0 f => @fpi I0 (fun i : I0 => dtfr (f i)) | rmaps.ListType T0 => flist (dtfr T0) end) release_arg_type) mpred) => let (_f, R) := args in let (v, sh) := _f in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (lock_inv sh v R) (@nil mpred))))) *)
  hnf.
(* Goal: forall (n : nat) (P : @pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap), @eq (@pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap) (compcert_rmaps.R.approx n (compcert_rmaps.R.approx n P)) (compcert_rmaps.R.approx n P) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (approx n ((let program_branch_0 := fun (v : val) (sh : share) (R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) (@pair val share v sh) R) x) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@data_at_ cs sh tlock v) (@cons mpred R (@nil mpred))))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) x' x, _functor (ffunc (fconst environ) fidentity) mpred) := x in let (v, sh) as _f0 return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) _f0 R) x, _functor (ffunc (fconst environ) fidentity) mpred) := _f in program_branch_0 v sh R) (@eq_refl (_functor (fpair (fconst (prod val share)) fidentity) mpred) x)) rho)) (approx n ((let program_branch_0 := fun (v : val) (sh : share) (R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) (@pair val share v sh) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x)) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@data_at_ cs sh tlock v) (@cons mpred R (@nil mpred))))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) x' (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := @fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x in let (v, sh) as _f0 return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) _f0 R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := _f in program_branch_0 v sh R) (@eq_refl (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x))) rho)) *)
  destruct x as [[v sh] R]; simpl in *.
  apply (nonexpansive_super_non_expansive
   (fun R => (PROP ()  LOCAL ()  SEP (lock_inv sh v R; R)) rho)).
  apply (PROP_LOCAL_SEP_nonexpansive
          nil
          nil
          ((fun R => lock_inv sh v R) :: (fun R => R) :: nil));
  repeat apply Forall_cons; try apply Forall_nil.
  + apply nonexpansive_lock_inv.
  + apply identity_nonexpansive.
Qed.

Definition acquire_spec: funspec := mk_funspec
  ((_lock OF tptr Tvoid)%formals :: nil, tvoid)
  cc_default
  acquire_arg_type
  (fun _ => acquire_pre)
  (fun _ => acquire_post)
  NP_acquire_pre
  NP_acquire_post
.

Definition release_arg_type: rmaps.TypeTree := rmaps.ProdType (rmaps.ConstType (val * share)) rmaps.Mpred.

Definition release_pre: val * share * mpred -> environ -> mpred :=
  fun args =>
  match args with
  | (v, sh, R) =>
     PROP (readable_share sh)
     LOCAL (temp _lock v)
     SEP (weak_exclusive_mpred R && emp; lock_inv sh v R; R)
  end.

Notation release_post :=
  (fun args =>
  match args with
  | (v, sh, R) =>
     PROP ()
     LOCAL ()
     SEP (lock_inv sh v R)
  end).

Lemma NP_release_pre: @super_non_expansive release_arg_type (fun _ => release_pre).
Proof.
(* Goal: @super_non_expansive release_arg_type (fun (ts : list Type) (args : _functor ((fix dtfr (T : rmaps.TypeTree) : functor := match T with | rmaps.ConstType A => fconst A | rmaps.Mpred => fidentity | rmaps.DependentType n => fconst (@nth Type n ts unit) | rmaps.ProdType T1 T2 => fpair (dtfr T1) (dtfr T2) | rmaps.ArrowType T1 T2 => ffunc (dtfr T1) (dtfr T2) | rmaps.PiType I0 f => @fpi I0 (fun i : I0 => dtfr (f i)) | rmaps.ListType T0 => flist (dtfr T0) end) release_arg_type) mpred) => let (_f, R) := args in let (v, sh) := _f in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (lock_inv sh v R) (@nil mpred))))) *)
  hnf.
(* Goal: forall (n : nat) (P : @pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap), @eq (@pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap) (compcert_rmaps.R.approx n (compcert_rmaps.R.approx n P)) (compcert_rmaps.R.approx n P) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (approx n ((let program_branch_0 := fun (v : val) (sh : share) (R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) (@pair val share v sh) R) x) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@data_at_ cs sh tlock v) (@cons mpred R (@nil mpred))))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) x' x, _functor (ffunc (fconst environ) fidentity) mpred) := x in let (v, sh) as _f0 return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) _f0 R) x, _functor (ffunc (fconst environ) fidentity) mpred) := _f in program_branch_0 v sh R) (@eq_refl (_functor (fpair (fconst (prod val share)) fidentity) mpred) x)) rho)) (approx n ((let program_branch_0 := fun (v : val) (sh : share) (R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) (@pair val share v sh) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x)) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@data_at_ cs sh tlock v) (@cons mpred R (@nil mpred))))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) x' (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := @fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x in let (v, sh) as _f0 return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) _f0 R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := _f in program_branch_0 v sh R) (@eq_refl (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x))) rho)) *)
  destruct x as [[v sh] R]; simpl in *.
  apply (nonexpansive_super_non_expansive
   (fun R => (PROP (readable_share sh)  LOCAL (temp _lock v)  SEP (weak_exclusive_mpred R && emp; lock_inv sh v R; R)) rho)).
  apply (PROP_LOCAL_SEP_nonexpansive
          ((fun _ => readable_share sh) :: nil)
          ((temp _lock v) :: nil)
          ((fun R => weak_exclusive_mpred R && emp)%logic :: (fun R => lock_inv sh v R) :: (fun R => R) :: nil));
  repeat apply Forall_cons; try apply Forall_nil.
  + apply const_nonexpansive.
  + apply (conj_nonexpansive (fun R => weak_exclusive_mpred R)%logic).
    - apply exclusive_mpred_nonexpansive.
    - apply const_nonexpansive.
  + apply nonexpansive_lock_inv.
  + apply identity_nonexpansive.
Qed.

Lemma NP_release_post: @super_non_expansive release_arg_type (fun _ => release_post).
Proof.
(* Goal: @super_non_expansive release_arg_type (fun (ts : list Type) (args : _functor ((fix dtfr (T : rmaps.TypeTree) : functor := match T with | rmaps.ConstType A => fconst A | rmaps.Mpred => fidentity | rmaps.DependentType n => fconst (@nth Type n ts unit) | rmaps.ProdType T1 T2 => fpair (dtfr T1) (dtfr T2) | rmaps.ArrowType T1 T2 => ffunc (dtfr T1) (dtfr T2) | rmaps.PiType I0 f => @fpi I0 (fun i : I0 => dtfr (f i)) | rmaps.ListType T0 => flist (dtfr T0) end) release_arg_type) mpred) => let (_f, R) := args in let (v, sh) := _f in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (lock_inv sh v R) (@nil mpred))))) *)
  hnf.
(* Goal: forall (n : nat) (P : @pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap), @eq (@pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap) (compcert_rmaps.R.approx n (compcert_rmaps.R.approx n P)) (compcert_rmaps.R.approx n P) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (approx n ((let program_branch_0 := fun (v : val) (sh : share) (R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) (@pair val share v sh) R) x) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@data_at_ cs sh tlock v) (@cons mpred R (@nil mpred))))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) x' x, _functor (ffunc (fconst environ) fidentity) mpred) := x in let (v, sh) as _f0 return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) _f0 R) x, _functor (ffunc (fconst environ) fidentity) mpred) := _f in program_branch_0 v sh R) (@eq_refl (_functor (fpair (fconst (prod val share)) fidentity) mpred) x)) rho)) (approx n ((let program_branch_0 := fun (v : val) (sh : share) (R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) (@pair val share v sh) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x)) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@data_at_ cs sh tlock v) (@cons mpred R (@nil mpred))))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) x' (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := @fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x in let (v, sh) as _f0 return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) _f0 R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := _f in program_branch_0 v sh R) (@eq_refl (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x))) rho)) *)
  destruct x as [[v sh] R]; simpl in *.
  apply (nonexpansive_super_non_expansive
   (fun R => (PROP ()  LOCAL ()  SEP (lock_inv sh v R)) rho)).
  apply (PROP_LOCAL_SEP_nonexpansive
          nil
          nil
          ((fun R => lock_inv sh v R) :: nil));
  repeat apply Forall_cons; try apply Forall_nil.
(* Goal: @nonexpansive rmap ag_rmap (fun R : mpred => lock_inv shl l R) *)
  apply nonexpansive_lock_inv.
Qed.

Definition release_spec: funspec := mk_funspec
  ((_lock OF tptr Tvoid)%formals :: nil, tvoid)
  cc_default
  release_arg_type
  (fun _ => release_pre)
  (fun _ => release_post)
  NP_release_pre
  NP_release_post
.

Program Definition makelock_spec cs: funspec := mk_funspec
  ((_lock OF tptr Tvoid)%formals :: nil, tvoid)
  cc_default
  (rmaps.ProdType (rmaps.ConstType (val * share)) rmaps.Mpred)
  (fun _ x =>
   match x with
   | (v, sh, R) =>
     PROP (writable_share sh)
     LOCAL (temp _lock v)
     SEP (@data_at_ cs sh tlock v)
   end)
  (fun _ x =>
   match x with
   | (v, sh, R) =>
     PROP ()
     LOCAL ()
     SEP (lock_inv sh v R)
   end)
  _
  _
.
Next Obligation.
(* Goal: @super_non_expansive release_arg_type (fun (ts : list Type) (args : _functor ((fix dtfr (T : rmaps.TypeTree) : functor := match T with | rmaps.ConstType A => fconst A | rmaps.Mpred => fidentity | rmaps.DependentType n => fconst (@nth Type n ts unit) | rmaps.ProdType T1 T2 => fpair (dtfr T1) (dtfr T2) | rmaps.ArrowType T1 T2 => ffunc (dtfr T1) (dtfr T2) | rmaps.PiType I0 f => @fpi I0 (fun i : I0 => dtfr (f i)) | rmaps.ListType T0 => flist (dtfr T0) end) release_arg_type) mpred) => let (_f, R) := args in let (v, sh) := _f in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (lock_inv sh v R) (@nil mpred))))) *)
  intros cs; hnf.
(* Goal: forall (n : nat) (P : @pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap), @eq (@pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap) (compcert_rmaps.R.approx n (compcert_rmaps.R.approx n P)) (compcert_rmaps.R.approx n P) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (approx n ((let program_branch_0 := fun (v : val) (sh : share) (R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) (@pair val share v sh) R) x) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@data_at_ cs sh tlock v) (@cons mpred R (@nil mpred))))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) x' x, _functor (ffunc (fconst environ) fidentity) mpred) := x in let (v, sh) as _f0 return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) _f0 R) x, _functor (ffunc (fconst environ) fidentity) mpred) := _f in program_branch_0 v sh R) (@eq_refl (_functor (fpair (fconst (prod val share)) fidentity) mpred) x)) rho)) (approx n ((let program_branch_0 := fun (v : val) (sh : share) (R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) (@pair val share v sh) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x)) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@data_at_ cs sh tlock v) (@cons mpred R (@nil mpred))))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) x' (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := @fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x in let (v, sh) as _f0 return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) _f0 R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := _f in program_branch_0 v sh R) (@eq_refl (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x))) rho)) *)
  destruct x as [[v sh] R]; simpl in *.
(* Goal: @eq (@pred rmap ag_rmap) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) *)
  auto.
Qed.
Next Obligation.
(* Goal: @super_non_expansive release_arg_type (fun (ts : list Type) (args : _functor ((fix dtfr (T : rmaps.TypeTree) : functor := match T with | rmaps.ConstType A => fconst A | rmaps.Mpred => fidentity | rmaps.DependentType n => fconst (@nth Type n ts unit) | rmaps.ProdType T1 T2 => fpair (dtfr T1) (dtfr T2) | rmaps.ArrowType T1 T2 => ffunc (dtfr T1) (dtfr T2) | rmaps.PiType I0 f => @fpi I0 (fun i : I0 => dtfr (f i)) | rmaps.ListType T0 => flist (dtfr T0) end) release_arg_type) mpred) => let (_f, R) := args in let (v, sh) := _f in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (lock_inv sh v R) (@nil mpred))))) *)
  intro cs; hnf.
(* Goal: forall (n : nat) (P : @pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap), @eq (@pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap) (compcert_rmaps.R.approx n (compcert_rmaps.R.approx n P)) (compcert_rmaps.R.approx n P) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (approx n ((let program_branch_0 := fun (v : val) (sh : share) (R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) (@pair val share v sh) R) x) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@data_at_ cs sh tlock v) (@cons mpred R (@nil mpred))))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) x' x, _functor (ffunc (fconst environ) fidentity) mpred) := x in let (v, sh) as _f0 return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) _f0 R) x, _functor (ffunc (fconst environ) fidentity) mpred) := _f in program_branch_0 v sh R) (@eq_refl (_functor (fpair (fconst (prod val share)) fidentity) mpred) x)) rho)) (approx n ((let program_branch_0 := fun (v : val) (sh : share) (R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) (@pair val share v sh) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x)) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@data_at_ cs sh tlock v) (@cons mpred R (@nil mpred))))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) x' (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := @fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x in let (v, sh) as _f0 return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) _f0 R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := _f in program_branch_0 v sh R) (@eq_refl (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x))) rho)) *)
  destruct x as [[v sh] R]; simpl in *.
  apply (nonexpansive_super_non_expansive
   (fun R => (PROP ()  LOCAL ()  SEP (lock_inv sh v R)) rho)).
  apply (PROP_LOCAL_SEP_nonexpansive
          nil
          nil
          ((fun R => lock_inv sh v R) :: nil));
  repeat apply Forall_cons; try apply Forall_nil.
(* Goal: @nonexpansive rmap ag_rmap (fun R : mpred => lock_inv shl l R) *)
  apply nonexpansive_lock_inv.
Qed.

Program Definition freelock_spec cs: funspec := mk_funspec
  ((_lock OF tptr Tvoid)%formals :: nil, tvoid)
  cc_default
  (rmaps.ProdType (rmaps.ConstType (val * share)) rmaps.Mpred)
  (fun _ x =>
   match x with
   | (v, sh, R) =>
     PROP (writable_share sh)
     LOCAL (temp _lock v)
     SEP (weak_exclusive_mpred R && emp; lock_inv sh v R; R)
   end)
  (fun _ x =>
   match x with
   | (v, sh, R) =>
     PROP ()
     LOCAL ()
     SEP (@data_at_ cs sh tlock v; R)
   end)
  _
  _
.
Next Obligation.
(* Goal: @super_non_expansive release_arg_type (fun (ts : list Type) (args : _functor ((fix dtfr (T : rmaps.TypeTree) : functor := match T with | rmaps.ConstType A => fconst A | rmaps.Mpred => fidentity | rmaps.DependentType n => fconst (@nth Type n ts unit) | rmaps.ProdType T1 T2 => fpair (dtfr T1) (dtfr T2) | rmaps.ArrowType T1 T2 => ffunc (dtfr T1) (dtfr T2) | rmaps.PiType I0 f => @fpi I0 (fun i : I0 => dtfr (f i)) | rmaps.ListType T0 => flist (dtfr T0) end) release_arg_type) mpred) => let (_f, R) := args in let (v, sh) := _f in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (lock_inv sh v R) (@nil mpred))))) *)
  intro cs; hnf.
(* Goal: forall (n : nat) (P : @pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap), @eq (@pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap) (compcert_rmaps.R.approx n (compcert_rmaps.R.approx n P)) (compcert_rmaps.R.approx n P) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (approx n ((let program_branch_0 := fun (v : val) (sh : share) (R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) (@pair val share v sh) R) x) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@data_at_ cs sh tlock v) (@cons mpred R (@nil mpred))))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) x' x, _functor (ffunc (fconst environ) fidentity) mpred) := x in let (v, sh) as _f0 return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) _f0 R) x, _functor (ffunc (fconst environ) fidentity) mpred) := _f in program_branch_0 v sh R) (@eq_refl (_functor (fpair (fconst (prod val share)) fidentity) mpred) x)) rho)) (approx n ((let program_branch_0 := fun (v : val) (sh : share) (R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) (@pair val share v sh) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x)) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@data_at_ cs sh tlock v) (@cons mpred R (@nil mpred))))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) x' (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := @fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x in let (v, sh) as _f0 return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) _f0 R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := _f in program_branch_0 v sh R) (@eq_refl (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x))) rho)) *)
  destruct x as [[v sh] R]; simpl in *.
Admitted. (* super_non_expansive obligation of freelock_spec' *)
(*
  apply (nonexpansive_super_non_expansive
   (fun R => (PROP (writable_share sh)
    LOCAL (temp _lock v)
    SEP (weak_positive_mpred R && emp; lock_inv sh v R; R)) rho)).
  apply (PROP_LOCAL_SEP_nonexpansive
          ((fun _ => writable_share sh) :: nil)
          (temp _lock v :: nil)
          ((fun R => weak_positive_mpred R && emp)%logic :: (fun R => lock_inv sh v R) :: (fun R => R) :: nil));
  repeat apply Forall_cons; try apply Forall_nil.
  + apply const_nonexpansive.
  + apply (conj_nonexpansive weak_positive_mpred).
    - apply positive_mpred_nonexpansive.
    - apply const_nonexpansive.
  + apply nonexpansive_lock_inv.
  + apply identity_nonexpansive.
Qed.
*)
Next Obligation.
(* Goal: @super_non_expansive release_arg_type (fun (ts : list Type) (args : _functor ((fix dtfr (T : rmaps.TypeTree) : functor := match T with | rmaps.ConstType A => fconst A | rmaps.Mpred => fidentity | rmaps.DependentType n => fconst (@nth Type n ts unit) | rmaps.ProdType T1 T2 => fpair (dtfr T1) (dtfr T2) | rmaps.ArrowType T1 T2 => ffunc (dtfr T1) (dtfr T2) | rmaps.PiType I0 f => @fpi I0 (fun i : I0 => dtfr (f i)) | rmaps.ListType T0 => flist (dtfr T0) end) release_arg_type) mpred) => let (_f, R) := args in let (v, sh) := _f in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (lock_inv sh v R) (@nil mpred))))) *)
  intro cs; hnf.
(* Goal: forall (n : nat) (P : @pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap), @eq (@pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap) (compcert_rmaps.R.approx n (compcert_rmaps.R.approx n P)) (compcert_rmaps.R.approx n P) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (approx n ((let program_branch_0 := fun (v : val) (sh : share) (R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) (@pair val share v sh) R) x) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@data_at_ cs sh tlock v) (@cons mpred R (@nil mpred))))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) x' x, _functor (ffunc (fconst environ) fidentity) mpred) := x in let (v, sh) as _f0 return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) _f0 R) x, _functor (ffunc (fconst environ) fidentity) mpred) := _f in program_branch_0 v sh R) (@eq_refl (_functor (fpair (fconst (prod val share)) fidentity) mpred) x)) rho)) (approx n ((let program_branch_0 := fun (v : val) (sh : share) (R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) (@pair val share v sh) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x)) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@data_at_ cs sh tlock v) (@cons mpred R (@nil mpred))))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) x' (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := @fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x in let (v, sh) as _f0 return (forall _ : @eq (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) _f0 R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := _f in program_branch_0 v sh R) (@eq_refl (_functor (fpair (fconst (prod val share)) fidentity) mpred) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x))) rho)) *)
  destruct x as [[v sh] R]; simpl in *.
  apply (nonexpansive_super_non_expansive
   (fun R => (PROP ()  LOCAL ()  SEP (data_at_ sh tlock v; R)) rho)).
  apply (PROP_LOCAL_SEP_nonexpansive
          nil
          nil
          ((fun _ => data_at_ sh tlock v) :: (fun R => R) :: nil));
  repeat apply Forall_cons; try apply Forall_nil.
  + apply const_nonexpansive.
  + apply identity_nonexpansive.
Qed.

(* versions that give away all their resources *)

Lemma selflock_rec : forall sh v R, rec_inv sh v R (selflock R sh v).
Proof.
(* Goal: forall (sh : share) (v : val) (R : mpred), rec_inv sh v R (selflock R sh v) *)
  intros; unfold rec_inv.
(* Goal: @eq mpred (selflock R sh v) (@sepcon mpred Nveric Sveric R (@later mpred Nveric Iveric (lock_inv sh v (selflock R sh v)))) *)
  apply selflock_eq.
Qed.

Program Definition freelock2_spec cs: funspec := mk_funspec
  ((_lock OF tptr Tvoid)%formals :: nil, tvoid)
  cc_default
  (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (val * share * share)) rmaps.Mpred) rmaps.Mpred)
  (fun _ x =>
   match x with
   | (v, sh, sh', Q, R) =>
     PROP (writable_share sh)
     LOCAL (temp _lock v)
     SEP (weak_exclusive_mpred R && weak_rec_inv sh' v Q R && emp; lock_inv sh v R)
   end)
  (fun _ x =>
   match x with
   | (v, sh, sh', Q, R) =>
     PROP ()
     LOCAL ()
     SEP (@data_at_ cs sh tlock v)
   end)
  _
  _
.
Next Obligation.
(* Goal: @super_non_expansive release_arg_type (fun (ts : list Type) (args : _functor ((fix dtfr (T : rmaps.TypeTree) : functor := match T with | rmaps.ConstType A => fconst A | rmaps.Mpred => fidentity | rmaps.DependentType n => fconst (@nth Type n ts unit) | rmaps.ProdType T1 T2 => fpair (dtfr T1) (dtfr T2) | rmaps.ArrowType T1 T2 => ffunc (dtfr T1) (dtfr T2) | rmaps.PiType I0 f => @fpi I0 (fun i : I0 => dtfr (f i)) | rmaps.ListType T0 => flist (dtfr T0) end) release_arg_type) mpred) => let (_f, R) := args in let (v, sh) := _f in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (lock_inv sh v R) (@nil mpred))))) *)
  intro cs; hnf.
(* Goal: forall (n : nat) (P : @pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap), @eq (@pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap) (compcert_rmaps.R.approx n (compcert_rmaps.R.approx n P)) (compcert_rmaps.R.approx n P) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (approx n ((let program_branch_0 := fun (v : val) (sh sh' : share) (Q R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fpair (fconst (prod (prod val share) share)) fidentity) fidentity) mpred) (@pair (_functor (fpair (fconst (prod (prod val share) share)) fidentity) mpred) (_functor fidentity mpred) (@pair (_functor (fconst (prod (prod val share) share)) mpred) (_functor fidentity mpred) (@pair (prod val share) share (@pair val share v sh) sh') Q) R) x) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@data_at_ cs sh tlock v) (@nil mpred)))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fpair (fconst (prod (prod val share) share)) fidentity) fidentity) mpred) x' x, _functor (ffunc (fconst environ) fidentity) mpred) := x in let (_f0, Q) as _f0 return (forall _ : @eq (_functor (fpair (fpair (fconst (prod (prod val share) share)) fidentity) fidentity) mpred) (@pair (_functor (fpair (fconst (prod (prod val share) share)) fidentity) mpred) (_functor fidentity mpred) _f0 R) x, _functor (ffunc (fconst environ) fidentity) mpred) := _f in let (p, sh') as _f1 return (forall _ : @eq (_functor (fpair (fpair (fconst (prod (prod val share) share)) fidentity) fidentity) mpred) (@pair (_functor (fpair (fconst (prod (prod val share) share)) fidentity) mpred) (_functor fidentity mpred) (@pair (_functor (fconst (prod (prod val share) share)) mpred) (_functor fidentity mpred) _f1 Q) R) x, _functor (ffunc (fconst environ) fidentity) mpred) := _f0 in let (v, sh) as p0 return (forall _ : @eq (_functor (fpair (fpair (fconst (prod (prod val share) share)) fidentity) fidentity) mpred) (@pair (_functor (fpair (fconst (prod (prod val share) share)) fidentity) mpred) (_functor fidentity mpred) (@pair (_functor (fconst (prod (prod val share) share)) mpred) (_functor fidentity mpred) (@pair (prod val share) share p0 sh') Q) R) x, _functor (ffunc (fconst environ) fidentity) mpred) := p in program_branch_0 v sh sh' Q R) (@eq_refl (_functor (fpair (fpair (fconst (prod (prod val share) share)) fidentity) fidentity) mpred) x)) rho)) (approx n ((let program_branch_0 := fun (v : val) (sh sh' : share) (Q R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fpair (fconst (prod (prod val share) share)) fidentity) fidentity) mpred) (@pair (_functor (fpair (fconst (prod (prod val share) share)) fidentity) mpred) (_functor fidentity mpred) (@pair (_functor (fconst (prod (prod val share) share)) mpred) (_functor fidentity mpred) (@pair (prod val share) share (@pair val share v sh) sh') Q) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (prod (prod val share) share)) rmaps.Mpred) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x)) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@data_at_ cs sh tlock v) (@nil mpred)))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fpair (fconst (prod (prod val share) share)) fidentity) fidentity) mpred) x' (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (prod (prod val share) share)) rmaps.Mpred) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := @fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (prod (prod val share) share)) rmaps.Mpred) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x in let (_f0, Q) as _f0 return (forall _ : @eq (_functor (fpair (fpair (fconst (prod (prod val share) share)) fidentity) fidentity) mpred) (@pair (_functor (fpair (fconst (prod (prod val share) share)) fidentity) mpred) (_functor fidentity mpred) _f0 R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (prod (prod val share) share)) rmaps.Mpred) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := _f in let (p, sh') as _f1 return (forall _ : @eq (_functor (fpair (fpair (fconst (prod (prod val share) share)) fidentity) fidentity) mpred) (@pair (_functor (fpair (fconst (prod (prod val share) share)) fidentity) mpred) (_functor fidentity mpred) (@pair (_functor (fconst (prod (prod val share) share)) mpred) (_functor fidentity mpred) _f1 Q) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (prod (prod val share) share)) rmaps.Mpred) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := _f0 in let (v, sh) as p0 return (forall _ : @eq (_functor (fpair (fpair (fconst (prod (prod val share) share)) fidentity) fidentity) mpred) (@pair (_functor (fpair (fconst (prod (prod val share) share)) fidentity) mpred) (_functor fidentity mpred) (@pair (_functor (fconst (prod (prod val share) share)) mpred) (_functor fidentity mpred) (@pair (prod val share) share p0 sh') Q) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (prod (prod val share) share)) rmaps.Mpred) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := p in program_branch_0 v sh sh' Q R) (@eq_refl (_functor (fpair (fpair (fconst (prod (prod val share) share)) fidentity) fidentity) mpred) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (prod (prod val share) share)) rmaps.Mpred) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x))) rho)) *)
  destruct x as [[[[v sh] sh'] Q] R]; simpl in *.
  apply (nonexpansive2_super_non_expansive
   (fun Q R => (PROP (writable_share sh)
     LOCAL (temp _lock v)
     SEP (weak_exclusive_mpred R && weak_rec_inv sh' v Q R && emp; lock_inv sh v R)) rho));
  [ clear Q R; intros Q;
    apply (PROP_LOCAL_SEP_nonexpansive
            ((fun _ => writable_share sh) :: nil)
            (temp _lock v :: nil)
            ((fun R => weak_exclusive_mpred R && weak_rec_inv sh' v Q R && emp)%logic :: (fun R => lock_inv sh v R) :: nil))
  | clear Q R; intros R;
    apply (PROP_LOCAL_SEP_nonexpansive
            ((fun _ => writable_share sh) :: nil)
            (temp _lock v :: nil)
            ((fun Q => weak_exclusive_mpred R && weak_rec_inv sh' v Q R && emp)%logic :: (fun _ => lock_inv sh v R) :: nil))];
  repeat apply Forall_cons; try apply Forall_nil.
  + apply const_nonexpansive.
  + apply (conj_nonexpansive (fun R => weak_exclusive_mpred R && weak_rec_inv sh' v Q R)%logic); [apply (conj_nonexpansive weak_exclusive_mpred) |].
    - apply exclusive_mpred_nonexpansive.
    - apply rec_inv1_nonexpansive.
    - apply const_nonexpansive.
  + apply nonexpansive_lock_inv.
  + apply const_nonexpansive.
  + apply (conj_nonexpansive (fun Q => weak_exclusive_mpred R && weak_rec_inv sh' v Q R)%logic); [apply (conj_nonexpansive (fun _ => weak_exclusive_mpred R)) |].
    - apply const_nonexpansive.
    - apply rec_inv2_nonexpansive.
    - apply const_nonexpansive.
  + apply const_nonexpansive.
Qed.
Next Obligation.
(* Goal: @super_non_expansive release_arg_type (fun (ts : list Type) (args : _functor ((fix dtfr (T : rmaps.TypeTree) : functor := match T with | rmaps.ConstType A => fconst A | rmaps.Mpred => fidentity | rmaps.DependentType n => fconst (@nth Type n ts unit) | rmaps.ProdType T1 T2 => fpair (dtfr T1) (dtfr T2) | rmaps.ArrowType T1 T2 => ffunc (dtfr T1) (dtfr T2) | rmaps.PiType I0 f => @fpi I0 (fun i : I0 => dtfr (f i)) | rmaps.ListType T0 => flist (dtfr T0) end) release_arg_type) mpred) => let (_f, R) := args in let (v, sh) := _f in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (lock_inv sh v R) (@nil mpred))))) *)
  intro cs; hnf.
(* Goal: forall (n : nat) (P : @pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap), @eq (@pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap) (compcert_rmaps.R.approx n (compcert_rmaps.R.approx n P)) (compcert_rmaps.R.approx n P) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (approx n ((let program_branch_0 := fun (v : val) (sh sh' : share) (Q R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fpair (fconst (prod (prod val share) share)) fidentity) fidentity) mpred) (@pair (_functor (fpair (fconst (prod (prod val share) share)) fidentity) mpred) (_functor fidentity mpred) (@pair (_functor (fconst (prod (prod val share) share)) mpred) (_functor fidentity mpred) (@pair (prod val share) share (@pair val share v sh) sh') Q) R) x) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@data_at_ cs sh tlock v) (@nil mpred)))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fpair (fconst (prod (prod val share) share)) fidentity) fidentity) mpred) x' x, _functor (ffunc (fconst environ) fidentity) mpred) := x in let (_f0, Q) as _f0 return (forall _ : @eq (_functor (fpair (fpair (fconst (prod (prod val share) share)) fidentity) fidentity) mpred) (@pair (_functor (fpair (fconst (prod (prod val share) share)) fidentity) mpred) (_functor fidentity mpred) _f0 R) x, _functor (ffunc (fconst environ) fidentity) mpred) := _f in let (p, sh') as _f1 return (forall _ : @eq (_functor (fpair (fpair (fconst (prod (prod val share) share)) fidentity) fidentity) mpred) (@pair (_functor (fpair (fconst (prod (prod val share) share)) fidentity) mpred) (_functor fidentity mpred) (@pair (_functor (fconst (prod (prod val share) share)) mpred) (_functor fidentity mpred) _f1 Q) R) x, _functor (ffunc (fconst environ) fidentity) mpred) := _f0 in let (v, sh) as p0 return (forall _ : @eq (_functor (fpair (fpair (fconst (prod (prod val share) share)) fidentity) fidentity) mpred) (@pair (_functor (fpair (fconst (prod (prod val share) share)) fidentity) mpred) (_functor fidentity mpred) (@pair (_functor (fconst (prod (prod val share) share)) mpred) (_functor fidentity mpred) (@pair (prod val share) share p0 sh') Q) R) x, _functor (ffunc (fconst environ) fidentity) mpred) := p in program_branch_0 v sh sh' Q R) (@eq_refl (_functor (fpair (fpair (fconst (prod (prod val share) share)) fidentity) fidentity) mpred) x)) rho)) (approx n ((let program_branch_0 := fun (v : val) (sh sh' : share) (Q R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fpair (fconst (prod (prod val share) share)) fidentity) fidentity) mpred) (@pair (_functor (fpair (fconst (prod (prod val share) share)) fidentity) mpred) (_functor fidentity mpred) (@pair (_functor (fconst (prod (prod val share) share)) mpred) (_functor fidentity mpred) (@pair (prod val share) share (@pair val share v sh) sh') Q) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (prod (prod val share) share)) rmaps.Mpred) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x)) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@data_at_ cs sh tlock v) (@nil mpred)))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fpair (fconst (prod (prod val share) share)) fidentity) fidentity) mpred) x' (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (prod (prod val share) share)) rmaps.Mpred) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := @fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (prod (prod val share) share)) rmaps.Mpred) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x in let (_f0, Q) as _f0 return (forall _ : @eq (_functor (fpair (fpair (fconst (prod (prod val share) share)) fidentity) fidentity) mpred) (@pair (_functor (fpair (fconst (prod (prod val share) share)) fidentity) mpred) (_functor fidentity mpred) _f0 R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (prod (prod val share) share)) rmaps.Mpred) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := _f in let (p, sh') as _f1 return (forall _ : @eq (_functor (fpair (fpair (fconst (prod (prod val share) share)) fidentity) fidentity) mpred) (@pair (_functor (fpair (fconst (prod (prod val share) share)) fidentity) mpred) (_functor fidentity mpred) (@pair (_functor (fconst (prod (prod val share) share)) mpred) (_functor fidentity mpred) _f1 Q) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (prod (prod val share) share)) rmaps.Mpred) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := _f0 in let (v, sh) as p0 return (forall _ : @eq (_functor (fpair (fpair (fconst (prod (prod val share) share)) fidentity) fidentity) mpred) (@pair (_functor (fpair (fconst (prod (prod val share) share)) fidentity) mpred) (_functor fidentity mpred) (@pair (_functor (fconst (prod (prod val share) share)) mpred) (_functor fidentity mpred) (@pair (prod val share) share p0 sh') Q) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (prod (prod val share) share)) rmaps.Mpred) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := p in program_branch_0 v sh sh' Q R) (@eq_refl (_functor (fpair (fpair (fconst (prod (prod val share) share)) fidentity) fidentity) mpred) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (prod (prod val share) share)) rmaps.Mpred) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x))) rho)) *)
  destruct x as [[[[v sh] sh'] Q] R]; simpl in *.
(* Goal: @eq (@pred rmap ag_rmap) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) *)
  auto.
Qed.

Program Definition release2_spec: funspec := mk_funspec
  ((_lock OF tptr Tvoid)%formals :: nil, tvoid)
  cc_default
  (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (val * share)) rmaps.Mpred) rmaps.Mpred)
  (fun _ x =>
   match x with
   | (v, sh, Q, R) =>
     PROP (readable_share sh)
     LOCAL (temp _lock v)
     SEP (weak_exclusive_mpred R && weak_rec_inv sh v Q R && emp; R)
   end)
  (fun _ x =>
   match x with
   | (v, sh, Q, R) =>
     PROP ()
     LOCAL ()
     SEP (emp)
   end)
  _
  _
.
Next Obligation.
(* Goal: @super_non_expansive release_arg_type (fun (ts : list Type) (args : _functor ((fix dtfr (T : rmaps.TypeTree) : functor := match T with | rmaps.ConstType A => fconst A | rmaps.Mpred => fidentity | rmaps.DependentType n => fconst (@nth Type n ts unit) | rmaps.ProdType T1 T2 => fpair (dtfr T1) (dtfr T2) | rmaps.ArrowType T1 T2 => ffunc (dtfr T1) (dtfr T2) | rmaps.PiType I0 f => @fpi I0 (fun i : I0 => dtfr (f i)) | rmaps.ListType T0 => flist (dtfr T0) end) release_arg_type) mpred) => let (_f, R) := args in let (v, sh) := _f in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (lock_inv sh v R) (@nil mpred))))) *)
  intro cs; hnf.
(* Goal: forall (n : nat) (P : @pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap), @eq (@pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap) (compcert_rmaps.R.approx n (compcert_rmaps.R.approx n P)) (compcert_rmaps.R.approx n P) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (approx cs ((let program_branch_0 := fun (v : val) (sh : share) (Q R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fpair (fconst (prod val share)) fidentity) fidentity) mpred) (@pair (_functor (fpair (fconst (prod val share)) fidentity) mpred) (_functor fidentity mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) (@pair val share v sh) Q) R) x) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fpair (fconst (prod val share)) fidentity) fidentity) mpred) x' x, _functor (ffunc (fconst environ) fidentity) mpred) := x in let (_f0, Q) as _f0 return (forall _ : @eq (_functor (fpair (fpair (fconst (prod val share)) fidentity) fidentity) mpred) (@pair (_functor (fpair (fconst (prod val share)) fidentity) mpred) (_functor fidentity mpred) _f0 R) x, _functor (ffunc (fconst environ) fidentity) mpred) := _f in let (v, sh) as _f1 return (forall _ : @eq (_functor (fpair (fpair (fconst (prod val share)) fidentity) fidentity) mpred) (@pair (_functor (fpair (fconst (prod val share)) fidentity) mpred) (_functor fidentity mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) _f1 Q) R) x, _functor (ffunc (fconst environ) fidentity) mpred) := _f0 in program_branch_0 v sh Q R) (@eq_refl (_functor (fpair (fpair (fconst (prod val share)) fidentity) fidentity) mpred) x)) rho)) (approx cs ((let program_branch_0 := fun (v : val) (sh : share) (Q R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fpair (fconst (prod val share)) fidentity) fidentity) mpred) (@pair (_functor (fpair (fconst (prod val share)) fidentity) mpred) (_functor fidentity mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) (@pair val share v sh) Q) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx cs) (approx cs) x)) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fpair (fconst (prod val share)) fidentity) fidentity) mpred) x' (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx cs) (approx cs) x), _functor (ffunc (fconst environ) fidentity) mpred) := @fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx cs) (approx cs) x in let (_f0, Q) as _f0 return (forall _ : @eq (_functor (fpair (fpair (fconst (prod val share)) fidentity) fidentity) mpred) (@pair (_functor (fpair (fconst (prod val share)) fidentity) mpred) (_functor fidentity mpred) _f0 R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx cs) (approx cs) x), _functor (ffunc (fconst environ) fidentity) mpred) := _f in let (v, sh) as _f1 return (forall _ : @eq (_functor (fpair (fpair (fconst (prod val share)) fidentity) fidentity) mpred) (@pair (_functor (fpair (fconst (prod val share)) fidentity) mpred) (_functor fidentity mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) _f1 Q) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx cs) (approx cs) x), _functor (ffunc (fconst environ) fidentity) mpred) := _f0 in program_branch_0 v sh Q R) (@eq_refl (_functor (fpair (fpair (fconst (prod val share)) fidentity) fidentity) mpred) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx cs) (approx cs) x))) rho)) *)
  destruct x as [[[v sh] Q] R]; simpl in *.
  apply (nonexpansive2_super_non_expansive
   (fun Q R => (PROP (readable_share sh)
     LOCAL (temp _lock v)
     SEP (weak_exclusive_mpred R && weak_rec_inv sh v Q R && emp; R)) rho));
  [ clear Q R; intros Q;
    apply (PROP_LOCAL_SEP_nonexpansive
            ((fun _ => readable_share sh) :: nil)
            (temp _lock v :: nil)
            ((fun R => weak_exclusive_mpred R && weak_rec_inv sh v Q R && emp)%logic :: (fun R => R) :: nil))
  | clear Q R; intros R;
    apply (PROP_LOCAL_SEP_nonexpansive
            ((fun _ => readable_share sh) :: nil)
            (temp _lock v :: nil)
            ((fun Q => weak_exclusive_mpred R && weak_rec_inv sh v Q R && emp)%logic :: (fun _ => R) :: nil))];
  repeat apply Forall_cons; try apply Forall_nil.
  + apply const_nonexpansive.
  + apply (conj_nonexpansive (fun R => weak_exclusive_mpred R && weak_rec_inv sh v Q R)%logic); [apply (conj_nonexpansive (fun R => weak_exclusive_mpred R)%logic) |].
    - apply exclusive_mpred_nonexpansive.
    - apply rec_inv1_nonexpansive.
    - apply const_nonexpansive.
  + apply identity_nonexpansive.
  + apply const_nonexpansive.
  + apply (conj_nonexpansive (fun Q => weak_exclusive_mpred R && weak_rec_inv sh v Q R)%logic); [apply (conj_nonexpansive (fun Q => weak_exclusive_mpred R)%logic) |].
    - apply const_nonexpansive.
    - apply rec_inv2_nonexpansive.
    - apply const_nonexpansive.
  + apply const_nonexpansive.
Qed.
Next Obligation.
(* Goal: @super_non_expansive release_arg_type (fun (ts : list Type) (args : _functor ((fix dtfr (T : rmaps.TypeTree) : functor := match T with | rmaps.ConstType A => fconst A | rmaps.Mpred => fidentity | rmaps.DependentType n => fconst (@nth Type n ts unit) | rmaps.ProdType T1 T2 => fpair (dtfr T1) (dtfr T2) | rmaps.ArrowType T1 T2 => ffunc (dtfr T1) (dtfr T2) | rmaps.PiType I0 f => @fpi I0 (fun i : I0 => dtfr (f i)) | rmaps.ListType T0 => flist (dtfr T0) end) release_arg_type) mpred) => let (_f, R) := args in let (v, sh) := _f in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (lock_inv sh v R) (@nil mpred))))) *)
  intro cs; hnf.
(* Goal: forall (n : nat) (P : @pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap), @eq (@pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap) (compcert_rmaps.R.approx n (compcert_rmaps.R.approx n P)) (compcert_rmaps.R.approx n P) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (approx cs ((let program_branch_0 := fun (v : val) (sh : share) (Q R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fpair (fconst (prod val share)) fidentity) fidentity) mpred) (@pair (_functor (fpair (fconst (prod val share)) fidentity) mpred) (_functor fidentity mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) (@pair val share v sh) Q) R) x) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fpair (fconst (prod val share)) fidentity) fidentity) mpred) x' x, _functor (ffunc (fconst environ) fidentity) mpred) := x in let (_f0, Q) as _f0 return (forall _ : @eq (_functor (fpair (fpair (fconst (prod val share)) fidentity) fidentity) mpred) (@pair (_functor (fpair (fconst (prod val share)) fidentity) mpred) (_functor fidentity mpred) _f0 R) x, _functor (ffunc (fconst environ) fidentity) mpred) := _f in let (v, sh) as _f1 return (forall _ : @eq (_functor (fpair (fpair (fconst (prod val share)) fidentity) fidentity) mpred) (@pair (_functor (fpair (fconst (prod val share)) fidentity) mpred) (_functor fidentity mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) _f1 Q) R) x, _functor (ffunc (fconst environ) fidentity) mpred) := _f0 in program_branch_0 v sh Q R) (@eq_refl (_functor (fpair (fpair (fconst (prod val share)) fidentity) fidentity) mpred) x)) rho)) (approx cs ((let program_branch_0 := fun (v : val) (sh : share) (Q R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fpair (fconst (prod val share)) fidentity) fidentity) mpred) (@pair (_functor (fpair (fconst (prod val share)) fidentity) mpred) (_functor fidentity mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) (@pair val share v sh) Q) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx cs) (approx cs) x)) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fpair (fconst (prod val share)) fidentity) fidentity) mpred) x' (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx cs) (approx cs) x), _functor (ffunc (fconst environ) fidentity) mpred) := @fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx cs) (approx cs) x in let (_f0, Q) as _f0 return (forall _ : @eq (_functor (fpair (fpair (fconst (prod val share)) fidentity) fidentity) mpred) (@pair (_functor (fpair (fconst (prod val share)) fidentity) mpred) (_functor fidentity mpred) _f0 R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx cs) (approx cs) x), _functor (ffunc (fconst environ) fidentity) mpred) := _f in let (v, sh) as _f1 return (forall _ : @eq (_functor (fpair (fpair (fconst (prod val share)) fidentity) fidentity) mpred) (@pair (_functor (fpair (fconst (prod val share)) fidentity) mpred) (_functor fidentity mpred) (@pair (_functor (fconst (prod val share)) mpred) (_functor fidentity mpred) _f1 Q) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx cs) (approx cs) x), _functor (ffunc (fconst environ) fidentity) mpred) := _f0 in program_branch_0 v sh Q R) (@eq_refl (_functor (fpair (fpair (fconst (prod val share)) fidentity) fidentity) mpred) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (prod val share)) rmaps.Mpred) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx cs) (approx cs) x))) rho)) *)
  destruct x as [[[v sh] Q] R]; simpl in *.
(* Goal: @eq (@pred rmap ag_rmap) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) *)
  auto.
Qed.

(* condition variables *)
Definition makecond_spec cs :=
   WITH v : val, sh : share
   PRE [ _cond OF tptr tcond ]
     PROP (writable_share sh)
     LOCAL (temp _cond v)
     SEP (@data_at_ cs sh tcond v)
   POST [ tvoid ]
     PROP ()
     LOCAL ()
     SEP (cond_var sh v).

Definition freecond_spec cs :=
   WITH v : val, sh : share
   PRE [ _cond OF tptr tcond ]
     PROP (writable_share sh)
     LOCAL (temp _cond v)
     SEP (@cond_var cs sh v)
   POST [ tvoid ]
     PROP ()
     LOCAL ()
     SEP (@data_at_ cs sh tcond v).

Program Definition wait_spec cs: funspec := mk_funspec
  ((_cond OF tptr tcond)%formals :: (_lock OF tptr Tvoid)%formals :: nil, tvoid)
  cc_default
  (rmaps.ProdType (rmaps.ConstType (val * val * share * share)) rmaps.Mpred)
  (fun _ x =>
   match x with
   | (c, l, shc, shl, R) =>
     PROP (readable_share shc)
     LOCAL (temp _cond c; temp _lock l)
     SEP (@cond_var cs shc c; lock_inv shl l R; R)
   end)
  (fun _ x =>
   match x with
   | (c, l, shc, shl, R) =>
     PROP ()
     LOCAL ()
     SEP (cond_var shc c; lock_inv shl l R; R)
   end)
  _
  _
.
Next Obligation.
(* Goal: @super_non_expansive release_arg_type (fun (ts : list Type) (args : _functor ((fix dtfr (T : rmaps.TypeTree) : functor := match T with | rmaps.ConstType A => fconst A | rmaps.Mpred => fidentity | rmaps.DependentType n => fconst (@nth Type n ts unit) | rmaps.ProdType T1 T2 => fpair (dtfr T1) (dtfr T2) | rmaps.ArrowType T1 T2 => ffunc (dtfr T1) (dtfr T2) | rmaps.PiType I0 f => @fpi I0 (fun i : I0 => dtfr (f i)) | rmaps.ListType T0 => flist (dtfr T0) end) release_arg_type) mpred) => let (_f, R) := args in let (v, sh) := _f in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (lock_inv sh v R) (@nil mpred))))) *)
  intros cs; hnf.
(* Goal: forall (n : nat) (P : @pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap), @eq (@pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap) (compcert_rmaps.R.approx n (compcert_rmaps.R.approx n P)) (compcert_rmaps.R.approx n P) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (approx n ((let program_branch_0 := fun (c l : val) (shc shl : share) (R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) (@pair (prod (prod val val) share) share (@pair (prod val val) share (@pair val val c l) shc) shl) R) x) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (lock_inv shl l R) (@cons mpred R (@nil mpred))))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) x' x, _functor (ffunc (fconst environ) fidentity) mpred) := x in let (p, shl) as _f0 return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) _f0 R) x, _functor (ffunc (fconst environ) fidentity) mpred) := _f in let (p0, shc) as p0 return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) (@pair (prod (prod val val) share) share p0 shl) R) x, _functor (ffunc (fconst environ) fidentity) mpred) := p in let (c, l) as p1 return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) (@pair (prod (prod val val) share) share (@pair (prod val val) share p1 shc) shl) R) x, _functor (ffunc (fconst environ) fidentity) mpred) := p0 in program_branch_0 c l shc shl R) (@eq_refl (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) x)) rho)) (approx n ((let program_branch_0 := fun (c l : val) (shc shl : share) (R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) (@pair (prod (prod val val) share) share (@pair (prod val val) share (@pair val val c l) shc) shl) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod (prod (prod val val) share) share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x)) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (lock_inv shl l R) (@cons mpred R (@nil mpred))))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) x' (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod (prod (prod val val) share) share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := @fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod (prod (prod val val) share) share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x in let (p, shl) as _f0 return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) _f0 R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod (prod (prod val val) share) share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := _f in let (p0, shc) as p0 return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) (@pair (prod (prod val val) share) share p0 shl) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod (prod (prod val val) share) share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := p in let (c, l) as p1 return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) (@pair (prod (prod val val) share) share (@pair (prod val val) share p1 shc) shl) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod (prod (prod val val) share) share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := p0 in program_branch_0 c l shc shl R) (@eq_refl (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod (prod (prod val val) share) share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x))) rho)) *)
  destruct x as [[[[c l] shc] shl] R]; simpl in *.
  apply (nonexpansive_super_non_expansive
   (fun R => (PROP (readable_share shc)
    LOCAL (temp _cond c; temp _lock l)
    SEP (cond_var shc c; lock_inv shl l R; R)) rho)).
  apply (PROP_LOCAL_SEP_nonexpansive
          ((fun _ => readable_share shc) :: nil)
          (temp _cond c :: temp _lock l :: nil)
          ((fun R => cond_var shc c) :: (fun R => lock_inv shl l R) :: (fun R => R) :: nil));
  repeat apply Forall_cons; try apply Forall_nil.
  + apply const_nonexpansive.
  + apply const_nonexpansive.
  + apply nonexpansive_lock_inv.
  + apply identity_nonexpansive.
Qed.
Next Obligation.
(* Goal: @super_non_expansive release_arg_type (fun (ts : list Type) (args : _functor ((fix dtfr (T : rmaps.TypeTree) : functor := match T with | rmaps.ConstType A => fconst A | rmaps.Mpred => fidentity | rmaps.DependentType n => fconst (@nth Type n ts unit) | rmaps.ProdType T1 T2 => fpair (dtfr T1) (dtfr T2) | rmaps.ArrowType T1 T2 => ffunc (dtfr T1) (dtfr T2) | rmaps.PiType I0 f => @fpi I0 (fun i : I0 => dtfr (f i)) | rmaps.ListType T0 => flist (dtfr T0) end) release_arg_type) mpred) => let (_f, R) := args in let (v, sh) := _f in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (lock_inv sh v R) (@nil mpred))))) *)
  intros cs; hnf.
(* Goal: forall (n : nat) (P : @pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap), @eq (@pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap) (compcert_rmaps.R.approx n (compcert_rmaps.R.approx n P)) (compcert_rmaps.R.approx n P) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (approx n ((let program_branch_0 := fun (c l : val) (shc shl : share) (R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) (@pair (prod (prod val val) share) share (@pair (prod val val) share (@pair val val c l) shc) shl) R) x) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (lock_inv shl l R) (@cons mpred R (@nil mpred))))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) x' x, _functor (ffunc (fconst environ) fidentity) mpred) := x in let (p, shl) as _f0 return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) _f0 R) x, _functor (ffunc (fconst environ) fidentity) mpred) := _f in let (p0, shc) as p0 return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) (@pair (prod (prod val val) share) share p0 shl) R) x, _functor (ffunc (fconst environ) fidentity) mpred) := p in let (c, l) as p1 return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) (@pair (prod (prod val val) share) share (@pair (prod val val) share p1 shc) shl) R) x, _functor (ffunc (fconst environ) fidentity) mpred) := p0 in program_branch_0 c l shc shl R) (@eq_refl (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) x)) rho)) (approx n ((let program_branch_0 := fun (c l : val) (shc shl : share) (R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) (@pair (prod (prod val val) share) share (@pair (prod val val) share (@pair val val c l) shc) shl) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod (prod (prod val val) share) share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x)) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (lock_inv shl l R) (@cons mpred R (@nil mpred))))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) x' (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod (prod (prod val val) share) share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := @fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod (prod (prod val val) share) share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x in let (p, shl) as _f0 return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) _f0 R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod (prod (prod val val) share) share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := _f in let (p0, shc) as p0 return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) (@pair (prod (prod val val) share) share p0 shl) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod (prod (prod val val) share) share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := p in let (c, l) as p1 return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) (@pair (prod (prod val val) share) share (@pair (prod val val) share p1 shc) shl) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod (prod (prod val val) share) share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := p0 in program_branch_0 c l shc shl R) (@eq_refl (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod (prod (prod val val) share) share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x))) rho)) *)
  destruct x as [[[[c l] shc] shl] R]; simpl in *.
  apply (nonexpansive_super_non_expansive
   (fun R => (PROP ()
    LOCAL ()
    SEP (cond_var shc c; lock_inv shl l R; R)) rho)).
  apply (PROP_LOCAL_SEP_nonexpansive
          nil
          nil
          ((fun R => cond_var shc c) :: (fun R => lock_inv shl l R) :: (fun R => R) :: nil));
  repeat apply Forall_cons; try apply Forall_nil.
  + apply const_nonexpansive.
  + apply nonexpansive_lock_inv.
  + apply identity_nonexpansive.
Qed.

Program Definition wait2_spec cs: funspec := mk_funspec
  ((_cond OF tptr tcond)%formals :: (_lock OF tptr Tvoid)%formals :: nil, tvoid)
  cc_default
  (rmaps.ProdType (rmaps.ConstType (val * val * share * share)) rmaps.Mpred)
  (fun _ x =>
   match x with
   | (c, l, shc, shl, R) =>
     PROP (readable_share shc)
     LOCAL (temp _cond c; temp _lock l)
     SEP (lock_inv shl l R; R && (@cond_var cs shc c * TT))
   end)
  (fun _ x =>
   match x with
   | (c, l, shc, shl, R) =>
     PROP ()
     LOCAL ()
     SEP (lock_inv shl l R; R)
   end)
  _
  _
.
Next Obligation.
(* Goal: @super_non_expansive release_arg_type (fun (ts : list Type) (args : _functor ((fix dtfr (T : rmaps.TypeTree) : functor := match T with | rmaps.ConstType A => fconst A | rmaps.Mpred => fidentity | rmaps.DependentType n => fconst (@nth Type n ts unit) | rmaps.ProdType T1 T2 => fpair (dtfr T1) (dtfr T2) | rmaps.ArrowType T1 T2 => ffunc (dtfr T1) (dtfr T2) | rmaps.PiType I0 f => @fpi I0 (fun i : I0 => dtfr (f i)) | rmaps.ListType T0 => flist (dtfr T0) end) release_arg_type) mpred) => let (_f, R) := args in let (v, sh) := _f in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (lock_inv sh v R) (@nil mpred))))) *)
  intros cs; hnf.
(* Goal: forall (n : nat) (P : @pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap), @eq (@pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap) (compcert_rmaps.R.approx n (compcert_rmaps.R.approx n P)) (compcert_rmaps.R.approx n P) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (approx n ((let program_branch_0 := fun (c l : val) (shc shl : share) (R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) (@pair (prod (prod val val) share) share (@pair (prod val val) share (@pair val val c l) shc) shl) R) x) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (lock_inv shl l R) (@cons mpred R (@nil mpred))))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) x' x, _functor (ffunc (fconst environ) fidentity) mpred) := x in let (p, shl) as _f0 return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) _f0 R) x, _functor (ffunc (fconst environ) fidentity) mpred) := _f in let (p0, shc) as p0 return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) (@pair (prod (prod val val) share) share p0 shl) R) x, _functor (ffunc (fconst environ) fidentity) mpred) := p in let (c, l) as p1 return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) (@pair (prod (prod val val) share) share (@pair (prod val val) share p1 shc) shl) R) x, _functor (ffunc (fconst environ) fidentity) mpred) := p0 in program_branch_0 c l shc shl R) (@eq_refl (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) x)) rho)) (approx n ((let program_branch_0 := fun (c l : val) (shc shl : share) (R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) (@pair (prod (prod val val) share) share (@pair (prod val val) share (@pair val val c l) shc) shl) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod (prod (prod val val) share) share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x)) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (lock_inv shl l R) (@cons mpred R (@nil mpred))))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) x' (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod (prod (prod val val) share) share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := @fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod (prod (prod val val) share) share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x in let (p, shl) as _f0 return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) _f0 R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod (prod (prod val val) share) share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := _f in let (p0, shc) as p0 return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) (@pair (prod (prod val val) share) share p0 shl) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod (prod (prod val val) share) share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := p in let (c, l) as p1 return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) (@pair (prod (prod val val) share) share (@pair (prod val val) share p1 shc) shl) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod (prod (prod val val) share) share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := p0 in program_branch_0 c l shc shl R) (@eq_refl (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod (prod (prod val val) share) share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x))) rho)) *)
  destruct x as [[[[c l] shc] shl] R]; simpl in *.
  apply (nonexpansive_super_non_expansive
   (fun R => (PROP (readable_share shc)
    LOCAL (temp _cond c; temp _lock l)
    SEP (lock_inv shl l R; R && (@cond_var cs shc c * TT))) rho)).
  apply (PROP_LOCAL_SEP_nonexpansive
          ((fun _ => readable_share shc) :: nil)
          (temp _cond c :: temp _lock l :: nil)
          ((fun R => lock_inv shl l R) :: (fun R => R && (@cond_var cs shc c * TT))%logic :: nil));
  repeat apply Forall_cons; try apply Forall_nil.
  + apply const_nonexpansive.
  + apply nonexpansive_lock_inv.
  + apply (conj_nonexpansive (fun R => R) (fun _ => (cond_var shc c * TT)%logic)).
    - apply identity_nonexpansive.
    - apply const_nonexpansive.
Qed.
Next Obligation.
(* Goal: @super_non_expansive release_arg_type (fun (ts : list Type) (args : _functor ((fix dtfr (T : rmaps.TypeTree) : functor := match T with | rmaps.ConstType A => fconst A | rmaps.Mpred => fidentity | rmaps.DependentType n => fconst (@nth Type n ts unit) | rmaps.ProdType T1 T2 => fpair (dtfr T1) (dtfr T2) | rmaps.ArrowType T1 T2 => ffunc (dtfr T1) (dtfr T2) | rmaps.PiType I0 f => @fpi I0 (fun i : I0 => dtfr (f i)) | rmaps.ListType T0 => flist (dtfr T0) end) release_arg_type) mpred) => let (_f, R) := args in let (v, sh) := _f in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (lock_inv sh v R) (@nil mpred))))) *)
  intros cs; hnf.
(* Goal: forall (n : nat) (P : @pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap), @eq (@pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap) (compcert_rmaps.R.approx n (compcert_rmaps.R.approx n P)) (compcert_rmaps.R.approx n P) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (approx n ((let program_branch_0 := fun (c l : val) (shc shl : share) (R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) (@pair (prod (prod val val) share) share (@pair (prod val val) share (@pair val val c l) shc) shl) R) x) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (lock_inv shl l R) (@cons mpred R (@nil mpred))))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) x' x, _functor (ffunc (fconst environ) fidentity) mpred) := x in let (p, shl) as _f0 return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) _f0 R) x, _functor (ffunc (fconst environ) fidentity) mpred) := _f in let (p0, shc) as p0 return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) (@pair (prod (prod val val) share) share p0 shl) R) x, _functor (ffunc (fconst environ) fidentity) mpred) := p in let (c, l) as p1 return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) (@pair (prod (prod val val) share) share (@pair (prod val val) share p1 shc) shl) R) x, _functor (ffunc (fconst environ) fidentity) mpred) := p0 in program_branch_0 c l shc shl R) (@eq_refl (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) x)) rho)) (approx n ((let program_branch_0 := fun (c l : val) (shc shl : share) (R : _functor fidentity mpred) (_ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) (@pair (prod (prod val val) share) share (@pair (prod val val) share (@pair val val c l) shc) shl) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod (prod (prod val val) share) share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x)) => PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (lock_inv shl l R) (@cons mpred R (@nil mpred))))) in (let (_f, R) as x' return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) x' (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod (prod (prod val val) share) share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := @fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod (prod (prod val val) share) share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x in let (p, shl) as _f0 return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) _f0 R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod (prod (prod val val) share) share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := _f in let (p0, shc) as p0 return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) (@pair (prod (prod val val) share) share p0 shl) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod (prod (prod val val) share) share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := p in let (c, l) as p1 return (forall _ : @eq (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@pair (_functor (fconst (prod (prod (prod val val) share) share)) mpred) (_functor fidentity mpred) (@pair (prod (prod val val) share) share (@pair (prod val val) share p1 shc) shl) R) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod (prod (prod val val) share) share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x), _functor (ffunc (fconst environ) fidentity) mpred) := p0 in program_branch_0 c l shc shl R) (@eq_refl (_functor (fpair (fconst (prod (prod (prod val val) share) share)) fidentity) mpred) (@fmap (rmaps.dependent_type_functor_rec ts (rmaps.ProdType (rmaps.ConstType (prod (prod (prod val val) share) share)) rmaps.Mpred)) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x))) rho)) *)
  destruct x as [[[[c l] shc] shl] R]; simpl in *.
  apply (nonexpansive_super_non_expansive
   (fun R => (PROP ()
    LOCAL ()
    SEP (lock_inv shl l R; R)) rho)).
  apply (PROP_LOCAL_SEP_nonexpansive
          nil
          nil
          ((fun R => lock_inv shl l R) :: (fun R => R) :: nil));
  repeat apply Forall_cons; try apply Forall_nil.
  + apply nonexpansive_lock_inv.
  + apply identity_nonexpansive.
Qed.

Definition signal_spec cs :=
   WITH c : val, shc : share
   PRE [ _cond OF tptr tcond ]
     PROP (readable_share shc)
     LOCAL (temp _cond c)
     SEP (@cond_var cs shc c)
   POST [ tvoid ]
     PROP ()
     LOCAL ()
     SEP (@cond_var cs shc c).



(* Notes about spawn_thread:

The spawned function has for argument name [_y], which is
existentially quantified.  The function also can use a list of global
variables [globals].

For now, the specification of the spawned function has to be exactly
of the form that you can see below (inside the "match ...").
Cao Qinxiang is working on a notion of sub-specification that might
enable us to have smoother specifications.

The postcondition might not be emp, so we have potential memory leaks
when a thread exists (those maps are still handled by the concurrent
machine).

To enable joinable threads, the postcondition would be [tptr tthread]
with a type [tthread] related to the postcondition through a [thread]
predicate in the logic.  The [join] would then also be implemented
using the oracle, as [acquire] is.  The postcondition would be [match
PrePost with existT ty (w, pre, post) => thread th (post w b)
end] *)

Local Open Scope logic.

(* @Qinxiang: it would be great to complete the annotation *)

Definition spawn_arg_type := rmaps.ProdType (rmaps.ProdType (rmaps.ProdType (rmaps.ConstType (val * val))
  (rmaps.ArrowType (rmaps.DependentType 0) (rmaps.ConstType globals))) (rmaps.DependentType 0))
  (rmaps.ArrowType (rmaps.DependentType 0) (rmaps.ArrowType (rmaps.ConstType val) rmaps.Mpred)).

Definition spawn_pre :=
  (fun (ts: list Type) (x: val * val * (nth 0 ts unit -> globals) * nth 0 ts unit *
                           (nth 0 ts unit -> val -> mpred)) =>
   match x with
   | (f, b, gv, w, pre) =>
     PROP (tc_val (tptr Tvoid) b)
     (LOCALx (temp _f f :: temp _args b :: gvars (gv w) :: nil)
     (SEP (
       EX _y : ident,
         (func_ptr'
           (WITH y : val, x : nth 0 ts unit
             PRE [ _y OF tptr tvoid ]
               PROP ()
               (LOCALx (temp _y y :: gvars (gv x) :: nil)
               (SEP   (pre x y)))
             POST [tptr tvoid]
               PROP  ()
               LOCAL ()
               SEP   ())
           f);
         pre w b)))
   end).

Definition spawn_post :=
  (fun (ts: list Type) (x: val * val * (nth 0 ts unit -> globals) * nth 0 ts unit *
                           (nth 0 ts unit -> val -> mpred)) =>
   match x with
   | (f, b, w, pre) =>
     PROP ()
     LOCAL ()
     SEP ()
   end).

Lemma approx_idem : forall n P, compcert_rmaps.R.approx n (compcert_rmaps.R.approx n P) =
  compcert_rmaps.R.approx n P.
Proof.
(* Goal: forall (n : nat) (P : @pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap), @eq (@pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap) (compcert_rmaps.R.approx n (compcert_rmaps.R.approx n P)) (compcert_rmaps.R.approx n P) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) *)
  transitivity (base.compose (compcert_rmaps.R.approx n) (compcert_rmaps.R.approx n) P); auto.
(* Goal: @eq (@pred rmap ag_rmap) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) *)
  rewrite compcert_rmaps.RML.approx_oo_approx; auto.
Qed.

Lemma spawn_pre_nonexpansive: @super_non_expansive spawn_arg_type spawn_pre.
Proof.
(* Goal: @super_non_expansive spawn_arg_type spawn_pre *)
  repeat intro.
(* Goal: @eq (@pred rmap ag_rmap) (approx n (spawn_pre ts x rho)) (approx n (spawn_pre ts (@fmap (rmaps.dependent_type_functor_rec ts spawn_arg_type) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx n) x) rho)) *)
  destruct x as ((((?, ?), ?), ?), ?); simpl.
(* Goal: @eq (@pred rmap ag_rmap) (approx n (PROPx (@cons Prop (is_pointer_or_null v0) (@nil Prop)) (LOCALx (@cons localdef (temp _f v) (@cons localdef (temp _args v0) (@cons localdef (gvars (_f0 _f1)) (@nil localdef)))) (SEPx (@cons mpred (@exp mpred Nveric ident (fun _y : ident => func_ptr' (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _y (tptr tvoid)) (@nil (prod ident type))) (tptr tvoid)) cc_default (prod val (@nth Type O ts unit)) (fun x0 : prod val (@nth Type O ts unit) => let (y, x) := x0 in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _y y) (@cons localdef (gvars (_f0 x)) (@nil localdef))) (SEPx (@cons mpred (_f2 x y) (@nil mpred))))) (fun x0 : prod val (@nth Type O ts unit) => let (_, _) := x0 in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@nil mpred))))) v)) (@cons mpred (_f2 _f1 v0) (@nil mpred))))) rho)) (approx n (PROPx (@cons Prop (is_pointer_or_null v0) (@nil Prop)) (LOCALx (@cons localdef (temp _f v) (@cons localdef (temp _args v0) (@cons localdef (gvars (_f0 _f1)) (@nil localdef)))) (SEPx (@cons mpred (@exp mpred Nveric ident (fun _y : ident => func_ptr' (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _y (tptr tvoid)) (@nil (prod ident type))) (tptr tvoid)) cc_default (prod val (@nth Type O ts unit)) (fun x0 : prod val (@nth Type O ts unit) => let (y, x) := x0 in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _y y) (@cons localdef (gvars (_f0 x)) (@nil localdef))) (SEPx (@cons mpred (approx n (_f2 x y)) (@nil mpred))))) (fun x0 : prod val (@nth Type O ts unit) => let (_, _) := x0 in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@nil mpred))))) v)) (@cons mpred (approx n (_f2 _f1 v0)) (@nil mpred))))) rho)) *)
  unfold PROPx; simpl; rewrite !approx_andp; f_equal.
(* Goal: @eq (@pred rmap ag_rmap) (approx n (LOCALx (@cons localdef (temp _f v) (@cons localdef (temp _args v0) (@cons localdef (gvars (_f0 _f1)) (@nil localdef)))) (SEPx (@cons mpred (@exp mpred Nveric ident (fun _y : ident => func_ptr' (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _y (tptr tvoid)) (@nil (prod ident type))) (tptr tvoid)) cc_default (prod val (@nth Type O ts unit)) (fun x0 : prod val (@nth Type O ts unit) => let (y, x) := x0 in fun x1 : environ => @andp mpred Nveric (@prop mpred Nveric True) (LOCALx (@cons localdef (temp _y y) (@cons localdef (gvars (_f0 x)) (@nil localdef))) (SEPx (@cons mpred (_f2 x y) (@nil mpred))) x1)) (fun x0 : prod val (@nth Type O ts unit) => let (_, _) := x0 in fun x1 : environ => @andp mpred Nveric (@prop mpred Nveric True) (LOCALx (@nil localdef) (SEPx (@nil mpred)) x1))) v)) (@cons mpred (_f2 _f1 v0) (@nil mpred)))) rho)) (approx n (LOCALx (@cons localdef (temp _f v) (@cons localdef (temp _args v0) (@cons localdef (gvars (_f0 _f1)) (@nil localdef)))) (SEPx (@cons mpred (@exp mpred Nveric ident (fun _y : ident => func_ptr' (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _y (tptr tvoid)) (@nil (prod ident type))) (tptr tvoid)) cc_default (prod val (@nth Type O ts unit)) (fun x0 : prod val (@nth Type O ts unit) => let (y, x) := x0 in fun x1 : environ => @andp mpred Nveric (@prop mpred Nveric True) (LOCALx (@cons localdef (temp _y y) (@cons localdef (gvars (_f0 x)) (@nil localdef))) (SEPx (@cons mpred (approx n (_f2 x y)) (@nil mpred))) x1)) (fun x0 : prod val (@nth Type O ts unit) => let (_, _) := x0 in fun x1 : environ => @andp mpred Nveric (@prop mpred Nveric True) (LOCALx (@nil localdef) (SEPx (@nil mpred)) x1))) v)) (@cons mpred (approx n (_f2 _f1 v0)) (@nil mpred)))) rho)) *)
  unfold LOCALx; simpl; rewrite !approx_andp; f_equal.
(* Goal: @eq (@pred rmap ag_rmap) (approx n (SEPx (@cons mpred (@exp mpred Nveric ident (fun _y : ident => func_ptr' (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _y (tptr tvoid)) (@nil (prod ident type))) (tptr tvoid)) cc_default (prod val (@nth Type O ts unit)) (fun x0 : prod val (@nth Type O ts unit) => let (y, x) := x0 in fun x1 : environ => @andp mpred Nveric (@prop mpred Nveric True) (@andp mpred Nveric (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (@liftx (Tarrow val (LiftEnviron Prop)) (@eq val y) (eval_id _y)) (@liftx (LiftEnviron Prop) (not (@eq val y Vundef)))) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (gvars_denote (_f0 x)) (@liftx (LiftEnviron Prop) True))) x1) (SEPx (@cons mpred (_f2 x y) (@nil mpred)) x1))) (fun x0 : prod val (@nth Type O ts unit) => let (_, _) := x0 in fun x1 : environ => @andp mpred Nveric (@prop mpred Nveric True) (@andp mpred Nveric (local (@liftx (LiftEnviron Prop) True) x1) (SEPx (@nil mpred) x1)))) v)) (@cons mpred (_f2 _f1 v0) (@nil mpred))) rho)) (approx n (SEPx (@cons mpred (@exp mpred Nveric ident (fun _y : ident => func_ptr' (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _y (tptr tvoid)) (@nil (prod ident type))) (tptr tvoid)) cc_default (prod val (@nth Type O ts unit)) (fun x0 : prod val (@nth Type O ts unit) => let (y, x) := x0 in fun x1 : environ => @andp mpred Nveric (@prop mpred Nveric True) (@andp mpred Nveric (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (@liftx (Tarrow val (LiftEnviron Prop)) (@eq val y) (eval_id _y)) (@liftx (LiftEnviron Prop) (not (@eq val y Vundef)))) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (gvars_denote (_f0 x)) (@liftx (LiftEnviron Prop) True))) x1) (SEPx (@cons mpred (approx n (_f2 x y)) (@nil mpred)) x1))) (fun x0 : prod val (@nth Type O ts unit) => let (_, _) := x0 in fun x1 : environ => @andp mpred Nveric (@prop mpred Nveric True) (@andp mpred Nveric (local (@liftx (LiftEnviron Prop) True) x1) (SEPx (@nil mpred) x1)))) v)) (@cons mpred (approx n (_f2 _f1 v0)) (@nil mpred))) rho)) *)
  unfold SEPx; simpl; rewrite !sepcon_emp, !approx_sepcon, ?approx_idem; f_equal.
(* Goal: @eq (@pred rmap ag_rmap) (approx n (@exp mpred Nveric ident (fun _y : ident => func_ptr' (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _y (tptr tvoid)) (@nil (prod ident type))) (tptr tvoid)) cc_default (prod val (@nth Type O ts unit)) (fun x0 : prod val (@nth Type O ts unit) => let (y, x) := x0 in fun x1 : environ => @andp mpred Nveric (@prop mpred Nveric True) (@andp mpred Nveric (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (@liftx (Tarrow val (LiftEnviron Prop)) (@eq val y) (eval_id _y)) (@liftx (LiftEnviron Prop) (not (@eq val y Vundef)))) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (gvars_denote (_f0 x)) (@liftx (LiftEnviron Prop) True))) x1) (@sepcon mpred Nveric Sveric (_f2 x y) (@emp mpred Nveric Sveric)))) (fun x0 : prod val (@nth Type O ts unit) => let (_, _) := x0 in fun x1 : environ => @andp mpred Nveric (@prop mpred Nveric True) (@andp mpred Nveric (local (@liftx (LiftEnviron Prop) True) x1) (@emp mpred Nveric Sveric)))) v))) (approx n (@exp mpred Nveric ident (fun _y : ident => func_ptr' (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _y (tptr tvoid)) (@nil (prod ident type))) (tptr tvoid)) cc_default (prod val (@nth Type O ts unit)) (fun x0 : prod val (@nth Type O ts unit) => let (y, x) := x0 in fun x1 : environ => @andp mpred Nveric (@prop mpred Nveric True) (@andp mpred Nveric (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (@liftx (Tarrow val (LiftEnviron Prop)) (@eq val y) (eval_id _y)) (@liftx (LiftEnviron Prop) (not (@eq val y Vundef)))) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (gvars_denote (_f0 x)) (@liftx (LiftEnviron Prop) True))) x1) (@sepcon mpred Nveric Sveric (approx n (_f2 x y)) (@emp mpred Nveric Sveric)))) (fun x0 : prod val (@nth Type O ts unit) => let (_, _) := x0 in fun x1 : environ => @andp mpred Nveric (@prop mpred Nveric True) (@andp mpred Nveric (local (@liftx (LiftEnviron Prop) True) x1) (@emp mpred Nveric Sveric)))) v))) *)
  rewrite !approx_exp; apply f_equal; extensionality y.
(* Goal: @eq (@pred rmap ag_rmap) (approx n (func_ptr' (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type y (tptr tvoid)) (@nil (prod ident type))) (tptr tvoid)) cc_default (prod val (@nth Type O ts unit)) (fun x0 : prod val (@nth Type O ts unit) => let (y0, x) := x0 in fun x1 : environ => @andp mpred Nveric (@prop mpred Nveric True) (@andp mpred Nveric (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (@liftx (Tarrow val (LiftEnviron Prop)) (@eq val y0) (eval_id y)) (@liftx (LiftEnviron Prop) (not (@eq val y0 Vundef)))) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (gvars_denote (_f0 x)) (@liftx (LiftEnviron Prop) True))) x1) (@sepcon mpred Nveric Sveric (_f2 x y0) (@emp mpred Nveric Sveric)))) (fun x0 : prod val (@nth Type O ts unit) => let (_, _) := x0 in fun x1 : environ => @andp mpred Nveric (@prop mpred Nveric True) (@andp mpred Nveric (local (@liftx (LiftEnviron Prop) True) x1) (@emp mpred Nveric Sveric)))) v)) (approx n (func_ptr' (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type y (tptr tvoid)) (@nil (prod ident type))) (tptr tvoid)) cc_default (prod val (@nth Type O ts unit)) (fun x0 : prod val (@nth Type O ts unit) => let (y0, x) := x0 in fun x1 : environ => @andp mpred Nveric (@prop mpred Nveric True) (@andp mpred Nveric (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (@liftx (Tarrow val (LiftEnviron Prop)) (@eq val y0) (eval_id y)) (@liftx (LiftEnviron Prop) (not (@eq val y0 Vundef)))) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (gvars_denote (_f0 x)) (@liftx (LiftEnviron Prop) True))) x1) (@sepcon mpred Nveric Sveric (approx n (_f2 x y0)) (@emp mpred Nveric Sveric)))) (fun x0 : prod val (@nth Type O ts unit) => let (_, _) := x0 in fun x1 : environ => @andp mpred Nveric (@prop mpred Nveric True) (@andp mpred Nveric (local (@liftx (LiftEnviron Prop) True) x1) (@emp mpred Nveric Sveric)))) v)) *)
  rewrite approx_func_ptr'.
(* Goal: @eq (@pred rmap ag_rmap) (approx n (func_ptr' (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type y (tptr tvoid)) (@nil (prod ident type))) (tptr tvoid)) cc_default (prod val (@nth Type O ts unit)) (fun (a : prod val (@nth Type O ts unit)) (rho : environ) => approx n ((let (y0, x) := a in fun x0 : environ => @andp mpred Nveric (@prop mpred Nveric True) (@andp mpred Nveric (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (@liftx (Tarrow val (LiftEnviron Prop)) (@eq val y0) (eval_id y)) (@liftx (LiftEnviron Prop) (not (@eq val y0 Vundef)))) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (gvars_denote (_f0 x)) (@liftx (LiftEnviron Prop) True))) x0) (@sepcon mpred Nveric Sveric (_f2 x y0) (@emp mpred Nveric Sveric)))) rho)) (fun (a : prod val (@nth Type O ts unit)) (rho : environ) => approx n ((let (_, _) := a in fun x0 : environ => @andp mpred Nveric (@prop mpred Nveric True) (@andp mpred Nveric (local (@liftx (LiftEnviron Prop) True) x0) (@emp mpred Nveric Sveric))) rho))) v)) (approx n (func_ptr' (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type y (tptr tvoid)) (@nil (prod ident type))) (tptr tvoid)) cc_default (prod val (@nth Type O ts unit)) (fun x0 : prod val (@nth Type O ts unit) => let (y0, x) := x0 in fun x1 : environ => @andp mpred Nveric (@prop mpred Nveric True) (@andp mpred Nveric (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (@liftx (Tarrow val (LiftEnviron Prop)) (@eq val y0) (eval_id y)) (@liftx (LiftEnviron Prop) (not (@eq val y0 Vundef)))) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (gvars_denote (_f0 x)) (@liftx (LiftEnviron Prop) True))) x1) (@sepcon mpred Nveric Sveric (approx n (_f2 x y0)) (@emp mpred Nveric Sveric)))) (fun x0 : prod val (@nth Type O ts unit) => let (_, _) := x0 in fun x1 : environ => @andp mpred Nveric (@prop mpred Nveric True) (@andp mpred Nveric (local (@liftx (LiftEnviron Prop) True) x1) (@emp mpred Nveric Sveric)))) v)) *)
  setoid_rewrite approx_func_ptr' at 2.
(* Goal: @eq (@pred rmap ag_rmap) (approx n (func_ptr' (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type y (tptr tvoid)) (@nil (prod ident type))) (tptr tvoid)) cc_default (prod val (@nth Type O ts unit)) (fun (a : prod val (@nth Type O ts unit)) (rho : environ) => approx n ((let (y0, x) := a in fun x0 : environ => @andp mpred Nveric (@prop mpred Nveric True) (@andp mpred Nveric (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (@liftx (Tarrow val (LiftEnviron Prop)) (@eq val y0) (eval_id y)) (@liftx (LiftEnviron Prop) (not (@eq val y0 Vundef)))) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (gvars_denote (_f0 x)) (@liftx (LiftEnviron Prop) True))) x0) (@sepcon mpred Nveric Sveric (_f2 x y0) (@emp mpred Nveric Sveric)))) rho)) (fun (a : prod val (@nth Type O ts unit)) (rho : environ) => approx n ((let (_, _) := a in fun x0 : environ => @andp mpred Nveric (@prop mpred Nveric True) (@andp mpred Nveric (local (@liftx (LiftEnviron Prop) True) x0) (@emp mpred Nveric Sveric))) rho))) v)) (approx n (func_ptr' (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type y (tptr tvoid)) (@nil (prod ident type))) (tptr tvoid)) cc_default (prod val (@nth Type O ts unit)) (fun (a : prod val (@nth Type O ts unit)) (rho : environ) => approx n ((let (y0, x) := a in fun x0 : environ => @andp mpred Nveric (@prop mpred Nveric True) (@andp mpred Nveric (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (@liftx (Tarrow val (LiftEnviron Prop)) (@eq val y0) (eval_id y)) (@liftx (LiftEnviron Prop) (not (@eq val y0 Vundef)))) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (gvars_denote (_f0 x)) (@liftx (LiftEnviron Prop) True))) x0) (@sepcon mpred Nveric Sveric (approx n (_f2 x y0)) (@emp mpred Nveric Sveric)))) rho)) (fun (a : prod val (@nth Type O ts unit)) (rho : environ) => approx n ((let (_, _) := a in fun x0 : environ => @andp mpred Nveric (@prop mpred Nveric True) (@andp mpred Nveric (local (@liftx (LiftEnviron Prop) True) x0) (@emp mpred Nveric Sveric))) rho))) v)) *)
  do 3 f_equal.
(* Goal: @eq (forall (_ : prod val (@nth Type O ts unit)) (_ : environ), @pred rmap ag_rmap) (fun (a : prod val (@nth Type O ts unit)) (rho : environ) => approx n ((let (y0, x) := a in fun x0 : environ => @andp mpred Nveric (@prop mpred Nveric True) (@andp mpred Nveric (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (@liftx (Tarrow val (LiftEnviron Prop)) (@eq val y0) (eval_id y)) (@liftx (LiftEnviron Prop) (not (@eq val y0 Vundef)))) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (gvars_denote (_f0 x)) (@liftx (LiftEnviron Prop) True))) x0) (@sepcon mpred Nveric Sveric (_f2 x y0) (@emp mpred Nveric Sveric)))) rho)) (fun (a : prod val (@nth Type O ts unit)) (rho : environ) => approx n ((let (y0, x) := a in fun x0 : environ => @andp mpred Nveric (@prop mpred Nveric True) (@andp mpred Nveric (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (@liftx (Tarrow val (LiftEnviron Prop)) (@eq val y0) (eval_id y)) (@liftx (LiftEnviron Prop) (not (@eq val y0 Vundef)))) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (gvars_denote (_f0 x)) (@liftx (LiftEnviron Prop) True))) x0) (@sepcon mpred Nveric Sveric (approx n (_f2 x y0)) (@emp mpred Nveric Sveric)))) rho)) *)
  extensionality a rho'; destruct a.
(* Goal: @eq (@pred rmap ag_rmap) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) *)
  rewrite !approx_andp, !approx_sepcon, approx_idem; auto.
Qed.

Lemma spawn_post_nonexpansive: @super_non_expansive spawn_arg_type spawn_post.
Proof.
(* Goal: forall (n : nat) (P : @pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap), @eq (@pred compcert_rmaps.R.rmap compcert_rmaps.R.ag_rmap) (compcert_rmaps.R.approx n (compcert_rmaps.R.approx n P)) (compcert_rmaps.R.approx n P) *)
  hnf; intros.
(* Goal: @eq (@pred rmap ag_rmap) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) *)
  destruct x as [[[]] pre]; auto.
Qed.

Definition spawn_spec := mk_funspec
  ((_f OF tptr voidstar_funtype)%formals :: (_args OF tptr tvoid)%formals :: nil, tvoid)
  cc_default
  spawn_arg_type
  spawn_pre
  spawn_post
  spawn_pre_nonexpansive
  spawn_post_nonexpansive.

(*+ Adding the specifications to a void ext_spec *)

Definition concurrent_simple_specs (cs : compspecs) (ext_link : string -> ident) :=
  (ext_link "acquire"%string, acquire_spec) ::
  (ext_link "release"%string, release_spec) ::
  nil.

Definition concurrent_simple_ext_spec Z (cs : compspecs) (ext_link : string -> ident) :=
  add_funspecs_rec
    ext_link
    (ok_void_spec Z).(@OK_ty)
    (ok_void_spec Z).(@OK_spec)
    (concurrent_simple_specs cs ext_link).

Definition Concurrent_Simple_Espec Z cs ext_link :=
  Build_OracleKind
    Z
    (concurrent_simple_ext_spec Z cs ext_link).

Lemma strong_nat_ind (P : nat -> Prop) (IH : forall n, (forall i, lt i n -> P i) -> P n) n : P n.
Proof.
(* Goal: @eq (@pred rmap ag_rmap) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) (approx cs (PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred)))) rho)) *)
  apply IH; induction n; intros i li; inversion li; eauto.
Qed.

Set Printing Implicit.

Definition concurrent_specs (cs : compspecs) (ext_link : string -> ident) :=
  (ext_link "acquire"%string, acquire_spec) ::
  (ext_link "release"%string, release_spec) ::
  (ext_link "makelock"%string, makelock_spec cs) ::
  (ext_link "freelock"%string, freelock_spec cs) ::
  (ext_link "spawn"%string, spawn_spec) ::
  nil.

Definition concurrent_ext_spec Z (cs : compspecs) (ext_link : string -> ident) :=
  add_funspecs_rec
    ext_link
    (ok_void_spec Z).(@OK_ty)
    (ok_void_spec Z).(@OK_spec)
    (concurrent_specs cs ext_link).

Definition Concurrent_Espec Z cs ext_link :=
  Build_OracleKind
    Z
    (concurrent_ext_spec Z cs ext_link).
