Adding (e < e') wrt evid → (e <_t e') to the notion of local validity

aneris/examples/crdt/statelib/STS/lst.v

@@ -6,7 +6,7 @@ From aneris.examples.crdt.statelib.proof Require Import utils events.
 From aneris.examples.crdt.statelib.time Require Import time maximality.
 
 Section Lst_definition.
-  Context `{!anerisG Mdl Σ, !CRDT_Params}.
+  Context `{!CRDT_Params}.
   Context `{Op: Type, !EqDecision Op, !Countable Op}.
 
   Definition Lst : Type := event_set Op.
@@ -40,9 +40,38 @@ Section Lst_definition.
       VLst_orig_max : event_set_orig_max_len ls;
       VLst_evid_mon : event_set_evid_mon ls;
       VLst_evid_incl_event: event_set_evid_incl_event ls;
+      VLst_evid_incl_time_le: ∀ ev ev', ev ∈ ls → ev' ∈ ls → get_evid ev' ∈ EV_Time ev → ev' ≤_t ev;
     }.
     Arguments VLst_orig {_ _ _} ls.
 
 End Lst_definition.
 Arguments Lst (Op) {_ _}.
 
+
+
+Section Lst_helper.
+  Context `{!CRDT_Params}.
+  Context `{Op: Type, !EqDecision Op, !Countable Op}.
+
+  Lemma Lst_Validity_implies_event_set_valid (s: Lst Op):
+    Lst_Validity s → event_set_valid s.
+  Proof.
+    intros [Hdc Horig_comp Hext_eid Hext_time Horig Hseqid Horig_depseq Hseqnum Horig_max Hevis_mon Hevis_incl_ev].
+    split; first done.
+    intros e e' He_in He'_in. split.
+    - intros Hevs_orig.
+      destruct Horig_comp with e e' as [? |[-> |?]]; try done.
+      + left. by apply strict_include.
+      + by left.
+      + right. by apply strict_include.
+    - intros Hevs_eqt.
+      by destruct Hext_time with e e'.
+  Qed.
+
+  Lemma Lst_Validity_implies_events_ext (s: Lst Op):
+    Lst_Validity s → events_ext s.
+  Proof. by intros []. Qed.
+  Lemma Lst_Validity_implies_same_orig_comparable (s: Lst Op):
+    Lst_Validity s → event_set_same_orig_comparable s.
+  Proof. by intros []. Qed.
+End Lst_helper.

aneris/examples/crdt/statelib/STS/merge.v

@@ -109,6 +109,17 @@ Section Gst_merge_local_valid.
     - intros ev [Hev_in | Hev_in%(iffLR (elem_of_subseteq s (g.2 !!! j)) Hs_incl)]%elem_of_union.
       + by apply (VLst_evid_incl_event _ (VGst_lhst_valid g Hv i)).
       + by apply (VLst_evid_incl_event _ (VGst_lhst_valid g Hv j)).
+   - intros x y [Hx_in | Hx_in%Hs_incl]%elem_of_union [Hy_in | Hy_in%Hs_incl]%elem_of_union.
+    + by apply (VLst_evid_incl_time_le _ (VGst_lhst_valid _ Hv i)).
+    + by apply (VLst_evid_incl_time_le _ (VGst_hst_valid _ Hv));
+        [ apply gst_valid_inclusion with i
+        | apply gst_valid_inclusion with j ].
+    + by apply (VLst_evid_incl_time_le _ (VGst_hst_valid _ Hv));
+        [ apply gst_valid_inclusion with j
+        | apply gst_valid_inclusion with i ].
+    + by apply (VLst_evid_incl_time_le _ (VGst_hst_valid _ Hv));
+        [ apply gst_valid_inclusion with j
+        | apply gst_valid_inclusion with j ].
   Qed.
 
   Lemma merge_loc_valid

aneris/examples/crdt/statelib/STS/mutation.v

@@ -924,6 +924,20 @@ Section Gst_mutator_local_valid.
     - by apply mutator_local_orig_max_len_preservation.
     - by apply mutator_local_evid_mon_preservation.
     - by apply mutator_local_evid_incl_event.
+    - intros ev ev'
+      [Hev_in | ->%elem_of_singleton]%elem_of_union
+      [Hev'_in | ->%elem_of_singleton]%elem_of_union
+      Hin;
+      [ by apply (VLst_evid_incl_time_le _ Hold_valid) | | | done ];
+      last (apply fresh_event_time_mon; by destruct Hold_valid).
+      exfalso.
+      apply (VLst_dep_closed _ (VGst_lhst_valid _ Hv orig) _ _ Hev_in) in Hin
+        as (ev' & ev'_orig & ev'_eid).
+      apply mutator_ext_evid_preservation with g op orig in ev'_eid; try done.
+      + apply (fresh_event_is_fresh (g.2 !!! orig) orig op (VGst_lhst_valid _ Hv orig)).
+        by rewrite-/fev -ev'_eid.
+      + simpl. by apply elem_of_union_l, gst_valid_inclusion with orig.
+      + simpl. by apply elem_of_union_r, elem_of_singleton.
   Qed.
 
   Lemma mutator_hst_valid
@@ -944,6 +958,38 @@ Section Gst_mutator_local_valid.
     - by apply mutator_orig_max_len_preservation.
     - by apply mutator_evid_mon_preservation.
     - by apply mutator_evid_incl_event_preservation.
+    - simpl.
+      intros ev ev'
+        [Hev_in | ->%elem_of_singleton ]%elem_of_union
+        [Hev'_in | ->%elem_of_singleton ]%elem_of_union Hin; try done;
+        first by apply (VLst_evid_incl_time_le _ (VGst_hst_valid _ Hv)).
+      + 
+        apply (VLst_dep_closed _ (VGst_hst_valid _ Hv) _ _ Hev_in) in Hin
+          as (ev' & ev'_orig & ev'_eid).
+        apply mutator_ext_evid_preservation with g op orig in ev'_eid; try done.
+        * destruct (fresh_event_is_fresh_global g orig op Hv).
+          by rewrite-/fev -ev'_eid.
+        * simpl. by apply elem_of_union_l.
+        * simpl. by apply elem_of_union_r, elem_of_singleton.
+      + apply fresh_event_time_mon;
+          try by destruct (VGst_lhst_valid _ Hv orig).
+        destruct (mutator_local_dep_closed_preservation (g.2 !!! orig) op orig (VGst_lhst_valid _ Hv orig))
+          with fev (get_evid ev')
+          as (x & [Hx_in | ->%elem_of_singleton]%elem_of_union & Hx_evid).
+        * by apply elem_of_union_r, elem_of_singleton.
+        * assumption.
+        * apply mutator_ext_evid_preservation with g op orig in Hx_evid as ->;
+            simpl; try done;
+            [by apply elem_of_union_l, gst_valid_inclusion with orig
+            | by apply elem_of_union_l].
+        * exfalso.
+          assert (ev' ∈ g.1) as Htmp; first exact Hev'_in.
+          epose (mutator_ext_evid_preservation g op orig Hv fev ev' _ _ Hx_evid).
+          rewrite<- e in Hev'_in.
+          exact (fresh_event_is_fresh_global g orig op Hv Hev'_in).
+          Unshelve.
+          by apply elem_of_union_r, elem_of_singleton.
+          by apply elem_of_union_l.
   Qed.
 
   Lemma mutator_global_valid
@@ -959,5 +1005,25 @@ Section Gst_mutator_local_valid.
     - by apply mutator_lhst_valid.
   Qed.
 
+  Lemma fresh_events_mutator_global_maximals
+    (g: Gst Op) (op: Op) (orig: fRepId):
+    let fev := fresh_event (g.2 !!! orig) op orig in
+    Gst_Validity g →
+    fev ∈ Maximals (g.1 ∪ {[fev]}).
+  Proof.
+    intros fev Hv.
+    apply Maximals_correct.
+    split; first by apply elem_of_union_r, elem_of_singleton.
+    intros e [He_in| ->%elem_of_singleton]%elem_of_union;
+      last by apply TM_lt_irreflexive.
+    intros Himp.
+    assert (get_evid fev ∈ time fev).
+    { apply (mutator_local_evid_incl_event (g.2 !!! orig) op orig
+        (VGst_lhst_valid _ Hv orig) fev).
+      by apply elem_of_union_r, elem_of_singleton. }
+    assert (get_evid fev ∈ time e).
+    { admit. }
+  Admitted.
+
 End Gst_mutator_local_valid.