def KCounter.valid

bend-kit-crdt@0.2.0.0 · crdt.bend:325

import Base

325# A valid state has strictly ascending IDs and no 0 count, so each counter has one form.
326def KCounter.valid(~K: Data, ~cmp: K -> K -> Cmp, s: KCounter<K>) -> Bool:
327  match s:
328    case KNil{}:
329      True{}
330    case KCon{+x, c, +r}:
331      Bool.and(Bool.and(U32.is_ne(c, 0), KCounter.above(~K, ~cmp, r, x)), KCounter.valid(~K, ~cmp, r))