dynamis-specs/RateLimiterInductive.tla at main · DynamisNetwork/dynamis-specs · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
---------------------- MODULE RateLimiterInductive ----------------------
(*
 * Inductive TLA+ Specification for RateLimiter
 *
 * Uses a strengthened inductive invariant for efficient verification.
 *)

EXTENDS Integers, FiniteSets, TLC

CONSTANTS
    CLIENTS,        \* Set of client IPs
    LIMIT,          \* Max requests per window
    WINDOW_MS       \* Window duration in ms

ASSUME LIMIT > 0
ASSUME WINDOW_MS > 0
ASSUME LIMIT \in Nat
ASSUME WINDOW_MS \in Nat

VARIABLES
    count,          \* count[c] = number of requests in current window
    windowStart,    \* windowStart[c] = timestamp when window started
    clock           \* Global clock (ms)

vars == <<count, windowStart, clock>>

-----------------------------------------------------------------------------
(* Type Invariant - Simplified for induction *)

MaxClock == 1000  \* Bound for inductive checking

TypeOK ==
    /\ count \in [CLIENTS -> 0..LIMIT]
    /\ windowStart \in [CLIENTS -> 0..MaxClock]
    /\ clock \in 0..MaxClock

-----------------------------------------------------------------------------
(* The Inductive Invariant *)

InductiveInvariant ==
    /\ TypeOK
    \* Core safety: count never exceeds limit
    /\ \A c \in CLIENTS : count[c] <= LIMIT
    \* Window consistency: windowStart is always <= clock
    /\ \A c \in CLIENTS : windowStart[c] <= clock

-----------------------------------------------------------------------------
(* Initial State *)

Init ==
    /\ count = [c \in CLIENTS |-> 0]
    /\ windowStart = [c \in CLIENTS |-> 0]
    /\ clock = 0

-----------------------------------------------------------------------------
(* Actions *)

MakeRequest(c) ==
    LET
        windowExpired == (clock - windowStart[c]) > WINDOW_MS
    IN
    IF windowExpired THEN
        /\ count' = [count EXCEPT ![c] = 1]
        /\ windowStart' = [windowStart EXCEPT ![c] = clock]
        /\ UNCHANGED clock
    ELSE IF count[c] < LIMIT THEN
        /\ count' = [count EXCEPT ![c] = @ + 1]
        /\ UNCHANGED <<windowStart, clock>>
    ELSE
        /\ UNCHANGED vars

Tick ==
    /\ clock < MaxClock
    /\ clock' = clock + 1
    /\ UNCHANGED <<count, windowStart>>

ExpireAllWindows ==
    /\ clock + WINDOW_MS + 1 <= MaxClock
    /\ clock' = clock + WINDOW_MS + 1
    /\ UNCHANGED <<count, windowStart>>

-----------------------------------------------------------------------------
(* Next State *)

Next ==
    \/ \E c \in CLIENTS : MakeRequest(c)
    \/ Tick
    \/ ExpireAllWindows

-----------------------------------------------------------------------------
(* Safety Property *)

Safety == \A c \in CLIENTS : count[c] <= LIMIT

-----------------------------------------------------------------------------
Spec == Init /\ [][Next]_vars

=============================================================================