Commit 4d86571d authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Work.

parent 0fedd453
......@@ -4,28 +4,24 @@ From iris.algebra Require Import excl auth.
From iris.base_logic.lib Require Import auth.
Set Default Proof Using "Type".
Definition exclUR (A : ofeT) : ucmraT :=
optionUR (exclR A).
Class auth_exclG (A : ofeT) (Σ : gFunctors) := AuthExclG {
exclG_authG :> inG Σ (authR (optionUR (exclR A)));
}.
Class auth_exclG (A : ofeT) (Σ :gFunctors) :=
AuthExclG {
exclG_authG :> authG Σ (exclUR A);
}.
Definition auth_exclΣ (F : cFunctor) `{!cFunctorContractive F} : gFunctors :=
#[GFunctor (authRF (optionURF (exclRF F)))].
Definition auth_exclΣ (A : ofeT) : gFunctors :=
#[GFunctor (authR (exclUR A))].
Instance subG_auth_exclG (F : cFunctor) `{!cFunctorContractive F} {Σ} :
subG (auth_exclΣ F) Σ auth_exclG (F (iPreProp Σ)) Σ.
Proof. solve_inG. Qed.
Instance subG_auth_exclG (A : ofeT) {Σ} :
subG (auth_exclΣ A) Σ (auth_exclG A) Σ.
Proof. (* TODO: RK fix this *) Admitted.
Definition to_auth_excl {A : ofeT} (a : A) : exclUR A :=
Definition to_auth_excl {A : ofeT} (a : A) : option (excl A) :=
Excl' a.
Instance: Params (@to_auth_excl) 1.
Section auth_excl_ofe.
Context {A : ofeT}.
Global Instance to_auth_excl_ne : NonExpansive (@to_auth_excl A).
Proof. solve_proper. Qed.
......@@ -36,15 +32,25 @@ End auth_excl_ofe.
Section auth_excl.
Context `{!auth_exclG A Σ}.
Implicit Types x y : A.
Lemma to_auth_excl_valid x y :
( to_auth_excl x to_auth_excl y) - (x y : iProp Σ).
Proof.
iIntros "Hvalid".
iDestruct (auth_validI with "Hvalid") as "[Hy Hvalid]"; simpl.
iDestruct "Hy" as ([z|]) "Hy"; last first.
- by rewrite left_id right_id_L bi.option_equivI /= excl_equivI.
- iRewrite "Hy" in "Hvalid".
by rewrite left_id uPred.option_validI /= excl_validI /=.
Qed.
Lemma excl_eq γ x y :
own γ ( to_auth_excl y) - own γ ( to_auth_excl x) - x y.
own γ ( to_auth_excl x) - own γ ( to_auth_excl y) - x y.
Proof.
iIntros "Hauth Hfrag".
iDestruct (own_valid_2 with "Hauth Hfrag") as %Hvalid.
apply auth_valid_discrete_2 in Hvalid.
destruct Hvalid as [Hincl _].
by apply Excl_included in Hincl.
iDestruct (own_valid_2 with "Hauth Hfrag") as "Hvalid".
iDestruct (to_auth_excl_valid with "Hvalid") as "$".
Qed.
Lemma excl_update γ x y z :
......@@ -56,7 +62,6 @@ Section auth_excl.
{ eapply (auth_update _ _ (to_auth_excl z) (to_auth_excl z)).
eapply option_local_update.
eapply exclusive_local_update. done. }
rewrite own_op.
done.
by rewrite own_op.
Qed.
End auth_excl.
......@@ -61,6 +61,10 @@ Class chanG Σ := {
chanG_lockG :> lockG Σ;
chanG_authG :> auth_exclG (listC valC) Σ;
}.
Definition chanΣ : gFunctors :=
#[ lockΣ; auth_exclΣ (constCF (listC valC)) ].
Instance subG_chanΣ {Σ} : subG chanΣ Σ chanG Σ.
Proof. solve_inG. Qed.
Section channel.
Context `{!heapG Σ, !chanG Σ} (N : namespace).
......@@ -164,7 +168,7 @@ Section channel.
wp_load. wp_apply (lsnoc_spec with "Hlvs"). iIntros (lhd' Hlvs).
wp_bind (_ <- _)%E.
iMod "HΦ" as (vs') "[Hchan HΦ]".
iDestruct (excl_eq with "Hvs Hchan") as %->%leibniz_equiv.
iDestruct (excl_eq with "Hvs Hchan") as %<-%leibniz_equiv.
iMod (excl_update _ _ _ (vs ++ [v]) with "Hvs Hchan") as "[Hvs Hchan]".
wp_store. iMod ("HΦ" with "Hchan") as "HΦ".
iModIntro.
......@@ -193,7 +197,7 @@ Section channel.
wp_bind (! _)%E.
iMod "HΦ" as (vs') "[Hchan HΦ]".
wp_load.
iDestruct (excl_eq with "Hvs Hchan") as %->%leibniz_equiv.
iDestruct (excl_eq with "Hvs Hchan") as %<-%leibniz_equiv.
destruct vs as [|v vs]; simpl.
- iDestruct "Hlvs" as %->.
iDestruct "HΦ" as "[HΦ _]".
......
......@@ -9,9 +9,14 @@ From iris.base_logic Require Import invariants.
Class logrelG Σ := {
logrelG_channelG :> chanG Σ;
logrelG_authG :> auth_exclG (stypeC (laterC (iProp Σ))) Σ;
logrelG_authG :> auth_exclG (laterC (stypeC (iPreProp Σ))) Σ;
}.
Definition logrelΣ :=
#[ chanΣ ; GFunctor (authRF (optionURF (exclRF (laterCF (stypeCF idCF))))) ].
Instance subG_chanΣ {Σ} : subG logrelΣ Σ logrelG Σ.
Proof. intros [??%subG_auth_exclG]%subG_inv. constructor; apply _. Qed.
Section logrel.
Context `{!heapG Σ, !lockG Σ} (N : namespace).
Context `{!logrelG Σ}.
......@@ -25,7 +30,7 @@ Section logrel.
}.
Definition to_stype_auth_excl (st : stype (iProp Σ)) :=
to_auth_excl (stype_map Next st).
to_auth_excl (Next (stype_map iProp_unfold st)).
Definition st_own (γ : st_name) (s : side) (st : stype (iProp Σ)) : iProp Σ :=
own (side_elim s st_l_name st_r_name γ)
......@@ -38,19 +43,16 @@ Section logrel.
Lemma st_excl_eq γ s st st' :
st_ctx γ s st - st_own γ s st' - (st st').
Proof.
iIntros "Hauth Hfrag".
iDestruct (own_valid_2 with "Hauth Hfrag") as %Hvalid.
apply auth_valid_discrete_2 in Hvalid.
destruct Hvalid as [Hincl _].
apply Excl_included in Hincl.
destruct st, st'; simpl in Hincl.
- eauto.
- inversion Hincl.
- inversion Hincl.
- inversion Hincl; subst.
admit.
Admitted.
iDestruct (own_valid_2 with "Hauth Hfrag") as "Hvalid".
iDestruct (to_auth_excl_valid with "Hvalid") as "Hvalid".
iDestruct (bi.later_eq_1 with "Hvalid") as "Hvalid"; iNext.
assert ( st : stype (iProp Σ),
stype_map iProp_fold (stype_map iProp_unfold st) st) as help.
{ intros st''. rewrite -stype_fmap_compose -{2}(stype_fmap_id st'').
apply stype_map_ext=> P. by rewrite /= iProp_fold_unfold. }
rewrite -{2}(help st). iRewrite "Hvalid". by rewrite help.
Qed.
Lemma st_excl_update γ s st st' st'' :
st_ctx γ s st - st_own γ s st' ==
......@@ -74,9 +76,16 @@ Section logrel.
| _ => False
end
end%I.
Arguments st_eval : simpl nomatch.
Global Instance st_eval_ne : NonExpansive2 (st_eval vs).
Proof.
intros vs n. induction vs as [|v vs IH]; [solve_proper|].
destruct 2 as [|[] ????? Hst]=> //=. f_equiv. solve_proper. by apply IH, Hst.
Qed.
Lemma st_eval_send (P : val -> iProp Σ) st l str v :
P v - st_eval l (TSR Send P st) str - st_eval (l ++ [v]) (st v) str.
P v - st_eval l (TSR Send P st) str - st_eval (l ++ [v]) (st v) str.
Proof.
iIntros "HP".
iRevert (str).
......@@ -189,48 +198,18 @@ Section logrel.
iMod (st_excl_update _ _ _ _ (st v) with "Hstla Hstlf")
as "[Hstla Hstlf]".
iMod ("Hinvstep" with "[-Hstlf]") as "_".
{
iNext.
iDestruct (stype_equivI with "Heq") as "Heq'".
{ iNext.
iExists _,_,_,_. iFrame.
iLeft.
iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]".
- iSplit=> //.
iApply (st_eval_send with "HP").
destruct stl.
+ iDestruct "Heq'" as %Heq'. inversion Heq'.
+ iDestruct "Heq'" as "[Ha [HP Hst]]".
iDestruct "Ha" as %->.
admit. (* Rewrite! *)
- destruct r.
iSplit=> //.
simpl.
iDestruct (stype_equivI with "Heval") as "Heval".
destruct stl.
+ iDestruct "Heq'" as %Heq'. inversion Heq'.
+ destruct str.
* simpl. iApply "Heval".
* simpl.
iDestruct "Heq'" as (Ha) "[HPeq Hsteq]".
iDestruct "Heval" as (Ha') "[HPeq' Hsteq']".
subst. simpl.
iSpecialize ("HPeq" $!v).
iSpecialize ("HPeq'" $!v).
iSplitL "HPeq' HP".
iRewrite "HPeq'". iRewrite "HPeq". iApply "HP".
iSpecialize ("Hsteq" $!v).
iSpecialize ("Hsteq'" $!v).
iRewrite "Hsteq'". iRewrite "Hsteq".
rewrite (involutive (st v)).
done.
+ simpl. destruct stl.
* iDestruct "Heq'" as %Heq'. inversion Heq'.
* iDestruct "Heq'" as (Ha) "Heq'".
rewrite Ha.
iDestruct "Heval" as %Heval. inversion Heval.
}
iModIntro. iFrame "Hcctx ∗ Hinv".
- admit. (* Converse case *)
by iRewrite -"Heq".
- iRewrite "Heq" in "Heval". destruct r as [|vr r]=> //.
iSplit; first done. simpl.
iRewrite "Heval". simpl. iFrame "HP". by rewrite involutive. }
iModIntro. iFrame. rewrite /is_st. auto.
-
Admitted.
Lemma send_st_spec st γ c s (P : val iProp Σ) v :
......
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