Commit ead5cad9 authored by Ralf Jung's avatar Ralf Jung

provide a closed proof of the client

parent 71dd8f63
From barrier Require Import barrier. From barrier Require Import barrier.
From program_logic Require Import auth sts saved_prop hoare ownership.
(* FIXME This needs to be imported even though barrier exports it *) (* FIXME This needs to be imported even though barrier exports it *)
From heap_lang Require Import notation. From heap_lang Require Import notation.
Import uPred. Import uPred.
...@@ -17,9 +18,7 @@ Section client. ...@@ -17,9 +18,7 @@ Section client.
heapN N heap_ctx heapN || client {{ λ _, True }}. heapN N heap_ctx heapN || client {{ λ _, True }}.
Proof. Proof.
intros ?. rewrite /client. intros ?. rewrite /client.
(* FIXME: wp (eapply newchan_spec with (P:=True%I)). *) ewp eapply (newchan_spec N heapN True%I); last done.
wp_focus (newchan _).
rewrite -(newchan_spec N heapN True%I) //.
apply sep_intro_True_r; first done. apply sep_intro_True_r; first done.
apply forall_intro=>l. apply wand_intro_l. rewrite right_id. apply forall_intro=>l. apply wand_intro_l. rewrite right_id.
wp_let. etrans; last eapply wait_spec. wp_let. etrans; last eapply wait_spec.
...@@ -27,3 +26,31 @@ Section client. ...@@ -27,3 +26,31 @@ Section client.
Qed. Qed.
End client. End client.
Section ClosedProofs.
Definition Σ : iFunctorG := agreeF .:: constF (stsRA barrier_proto.sts) .:: authF (constF heapRA)
.:: (λ _, constF unitRA) : iFunctorG.
Notation iProp := (iPropG heap_lang Σ).
Instance: authG heap_lang Σ heapRA.
Proof. split; try apply _. by exists 2%nat. Qed.
Instance: stsG heap_lang Σ barrier_proto.sts.
Proof. split; try apply _. by exists 1%nat. Qed.
Instance: savedPropG heap_lang Σ.
Proof. by exists 0%nat. Qed.
Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
Proof.
apply ht_alt. rewrite (heap_alloc (ndot nroot "Barrier")); last first.
{ (* FIXME Really?? set_solver takes forever on "⊆ ⊤"?!? *)
move=>? _. exact I. }
apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
rewrite -(client_safe (ndot nroot "Heap" ) (ndot nroot "Barrier" )) //.
(* This, too, should be automated. *)
apply ndot_ne_disjoint. discriminate.
Qed.
Print Assumptions client_safe_closed.
End ClosedProofs.
...@@ -82,12 +82,12 @@ Section ClosedProofs. ...@@ -82,12 +82,12 @@ Section ClosedProofs.
Instance: authG heap_lang Σ heapRA. Instance: authG heap_lang Σ heapRA.
Proof. split; try apply _. by exists 1%nat. Qed. Proof. split; try apply _. by exists 1%nat. Qed.
Lemma heap_e_hoare σ : {{ ownP σ : iProp }} heap_e {{ λ v, v = '2 }}. Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ λ v, v = '2 }}.
Proof. Proof.
apply ht_alt. rewrite (heap_alloc nroot); last by rewrite nclose_nroot. apply ht_alt. rewrite (heap_alloc nroot); last by rewrite nclose_nroot.
apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l. apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
rewrite -heap_e_spec; first by eauto with I. by rewrite nclose_nroot. rewrite -heap_e_spec; first by eauto with I. by rewrite nclose_nroot.
Qed. Qed.
Print Assumptions heap_e_hoare. Print Assumptions heap_e_closed.
End ClosedProofs. End ClosedProofs.
From prelude Require Export functions.
From algebra Require Export iprod. From algebra Require Export iprod.
From program_logic Require Export pviewshifts. From program_logic Require Export pviewshifts.
From program_logic Require Import ownership. From program_logic Require Import ownership.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment