Demonstrate that the two styles of CRDTs are equivalent

proofs/crdt/equivalence.v

@@ -0,0 +1,82 @@
+(**************************************************************************)
+(**************************************************************************)
+(****                                                                  ****)
+(****   Equivalence of state-based and operation-based conflict-free   ****)
+(****   replicated data types                                          ****)
+(****                                                                  ****)
+(**************************************************************************)
+(**************************************************************************)
+
+Require Import Coq.Lists.List.
+Require Import main.tactics.
+
+Require main.crdt.operation_crdt.
+
+Import Coq.Lists.List.ListNotations.
+
+(* We can emulate a state-based CRDT with an operation-based CRDT. *)
+
+Definition operation_crdt_data_from_state_crdt
+  [A Q]
+  (crdt : state_crdt.Crdt A Q)
+: operation_crdt.CrdtData A Q
+:=
+  {|
+    operation_crdt.State := crdt.(state_crdt.State);
+    operation_crdt.Operation := crdt.(state_crdt.State);
+    operation_crdt.initial := crdt.(state_crdt.initial);
+    operation_crdt.update x s := crdt.(state_crdt.update) x s;
+    operation_crdt.interpret o s := crdt.(state_crdt.merge) o s;
+    operation_crdt.query s := crdt.(state_crdt.query) s;
+    operation_crdt.Precondition _ _ := True;
+  |}.
+
+Program Definition operation_crdt_from_state_crdt
+  [A Q]
+  (crdt : state_crdt.Crdt A Q)
+: operation_crdt.Crdt (operation_crdt_data_from_state_crdt crdt)
+:= {| operation_crdt.commutativity := _ |}.
+Next Obligation.
+  clean.
+  pose proof (crdt.(state_crdt.semilattice _ _)).
+  rewrite state_crdt.associativity
+    with (initial := crdt.(state_crdt.initial)); search.
+  rewrite state_crdt.commutativity
+    with (initial := crdt.(state_crdt.initial)) (x := o1); search.
+Qed.
+
+(*
+  We can emulate an operation-based CRDT with a state-based CRDT if the
+  delivery precondition and equality of operations are decidable.
+*)
+
+#[local] Obligation Tactic := auto. (* `search` diverges here, sadly. *)
+
+Program Definition state_crdt_from_operation_crdt
+  [A Q]
+  [crdt_data : operation_crdt.CrdtData A Q]
+  (crdt : operation_crdt.Crdt crdt_data)
+  (precondition :
+    forall s o,
+    {crdt_data.(operation_crdt.Precondition) s o} +
+    {~ crdt_data.(operation_crdt.Precondition) s o}
+  )
+  (equal :
+    forall o1 o2 : crdt_data.(operation_crdt.Operation),
+    {o1 = o2} + {o1 <> o2}
+  )
+: state_crdt.Crdt A Q :=
+  {|
+    state_crdt.State :=
+      list crdt_data.(operation_crdt.Operation) *
+      list crdt_data.(operation_crdt.Operation) *
+      crdt_data.(operation_crdt.State);
+    state_crdt.initial := ([], [], crdt_data.(operation_crdt.initial));
+    state_crdt.merge := _;
+    state_crdt.update _ _ := _;
+    state_crdt.query '(_, _, s) := crdt_data.(operation_crdt.query) s;
+  |}.
+Next Obligation.
+Admitted.
+Next Obligation.
+Admitted.