GCounter.idr

GCounter.idr

module GCounter

import Data.Fin
import Data.Vect

||| GCounter is a Conflict Free Replicated Datatype.
||| For a definition, see https://en.wikipedia.org/wiki/Conflict-free_replicated_data_type
||| It provides update, query and merge operations.
||| merge is commutative, associative and idempotent.
data GCounter : Nat -> Type where
  Nil : GCounter Z
  (::) : (a: Nat) -> GCounter k -> GCounter (S k)

total
initGC: (size: Nat) -> GCounter size
initGC Z = []
initGC (S k) = Z :: initGC k

total
updateGC: (id: Fin size) -> GCounter size -> GCounter size
updateGC FZ (a :: xs) = (a + 1) :: xs
updateGC (FS y) (x :: xs) = x :: updateGC y xs

total
queryGC: GCounter size -> Nat
queryGC [] = 0
queryGC (a :: xs) = a + queryGC xs

private total
toVect: GCounter n -> Vect n Nat
toVect [] = []
toVect (a :: x) = a :: toVect x

||| defines a partial ordering for GCounter
total
compareGC: GCounter size -> GCounter size -> Bool
compareGC x y = let zipped = zip (toVect x) (toVect y)
                  in all (\e => (fst e) <= (snd e)) zipped

total
mergeGC: GCounter size -> GCounter size -> GCounter size
mergeGC [] [] = []
mergeGC (a :: x) (k :: y) = (maximum a k) :: mergeGC x y

total
mergeIsCommutative: (x: GCounter size) -> (y: GCounter size) -> x `mergeGC` y = y `mergeGC` x
mergeIsCommutative [] [] = Refl
mergeIsCommutative (a :: x) (k :: y) = rewrite maximumCommutative a k
                                       in rewrite mergeIsCommutative x y
                                       in Refl

total
mergeIsAssociative: (x: GCounter size) -> (y: GCounter size) -> (z: GCounter size) ->
                    x `mergeGC` (y `mergeGC` z) = (x `mergeGC` y) `mergeGC` z
mergeIsAssociative [] [] [] = Refl
mergeIsAssociative (a :: x) (k :: y) (j :: z) = rewrite maximumAssociative a k j
                                                in rewrite mergeIsAssociative x y z
                                                in Refl

total
mergeIsIdempotent: (x: GCounter size) -> x `mergeGC` x = x
mergeIsIdempotent [] = Refl
mergeIsIdempotent (a :: xs) = rewrite maximumIdempotent a
                              in rewrite mergeIsIdempotent xs
                              in Refl