Applications

---------------------------- MODULE Applications ---------------------------- (***************************************************************************) (* Lifecycle of fee-paying applications in a government services portal. *) (* *) (* The backend is a single SQLite-style table `applications`. Every *) (* request is exactly ONE SQL statement, so each applies atomically, but *) (* requests may be duplicated (client retry, double-click) and interleave *) (* arbitrarily. The DB is modelled as a SET of rows so that "one row per *) (* id" is a real property of INSERT OR IGNORE, not of the representation. *) (* *) (* create(id,u): INSERT OR IGNORE (id, user_id=u, status=awaiting_payment)*) (* pay(id,u): UPDATE SET status=complete, reference=<fresh> *) (* WHERE id=? AND user_id=u AND status=awaiting_payment *) (* cancel(id,u): UPDATE SET status=cancelled *) (* WHERE id=? AND user_id=u AND status=awaiting_payment *) (* *) (* Because a request reads nothing before its single statement, an *) (* in-flight request is fully described by (kind, id, user); every *) (* interleaving of in-flight requests is some ordering of atomic applies, *) (* so each step below issues-and-applies one request. Duplicates are *) (* modelled by allowing the same request up to MaxPerKind times per id. *) (* *) (* References are a monotonically allocated counter (fresh per winning *) (* transition). The fee is a pure function of the application kind and is *) (* not modelled. *) (***************************************************************************) EXTENDS Naturals, FiniteSets CONSTANTS Users, \* set of user ids (model values) Ids, \* set of client-generated application ids (model values) Refs, \* finite set of naturals available as references MaxPerKind, \* how many requests of each kind may be applied per id NoRef \* sentinel: no reference assigned ASSUME NoRef \notin Refs ASSUME Cardinality(Refs) >= Cardinality(Ids) \* references never run out Kinds == {"create", "pay", "cancel"} Statuses == {"awaiting_payment", "complete", "cancelled"} Terminal == {"complete", "cancelled"} Ops == [kind: Kinds, id: Ids, user: Users] Rows == [id: Ids, owner: Users, status: Statuses, ref: Refs \cup {NoRef}] MinRef == CHOOSE r \in Refs : \A s \in Refs : r <= s MaxRef == CHOOSE r \in Refs : \A s \in Refs : r >= s VARIABLES db, \* set of rows in the applications table nextRef, \* next reference to allocate applied \* Ids x Kinds -> how many requests of that kind were applied vars == <<db, nextRef, applied>> RowsFor(i) == {r \in db : r.id = i} Init == /\ db = {} /\ nextRef = MinRef /\ applied = [x \in Ids \X Kinds |-> 0] (* Budget: the same request may arrive again (retry, double-click). *) Budget(o) == /\ applied[<<o.id, o.kind>>] < MaxPerKind /\ applied' = [applied EXCEPT ![<<o.id, o.kind>>] = @ + 1] (* INSERT OR IGNORE keyed on id. *) Create(o) == /\ o.kind = "create" /\ Budget(o) /\ IF RowsFor(o.id) = {} THEN db' = db \cup {[id |-> o.id, owner |-> o.user, status |-> "awaiting_payment", ref |-> NoRef]} ELSE UNCHANGED db /\ UNCHANGED nextRef (* Rows matched by the WHERE clause of pay/cancel. *) Matching(o) == {r \in db : r.id = o.id /\ r.owner = o.user /\ r.status = "awaiting_payment"} (* Conditional UPDATE; the server learns whether it won from changes(). *) Pay(o) == /\ o.kind = "pay" /\ Budget(o) /\ IF Matching(o) = {} THEN UNCHANGED <<db, nextRef>> ELSE /\ db' = (db \ Matching(o)) \cup {[r EXCEPT !.status = "complete", !.ref = nextRef] : r \in Matching(o)} /\ nextRef' = nextRef + 1 Cancel(o) == /\ o.kind = "cancel" /\ Budget(o) /\ IF Matching(o) = {} THEN UNCHANGED db ELSE db' = (db \ Matching(o)) \cup {[r EXCEPT !.status = "cancelled"] : r \in Matching(o)} /\ UNCHANGED nextRef Next == \E o \in Ops : Create(o) \/ Pay(o) \/ Cancel(o) Spec == Init /\ [][Next]_vars ----------------------------------------------------------------------------- (* Invariants *) TypeOK == /\ db \subseteq Rows /\ nextRef \in MinRef..(MaxRef + 1) /\ applied \in [Ids \X Kinds -> 0..MaxPerKind] (* At most one row per id: a duplicated create never inserts twice. *) NoDuplicateCreate == \A r1, r2 \in db : r1.id = r2.id => r1 = r2 (* A reference is present exactly on complete applications. *) RefIffComplete == \A r \in db : (r.status = "complete") <=> (r.ref \in Refs) (* No two applications share a reference. *) UniqueRefs == \A r1, r2 \in db : (r1.ref \in Refs /\ r1.ref = r2.ref) => r1 = r2 (* Exactly one reference was allocated per transition to complete: repeated/concurrent pay calls on one application cannot allocate twice. *) OneRefPerTransition == Cardinality({r \in db : r.status = "complete"}) = nextRef - MinRef ----------------------------------------------------------------------------- (* Action properties, checked as PROPERTY *) (* Once complete or cancelled, the row (status, reference, owner) is never touched again. *) TerminalStatesFrozen == [][\A r \in db : r.status \in Terminal => r \in db']_vars (* The owner is the creating user and never changes; a pay/cancel by any other user leaves the database untouched. *) OwnerOnly == [][ /\ \A r \in db : \E r2 \in db' : r2.id = r.id /\ r2.owner = r.owner /\ \A o \in Ops : (Pay(o) \/ Cancel(o)) => \A r \in db : r.owner # o.user => r \in db' ]_vars =============================================================================

SPECIFICATION Spec CONSTANTS Users = {u1, u2} Ids = {a, b} Refs = {1, 2, 3} MaxPerKind = 2 NoRef = NoRef INVARIANTS TypeOK NoDuplicateCreate RefIffComplete UniqueRefs OneRefPerTransition PROPERTIES TerminalStatesFrozen OwnerOnly CHECK_DEADLOCK FALSE