diff --git a/doc/case-studies/xycloans/MCxycloans_monitor_simpler.ejs.tla b/doc/case-studies/xycloans/MCxycloans_monitor_simpler.ejs.tla new file mode 100644 index 00000000..1e6adb19 --- /dev/null +++ b/doc/case-studies/xycloans/MCxycloans_monitor_simpler.ejs.tla @@ -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 == <> +========================================================================================= \ No newline at end of file diff --git a/doc/case-studies/xycloans/defs.tla b/doc/case-studies/xycloans/defs.tla new file mode 100644 index 00000000..0718edde --- /dev/null +++ b/doc/case-studies/xycloans/defs.tla @@ -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) + +=============================================================================== \ No newline at end of file diff --git a/doc/case-studies/xycloans/ingest.js b/doc/case-studies/xycloans/ingest.js index 6759e660..8905b76a 100755 --- a/doc/case-studies/xycloans/ingest.js +++ b/doc/case-studies/xycloans/ingest.js @@ -81,6 +81,17 @@ switch (callType) { callArgs = `update_fee_rewards --addr ${signer}` break + case 'WithdrawMatured': + signer = accounts[call.value.addr] + callArgs = `withdraw_matured --addr ${signer}` + break + + case 'Withdraw': + signer = accounts[call.value.addr] + const amount = call.value.amount["#bigint"] + callArgs = `withdraw --addr ${signer} --amount ${amount}` + break + default: console.error(`Unknown call type: ${callType}`) process.exit(1) diff --git a/doc/case-studies/xycloans/xycloans_monitor.tla b/doc/case-studies/xycloans/xycloans_monitor.tla index 71a70f21..74542eb5 100644 --- a/doc/case-studies/xycloans/xycloans_monitor.tla +++ b/doc/case-studies/xycloans/xycloans_monitor.tla @@ -12,7 +12,7 @@ * Igor Konnov, 2024 *) -EXTENDS Integers, xycloans_types +EXTENDS Integers, defs, xycloans_types STROOP == 10000000 @@ -33,24 +33,6 @@ VARIABLES \* @type: Int; fee_per_share_universal -(* The core logic of the monitor for the contract data *) - -\* @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) - \* @type: $tx => Bool; initialize(tx) == LET call == AsInitialize(tx.call) IN diff --git a/doc/case-studies/xycloans/xycloans_monitor_simpler.tla b/doc/case-studies/xycloans/xycloans_monitor_simpler.tla new file mode 100644 index 00000000..fe309d58 --- /dev/null +++ b/doc/case-studies/xycloans/xycloans_monitor_simpler.tla @@ -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) + +============================================================================= \ No newline at end of file diff --git a/doc/case-studies/xycloans/xycloans_types.tla b/doc/case-studies/xycloans/xycloans_types.tla index 3d279b2a..7c91208c 100644 --- a/doc/case-studies/xycloans/xycloans_types.tla +++ b/doc/case-studies/xycloans/xycloans_types.tla @@ -38,6 +38,8 @@ EXTENDS Variants | Deposit({ from: Str, amount: Int }) | Borrow({ receiver_id: Str, amount: Int }) | UpdateFeeRewards({ addr: Str}) + | WithdrawMatured({ addr: Str}) + | Withdraw({ addr: Str, amount: Int}) ; Finally, a transaction is: @@ -84,4 +86,18 @@ IsUpdateFeeRewards(call) == VariantTag(call) = "UpdateFeeRewards" \* @type: $call => { addr: Str }; AsUpdateFeeRewards(call) == VariantGetUnsafe("UpdateFeeRewards", call) +\* @type: Str => $call; +WithdrawMatured(addr) == Variant("WithdrawMatured", [ addr |-> addr ]) +\* @type: $call => Bool; +IsWithdrawMatured(call) == VariantTag(call) = "WithdrawMatured" +\* @type: $call => { addr: Str }; +AsWithdrawMatured(call) == VariantGetUnsafe("WithdrawMatured", call) + +\* @type: (Str, Int) => $call; +Withdraw(addr, amount) == Variant("Withdraw", [ addr |-> addr, amount |-> amount ]) +\* @type: $call => Bool; +IsWithdraw(call) == VariantTag(call) = "Withdraw" +\* @type: $call => { addr: Str, amount: Int }; +AsWithdraw(call) == VariantGetUnsafe("Withdraw", call) + =============================================================================== \ No newline at end of file