diff --git a/_CoqProject b/_CoqProject
index 700e7c386dddbe3cb9e220209bda79c7196039b7..16fda88572bd3a96b697c6dfcff9e4e6a38bbefd 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -21,6 +21,7 @@ theories/lang/new_delete.v
theories/lang/swap.v
theories/lang/lock.v
theories/lang/spawn.v
+theories/lang/arc_cmra.v
theories/lang/arc.v
theories/typing/base.v
theories/typing/lft_contexts.v
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index abcbd550b3e1219828e5cbad5bcd499547dc2701..92fc2278086f5a94b7883e41516839f80a210049 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -3,7 +3,7 @@ From iris.base_logic.lib Require Import invariants.
From iris.proofmode Require Import tactics.
From iris.bi Require Import fractional.
From iris.algebra Require Import excl csum frac auth agree.
-From lrust.lang Require Import notation new_delete.
+From lrust.lang Require Import notation new_delete arc_cmra.
From gpfsl.gps Require Import middleware protocols.
Set Default Proof Using "Type".
@@ -125,640 +125,6 @@ Definition try_unwrap_full : val :=
else #1
else #2.
-(* Lattice of sets with subseteq *)
-Program Canonical Structure gset_Lat (A: Type) `{Countable A} :=
- Make_Lat (gset A) (≡) subseteq union intersection
- _ _ _ _ _ _ _ _ _ _ _ _ _.
-Next Obligation. move => ???. by apply union_subseteq_l. Qed.
-Next Obligation. move => ???. by apply union_subseteq_r. Qed.
-Next Obligation. move => ???. by apply union_least. Qed.
-Next Obligation. move => ???. by apply intersection_subseteq_l. Qed.
-Next Obligation. move => ???. by apply intersection_subseteq_r. Qed.
-Next Obligation. move => ??????. by apply intersection_greatest. Qed.
-
-Instance gset_Lat_bot `{Countable A} : LatBottom (∅ : gset_Lat A).
-Proof. done. Qed.
-
-(** The CMRAs we need. *)
-
-(* This cmra tracks what the arc must have done by itself when it is the unique clone.
-
- Self here means that the cmra is updated when the caller moves its own counter,
- e.g. the strong arc modifying the strong counter, or the weak arc modifying
- the weak counter.
- For the strong counter, it tracks the actions: moving 1 to 0
- (the last release/drop), and 1 to 2 (the unique clone).
- For the weak counter, it tracks the self actions: moving 1 to -1 (locking),
- moving 1 to 0 (the last drop), and 1 to 2 (the unique clone).
-
- The authority should only be updated when having full fraction,
- i.e. the caller being unique. A persistent certificate is issued when the
- authority is updated. A fraction of the authority must have seen all certificates. *)
-Definition move_selfUR :=
- prodUR (authUR (optionUR (prodR fracR (agreeR (latC (gset_Lat time))))))
- (authUR (latUR (gset_Lat time))).
-
-(* This cmra tracks what the arc has asked the other to do, e.g., the weak arc
- asks the strong counter to increment when upgrading, or the strong arc asks
- the weak counter to increment when downgrading.
-
- The authority part is owned by the caller, and issue a certificate for
- the callee to store in its update. There can be multiple authorities,
- each is owned by one caller. A fraction of the authority can issue certificates,
- while only the full fraction authority is guaranteed to have seen all certificates. *)
-Definition move_otherUR :=
- prodUR (authUR (optionUR (prodR fracR (latR (gset_Lat time)))))
- (authUR (latUR (gset_Lat time))).
-
-(* This cmra tracks states of the weak counter:
- - (None, None) : no strong or weak arc, v = 0.
- - (None, Some Cinl (q,n)) : no strong arc, n weak arcs that use q permission,
- v = n.
- - (None, Some Cinr q) : no strong arc, no weak arc, the weak counter is locked
- with a payload of q from a strong arc, v = -1. This state is IMPOSSIBLE.
- - (Some 1, None) : some strong arcs, no weak arcs, v = 1.
- - (Some 1, Some Cinl (q,n)) : some strong arcs, n weak arcs that use q, v = S n.
- - (Some 1, Some Cinr q) : some strong arcs, no weak arc, the weak counter is
- locked with a payload of q from a strong arc, v = -1.
-*)
-
-Definition weak_stUR :=
- prodUR (optionUR fracR)
- (optionUR (csumR (prodR fracR positiveR) (prodR (exclR unitC) (agreeR fracC)))).
-
-(* This cmra tracks states of the strong counter:
- - None: no strong arc, v = 0.
- - Some (q,n): n strong arcs that took out q, v = n. *)
-Definition strong_stUR :=
- optionUR (prodR fracR positiveR).
-
-(* The final cmra has 5 components
- (strong arc states, weak arc states),
- (strong arc self, strong arc downgrade),
- (weak arc upgrade) *)
-Definition arcUR :=
- prodUR (prodUR (authUR strong_stUR) (authUR weak_stUR))
- (prodUR (prodUR move_selfUR move_otherUR) move_otherUR).
-
-Class arcG Σ := {
- ArcStG :> inG Σ arcUR;
- ArcPrt_gpsG :> gpsG Σ unitProtocol;
-}.
-Definition arcΣ : gFunctors := #[GFunctor arcUR; gpsΣ unitProtocol].
-Instance subG_arcΣ {Σ} : subG arcΣ Σ → arcG Σ.
-Proof. solve_inG. Qed.
-
-Definition Z_of_arcweak_st (st : weak_stUR) : Z :=
- match st with
- | (None, None) => 0
- | (Some _, None) => 1
- | (None, Some (Cinl (_, n))) => Zpos n
- | (Some _, Some (Cinl (_, n))) => Zpos n +1
- | (_, Some _) => -1
- end.
-
-Definition Z_of_arcstrong_st (st : strong_stUR) : Z :=
- match st with
- | None => 0
- | Some (_, n) => Zpos n
- end.
-
-
-Lemma strong_stUR_value st: 0 ≤ Z_of_arcstrong_st st.
-Proof. destruct st as [[]|]; simpl; lia. Qed.
-
-Lemma weak_stUR_value st: -1 ≤ Z_of_arcweak_st st.
-Proof. destruct st as [[|] [[[]| |]|]]; simpl; lia. Qed.
-
-Notation agown γ st := (⎡ own γ (st : arcUR) ⎤ : vProp _)%I.
-Notation awk_n st := ((ε, ◯ (st : weak_stUR)), ε).
-
-Section ArcGhost.
- Context `{inG Σ arcUR}.
- Local Notation vProp := (vProp Σ).
- Implicit Types (Mt Ut Dt: gset time).
-
- Definition StrongAuth γ (st : strong_stUR) :=
- agown γ ((● st, ε), ε).
- Definition StrongTok γ q :=
- agown γ ((◯ Some (q, xH), ε), ε).
- Definition StrongMoveAuth γ Mt :=
- agown γ (ε, (((● Some (1%Qp, to_agree $ to_latT Mt), ● to_latT Mt) : move_selfUR, ε), ε)).
- Definition StrMoves γ (q: frac) Mt :=
- agown γ (ε, (((◯ Some (q, to_agree $ to_latT Mt), ε) : move_selfUR, ε), ε)).
- Definition StrongDownAuth γ Dt :=
- agown γ (ε, ((ε, (● Some (1%Qp, to_latT Dt), ● to_latT Dt) : move_otherUR), ε)).
- Definition StrDowns γ (q: frac) Dt :=
- agown γ (ε, ((ε, (◯ Some (q, to_latT Dt), ε) : move_otherUR), ε)).
- Definition StrMoveCertS γ Mt : vProp :=
- agown γ (ε, (((ε, ◯ to_latT Mt) : move_selfUR, ε), ε)).
- Definition StrDownCertS γ Mt : vProp :=
- agown γ (ε, ((ε, (ε, ◯ to_latT Mt) : move_otherUR), ε)).
- Definition StrMoveCert γ t := StrMoveCertS γ {[t : time]}.
- Definition StrDownCert γ t := StrDownCertS γ {[t : time]}.
-
- Definition WeakAuth γ (st : weak_stUR) :=
- agown γ ((ε, ● st), ε).
- Definition WeakTok γ q :=
- agown γ ((ε, ◯ (ε, Some (Cinl (q, xH)))), ε).
- Definition WeakUpAuth γ Ut :=
- agown γ (ε, (ε, (● Some (1%Qp, to_latT Ut), ● to_latT Ut) : move_otherUR)).
- Definition WkUps γ (q: frac) Ut :=
- agown γ (ε, (ε, (◯ Some (q, to_latT Ut), ε) : move_otherUR)).
- Definition WkUpCertS γ Mt :=
- agown γ (ε, (ε, (ε, ◯ to_latT Mt) : move_otherUR)).
- Definition WkUpCert γ t := WkUpCertS γ {[t : time]}.
- Definition WkLock γ q :=
- agown γ (ε, ◯ (ε, Some $ Cinr (Excl(), to_agree q)),ε) .
-
- Global Instance StrMoveCertS_persistent γ Mt : Persistent (StrMoveCertS γ Mt).
- Proof. apply embed_persistent, own_core_persistent, pair_core_id; by apply _. Qed.
- Global Instance StrDownCertS_persistent γ Mt : Persistent (StrDownCertS γ Mt).
- Proof. apply embed_persistent, own_core_persistent, pair_core_id; by apply _. Qed.
- Global Instance WkUpCertS_persistent γ Mt : Persistent (WkUpCertS γ Mt).
- Proof. apply embed_persistent, own_core_persistent, pair_core_id; by apply _. Qed.
- Global Instance StrMoves_fractional γ Mt : Fractional (λ q, StrMoves γ q Mt).
- Proof.
- rewrite /Fractional => p q. rewrite -embed_sep -own_op.
- apply embed_proper, own.own_proper.
- apply pair_proper; [done|]. do 3 (apply pair_proper; [|done]). simpl.
- by rewrite -auth_frag_op -Some_op pair_op frac_op' agree_idemp.
- Qed.
- Global Instance StrMoves_asfractional γ q Mt :
- AsFractional (StrMoves γ q Mt) (λ q, StrMoves γ q Mt) q.
- Proof. split. done. apply _. Qed.
- Global Instance StrDowns_fractional γ Dt : Fractional (λ q, StrDowns γ q Dt).
- Proof.
- rewrite /Fractional => p q. rewrite -embed_sep -own_op.
- apply embed_proper, own.own_proper.
- apply pair_proper; [done|]. apply pair_proper; [|done].
- rewrite /=. setoid_rewrite pair_op. apply pair_proper; [done|].
- rewrite pair_op. apply pair_proper; [|done].
- by rewrite -auth_frag_op -Some_op pair_op frac_op' lat_op_join' lat_join_idem_L.
- Qed.
- Global Instance StrDowns_asfractional γ q Dt :
- AsFractional (StrDowns γ q Dt) (λ q, StrDowns γ q Dt) q.
- Proof. split. done. apply _. Qed.
- Global Instance WkUps_fractional γ Ut : Fractional (λ q, WkUps γ q Ut).
- Proof.
- rewrite /Fractional => p q. rewrite -embed_sep -own_op.
- apply embed_proper, own.own_proper.
- do 2 (apply pair_proper; [done|]).
- rewrite /=. setoid_rewrite pair_op. apply pair_proper; [|done].
- by rewrite -auth_frag_op -Some_op pair_op frac_op' lat_op_join' lat_join_idem_L.
- Qed.
- Global Instance WkUps_asfractional γ q Ut :
- AsFractional (WkUps γ q Ut) (λ q, WkUps γ q Ut) q.
- Proof. split. done. apply _. Qed.
-
- (* move_self *)
- Local Notation moveSAuth Mt
- := ((● Some (1%Qp, to_agree $ to_latT Mt), ● to_latT Mt) : move_selfUR).
- Local Notation moveSMain q Mt
- := ((◯ Some (q, to_agree $ to_latT Mt), ε) : move_selfUR).
- Local Notation certS Mt
- := ((ε, ◯ to_latT Mt) : move_selfUR).
-
- Lemma arc_ghost_move_self_main_valid Mt1 Mt2 q:
- ✓ (moveSAuth Mt1 ⋅ moveSMain q Mt2) → Mt2 = Mt1.
- Proof.
- rewrite pair_op right_id_L.
- move => [/= /auth_valid_discrete_2 [/Some_included
- [[_ /= /to_agree_inj /to_latT_inj /leibniz_equiv_iff //]|
- /prod_included[_ /to_agree_included /to_latT_inj /leibniz_equiv_iff //]]_]_].
- Qed.
-
- Lemma arc_ghost_move_self_cert_valid Mt1 Mt2:
- ✓ (moveSAuth Mt1 ⋅ certS Mt2) → Mt2 ⊆ Mt1.
- Proof. rewrite pair_op => [[_ /auth_valid_discrete_2 [/latT_included // _]]]. Qed.
-
- Lemma StrongMoveAuth_agree γ Mt q Mt':
- StrongMoveAuth γ Mt ∗ StrMoves γ q Mt' -∗ ⌜Mt = Mt'⌝.
- Proof.
- rewrite -embed_sep -own_op.
- iIntros "own". iDestruct (own_valid with "own") as %VALID. iPureIntro.
- move : VALID => [/=_ [/= ]]. rewrite pair_op.
- move => [/= /arc_ghost_move_self_main_valid //].
- Qed.
-
- Lemma StrMoves_agree γ Mt Mt' q q':
- StrMoves γ q Mt ∗ StrMoves γ q' Mt' -∗ ⌜Mt = Mt'⌝.
- Proof.
- rewrite -embed_sep -own_op.
- iIntros "own". iDestruct (own_valid with "own") as %VAL. iPureIntro.
- move : VAL => [/=_ [/= [[VAL _]_]_]]. move :VAL.
- rewrite /= -auth_frag_op -Some_op pair_op auth_valid_discrete /= Some_valid.
- move => [_ /agree_op_inv' /to_latT_inj /leibniz_equiv_iff // ].
- Qed.
-
- Lemma StrongMoveAuth_Cert_include γ Mt Mt':
- StrongMoveAuth γ Mt ∗ StrMoveCertS γ Mt' -∗ ⌜Mt' ⊆ Mt⌝.
- Proof.
- rewrite -embed_sep -own_op.
- iIntros "own". iDestruct (own_valid with "own") as %VALID. iPureIntro.
- move :VALID => [/= _ [/= ]]. rewrite pair_op.
- move => [/= /arc_ghost_move_self_cert_valid //].
- Qed.
-
- Lemma StrMoves_update γ Mt Mt':
- StrongMoveAuth γ Mt ∗ StrMoves γ 1%Qp Mt ==∗
- StrongMoveAuth γ (Mt ∪ Mt') ∗ StrMoves γ 1%Qp (Mt ∪ Mt') ∗ StrMoveCertS γ Mt'.
- Proof.
- rewrite -3!embed_sep -3!own_op. iIntros "own".
- iMod (own_update with "own") as "$"; [|done].
- apply prod_update; [done|].
- apply prod_update; [|rewrite /= left_id right_id //].
- setoid_rewrite pair_op. rewrite /=.
- apply prod_update; [|rewrite /= left_id right_id //].
- rewrite /= 2!pair_op /= 2!right_id left_id.
- apply prod_update; simpl.
- - by apply auth_update, option_local_update, exclusive_local_update.
- - apply auth_update_alloc.
- rewrite -(right_id_L ε op (to_latT Mt')) -lat_op_join' cmra_comm.
- by apply op_local_update_discrete.
- Qed.
-
- (* move_other *)
- Local Notation moveOAuth Mt := ((● Some (1%Qp, to_latT Mt), ● to_latT Mt) : move_otherUR).
- Local Notation moveOMain q Mt := ((◯ Some (q, to_latT Mt), ε) : move_otherUR).
- Local Notation certO Mt := ((ε, ◯ to_latT Mt) : move_otherUR).
-
- Lemma arc_ghost_move_other_main_valid Mt1 Mt2:
- ✓ (moveOAuth Mt1 ⋅ moveOMain 1%Qp Mt2) → Mt2 = Mt1.
- Proof.
- rewrite pair_op.
- move => [/= /auth_valid_discrete_2 [/Some_included
- [[/= _ /to_latT_inj /leibniz_equiv_iff //]|
- /prod_included [/= /frac_included /= // _]]]].
- Qed.
-
- Lemma arc_ghost_move_other_cert_valid Mt1 Mt2:
- ✓ (moveOAuth Mt1 ⋅ certO Mt2) → Mt2 ⊆ Mt1.
- Proof.
- rewrite pair_op right_id_L.
- move => [/= _ /auth_valid_discrete_2 [/latT_included // ]].
- Qed.
-
- Lemma StrongDownAuth_agree γ Dt Dt':
- StrongDownAuth γ Dt ∗ StrDowns γ 1%Qp Dt' -∗ ⌜Dt = Dt'⌝.
- Proof.
- rewrite -embed_sep -own_op.
- iIntros "own". iDestruct (own_valid with "own") as %VALID. iPureIntro.
- move : VALID => [/=_ [/= [/= _ /arc_ghost_move_other_main_valid //]]].
- Qed.
-
- Lemma StrongDownAuth_Cert_include γ Dt Dt':
- StrongDownAuth γ Dt ∗ StrDownCertS γ Dt' -∗ ⌜Dt' ⊆ Dt⌝.
- Proof.
- rewrite -embed_sep -own_op.
- iIntros "own". iDestruct (own_valid with "own") as %VALID. iPureIntro.
- move :VALID => [/= _ [/= [/= _ /arc_ghost_move_other_cert_valid //]]].
- Qed.
-
- Lemma StrDowns_forget γ q q' Dt Dt':
- StrDowns γ (q + q')%Qp (Dt ∪ Dt') ≡
- (StrDowns γ q (Dt ∪ Dt') ∗ StrDowns γ q' Dt')%I.
- Proof.
- rewrite -embed_sep -own_op. apply embed_proper, own.own_proper.
- do 2 (apply pair_proper; [done|]; apply pair_proper; [|done]).
- simpl. rewrite -auth_frag_op -Some_op pair_op -frac_op' lat_op_join'.
- rewrite (lat_le_join_l_L (Dt ∪ Dt') Dt'); [done|solve_lat].
- Qed.
-
- Lemma WeakUpAuth_agree γ Ut Ut':
- WeakUpAuth γ Ut ∗ WkUps γ 1%Qp Ut' -∗ ⌜Ut = Ut'⌝.
- Proof.
- rewrite -embed_sep -own_op.
- iIntros "own". iDestruct (own_valid with "own") as %VALID. iPureIntro.
- move : VALID => [/=_ [/= _ /arc_ghost_move_other_main_valid //]].
- Qed.
-
- Lemma WeakUpAuth_Cert_include γ Ut Ut':
- WeakUpAuth γ Ut ∗ WkUpCertS γ Ut' -∗ ⌜Ut' ⊆ Ut⌝.
- Proof.
- rewrite -embed_sep -own_op.
- iIntros "own". iDestruct (own_valid with "own") as %VALID. iPureIntro.
- move :VALID => [/= _ [/= _ /arc_ghost_move_other_cert_valid //]].
- Qed.
-
- Lemma WkUps_forget γ q q' Ut Ut':
- WkUps γ (q + q')%Qp (Ut ∪ Ut') ≡
- (WkUps γ q (Ut ∪ Ut') ∗ WkUps γ q' Ut')%I.
- Proof.
- rewrite -embed_sep -own_op. apply embed_proper, own.own_proper.
- do 2 (apply pair_proper; [done|]). apply pair_proper; [|done]. simpl.
- rewrite -auth_frag_op -Some_op pair_op -frac_op' lat_op_join'.
- rewrite (lat_le_join_l_L (Ut ∪ Ut') Ut'); [done|solve_lat].
- Qed.
-
- Lemma StrDowns_join γ Dt Dt' q q' :
- StrDowns γ (q + q')%Qp (Dt ∪ Dt') ≡
- (StrDowns γ q Dt ∗ StrDowns γ q' Dt')%I.
- Proof.
- rewrite -embed_sep -own_op. apply embed_proper, own.own_proper.
- do 2 (apply pair_proper; [done|]; apply pair_proper; [|done]).
- simpl. by rewrite -auth_frag_op -Some_op pair_op -frac_op' lat_op_join'.
- Qed.
-
- Lemma StrDowns_update γ Dt1 Dt2 Dt' q :
- StrongDownAuth γ Dt1 ∗ StrDowns γ q Dt2 ==∗
- StrongDownAuth γ (Dt1 ⊔ Dt') ∗ StrDowns γ q (Dt2 ⊔ Dt') ∗ StrDownCertS γ Dt'.
- Proof.
- rewrite -3!embed_sep -3!own_op. iIntros "own".
- iMod (own_update with "own") as "$"; [|done].
- apply prod_update; [done|]. simpl.
- apply prod_update; [|rewrite /= !right_id //].
- setoid_rewrite pair_op. rewrite /=.
- apply prod_update; [rewrite /= !right_id //|].
- rewrite /= 2!pair_op /= 2!right_id_L left_id_L. rewrite -2!lat_op_join'.
- apply prod_update; simpl.
- - apply auth_update, option_local_update, prod_local_update_2.
- rewrite (cmra_comm_L (to_latT Dt1)) (cmra_comm_L (to_latT Dt2)).
- by apply op_local_update_discrete.
- - apply auth_update_alloc.
- rewrite cmra_comm_L -{2}(right_id_L ε op (to_latT Dt')).
- by apply op_local_update_discrete.
- Qed.
-
- Lemma WkUps_join γ Ut Ut' q q' :
- WkUps γ (q + q')%Qp (Ut ∪ Ut') ≡
- (WkUps γ q Ut ∗ WkUps γ q' Ut')%I.
- Proof.
- rewrite -embed_sep -own_op. apply embed_proper, own.own_proper.
- by do 3 (apply pair_proper; [done|]).
- Qed.
-
- Lemma WkUps_full_exclusive γ q Ut' :
- (∃ Ut, WkUps γ 1%Qp Ut) -∗ WkUps γ q Ut' -∗ False.
- Proof.
- iDestruct 1 as (Ut) "WU". iIntros "WU'".
- iDestruct (WkUps_join with "[$WU $WU']") as "WU".
- iDestruct (@own_valid _ arcUR with "WU")
- as %[_ [_ [[VAL _]%auth_valid_discrete _]]].
- iPureIntro. simpl in VAL.
- have Lt: (1%Qp < (1%Qp + q)%Qp)%Qc. apply Qp_lt_sum. by eexists.
- apply (irreflexive_eq (R:= Qclt) 1%Qp 1%Qp); [done|].
- eapply Qclt_le_trans; [apply Lt|done].
- Qed.
-
- Lemma WkUps_update γ Ut1 Ut2 Ut' q :
- WeakUpAuth γ Ut1 ∗ WkUps γ q Ut2 ==∗
- WeakUpAuth γ (Ut1 ⊔ Ut') ∗ WkUps γ q (Ut2 ⊔ Ut') ∗ WkUpCertS γ Ut'.
- Proof.
- rewrite -3!embed_sep -3!own_op. iIntros "own".
- iMod (own_update with "own") as "$"; [|done].
- apply prod_update; [done|]. simpl.
- apply prod_update; [rewrite /= !right_id //|].
- apply prod_update; rewrite /=.
- - apply auth_update, option_local_update, prod_local_update_2.
- rewrite -2!lat_op_join' (cmra_comm_L (to_latT Ut1)) (cmra_comm_L (to_latT Ut2)).
- by apply op_local_update_discrete.
- - rewrite -lat_op_join' right_id_L left_id_L. apply auth_update_alloc.
- rewrite cmra_comm_L -{2}(right_id_L ε op (to_latT Ut')).
- by apply op_local_update_discrete.
- Qed.
-
- Lemma StrongTok_Auth_agree γ st q :
- StrongAuth γ st ∗ StrongTok γ q -∗
- ⌜∃ q' strong, st = Some (q', strong) ∧
- if decide (strong = xH) then q = q' else ∃ q'', q' = (q + q'')%Qp⌝.
- Proof.
- rewrite -embed_sep -own_op. iIntros "oA".
- iDestruct (own_valid with "oA")
- as %[[[[|INCL]%option_included _]%auth_valid_discrete_2 _] _]; [done|].
- iPureIntro. destruct INCL as [q1 [[q' n] [Eq1 [Eq2 Eq3]]]].
- inversion Eq1. subst q1. exists q', n. split; [done|].
- destruct Eq3 as [[Eq3 Eq4]|[[q'' Le1] Le2%pos_included]%prod_included].
- - inversion Eq3. inversion Eq4. simpl in *. by subst.
- - simpl in *. rewrite decide_False. exists q''. by rewrite Le1 frac_op'.
- move => ?. by subst n.
- Qed.
-
- Lemma WeakTok_Auth_agree γ st q :
- WeakAuth γ st ∗ WeakTok γ q -∗
- ⌜∃ q' weak isStr, st = (isStr, Some $ Cinl (q', weak)) ∧
- if decide (weak = xH) then q = q' else ∃ q'', q' = (q + q'')%Qp⌝.
- Proof.
- rewrite -embed_sep -own_op. iIntros "oA".
- iDestruct (own_valid with "oA")
- as %[[_ [[_ INCL]%prod_included VALID]%auth_valid_discrete_2] _].
- iPureIntro. destruct st as [st' st]. simpl in *.
- apply option_included in INCL as [|[q1 [qn [Eq1 [Eq2 Eq3]]]]]; [done|].
- subst st. inversion Eq1. subst q1. destruct Eq3 as [Eq3|INCL].
- - exists q, xH, st'. inversion Eq3 as [? ? Eq4| |]. subst.
- apply leibniz_equiv_iff in Eq4. by subst.
- - destruct VALID as [? ?]. simpl in *.
- apply csum_included in INCL as [?|[([??]&[q' weak]&Eq2&?&INCL)|(?&?&?&?)]];
- [by subst qn|..|done].
- subst qn. exists q', weak, st'. split; [done|]. inversion Eq2. subst.
- apply prod_included in INCL as [[q'' Eq] INCLs%pos_included]. simpl in *.
- rewrite decide_False.
- exists q''. by rewrite Eq frac_op'. move => ?. by subst weak.
- Qed.
-
- Lemma StrongAuth_first_tok γ :
- StrongAuth γ None ==∗
- StrongAuth γ (Some ((1/2)%Qp, 1%positive)) ∗ StrongTok γ (1/2)%Qp.
- Proof.
- iIntros "own". rewrite -embed_sep -own_op.
- iMod (@own_update _ arcUR with "own") as "$"; [|done].
- apply prod_update; simpl; [|by rewrite right_id].
- apply prod_update; simpl; [|done]. apply auth_update_alloc.
- rewrite /= -(right_id None op (Some _)). by apply op_local_update_discrete.
- Qed.
-
- Lemma StrongAuth_new_tok γ (q q': frac) n (Hqq' : (q + q')%Qp = 1%Qp):
- StrongAuth γ (Some (q,n)) ==∗
- StrongAuth γ (Some ((q + (q'/2)%Qp)%Qp, (n + 1)%positive)) ∗
- StrongTok γ (q'/2)%Qp.
- Proof.
- iIntros "own". rewrite -embed_sep -own_op.
- iMod (@own_update _ arcUR with "own") as "$"; [|done].
- apply prod_update; simpl; [|by rewrite right_id].
- apply prod_update; simpl; [|done]. apply auth_update_alloc.
- rewrite Pos.add_comm Qp_plus_comm -pos_op_plus /= -frac_op' -pair_op Some_op.
- rewrite -{2}(right_id None op (Some ((q' /2)%Qp, _))).
- apply op_local_update_discrete => _ /=. split; simpl; [|done].
- apply frac_valid'. rewrite -Hqq' comm -{2}(Qp_div_2 q').
- apply Qcplus_le_mono_l. rewrite -{1}(Qcanon.Qcplus_0_l (q'/2)%Qp).
- apply Qcplus_le_mono_r, Qp_ge_0.
- Qed.
-
- Lemma WeakAuth_first_tok γ iS :
- WeakAuth γ (iS, None) ==∗
- WeakAuth γ (iS, Some $ Cinl ((1/2)%Qp, 1%positive)) ∗ WeakTok γ (1/2)%Qp.
- Proof.
- iIntros "own". rewrite -embed_sep -own_op.
- iMod (@own_update _ arcUR with "own") as "$"; [|done].
- apply prod_update; simpl; [|by rewrite right_id].
- apply prod_update; simpl; [done|]. apply auth_update_alloc.
- apply prod_local_update; simpl; [done|].
- rewrite /= -(right_id None op (Some _)). by apply op_local_update_discrete.
- Qed.
-
- Lemma WeakAuth_new_tok γ iS (q q': frac) n (Hqq' : (q + q')%Qp = 1%Qp):
- WeakAuth γ (iS, Some (Cinl (q, n))) ==∗
- WeakAuth γ (iS, Some (Cinl ((q + (q'/2)%Qp)%Qp, (n + 1)%positive))) ∗
- WeakTok γ (q'/2)%Qp.
- Proof.
- iIntros "own". rewrite -embed_sep -own_op.
- iMod (@own_update _ arcUR with "own") as "$"; [|done].
- apply prod_update; simpl; [|by rewrite right_id].
- apply prod_update; simpl; [done|]. apply auth_update_alloc.
- apply prod_local_update; simpl; [done|].
- rewrite Pos.add_comm Qp_plus_comm -pos_op_plus /=
- -frac_op' -pair_op -Cinl_op Some_op.
- rewrite -{2}(right_id None op (Some $ Cinl ((q' /2)%Qp, _))).
- apply op_local_update_discrete => _ /=. split; simpl; [|done].
- apply frac_valid'. rewrite -Hqq' comm -{2}(Qp_div_2 q').
- apply Qcplus_le_mono_l. rewrite -{1}(Qcanon.Qcplus_0_l (q'/2)%Qp).
- apply Qcplus_le_mono_r, Qp_ge_0.
- Qed.
-
- Lemma StrongAuth_drop_last γ q:
- StrongAuth γ (Some (q,1%positive)) ∗ StrongTok γ q ==∗
- StrongAuth γ None.
- Proof.
- rewrite -embed_sep -own_op. iIntros "own".
- iMod (@own_update _ arcUR with "own") as "$"; [|done].
- apply prod_update; simpl; [|by rewrite right_id].
- apply prod_update; simpl; [|done].
- apply auth_update_dealloc. rewrite /= -(right_id None op (Some _)).
- apply cancel_local_update_unit, _.
- Qed.
-
- Lemma StrongAuth_drop γ q q' n:
- StrongAuth γ (Some ((q + q')%Qp,(1 + n)%positive)) ∗ StrongTok γ q' ==∗
- StrongAuth γ (Some (q,n)).
- Proof.
- rewrite -embed_sep -own_op. iIntros "own".
- iMod (@own_update _ arcUR with "own") as "$"; [|done].
- apply prod_update; [|simpl; by rewrite right_id]. apply prod_update; [|done].
- apply auth_update_dealloc.
- rewrite -frac_op' -pos_op_plus /= (cmra_comm_L q) -pair_op Some_op.
- by apply (cancel_local_update_unit (Some _)), _.
- Qed.
-
- Lemma WeakAuth_drop_last γ iS q:
- WeakAuth γ (iS, Some $ Cinl (q,1%positive)) ∗ WeakTok γ q ==∗
- WeakAuth γ (iS, None).
- Proof.
- rewrite -embed_sep -own_op. iIntros "own".
- iMod (@own_update _ arcUR with "own") as "$"; [|done].
- apply prod_update; [|by rewrite /= right_id]. apply prod_update; [done|].
- apply auth_update_dealloc. apply prod_local_update; [done|].
- rewrite /= -(right_id None op (Some _)). apply cancel_local_update_unit, _.
- Qed.
-
- Lemma WeakAuth_drop γ iS (q q': frac) n:
- WeakAuth γ (iS, Some (Cinl ((q + q')%Qp,(1 + n)%positive))) ∗
- WeakTok γ q' ==∗
- WeakAuth γ (iS, Some (Cinl (q,n))).
- Proof.
- rewrite -embed_sep -own_op. iIntros "own".
- iMod (@own_update _ arcUR with "own") as "$"; [|done].
- apply prod_update; [|simpl; by rewrite right_id]. apply prod_update; [done|].
- apply auth_update_dealloc. apply prod_local_update; [done|].
- rewrite -frac_op' -pos_op_plus /= (cmra_comm_L q) -pair_op -Cinl_op Some_op.
- by apply (cancel_local_update_unit (Some _)), _.
- Qed.
-
- Lemma WeakAuth_strong γ iS st q :
- WeakAuth γ (iS, st) ∗ agown γ (awk_n ((Some q, ε))) -∗ ∃ q', ⌜iS = Some q'⌝.
- Proof.
- rewrite -embed_sep -own_op. iIntros "own".
- iDestruct (own_valid with "own") as %[[_ [VAL _]%auth_valid_discrete_2] _].
- iPureIntro. move : VAL => /prod_included /= [/option_included [//|[?[? [?[??]]]]] _].
- subst iS. by eexists.
- Qed.
-
- Lemma WeakAuth_valid γ iS st :
- WeakAuth γ (iS, st) -∗ ⌜st ≠ Some CsumBot⌝.
- Proof.
- iIntros "own".
- iDestruct (@own_valid _ arcUR with "own") as %[[_ [_ [_ VAL]]%auth_valid_discrete] _].
- simpl in VAL. iPureIntro. by destruct st as [[| |]|].
- Qed.
-
- Lemma WeakAuth_drop_strong γ st:
- WeakAuth γ (Some 1%Qp, st) ∗ agown γ (awk_n ((Some 1%Qp, ε))) ==∗
- WeakAuth γ (None, st).
- Proof.
- rewrite -embed_sep -own_op. iIntros "own".
- iMod (@own_update _ arcUR with "own") as "$"; [|done].
- apply prod_update; [|by rewrite /= right_id]. apply prod_update; [done|].
- apply auth_update_dealloc. apply prod_local_update; [|done].
- rewrite /= -{1}(right_id None op (Some _)).
- by apply (cancel_local_update_unit (Some _)), _.
- Qed.
-
- Lemma StrWkTok_exclusive γ q :
- agown γ (awk_n ((Some 1%Qp, ε))) ∗ agown γ (awk_n ((Some q, ε))) -∗ False.
- Proof.
- rewrite -embed_sep -own_op. iIntros "own".
- iDestruct (@own_valid _ arcUR with "own") as %[[_ VAL] _]. simpl in VAL.
- iPureIntro. move : VAL. rewrite -auth_frag_op pair_op -Some_op frac_op'.
- move => /auth_valid_discrete /= [/= ? _].
- have Lt: (1%Qp < (1%Qp + q)%Qp)%Qc. apply Qp_lt_sum. by eexists.
- apply (irreflexive_eq (R:= Qclt) 1%Qp 1%Qp); [done|].
- eapply Qclt_le_trans; [apply Lt|done].
- Qed.
-
- Lemma StrMoves_full_exclusive γ q Mt' :
- (∃ Mt, StrMoves γ 1%Qp Mt) -∗ StrMoves γ q Mt' -∗ False.
- Proof.
- iDestruct 1 as (Mt) "SM". iIntros "SM'".
- iDestruct (StrMoves_agree with "[$SM $SM']") as %?. subst Mt'.
- iDestruct (StrMoves_fractional with "[$SM $SM']") as "SM".
- iDestruct (@own_valid _ arcUR with "SM") as %[_ [[[[VAL _] _] _] _]].
- iPureIntro. simpl in VAL.
- have Lt: (1%Qp < (1%Qp + q)%Qp)%Qc. apply Qp_lt_sum. by eexists.
- apply (irreflexive_eq (R:= Qclt) 1%Qp 1%Qp); [done|].
- eapply Qclt_le_trans; [apply Lt|done].
- Qed.
-
- Lemma WeakAuth_new_lock γ iS q:
- WeakAuth γ (iS, None) ==∗
- WeakAuth γ (iS, Some $ Cinr (Excl (), to_agree q)) ∗ WkLock γ q.
- Proof.
- rewrite -embed_sep -own_op. iIntros "own".
- iMod (@own_update _ arcUR with "own") as "$"; [|done].
- apply prod_update; [|by rewrite /= right_id]. apply prod_update; [done|]. simpl.
- apply auth_update_alloc. apply prod_local_update; simpl; [done|].
- rewrite -(right_id None op (Some _)).
- by apply op_local_update_discrete.
- Qed.
-
- Lemma WeakAuth_lock_agree γ iS st q:
- WeakAuth γ (iS, st) ∗ WkLock γ q -∗
- ⌜st ≡ Some (Cinr (Excl tt, to_agree q))⌝.
- Proof.
- rewrite -embed_sep -own_op. iIntros "own".
- iDestruct (@own_valid _ arcUR with "own")
- as %[[_ [[_ [?|INCL]%option_included]%prod_included [_ VAL]]%auth_valid_discrete_2] _];
- [done|]. iPureIntro.
- destruct INCL as (x & y & Eq1 & Eq2 & INCL). simpl in *. inversion Eq1.
- subst x st. destruct INCL as [Eq|INCL].
- - inversion Eq as [|? b Eq2 |]. subst. by rewrite -Eq2.
- - apply csum_included in INCL as [?|[(?&?&?&?)|(?&[u v]&Eq&?&[IN1 IN2]%prod_included)]];
- [by subst y|done|..].
- subst. inversion Eq. clear Eq. subst.
- move : VAL => [VAL1 /to_agree_uninj [? VAL2]]. destruct u as [[]|]; [|done].
- simpl in *. move : IN2. rewrite -VAL2. move => /to_agree_included <- //.
- Qed.
-
- Lemma WeakAuth_unlock γ iS st q :
- WeakAuth γ (iS, st) ∗ WkLock γ q ==∗ WeakAuth γ (iS, None).
- Proof.
- iIntros "own". iDestruct (WeakAuth_lock_agree with "own") as %Eq.
- rewrite -embed_sep -own_op.
- iMod (@own_update _ arcUR with "own") as "$"; [|done].
- apply prod_update; [|by rewrite /= right_id]. apply prod_update; [done|]. simpl.
- rewrite Eq. apply auth_update_dealloc. apply prod_local_update; [done|].
- rewrite /= -{1}(right_id None op (Some _)).
- apply (cancel_local_update_unit (Some _)), _.
- Qed.
-End ArcGhost.
Section ArcInv.
(* P1 is the thing that is shared by strong reference owners (in practice,
@@ -934,11 +300,14 @@ Section arc.
destruct st as [[|] [[[]| |]|]]; simpl; try done. solve_proper.
Qed.
- (* TODO: port to local assertion iff
Global Instance arc_inv_proper :
- Proper (pointwise_relation _ (≡) ==> (≡) ==> eq ==> eq ==> (≡))
+ Proper (pointwise_relation _ (≡) ==> (≡) ==> eq ==> eq ==> eq ==> eq ==> (≡))
arc_inv.
- Proof. solve_proper. Qed. *)
+ Proof.
+ move => ??????????????????. subst. apply bi.or_proper; [done|].
+ apply bi.sep_proper; [done|].
+ apply bi.sep_proper; apply bi.exist_proper => V.
+ Abort.
Global Instance is_arc_contractive n :
Proper (pointwise_relation _ (dist_later n) ==> dist_later n ==>
diff --git a/theories/lang/arc_cmra.v b/theories/lang/arc_cmra.v
new file mode 100644
index 0000000000000000000000000000000000000000..ff20954a9b5b5272ad38ca5ee9338d2d7bf78509
--- /dev/null
+++ b/theories/lang/arc_cmra.v
@@ -0,0 +1,643 @@
+From Coq.QArith Require Import Qcanon.
+From iris.base_logic.lib Require Import invariants.
+From iris.proofmode Require Import tactics.
+From iris.bi Require Import fractional.
+From iris.algebra Require Import excl csum frac auth agree.
+From lrust.lang Require Import notation.
+From gpfsl.gps Require Import middleware protocols.
+Set Default Proof Using "Type".
+
+(* Lattice of sets with subseteq *)
+Program Canonical Structure gset_Lat (A: Type) `{Countable A} :=
+ Make_Lat (gset A) (≡) subseteq union intersection
+ _ _ _ _ _ _ _ _ _ _ _ _ _.
+Next Obligation. move => ???. by apply union_subseteq_l. Qed.
+Next Obligation. move => ???. by apply union_subseteq_r. Qed.
+Next Obligation. move => ???. by apply union_least. Qed.
+Next Obligation. move => ???. by apply intersection_subseteq_l. Qed.
+Next Obligation. move => ???. by apply intersection_subseteq_r. Qed.
+Next Obligation. move => ??????. by apply intersection_greatest. Qed.
+
+Instance gset_Lat_bot `{Countable A} : LatBottom (∅ : gset_Lat A).
+Proof. done. Qed.
+
+(** The CMRAs we need. *)
+
+(* This cmra tracks what the arc must have done by itself when it is the unique clone.
+
+ Self here means that the cmra is updated when the caller moves its own counter,
+ e.g. the strong arc modifying the strong counter, or the weak arc modifying
+ the weak counter.
+ For the strong counter, it tracks the actions: moving 1 to 0
+ (the last release/drop), and 1 to 2 (the unique clone).
+ For the weak counter, it tracks the self actions: moving 1 to -1 (locking),
+ moving 1 to 0 (the last drop), and 1 to 2 (the unique clone).
+
+ The authority should only be updated when having full fraction,
+ i.e. the caller being unique. A persistent certificate is issued when the
+ authority is updated. A fraction of the authority must have seen all certificates. *)
+Definition move_selfUR :=
+ prodUR (authUR (optionUR (prodR fracR (agreeR (latC (gset_Lat time))))))
+ (authUR (latUR (gset_Lat time))).
+
+(* This cmra tracks what the arc has asked the other to do, e.g., the weak arc
+ asks the strong counter to increment when upgrading, or the strong arc asks
+ the weak counter to increment when downgrading.
+
+ The authority part is owned by the caller, and issue a certificate for
+ the callee to store in its update. There can be multiple authorities,
+ each is owned by one caller. A fraction of the authority can issue certificates,
+ while only the full fraction authority is guaranteed to have seen all certificates. *)
+Definition move_otherUR :=
+ prodUR (authUR (optionUR (prodR fracR (latR (gset_Lat time)))))
+ (authUR (latUR (gset_Lat time))).
+
+(* This cmra tracks states of the weak counter:
+ - (None, None) : no strong or weak arc, v = 0.
+ - (None, Some Cinl (q,n)) : no strong arc, n weak arcs that use q permission,
+ v = n.
+ - (None, Some Cinr q) : no strong arc, no weak arc, the weak counter is locked
+ with a payload of q from a strong arc, v = -1. This state is IMPOSSIBLE.
+ - (Some 1, None) : some strong arcs, no weak arcs, v = 1.
+ - (Some 1, Some Cinl (q,n)) : some strong arcs, n weak arcs that use q, v = S n.
+ - (Some 1, Some Cinr q) : some strong arcs, no weak arc, the weak counter is
+ locked with a payload of q from a strong arc, v = -1.
+*)
+
+Definition weak_stUR :=
+ prodUR (optionUR fracR)
+ (optionUR (csumR (prodR fracR positiveR) (prodR (exclR unitC) (agreeR fracC)))).
+
+(* This cmra tracks states of the strong counter:
+ - None: no strong arc, v = 0.
+ - Some (q,n): n strong arcs that took out q, v = n. *)
+Definition strong_stUR :=
+ optionUR (prodR fracR positiveR).
+
+(* The final cmra has 5 components
+ (strong arc states, weak arc states),
+ (strong arc self, strong arc downgrade),
+ (weak arc upgrade) *)
+Definition arcUR :=
+ prodUR (prodUR (authUR strong_stUR) (authUR weak_stUR))
+ (prodUR (prodUR move_selfUR move_otherUR) move_otherUR).
+
+Class arcG Σ := {
+ ArcStG :> inG Σ arcUR;
+ ArcPrt_gpsG :> gpsG Σ unitProtocol;
+}.
+Definition arcΣ : gFunctors := #[GFunctor arcUR; gpsΣ unitProtocol].
+Instance subG_arcΣ {Σ} : subG arcΣ Σ → arcG Σ.
+Proof. solve_inG. Qed.
+
+Definition Z_of_arcweak_st (st : weak_stUR) : Z :=
+ match st with
+ | (None, None) => 0
+ | (Some _, None) => 1
+ | (None, Some (Cinl (_, n))) => Zpos n
+ | (Some _, Some (Cinl (_, n))) => Zpos n +1
+ | (_, Some _) => -1
+ end.
+
+Definition Z_of_arcstrong_st (st : strong_stUR) : Z :=
+ match st with
+ | None => 0
+ | Some (_, n) => Zpos n
+ end.
+
+
+Lemma strong_stUR_value st: 0 ≤ Z_of_arcstrong_st st.
+Proof. destruct st as [[]|]; simpl; lia. Qed.
+
+Lemma weak_stUR_value st: -1 ≤ Z_of_arcweak_st st.
+Proof. destruct st as [[|] [[[]| |]|]]; simpl; lia. Qed.
+
+Notation agown γ st := (⎡ own γ (st : arcUR) ⎤ : vProp _)%I.
+Notation awk_n st := ((ε, ◯ (st : weak_stUR)), ε).
+
+Section ArcGhost.
+ Context `{inG Σ arcUR}.
+ Local Notation vProp := (vProp Σ).
+ Implicit Types (Mt Ut Dt: gset time).
+
+ Definition StrongAuth γ (st : strong_stUR) :=
+ agown γ ((● st, ε), ε).
+ Definition StrongTok γ q :=
+ agown γ ((◯ Some (q, xH), ε), ε).
+ Definition StrongMoveAuth γ Mt :=
+ agown γ (ε, (((● Some (1%Qp, to_agree $ to_latT Mt), ● to_latT Mt) : move_selfUR, ε), ε)).
+ Definition StrMoves γ (q: frac) Mt :=
+ agown γ (ε, (((◯ Some (q, to_agree $ to_latT Mt), ε) : move_selfUR, ε), ε)).
+ Definition StrongDownAuth γ Dt :=
+ agown γ (ε, ((ε, (● Some (1%Qp, to_latT Dt), ● to_latT Dt) : move_otherUR), ε)).
+ Definition StrDowns γ (q: frac) Dt :=
+ agown γ (ε, ((ε, (◯ Some (q, to_latT Dt), ε) : move_otherUR), ε)).
+ Definition StrMoveCertS γ Mt : vProp :=
+ agown γ (ε, (((ε, ◯ to_latT Mt) : move_selfUR, ε), ε)).
+ Definition StrDownCertS γ Mt : vProp :=
+ agown γ (ε, ((ε, (ε, ◯ to_latT Mt) : move_otherUR), ε)).
+ Definition StrMoveCert γ t := StrMoveCertS γ {[t : time]}.
+ Definition StrDownCert γ t := StrDownCertS γ {[t : time]}.
+
+ Definition WeakAuth γ (st : weak_stUR) :=
+ agown γ ((ε, ● st), ε).
+ Definition WeakTok γ q :=
+ agown γ ((ε, ◯ (ε, Some (Cinl (q, xH)))), ε).
+ Definition WeakUpAuth γ Ut :=
+ agown γ (ε, (ε, (● Some (1%Qp, to_latT Ut), ● to_latT Ut) : move_otherUR)).
+ Definition WkUps γ (q: frac) Ut :=
+ agown γ (ε, (ε, (◯ Some (q, to_latT Ut), ε) : move_otherUR)).
+ Definition WkUpCertS γ Mt :=
+ agown γ (ε, (ε, (ε, ◯ to_latT Mt) : move_otherUR)).
+ Definition WkUpCert γ t := WkUpCertS γ {[t : time]}.
+ Definition WkLock γ q :=
+ agown γ (ε, ◯ (ε, Some $ Cinr (Excl(), to_agree q)),ε) .
+
+ Global Instance StrMoveCertS_persistent γ Mt : Persistent (StrMoveCertS γ Mt).
+ Proof. apply embed_persistent, own_core_persistent, pair_core_id; by apply _. Qed.
+ Global Instance StrDownCertS_persistent γ Mt : Persistent (StrDownCertS γ Mt).
+ Proof. apply embed_persistent, own_core_persistent, pair_core_id; by apply _. Qed.
+ Global Instance WkUpCertS_persistent γ Mt : Persistent (WkUpCertS γ Mt).
+ Proof. apply embed_persistent, own_core_persistent, pair_core_id; by apply _. Qed.
+ Global Instance StrMoves_fractional γ Mt : Fractional (λ q, StrMoves γ q Mt).
+ Proof.
+ rewrite /Fractional => p q. rewrite -embed_sep -own_op.
+ apply embed_proper, own.own_proper.
+ apply pair_proper; [done|]. do 3 (apply pair_proper; [|done]). simpl.
+ by rewrite -auth_frag_op -Some_op pair_op frac_op' agree_idemp.
+ Qed.
+ Global Instance StrMoves_asfractional γ q Mt :
+ AsFractional (StrMoves γ q Mt) (λ q, StrMoves γ q Mt) q.
+ Proof. split. done. apply _. Qed.
+ Global Instance StrDowns_fractional γ Dt : Fractional (λ q, StrDowns γ q Dt).
+ Proof.
+ rewrite /Fractional => p q. rewrite -embed_sep -own_op.
+ apply embed_proper, own.own_proper.
+ apply pair_proper; [done|]. apply pair_proper; [|done].
+ rewrite /=. setoid_rewrite pair_op. apply pair_proper; [done|].
+ rewrite pair_op. apply pair_proper; [|done].
+ by rewrite -auth_frag_op -Some_op pair_op frac_op' lat_op_join' lat_join_idem_L.
+ Qed.
+ Global Instance StrDowns_asfractional γ q Dt :
+ AsFractional (StrDowns γ q Dt) (λ q, StrDowns γ q Dt) q.
+ Proof. split. done. apply _. Qed.
+ Global Instance WkUps_fractional γ Ut : Fractional (λ q, WkUps γ q Ut).
+ Proof.
+ rewrite /Fractional => p q. rewrite -embed_sep -own_op.
+ apply embed_proper, own.own_proper.
+ do 2 (apply pair_proper; [done|]).
+ rewrite /=. setoid_rewrite pair_op. apply pair_proper; [|done].
+ by rewrite -auth_frag_op -Some_op pair_op frac_op' lat_op_join' lat_join_idem_L.
+ Qed.
+ Global Instance WkUps_asfractional γ q Ut :
+ AsFractional (WkUps γ q Ut) (λ q, WkUps γ q Ut) q.
+ Proof. split. done. apply _. Qed.
+
+ (* move_self *)
+ Local Notation moveSAuth Mt
+ := ((● Some (1%Qp, to_agree $ to_latT Mt), ● to_latT Mt) : move_selfUR).
+ Local Notation moveSMain q Mt
+ := ((◯ Some (q, to_agree $ to_latT Mt), ε) : move_selfUR).
+ Local Notation certS Mt
+ := ((ε, ◯ to_latT Mt) : move_selfUR).
+
+ Lemma arc_ghost_move_self_main_valid Mt1 Mt2 q:
+ ✓ (moveSAuth Mt1 ⋅ moveSMain q Mt2) → Mt2 = Mt1.
+ Proof.
+ rewrite pair_op right_id_L.
+ move => [/= /auth_valid_discrete_2 [/Some_included
+ [[_ /= /to_agree_inj /to_latT_inj /leibniz_equiv_iff //]|
+ /prod_included[_ /to_agree_included /to_latT_inj /leibniz_equiv_iff //]]_]_].
+ Qed.
+
+ Lemma arc_ghost_move_self_cert_valid Mt1 Mt2:
+ ✓ (moveSAuth Mt1 ⋅ certS Mt2) → Mt2 ⊆ Mt1.
+ Proof. rewrite pair_op => [[_ /auth_valid_discrete_2 [/latT_included // _]]]. Qed.
+
+ Lemma StrongMoveAuth_agree γ Mt q Mt':
+ StrongMoveAuth γ Mt ∗ StrMoves γ q Mt' -∗ ⌜Mt = Mt'⌝.
+ Proof.
+ rewrite -embed_sep -own_op.
+ iIntros "own". iDestruct (own_valid with "own") as %VALID. iPureIntro.
+ move : VALID => [/=_ [/= ]]. rewrite pair_op.
+ move => [/= /arc_ghost_move_self_main_valid //].
+ Qed.
+
+ Lemma StrMoves_agree γ Mt Mt' q q':
+ StrMoves γ q Mt ∗ StrMoves γ q' Mt' -∗ ⌜Mt = Mt'⌝.
+ Proof.
+ rewrite -embed_sep -own_op.
+ iIntros "own". iDestruct (own_valid with "own") as %VAL. iPureIntro.
+ move : VAL => [/=_ [/= [[VAL _]_]_]]. move :VAL.
+ rewrite /= -auth_frag_op -Some_op pair_op auth_valid_discrete /= Some_valid.
+ move => [_ /agree_op_inv' /to_latT_inj /leibniz_equiv_iff // ].
+ Qed.
+
+ Lemma StrongMoveAuth_Cert_include γ Mt Mt':
+ StrongMoveAuth γ Mt ∗ StrMoveCertS γ Mt' -∗ ⌜Mt' ⊆ Mt⌝.
+ Proof.
+ rewrite -embed_sep -own_op.
+ iIntros "own". iDestruct (own_valid with "own") as %VALID. iPureIntro.
+ move :VALID => [/= _ [/= ]]. rewrite pair_op.
+ move => [/= /arc_ghost_move_self_cert_valid //].
+ Qed.
+
+ Lemma StrMoves_update γ Mt Mt':
+ StrongMoveAuth γ Mt ∗ StrMoves γ 1%Qp Mt ==∗
+ StrongMoveAuth γ (Mt ∪ Mt') ∗ StrMoves γ 1%Qp (Mt ∪ Mt') ∗ StrMoveCertS γ Mt'.
+ Proof.
+ rewrite -3!embed_sep -3!own_op. iIntros "own".
+ iMod (own_update with "own") as "$"; [|done].
+ apply prod_update; [done|].
+ apply prod_update; [|rewrite /= left_id right_id //].
+ setoid_rewrite pair_op. rewrite /=.
+ apply prod_update; [|rewrite /= left_id right_id //].
+ rewrite /= 2!pair_op /= 2!right_id left_id.
+ apply prod_update; simpl.
+ - by apply auth_update, option_local_update, exclusive_local_update.
+ - apply auth_update_alloc.
+ rewrite -(right_id_L ε op (to_latT Mt')) -lat_op_join' cmra_comm.
+ by apply op_local_update_discrete.
+ Qed.
+
+ (* move_other *)
+ Local Notation moveOAuth Mt := ((● Some (1%Qp, to_latT Mt), ● to_latT Mt) : move_otherUR).
+ Local Notation moveOMain q Mt := ((◯ Some (q, to_latT Mt), ε) : move_otherUR).
+ Local Notation certO Mt := ((ε, ◯ to_latT Mt) : move_otherUR).
+
+ Lemma arc_ghost_move_other_main_valid Mt1 Mt2:
+ ✓ (moveOAuth Mt1 ⋅ moveOMain 1%Qp Mt2) → Mt2 = Mt1.
+ Proof.
+ rewrite pair_op.
+ move => [/= /auth_valid_discrete_2 [/Some_included
+ [[/= _ /to_latT_inj /leibniz_equiv_iff //]|
+ /prod_included [/= /frac_included /= // _]]]].
+ Qed.
+
+ Lemma arc_ghost_move_other_cert_valid Mt1 Mt2:
+ ✓ (moveOAuth Mt1 ⋅ certO Mt2) → Mt2 ⊆ Mt1.
+ Proof.
+ rewrite pair_op right_id_L.
+ move => [/= _ /auth_valid_discrete_2 [/latT_included // ]].
+ Qed.
+
+ Lemma StrongDownAuth_agree γ Dt Dt':
+ StrongDownAuth γ Dt ∗ StrDowns γ 1%Qp Dt' -∗ ⌜Dt = Dt'⌝.
+ Proof.
+ rewrite -embed_sep -own_op.
+ iIntros "own". iDestruct (own_valid with "own") as %VALID. iPureIntro.
+ move : VALID => [/=_ [/= [/= _ /arc_ghost_move_other_main_valid //]]].
+ Qed.
+
+ Lemma StrongDownAuth_Cert_include γ Dt Dt':
+ StrongDownAuth γ Dt ∗ StrDownCertS γ Dt' -∗ ⌜Dt' ⊆ Dt⌝.
+ Proof.
+ rewrite -embed_sep -own_op.
+ iIntros "own". iDestruct (own_valid with "own") as %VALID. iPureIntro.
+ move :VALID => [/= _ [/= [/= _ /arc_ghost_move_other_cert_valid //]]].
+ Qed.
+
+ Lemma StrDowns_forget γ q q' Dt Dt':
+ StrDowns γ (q + q')%Qp (Dt ∪ Dt') ≡
+ (StrDowns γ q (Dt ∪ Dt') ∗ StrDowns γ q' Dt')%I.
+ Proof.
+ rewrite -embed_sep -own_op. apply embed_proper, own.own_proper.
+ do 2 (apply pair_proper; [done|]; apply pair_proper; [|done]).
+ simpl. rewrite -auth_frag_op -Some_op pair_op -frac_op' lat_op_join'.
+ rewrite (lat_le_join_l_L (Dt ∪ Dt') Dt'); [done|solve_lat].
+ Qed.
+
+ Lemma WeakUpAuth_agree γ Ut Ut':
+ WeakUpAuth γ Ut ∗ WkUps γ 1%Qp Ut' -∗ ⌜Ut = Ut'⌝.
+ Proof.
+ rewrite -embed_sep -own_op.
+ iIntros "own". iDestruct (own_valid with "own") as %VALID. iPureIntro.
+ move : VALID => [/=_ [/= _ /arc_ghost_move_other_main_valid //]].
+ Qed.
+
+ Lemma WeakUpAuth_Cert_include γ Ut Ut':
+ WeakUpAuth γ Ut ∗ WkUpCertS γ Ut' -∗ ⌜Ut' ⊆ Ut⌝.
+ Proof.
+ rewrite -embed_sep -own_op.
+ iIntros "own". iDestruct (own_valid with "own") as %VALID. iPureIntro.
+ move :VALID => [/= _ [/= _ /arc_ghost_move_other_cert_valid //]].
+ Qed.
+
+ Lemma WkUps_forget γ q q' Ut Ut':
+ WkUps γ (q + q')%Qp (Ut ∪ Ut') ≡
+ (WkUps γ q (Ut ∪ Ut') ∗ WkUps γ q' Ut')%I.
+ Proof.
+ rewrite -embed_sep -own_op. apply embed_proper, own.own_proper.
+ do 2 (apply pair_proper; [done|]). apply pair_proper; [|done]. simpl.
+ rewrite -auth_frag_op -Some_op pair_op -frac_op' lat_op_join'.
+ rewrite (lat_le_join_l_L (Ut ∪ Ut') Ut'); [done|solve_lat].
+ Qed.
+
+ Lemma StrDowns_join γ Dt Dt' q q' :
+ StrDowns γ (q + q')%Qp (Dt ∪ Dt') ≡
+ (StrDowns γ q Dt ∗ StrDowns γ q' Dt')%I.
+ Proof.
+ rewrite -embed_sep -own_op. apply embed_proper, own.own_proper.
+ do 2 (apply pair_proper; [done|]; apply pair_proper; [|done]).
+ simpl. by rewrite -auth_frag_op -Some_op pair_op -frac_op' lat_op_join'.
+ Qed.
+
+ Lemma StrDowns_update γ Dt1 Dt2 Dt' q :
+ StrongDownAuth γ Dt1 ∗ StrDowns γ q Dt2 ==∗
+ StrongDownAuth γ (Dt1 ⊔ Dt') ∗ StrDowns γ q (Dt2 ⊔ Dt') ∗ StrDownCertS γ Dt'.
+ Proof.
+ rewrite -3!embed_sep -3!own_op. iIntros "own".
+ iMod (own_update with "own") as "$"; [|done].
+ apply prod_update; [done|]. simpl.
+ apply prod_update; [|rewrite /= !right_id //].
+ setoid_rewrite pair_op. rewrite /=.
+ apply prod_update; [rewrite /= !right_id //|].
+ rewrite /= 2!pair_op /= 2!right_id_L left_id_L. rewrite -2!lat_op_join'.
+ apply prod_update; simpl.
+ - apply auth_update, option_local_update, prod_local_update_2.
+ rewrite (cmra_comm_L (to_latT Dt1)) (cmra_comm_L (to_latT Dt2)).
+ by apply op_local_update_discrete.
+ - apply auth_update_alloc.
+ rewrite cmra_comm_L -{2}(right_id_L ε op (to_latT Dt')).
+ by apply op_local_update_discrete.
+ Qed.
+
+ Lemma WkUps_join γ Ut Ut' q q' :
+ WkUps γ (q + q')%Qp (Ut ∪ Ut') ≡
+ (WkUps γ q Ut ∗ WkUps γ q' Ut')%I.
+ Proof.
+ rewrite -embed_sep -own_op. apply embed_proper, own.own_proper.
+ by do 3 (apply pair_proper; [done|]).
+ Qed.
+
+ Lemma WkUps_full_exclusive γ q Ut' :
+ (∃ Ut, WkUps γ 1%Qp Ut) -∗ WkUps γ q Ut' -∗ False.
+ Proof.
+ iDestruct 1 as (Ut) "WU". iIntros "WU'".
+ iDestruct (WkUps_join with "[$WU $WU']") as "WU".
+ iDestruct (@own_valid _ arcUR with "WU")
+ as %[_ [_ [[VAL _]%auth_valid_discrete _]]].
+ iPureIntro. simpl in VAL.
+ have Lt: (1%Qp < (1%Qp + q)%Qp)%Qc. apply Qp_lt_sum. by eexists.
+ apply (irreflexive_eq (R:= Qclt) 1%Qp 1%Qp); [done|].
+ eapply Qclt_le_trans; [apply Lt|done].
+ Qed.
+
+ Lemma WkUps_update γ Ut1 Ut2 Ut' q :
+ WeakUpAuth γ Ut1 ∗ WkUps γ q Ut2 ==∗
+ WeakUpAuth γ (Ut1 ⊔ Ut') ∗ WkUps γ q (Ut2 ⊔ Ut') ∗ WkUpCertS γ Ut'.
+ Proof.
+ rewrite -3!embed_sep -3!own_op. iIntros "own".
+ iMod (own_update with "own") as "$"; [|done].
+ apply prod_update; [done|]. simpl.
+ apply prod_update; [rewrite /= !right_id //|].
+ apply prod_update; rewrite /=.
+ - apply auth_update, option_local_update, prod_local_update_2.
+ rewrite -2!lat_op_join' (cmra_comm_L (to_latT Ut1)) (cmra_comm_L (to_latT Ut2)).
+ by apply op_local_update_discrete.
+ - rewrite -lat_op_join' right_id_L left_id_L. apply auth_update_alloc.
+ rewrite cmra_comm_L -{2}(right_id_L ε op (to_latT Ut')).
+ by apply op_local_update_discrete.
+ Qed.
+
+ Lemma StrongTok_Auth_agree γ st q :
+ StrongAuth γ st ∗ StrongTok γ q -∗
+ ⌜∃ q' strong, st = Some (q', strong) ∧
+ if decide (strong = xH) then q = q' else ∃ q'', q' = (q + q'')%Qp⌝.
+ Proof.
+ rewrite -embed_sep -own_op. iIntros "oA".
+ iDestruct (own_valid with "oA")
+ as %[[[[|INCL]%option_included _]%auth_valid_discrete_2 _] _]; [done|].
+ iPureIntro. destruct INCL as [q1 [[q' n] [Eq1 [Eq2 Eq3]]]].
+ inversion Eq1. subst q1. exists q', n. split; [done|].
+ destruct Eq3 as [[Eq3 Eq4]|[[q'' Le1] Le2%pos_included]%prod_included].
+ - inversion Eq3. inversion Eq4. simpl in *. by subst.
+ - simpl in *. rewrite decide_False. exists q''. by rewrite Le1 frac_op'.
+ move => ?. by subst n.
+ Qed.
+
+ Lemma WeakTok_Auth_agree γ st q :
+ WeakAuth γ st ∗ WeakTok γ q -∗
+ ⌜∃ q' weak isStr, st = (isStr, Some $ Cinl (q', weak)) ∧
+ if decide (weak = xH) then q = q' else ∃ q'', q' = (q + q'')%Qp⌝.
+ Proof.
+ rewrite -embed_sep -own_op. iIntros "oA".
+ iDestruct (own_valid with "oA")
+ as %[[_ [[_ INCL]%prod_included VALID]%auth_valid_discrete_2] _].
+ iPureIntro. destruct st as [st' st]. simpl in *.
+ apply option_included in INCL as [|[q1 [qn [Eq1 [Eq2 Eq3]]]]]; [done|].
+ subst st. inversion Eq1. subst q1. destruct Eq3 as [Eq3|INCL].
+ - exists q, xH, st'. inversion Eq3 as [? ? Eq4| |]. subst.
+ apply leibniz_equiv_iff in Eq4. by subst.
+ - destruct VALID as [? ?]. simpl in *.
+ apply csum_included in INCL as [?|[([??]&[q' weak]&Eq2&?&INCL)|(?&?&?&?)]];
+ [by subst qn|..|done].
+ subst qn. exists q', weak, st'. split; [done|]. inversion Eq2. subst.
+ apply prod_included in INCL as [[q'' Eq] INCLs%pos_included]. simpl in *.
+ rewrite decide_False.
+ exists q''. by rewrite Eq frac_op'. move => ?. by subst weak.
+ Qed.
+
+ Lemma StrongAuth_first_tok γ :
+ StrongAuth γ None ==∗
+ StrongAuth γ (Some ((1/2)%Qp, 1%positive)) ∗ StrongTok γ (1/2)%Qp.
+ Proof.
+ iIntros "own". rewrite -embed_sep -own_op.
+ iMod (@own_update _ arcUR with "own") as "$"; [|done].
+ apply prod_update; simpl; [|by rewrite right_id].
+ apply prod_update; simpl; [|done]. apply auth_update_alloc.
+ rewrite /= -(right_id None op (Some _)). by apply op_local_update_discrete.
+ Qed.
+
+ Lemma StrongAuth_new_tok γ (q q': frac) n (Hqq' : (q + q')%Qp = 1%Qp):
+ StrongAuth γ (Some (q,n)) ==∗
+ StrongAuth γ (Some ((q + (q'/2)%Qp)%Qp, (n + 1)%positive)) ∗
+ StrongTok γ (q'/2)%Qp.
+ Proof.
+ iIntros "own". rewrite -embed_sep -own_op.
+ iMod (@own_update _ arcUR with "own") as "$"; [|done].
+ apply prod_update; simpl; [|by rewrite right_id].
+ apply prod_update; simpl; [|done]. apply auth_update_alloc.
+ rewrite Pos.add_comm Qp_plus_comm -pos_op_plus /= -frac_op' -pair_op Some_op.
+ rewrite -{2}(right_id None op (Some ((q' /2)%Qp, _))).
+ apply op_local_update_discrete => _ /=. split; simpl; [|done].
+ apply frac_valid'. rewrite -Hqq' comm -{2}(Qp_div_2 q').
+ apply Qcplus_le_mono_l. rewrite -{1}(Qcanon.Qcplus_0_l (q'/2)%Qp).
+ apply Qcplus_le_mono_r, Qp_ge_0.
+ Qed.
+
+ Lemma WeakAuth_first_tok γ iS :
+ WeakAuth γ (iS, None) ==∗
+ WeakAuth γ (iS, Some $ Cinl ((1/2)%Qp, 1%positive)) ∗ WeakTok γ (1/2)%Qp.
+ Proof.
+ iIntros "own". rewrite -embed_sep -own_op.
+ iMod (@own_update _ arcUR with "own") as "$"; [|done].
+ apply prod_update; simpl; [|by rewrite right_id].
+ apply prod_update; simpl; [done|]. apply auth_update_alloc.
+ apply prod_local_update; simpl; [done|].
+ rewrite /= -(right_id None op (Some _)). by apply op_local_update_discrete.
+ Qed.
+
+ Lemma WeakAuth_new_tok γ iS (q q': frac) n (Hqq' : (q + q')%Qp = 1%Qp):
+ WeakAuth γ (iS, Some (Cinl (q, n))) ==∗
+ WeakAuth γ (iS, Some (Cinl ((q + (q'/2)%Qp)%Qp, (n + 1)%positive))) ∗
+ WeakTok γ (q'/2)%Qp.
+ Proof.
+ iIntros "own". rewrite -embed_sep -own_op.
+ iMod (@own_update _ arcUR with "own") as "$"; [|done].
+ apply prod_update; simpl; [|by rewrite right_id].
+ apply prod_update; simpl; [done|]. apply auth_update_alloc.
+ apply prod_local_update; simpl; [done|].
+ rewrite Pos.add_comm Qp_plus_comm -pos_op_plus /=
+ -frac_op' -pair_op -Cinl_op Some_op.
+ rewrite -{2}(right_id None op (Some $ Cinl ((q' /2)%Qp, _))).
+ apply op_local_update_discrete => _ /=. split; simpl; [|done].
+ apply frac_valid'. rewrite -Hqq' comm -{2}(Qp_div_2 q').
+ apply Qcplus_le_mono_l. rewrite -{1}(Qcanon.Qcplus_0_l (q'/2)%Qp).
+ apply Qcplus_le_mono_r, Qp_ge_0.
+ Qed.
+
+ Lemma StrongAuth_drop_last γ q:
+ StrongAuth γ (Some (q,1%positive)) ∗ StrongTok γ q ==∗
+ StrongAuth γ None.
+ Proof.
+ rewrite -embed_sep -own_op. iIntros "own".
+ iMod (@own_update _ arcUR with "own") as "$"; [|done].
+ apply prod_update; simpl; [|by rewrite right_id].
+ apply prod_update; simpl; [|done].
+ apply auth_update_dealloc. rewrite /= -(right_id None op (Some _)).
+ apply cancel_local_update_unit, _.
+ Qed.
+
+ Lemma StrongAuth_drop γ q q' n:
+ StrongAuth γ (Some ((q + q')%Qp,(1 + n)%positive)) ∗ StrongTok γ q' ==∗
+ StrongAuth γ (Some (q,n)).
+ Proof.
+ rewrite -embed_sep -own_op. iIntros "own".
+ iMod (@own_update _ arcUR with "own") as "$"; [|done].
+ apply prod_update; [|simpl; by rewrite right_id]. apply prod_update; [|done].
+ apply auth_update_dealloc.
+ rewrite -frac_op' -pos_op_plus /= (cmra_comm_L q) -pair_op Some_op.
+ by apply (cancel_local_update_unit (Some _)), _.
+ Qed.
+
+ Lemma WeakAuth_drop_last γ iS q:
+ WeakAuth γ (iS, Some $ Cinl (q,1%positive)) ∗ WeakTok γ q ==∗
+ WeakAuth γ (iS, None).
+ Proof.
+ rewrite -embed_sep -own_op. iIntros "own".
+ iMod (@own_update _ arcUR with "own") as "$"; [|done].
+ apply prod_update; [|by rewrite /= right_id]. apply prod_update; [done|].
+ apply auth_update_dealloc. apply prod_local_update; [done|].
+ rewrite /= -(right_id None op (Some _)). apply cancel_local_update_unit, _.
+ Qed.
+
+ Lemma WeakAuth_drop γ iS (q q': frac) n:
+ WeakAuth γ (iS, Some (Cinl ((q + q')%Qp,(1 + n)%positive))) ∗
+ WeakTok γ q' ==∗
+ WeakAuth γ (iS, Some (Cinl (q,n))).
+ Proof.
+ rewrite -embed_sep -own_op. iIntros "own".
+ iMod (@own_update _ arcUR with "own") as "$"; [|done].
+ apply prod_update; [|simpl; by rewrite right_id]. apply prod_update; [done|].
+ apply auth_update_dealloc. apply prod_local_update; [done|].
+ rewrite -frac_op' -pos_op_plus /= (cmra_comm_L q) -pair_op -Cinl_op Some_op.
+ by apply (cancel_local_update_unit (Some _)), _.
+ Qed.
+
+ Lemma WeakAuth_strong γ iS st q :
+ WeakAuth γ (iS, st) ∗ agown γ (awk_n ((Some q, ε))) -∗ ∃ q', ⌜iS = Some q'⌝.
+ Proof.
+ rewrite -embed_sep -own_op. iIntros "own".
+ iDestruct (own_valid with "own") as %[[_ [VAL _]%auth_valid_discrete_2] _].
+ iPureIntro. move : VAL => /prod_included /= [/option_included [//|[?[? [?[??]]]]] _].
+ subst iS. by eexists.
+ Qed.
+
+ Lemma WeakAuth_valid γ iS st :
+ WeakAuth γ (iS, st) -∗ ⌜st ≠ Some CsumBot⌝.
+ Proof.
+ iIntros "own".
+ iDestruct (@own_valid _ arcUR with "own") as %[[_ [_ [_ VAL]]%auth_valid_discrete] _].
+ simpl in VAL. iPureIntro. by destruct st as [[| |]|].
+ Qed.
+
+ Lemma WeakAuth_drop_strong γ st:
+ WeakAuth γ (Some 1%Qp, st) ∗ agown γ (awk_n ((Some 1%Qp, ε))) ==∗
+ WeakAuth γ (None, st).
+ Proof.
+ rewrite -embed_sep -own_op. iIntros "own".
+ iMod (@own_update _ arcUR with "own") as "$"; [|done].
+ apply prod_update; [|by rewrite /= right_id]. apply prod_update; [done|].
+ apply auth_update_dealloc. apply prod_local_update; [|done].
+ rewrite /= -{1}(right_id None op (Some _)).
+ by apply (cancel_local_update_unit (Some _)), _.
+ Qed.
+
+ Lemma StrWkTok_exclusive γ q :
+ agown γ (awk_n ((Some 1%Qp, ε))) ∗ agown γ (awk_n ((Some q, ε))) -∗ False.
+ Proof.
+ rewrite -embed_sep -own_op. iIntros "own".
+ iDestruct (@own_valid _ arcUR with "own") as %[[_ VAL] _]. simpl in VAL.
+ iPureIntro. move : VAL. rewrite -auth_frag_op pair_op -Some_op frac_op'.
+ move => /auth_valid_discrete /= [/= ? _].
+ have Lt: (1%Qp < (1%Qp + q)%Qp)%Qc. apply Qp_lt_sum. by eexists.
+ apply (irreflexive_eq (R:= Qclt) 1%Qp 1%Qp); [done|].
+ eapply Qclt_le_trans; [apply Lt|done].
+ Qed.
+
+ Lemma StrMoves_full_exclusive γ q Mt' :
+ (∃ Mt, StrMoves γ 1%Qp Mt) -∗ StrMoves γ q Mt' -∗ False.
+ Proof.
+ iDestruct 1 as (Mt) "SM". iIntros "SM'".
+ iDestruct (StrMoves_agree with "[$SM $SM']") as %?. subst Mt'.
+ iDestruct (StrMoves_fractional with "[$SM $SM']") as "SM".
+ iDestruct (@own_valid _ arcUR with "SM") as %[_ [[[[VAL _] _] _] _]].
+ iPureIntro. simpl in VAL.
+ have Lt: (1%Qp < (1%Qp + q)%Qp)%Qc. apply Qp_lt_sum. by eexists.
+ apply (irreflexive_eq (R:= Qclt) 1%Qp 1%Qp); [done|].
+ eapply Qclt_le_trans; [apply Lt|done].
+ Qed.
+
+ Lemma WeakAuth_new_lock γ iS q:
+ WeakAuth γ (iS, None) ==∗
+ WeakAuth γ (iS, Some $ Cinr (Excl (), to_agree q)) ∗ WkLock γ q.
+ Proof.
+ rewrite -embed_sep -own_op. iIntros "own".
+ iMod (@own_update _ arcUR with "own") as "$"; [|done].
+ apply prod_update; [|by rewrite /= right_id]. apply prod_update; [done|]. simpl.
+ apply auth_update_alloc. apply prod_local_update; simpl; [done|].
+ rewrite -(right_id None op (Some _)).
+ by apply op_local_update_discrete.
+ Qed.
+
+ Lemma WeakAuth_lock_agree γ iS st q:
+ WeakAuth γ (iS, st) ∗ WkLock γ q -∗
+ ⌜st ≡ Some (Cinr (Excl tt, to_agree q))⌝.
+ Proof.
+ rewrite -embed_sep -own_op. iIntros "own".
+ iDestruct (@own_valid _ arcUR with "own")
+ as %[[_ [[_ [?|INCL]%option_included]%prod_included [_ VAL]]%auth_valid_discrete_2] _];
+ [done|]. iPureIntro.
+ destruct INCL as (x & y & Eq1 & Eq2 & INCL). simpl in *. inversion Eq1.
+ subst x st. destruct INCL as [Eq|INCL].
+ - inversion Eq as [|? b Eq2 |]. subst. by rewrite -Eq2.
+ - apply csum_included in INCL as [?|[(?&?&?&?)|(?&[u v]&Eq&?&[IN1 IN2]%prod_included)]];
+ [by subst y|done|..].
+ subst. inversion Eq. clear Eq. subst.
+ move : VAL => [VAL1 /to_agree_uninj [? VAL2]]. destruct u as [[]|]; [|done].
+ simpl in *. move : IN2. rewrite -VAL2. move => /to_agree_included <- //.
+ Qed.
+
+ Lemma WeakAuth_unlock γ iS st q :
+ WeakAuth γ (iS, st) ∗ WkLock γ q ==∗ WeakAuth γ (iS, None).
+ Proof.
+ iIntros "own". iDestruct (WeakAuth_lock_agree with "own") as %Eq.
+ rewrite -embed_sep -own_op.
+ iMod (@own_update _ arcUR with "own") as "$"; [|done].
+ apply prod_update; [|by rewrite /= right_id]. apply prod_update; [done|]. simpl.
+ rewrite Eq. apply auth_update_dealloc. apply prod_local_update; [done|].
+ rewrite /= -{1}(right_id None op (Some _)).
+ apply (cancel_local_update_unit (Some _)), _.
+ Qed.
+End ArcGhost.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
new file mode 100644
index 0000000000000000000000000000000000000000..03825ae3030bbd1c245c9dac03937e3118ad3168
--- /dev/null
+++ b/theories/typing/lib/arc.v
@@ -0,0 +1,108 @@
+From Coq.QArith Require Import Qcanon.
+
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import auth csum frac agree.
+From iris.bi Require Import fractional.
+
+From lrust.lang Require Import memcpy arc.
+From lrust.lifetime Require Import at_borrow.
+From lrust.typing Require Export type.
+From lrust.typing Require Import typing option.
+
+From gpfsl.gps Require Import middleware protocols.
+
+Set Default Proof Using "Type".
+
+Definition arcN := lrustN .@ "arc".
+Definition arc_invN := arcN .@ "inv".
+Definition arc_shrN := arcN .@ "shr".
+Definition arc_endN := arcN .@ "end".
+
+Section arc.
+ Context `{!typeG Σ, !arcG Σ}.
+ Local Notation vProp := (vProp Σ).
+
+ (* Preliminary definitions. *)
+ Let P1 ν q := (q.[ν])%I.
+ Instance P1_fractional ν : Fractional (P1 ν).
+ Proof. unfold P1. apply _. Qed.
+ Let P2 l n := (⎡ † l…(2 + n) ⎤ ∗ (l +ₗ 2) ↦∗: λ vl, ⌜length vl = n⌝)%I.
+
+ Definition arc_persist tid ν (γs γw γsw : gname) (l : loc) (ty : type) : vProp :=
+ (is_arc (P1 ν) (P2 l ty.(ty_size)) arc_invN γs γw γsw l ∗
+ (* We use this disjunction, and not simply [ty_shr] here, *)
+ (* because [weak_new] cannot prove ty_shr, even for a dead *)
+ (* lifetime. *)
+ (ty.(ty_shr) ν tid (l +ₗ 2) ∨ [†ν]) ∗
+ □ (1.[ν] ={↑lftN ∪ ↑arc_endN,∅}▷=∗
+ [†ν] ∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗ ⎡ † l…(2 + ty.(ty_size)) ⎤))%I.
+
+ Global Instance arc_persist_ne tid ν γs γw γsw l n :
+ Proper (type_dist2 n ==> dist n) (arc_persist tid ν γs γw γsw l).
+ Proof.
+ unfold arc_persist, P1, P2. move => ???.
+ apply bi.sep_ne.
+ - apply is_arc_contractive; eauto. done.
+ solve_proper_core ltac:(fun _ => f_type_equiv || f_equiv).
+ - solve_proper_core ltac:(fun _ => exact: type_dist2_S || exact: type_dist2_dist ||
+ f_type_equiv || f_contractive || f_equiv).
+ Qed.
+
+ Lemma arc_persist_type_incl tid ν γs γw γsw l ty1 ty2:
+ type_incl ty1 ty2 -∗ arc_persist tid ν γs γw γsw l ty1 -∗ arc_persist tid ν γs γw γsw l ty2.
+ Proof.
+ iIntros "#(Heqsz & Hinclo & Hincls) #(?& Hs & Hvs)".
+ iDestruct "Heqsz" as %->. iFrame "#". iSplit.
+ - iDestruct "Hs" as "[?|?]"; last auto. iLeft. by iApply "Hincls".
+ - iIntros "!# Hν". iMod ("Hvs" with "Hν") as "H". iModIntro. iNext.
+ iMod "H" as "($ & H & $)". iDestruct "H" as (vl) "[??]". iExists _.
+ iFrame. by iApply "Hinclo".
+ Qed.
+
+ Lemma arc_persist_send tid tid' ν γs γw γsw l ty `{!Send ty,!Sync ty} :
+ arc_persist tid ν γs γw γsw l ty -∗ arc_persist tid' ν γs γw γsw l ty.
+ Proof.
+ iIntros "#($ & ? & Hvs)". rewrite sync_change_tid. iFrame "#".
+ iIntros "!# Hν". iMod ("Hvs" with "Hν") as "H". iModIntro. iNext.
+ iMod "H" as "($ & H & $)". iDestruct "H" as (vl) "?". iExists _.
+ by rewrite send_change_tid.
+ Qed.
+
+ (* Model of arc *)
+ (* The ty_own part of the arc type cointains either the
+ shared protocol or the full ownership of the
+ content. The reason is that get_mut does not have the
+ masks to rebuild the invariants. *)
+ Definition full_arc_own l ty tid : vProp :=
+ (l ↦ #1 ∗ (l +ₗ 1) ↦ #1 ∗ ⎡ † l…(2 + ty.(ty_size)) ⎤ ∗
+ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid)%I.
+ Definition shared_arc_own l ty tid : vProp :=
+ (∃ γs γw γsw ν q, arc_persist tid ν γs γw γsw l ty ∗
+ strong_arc q l γs γw γsw ∗ q.[ν])%I.
+ Lemma arc_own_share E l ty tid :
+ ↑lftN ⊆ E →
+ ⎡ lft_ctx ⎤ -∗ full_arc_own l ty tid ={E}=∗ shared_arc_own l ty tid.
+ Proof.
+ iIntros (?) "#LFT (Hl1 & Hl2 & H† & Hown)".
+ iMod (lft_create with "LFT") as (ν) "[Hν #Hν†]"=>//.
+ (* TODO: We should consider changing the statement of
+ bor_create to dis-entangle the two masks such that this is no
+ longer necessary. *)
+ iApply fupd_trans. iApply (fupd_mask_mono (↑lftN))=>//.
+ iMod (bor_create _ ν with "LFT Hown") as "[HP HPend]"=>//. iModIntro.
+ iMod (ty_share with "LFT HP Hν") as "[#? Hν]"; first solve_ndisj.
+ iMod (create_arc (P1 ν) (P2 l ty.(ty_size)) arc_invN with "Hl1 Hl2 Hν")
+ as (γ q') "(#? & ? & ?)".
+ iExists _, _, _. iFrame "∗#". iCombine "H†" "HPend" as "H".
+ iMod (inv_alloc arc_endN _ ([†ν] ∨ _)%I with "[H]") as "#INV";
+ first by iRight; iApply "H". iIntros "!> !# Hν".
+ iMod (inv_open with "INV") as "[[H†|[$ Hvs]] Hclose]";
+ [set_solver|iDestruct (lft_tok_dead with "Hν H†") as ">[]"|].
+ rewrite difference_union_distr_l_L difference_diag_L right_id_L
+ difference_disjoint_L; last solve_ndisj.
+ iMod ("Hν†" with "Hν") as "H". iModIntro. iNext. iApply fupd_trans.
+ iMod "H" as "#Hν". iMod ("Hvs" with "Hν") as "$". iIntros "{$Hν} !>".
+ iApply "Hclose". auto.
+ Qed.
+
+End arc.
\ No newline at end of file