Continuing my previous post on proving properties about
CRDTs, specifically G-Counters, we’ll now look at the PN-Counter, a
counter which allows the value to both increment and decrement while
guaranteeing convergence. Since this builds off of the lemmas proven in
the previous post, I highly recommend you read that post
first.

First, let’s define a PN-Counter as a product of two G-Counters.
We’ll use one set for counting the increments, and one for counting the
decrements.

Then, let’s define increment and decrement functions for a particular
actor, which call the G-Counter increment function on each set. In
this example, we use fst and snd to destructure the PN-Counter
into two seperate counters, and then after we perform the increment we
use pair, the product constructor, to rebuild the PN-Counter.

Let’s define a function to reveal the current value of the PN-Counter,
by subtracting the values of each counter.

Then, let’s define merge, comparsion, and equality functions, which
leverage the functions we’ve defined over G-Counters.

Cool. Now, let’s start proving things.

First, let’s prove that the merge operation commutes. Similar to our
G-Counter proof, we can simply perform the necessary destructuring of
the PN-Counter type, and then apply the lemma we’ve previously defined
which shows that the merge operation on clocks commute.

Same thing, we can use the existing lemmas we’ve proven about
G-Counter’s and their merge operation, and apply it to prove that, in
addition to being commutative, they are also associative and idempotent.

Now, let’s prove that both the increment and decrement operations
monotonically advance the structure. This is extremely trivial, as
we’ve already proven that incrementing an individual G-Counter
monotonically advances the structure, given that the increment and
decrement are both only increment operations operating on either side of
a product.

Now, let’s confirm that the merge operation of the PN-Counter cause
the data structure to monotonically advance. This proof is trivial,
given we’ve already proven that this property holds true for the
G-Counter. We can simply apply the theorem we’ve already defined.