GCounter.idr

GCounter.idr

module GCounter

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 :: x) = (a + 1) :: x
updateGC (FS y) (x :: xs) = x :: updateGC y xs

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

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

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

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) =
  let inductiveHypothesis = mergeIsAssociative x y z
  in rewrite inductiveHypothesis
  in rewrite (maximumAssociative a k j)
  in Refl

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