BoundedCounter

A bounded / escrow counter: a shared budget pre-divided into per-replica quotas, with the invariant quota(r) >= 0 enforced locally and the derived global invariant "total spent <= total received" held by construction. No coordination is required for the local check — only for redistributing quota via transfer.

Internally, three per-replica state components — every one a join-semilattice, so piece is just the per-component merge:

• initial[r] — r's seed quota (set by init, immutable after).

• transfers[s].count(r) — total quota s has ever transferred to r; each (s, r) slot is owned exclusively by s, so concurrent transfers from different donors to the same receiver compose without collision.

• spent[r] — total r has ever consumed. Transfers out do NOT bump spent — they move through transfers instead — so totalSpent reads as pure consumption.

Derived:

• quota(r) = initial[r] + Σ_s transfers[s].count(r) − Σ_t transfers[r].count(t) − spent[r]

• totalBudget = sum(initial) − sum(spent) (transfers conserved)

• totalSpent = sum(spent)

Rung 5a scope: the data type and local-decrement safety. The transfer-request protocol — how a low replica asks a peer to invoke transfer over a Seam, and rebalancing policy — is deferred to Rung 5b once the Seam replicator (Rung 12) exists.

Samples

val a = ReplicaId("A")
val b = ReplicaId("B")

var counter = BoundedCounter.init(mapOf(a to 5L, b to 3L))

// A spends 2 from its own quota.
val spendPatch = counter.trySpend(a, 2L) ?: error("quota sufficient")
counter = counter.piece(spendPatch)
check(counter.quota(a) == 3L)

// B transfers 1 unit to A.
val transferPatch = counter.transfer(from = b, to = a, amount = 1L) ?: error("quota sufficient")
counter = counter.piece(transferPatch)
check(counter.quota(a) == 4L)
check(counter.quota(b) == 2L)