Macaw.Auth.Native.Throttle as a model (spec/10 §7): the table of failures, shared by every sign-in in flight, and what each call does to it.

State. table is the ETS table, row for row: a set of {key, failures, last}, where a key is {:user, u} or {:ip, a} and last is the last-failure time. now is the clock. proc is each sign-in in flight: :idle, or admitted at ts and verifying its password, or part-way through recording its failure. Two history variables record a broken rule once it has happened: early_admit and address_lowered. truth is a ghost, the table as the throttle's rules define it: for each key, the failures counted since its last reset, and the latest of their times. The invariants hold the table to it.

Actions. attempt(p, u, a): Throttle.check/3 at now admits a sign-in from address a (:none is a caller with no address); the model has no refused attempt, since a refusal changes nothing. succeed(p): Throttle.success/1. fail(p): Throttle.failure/3 with the time the sign-in was admitted at, which may be older than now and older than another sign-in's failure. tick(d): time passes. sweep: Throttle.sweep/1 at now.

What is abstracted. A failure updates its keys one after another; the model updates them in one step. Every operation reads and writes one key alone (a sweep decides each key on its own row), so the order across keys changes nothing a key's own history shows. Within a key, the steps are kept as the code takes them. A check reads its keys in one step. A check and the failure that follows it are separate steps, as in the code: concurrent sign-ins can all be admitted before any of their failures is counted.

Time is a bounded integer (horizon), advanced by ticks. The constants are the code's (five free failures, a second, 15 minutes, a day) when the model is run against the code, and a scaled instance (one free failure, waits of 1 and 2, a sweep after 3) when it is checked exhaustively: the rules are the same, and the scaled waits keep the state space small. max_failures bounds the failures counted on a key: an attempt starts only on keys below it.

Three constants select the design (the default) or a defect, and the tests in test/macaw/auth/specs/ prove the checker finds each:

• atomic_stamp - a failure counts and stamps its key in one atomic step, keeping the later of the row's time and its own. false is the code as it shipped: an update_counter, then an update_element that writes its own time.
• atomic_increment - the count is an atomic increment. false is a lookup, then an insert, as a naive table would do.
• success_resets_address - false: a success forgets the username's count only. true forgets the address's too.