G-Counter CRDT

A Grow-only Counter where each process maintains a local counter. Processes increment their own counter and merge others’ state via pointwise max. The global value is the sum of all local counters.

The spec

Source

module GCounter

// G-Counter (Grow-only Counter) CRDT
// Each of N+1 processes maintains a local counter.
// Increment: process p increments its own counter.
// Merge: process p merges another process q's counter (pointwise max).
// The global counter value is the sum of all local counters.
//
// Key properties:
// - Monotonicity: the global value never decreases.
// - Convergence: if all increments stop and merges propagate, all processes agree.
//
// Use: specl check g-counter.specl -c N=2 -c Max=3 --no-deadlock
// Verified: N=2 Max=3 -> OK (188K states, 1.3s)

const N: 0..4
const Max: 1..5

// counter[p][q] = process p's view of process q's count
var counter: Dict[0..N, Dict[0..N, 0..Max]]

// Shadow variable tracking sum before each step (for monotonicity check)
var prev_sum: 0..255

func GlobalSum() {
    let s0 = counter[0][0] + counter[0][1] in
    if N >= 2 then s0 + counter[0][2]
    else s0
}

init {
    counter = {p: {q: 0 for q in 0..N} for p in 0..N};
    prev_sum = 0;
}

// Process p increments its own counter
action Increment(p: 0..N) {
    require counter[p][p] < Max;
    prev_sum = GlobalSum();
    counter = counter | {p: counter[p] | {p: counter[p][p] + 1}};
}

// Process p merges process q's state (pointwise max)
action Merge(p: 0..N, q: 0..N) {
    require p != q;
    // Only merge if q has something p doesn't know about
    require any r in 0..N: counter[q][r] > counter[p][r];
    prev_sum = GlobalSum();
    counter = counter | {p:
        {r: if counter[q][r] > counter[p][r] then counter[q][r] else counter[p][r]
         for r in 0..N}
    }
}

// Monotonicity: the global value (from any process's view) never decreases.
// We check process 0's view as representative.
invariant Monotonic {
    let cur = GlobalSum() in
    cur >= prev_sum
}

// Local monotonicity: individual counters never decrease
invariant CountersNonNegative {
    all p in 0..N: all q in 0..N: counter[p][q] >= 0
}

// Consistency: if two processes have identical views, they compute the same total
// (This is trivially true by construction, but documents the CRDT contract)
invariant SameViewSameValue {
    all p in 0..N: all q in 0..N:
        (all r in 0..N: counter[p][r] == counter[q][r])
        implies
        (let sp = counter[p][0] + counter[p][1] in
         let sq = counter[q][0] + counter[q][1] in
         if N >= 2 then sp + counter[p][2] == sq + counter[q][2]
         else sp == sq)
}

What to notice

• Nested dicts. counter: Dict[0..N, Dict[0..N, 0..Max]] — counter[p][q] is process p’s view of process q’s count.
• Nested dict update. counter = counter | {p: counter[p] | {p: counter[p][p] + 1}} — updates the inner dict for the incrementing process.
• Conditional comprehension. The Merge action uses if counter[q][r] > counter[p][r] then counter[q][r] else counter[p][r] inside a dict comprehension to compute the pointwise max.
• func and let. GlobalSum() is a pure function used in the Monotonic invariant via let cur = GlobalSum().
• Shadow variable for temporal reasoning. prev_sum tracks the previous global sum to verify monotonicity as a safety property (since temporal operators are not yet implemented).

specl check g-counter.specl -c N=2 -c Max=3 --no-deadlock