From 8cd2308c8fb995d4b938505ffa59fc0c283e54c3 Mon Sep 17 00:00:00 2001
From: dsac <arnaud@dabyseesaram.info>
Date: Tue, 28 Jun 2022 14:26:35 +0200
Subject: [PATCH] model definition

---
 aneris/examples/crdt/statelib/spec/model.v    |  78 -----
 .../examples/crdt/statelib/user_model/model.v | 127 +++++++
 .../examples/crdt/statelib/user_model/spec.v  | 313 ++++++++++++++++++
 3 files changed, 440 insertions(+), 78 deletions(-)
 delete mode 100644 aneris/examples/crdt/statelib/spec/model.v
 create mode 100644 aneris/examples/crdt/statelib/user_model/model.v
 create mode 100644 aneris/examples/crdt/statelib/user_model/spec.v

diff --git a/aneris/examples/crdt/statelib/spec/model.v b/aneris/examples/crdt/statelib/spec/model.v
deleted file mode 100644
index 923929c..0000000
--- a/aneris/examples/crdt/statelib/spec/model.v
+++ /dev/null
@@ -1,78 +0,0 @@
-From stdpp Require Import base gmap.
-From aneris.examples.crdt.spec Require Import crdt_time crdt_events crdt_denot.
-
-(** * Models for state-based CRDTs **)
-
-(* The "state" in "state-based CRDTs" are join semilattices: i.e.
-   a poset with a lub operation. *)
-Section Lattices.
-
-  Class Lattice (E : Type) := {
-    lat_le : relation E;
-    lat_po :> PartialOrder lat_le;
-    lat_lub : E -> E -> E;
-    lat_lub_le : âˆ€ e1 e2 e3,
-        lat_le e1 e3 -> lat_le e2 e3 -> lat_le (lat_lub e1 e2) e3
-  }.
-
-End Lattices.
-
-Infix "â‰¤_l" := lat_le (at level 80, no associativity).
-Infix "âŠ”_l" := lat_lub (at level 50, left associativity).
-
-Section ModelDef.
-
-  Context {Op : Type}.
-  Context `{!Lattice LatSt, !Log_Time, !EqDecision Op, !Countable Op, !CrdtDenot Op LatSt}.
-
-  (* A set of events is `dep_closed` if it contains every causal dependency of
-     every element of the set. *)
-  Definition dep_closed (s : gset (Event Op)) : Prop :=
-    âˆ€ e e' : Event Op, e âˆˆ s -> e' <_t e -> e' âˆˆ s.
-
-  Lemma dep_closed_union (s s' : gset (Event Op)) :
-    dep_closed s -> dep_closed s' -> dep_closed (s âˆª s').
-  Proof.
-    intros Hsc Hs'c e e' [Hl | Hr]%elem_of_union Hlt.
-    - apply elem_of_union_l.
-      eapply Hsc; eauto.
-    - apply elem_of_union_r.
-      eapply Hs'c; eauto.
-  Qed.
-
-  Class StateCrdtModel := {
-    (* The lub operation must be coherent with respect to denotations.
-       We can assume that s1 and s2 are dep_closed because that is an invariant
-       that is always preserved by state-based CRDTs. *)
-    st_crdtM_lub_coh : âˆ€ (s1 s2 : gset (Event Op)) (st1 st2 st3 : LatSt),
-      âŸ¦ s1 âŸ§ â‡ st1 ->
-      âŸ¦ s2 âŸ§ â‡ st2 ->
-      dep_closed s1 ->
-      dep_closed s2 ->
-      st1 âŠ”_l st2 = st3 <-> âŸ¦ s1 âˆª s2 âŸ§ â‡ st3;
-
-    (* The mutator sends a state, an operation, and the replica id where the
-       mutation is taking place to a new state.  *)
-    st_crdtM_mut (st : LatSt) (op : Op) (repId : nat) : LatSt;
-
-    (* All mutations are monotone, so always end up higher up in the lattice.  *)
-    st_crdtM_mut_mon (st : LatSt) (op : Op) (repId : nat) :
-      st â‰¤_l (st_crdtM_mut st op repId);
-
-    (* Mutations are coherent with denotations. *)
-    st_crdtM_mut_coh (s : gset (Event Op)) (st st' : LatSt) (op : Op) (repId : nat) (ev : (Event Op)) :
-      âŸ¦ s âŸ§ â‡ st ->
-      ev.(EV_Op) = op ->
-      ev.(EV_Orig) = repId ->
-      ev âˆ‰ s ->
-      is_maximum ev (s âˆª {[ ev ]}) ->
-      st' = st_crdtM_mut st op repId <-> âŸ¦ s âˆª {[ ev ]} âŸ§ â‡ st';
-
-    (* The initial CRDT state. *)
-    st_crdtM_init_st : LatSt;
-
-    (* The initial state is the denotation of the empty set of operations. *)
-    st_crdtM_init_st_coh : âŸ¦ âˆ… âŸ§ â‡ st_crdtM_init_st
-  }.
-
-End ModelDef.
diff --git a/aneris/examples/crdt/statelib/user_model/model.v b/aneris/examples/crdt/statelib/user_model/model.v
new file mode 100644
index 0000000..a10e0e8
--- /dev/null
+++ b/aneris/examples/crdt/statelib/user_model/model.v
@@ -0,0 +1,127 @@
+From stdpp Require Import base gmap.
+From aneris.examples.crdt.spec Require Import crdt_denot crdt_events crdt_time.
+From aneris.examples.crdt.statelib.time Require Import time.
+From aneris.examples.crdt.statelib.proof Require Import events.
+
+(** * Models for state-based CRDTs **)
+
+(* The "state" in "state-based CRDTs" are join semilattices: i.e.
+   a poset with a lub operation. *)
+Section Lattices.
+
+  Class Lattice (E : Type) := {
+    lat_le : relation E;
+    lat_po :> PartialOrder lat_le;
+    lat_lub : E -> E -> E;
+    lat_lub_spec :
+      âˆ€ e1 e2,
+        lat_le e1 (lat_lub e1 e2)
+          âˆ§ lat_le e2 (lat_lub e1 e2)
+          âˆ§ âˆ€ e, lat_le e1 e â†’ lat_le e2 e â†’ lat_le (lat_lub e1 e2) e;
+  }.
+
+  (** Properties on the least upper bound *)
+  Lemma lat_lub_idem {E: Type} (L: Lattice E) (e: E) :
+    lat_lub e e = e.
+  Proof.
+    destruct lat_po as [[_ _] Ha].
+    destruct (lat_lub_spec e e) as (Hle1 & Hle2 & Hsp).
+    apply Ha; last assumption.
+    by apply Hsp.
+  Qed.
+  Lemma lat_lub_comm {E: Type} (L: Lattice E) (e e': E) :
+    lat_lub e e' = lat_lub e' e.
+  Proof.
+    destruct lat_po as [[_ _] Ha].
+    destruct (lat_lub_spec e e') as (Hle1 & Hle2 & Hsp).
+    destruct (lat_lub_spec e' e) as (Hle1' & Hle2' & Hsp').
+    apply Ha.
+    - by apply Hsp.
+    - by apply Hsp'.
+  Qed.
+
+  Lemma lat_lub_le_l {E: Type} (L: Lattice E) (e e' e'': E):
+    lat_le e'' e â†’ lat_le e'' (lat_lub e e').
+  Proof.
+    destruct lat_po as [[_ Rt] _].
+    destruct (lat_lub_spec e e') as (A & B & C).
+    intros Hle.
+    by apply (Rt e'' e (lat_lub e e')).
+  Qed.
+  Lemma lat_lub_le_r {E: Type} (L: Lattice E) (e e' e'': E):
+    lat_le e'' e' â†’ lat_le e'' (lat_lub e e').
+  Proof.
+    destruct lat_po as [[_ Rt] _].
+    destruct (lat_lub_spec e e') as (A & B & C).
+    intros Hle.
+    by apply (Rt e'' e' (lat_lub e e')).
+  Qed.
+
+  Lemma lat_lub_assoc {E: Type} (L: Lattice E) (e e' e'': E) :
+    lat_lub e (lat_lub e' e'') = lat_lub (lat_lub e e') e''.
+  Proof.
+    destruct lat_po as [[_ _] Ha].
+    apply Ha.
+    - destruct (lat_lub_spec e (lat_lub e' e'')) as (Hubl & Hubr & Hleast).
+      apply Hleast.
+      + by do 2 apply lat_lub_le_l.
+      + destruct (lat_lub_spec e' e'') as (Hubl' & Hubr' & Hleast').
+        apply (Hleast' (lat_lub (lat_lub e e') e'')).
+        * by apply lat_lub_le_l, lat_lub_le_r.
+        * by apply lat_lub_le_r.
+    - destruct (lat_lub_spec (lat_lub e e') e'') as (Hubl & Hubr & Hleast).
+      apply Hleast.
+      + destruct (lat_lub_spec e e') as (Hubl' & Hubr' & Hleast').
+        apply Hleast'.
+        * by apply lat_lub_le_l.
+        * by apply lat_lub_le_r, lat_lub_le_l.
+      + by do 2 apply lat_lub_le_r.
+  Qed.
+End Lattices.
+
+Infix "â‰¤_l" := lat_le (at level 80, no associativity).
+Infix "âŠ”_l" := lat_lub (at level 50, left associativity).
+
+Section ModelDef.
+
+  Context {Op : Type} {LatSt: Type}.
+  Context `{!Lattice LatSt, !EqDecision Op, !Countable Op, !CrdtDenot Op LatSt}.
+
+  Class StateCrdtModel := {
+    (* The lub operation must be coherent with respect to denotations.
+       We can assume that s1 and s2 are dep_closed because that is an invariant
+       that is always preserved by state-based CRDTs. *)
+    st_crdtM_lub_coh : âˆ€ (s1 s2 : gset (Event Op)) (st1 st2 st3 : LatSt),
+      âŸ¦ s1 âŸ§ â‡ st1 ->
+      âŸ¦ s2 âŸ§ â‡ st2 ->
+      event_set_valid s1 ->
+      event_set_valid s2 ->
+      st1 âŠ”_l st2 = st3 <-> âŸ¦ s1 âˆª s2 âŸ§ â‡ st3;
+
+    (* The mutator sends a state, an operation, and the replica id where the
+       mutation is taking place to a new state.  *)
+    st_crdtM_mut: LatSt â†’ Event Op â†’ LatSt â†’ Prop;
+
+    (* All mutations are monotone, so always end up higher up in the lattice.  *)
+    st_crdtM_mut_mon (st : LatSt) (e: Event Op) (st': LatSt) :
+      st_crdtM_mut st e st' â†’ st â‰¤_l st';
+
+    (* Mutations are coherent with denotations. *)
+    st_crdtM_mut_coh (s : gset (Event Op)) (st st' : LatSt) (ev: Event Op) :
+      âŸ¦ s âŸ§ â‡ st ->
+      event_set_valid s ->
+      ev âˆ‰ s ->
+      is_maximum ev (s âˆª {[ ev ]}) ->
+      st_crdtM_mut st ev st' <->
+      âŸ¦ s âˆª {[ ev ]} âŸ§ â‡ st';
+
+    (* The initial CRDT state. *)
+    st_crdtM_init_st : LatSt;
+
+    (* The initial state is the denotation of the empty set of operations. *)
+    st_crdtM_init_st_coh : âŸ¦ âˆ… âŸ§ â‡ st_crdtM_init_st
+  }.
+
+End ModelDef.
+Arguments StateCrdtModel (Op LatSt) {_ _ _ _}.
+
diff --git a/aneris/examples/crdt/statelib/user_model/spec.v b/aneris/examples/crdt/statelib/user_model/spec.v
new file mode 100644
index 0000000..84cbe1b
--- /dev/null
+++ b/aneris/examples/crdt/statelib/user_model/spec.v
@@ -0,0 +1,313 @@
+From iris.algebra Require Import auth gmap excl csum.
+From aneris.algebra Require Import monotone.
+From aneris.aneris_lang Require Import network resources proofmode.
+From aneris.prelude Require Import time.
+From aneris.aneris_lang.lib Require Import list_proof lock_proof vector_clock_proof serialization_proof.
+From aneris.aneris_lang.program_logic Require Import lightweight_atomic.
+From aneris.examples.crdt.spec Require Import crdt_spec.
+From aneris.examples.crdt.statelib.user_model Require Import model.
+From aneris.examples.crdt.statelib.proof Require Import events.
+
+(** * Specification of the op-based CRDT library *)
+
+Section Params.
+  Context {LogOp LogSt : Type}.
+  Context `{!anerisG Mdl Î£, !EqDecision LogOp, !Countable LogOp}.
+  Context `{!Lattice LogSt}.
+
+  (* User-supplied parameters when using the library. *)
+  Class StLib_Params := {
+    (* Serialization of operations. *)
+    StLib_Serialization : serialization;
+
+    (* CRDT model *)
+    StLib_Denot :> CrdtDenot LogOp LogSt;
+    StLib_Model :> StateCrdtModel LogOp LogSt;
+
+    (* Coherence between logical and physical state: for
+       states, operations, and events (event = operation + timestamp).
+
+       For example, for a counter CRDT the logical state is
+       (morally) an integer, while the physical state is an
+       AnerisLang `val` (containing the integer).
+       The correspondence is trivial in that case, but can
+       be more complicated for other CRDTs. *)
+    StLib_State_Coh : LogSt -> val -> Prop;
+    StLib_Op_Coh : LogOp -> val -> Prop;
+    StLib_Op_Coh_Inj o1 o2 v : StLib_Op_Coh o1 v -> StLib_Op_Coh o2 v -> o1 = o2;
+    StLib_St_Coh : LogSt -> val -> Prop;
+    StLib_St_Coh_Inj o1 o2 v : StLib_St_Coh o1 v -> StLib_St_Coh o2 v -> o1 = o2;
+    StLib_Coh_Ser op v : StLib_Op_Coh op v -> Serializable StLib_Serialization v;
+  }.
+
+  Definition StLib_Event_Coh `{!StLib_Params} (e : Event LogOp) (v : val) : Prop :=
+    âˆƒ valOp valTime valOrig,
+      v = ((valOp, valTime), valOrig)%V âˆ§
+      StLib_Op_Coh e.(EV_Op) valOp âˆ§
+      True âˆ§ (*is_list (elements e.(EV_Time)) valTime âˆ§ TODO: deal with the time representation *)
+      valOrig = #(e.(EV_Orig)).
+
+  Class StLib_Res `{!CRDT_Params} := {
+    StLib_CRDT_Res :> CRDT_Res_Mixin Mdl Î£ LogOp;
+    StLib_InitToken : nat -> iProp Î£;
+    StLib_SocketProto : nat -> socket_interp Î£;
+  }.
+
+End Params.
+
+Global Arguments StLib_Params (LogOp LogSt) {_ _ _}.
+Global Arguments StLib_Res (LogOp) {_ _ _ _ _ _}.
+
+Section Specification.
+
+  (* The following resources are all needed to _state_ the specifications of library
+     functions, but they should _not_ all be provided by the user of the library
+     (e.g. the user provides StLib_UserParams, but not StLib_SysParams).
+
+     To use the library, the user should refer to class StLibSetup below.
+   *)
+  Context `{!anerisG Mdl Î£,
+            !EqDecision LogOp,
+            !Countable LogOp,
+            !Lattice LogSt,
+            !StLib_Params LogOp LogSt,
+            !StLib_SysParams Î£,
+            !CRDT_Params,
+            !StLib_Res LogOp}.
+
+  Definition get_state_spec (get_state : val) (repId : nat) (addr : socket_address) : iProp Î£ :=
+    âŒœCRDT_Addresses !! repId = Some addrâŒ -âˆ—
+     <<< âˆ€âˆ€ (s1 s2 : gset (Event LogOp)), LocState repId s1 s2 >>>
+       get_state #() @[ip_of_address addr] â†‘CRDT_InvName
+     <<<â–· âˆƒâˆƒ (s2' : gset (Event LogOp)) (phys_st : val) (log_st : LogSt), RET phys_st;
+             âŒœs2 âŠ† s2'âŒ âˆ—
+             LocState repId s1 s2' âˆ—
+             âŒœStLib_State_Coh log_st phys_stâŒ âˆ—
+             âŒœâŸ¦s1 âˆª s2'âŸ§ â‡ log_stâŒ >>>.
+
+  Definition mutator_spec (mutator : val) (repId : nat) (addr : socket_address) : iProp Î£ :=
+    âˆ€ (op : val) (log_op : LogOp),
+    âŒœCRDT_Addresses !! repId = Some addrâŒ -âˆ—
+    âŒœStLib_Op_Coh log_op opâŒ -âˆ—
+    <<< âˆ€âˆ€ (h s1 s2 : gset (Event LogOp)),
+           GlobState h âˆ—
+           LocState repId s1 s2 >>>
+      mutator op @[ip_of_address addr] â†‘CRDT_InvName
+    <<<â–· âˆƒâˆƒ (e : Event LogOp) (h' s1' s2' : gset (Event LogOp)), RET #();
+           âŒœe.(EV_Op) = log_opâŒ âˆ—
+           âŒœe.(EV_Orig) = repIdâŒ âˆ—
+           âŒœh' = h âˆª {[ e ]}âŒ âˆ—
+           âŒœs1' = s1 âˆª {[ e ]}âŒ âˆ—
+           âŒœs2 âŠ† s2'âŒ âˆ—
+           âŒœe âˆ‰ hâŒ âˆ—
+           âŒœe âˆ‰ s1âŒ âˆ—
+           âŒœe âˆˆ Maximals h'âŒ âˆ—
+           âŒœMaximum (s1' âˆª s2') = Some eâŒ âˆ—
+           GlobState h' âˆ—
+           LocState repId s1' s2' >>>.
+
+  Definition effect_spec (effect_fn : val) : iProp Î£ :=
+    âˆ€ (addr : socket_address) (ev st : val) (s : (event_set LogOp))
+      (log_ev : Event LogOp) (log_st : LogSt),
+    {{{ âŒœStLib_Event_Coh log_ev evâŒ âˆ—
+        âŒœStLib_State_Coh log_st stâŒ âˆ—
+        âŒœâŸ¦ s âŸ§ â‡ log_stâŒ âˆ—
+        âŒœlog_ev âˆ‰ sâŒ âˆ—
+        âŒœmaximal log_ev (s âˆª {[ log_ev ]})âŒ âˆ—
+        âŒœevents_ext (s âˆª {[ log_ev ]})âŒ âˆ—
+        âŒœevents_total_order (s âˆª {[ log_ev ]})âŒ
+    }}}
+      effect_fn ev st @[ip_of_address addr]
+    {{{ st', RET st';
+        âˆƒ (log_st' : LogSt),
+          âŒœStLib_State_Coh log_st' st'âŒ âˆ—
+          âŒœst_crdtM_mut log_st log_ev log_st'âŒ
+    }}}.
+
+  Definition merge_spec (merge_fn : val) : iProp Î£ :=
+    âˆ€ (addr : socket_address) (st st' : val) (s s' : (event_set LogOp))
+      (log_st log_st' : LogSt),
+    {{{ âŒœStLib_State_Coh log_st stâŒ âˆ—
+        âŒœStLib_State_Coh log_st' st'âŒ âˆ—
+        âŒœâŸ¦ s âŸ§ â‡ log_stâŒ âˆ—
+        âŒœâŸ¦ s' âŸ§ â‡ log_st'âŒ
+    }}}
+      merge_fn st st' @[ip_of_address addr]
+    {{{ st'', RET st'';
+        âˆƒ (log_st'' : LogSt),
+          âŒœStLib_State_Coh log_st'' st''âŒ âˆ—
+          âŒœlat_lub log_st log_st' = log_st''âŒ
+    }}}.
+
+  Definition init_st_fn_spec (init_st_fun : val) : iProp Î£ :=
+    âˆ€ addr,
+      {{{ True }}}
+        init_st_fun #() @[ip_of_address addr]
+      {{{ v, RET v; âŒœStLib_State_Coh st_crdtM_init_st vâŒ }}}.
+
+  Definition crdt_triplet_spec (crdt_triplet : val) : iProp Î£ :=
+    âˆƒ (init_st_fn effect_fn merge_fn : val),
+      âŒœcrdt_triplet = PairV (PairV init_st_fn effect_fn) merge_fnâŒ âˆ—
+      init_st_fn_spec init_st_fn  âˆ—
+      effect_spec effect_fn âˆ—
+      merge_spec merge_fn.
+
+  Definition crdt_fun_spec (crdt_fun : val) : iProp Î£ :=
+    âˆ€ addr,
+      {{{ True }}}
+        crdt_fun #() @[ip_of_address addr]
+      {{{ v, RET v; crdt_triplet_spec v }}}.
+
+  Definition init_spec_for_specific_crdt (init : val)  : iProp Î£ :=
+    âˆ€ (repId : nat) (addr : socket_address) (fixedAddrs : gset socket_address)
+      (addrs_val : val),
+        {{{ âŒœis_list CRDT_Addresses addrs_valâŒ âˆ—
+            âŒœCRDT_Addresses !! repId = Some addrâŒ âˆ—
+            âŒœaddr âˆˆ fixedAddrsâŒ âˆ—
+            fixed fixedAddrs âˆ—
+            ([âˆ— list] i â†¦ z âˆˆ CRDT_Addresses, z â¤‡ StLib_SocketProto i) âˆ—
+            addr â¤³ (âˆ…, âˆ…) âˆ—
+            free_ports (ip_of_address addr) {[port_of_address addr]} âˆ—
+            StLib_InitToken repId
+        }}}
+          init addrs_val #repId @[ip_of_address addr]
+        {{{ get_state_val mutator_val, RET (get_state_val, mutator_val);
+            LocState repId âˆ… âˆ… âˆ—
+            get_state_spec get_state_val repId addr âˆ—
+            mutator_spec mutator_val repId addr
+        }}}.
+
+    Definition init_spec (init : val) : iProp Î£ :=
+    âˆ€ (repId : nat) (addr : socket_address) (fixedAddrs : gset socket_address)
+      (addrs_val crdt_val : val),
+        {{{ âŒœis_list CRDT_Addresses addrs_valâŒ âˆ—
+            âŒœCRDT_Addresses !! repId = Some addrâŒ âˆ—
+            âŒœaddr âˆˆ fixedAddrsâŒ âˆ—
+            fixed fixedAddrs âˆ—
+            ([âˆ— list] i â†¦ z âˆˆ CRDT_Addresses, z â¤‡ StLib_SocketProto i) âˆ—
+            addr â¤³ (âˆ…, âˆ…) âˆ—
+            free_ports (ip_of_address addr) {[port_of_address addr]} âˆ—
+            StLib_InitToken repId âˆ—
+            crdt_fun_spec crdt_val
+        }}}
+          init addrs_val #repId crdt_val @[ip_of_address addr]
+        {{{ get_state_val mutator_val, RET (get_state_val, mutator_val);
+            LocState repId âˆ… âˆ… âˆ—
+            get_state_spec get_state_val repId addr âˆ—
+            mutator_spec mutator_val repId addr
+        }}}.
+
+  (** * Simplified specs for when we have full ownership *)
+
+  Definition simplified_get_state_spec (get_state : val) (repId : nat) (addr : socket_address) : iProp Î£ :=
+    âˆ€ (s1 s2 : event_set LogOp),
+      âŒœCRDT_Addresses !! repId = Some addrâŒ -âˆ—
+      {{{ LocState repId s1 s2 }}}
+        get_state #() @[ip_of_address addr]
+      {{{ phys_st log_st, RET phys_st; âˆƒ s2',
+          âŒœs2 âŠ† s2'âŒ âˆ—
+          LocState repId s1 s2' âˆ—
+          âŒœStLib_State_Coh log_st phys_stâŒ âˆ—
+          âŒœâŸ¦ s1 âˆª s2' âŸ§ â‡ log_stâŒ
+      }}}.
+
+  Lemma read_spec_implies_simplified_spec get_state repId addr :
+    get_state_spec get_state repId addr âŠ¢ simplified_get_state_spec get_state repId addr.
+  Proof.
+    iIntros "#Hgetstate".
+    rewrite /simplified_get_state_spec.
+    iIntros (s1 s2) "#Haddr !>". iIntros (Î¦) "Hloc HÎ¦".
+    iApply ("Hgetstate" with "[//]").
+    iExists s1, s2; iFrame.
+    iApply fupd_mask_intro; [set_solver |].
+    iIntros "Hcl !>".
+    iIntros (? ? ?) "(? & ? & ?)". iMod "Hcl". iModIntro.
+    iApply "HÎ¦".
+    eauto with iFrame.
+  Qed.
+
+  Definition simplified_mutator_spec (mutator : val) repId addr : iProp Î£ :=
+    âˆ€ (op : val) (log_op : LogOp) (h s1 s2 : event_set LogOp),
+     âŒœCRDT_Addresses !! repId = Some addrâŒ -âˆ—
+     âŒœStLib_Op_Coh log_op opâŒ -âˆ—
+     {{{ GlobState h âˆ—
+         LocState repId s1 s2
+     }}}
+        mutator op @[ip_of_address addr]
+     {{{ RET #();
+         âˆƒ (e : Event LogOp) (h' s1' s2' : gset (Event LogOp)),
+           âŒœe.(EV_Op) = log_opâŒ âˆ—
+           âŒœe.(EV_Orig) = repIdâŒ âˆ—
+           âŒœh' = h âˆª {[ e ]}âŒ âˆ—
+           âŒœs1' = s1 âˆª {[ e ]}âŒ âˆ—
+           âŒœs2 âŠ† s2'âŒ âˆ—
+           âŒœe âˆ‰ hâŒ âˆ—
+           âŒœe âˆ‰ s1âŒ âˆ—
+           âŒœe âˆˆ Maximals h'âŒ âˆ—
+           âŒœMaximum (s1' âˆª s2') = Some eâŒ âˆ—
+           GlobState h' âˆ—
+           LocState repId s1' s2' }}}.
+
+  Lemma mutator_spec_implies_simplified_mutator mutator repId addr :
+    mutator_spec mutator repId addr âŠ¢ simplified_mutator_spec mutator repId addr.
+  Proof.
+    iIntros "#Hmutator" (op log_op h s1 s2) "#Haddr %Hcoh".
+    iModIntro.
+    iIntros (Î¦) "[Hglob Hloc] HÎ¦".
+    iApply ("Hmutator" with "[//]"); [done |].
+    iApply fupd_mask_intro; [set_solver |].
+    iIntros "Hcl". iExists h, s1, s2. iFrame.
+    iModIntro.
+    iIntros (e h' s1' s2') "(? & ? & ? & ? & ? & ? & ? & ? & ?)".
+    iMod "Hcl". iModIntro.
+    iApply "HÎ¦". eauto with iFrame.
+  Qed.
+
+End Specification.
+
+(** * Library interface **)
+Section StLibSetup.
+
+  Class StLib_Init_Function := { init : val }.
+
+  Context {LogOp LogSt : Type}.
+  Context `{!anerisG Mdl Î£, !EqDecision LogOp, !Countable LogOp,
+            !CRDT_Params, !Lattice LogSt, !StLib_Params LogOp LogSt, !StLib_Init_Function}.
+
+  Class StLibSetup :=
+      StLibSetup_Init E :
+      True âŠ¢ |={E}=> âˆƒ (Res : StLib_Res LogOp),
+        GlobInv âˆ—
+        GlobState âˆ… âˆ—
+        ([âˆ— list] i â†¦ _ âˆˆ CRDT_Addresses, StLib_InitToken i) âˆ—
+        init_spec init.
+
+End StLibSetup.
+
+Section RAs.
+
+  Context {LogOp LogSt : Type}.
+  Context `{!EqDecision LogOp, !Countable LogOp}.
+
+  Definition oneShotR := csumR (exclR unitO) (agreeR unitO).
+
+  Class StLibG Î£ := {
+      StLibG_auth_gset_ev :> inG Î£ (authUR (gsetUR (Event LogOp)));
+      StLibG_frac_agree :> inG Î£ (prodR fracR (agreeR (gsetO (Event LogOp))));
+      StLibG_mono :> inG Î£ (authUR (monotoneUR (@cc_subseteq LogOp _ _)));
+      StLibG_lockG :> lockG Î£;
+      StLibG_oneshot :> inG Î£ oneShotR;
+  }.
+
+  Definition OPLIBÎ£  : gFunctors :=
+    #[GFunctor (authUR (gsetUR (Event LogOp)));
+      GFunctor (prodR fracR (agreeR (gsetO (Event LogOp))));
+      GFunctor (authUR (monotoneUR (@cc_subseteq LogOp _ _)));
+      lockÎ£;
+      GFunctor oneShotR].
+
+  Global Instance subG_OPLIBÎ£ {Î£} : subG OPLIBÎ£ Î£ â†’ StLibG Î£.
+  Proof. constructor; solve_inG. Qed.
+
+End RAs.
+
-- 
GitLab