Ledger

---- MODULE Ledger ---- (***************************************************************************) (* The tabby group-expense ledger (Splitwise-style), balances derived. *) (* *) (* Balances are never stored: Net(u) is derived from the expense log and *) (* the payments table. Expenses split by the exact remainder rule (first *) (* amt % n participants in a fixed user ordering pay one extra unit). *) (* Payments are keyed by a client-generated id: Propose binds a transfer *) (* suggested by greedy settlement over CURRENT nets to a fresh id; Submit *) (* records it iff the id is unset (SQL INSERT OR IGNORE); Resubmit is a *) (* no-op. AddExpense may interleave with Propose/Submit, so a payment can *) (* be recorded against a stale suggestion -- conservation must still hold. *) (* Payment method (XMR vs cash) and recorder (payer or recipient) are *) (* metadata: both reach the ledger as the same idempotent Transfer row. *) (* Cash adds ProposeCash: an ARBITRARY transfer ("they handed me $300") *) (* bound to a fresh id, unconstrained by the greedy suggestions, so nets *) (* may overshoot and flip sign -- conservation must survive that too. *) (***************************************************************************) EXTENDS Integers, Sequences, FiniteSets CONSTANTS Users, \* model values: group members MaxAmt, \* max single-expense amount (abstract units) MaxExpenses, \* bound on the expense log PaymentIds, \* model values: client-generated payment ids NULL \* absent row / unbound attempt ASSUME MaxAmt >= 1 /\ MaxExpenses >= 1 (* ---- Fixed deterministic user ordering (models ORDER BY user id) ---- *) RECURSIVE SetToSeq(_) SetToSeq(S) == IF S = {} THEN <<>> ELSE LET x == CHOOSE x \in S : TRUE IN <<x>> \o SetToSeq(S \ {x}) UserSeq == SetToSeq(Users) NU == Cardinality(Users) Idx(u) == CHOOSE i \in 1..NU : UserSeq[i] = u PidSeq == SetToSeq(PaymentIds) Min(a, b) == IF a < b THEN a ELSE b RECURSIVE SumSeq(_) SumSeq(s) == IF s = <<>> THEN 0 ELSE Head(s) + SumSeq(Tail(s)) MaxTotal == MaxAmt * MaxExpenses \* Multi-person expenses only: single-participant expenses shift one \* pairwise IOU and exercise no remainder/settlement structure; excluding \* them keeps the model finite-small. SplitSets == {P \in SUBSET Users : Cardinality(P) >= 2} Expense == [payer: Users, parts: SplitSets, amt: 1..MaxAmt] Transfer == [from: Users, to: Users, amt: 1..(2 * MaxTotal)] VARIABLES expenses, \* Seq(Expense): append-only expense log payments, \* [PaymentIds -> Transfer \cup {NULL}]: recorded payment rows attempts \* [PaymentIds -> Transfer \cup {NULL}]: transfer bound at propose vars == <<expenses, payments, attempts>> (* ---- Exact remainder split rule ---- *) ShareOf(e, u) == IF u \notin e.parts THEN 0 ELSE LET n == Cardinality(e.parts) base == e.amt \div n r == e.amt % n pseq == SelectSeq(UserSeq, LAMBDA v : v \in e.parts) k == CHOOSE i \in 1..n : pseq[i] = u IN base + (IF k <= r THEN 1 ELSE 0) (* ---- Derived balances (never stored) ---- *) Paid(u) == SumSeq([i \in 1..Len(expenses) |-> IF expenses[i].payer = u THEN expenses[i].amt ELSE 0]) Owed(u) == SumSeq([i \in 1..Len(expenses) |-> ShareOf(expenses[i], u)]) Sent(u) == SumSeq([i \in 1..Len(PidSeq) |-> LET p == payments[PidSeq[i]] IN IF p # NULL /\ p.from = u THEN p.amt ELSE 0]) Recv(u) == SumSeq([i \in 1..Len(PidSeq) |-> LET p == payments[PidSeq[i]] IN IF p # NULL /\ p.to = u THEN p.amt ELSE 0]) Net(u) == Paid(u) - Owed(u) + Sent(u) - Recv(u) NetF == [u \in Users |-> Net(u)] (* ---- Greedy settlement: largest debtor pays largest creditor, ---- *) (* ---- deterministic tiebreak by user order ---- *) RECURSIVE GreedyRec(_) GreedyRec(f) == IF \A u \in Users : f[u] = 0 THEN <<>> ELSE LET debtors == {u \in Users : f[u] < 0} creditors == {u \in Users : f[u] > 0} d == CHOOSE u \in debtors : \A v \in debtors : f[u] < f[v] \/ (f[u] = f[v] /\ Idx(u) <= Idx(v)) c == CHOOSE u \in creditors : \A v \in creditors : f[u] > f[v] \/ (f[u] = f[v] /\ Idx(u) <= Idx(v)) m == Min(0 - f[d], f[c]) IN <<[from |-> d, to |-> c, amt |-> m]>> \o GreedyRec([f EXCEPT ![d] = @ + m, ![c] = @ - m]) RECURSIVE ApplyRec(_, _) ApplyRec(f, ts) == IF ts = <<>> THEN f ELSE LET t == Head(ts) IN ApplyRec([f EXCEPT ![t.from] = @ + t.amt, ![t.to] = @ - t.amt], Tail(ts)) (* ---- Actions ---- *) Init == /\ expenses = <<>> /\ payments = [id \in PaymentIds |-> NULL] /\ attempts = [id \in PaymentIds |-> NULL] AddExpense == /\ Len(expenses) < MaxExpenses /\ \E e \in Expense : expenses' = Append(expenses, e) /\ UNCHANGED <<payments, attempts>> \* A client renders the greedy settlement over CURRENT nets and binds one \* of its suggested transfers to a fresh client-generated id. Nets may \* change (AddExpense) before the submit lands: the stale-suggestion race. \* (\E f \in {NetF} forces the derived nets to a concrete value before the \* recursive settlement walks over them.) ProposePayment == \E id \in PaymentIds : /\ attempts[id] = NULL /\ \E f \in {NetF} : LET ts == GreedyRec(f) IN /\ ts # <<>> /\ \E i \in 1..Len(ts) : attempts' = [attempts EXCEPT ![id] = ts[i]] /\ UNCHANGED <<expenses, payments>> \* Cash settles out-of-band at any amount, recorded by either party: the \* bound transfer is arbitrary, not one of the greedy suggestions. ProposeCash == \E id \in PaymentIds : /\ attempts[id] = NULL /\ \E from \in Users, to \in Users, amt \in 1..MaxAmt : /\ from # to /\ attempts' = [attempts EXCEPT ![id] = [from |-> from, to |-> to, amt |-> amt]] /\ UNCHANGED <<expenses, payments>> \* INSERT OR IGNORE: the row is written iff the id is unset. SubmitPayment == \E id \in PaymentIds : /\ attempts[id] # NULL /\ payments[id] = NULL /\ payments' = [payments EXCEPT ![id] = attempts[id]] /\ UNCHANGED <<expenses, attempts>> \* Redelivery of an already-recorded id (double tap / network retry): \* the IGNORE branch fires and nothing changes. ResubmitPayment == \E id \in PaymentIds : /\ attempts[id] # NULL /\ payments[id] # NULL /\ payments' = payments /\ UNCHANGED <<expenses, attempts>> Next == AddExpense \/ ProposePayment \/ ProposeCash \/ SubmitPayment \/ ResubmitPayment Spec == Init /\ [][Next]_vars (* ---- Invariants ---- *) TypeOK == /\ Len(expenses) <= MaxExpenses /\ \A i \in 1..Len(expenses) : expenses[i] \in Expense /\ payments \in [PaymentIds -> Transfer \cup {NULL}] /\ attempts \in [PaymentIds -> Transfer \cup {NULL}] \* Money is conserved: derived nets always sum to zero, even when a \* payment was recorded against a stale suggestion. Conservation == SumSeq([i \in 1..NU |-> Net(UserSeq[i])]) = 0 \* The remainder rule distributes every expense exactly. SharesExact == \A i \in 1..Len(expenses) : SumSeq([k \in 1..NU |-> ShareOf(expenses[i], UserSeq[k])]) = expenses[i].amt \* Greedy settlement zeroes all nets in at most |Users|-1 transfers. SettlementSound == \A f \in {NetF} : LET ts == GreedyRec(f) IN /\ Len(ts) <= NU - 1 /\ \A u \in Users : ApplyRec(f, ts)[u] = 0 \* A recorded row is exactly the attempt bound to its id. IdempotentPayments == \A id \in PaymentIds : payments[id] # NULL => payments[id] = attempts[id] \* Once written, a payment row never changes (action property). NoOverwrite == [][\A id \in PaymentIds : payments[id] # NULL => payments'[id] = payments[id]]_vars ====

CONSTANTS Users = {u1, u2, u3} MaxAmt = 2 MaxExpenses = 1 PaymentIds = {p1, p2} NULL = NULL SPECIFICATION Spec INVARIANT TypeOK INVARIANT Conservation INVARIANT SharesExact INVARIANT SettlementSound INVARIANT IdempotentPayments PROPERTY NoOverwrite CHECK_DEADLOCK FALSE