Skip to content
Snippets Groups Projects
Commit f7487fba authored by Jonas Kastberg's avatar Jonas Kastberg
Browse files

WIP: proto_model version with unrolled RDE

parent 1888d5fe
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
multris/channel/proto_model.v
+ 98
− 121
View file @ f7487fba
......@@ -34,6 +34,7 @@ The defined functions on the type [proto] are:
a given protocol.
- [proto_app], which appends two protocols [p1] and [p2], by substituting
all terminations [END] in [p1] with [p2]. *)
From stdpp Require Import gmap.
From iris.algebra Require Import gmap.
From iris.base_logic Require Import base_logic.
From iris.proofmode Require Import proofmode.
......@@ -62,187 +63,154 @@ Module Export action.
Proof. by intros [[]]. Qed.
End action.
Notation proto_aux V PROP A :=
(gmap action (V -d> laterO A -n> PROP)).
Notation proto_auxO V PROP A :=
(gmapO actionO (V -d> later A -n> PROP)).
(* Notation proto_auxOF V PROP := *)
(* (gmapOF actionO ((V -d> ▶ ∙ -n> PROP))). *)
(* Definition proto_auxO (V : Type) (PROP : ofe) (A : ofe) : ofe := *)
(* (gmapO actionO (V -d> laterO A -n> PROP)). *)
Definition proto_auxOF (V : Type) (PROP : ofe) : oFunctor :=
(gmapO actionO (V -d> laterO A -n> PROP)).
Definition proto_auxOF V PROP :=
(gmapOF actionO ((V -d> ▶ ∙ -n> PROP))).
Definition proto_result (V : Type) := result_2 (proto_auxOF V).
Definition proto (V : Type) (PROPn PROP : ofe) `{!Cofe PROPn, !Cofe PROP} : ofe :=
Definition pre_protoO (V : Type) (PROPn PROP : ofe) `{!Cofe PROPn, !Cofe PROP} : ofe :=
solution_2_car (proto_result V) PROPn _ PROP _.
Global Instance pre_proto_cofe {V} `{!Cofe PROPn, !Cofe PROP} : Cofe (pre_protoO V PROPn PROP).
Proof. apply _. Qed.
Definition protoO (V : Type) (PROPn PROP : ofe) `{!Cofe PROPn, !Cofe PROP} : ofe :=
proto_auxO V PROP (pre_protoO V PROP PROPn).
Global Instance protoO_cofe {V} `{!Cofe PROPn, !Cofe PROP} : Cofe (protoO V PROPn PROP).
Proof. apply _. Qed.
Lemma protoO_iso {V} `{!Cofe PROPn, !Cofe PROP} :
ofe_iso (protoO V PROPn PROP) (pre_protoO V PROPn PROP).
Proof. apply proto_result. Qed.
Definition proto (V : Type) (PROPn PROP : ofe) `{!Cofe PROPn, !Cofe PROP} : ofe :=
proto_aux V PROP (pre_protoO V PROP PROPn).
Global Instance proto_cofe {V} `{!Cofe PROPn, !Cofe PROP} : Cofe (proto V PROPn PROP).
Proof. apply _. Qed.
Lemma proto_iso {V} `{!Cofe PROPn, !Cofe PROP} :
ofe_iso (proto_auxO V PROP (proto V PROP PROPn)) (proto V PROPn PROP).
ofe_iso (proto V PROPn PROP) (pre_protoO V PROPn PROP).
Proof. apply proto_result. Qed.
Definition proto_fold {V} `{!Cofe PROPn, !Cofe PROP} :
proto_auxO V PROP (proto V PROP PROPn) -n> proto V PROPn PROP := ofe_iso_1 proto_iso.
Definition proto_unfold {V} `{!Cofe PROPn, !Cofe PROP} :
proto V PROPn PROP -n> proto_auxO V PROP (proto V PROP PROPn) := ofe_iso_2 proto_iso.
proto V PROPn PROP -n> pre_protoO V PROPn PROP := ofe_iso_1 proto_iso.
Definition proto_fold {V} `{!Cofe PROPn, !Cofe PROP} :
pre_protoO V PROPn PROP -n> proto V PROPn PROP := ofe_iso_2 proto_iso.
Lemma proto_fold_unfold {V} `{!Cofe PROPn, !Cofe PROP} (p : proto V PROPn PROP) :
proto_fold (proto_unfold p) ≡ p.
Proof. apply (ofe_iso_12 proto_iso). Qed.
Proof. apply (ofe_iso_21 proto_iso). Qed.
Lemma proto_unfold_fold {V} `{!Cofe PROPn, !Cofe PROP}
(p : proto_auxO V PROP (proto V PROP PROPn)) :
(p : pre_protoO V PROP PROPn) :
proto_unfold (proto_fold p) ≡ p.
Proof. apply (ofe_iso_21 proto_iso). Qed.
(* Derived laws *)
Section internal_eq_derived.
Context {PROP : bi} `{!BiInternalEq PROP}.
Context `{Countable K} {A : ofe}.
Implicit Types P : PROP.
(* Force implicit argument PROP *)
Notation "P ⊢ Q" := (P ⊢@{PROP} Q).
Notation "P ⊣⊢ Q" := (P ⊣⊢@{PROP} Q).
Lemma gmap_equivI (m1 m2 : gmap K A) :
m1 ≡ m2 ⊣⊢ ∀ i, m1 !! i ≡ m2 !! i.
Proof. Admitted.
Lemma gmap_union_equiv_eqI (m m1 m2 : gmap K A) :
m ≡ m1 ∪ m2 ⊣⊢ ∃ m1' m2', ⌜ m = m1' ∪ m2' ⌝ ∧ m1' ≡ m1 ∧ m2' ≡ m2.
Proof. Admitted.
Lemma gmap_singleton_equivI (k1 k2 : K) (a1 a2 : A) :
{[ k1 := a1 ]} ≡ {[ k2 := a2 ]} ⊣⊢ ⌜ k1 = k2 ⌝ ∧ a1 ≡ a2.
Proof. Admitted.
End internal_eq_derived.
Proof. apply (ofe_iso_12 proto_iso). Qed.
Global Instance subseteq_proper `{Countable K} {A:Type} `{Equiv A} :
Proper ((≡@{gmap K A}) ==> (≡@{gmap K A}) ==> iff) (⊆).
Proof. Admitted.
Global Instance subset_proper `{Countable K} {A:Type} `{Equiv A} :
Proper ((≡@{gmap K A}) ==> (≡@{gmap K A}) ==> iff) (⊂).
Proof. solve_proper. Qed.
Definition proto_end {V} `{!Cofe PROPn, !Cofe PROP} : proto V PROPn PROP :=
proto_fold ∅ .
Definition proto_end {V} `{!Cofe PROPn, !Cofe PROP} : proto V PROPn PROP := ∅ .
Definition proto_message {V} `{!Cofe PROPn, !Cofe PROP} (a : action)
(m : V → laterO (proto V PROP PROPn) -n> PROP) : proto V PROPn PROP :=
proto_fold {[a := m]}.
(m : V -d> later (proto V PROP PROPn) -n> PROP) : proto V PROPn PROP :=
({[a := (λ v, m v ◎ laterO_map proto_fold)]}).
Definition proto_union {V} `{!Cofe PROPn, !Cofe PROP} (p1 p2 : proto V PROPn PROP) : proto V PROPn PROP :=
proto_fold (((proto_unfold p1):gmap _ _) ∪ (proto_unfold p2)).
(p1:gmap _ _) ∪ p2.
Global Instance proto_message_ne {V} `{!Cofe PROPn, !Cofe PROP} a n :
Proper (pointwise_relation V (dist n) ==> dist n)
(proto_message (PROPn:=PROPn) (PROP:=PROP) a).
Proof.
intros c1 c2 Hc. rewrite /proto_message. f_equiv. by apply insert_ne.
intros c1 c2 Hc. rewrite /proto_message.
apply insert_ne; [|done]. solve_proper.
Qed.
(* TODO: Why does unification algorithm fail here? *)
Global Instance proto_message_proper {V} `{!Cofe PROPn, !Cofe PROP} a :
Proper (pointwise_relation V (≡) ==> (≡))
(proto_message (PROPn:=PROPn) (PROP:=PROP) a).
Proof. intros c1 c2 Hc. rewrite /proto_message. f_equiv. by apply: insert_proper. Qed.
Proof. intros c1 c2 Hc. rewrite /proto_message. apply: insert_proper; [|done]. solve_proper.
Qed.
Global Instance proto_union_ne {V} `{!Cofe PROPn, !Cofe PROP} n :
Proper ((dist n) ==> (dist n) ==> dist n)
(proto_union (V:=V) (PROPn:=PROPn) (PROP:=PROP)).
Proof.
intros p11 p12 Hp1 p21 p22 Hp2. rewrite /proto_union. by do 3 f_equiv.
intros p11 p12 Hp1 p21 p22 Hp2. rewrite /proto_union. by f_equiv.
Qed.
(* TODO: Why does unification algorithm fail here? *)
Global Instance proto_union_proper {V} `{!Cofe PROPn, !Cofe PROP} :
Proper ((≡) ==> (≡) ==> (≡))
(proto_union (V:=V) (PROPn:=PROPn) (PROP:=PROP)).
Proof. intros p11 p12 Hp1 p21 p22 Hp2. rewrite /proto_union. solve_proper. Qed.
Proof.
intros p11 p12 Hp1 p21 p22 Hp2. rewrite /proto_union. by f_equiv.
Qed.
(* TODO: Missing Proper stuff *)
(* Should hold in the same way map_ind holds *)
Lemma proto_ind {V} `{!Cofe PROPn, !Cofe PROP} (P : proto V PROPn PROP → Prop) :
Proper ((≡) ==> impl) P →
P proto_end → (∀ i x p, proto_unfold p !! i ≡ None → P p → P (proto_union (proto_message i x) p)) → ∀ m, P m.
P proto_end → (∀ i x p, p !! i ≡ None → P p → P (proto_union (proto_message i x) p)) → ∀ m, P m.
Proof.
intros HP ? Hins m'.
assert (∃ m, m = proto_unfold m') as [m Hm].
{ eexists _. done. }
revert Hm. revert m'.
intros HP ? Hins m.
induction (map_wf m) as [m _ IH].
intros m' Hm.
destruct (map_choose_or_empty m) as [(i&x&?)| H'].
{
assert (m' ≡ proto_union (proto_message i x) (proto_fold (delete i (proto_unfold m'))))
as Heq.
assert (m ≡ proto_union (proto_message i (λ v, x v ◎ laterO_map proto_unfold)) (delete i m)) as Heq.
{
rewrite -Hm /proto_union /proto_message !proto_unfold_fold -(proto_fold_unfold m').
f_equiv. rewrite -Hm -insert_union_singleton_l. by rewrite insert_delete.
}
rewrite /proto_message /proto_union.
rewrite -insert_union_singleton_l.
intros i'.
(* TODO: Simplify *)
destruct (decide (i=i')) as [->|].
{ rewrite H0. rewrite lookup_insert. f_equiv.
intros v.
intros x''.
simpl.
rewrite -later_map_compose.
simpl. f_equiv.
destruct x''.
rewrite later_map_Next. f_equiv.
simpl. rewrite proto_unfold_fold. done. }
rewrite lookup_insert_ne; [|done].
by rewrite lookup_delete_ne. }
rewrite Heq.
apply Hins.
{ rewrite -Hm lookup_proper; [|apply proto_unfold_fold]. by rewrite lookup_delete. }
eapply IH; [|done]. rewrite -Hm (proto_unfold_fold (delete i m)).
by apply: delete_subset.
{ by rewrite lookup_delete. }
eapply IH. by apply: delete_subset.
}
rewrite /proto_end in H.
rewrite Hm in H'. rewrite -H' in H. by rewrite -(proto_fold_unfold m').
by rewrite -H' in H.
Qed.
Global Instance proto_inhabited {V} `{!Cofe PROPn, !Cofe PROP} :
Inhabited (proto V PROPn PROP) := populate proto_end.
Lemma proto_message_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe PROP} a1 a2 m1 m2 :
proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a1 m1 ≡ proto_message a2 m2
⊣⊢@{SPROP} ⌜ a1 = a2 ⌝ ∧ (∀ v p', m1 v p' ≡ m2 v p').
Proof.
trans (proto_unfold (proto_message a1 m1) ≡ proto_unfold (proto_message a2 m2) : SPROP)%I.
{ iSplit.
- iIntros "Heq". by iRewrite "Heq".
- iIntros "Heq". rewrite -{2}(proto_fold_unfold (proto_message _ _)).
iRewrite "Heq". by rewrite proto_fold_unfold. }
rewrite /proto_message !proto_unfold_fold.
rewrite gmap_singleton_equivI /=.
rewrite discrete_fun_equivI.
by setoid_rewrite ofe_morO_equivI.
Qed.
Proof. Admitted.
Lemma proto_message_end_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe PROP} a m :
proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a m ≡ proto_end ⊢@{SPROP} False.
Proof.
trans (proto_unfold (proto_message a m) ≡ proto_unfold proto_end : SPROP)%I.
{ iIntros "Heq". by iRewrite "Heq". }
rewrite /proto_message !proto_unfold_fold.
Admitted.
Proof. Admitted.
Lemma proto_end_message_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe PROP} a m :
proto_end ≡ proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a m ⊢@{SPROP} False.
Proof. by rewrite internal_eq_sym proto_message_end_equivI. Qed.
(** Functor *)
Program Definition proto_map_aux {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(g : PROP -n> PROP') (rec : proto V PROP' PROPn' -n> proto V PROP PROPn) :
proto V PROPn PROP -n> proto V PROPn' PROP' := λne p,
(* fmap (λ (m:proto V PROPn PROP), (λ v, g ◎ m v ◎ laterO_map rec)) (proto_unfold p). *)
(* proto_fold $ gmap_fmap _ _ (λ m, (λ v, g ◎ m v ◎ laterO_map rec)) (proto_unfold p). *)
proto_fold $ fmap (λ m, (λ v, g ◎ m v ◎ laterO_map rec)) (proto_unfold p).
proto V PROPn PROP -n> proto V PROPn' PROP' := λne p,
(λ m, λ v, g ◎ m v ◎ laterO_map proto_unfold ◎ laterO_map rec ◎ laterO_map proto_fold) <$> p.
Next Obligation.
intros V PROPn ? PROPn' ? PROP ? PROP' ? g rec n p1 p2 Hp.
f_equiv. simpl.
apply (_ : NonExpansive proto_unfold) in Hp.
Admitted.
(* TODO: Needs non expansiveness of fmap *)
(* (* Admitted. *) *)
(* apply map_fmap_ne. *)
(* apply gmap_fmap_ne_ext. *)
(* apply proto_elim_ne=> // a m1 m2 Hm. by repeat f_equiv. *)
(* Qed. *)
apply: (map_fmap_ne _ n _ p1 p2); [|done].
solve_proper.
Qed.
Global Instance proto_map_aux_contractive {V}
`{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'} (g : PROP -n> PROP') :
Contractive (proto_map_aux (V:=V) (PROPn:=PROPn) (PROPn':=PROPn') g).
Proof. Admitted.
(* intros n rec1 rec2 Hrec p. simpl. apply proto_elim_ne=> // a m1 m2 Hm. *)
(* f_equiv=> v p' /=. do 2 f_equiv; [done|]. *)
(* apply Next_contractive; by dist_later_intro as n' Hn'. *)
(* Qed. *)
Proof.
intros n p1 p2 Hp. rewrite /proto_map_aux.
intros p. simpl.
apply: gmap_fmap_ne_ext.
intros i x Hix v. f_equiv. f_equiv. f_contractive.
done.
Qed.
Definition proto_map_aux_2 {V}
`{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
......@@ -280,28 +248,37 @@ Lemma proto_map_end {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
proto_map (V:=V) gn g proto_end ≡ proto_end.
Proof.
rewrite proto_map_unfold /proto_map_aux /=.
(* pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn) (PROP:=PROP) ∅) as Hfold. *)
rewrite /proto_end. f_equiv.
rewrite -(fmap_empty (λ (m : V → laterO (proto V PROP PROPn) -n> PROP) (v : V),
g ◎ m v ◎ laterO_map (proto_map g gn))).
f_equiv.
(* proto_unfold_fold not working ??? *)
Admitted.
done.
Qed.
Lemma proto_map_message {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(gn : PROPn' -n> PROPn) (g : PROP -n> PROP') a m :
proto_map (V:=V) gn g (proto_message a m)
≡ proto_message a (λ v, g ◎ m v ◎ laterO_map (proto_map g gn)).
Proof.
rewrite proto_map_unfold /proto_map_aux /=.
rewrite /proto_message. f_equiv.
Admitted.
rewrite /proto_message.
rewrite fmap_insert. rewrite fmap_empty.
intros a'. destruct (decide (a=a')).
{ subst. rewrite !lookup_insert.
f_equiv.
intros v. f_equiv. f_equiv.
intros x. simpl. f_equiv. f_equiv.
intros y. simpl. rewrite proto_fold_unfold. done.
}
by rewrite !lookup_insert_ne.
Qed.
Lemma proto_map_union {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(gn : PROPn' -n> PROPn) (g : PROP -n> PROP') p1 p2 :
proto_map (V:=V) gn g (proto_union p1 p2)
≡ proto_union (proto_map gn g p1) (proto_map gn g p2).
Proof.
rewrite proto_map_unfold /proto_map_aux /=.
Admitted.
rewrite proto_map_unfold /proto_map_aux /=.
rewrite proto_map_unfold /proto_map_aux /=.
rewrite !/proto_union.
rewrite !map_fmap_union.
f_equiv.
Qed.
Lemma proto_map_ne {V}
`{Hcn:!Cofe PROPn, Hcn':!Cofe PROPn', Hc:!Cofe PROP, Hc':!Cofe PROP'}
......@@ -350,7 +327,7 @@ Lemma proto_map_compose {V}
(gn1 : PROPn'' -n> PROPn') (gn2 : PROPn' -n> PROPn)
(g1 : PROP -n> PROP') (g2 : PROP' -n> PROP'') (p : proto V PROPn PROP) :
proto_map (gn2 ◎ gn1) (g2 ◎ g1) p ≡ proto_map gn1 g2 (proto_map gn2 g1 p).
Proof.
Proof.
apply equiv_dist=> n. revert PROPn Hcn PROPn' Hcn' PROPn'' Hcn''
PROP Hc PROP' Hc' PROP'' Hc'' gn1 gn2 g1 g2 p.
induction (lt_wf n) as [n _ IH]=> PROPn ? PROPn' ? PROPn'' ?
......@@ -389,7 +366,7 @@ Qed.
Global Instance protoOF_contractive (V : Type) (Fn F : oFunctor)
`{!∀ A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car Fn A B)}
`{!∀ A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F A B)} :
oFunctorContractive Fn → oFunctorContractive F →
oFunctorContractive Fn → oFunctorContractive F →
oFunctorContractive (protoOF V Fn F).
Proof.
intros HFn HF A1 ? A2 ? B1 ? B2 ? n f g Hfg p; simpl in *.
......
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