Commit 77eb6feb authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Working.

parent 87d468e8
......@@ -4,29 +4,29 @@ From iris.algebra Require Import excl auth.
From iris.base_logic.lib Require Import auth.
Set Default Proof Using "Type".
Definition exclUR (A : Type) : ucmraT :=
optionUR (exclR (leibnizC A)).
Definition exclUR (A : ofeT) : ucmraT :=
optionUR (exclR A).
Class auth_exclG (A : Type) (Σ :gFunctors) :=
Class auth_exclG (A : ofeT) (Σ :gFunctors) :=
AuthExclG {
exclG_authG :> authG Σ (exclUR A);
}.
Definition auth_exclΣ (A : Type) : gFunctors :=
Definition auth_exclΣ (A : ofeT) : gFunctors :=
#[GFunctor (authR (exclUR A))].
Instance subG_auth_exclG (A : Type) {Σ} :
Instance subG_auth_exclG (A : ofeT) {Σ} :
subG (auth_exclΣ A) Σ (auth_exclG A) Σ.
Proof. solve_inG. Qed.
Proof. (* TODO: RK fix this *) Admitted.
Definition to_auth_excl {A : Type} (a : A) : exclUR A :=
Excl' (a: leibnizC A).
Definition to_auth_excl {A : ofeT} (a : A) : exclUR A :=
Excl' a.
Section auth_excl.
Context `{!auth_exclG A Σ}.
Lemma excl_eq γ x y :
own γ ( to_auth_excl y) - own γ ( to_auth_excl x) - x = y%I.
own γ ( to_auth_excl y) - own γ ( to_auth_excl x) - x y.
Proof.
iIntros "Hauth Hfrag".
iDestruct (own_valid_2 with "Hauth Hfrag") as %Hvalid.
......@@ -51,5 +51,4 @@ Section auth_excl.
rewrite own_op.
done.
Qed.
End auth_excl.
......@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl auth.
From iris.algebra Require Import excl auth list.
From iris.base_logic.lib Require Import auth.
From iris.heap_lang.lib Require Import spin_lock.
From osiris Require Import list.
......@@ -57,8 +57,13 @@ Definition recv : val :=
| NONE => "go" "c" "s"
end.
Class chanG Σ := {
chanG_lockG :> lockG Σ;
chanG_authG :> auth_exclG (listC valC) Σ;
}.
Section channel.
Context `{!heapG Σ, !lockG Σ, !auth_exclG (list val) Σ} (N : namespace).
Context `{!heapG Σ, !chanG Σ} (N : namespace).
Definition is_list_ref (l : val) (xs : list val) : iProp Σ :=
( l':loc, hd : val, l = #l' l' hd is_list hd xs)%I.
......
......@@ -154,15 +154,13 @@ Lemma lsnoc_spec hd vs v :
Proof.
iIntros (Φ Hvs) "HΦ".
iInduction vs as [|v' vs] "IH" forall (hd Hvs Φ).
- inversion Hvs.
subst.
- simplify_eq/=.
wp_rec.
wp_pures.
wp_lam.
wp_pures.
iApply "HΦ". simpl. eauto.
- inversion Hvs as [vs' [Hhd Hvs']]; subst.
eauto.
- destruct Hvs as [vs' [-> Hvs']].
wp_rec.
wp_pures.
wp_bind (lsnoc vs' v).
......@@ -175,5 +173,4 @@ Proof.
eauto.
iApply "HΦ".
Qed.
End lists.
\ No newline at end of file
......@@ -7,6 +7,11 @@ From osiris Require Import typing auth_excl channel.
From iris.algebra Require Import list auth excl.
From iris.base_logic Require Import invariants.
Class logrelG Σ := {
logrelG_channelG : chanG Σ;
logrelG_authG : auth_exclG (stype (later (iProp Σ))) Σ;
}.
Section logrel.
Context `{!heapG Σ, !lockG Σ} (N : namespace).
Context `{!auth_exclG (list val) Σ}.
......@@ -58,7 +63,7 @@ Section logrel.
constructor=> //.
Qed.
Definition inv_st (γ :st_name) (c : val) : iProp Σ :=
Definition inv_st (γ : st_name) (c : val) : iProp Σ :=
( l r stl str,
chan_own (st_c_name γ) Left l
chan_own (st_c_name γ) Right r
......@@ -216,7 +221,7 @@ Section logrel.
iDestruct "Hinv'" as "[Hinv' Hinvstep]".
iDestruct "Hinv'" as
(l r stl str) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')".
iModIntro.
iExists (side_elim s l r). iModIntro.
destruct s.
- iExists _.
iIntros "{$Hcrf} !>".
......
From iris.heap_lang Require Export lang.
Require Import FunctionalExtensionality.
Class Involutive {A} (R : relation A) (f : A A) :=
involutive x : R (f (f x)) x.
Class Involutive {T} (f : T T) :=
involutive : t : T, t = f (f t).
Inductive side : Set :=
| Left
| Right.
Inductive side := Left | Right.
Instance side_inhabited : Inhabited side := populate Left.
Definition dual_side (s : side) : side :=
match s with Left => Right | Right => Left end.
Instance dual_side_involutive : Involutive (=) dual_side.
Proof. by intros []. Qed.
Inductive action := Send | Receive.
Instance action_inhabited : Inhabited action := populate Send.
Definition dual_action (a : action) : action :=
match a with Send => Receive | Receive => Send end.
Instance dual_action_involutive : Involutive (=) dual_action.
Proof. by intros []. Qed.
Inductive stype (A : Type) :=
| TEnd
| TSR (a : action) (P : val A) (st : val stype A).
Arguments TEnd {_}.
Arguments TSR {_} _ _ _.
Instance: Params (@TSR) 2.
Instance stype_inhabited A : Inhabited (stype A) := populate TEnd.
Fixpoint dual_stype {A} (st : stype A) :=
match st with
| TEnd => TEnd
| TSR a P st => TSR (dual_action a) P (λ v, dual_stype (st v))
end.
Instance: Params (@dual_stype) 1.
Section stype_ofe.
Context {A : ofeT}.
Inductive stype_equiv : Equiv (stype A) :=
| TEnd_equiv : TEnd TEnd
| TSR_equiv a P1 P2 st1 st2 :
pointwise_relation val () P1 P2
pointwise_relation val () st1 st2
TSR a P1 st1 TSR a P2 st2.
Existing Instance stype_equiv.
Instance dual_side_involutive : Involutive dual_side.
Proof. intros s; destruct s; eauto. Qed.
Inductive stype_dist' (n : nat) : relation (stype A) :=
| TEnd_dist : stype_dist' n TEnd TEnd
| TSR_dist a P1 P2 st1 st2 :
pointwise_relation val (dist n) P1 P2
pointwise_relation val (stype_dist' n) st1 st2
stype_dist' n (TSR a P1 st1) (TSR a P2 st2).
Instance stype_dist : Dist (stype A) := stype_dist'.
Inductive stype :=
| TEnd
| TSend (P : val Prop) (st : val stype)
| TRecv (P : val Prop) (st : val stype).
Definition stype_ofe_mixin : OfeMixin (stype A).
Proof.
split.
- intros st1 st2. rewrite /dist /stype_dist. split.
+ intros Hst n. induction Hst as [|a P1 P2 st1 st2 HP Hst IH]; constructor.
* intros v. apply equiv_dist, HP.
* intros v. apply IH.
+ revert st2. induction st1 as [|a P1 st1 IH]; intros [|a' P2 st2] Hst.
* constructor.
* feed inversion (Hst O).
* feed inversion (Hst O).
* feed inversion (Hst O); subst.
constructor.
** intros v. apply equiv_dist=> n. feed inversion (Hst n); subst; auto.
** intros v. apply IH=> n. feed inversion (Hst n); subst; auto.
- rewrite /dist /stype_dist. split.
+ intros st. induction st; constructor; repeat intro; auto.
+ intros st1 st2. induction 1; constructor; repeat intro; auto.
symmetry; auto.
+ admit.
- intros n st1 st2. induction 1; constructor; auto.
Admitted.
Canonical Structure stypeC : ofeT := OfeT (stype A) stype_ofe_mixin.
Instance stype_inhabited : Inhabited stype := populate TEnd.
Global Instance TSR_stype_ne a n :
Proper (pointwise_relation _ (dist n) ==> pointwise_relation _ (dist n) ==> dist n) (TSR a).
Proof. Admitted.
Global Instance TSR_stype_proper a :
Proper (pointwise_relation _ () ==> pointwise_relation _ () ==> ()) (TSR a).
Proof.
intros P1 P2 HP st1 st2 Hst. apply equiv_dist=> n.
by f_equiv; intros v; apply equiv_dist.
Qed.
Fixpoint dual_stype (st :stype) :=
Global Instance dual_stype_ne : NonExpansive dual_stype.
Proof. Admitted.
Global Instance dual_stype_proper : Proper (() ==> ()) dual_stype.
Proof. apply (ne_proper _). Qed.
Global Instance dual_stype_involutive : Involutive () dual_stype.
Proof.
intros st.
Admitted.
End stype_ofe.
Fixpoint stype_map {A B} (f : A B) (st : stype A) : stype B :=
match st with
| TEnd => TEnd
| TSend P st => TRecv P (λ v, dual_stype (st v))
| TRecv P st => TSend P (λ v, dual_stype (st v))
| TSR a P st => TSR a (λ v, f (P v)) (λ v, stype_map f (st v))
end.
Lemma stype_map_ext_ne {A} {B : ofeT} (f g : A B) (st : stype A) n :
( x, f x {n} g x) stype_map f st {n} stype_map g st.
Proof.
intros Hf. induction st; simpl.
Admitted.
Lemma stype_map_ext {A} {B : ofeT} (f g : A B) (st : stype A) :
( x, f x g x) stype_map f st stype_map g st.
Proof.
intros Hf. induction st; simpl.
Admitted.
Instance styope_map_ne {A B : ofeT} (f : A B) n:
Proper (dist n ==> dist n) f Proper (dist n ==> dist n) (stype_map f).
Proof.
intros Hf st1 st2. induction 1; simpl; constructor.
Admitted.
Lemma stype_fmap_id {A : ofeT} (st : stype A) : stype_map id st st.
Proof.
Admitted.
Check @list_fmap_compose.
Lemma stype_fmap_compose {A B C : ofeT} (f : A B) (g : B C) st :
stype_map (g f) st stype_map g (stype_map f st).
Proof.
Admitted.
Definition stypeC_map {A B} (f : A -n> B) : stypeC A -n> stypeC B :=
CofeMor (stype_map f : stypeC A stypeC B).
Instance stypeC_map_ne A B : NonExpansive (@stypeC_map A B).
Proof. intros n f g ? st. by apply stype_map_ext_ne. Qed.
Program Definition stypeCF (F : cFunctor) : cFunctor := {|
cFunctor_car A B := stypeC (cFunctor_car F A B);
cFunctor_map A1 A2 B1 B2 fg := stypeC_map (cFunctor_map F fg)
|}.
Next Obligation.
by intros F A1 A2 B1 B2 n f g Hfg; apply stypeC_map_ne, cFunctor_ne.
Qed.
Next Obligation.
intros F A B x. rewrite /= -{2}(stype_fmap_id x).
apply stype_map_ext=>y. apply cFunctor_id.
Qed.
Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -stype_fmap_compose.
apply stype_map_ext=>y; apply cFunctor_compose.
Qed.
Instance dual_stype_involutive : Involutive dual_stype.
Instance stypeCF_contractive F :
cFunctorContractive F cFunctorContractive (stypeCF F).
Proof.
intros st.
induction st => //; simpl;
assert (st = (λ v : val, dual_stype (dual_stype (st v)))) as Heq
by apply functional_extensionality => //;
rewrite -Heq => //.
by intros ? A1 A2 B1 B2 n f g Hfg; apply stypeC_map_ne, cFunctor_contractive.
Qed.
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