-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
6 changed files
with
323 additions
and
19 deletions.
There are no files selected for viewing
175 changes: 175 additions & 0 deletions
175
doc/case-studies/xycloans/MCxycloans_monitor_simpler.ejs.tla
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,175 @@ | ||
| ------------------------------- MODULE MC ------------------------------- | ||
| <%# | ||
| /* | ||
| * An EJS template for generating the initial state from the aggregated | ||
| * state of the contract. | ||
| * | ||
| * Usage: | ||
| * | ||
| * npx ejs MCxycloans_monitor_simpler.ejs.tla -f state.json >MC.tla | ||
| * | ||
| * Igor Konnov, 2024 | ||
| */ | ||
| %> | ||
| (* THIS MODULE IS AUTOGENERATED FROM SOROBAN STATE *) | ||
| EXTENDS Integers, Apalache, xycloans_types | ||
|
|
||
| \* the set of all possible token amounts | ||
| AMOUNTS == Nat | ||
| \* the contract address for the xycLoans contract | ||
| XYCLOANS == "<%- contractId %>" | ||
| \* the token address | ||
| XLM_TOKEN_SAC_TESTNET == "<%- storage[contractId].instance.TokenId %>" | ||
|
|
||
| <% | ||
| const balanceAddrs = | ||
| Object.keys(storage[contractId].persistent) | ||
| .filter((key) => key.startsWith("Balance,")) | ||
| .map((key) => key.split(",")[1]) | ||
| %> | ||
| \* user-controlled addresses | ||
| USER_ADDR == { | ||
| <%- | ||
| balanceAddrs | ||
| .map((addr) => ` "${addr}"`) | ||
| .join(",\n") | ||
| %> | ||
| } | ||
|
|
||
| <% | ||
| const tokenAddrs = | ||
| Object.keys(storage[storage[contractId].instance.TokenId].persistent) | ||
| .filter((key) => key.startsWith("Balance,")) | ||
| .filter((key) => key !== `Balance,${contractId}`) | ||
| .map((key) => key.split(",")[1]) | ||
| %> | ||
| \* addresses that hold token balances | ||
| TOKEN_ADDR == { | ||
| <%- | ||
| tokenAddrs | ||
| .map((addr) => ` "${addr}"`) | ||
| .join(",\n") | ||
| %> | ||
| } | ||
|
|
||
| \* the pool of addresses to draw the values from | ||
| ADDR == { XYCLOANS, XLM_TOKEN_SAC_TESTNET } \union TOKEN_ADDR \union USER_ADDR | ||
|
|
||
| VARIABLES | ||
| \* @type: $tx; | ||
| last_tx, | ||
| \* Keep track of the current storage, | ||
| \* which can be only changed by a successful transaction. | ||
| \* @type: $storage; | ||
| storage | ||
|
|
||
| INSTANCE xycloans_monitor_simpler | ||
|
|
||
| <% | ||
| function renderKVStore(storage, prefix, mapper = (x) => x) { | ||
| return Object.keys(storage) | ||
| .filter((key) => key.startsWith(prefix)) | ||
| .map((key) => key.split(",")[1]) | ||
| .map((addr) => ` <<"${addr}", ${mapper(storage[prefix + addr])}>>`) | ||
| .join(",\n") | ||
| } | ||
| %> | ||
|
|
||
| Init == | ||
| LET init_stor == [ | ||
| self_instance |-> [ | ||
| FeePerShareUniversal |-> <%- storage[contractId].instance.FeePerShareUniversal %>, | ||
| TokenId |-> "<%- storage[contractId].instance.TokenId %>" | ||
| ], | ||
| self_persistent |-> [ | ||
| Balance |-> SetAsFun({ | ||
| <%- | ||
| renderKVStore(storage[contractId].persistent, "Balance,") | ||
| %> | ||
| }), | ||
| MaturedFeesParticular |-> SetAsFun({ | ||
| <%- | ||
| renderKVStore(storage[contractId].persistent, "MaturedFeesParticular,") | ||
| %> | ||
| }), | ||
| FeePerShareParticular |-> SetAsFun({ | ||
| <%- | ||
| renderKVStore(storage[contractId].persistent, "FeePerShareParticular,") | ||
| %> | ||
| }) | ||
| ], | ||
| token_persistent |-> [ Balance |-> SetAsFun({ | ||
| <%- | ||
| renderKVStore(storage[storage[contractId].instance.TokenId].persistent, "Balance,", (x) => x.amount) | ||
| %> | ||
| })] | ||
| ] | ||
| IN | ||
| \* initialize the contract state that we model | ||
| /\ last_tx = [ | ||
| call |-> Constructor(XYCLOANS), | ||
| status |-> TRUE, | ||
| env |-> [ | ||
| current_contract_address |-> XYCLOANS, | ||
| storage |-> init_stor, | ||
| old_storage |-> init_stor | ||
| ] | ||
| ] | ||
| /\ storage = init_stor | ||
|
|
||
| Next == | ||
| \* Generate some values for the storage. | ||
| \* For value generation, we go over all addresses, not subsets of addresses. | ||
| \E fpsu \in AMOUNTS, tid \in { "", XLM_TOKEN_SAC_TESTNET }: | ||
| \E b, mfp, fpsp, tb \in [ ADDR -> AMOUNTS ]: | ||
| LET new_stor == [ | ||
| self_instance |-> [ FeePerShareUniversal |-> fpsu, TokenId |-> tid ], | ||
| self_persistent |-> | ||
| [ Balance |-> b, MaturedFeesParticular |-> mfp, FeePerShareParticular |-> fpsp ], | ||
| token_persistent |-> [ Balance |-> tb ] | ||
| ] | ||
| env == [ | ||
| current_contract_address |-> XYCLOANS, | ||
| storage |-> new_stor, | ||
| old_storage |-> storage | ||
| ] | ||
| IN | ||
| \E addr \in USER_ADDR, amount \in AMOUNTS, success \in BOOLEAN: | ||
| /\ \/ LET tx == [ env |-> env, call |-> Initialize(XLM_TOKEN_SAC_TESTNET), status |-> success ] IN | ||
| initialize(tx) /\ last_tx' = tx | ||
| \/ LET tx == [ env |-> env, call |-> Deposit(addr, amount), status |-> success ] IN | ||
| deposit(tx) /\ last_tx' = tx | ||
| \/ LET tx == [ env |-> env, call |-> Borrow(addr, amount), status |-> success ] IN | ||
| borrow(tx) /\ last_tx' = tx | ||
| \/ LET tx == [ env |-> env, call |-> UpdateFeeRewards(addr), status |-> success ] IN | ||
| update_fee_rewards(tx) /\ last_tx' = tx | ||
| \/ LET tx == [ env |-> env, call |-> WithdrawMatured(addr), status |-> success ] IN | ||
| withdraw_matured(tx) /\ last_tx' = tx | ||
| \/ LET tx == [ env |-> env, call |-> Withdraw(addr, amount), status |-> success ] IN | ||
| withdraw(tx) /\ last_tx' = tx | ||
| /\ storage' = IF success THEN new_stor ELSE storage | ||
|
|
||
| \* restrict the executions to the successful transactions | ||
| NextOk == | ||
| Next /\ last_tx'.status | ||
|
|
||
| \* a core invariant that should be always satisfied | ||
| SolvencyInv == | ||
| \* NOTE: we can use TotSupply of the contract storage, if we add it to the storage definitions | ||
| LET Add(sum, addr) == sum + storage.self_persistent.Balance[addr] | ||
| totSupply == ApaFoldSet(Add, 0, DOMAIN storage.self_persistent.Balance) | ||
| IN | ||
| totSupply <= get_or_else(storage.token_persistent.Balance, XYCLOANS, 0) | ||
|
|
||
| \* use this falsy invariant to generate examples of successful transactions | ||
| NoSuccessInv == | ||
| ~IsConstructor(last_tx.call) => ~last_tx.status | ||
|
|
||
| \* use this invariant to generate transactions that are both successful and lead to insolvency | ||
| NoSuccessOrSolventInv == | ||
| NoSuccessInv \/ SolvencyInv | ||
|
|
||
| \* use this view to generate better test coverage | ||
| \* apalache-mc check --max-error=10 --length=10 --inv=NoSuccessInv --view=View MCxycloans_monitor.tla | ||
| View == <<last_tx.status, VariantTag(last_tx.call)>> | ||
| ========================================================================================= |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,23 @@ | ||
| ------------------------------ MODULE defs ------------------------------------ | ||
| (* | ||
| * Common definitions for the xycloans contract. | ||
| *) | ||
| EXTENDS Integers, xycloans_types | ||
|
|
||
| \* @type: ($tx, Bool) => Bool; | ||
| reverts_if(tx, cond) == cond => ~tx.status | ||
| \* @type: ($tx, Bool) => Bool; | ||
| succeeds_with(tx, cond) == tx.status => cond | ||
| \* @type: (Str -> a, Str, a) => a; | ||
| get_or_else(map, key, default) == | ||
| IF key \in DOMAIN map THEN map[key] ELSE default | ||
| \* integer division with rounding up | ||
| div_ceil(a, b) == (a + (b - 1)) \div b | ||
| \* integer division with rounding down | ||
| div_floor(a, b) == a \div b | ||
| \* @type: ($env, Str) => Int; | ||
| token_balance(env, a) == get_or_else(env.storage.token_persistent.Balance, a, 0) | ||
| \* @type: ($env, Str) => Int; | ||
| old_token_balance(env, a) == get_or_else(env.old_storage.token_persistent.Balance, a, 0) | ||
|
|
||
| =============================================================================== |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,97 @@ | ||
| ---------------------- MODULE xycloans_monitor_simpler ------------------------- | ||
| (* | ||
| * A simpler monitor for the xycLoans contract to detect the known issue. | ||
| * We have understood that input generation for a single step allows us | ||
| * to keep the monitor simple, in comparison to multiple steps. | ||
| * | ||
| * Igor Konnov, 2024 | ||
| *) | ||
|
|
||
| EXTENDS Integers, defs, xycloans_types | ||
|
|
||
| STROOP == 10000000 | ||
|
|
||
| CONSTANT | ||
| \* The token address for the xycLoans contract. | ||
| \* @type: Str; | ||
| XLM_TOKEN_SAC_TESTNET | ||
|
|
||
| \* @type: $tx => Bool; | ||
| initialize(tx) == | ||
| LET call == AsInitialize(tx.call) IN | ||
| /\ IsInitialize(tx.call) | ||
| /\ reverts_if(tx, tx.env.old_storage.self_instance.TokenId /= "") | ||
| /\ succeeds_with(tx, tx.env.storage.self_instance.TokenId = XLM_TOKEN_SAC_TESTNET) | ||
|
|
||
| \* @type: $tx => Bool; | ||
| deposit(tx) == | ||
| LET call == AsDeposit(tx.call) | ||
| token == tx.env.old_storage.self_instance.TokenId | ||
| IN | ||
| /\ IsDeposit(tx.call) | ||
| \* the pool has received `amount` tokens | ||
| /\ LET self == tx.env.current_contract_address IN | ||
| /\ succeeds_with(tx, token_balance(tx.env, self) = old_token_balance(tx.env, self) + call.amount) | ||
| \* the balance of the sender is increased by the amount | ||
| /\ succeeds_with(tx, | ||
| tx.env.storage.self_persistent.Balance = | ||
| [ tx.env.old_storage.self_persistent.Balance EXCEPT ![call.from] = @ + call.amount ]) | ||
|
|
||
| \* @type: $tx => Bool; | ||
| borrow(tx) == | ||
| \* note that we do not compute the fees here, as it may require good understanding of the protocol | ||
| LET call == AsBorrow(tx.call) | ||
| token == tx.env.old_storage.self_instance.TokenId | ||
| IN | ||
| /\ IsBorrow(tx.call) | ||
| \* the receiver paid the expected fee to the pool | ||
| /\ LET rcvr == call.receiver_id | ||
| self == tx.env.current_contract_address IN | ||
| /\ succeeds_with(tx, old_token_balance(tx.env, call.receiver_id) >= call.amount) | ||
| /\ succeeds_with(tx, token_balance(tx.env, rcvr) = old_token_balance(tx.env, rcvr) - call.amount) | ||
| /\ succeeds_with(tx, token_balance(tx.env, self) = old_token_balance(tx.env, self) + call.amount) | ||
| /\ succeeds_with(tx, call.amount > 0) | ||
| /\ succeeds_with(tx, tx.env.storage.self_instance.TokenId = token) | ||
|
|
||
| \* @type: $tx => Bool; | ||
| update_fee_rewards(tx) == | ||
| \* note that we do not compute the fees here, as it may require good understanding of the protocol | ||
| LET call == AsUpdateFeeRewards(tx.call) | ||
| token == tx.env.old_storage.self_instance.TokenId | ||
| IN | ||
| /\ IsUpdateFeeRewards(tx.call) | ||
| /\ succeeds_with(tx, tx.env.storage.self_instance.TokenId = token) | ||
| /\ succeeds_with(tx, tx.env.storage.token_persistent = tx.env.old_storage.token_persistent) | ||
|
|
||
| \* @type: $tx => Bool; | ||
| withdraw_matured(tx) == | ||
| \* note that we do not compute the fees here, as it may require good understanding of the protocol | ||
| LET call == AsWithdrawMatured(tx.call) | ||
| token == tx.env.old_storage.self_instance.TokenId | ||
| IN | ||
| /\ IsWithdrawMatured(tx.call) | ||
| /\ succeeds_with(tx, tx.env.storage.self_instance.TokenId = token) | ||
| \* otherwise, the contract reverts | ||
| /\ succeeds_with(tx, tx.env.old_storage.self_persistent.MaturedFeesParticular[call.addr] > 0) | ||
| \* the pool gets smaller | ||
| /\ LET self == tx.env.current_contract_address IN | ||
| \E amount \in Nat: | ||
| \* we do not want into a precise computation, but only specify the conditions | ||
| /\ (amount > 0) <=> (tx.env.old_storage.self_persistent.MaturedFeesParticular[call.addr] > 0) | ||
| /\ succeeds_with(tx, token_balance(tx.env, self) = old_token_balance(tx.env, self) - amount) | ||
|
|
||
| \* @type: $tx => Bool; | ||
| withdraw(tx) == | ||
| \* note that we do not compute the fees here, as it may require good understanding of the protocol | ||
| LET call == AsWithdraw(tx.call) | ||
| token == tx.env.old_storage.self_instance.TokenId | ||
| IN | ||
| /\ IsWithdraw(tx.call) | ||
| /\ succeeds_with(tx, tx.env.storage.self_instance.TokenId = token) | ||
| \* the pool gets smaller by the amount | ||
| /\ LET self == tx.env.current_contract_address IN | ||
| /\ succeeds_with(tx, old_token_balance(tx.env, self) - call.amount >= 0) | ||
| /\ succeeds_with(tx, | ||
| token_balance(tx.env, self) = old_token_balance(tx.env, self) - call.amount) | ||
|
|
||
| ============================================================================= |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters