solarkraft/doc/case-studies/timelock/token_balance.tla at cf26a544ab204220eab62a3545300cb689aa899b · freespek/solarkraft · 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
(*
 * Token balance effect monitor for the Timelock contract
 *
 * Andrey Kuprianov, 2024
 *)
---- MODULE token_balance ----

EXTENDS timelock

\* This trigger fires when the token balance of this contract is reduced
\* Notice that it will panic (won't fire) if balance record doesn't exist
MonitorTrigger_TokenBalance_BalanceReduced ==
    next_token_balance(Balance.token, env.current_contract_address) <
    token_balance(Balance.token, env.current_contract_address)

\* Only claim method is allowed to reduce this contract token balance
MonitorEffect_TokenBalance_AllowedToReduce ==
    tx.status = TRUE => tx.method_name = "claim"


\* Everything below is deterministic, and will be generated automatically
\* For now, we encode this manually

MonitorTrigger_TokenBalance ==
    \/ MonitorTrigger_TokenBalance_BalanceReduced

MonitorEffect_TokenBalance ==
    /\ MonitorEffect_TokenBalance_AllowedToReduce

Monitor_TokenBalance ==
    MonitorTrigger_TokenBalance => MonitorEffect_TokenBalance

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